[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

On 08/24/2010 10:51 PM, Makarius wrote:
> On Tue, 24 Aug 2010, Andreas Schropp wrote:
>
>> And actually any tactic can peek at the assumptions, via examination 
>> of the hyps of the goal-state
>
> 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.

Section 3.2 only lists the following

         The main well-formedness conditions for proper tactics are
    summarized
    as follows.
         · General tactic failure is indicated by an empty result, only
    serious faults
            may produce an exception.
         · The main conclusion must not be changed, apart from instantiating
            schematic variables.
         · A tactic operates either uniformly on all subgoals, or
    specifically on a
            selected subgoal (without bumping into unrelated subgoals).
         · Range errors in subgoal addressing produce an empty result.

Can someone provide a full list?
Is everybody respecting all of them? I don't even know them ...

BTW: this email asks a lot of questions about conformity to seemingly
undocumented design principles.
Please don't mistake that for aggressiveness or something. ^^

>
> The LCF type discipline of the kernel prevents proving wrong results, 
> but it does not prevent breaking tools, or violating higher 
> structuring principles. 

What are those higher structuring principles?
What does violation of them imply?

> One very important one is independence on logical details of the 
> derivation of previous results.

This forbids any tools using proof terms, e.g.
Extraction, AWE, unoverloading, HOL->ZF.

What is the motivation behind our proof terms if it is
considered a well-formedness violation to use them?

> E.g. tools need to work uniformly for assumptions or derived facts, 
> fixed parameters or locally defined entities.

This means I should not do a case distinction based on if something is 
an assumption etc?
That sounds reasonable, but why is it important?
Logically an assumption is quite different from a derived fact:
   introducing an assumption weakens your results, whereas introducing a 
derived fact
never does. Why do we try to blur the line here?

What does this say about our equality-elimination criterion, which wants 
to check if there
are any assumptions involving a Free?


> For historical reasons one can also have Frees that are not fixed in 
> the context, or hyps that are not assumed.

So is that a higher structuring principle?
Can you list some more with motivations behind them?

>
>
> 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:
>
>   have "P x" sorry

This doesn't change the assumptions, so no interaction with
that equality-elimination safeness approximation idea?

>
> or
>
>   obtain "P x" sorry

This adds the assumption "P x", so hyps x=t are not
eliminated, which may be more conservative than
we need it to be, if there is no further assumption on x
(but how realistic is that?).

What is obtain without a where clause good for? It looks
like a complicated way to write a  have "P x".
The behaviour wrt
   obtain x where "P x"
is right:
   this adds fix x assume "P x", so hyps x=t are not
eliminated, which is correct because we don't know "P t"
so the elimination would loose information.

>
> These are just necessariy conditions on structural integrity wrt. the 
> context, not sufficient ones.

And are there sufficient ones? Is structural integrity of contexts
important for that equality-elimination safeness approximation idea?

Where is structural integrity of contexts used and established?

You mentioned above that

       "For historical reasons one can also have Frees that are not
    fixed in the context, or hyps that are not assumed.",

so this is not part of structural integrity for contexts?



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100825/e688138a/attachment-0002.html>