*To*: "Roger H." <s57076 at hotmail.com>*Subject*: Re: [isabelle] THE - equality*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 18 Apr 2014 11:39:32 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DUB124-W17C03485552BD325DD9B938F5D0@phx.gbl>*References*: <DUB124-W17C03485552BD325DD9B938F5D0@phx.gbl>

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 On 18 Apr 2014, at 11:24, Roger H. <s57076 at hotmail.com> wrote: > 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! >

**References**:**[isabelle] THE - equality***From:*Roger H .

- Previous by Date: [isabelle] THE - equality
- Next by Date: Re: [isabelle] THE - equality
- Previous by Thread: [isabelle] THE - equality
- Next by Thread: Re: [isabelle] THE - equality
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list