add lemma Suc_1
authorhuffman
Mon Apr 02 16:06:24 2012 +0200 (2012-04-02)
changeset 47299e705ef5ffe95
parent 47298 8b63aaec0a0e
child 47300 2284a40e0f57
add lemma Suc_1
src/HOL/Num.thy
     1.1 --- a/src/HOL/Num.thy	Mon Apr 02 14:09:27 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Mon Apr 02 16:06:24 2012 +0200
     1.3 @@ -865,8 +865,11 @@
     1.4    Natural numbers
     1.5  *}
     1.6  
     1.7 +lemma Suc_1 [simp]: "Suc 1 = 2"
     1.8 +  unfolding Suc_eq_plus1 by (rule one_add_one)
     1.9 +
    1.10  lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
    1.11 -  unfolding numeral_plus_one [symmetric] by simp
    1.12 +  unfolding Suc_eq_plus1 by (rule numeral_plus_one)
    1.13  
    1.14  definition pred_numeral :: "num \<Rightarrow> nat"
    1.15    where [code del]: "pred_numeral k = numeral k - 1"