Arithmetic calculations in ZF
13 views
Skip to first unread message
Victor Porton
Mar 6, 2009, 2:05:35 PM3/6/09
to vdash
It seems that ZF does not understand "arith" proof method.
How I should prove "1 + 1 = 2" theorem?
P.S. I just installed Isabelle and Proof General and have the first
experience.
How I should prove "1 + 1 = 2" theorem?
P.S. I just installed Isabelle and Proof General and have the first
experience.
Slawomir Kolodynski
Mar 6, 2009, 6:32:34 PM3/6/09
to vd...@googlegroups.com
> How I should prove "1 + 1 = 2" theorem?
>
Look at Arith.thy in the standard library. Note that addition of natural numbers is denoted "#+" . 1 = succ(0) and 2 = succ(1).
You might want to ask questions like this on the Isabelle mailing list.
Slawekk
Reply all
Reply to author
Forward
0 new messages