Email Gateway (Aug 22 2022 at 19:05): Email Gateway (Aug 22 2022 at 19:05):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I learned from Makarius yesterday that these things are not generally
intended to be possible with Isar (see the mailing list thread “How can
I access a fact statement as a term?”). That said, there are ways to get
at least closer to what you want.
The key is, in my opinion, the ?case variable. While it won’t give you
access to the subgoals of the proof–qed block, it at least can give
you access to their conclusions.
The induction and cases proof methods create named cases, and a
case statement subsequently introduces the ?case variable for the
specified case. You can make this mechanism available for other proof
methods by means of the goal_cases method. For example, you can write:
lemma "(z :: int) < 0 ∨ z > 0 ⟹ ¦z¦ ≠ 0"
proof (elim disjE, goal_cases negative positive)
case negative
then show ?case by simp
next
case positive
then show ?case by simp
qed
This approach works very well for me when defining shortcuts for complex
proof method expressions via Eisbach: I just put the application of
goal_cases into the shortcut definition, so that in the Isar proofs I
only have a single application of my custom proof method, which
generates the named cases for me. In the above example I would have the
Eisbach definition
method negative_positive =
(elim disjE, goal_cases negative positive)
and then start the proof of the lemma with proof negative_positive.
As soon as you have ?case available, you can match it against a
pattern to get hold of parts of it. For instance, you could add the line
let "_ ≠ ?zero" = ?case
to the above code after case negative, and this would result in
?zero being 0 :: int.
All the best,
Wolfgang
Last updated: Apr 26 2024 at 08:19 UTC