equal
deleted
inserted
replaced
66 (let pv = number_of (Int.pred v) in |
66 (let pv = number_of (Int.pred v) in |
67 if neg pv then nat_case a f n else f (nat pv + n))" |
67 if neg pv then nat_case a f n else f (nat pv + n))" |
68 apply (subst add_eq_if) |
68 apply (subst add_eq_if) |
69 apply (simp split add: nat.split |
69 apply (simp split add: nat.split |
70 del: nat_numeral_1_eq_1 |
70 del: nat_numeral_1_eq_1 |
71 add: numeral_1_eq_Suc_0 [symmetric] Let_def |
71 add: nat_numeral_1_eq_1 [symmetric] |
72 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0) |
72 numeral_1_eq_Suc_0 [symmetric] |
|
73 neg_number_of_pred_iff_0) |
73 done |
74 done |
74 |
75 |
75 lemma nat_rec_number_of [simp]: |
76 lemma nat_rec_number_of [simp]: |
76 "nat_rec a f (number_of v) = |
77 "nat_rec a f (number_of v) = |
77 (let pv = number_of (Int.pred v) in |
78 (let pv = number_of (Int.pred v) in |
87 if neg pv then nat_rec a f n |
88 if neg pv then nat_rec a f n |
88 else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
89 else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
89 apply (subst add_eq_if) |
90 apply (subst add_eq_if) |
90 apply (simp split add: nat.split |
91 apply (simp split add: nat.split |
91 del: nat_numeral_1_eq_1 |
92 del: nat_numeral_1_eq_1 |
92 add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 |
93 add: nat_numeral_1_eq_1 [symmetric] |
|
94 numeral_1_eq_Suc_0 [symmetric] |
93 neg_number_of_pred_iff_0) |
95 neg_number_of_pred_iff_0) |
94 done |
96 done |
95 |
97 |
96 |
98 |
97 subsubsection{*Various Other Lemmas*} |
99 subsubsection{*Various Other Lemmas*} |