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.