# Re: [isabelle] typo in isar-ref?

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.

I guess, the trace should correspond to the following apply-script:
ML {*
fun my_print_tac ctxt thm =
let
fun pretty_thm_no_vars ctxt thm =
let
val ctxt' = Config.put show_question_marks false ctxt
in Syntax.pretty_term ctxt' (prop_of thm) end
val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
in Seq.single thm end
*}
notation "prop" ("#(_)")
lemma "A ∧ B ⟹ B ∧ A"
apply (tactic {* my_print_tac @{context} *})
apply (rule conjI [of B A])
apply (tactic {* my_print_tac @{context} *})
apply (rule conjunct2 [of A B])
apply (tactic {* my_print_tac @{context} *})
apply assumption
apply (tactic {* my_print_tac @{context} *})
apply (rule conjunct1 [of A B])
apply (tactic {* my_print_tac @{context} *})
apply assumption
apply (tactic {* my_print_tac @{context} *})
done

`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".
`
cheers
chris

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