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 +