Re: [isabelle] typo in isar-ref?



On Tue, 17 Jul 2012, Christian Sternagel wrote:

On 07/15/2012 04:52 PM, Ramana Kumar wrote:
I'm trying to understand exactly what Isabelle/HOL proofs are at a low
level so I have a chance at understanding how to extract OpenTheory proofs
for Isabelle/HOL theories.

On page 30 (pdf page 41) of isar-ref.pdf the example of goal oriented
reasoning is either wrong or too confusing for me. In particular the third
application of the resolution seems to introduce the wrong subgoal, and
then the application of assumption seems magical.

where we use "my_print_tac" to reproduce internal goal states as presented in isar-ref, "rule" stands for resolution with a given rule, and the rules conjI [of B A], conjunct2 [of A B], and conjunct1 [of A B] correspond to "B ==> A ==> B & A", "A & B ==> B", and "A & B ==> A", from the example trace.

Thus I agree that after the third "rule"-application the subgoal should be "A & B ==> A & B", rather than "A & B ==> B & A".

OK, I better change that. Most of the isar-ref manual is formally checked or generated from prover output, but this part is just some adhoc LaTeX-painting with tabular environment and some @{text} antiquotations to imitate the formal style of Isabelle.


While this rule composition framework is the main concept of Isabelle/Pure, it is not relevant for proof terms. The "assumption" and "resolution" inferences are derived rules on top of plain minimal logic over !! and ==> as explained by Larry in his early Isabelle papers from around 1989. The proof term layer by Berghofer and Nipkow expands these "derived primitives" on the fly, see here http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/proofterm.ML#l821

Note that "bicompose_aux" is a slight generalization of the resolution principle. You can see further in thm.ML and drule.ML how Larry makes the actual user-space d/e/f/res operations from that blueprint.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.