Email Gateway (Aug 18 2022 at 18:40): Email Gateway (Aug 18 2022 at 18:40):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi,
when I declare an shorthand via (is "?A") in an obtain statement, the shorthand
only becomes bound after the proof has been completed. Why is this? For ordinary
have and show, I can use such shortcuts inside the proof. Is this different
behaviour intended?
Here's an example:
notepad begin
fix f :: "'a => 'b"
obtain x y where "f x = y" (is "?A x y")
(* term "?A" fails *)
proof -
(* term "?A" fails *)
show thesis sorry
qed
term ?A (* works *)
have "f x = y" (is "?A x y")
proof -
term "?A" (* works *)
show ?thesis sorry
qed
end
Andreas
Email Gateway (Aug 19 2022 at 11:18):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear all,
I ran into an issue related to one that was reported on this list before
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-November/msg00002.html,
by Andreas Lochbihler) but didn't get answered back then.
Is there a way of abbreviating, with '(is "<abbrev-pattern>")', terms in
a statement involving 'obtain … where "<term>"' or 'obtains … where
"<term>"' such that the abbreviations are usable in the proof of the
statement? Or, if there is no such way, is there are particular reason
for why this is not possible?
I encountered this in a lemma roughly structured as follows:
lemma
assumes …
obtains thing where "prop1 thing" (* actually a lengthy expression *)
and "prop2 thing"
proof -
from assms obtain thing
where "prop1 thing"
and "prop2 thing"
… (* proof *)
then show ?thesis ..
qed
I would have liked to abbreviate this to, e.g.,
lemma
assumes …
obtains thing where "prop1 thing" (is "?prop1")
and "prop2 thing" (is "?prop2")
proof -
from assms obtain thing
where "?prop1"
and "?prop2"
… (* proof *)
then show ?thesis ..
qed
Cheers, and thanks in advance for any help,
Christoph
Last updated: May 01 2024 at 20:18 UTC