20 by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) |
20 by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) |
21 |
21 |
22 text {*Now just instantiating @{text n} to @{text "number_of v"} does |
22 text {*Now just instantiating @{text n} to @{text "number_of v"} does |
23 the right simplification, but with some redundant inequality |
23 the right simplification, but with some redundant inequality |
24 tests.*} |
24 tests.*} |
25 lemma neg_number_of_bin_pred_iff_0: |
25 lemma neg_number_of_pred_iff_0: |
26 "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))" |
26 "neg (number_of (pred v)::int) = (number_of v = (0::nat))" |
27 apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ") |
27 apply (subgoal_tac "neg (number_of (pred v)) = (number_of v < Suc 0) ") |
28 apply (simp only: less_Suc_eq_le le_0_eq) |
28 apply (simp only: less_Suc_eq_le le_0_eq) |
29 apply (subst less_number_of_Suc, simp) |
29 apply (subst less_number_of_Suc, simp) |
30 done |
30 done |
31 |
31 |
32 text{*No longer required as a simprule because of the @{text inverse_fold} |
32 text{*No longer required as a simprule because of the @{text inverse_fold} |
33 simproc*} |
33 simproc*} |
34 lemma Suc_diff_number_of: |
34 lemma Suc_diff_number_of: |
35 "neg (number_of (bin_minus v)::int) ==> |
35 "neg (number_of (uminus v)::int) ==> |
36 Suc m - (number_of v) = m - (number_of (bin_pred v))" |
36 Suc m - (number_of v) = m - (number_of (pred v))" |
37 apply (subst Suc_diff_eq_diff_pred) |
37 apply (subst Suc_diff_eq_diff_pred) |
38 apply simp |
38 apply simp |
39 apply (simp del: nat_numeral_1_eq_1) |
39 apply (simp del: nat_numeral_1_eq_1) |
40 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
40 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
41 neg_number_of_bin_pred_iff_0) |
41 neg_number_of_pred_iff_0) |
42 done |
42 done |
43 |
43 |
44 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
44 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
45 by (simp add: numerals split add: nat_diff_split) |
45 by (simp add: numerals split add: nat_diff_split) |
46 |
46 |
47 |
47 |
48 subsection{*For @{term nat_case} and @{term nat_rec}*} |
48 subsection{*For @{term nat_case} and @{term nat_rec}*} |
49 |
49 |
50 lemma nat_case_number_of [simp]: |
50 lemma nat_case_number_of [simp]: |
51 "nat_case a f (number_of v) = |
51 "nat_case a f (number_of v) = |
52 (let pv = number_of (bin_pred v) in |
52 (let pv = number_of (pred v) in |
53 if neg pv then a else f (nat pv))" |
53 if neg pv then a else f (nat pv))" |
54 by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0) |
54 by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) |
55 |
55 |
56 lemma nat_case_add_eq_if [simp]: |
56 lemma nat_case_add_eq_if [simp]: |
57 "nat_case a f ((number_of v) + n) = |
57 "nat_case a f ((number_of v) + n) = |
58 (let pv = number_of (bin_pred v) in |
58 (let pv = number_of (pred v) in |
59 if neg pv then nat_case a f n else f (nat pv + n))" |
59 if neg pv then nat_case a f n else f (nat pv + n))" |
60 apply (subst add_eq_if) |
60 apply (subst add_eq_if) |
61 apply (simp split add: nat.split |
61 apply (simp split add: nat.split |
62 del: nat_numeral_1_eq_1 |
62 del: nat_numeral_1_eq_1 |
63 add: numeral_1_eq_Suc_0 [symmetric] Let_def |
63 add: numeral_1_eq_Suc_0 [symmetric] Let_def |
64 neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0) |
64 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0) |
65 done |
65 done |
66 |
66 |
67 lemma nat_rec_number_of [simp]: |
67 lemma nat_rec_number_of [simp]: |
68 "nat_rec a f (number_of v) = |
68 "nat_rec a f (number_of v) = |
69 (let pv = number_of (bin_pred v) in |
69 (let pv = number_of (pred v) in |
70 if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" |
70 if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" |
71 apply (case_tac " (number_of v) ::nat") |
71 apply (case_tac " (number_of v) ::nat") |
72 apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0) |
72 apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) |
73 apply (simp split add: split_if_asm) |
73 apply (simp split add: split_if_asm) |
74 done |
74 done |
75 |
75 |
76 lemma nat_rec_add_eq_if [simp]: |
76 lemma nat_rec_add_eq_if [simp]: |
77 "nat_rec a f (number_of v + n) = |
77 "nat_rec a f (number_of v + n) = |
78 (let pv = number_of (bin_pred v) in |
78 (let pv = number_of (pred v) in |
79 if neg pv then nat_rec a f n |
79 if neg pv then nat_rec a f n |
80 else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
80 else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
81 apply (subst add_eq_if) |
81 apply (subst add_eq_if) |
82 apply (simp split add: nat.split |
82 apply (simp split add: nat.split |
83 del: nat_numeral_1_eq_1 |
83 del: nat_numeral_1_eq_1 |
84 add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 |
84 add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 |
85 neg_number_of_bin_pred_iff_0) |
85 neg_number_of_pred_iff_0) |
86 done |
86 done |
87 |
87 |
88 |
88 |
89 subsection{*Various Other Lemmas*} |
89 subsection{*Various Other Lemmas*} |
90 |
90 |