> 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