equal
deleted
inserted
replaced
1105 |
1105 |
1106 text \<open>Case analysis on \<^term>\<open>n < 2\<close>.\<close> |
1106 text \<open>Case analysis on \<^term>\<open>n < 2\<close>.\<close> |
1107 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
1107 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
1108 by (auto simp add: numeral_2_eq_2) |
1108 by (auto simp add: numeral_2_eq_2) |
1109 |
1109 |
|
1110 lemma less_2_cases_iff: "n < 2 \<longleftrightarrow> n = 0 \<or> n = Suc 0" |
|
1111 by (auto simp add: numeral_2_eq_2) |
|
1112 |
1110 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close> |
1113 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close> |
1111 text \<open>bh: Are these rules really a good idea?\<close> |
1114 text \<open>bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\<close> |
1112 |
1115 |
1113 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
1116 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
1114 by simp |
1117 by simp |
1115 |
1118 |
1116 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
1119 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |