Email Gateway (Aug 18 2022 at 20:29): Email Gateway (Aug 18 2022 at 20:29):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 18 2022 at 20:31):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 08:11):From: Ramana Kumar <rk436@cam.ac.uk>
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.
While I'm asking, in the description of resolution and assumption rules on
the top half of that page, is it assumed that any subgoal can be worked on,
or does it have to be the leftmost one? If the former is true it would be
better if the example demonstrated that.
Finally, if anyone knows about the proof terms that can be recorded, I'd
love to eventually know exactly how (or whether) they relate to which parts
of Isabelle reasoning. Do they perhaps encode resolution and assumption
applications? Anything else?
Email Gateway (Aug 19 2022 at 08:12):From: Tobias Nipkow <nipkow@in.tum.de>
The proof terms encode the primitive inferences in the framework logic, i.e. ==,
==> and !!. For details see
http://www21.in.tum.de/~nipkow/pubs/tphols00.html
Tobias
Last updated: Apr 19 2024 at 01:05 UTC