author | paulson |
Fri, 15 Sep 2000 12:39:57 +0200 | |
changeset 9969 | 4753185f1dd2 |
parent 9945 | a0efbd7c88dc |
child 10701 | 16493f0cee9a |
permissions | -rw-r--r-- |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
1 |
(* Title: HOL/Integ/Bin.ML |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset
|
2 |
ID: $Id$ |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
4 |
David Spelt, University of Twente |
6060 | 5 |
Tobias Nipkow, Technical University Munich |
1632 | 6 |
Copyright 1994 University of Cambridge |
6060 | 7 |
Copyright 1996 University of Twente |
8 |
Copyright 1999 TU Munich |
|
1632 | 9 |
|
7708 | 10 |
Arithmetic on binary integers. |
1632 | 11 |
*) |
12 |
||
13 |
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
|
14 |
||
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
15 |
Goal "NCons Pls False = Pls"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
16 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
17 |
qed "NCons_Pls_0"; |
1632 | 18 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
19 |
Goal "NCons Pls True = Pls BIT True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
20 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
21 |
qed "NCons_Pls_1"; |
1632 | 22 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
23 |
Goal "NCons Min False = Min BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
24 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
25 |
qed "NCons_Min_0"; |
1632 | 26 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
27 |
Goal "NCons Min True = Min"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
28 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
29 |
qed "NCons_Min_1"; |
1632 | 30 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
31 |
Goal "bin_succ(w BIT True) = (bin_succ w) BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
32 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
33 |
qed "bin_succ_1"; |
1632 | 34 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
35 |
Goal "bin_succ(w BIT False) = NCons w True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
36 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
37 |
qed "bin_succ_0"; |
1632 | 38 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
39 |
Goal "bin_pred(w BIT True) = NCons w False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
40 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
41 |
qed "bin_pred_1"; |
1632 | 42 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
43 |
Goal "bin_pred(w BIT False) = (bin_pred w) BIT True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
44 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
45 |
qed "bin_pred_0"; |
1632 | 46 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
47 |
Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
48 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
49 |
qed "bin_minus_1"; |
1632 | 50 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
51 |
Goal "bin_minus(w BIT False) = (bin_minus w) BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
52 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
53 |
qed "bin_minus_0"; |
1632 | 54 |
|
5491 | 55 |
|
1632 | 56 |
(*** bin_add: binary addition ***) |
57 |
||
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
58 |
Goal "bin_add (v BIT True) (w BIT True) = \ |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
59 |
\ NCons (bin_add v (bin_succ w)) False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
60 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
61 |
qed "bin_add_BIT_11"; |
1632 | 62 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
63 |
Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
64 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
65 |
qed "bin_add_BIT_10"; |
1632 | 66 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
67 |
Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
68 |
by Auto_tac; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
69 |
qed "bin_add_BIT_0"; |
1632 | 70 |
|
5551 | 71 |
Goal "bin_add w Pls = w"; |
72 |
by (induct_tac "w" 1); |
|
73 |
by Auto_tac; |
|
74 |
qed "bin_add_Pls_right"; |
|
1632 | 75 |
|
7517
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset
|
76 |
Goal "bin_add w Min = bin_pred w"; |
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset
|
77 |
by (induct_tac "w" 1); |
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset
|
78 |
by Auto_tac; |
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset
|
79 |
qed "bin_add_Min_right"; |
1632 | 80 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
81 |
Goal "bin_add (v BIT x) (w BIT y) = \ |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
82 |
\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
83 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
84 |
qed "bin_add_BIT_BIT"; |
1632 | 85 |
|
86 |
||
6036 | 87 |
(*** bin_mult: binary multiplication ***) |
1632 | 88 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
89 |
Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
90 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
91 |
qed "bin_mult_1"; |
1632 | 92 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
93 |
Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
94 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
95 |
qed "bin_mult_0"; |
1632 | 96 |
|
97 |
||
98 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
99 |
||
100 |
||
6910 | 101 |
(**** number_of ****) |
1632 | 102 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
103 |
Goal "number_of(NCons w b) = (number_of(w BIT b)::int)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
104 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
105 |
by (ALLGOALS Asm_simp_tac); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
106 |
qed "number_of_NCons"; |
1632 | 107 |
|
6910 | 108 |
Addsimps [number_of_NCons]; |
1632 | 109 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
110 |
Goal "number_of(bin_succ w) = int 1 + number_of w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
111 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
112 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
113 |
qed "number_of_succ"; |
5491 | 114 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
115 |
Goal "number_of(bin_pred w) = - (int 1) + number_of w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
116 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
117 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
118 |
qed "number_of_pred"; |
1632 | 119 |
|
6910 | 120 |
Goal "number_of(bin_minus w) = (- (number_of w)::int)"; |
121 |
by (induct_tac "w" 1); |
|
5491 | 122 |
by (Simp_tac 1); |
123 |
by (Simp_tac 1); |
|
124 |
by (asm_simp_tac (simpset() |
|
5551 | 125 |
delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] |
6910 | 126 |
addsimps [number_of_succ,number_of_pred, |
5491 | 127 |
zadd_assoc]) 1); |
6910 | 128 |
qed "number_of_minus"; |
1632 | 129 |
|
130 |
||
9108 | 131 |
bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]); |
1632 | 132 |
|
6036 | 133 |
(*This proof is complicated by the mutual recursion*) |
6910 | 134 |
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)"; |
5184 | 135 |
by (induct_tac "v" 1); |
4686 | 136 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
137 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 138 |
by (rtac allI 1); |
5184 | 139 |
by (induct_tac "w" 1); |
5540 | 140 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); |
6910 | 141 |
qed_spec_mp "number_of_add"; |
1632 | 142 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
143 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
144 |
(*Subtraction*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
145 |
Goalw [zdiff_def] |
6910 | 146 |
"number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)"; |
147 |
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1); |
|
148 |
qed "diff_number_of_eq"; |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
149 |
|
9108 | 150 |
bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]); |
1632 | 151 |
|
6910 | 152 |
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)"; |
5184 | 153 |
by (induct_tac "v" 1); |
4686 | 154 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
155 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
5491 | 156 |
by (asm_simp_tac |
5540 | 157 |
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); |
6910 | 158 |
qed "number_of_mult"; |
5491 | 159 |
|
1632 | 160 |
|
6941 | 161 |
(*The correctness of shifting. But it doesn't seem to give a measurable |
162 |
speed-up.*) |
|
163 |
Goal "(#2::int) * number_of w = number_of (w BIT False)"; |
|
164 |
by (induct_tac "w" 1); |
|
165 |
by (ALLGOALS (asm_simp_tac |
|
166 |
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac))); |
|
167 |
qed "double_number_of_BIT"; |
|
168 |
||
169 |
||
5491 | 170 |
(** Simplification rules with integer constants **) |
171 |
||
6910 | 172 |
Goal "#0 + z = (z::int)"; |
5491 | 173 |
by (Simp_tac 1); |
174 |
qed "zadd_0"; |
|
175 |
||
6910 | 176 |
Goal "z + #0 = (z::int)"; |
5491 | 177 |
by (Simp_tac 1); |
178 |
qed "zadd_0_right"; |
|
179 |
||
5592 | 180 |
Addsimps [zadd_0, zadd_0_right]; |
181 |
||
182 |
||
183 |
(** Converting simple cases of (int n) to numerals **) |
|
5491 | 184 |
|
5592 | 185 |
(*int 0 = #0 *) |
6910 | 186 |
bind_thm ("int_0", number_of_Pls RS sym); |
5491 | 187 |
|
5592 | 188 |
Goal "int (Suc n) = #1 + int n"; |
189 |
by (simp_tac (simpset() addsimps [zadd_int]) 1); |
|
190 |
qed "int_Suc"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
191 |
|
6910 | 192 |
Goal "- (#0) = (#0::int)"; |
5491 | 193 |
by (Simp_tac 1); |
194 |
qed "zminus_0"; |
|
195 |
||
196 |
Addsimps [zminus_0]; |
|
197 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
198 |
|
6910 | 199 |
Goal "(#0::int) - x = -x"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
200 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
201 |
qed "zdiff0"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
202 |
|
6910 | 203 |
Goal "x - (#0::int) = x"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
204 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
205 |
qed "zdiff0_right"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
206 |
|
6910 | 207 |
Goal "x - x = (#0::int)"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
208 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
209 |
qed "zdiff_self"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
210 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
211 |
Addsimps [zdiff0, zdiff0_right, zdiff_self]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
212 |
|
6917 | 213 |
|
214 |
(** Special simplification, for constants only **) |
|
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
215 |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset
|
216 |
(*Distributive laws for literals*) |
6917 | 217 |
Addsimps (map (inst "w" "number_of ?v") |
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
218 |
[zadd_zmult_distrib, zadd_zmult_distrib2, |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
219 |
zdiff_zmult_distrib, zdiff_zmult_distrib2]); |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
220 |
|
6917 | 221 |
Addsimps (map (inst "x" "number_of ?v") |
222 |
[zless_zminus, zle_zminus, equation_zminus]); |
|
223 |
Addsimps (map (inst "y" "number_of ?v") |
|
224 |
[zminus_zless, zminus_zle, zminus_equation]); |
|
225 |
||
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset
|
226 |
(*Moving negation out of products*) |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset
|
227 |
Addsimps [zmult_zminus, zmult_zminus_right]; |
6917 | 228 |
|
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
229 |
(*Cancellation of constant factors in comparisons (< and <=) *) |
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
230 |
Addsimps (map (inst "k" "number_of ?v") |
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
231 |
[zmult_zless_cancel1, zmult_zless_cancel2, |
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
232 |
zmult_zle_cancel1, zmult_zle_cancel2]); |
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
233 |
|
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset
|
234 |
|
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
235 |
(** Special-case simplification for small constants **) |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
236 |
|
6910 | 237 |
Goal "#0 * z = (#0::int)"; |
5491 | 238 |
by (Simp_tac 1); |
239 |
qed "zmult_0"; |
|
240 |
||
6910 | 241 |
Goal "z * #0 = (#0::int)"; |
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
242 |
by (Simp_tac 1); |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
243 |
qed "zmult_0_right"; |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
244 |
|
6910 | 245 |
Goal "#1 * z = (z::int)"; |
5491 | 246 |
by (Simp_tac 1); |
247 |
qed "zmult_1"; |
|
248 |
||
6910 | 249 |
Goal "z * #1 = (z::int)"; |
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
250 |
by (Simp_tac 1); |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
251 |
qed "zmult_1_right"; |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
252 |
|
6917 | 253 |
Goal "#-1 * z = -(z::int)"; |
254 |
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1); |
|
255 |
qed "zmult_minus1"; |
|
256 |
||
257 |
Goal "z * #-1 = -(z::int)"; |
|
258 |
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1); |
|
259 |
qed "zmult_minus1_right"; |
|
260 |
||
261 |
Addsimps [zmult_0, zmult_0_right, |
|
262 |
zmult_1, zmult_1_right, |
|
263 |
zmult_minus1, zmult_minus1_right]; |
|
264 |
||
8785 | 265 |
(*Negation of a coefficient*) |
266 |
Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)"; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9214
diff
changeset
|
267 |
by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1); |
8785 | 268 |
qed "zminus_number_of_zmult"; |
269 |
||
270 |
Addsimps [zminus_number_of_zmult]; |
|
271 |
||
6917 | 272 |
|
273 |
(** Inequality reasoning **) |
|
5491 | 274 |
|
6989 | 275 |
Goal "(m*n = (#0::int)) = (m = #0 | n = #0)"; |
276 |
by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1); |
|
277 |
qed "zmult_eq_0_iff"; |
|
278 |
||
9062 | 279 |
Goal "((#0::int) = m*n) = (#0 = m | #0 = n)"; |
280 |
by (stac eq_commute 1 THEN stac zmult_eq_0_iff 1); |
|
281 |
by Auto_tac; |
|
282 |
qed "zmult_0_eq_iff"; |
|
283 |
||
9969 | 284 |
AddIffs [zmult_eq_0_iff, zmult_0_eq_iff]; |
9062 | 285 |
|
6910 | 286 |
Goal "(w < z + (#1::int)) = (w<z | w=z)"; |
5592 | 287 |
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1); |
5491 | 288 |
qed "zless_add1_eq"; |
289 |
||
6910 | 290 |
Goal "(w + (#1::int) <= z) = (w<z)"; |
5592 | 291 |
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1); |
5491 | 292 |
qed "add1_zle_eq"; |
6997 | 293 |
|
294 |
Goal "((#1::int) + w <= z) = (w<z)"; |
|
295 |
by (stac zadd_commute 1); |
|
296 |
by (rtac add1_zle_eq 1); |
|
297 |
qed "add1_left_zle_eq"; |
|
5491 | 298 |
|
5540 | 299 |
Goal "neg x = (x < #0)"; |
6917 | 300 |
by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); |
5540 | 301 |
qed "neg_eq_less_0"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
302 |
|
6989 | 303 |
Goal "(~neg x) = (#0 <= x)"; |
6917 | 304 |
by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); |
5540 | 305 |
qed "not_neg_eq_ge_0"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
306 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
307 |
Goal "#0 <= int m"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
308 |
by (Simp_tac 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
309 |
qed "zero_zle_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
310 |
AddIffs [zero_zle_int]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
311 |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
312 |
|
5747 | 313 |
(** Needed because (int 0) rewrites to #0. |
314 |
Can these be generalized without evaluating large numbers?**) |
|
315 |
||
316 |
Goal "~ (int k < #0)"; |
|
317 |
by (Simp_tac 1); |
|
318 |
qed "int_less_0_conv"; |
|
319 |
||
320 |
Goal "(int k <= #0) = (k=0)"; |
|
321 |
by (Simp_tac 1); |
|
322 |
qed "int_le_0_conv"; |
|
323 |
||
324 |
Goal "(int k = #0) = (k=0)"; |
|
325 |
by (Simp_tac 1); |
|
326 |
qed "int_eq_0_conv"; |
|
327 |
||
328 |
Goal "(#0 = int k) = (k=0)"; |
|
329 |
by Auto_tac; |
|
330 |
qed "int_eq_0_conv'"; |
|
331 |
||
9945 | 332 |
Goal "(#0 < int k) = (0<k)"; |
333 |
by (Simp_tac 1); |
|
334 |
qed "zero_less_int_conv"; |
|
335 |
||
336 |
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv', |
|
337 |
zero_less_int_conv]; |
|
338 |
||
339 |
Goal "(0 < nat z) = (#0 < z)"; |
|
340 |
by (cut_inst_tac [("w","#0")] zless_nat_conj 1); |
|
341 |
by Auto_tac; |
|
342 |
qed "zero_less_nat_eq"; |
|
343 |
Addsimps [zero_less_nat_eq]; |
|
5747 | 344 |
|
345 |
||
5491 | 346 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
347 |
||
348 |
(** Equals (=) **) |
|
1632 | 349 |
|
5491 | 350 |
Goalw [iszero_def] |
6997 | 351 |
"((number_of x::int) = number_of y) = \ |
352 |
\ iszero (number_of (bin_add x (bin_minus y)))"; |
|
5491 | 353 |
by (simp_tac (simpset() addsimps |
6910 | 354 |
(zcompare_rls @ [number_of_add, number_of_minus])) 1); |
355 |
qed "eq_number_of_eq"; |
|
5491 | 356 |
|
6910 | 357 |
Goalw [iszero_def] "iszero ((number_of Pls)::int)"; |
5491 | 358 |
by (Simp_tac 1); |
6910 | 359 |
qed "iszero_number_of_Pls"; |
5491 | 360 |
|
6910 | 361 |
Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; |
5491 | 362 |
by (Simp_tac 1); |
6910 | 363 |
qed "nonzero_number_of_Min"; |
5491 | 364 |
|
365 |
Goalw [iszero_def] |
|
6910 | 366 |
"iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; |
5491 | 367 |
by (Simp_tac 1); |
6910 | 368 |
by (int_case_tac "number_of w" 1); |
5491 | 369 |
by (ALLGOALS (asm_simp_tac |
5540 | 370 |
(simpset() addsimps zcompare_rls @ |
371 |
[zminus_zadd_distrib RS sym, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
372 |
zadd_int]))); |
6910 | 373 |
qed "iszero_number_of_BIT"; |
5491 | 374 |
|
6910 | 375 |
Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; |
376 |
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); |
|
377 |
qed "iszero_number_of_0"; |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
378 |
|
6910 | 379 |
Goal "~ iszero (number_of (w BIT True)::int)"; |
380 |
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); |
|
381 |
qed "iszero_number_of_1"; |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
382 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
383 |
|
5491 | 384 |
|
385 |
(** Less-than (<) **) |
|
386 |
||
387 |
Goalw [zless_def,zdiff_def] |
|
6910 | 388 |
"(number_of x::int) < number_of y \ |
389 |
\ = neg (number_of (bin_add x (bin_minus y)))"; |
|
5491 | 390 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
6910 | 391 |
qed "less_number_of_eq_neg"; |
5491 | 392 |
|
6910 | 393 |
Goal "~ neg (number_of Pls)"; |
5491 | 394 |
by (Simp_tac 1); |
6910 | 395 |
qed "not_neg_number_of_Pls"; |
5491 | 396 |
|
6910 | 397 |
Goal "neg (number_of Min)"; |
5491 | 398 |
by (Simp_tac 1); |
6910 | 399 |
qed "neg_number_of_Min"; |
5491 | 400 |
|
6910 | 401 |
Goal "neg (number_of (w BIT x)) = neg (number_of w)"; |
5491 | 402 |
by (Asm_simp_tac 1); |
6910 | 403 |
by (int_case_tac "number_of w" 1); |
5491 | 404 |
by (ALLGOALS (asm_simp_tac |
6917 | 405 |
(simpset() addsimps [zadd_int, neg_eq_less_int0, |
5540 | 406 |
symmetric zdiff_def] @ zcompare_rls))); |
6910 | 407 |
qed "neg_number_of_BIT"; |
5491 | 408 |
|
409 |
||
410 |
(** Less-than-or-equals (<=) **) |
|
411 |
||
7033 | 412 |
Goal "(number_of x <= (number_of y::int)) = \ |
413 |
\ (~ number_of y < (number_of x::int))"; |
|
414 |
by (rtac (linorder_not_less RS sym) 1); |
|
6910 | 415 |
qed "le_number_of_eq_not_less"; |
5491 | 416 |
|
9214 | 417 |
(** Absolute value (abs) **) |
418 |
||
419 |
Goalw [zabs_def] |
|
420 |
"abs(number_of x::int) = \ |
|
421 |
\ (if number_of x < (0::int) then -number_of x else number_of x)"; |
|
422 |
by(rtac refl 1); |
|
423 |
qed "abs_number_of"; |
|
424 |
||
425 |
||
5540 | 426 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5551 | 427 |
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, |
428 |
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; |
|
5491 | 429 |
|
430 |
(*Hide the binary representation of integer constants*) |
|
6910 | 431 |
Delsimps [number_of_Pls, number_of_Min, number_of_BIT]; |
5491 | 432 |
|
8787 | 433 |
(*Simplification of arithmetic operations on integer constants. |
434 |
Note that bin_pred_Pls, etc. were added to the simpset by primrec.*) |
|
435 |
||
9108 | 436 |
bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]); |
8787 | 437 |
|
9108 | 438 |
bind_thms ("bin_arith_extra_simps", |
6910 | 439 |
[number_of_add RS sym, |
440 |
number_of_minus RS sym, |
|
441 |
number_of_mult RS sym, |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
442 |
bin_succ_1, bin_succ_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
443 |
bin_pred_1, bin_pred_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
444 |
bin_minus_1, bin_minus_0, |
7517
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset
|
445 |
bin_add_Pls_right, bin_add_Min_right, |
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
446 |
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, |
9214 | 447 |
diff_number_of_eq, abs_number_of, |
9108 | 448 |
bin_mult_1, bin_mult_0] @ NCons_simps); |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
449 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
450 |
(*For making a minimal simpset, one must include these default simprules |
6910 | 451 |
of thy. Also include simp_thms, or at least (~False)=True*) |
9108 | 452 |
bind_thms ("bin_arith_simps", |
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
453 |
[bin_pred_Pls, bin_pred_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
454 |
bin_succ_Pls, bin_succ_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
455 |
bin_add_Pls, bin_add_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
456 |
bin_minus_Pls, bin_minus_Min, |
9108 | 457 |
bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps); |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
458 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
459 |
(*Simplification of relational operations*) |
9108 | 460 |
bind_thms ("bin_rel_simps", |
6910 | 461 |
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min, |
462 |
iszero_number_of_0, iszero_number_of_1, |
|
463 |
less_number_of_eq_neg, |
|
464 |
not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT, |
|
9108 | 465 |
le_number_of_eq_not_less]); |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
466 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
467 |
Addsimps bin_arith_extra_simps; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
468 |
Addsimps bin_rel_simps; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
469 |
|
6997 | 470 |
|
8764 | 471 |
(** Simplification of arithmetic when nested to the right **) |
6997 | 472 |
|
8764 | 473 |
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"; |
474 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
|
475 |
qed "add_number_of_left"; |
|
476 |
||
477 |
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"; |
|
478 |
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); |
|
479 |
qed "mult_number_of_left"; |
|
6997 | 480 |
|
481 |
Goalw [zdiff_def] |
|
482 |
"number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)"; |
|
8764 | 483 |
by (rtac add_number_of_left 1); |
484 |
qed "add_number_of_diff1"; |
|
6997 | 485 |
|
486 |
Goal "number_of v + (c - number_of w) = \ |
|
487 |
\ number_of (bin_add v (bin_minus w)) + (c::int)"; |
|
488 |
by (stac (diff_number_of_eq RS sym) 1); |
|
489 |
by Auto_tac; |
|
8764 | 490 |
qed "add_number_of_diff2"; |
6997 | 491 |
|
8764 | 492 |
Addsimps [add_number_of_left, mult_number_of_left, |
493 |
add_number_of_diff1, add_number_of_diff2]; |