Re: [isabelle] Domain proof



On Fr, 2014-01-17 at 18:03 +0200, Roger H. wrote:
> Hi,
> 
> how can i prove
> 
> lemma "dom (SOME b. dom b = A) = A"
> 

You have to show that there is such a beast b, ie,

proof -
  obtain b where "dom b = A" ...
  thus ?thesis 
	sledgehammer (*Should find a proof now, using the rules for SOME,
probably SomeI*)

-- Peter


> Thank you!
>  		 	   		  






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