41 (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, |
41 (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, |
42 not_neg_nat, int_0]) 1); |
42 not_neg_nat, int_0]) 1); |
43 qed "int_nat_number_of"; |
43 qed "int_nat_number_of"; |
44 Addsimps [int_nat_number_of]; |
44 Addsimps [int_nat_number_of]; |
45 |
45 |
|
46 |
|
47 (** Successor **) |
|
48 |
|
49 Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"; |
|
50 by (rtac sym 1); |
|
51 by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1); |
|
52 qed "Suc_nat_eq_nat_zadd1"; |
|
53 |
|
54 Goal "Suc (number_of v + n) = \ |
|
55 \ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"; |
|
56 by (simp_tac |
|
57 (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, |
|
58 nat_number_of_def, int_Suc, |
|
59 Suc_nat_eq_nat_zadd1, number_of_succ]) 1); |
|
60 qed "Suc_nat_number_of_add"; |
|
61 |
|
62 Goal "Suc (number_of v) = \ |
|
63 \ (if neg (number_of v) then 1 else number_of (bin_succ v))"; |
|
64 by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1); |
|
65 by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); |
|
66 qed "Suc_nat_number_of"; |
|
67 Addsimps [Suc_nat_number_of]; |
46 |
68 |
47 val nat_bin_arith_setup = |
69 val nat_bin_arith_setup = |
48 [Fast_Arith.map_data |
70 [Fast_Arith.map_data |
49 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
71 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
50 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
72 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
51 inj_thms = inj_thms, |
73 inj_thms = inj_thms, |
52 lessD = lessD, |
74 lessD = lessD, |
53 simpset = simpset addsimps [int_nat_number_of, not_neg_number_of_Pls, |
75 simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, |
|
76 not_neg_number_of_Pls, |
54 neg_number_of_Min,neg_number_of_BIT]})]; |
77 neg_number_of_Min,neg_number_of_BIT]})]; |
55 |
|
56 (** Successor **) |
|
57 |
|
58 Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"; |
|
59 by (rtac sym 1); |
|
60 by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1); |
|
61 qed "Suc_nat_eq_nat_zadd1"; |
|
62 |
|
63 Goal "Suc (number_of v + n) = \ |
|
64 \ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"; |
|
65 by (simp_tac |
|
66 (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, |
|
67 nat_number_of_def, int_Suc, |
|
68 Suc_nat_eq_nat_zadd1, number_of_succ]) 1); |
|
69 qed "Suc_nat_number_of_add"; |
|
70 |
|
71 Goal "Suc (number_of v) = \ |
|
72 \ (if neg (number_of v) then 1 else number_of (bin_succ v))"; |
|
73 by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1); |
|
74 by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); |
|
75 qed "Suc_nat_number_of"; |
|
76 Addsimps [Suc_nat_number_of]; |
|
77 |
78 |
78 (** Addition **) |
79 (** Addition **) |
79 |
80 |
80 Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'"; |
81 Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'"; |
81 by (rtac (inj_int RS injD) 1); |
82 by (rtac (inj_int RS injD) 1); |