[isabelle-dev] Safe approach to hypothesis substitution

[Makarius]

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.

The LCF type discipline of the kernel prevents proving wrong results, but 
it does not prevent breaking tools, or violating higher structuring 
principles.  One very important one is independence on logical details of 
the derivation of previous results.  E.g. tools need to work uniformly for 
assumptions or derived facts, fixed parameters or locally defined 
entities.  For historical reasons one can also have Frees that are not 
fixed in the context, or hyps that are not assumed.


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

or

   obtain "P x" sorry

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


 	Makarius