Re: [isabelle] SOME-operator



On 23.05.2013 10:05, René Thiemann wrote:
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

Roger, please not, that only the type of "?a" matters, not the value. René used "SOME x. True" here to get an arbitrary value of the required type. But the use of SOME is not essential here:

proof (rule someI)
  show "Domain {(2,undefined), (3,undefined)} = {2,3}" by auto
qed

or (personally, I like this best)

proof (rule someI)
  fix x show "Domain {(2,x), (3,x)} = {2,3}" by auto
qed

  -- Lars




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