Re: [isabelle] THE - equality



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!
>                                   		 	   		  





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.