THE vs. SOME
7 views
Skip to first unread message
Victor Porton
Mar 6, 2009, 4:25:44 PM3/6/09
to vdash
The following theory verifies without errors
theory embedding
imports ZF
begin
definition "ZZZ == ( THE x. x = 0 )"
end
It however ceases to work when I replace THE with SOME. How we can
live without SOME?! I need some solution to use in place of SOME or to
make SOME work. Or maybe THE will work in the case when there are more
than one value? Will it?
theory embedding
imports ZF
begin
definition "ZZZ == ( THE x. x = 0 )"
end
It however ceases to work when I replace THE with SOME. How we can
live without SOME?! I need some solution to use in place of SOME or to
make SOME work. Or maybe THE will work in the case when there are more
than one value? Will it?
Slawomir Kolodynski
Mar 6, 2009, 5:35:35 PM3/6/09
to vd...@googlegroups.com
Indeed, it looks like SOME is not supported in Isabelle/ZF. You may want to make sure by asking on the Isabelle mailing list.
I have done quite a lot of proofs in Isabelle/ZF and I have never needed SOME. Can provide a small example of how you would use SOME if it worked?
Maybe I will come up with some other approach that is sufficient for what you want to do.
THE is only usable when you have uniqueness.
Slawekk
--- On Fri, 3/6/09, Victor Porton <por...@narod.ru> wrote:
Reply all
Reply to author
Forward
0 new messages