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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
