# 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.*