Re: [isabelle] SOME-operator



Dear Roger,

yes it is True, and the crucial lemma is "someI":

lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
proof (rule someI)
  let ?a = "SOME x. True"
  show "Domain {(2,?a), (3,?a)} = {2,3}" by auto
qed

the "SOME x. True" is just some arbitrary element in
the range of your relation. (You did not specify the type
of the relation, hence the usage of the polymorphic SOME.

Kind regards,
René


Am 22.05.2013 um 20:51 schrieb "Roger H." <s57076 at hotmail.com>:

> 
> 
> Hello,
> 
> 
> is this lemma true?
> 
> 
> lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
> 
> 
> if yes, how can it be proved?
> 
> 
> Thank you!
> 
> 
> 		 	   		  
> 





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