[isabelle-dev] Safe approach to hypothesis substitution

Makarius makarius at sketis.net
Tue Aug 24 22:51:01 CEST 2010

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


   obtain "P x" sorry

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


More information about the isabelle-dev mailing list