src/HOL/Num.thy
changeset 47255 30a1692557b0
parent 47228 4f4d85c3516f
child 47299 e705ef5ffe95
     1.1 --- a/src/HOL/Num.thy	Sun Apr 01 09:12:03 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Sun Apr 01 16:09:58 2012 +0200
     1.3 @@ -965,6 +965,27 @@
     1.4      (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
     1.5    by (simp add: numeral_eq_Suc Let_def)
     1.6  
     1.7 +text {* Case analysis on @{term "n < 2"} *}
     1.8 +
     1.9 +lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
    1.10 +  by (auto simp add: numeral_2_eq_2)
    1.11 +
    1.12 +text {* Removal of Small Numerals: 0, 1 and (in additive positions) 2 *}
    1.13 +text {* bh: Are these rules really a good idea? *}
    1.14 +
    1.15 +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
    1.16 +  by simp
    1.17 +
    1.18 +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
    1.19 +  by simp
    1.20 +
    1.21 +text {* Can be used to eliminate long strings of Sucs, but not by default. *}
    1.22 +
    1.23 +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
    1.24 +  by simp
    1.25 +
    1.26 +lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
    1.27 +
    1.28  
    1.29  subsection {* Numeral equations as default simplification rules *}
    1.30