Email Gateway (Aug 19 2022 at 14:51): Email Gateway (Aug 19 2022 at 14:51):From: Holden Lee <hl422@cam.ac.uk>
In the example, p and q are of type int==>bool. Contrast:
lemma "⋀x. (p x)==>(q x)"
proof -
term ?thesis ("q":: "int ⇒ bool")
show ?thesis sorry
qed
(*
Type unification failed: Clash of types "_ ⇒ _" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool ⇒ prop
Operand: ?thesis :: int ⇒ bool
*)
is not OK (I'm mystified as to why ?thesis is "q".) but
lemma "p x==>q x"
proof -
term ?thesis (* "q x":: "bool" *)
show ?thesis sorry
qed
is OK.
In the first case, what should I replace ?thesis by to make it correct
(other than the whole statement in quotes)?
Thanks,
Holden
Email Gateway (Aug 19 2022 at 14:51):From: Lawrence Paulson <lp15@cam.ac.uk>
You shouldn’t write a structured proof if the lemma statement includes meta-logical symbols in that way. Instead, try
lemma
fixes x
assumes “p x”
shows “q x”
proof … qed
Larry
Email Gateway (Aug 19 2022 at 14:51):From: Lars Noschinski <noschinl@in.tum.de>
If you have a look at ?thesis ("term ?thesis"), you'll see that ?thesis
is a lambda abstraction in this case and must be given a parameter.
Last updated: May 06 2024 at 12:29 UTC