Email Gateway (Aug 18 2022 at 15:26): Email Gateway (Aug 18 2022 at 15:26):From: Steve W <s.wong.731@gmail.com>
Hi,
Please correct my understanding of this situation. Suppose I have:
consts
a :: real
axioms
ax1: "f a = 0"
lemma lemma1: "EX func arg. func arg = 0"
proof -
show "g a = 0"
using ax1
by auto
qed
I cannot proceed to the line with the proof goal "g a = 0" because the type
implied by this proof goal is more specific than the lemma.
However, why is the following fine:
lemma lemma2: "EX func arg. func arg = 0"
proof -
have "g a = 0"
using ax1
by auto
show ?thesis
by auto
qed
Are the types of func and arg in lemma2 not also universally quantified? I'm
proving it using ax1, in which f and a have more specific types.
Thanks for any help.
Steve
Email Gateway (Aug 18 2022 at 15:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,
This will not work since the proof constructed in the proof ... qed body
(by means of "fixes", "assumes", "shows" -- only the latter present in
this example) does not match the outer proposition.
Hope this helps
Florian
signature.asc
Last updated: Apr 18 2024 at 16:19 UTC