Email Gateway (Aug 19 2022 at 10:32): Email Gateway (Aug 19 2022 at 10:32):From: "W. Li" <wl302@cam.ac.uk>
Dear Isabelle pros,
I have encountered a tricky problem with Isabelle locales. Is there anyone
kind enough to help?
Suppose we have a dummy locale and a definition:
locale dummy = fixes x::bool assumes x_true:x
definition (in dummy) f::bool where "f ≡ ∀y::bool. y∨x"
We can show the following lemma by unfolding 'f' first:
lemma (in dummy) f
proof (unfold f_def,rule)
fix y
show "y∨x" using x_true by auto
qed
However, when trying to prove a similar lemma, I don't know how to unfold
'f' :(
lemma (in dummy) "dummy.f True"
Any help is highly appreciated.
Best regards,
Wenda Li
Email Gateway (Aug 19 2022 at 10:32):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
first of all, I cannot quite see the purpose of declaring the second
lemma as "in dummy".
The reason why you cannot simply unfold the definition of f in your
second lemma is that the definition lemma dummy.f_def is conditional:
Try "thm dummy.f_def" and you'll get:
dummy ?x ⟹ dummy.f ?x ≡ ∀y. y ∨ ?x
i.e. your definition of is is conditional; it only exists inside the
locale, and therefore you must first prove that the assumptions of the
locale hold, i.e. "dummy True" in your case, since you want to show that
"dummy.f True" holds; "True" is the parameter x that you give to the
locale. Your proof could then look like this:
What you can do is this:
lemma "dummy.f True"
proof-
have "dummy True" by (unfold_locales, rule)
from dummy.f_def[OF this] show "dummy.f True" by simp
qed
Cheers,
Manuel
Last updated: Apr 25 2024 at 20:15 UTC