1048 |
1048 |
1049 lemma min_numeral_Suc [simp]: |
1049 lemma min_numeral_Suc [simp]: |
1050 "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)" |
1050 "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)" |
1051 by (simp add: numeral_eq_Suc) |
1051 by (simp add: numeral_eq_Suc) |
1052 |
1052 |
1053 text {* For @{term nat_case} and @{term nat_rec}. *} |
1053 text {* For @{term case_nat} and @{term rec_nat}. *} |
1054 |
1054 |
1055 lemma nat_case_numeral [simp]: |
1055 lemma case_nat_numeral [simp]: |
1056 "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)" |
1056 "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)" |
1057 by (simp add: numeral_eq_Suc) |
1057 by (simp add: numeral_eq_Suc) |
1058 |
1058 |
1059 lemma nat_case_add_eq_if [simp]: |
1059 lemma case_nat_add_eq_if [simp]: |
1060 "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))" |
1060 "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))" |
1061 by (simp add: numeral_eq_Suc) |
1061 by (simp add: numeral_eq_Suc) |
1062 |
1062 |
1063 lemma nat_rec_numeral [simp]: |
1063 lemma rec_nat_numeral [simp]: |
1064 "nat_rec a f (numeral v) = |
1064 "rec_nat a f (numeral v) = |
1065 (let pv = pred_numeral v in f pv (nat_rec a f pv))" |
1065 (let pv = pred_numeral v in f pv (rec_nat a f pv))" |
1066 by (simp add: numeral_eq_Suc Let_def) |
1066 by (simp add: numeral_eq_Suc Let_def) |
1067 |
1067 |
1068 lemma nat_rec_add_eq_if [simp]: |
1068 lemma rec_nat_add_eq_if [simp]: |
1069 "nat_rec a f (numeral v + n) = |
1069 "rec_nat a f (numeral v + n) = |
1070 (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))" |
1070 (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))" |
1071 by (simp add: numeral_eq_Suc Let_def) |
1071 by (simp add: numeral_eq_Suc Let_def) |
1072 |
1072 |
1073 text {* Case analysis on @{term "n < 2"} *} |
1073 text {* Case analysis on @{term "n < 2"} *} |
1074 |
1074 |
1075 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
1075 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |