Email Gateway (Aug 19 2022 at 14:20): Email Gateway (Aug 19 2022 at 14:20):From: "Roger H." <s57076@hotmail.com>
Hello,
how can i prove
(THE x. x + 1 = 3) = 2 ?
After
"apply (rule the_equality, simp)"
i get:
⋀x. x + 1 = 3 ⟹ x = 2
I think i have to prove that the solution is unique.
how do i continue?
Thank you!
Email Gateway (Aug 19 2022 at 14:21):From: Lawrence Paulson <lp15@cam.ac.uk>
You need a type constraint:
lemma "(THE x::int. x + 1 = 3) = 2"
by auto
Otherwise, Isabelle doesn’t know what sort of numbers you are talking about. Numerals are polymorphic.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:21):From: "C. Diekmann" <diekmann@in.tum.de>
What is the type of x? Did you try x::nat?
Last updated: Apr 27 2024 at 04:17 UTC