<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#ffffff">
On 08/24/2010 10:51 PM, Makarius wrote:
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite">On Tue, 24 Aug 2010, Andreas Schropp wrote:
<br>
<br>
<blockquote type="cite">And actually any tactic can peek at the
assumptions, via examination of the hyps of the goal-state
<br>
</blockquote>
<br>
A tactic must never peek at the "hyps" field of the goal state, and it
must never peek at the main goal being proved. See also section 3.2 in
the Isabelle/Isar implementation manual for some further
well-formedness conditions that cannot be enforced by the ML type
discipline.<br>
</blockquote>
<br>
Section 3.2 only lists the following<br>
<blockquote> The main well-formedness conditions for proper tactics
are summarized<br>
as follows.<br>
· General tactic failure is indicated by an empty result, only
serious faults<br>
may produce an exception.<br>
· The main conclusion must not be changed, apart from instantiating<br>
schematic variables.<br>
· A tactic operates either uniformly on all subgoals, or
specifically on a<br>
selected subgoal (without bumping into unrelated subgoals).<br>
· Range errors in subgoal addressing produce an empty result.<br>
</blockquote>
Can someone provide a full list?<br>
Is everybody respecting all of them? I don't even know them ...<br>
<br>
BTW: this email asks a lot of questions about conformity to seemingly<br>
undocumented design principles.<br>
Please don't mistake that for aggressiveness or something. ^^<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
The LCF type discipline of the kernel prevents proving wrong results,
but it does not prevent breaking tools, or violating higher structuring
principles. </blockquote>
<br>
What are those higher structuring principles?<br>
What does violation of them imply?<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite">One very important one is independence on logical details
of the derivation of previous results.</blockquote>
<br>
This forbids any tools using proof terms, e.g.<br>
Extraction, AWE, unoverloading, HOL->ZF.<br>
<br>
What is the motivation behind our proof terms if it is<br>
considered a well-formedness violation to use them?<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite">E.g. tools need to work uniformly for assumptions or
derived facts, fixed parameters or locally defined entities.</blockquote>
<br>
This means I should not do a case distinction based on if something is
an assumption etc?<br>
That sounds reasonable, but why is it important?<br>
Logically an assumption is quite different from a derived fact: <br>
introducing an assumption weakens your results, whereas introducing a
derived fact<br>
never does. Why do we try to blur the line here?<br>
<br>
What does this say about our equality-elimination criterion, which
wants to check if there<br>
are any assumptions involving a Free?<br>
<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite">For historical reasons one can also have Frees that are
not fixed in the context, or hyps that are not assumed.<br>
</blockquote>
<br>
So is that a higher structuring principle?<br>
Can you list some more with motivations behind them?<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
<br>
A good sanity check of some idea that involves the proof context is to
see how it interacts either with 'have' or 'obtain' in Isar. I.e. the
following should be conservative additions to the proof situation:
<br>
<br>
have "P x" sorry<br>
</blockquote>
<br>
This doesn't change the assumptions, so no interaction with<br>
that equality-elimination safeness approximation idea?<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
or
<br>
<br>
obtain "P x" sorry<br>
</blockquote>
<br>
This adds the assumption "P x", so hyps x=t are not<br>
eliminated, which may be more conservative than<br>
we need it to be, if there is no further assumption on x<br>
(but how realistic is that?).<br>
<br>
What is obtain without a where clause good for? It looks<br>
like a complicated way to write a have "P x".<br>
The behaviour wrt<br>
obtain x where "P x"<br>
is right:<br>
this adds fix x assume "P x", so hyps x=t are not<br>
eliminated, which is correct because we don't know "P t"<br>
so the elimination would loose information.<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1008242241180.17618@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
These are just necessariy conditions on structural integrity wrt. the
context, not sufficient ones.<br>
</blockquote>
<br>
And are there sufficient ones? Is structural integrity of contexts<br>
important for that equality-elimination safeness approximation idea?<br>
<br>
Where is structural integrity of contexts used and established?<br>
<br>
You mentioned above that <br>
<blockquote> "For historical reasons one can also have Frees that are
not<br>
fixed in the context, or hyps that are not assumed.",<br>
</blockquote>
so this is not part of structural integrity for contexts?<br>
<br>
<br>
<br>
</body>
</html>