author | wenzelm |
Fri, 05 Oct 2001 21:52:39 +0200 | |
changeset 11701 | 3d51fbf81c17 |
parent 10701 | 16493f0cee9a |
child 11704 | 3c50a2cd6f00 |
permissions | -rw-r--r-- |
6917 | 1 |
(* Title: HOL/IntDiv.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
The division operators div, mod and the divides relation "dvd" |
|
6992 | 7 |
|
8 |
Here is the division algorithm in ML: |
|
9 |
||
10 |
fun posDivAlg (a,b) = |
|
11 |
if a<b then (0,a) |
|
12 |
else let val (q,r) = posDivAlg(a, 2*b) |
|
13 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
|
14 |
end; |
|
15 |
||
16 |
fun negDivAlg (a,b) = |
|
17 |
if 0<=a+b then (~1,a+b) |
|
18 |
else let val (q,r) = negDivAlg(a, 2*b) |
|
19 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
|
20 |
end; |
|
21 |
||
22 |
fun negateSnd (q,r:int) = (q,~r); |
|
23 |
||
24 |
fun divAlg (a,b) = if 0<=a then |
|
25 |
if b>0 then posDivAlg (a,b) |
|
26 |
else if a=0 then (0,0) |
|
27 |
else negateSnd (negDivAlg (~a,~b)) |
|
28 |
else |
|
29 |
if 0<b then negDivAlg (a,b) |
|
30 |
else negateSnd (posDivAlg (~a,~b)); |
|
6917 | 31 |
*) |
32 |
||
33 |
Addsimps [zless_nat_conj]; |
|
34 |
||
35 |
(*** Uniqueness and monotonicity of quotients and remainders ***) |
|
36 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
37 |
Goal "[| b*q' + r' <= b*q + r; Numeral0 <= r'; Numeral0 < b; r < b |] \ |
6917 | 38 |
\ ==> q' <= (q::int)"; |
39 |
by (subgoal_tac "r' + b * (q'-q) <= r" 1); |
|
8918 | 40 |
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
41 |
by (subgoal_tac "Numeral0 < b * (Numeral1 + q - q')" 1); |
6917 | 42 |
by (etac order_le_less_trans 2); |
8918 | 43 |
by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
44 |
zadd_zmult_distrib2]) 2); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
45 |
by (subgoal_tac "b * q' < b * (Numeral1 + q)" 1); |
8918 | 46 |
by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
47 |
zadd_zmult_distrib2]) 2); |
|
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
48 |
by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
6917 | 49 |
qed "unique_quotient_lemma"; |
50 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
51 |
Goal "[| b*q' + r' <= b*q + r; r <= Numeral0; b < Numeral0; b < r' |] \ |
6917 | 52 |
\ ==> q <= (q'::int)"; |
53 |
by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] |
|
54 |
unique_quotient_lemma 1); |
|
55 |
by (auto_tac (claset(), |
|
8918 | 56 |
simpset() addsimps [zmult_zminus, zmult_zminus_right])); |
6917 | 57 |
qed "unique_quotient_lemma_neg"; |
58 |
||
59 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
60 |
Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= Numeral0 |] \ |
6917 | 61 |
\ ==> q = q'"; |
62 |
by (asm_full_simp_tac |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
63 |
(simpset() addsimps split_ifs@ |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
64 |
[quorem_def, linorder_neq_iff]) 1); |
6917 | 65 |
by Safe_tac; |
66 |
by (ALLGOALS Asm_full_simp_tac); |
|
67 |
by (REPEAT |
|
68 |
(blast_tac (claset() addIs [order_antisym] |
|
69 |
addDs [order_eq_refl RS unique_quotient_lemma, |
|
70 |
order_eq_refl RS unique_quotient_lemma_neg, |
|
71 |
sym]) 1)); |
|
72 |
qed "unique_quotient"; |
|
73 |
||
74 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
75 |
Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= Numeral0 |] \ |
6917 | 76 |
\ ==> r = r'"; |
77 |
by (subgoal_tac "q = q'" 1); |
|
78 |
by (blast_tac (claset() addIs [unique_quotient]) 2); |
|
79 |
by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); |
|
80 |
qed "unique_remainder"; |
|
81 |
||
82 |
||
83 |
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***) |
|
84 |
||
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
85 |
|
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
86 |
Goal "adjust a b (q,r) = (let diff = r-b in \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
87 |
\ if Numeral0 <= diff then (# 2*q + Numeral1, diff) \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
88 |
\ else (# 2*q, r))"; |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
89 |
by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1); |
6917 | 90 |
qed "adjust_eq"; |
91 |
Addsimps [adjust_eq]; |
|
92 |
||
93 |
(*Proving posDivAlg's termination condition*) |
|
94 |
val [tc] = posDivAlg.tcs; |
|
9367 | 95 |
goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc)); |
8787 | 96 |
by Auto_tac; |
6917 | 97 |
val lemma = result(); |
98 |
||
99 |
(* removing the termination condition from the generated theorems *) |
|
100 |
||
8624 | 101 |
bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps); |
6917 | 102 |
|
103 |
(**use with simproc to avoid re-proving the premise*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
104 |
Goal "Numeral0 < b ==> \ |
6917 | 105 |
\ posDivAlg (a,b) = \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
106 |
\ (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, # 2*b)))"; |
6917 | 107 |
by (rtac (posDivAlg_raw_eqn RS trans) 1); |
108 |
by (Asm_simp_tac 1); |
|
109 |
qed "posDivAlg_eqn"; |
|
110 |
||
9108 | 111 |
bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct); |
6917 | 112 |
|
113 |
||
114 |
(*Correctness of posDivAlg: it computes quotients correctly*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
115 |
Goal "Numeral0 <= a --> Numeral0 < b --> quorem ((a, b), posDivAlg (a, b))"; |
9747 | 116 |
by (induct_thm_tac posDivAlg_induct "a b" 1); |
6917 | 117 |
by Auto_tac; |
9063 | 118 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); |
6917 | 119 |
(*base case: a<b*) |
120 |
by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1); |
|
121 |
(*main argument*) |
|
122 |
by (stac posDivAlg_eqn 1); |
|
123 |
by (ALLGOALS Asm_simp_tac); |
|
124 |
by (etac splitE 1); |
|
8918 | 125 |
by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def])); |
6917 | 126 |
qed_spec_mp "posDivAlg_correct"; |
127 |
||
128 |
||
129 |
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***) |
|
130 |
||
131 |
(*Proving negDivAlg's termination condition*) |
|
132 |
val [tc] = negDivAlg.tcs; |
|
9422 | 133 |
goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc)); |
8787 | 134 |
by Auto_tac; |
6917 | 135 |
val lemma = result(); |
136 |
||
137 |
(* removing the termination condition from the generated theorems *) |
|
138 |
||
8624 | 139 |
bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps); |
6917 | 140 |
|
141 |
(**use with simproc to avoid re-proving the premise*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
142 |
Goal "Numeral0 < b ==> \ |
6917 | 143 |
\ negDivAlg (a,b) = \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
144 |
\ (if Numeral0<=a+b then (# -1,a+b) else adjust a b (negDivAlg(a, # 2*b)))"; |
6917 | 145 |
by (rtac (negDivAlg_raw_eqn RS trans) 1); |
146 |
by (Asm_simp_tac 1); |
|
147 |
qed "negDivAlg_eqn"; |
|
148 |
||
9108 | 149 |
bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct); |
6917 | 150 |
|
151 |
||
152 |
(*Correctness of negDivAlg: it computes quotients correctly |
|
153 |
It doesn't work if a=0 because the 0/b=0 rather than -1*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
154 |
Goal "a < Numeral0 --> Numeral0 < b --> quorem ((a, b), negDivAlg (a, b))"; |
9747 | 155 |
by (induct_thm_tac negDivAlg_induct "a b" 1); |
6917 | 156 |
by Auto_tac; |
9063 | 157 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); |
6917 | 158 |
(*base case: 0<=a+b*) |
159 |
by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1); |
|
160 |
(*main argument*) |
|
161 |
by (stac negDivAlg_eqn 1); |
|
162 |
by (ALLGOALS Asm_simp_tac); |
|
163 |
by (etac splitE 1); |
|
8918 | 164 |
by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def])); |
6917 | 165 |
qed_spec_mp "negDivAlg_correct"; |
166 |
||
167 |
||
168 |
(*** Existence shown by proving the division algorithm to be correct ***) |
|
169 |
||
170 |
(*the case a=0*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
171 |
Goal "b ~= Numeral0 ==> quorem ((Numeral0,b), (Numeral0,Numeral0))"; |
6917 | 172 |
by (auto_tac (claset(), |
173 |
simpset() addsimps [quorem_def, linorder_neq_iff])); |
|
174 |
qed "quorem_0"; |
|
175 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
176 |
Goal "posDivAlg (Numeral0, b) = (Numeral0, Numeral0)"; |
6917 | 177 |
by (stac posDivAlg_raw_eqn 1); |
178 |
by Auto_tac; |
|
179 |
qed "posDivAlg_0"; |
|
180 |
Addsimps [posDivAlg_0]; |
|
181 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
182 |
Goal "negDivAlg (# -1, b) = (# -1, b-Numeral1)"; |
6917 | 183 |
by (stac negDivAlg_raw_eqn 1); |
184 |
by Auto_tac; |
|
185 |
qed "negDivAlg_minus1"; |
|
186 |
Addsimps [negDivAlg_minus1]; |
|
187 |
||
188 |
Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)"; |
|
189 |
by Auto_tac; |
|
190 |
qed "negateSnd_eq"; |
|
191 |
Addsimps [negateSnd_eq]; |
|
192 |
||
193 |
Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"; |
|
8785 | 194 |
by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def])); |
6917 | 195 |
qed "quorem_neg"; |
196 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
197 |
Goal "b ~= Numeral0 ==> quorem ((a,b), divAlg(a,b))"; |
6917 | 198 |
by (auto_tac (claset(), |
199 |
simpset() addsimps [quorem_0, divAlg_def])); |
|
200 |
by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct, |
|
201 |
negDivAlg_correct])); |
|
202 |
by (auto_tac (claset(), |
|
203 |
simpset() addsimps [quorem_def, linorder_neq_iff])); |
|
204 |
qed "divAlg_correct"; |
|
205 |
||
10701 | 206 |
(** Arbitrary definitions for division by zero. Useful to simplify |
6992 | 207 |
certain equations **) |
208 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
209 |
Goal "a div (Numeral0::int) = Numeral0"; |
6992 | 210 |
by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1); |
7035 | 211 |
qed "DIVISION_BY_ZERO_ZDIV"; (*NOT for adding to default simpset*) |
6992 | 212 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
213 |
Goal "a mod (Numeral0::int) = a"; |
6992 | 214 |
by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1); |
7035 | 215 |
qed "DIVISION_BY_ZERO_ZMOD"; (*NOT for adding to default simpset*) |
6992 | 216 |
|
7035 | 217 |
fun zdiv_undefined_case_tac s i = |
6992 | 218 |
case_tac s i THEN |
7035 | 219 |
asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_ZDIV, |
220 |
DIVISION_BY_ZERO_ZMOD]) i; |
|
6992 | 221 |
|
222 |
(** Basic laws about division and remainder **) |
|
223 |
||
224 |
Goal "(a::int) = b * (a div b) + (a mod b)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
225 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6917 | 226 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
227 |
by (auto_tac (claset(), |
|
228 |
simpset() addsimps [quorem_def, div_def, mod_def])); |
|
229 |
qed "zmod_zdiv_equality"; |
|
230 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
231 |
Goal "(Numeral0::int) < b ==> Numeral0 <= a mod b & a mod b < b"; |
6917 | 232 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
233 |
by (auto_tac (claset(), |
|
234 |
simpset() addsimps [quorem_def, mod_def])); |
|
235 |
bind_thm ("pos_mod_sign", result() RS conjunct1); |
|
236 |
bind_thm ("pos_mod_bound", result() RS conjunct2); |
|
237 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
238 |
Goal "b < (Numeral0::int) ==> a mod b <= Numeral0 & b < a mod b"; |
6917 | 239 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
240 |
by (auto_tac (claset(), |
|
241 |
simpset() addsimps [quorem_def, div_def, mod_def])); |
|
242 |
bind_thm ("neg_mod_sign", result() RS conjunct1); |
|
243 |
bind_thm ("neg_mod_bound", result() RS conjunct2); |
|
244 |
||
245 |
||
6992 | 246 |
(** proving general properties of div and mod **) |
247 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
248 |
Goal "b ~= Numeral0 ==> quorem ((a, b), (a div b, a mod b))"; |
6992 | 249 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
250 |
by (auto_tac |
|
251 |
(claset(), |
|
252 |
simpset() addsimps [quorem_def, linorder_neq_iff, |
|
253 |
pos_mod_sign,pos_mod_bound, |
|
254 |
neg_mod_sign, neg_mod_bound])); |
|
255 |
qed "quorem_div_mod"; |
|
256 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
257 |
Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a div b = q"; |
6992 | 258 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); |
259 |
qed "quorem_div"; |
|
260 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
261 |
Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a mod b = r"; |
6992 | 262 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); |
263 |
qed "quorem_mod"; |
|
264 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
265 |
Goal "[| (Numeral0::int) <= a; a < b |] ==> a div b = Numeral0"; |
6992 | 266 |
by (rtac quorem_div 1); |
267 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
|
6999 | 268 |
qed "div_pos_pos_trivial"; |
6992 | 269 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
270 |
Goal "[| a <= (Numeral0::int); b < a |] ==> a div b = Numeral0"; |
6992 | 271 |
by (rtac quorem_div 1); |
272 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
|
6999 | 273 |
qed "div_neg_neg_trivial"; |
274 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
275 |
Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = # -1"; |
6999 | 276 |
by (rtac quorem_div 1); |
277 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
|
278 |
qed "div_pos_neg_trivial"; |
|
279 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
280 |
(*There is no div_neg_pos_trivial because Numeral0 div b = Numeral0 would supersede it*) |
6992 | 281 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
282 |
Goal "[| (Numeral0::int) <= a; a < b |] ==> a mod b = a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
283 |
by (res_inst_tac [("q","Numeral0")] quorem_mod 1); |
6992 | 284 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
6999 | 285 |
qed "mod_pos_pos_trivial"; |
6992 | 286 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
287 |
Goal "[| a <= (Numeral0::int); b < a |] ==> a mod b = a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
288 |
by (res_inst_tac [("q","Numeral0")] quorem_mod 1); |
6992 | 289 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
6999 | 290 |
qed "mod_neg_neg_trivial"; |
291 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
292 |
Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a mod b = a+b"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
293 |
by (res_inst_tac [("q","# -1")] quorem_mod 1); |
6999 | 294 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
295 |
qed "mod_pos_neg_trivial"; |
|
296 |
||
297 |
(*There is no mod_neg_pos_trivial...*) |
|
6992 | 298 |
|
299 |
||
9945 | 300 |
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
6992 | 301 |
Goal "(-a) div (-b) = a div (b::int)"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
302 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 303 |
by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
304 |
RS quorem_div) 1); |
|
305 |
by Auto_tac; |
|
306 |
qed "zdiv_zminus_zminus"; |
|
307 |
Addsimps [zdiv_zminus_zminus]; |
|
308 |
||
9945 | 309 |
(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
6992 | 310 |
Goal "(-a) mod (-b) = - (a mod (b::int))"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
311 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 312 |
by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
313 |
RS quorem_mod) 1); |
|
314 |
by Auto_tac; |
|
315 |
qed "zmod_zminus_zminus"; |
|
316 |
Addsimps [zmod_zminus_zminus]; |
|
317 |
||
318 |
||
9945 | 319 |
(*** div, mod and unary minus ***) |
320 |
||
321 |
Goal "quorem((a,b),(q,r)) \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
322 |
\ ==> quorem ((-a,b), (if r=Numeral0 then -q else -q-Numeral1), \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
323 |
\ (if r=Numeral0 then Numeral0 else b-r))"; |
9945 | 324 |
by (auto_tac |
325 |
(claset(), |
|
326 |
simpset() addsimps split_ifs@ |
|
327 |
[quorem_def, linorder_neq_iff, |
|
328 |
zdiff_zmult_distrib2])); |
|
329 |
val lemma = result(); |
|
330 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
331 |
Goal "b ~= (Numeral0::int) \ |
10139 | 332 |
\ ==> (-a) div b = \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
333 |
\ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; |
9945 | 334 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
335 |
qed "zdiv_zminus1_eq_if"; |
|
336 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
337 |
Goal "(-a::int) mod b = (if a mod b = Numeral0 then Numeral0 else b - (a mod b))"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
338 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
9945 | 339 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
340 |
qed "zmod_zminus1_eq_if"; |
|
341 |
||
342 |
Goal "a div (-b) = (-a::int) div b"; |
|
343 |
by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1); |
|
344 |
by Auto_tac; |
|
345 |
qed "zdiv_zminus2"; |
|
346 |
||
347 |
Goal "a mod (-b) = - ((-a::int) mod b)"; |
|
348 |
by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1); |
|
349 |
by Auto_tac; |
|
350 |
qed "zmod_zminus2"; |
|
351 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
352 |
Goal "b ~= (Numeral0::int) \ |
10139 | 353 |
\ ==> a div (-b) = \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
354 |
\ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; |
9945 | 355 |
by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); |
356 |
qed "zdiv_zminus2_eq_if"; |
|
357 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
358 |
Goal "a mod (-b::int) = (if a mod b = Numeral0 then Numeral0 else (a mod b) - b)"; |
9945 | 359 |
by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); |
360 |
qed "zmod_zminus2_eq_if"; |
|
361 |
||
362 |
||
6992 | 363 |
(*** division of a number by itself ***) |
364 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
365 |
Goal "[| (Numeral0::int) < a; a = r + a*q; r < a |] ==> Numeral1 <= q"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
366 |
by (subgoal_tac "Numeral0 < a*q" 1); |
6992 | 367 |
by (arith_tac 2); |
9063 | 368 |
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
6992 | 369 |
val lemma1 = result(); |
370 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
371 |
Goal "[| (Numeral0::int) < a; a = r + a*q; Numeral0 <= r |] ==> q <= Numeral1"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
372 |
by (subgoal_tac "Numeral0 <= a*(Numeral1-q)" 1); |
6992 | 373 |
by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
9063 | 374 |
by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
6992 | 375 |
val lemma2 = result(); |
376 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
377 |
Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> q = Numeral1"; |
6992 | 378 |
by (asm_full_simp_tac |
379 |
(simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1); |
|
380 |
by (rtac order_antisym 1); |
|
381 |
by Safe_tac; |
|
382 |
by Auto_tac; |
|
383 |
by (res_inst_tac [("a", "-a"),("r", "-r")] lemma1 3); |
|
384 |
by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1); |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
385 |
by (REPEAT (force_tac (claset() addIs [lemma1,lemma2], |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
386 |
simpset() addsimps [zadd_commute, zmult_zminus]) 1)); |
6992 | 387 |
qed "self_quotient"; |
388 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
389 |
Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> r = Numeral0"; |
7499 | 390 |
by (ftac self_quotient 1); |
6992 | 391 |
by (assume_tac 1); |
392 |
by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); |
|
393 |
qed "self_remainder"; |
|
394 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
395 |
Goal "a ~= Numeral0 ==> a div a = (Numeral1::int)"; |
6992 | 396 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); |
397 |
qed "zdiv_self"; |
|
398 |
Addsimps [zdiv_self]; |
|
399 |
||
400 |
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
401 |
Goal "a mod a = (Numeral0::int)"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
402 |
by (zdiv_undefined_case_tac "a = Numeral0" 1); |
6992 | 403 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); |
404 |
qed "zmod_self"; |
|
405 |
Addsimps [zmod_self]; |
|
406 |
||
407 |
||
6917 | 408 |
(*** Computation of division and remainder ***) |
409 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
410 |
Goal "(Numeral0::int) div b = Numeral0"; |
6917 | 411 |
by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
412 |
qed "zdiv_zero"; |
6917 | 413 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
414 |
Goal "(Numeral0::int) < b ==> # -1 div b = # -1"; |
7035 | 415 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
416 |
qed "div_eq_minus1"; |
|
417 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
418 |
Goal "(Numeral0::int) mod b = Numeral0"; |
6917 | 419 |
by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
420 |
qed "zmod_zero"; |
6917 | 421 |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
422 |
Addsimps [zdiv_zero, zmod_zero]; |
6917 | 423 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
424 |
Goal "(Numeral0::int) < b ==> # -1 div b = # -1"; |
7035 | 425 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
426 |
qed "zdiv_minus1"; |
7035 | 427 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
428 |
Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1"; |
7035 | 429 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
430 |
qed "zmod_minus1"; |
7035 | 431 |
|
6917 | 432 |
(** a positive, b positive **) |
433 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
434 |
Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a div b = fst (posDivAlg(a,b))"; |
6917 | 435 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
436 |
qed "div_pos_pos"; |
|
437 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
438 |
Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"; |
6917 | 439 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
440 |
qed "mod_pos_pos"; |
|
441 |
||
442 |
(** a negative, b positive **) |
|
443 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
444 |
Goal "[| a < Numeral0; Numeral0 < b |] ==> a div b = fst (negDivAlg(a,b))"; |
6917 | 445 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
446 |
qed "div_neg_pos"; |
|
447 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
448 |
Goal "[| a < Numeral0; Numeral0 < b |] ==> a mod b = snd (negDivAlg(a,b))"; |
6917 | 449 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
450 |
qed "mod_neg_pos"; |
|
451 |
||
452 |
(** a positive, b negative **) |
|
453 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
454 |
Goal "[| Numeral0 < a; b < Numeral0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"; |
6917 | 455 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
456 |
qed "div_pos_neg"; |
|
457 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
458 |
Goal "[| Numeral0 < a; b < Numeral0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"; |
6917 | 459 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
460 |
qed "mod_pos_neg"; |
|
461 |
||
462 |
(** a negative, b negative **) |
|
463 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
464 |
Goal "[| a < Numeral0; b <= Numeral0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; |
6917 | 465 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
466 |
qed "div_neg_neg"; |
|
467 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
468 |
Goal "[| a < Numeral0; b <= Numeral0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"; |
6917 | 469 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
470 |
qed "mod_neg_neg"; |
|
471 |
||
9422 | 472 |
Addsimps (map (read_instantiate_sg (sign_of (the_context ())) |
6917 | 473 |
[("a", "number_of ?v"), ("b", "number_of ?w")]) |
474 |
[div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg, |
|
475 |
mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg, |
|
476 |
posDivAlg_eqn, negDivAlg_eqn]); |
|
6992 | 477 |
|
6917 | 478 |
|
479 |
(** Special-case simplification **) |
|
480 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
481 |
Goal "a mod (Numeral1::int) = Numeral0"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
482 |
by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_sign 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
483 |
by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_bound 2); |
6917 | 484 |
by Auto_tac; |
485 |
qed "zmod_1"; |
|
486 |
Addsimps [zmod_1]; |
|
487 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
488 |
Goal "a div (Numeral1::int) = a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
489 |
by (cut_inst_tac [("a","a"),("b","Numeral1")] zmod_zdiv_equality 1); |
6917 | 490 |
by Auto_tac; |
491 |
qed "zdiv_1"; |
|
492 |
Addsimps [zdiv_1]; |
|
493 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
494 |
Goal "a mod (# -1::int) = Numeral0"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
495 |
by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
496 |
by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2); |
6917 | 497 |
by Auto_tac; |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
498 |
qed "zmod_minus1_right"; |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
499 |
Addsimps [zmod_minus1_right]; |
6917 | 500 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
501 |
Goal "a div (# -1::int) = -a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
502 |
by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1); |
6917 | 503 |
by Auto_tac; |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
504 |
qed "zdiv_minus1_right"; |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
505 |
Addsimps [zdiv_minus1_right]; |
6917 | 506 |
|
507 |
||
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
508 |
(*** Monotonicity in the first argument (divisor) ***) |
6917 | 509 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
510 |
Goal "[| a <= a'; Numeral0 < (b::int) |] ==> a div b <= a' div b"; |
6917 | 511 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
6992 | 512 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
6917 | 513 |
by (rtac unique_quotient_lemma 1); |
514 |
by (etac subst 1); |
|
515 |
by (etac subst 1); |
|
516 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
|
517 |
qed "zdiv_mono1"; |
|
518 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
519 |
Goal "[| a <= a'; (b::int) < Numeral0 |] ==> a' div b <= a div b"; |
6917 | 520 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
6992 | 521 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
6917 | 522 |
by (rtac unique_quotient_lemma_neg 1); |
523 |
by (etac subst 1); |
|
524 |
by (etac subst 1); |
|
525 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound]))); |
|
526 |
qed "zdiv_mono1_neg"; |
|
527 |
||
528 |
||
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
529 |
(*** Monotonicity in the second argument (dividend) ***) |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
530 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
531 |
Goal "[| b*q + r = b'*q' + r'; Numeral0 <= b'*q' + r'; \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
532 |
\ r' < b'; Numeral0 <= r; Numeral0 < b'; b' <= b |] \ |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
533 |
\ ==> q <= (q'::int)"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
534 |
by (subgoal_tac "Numeral0 <= q'" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
535 |
by (subgoal_tac "Numeral0 < b'*(q' + Numeral1)" 2); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
536 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3); |
9063 | 537 |
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
538 |
by (subgoal_tac "b*q < b*(q' + Numeral1)" 1); |
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
539 |
by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
540 |
by (subgoal_tac "b*q = r' - r + b'*q'" 1); |
8918 | 541 |
by (Simp_tac 2); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
542 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
543 |
by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
544 |
by (rtac zmult_zle_mono1 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
545 |
by Auto_tac; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
546 |
qed "zdiv_mono2_lemma"; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
547 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
548 |
Goal "[| (Numeral0::int) <= a; Numeral0 < b'; b' <= b |] \ |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
549 |
\ ==> a div b <= a div b'"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
550 |
by (subgoal_tac "b ~= Numeral0" 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
551 |
by (arith_tac 2); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
552 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
6992 | 553 |
by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
554 |
by (rtac zdiv_mono2_lemma 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
555 |
by (etac subst 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
556 |
by (etac subst 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
557 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
558 |
qed "zdiv_mono2"; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
559 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
560 |
Goal "[| b*q + r = b'*q' + r'; b'*q' + r' < Numeral0; \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
561 |
\ r < b; Numeral0 <= r'; Numeral0 < b'; b' <= b |] \ |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
562 |
\ ==> q' <= (q::int)"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
563 |
by (subgoal_tac "q' < Numeral0" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
564 |
by (subgoal_tac "b'*q' < Numeral0" 2); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
565 |
by (arith_tac 3); |
9063 | 566 |
by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
567 |
by (subgoal_tac "b*q' < b*(q + Numeral1)" 1); |
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
568 |
by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
569 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
570 |
by (subgoal_tac "b*q' <= b'*q'" 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
571 |
by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
572 |
by (subgoal_tac "b'*q' < b + b*q" 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
573 |
by (Asm_simp_tac 2); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
574 |
by (arith_tac 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
575 |
qed "zdiv_mono2_neg_lemma"; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
576 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
577 |
Goal "[| a < (Numeral0::int); Numeral0 < b'; b' <= b |] \ |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
578 |
\ ==> a div b' <= a div b"; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
579 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
6992 | 580 |
by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
581 |
by (rtac zdiv_mono2_neg_lemma 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
582 |
by (etac subst 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
583 |
by (etac subst 1); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
584 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
585 |
qed "zdiv_mono2_neg"; |
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
586 |
|
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
587 |
|
6992 | 588 |
(*** More algebraic laws for div and mod ***) |
6943
2cde117d2738
faster division algorithm; monotonicity of div in 2nd arg
paulson
parents:
6917
diff
changeset
|
589 |
|
6992 | 590 |
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) |
591 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
592 |
Goal "[| quorem((b,c),(q,r)); c ~= Numeral0 |] \ |
6992 | 593 |
\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; |
594 |
by (auto_tac |
|
595 |
(claset(), |
|
8918 | 596 |
simpset() addsimps split_ifs@ |
6992 | 597 |
[quorem_def, linorder_neq_iff, |
598 |
zadd_zmult_distrib2, |
|
599 |
pos_mod_sign,pos_mod_bound, |
|
600 |
neg_mod_sign, neg_mod_bound])); |
|
7549 | 601 |
by (ALLGOALS(rtac zmod_zdiv_equality)); |
6992 | 602 |
val lemma = result(); |
603 |
||
604 |
Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
605 |
by (zdiv_undefined_case_tac "c = Numeral0" 1); |
6992 | 606 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
607 |
qed "zdiv_zmult1_eq"; |
|
608 |
||
609 |
Goal "(a*b) mod c = a*(b mod c) mod (c::int)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
610 |
by (zdiv_undefined_case_tac "c = Numeral0" 1); |
6992 | 611 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
612 |
qed "zmod_zmult1_eq"; |
|
613 |
||
9509 | 614 |
Goal "(a*b) mod (c::int) = ((a mod c) * b) mod c"; |
615 |
by (rtac trans 1); |
|
616 |
by (res_inst_tac [("s","b*a mod c")] trans 1); |
|
617 |
by (rtac zmod_zmult1_eq 2); |
|
618 |
by (ALLGOALS (simp_tac (simpset() addsimps [zmult_commute]))); |
|
619 |
qed "zmod_zmult1_eq'"; |
|
620 |
||
621 |
Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"; |
|
622 |
by (rtac (zmod_zmult1_eq' RS trans) 1); |
|
623 |
by (rtac zmod_zmult1_eq 1); |
|
624 |
qed "zmod_zmult_distrib"; |
|
625 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
626 |
Goal "b ~= (Numeral0::int) ==> (a*b) div b = a"; |
6992 | 627 |
by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); |
628 |
qed "zdiv_zmult_self1"; |
|
629 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
630 |
Goal "b ~= (Numeral0::int) ==> (b*a) div b = a"; |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
631 |
by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1); |
6992 | 632 |
qed "zdiv_zmult_self2"; |
633 |
||
634 |
Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; |
|
635 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
636 |
Goal "(a*b) mod b = (Numeral0::int)"; |
6992 | 637 |
by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); |
638 |
qed "zmod_zmult_self1"; |
|
639 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
640 |
Goal "(b*a) mod b = (Numeral0::int)"; |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
641 |
by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
6992 | 642 |
qed "zmod_zmult_self2"; |
643 |
||
644 |
Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
|
645 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
646 |
Goal "(m mod d = Numeral0) = (EX q::int. m = d*q)"; |
10200 | 647 |
by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1); |
648 |
by Auto_tac; |
|
649 |
qed "zmod_eq_0_iff"; |
|
650 |
AddSDs [zmod_eq_0_iff RS iffD1]; |
|
651 |
||
6992 | 652 |
|
653 |
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
|
6917 | 654 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
655 |
Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= Numeral0 |] \ |
6992 | 656 |
\ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; |
657 |
by (auto_tac |
|
658 |
(claset(), |
|
8918 | 659 |
simpset() addsimps split_ifs@ |
6992 | 660 |
[quorem_def, linorder_neq_iff, |
661 |
zadd_zmult_distrib2, |
|
662 |
pos_mod_sign,pos_mod_bound, |
|
663 |
neg_mod_sign, neg_mod_bound])); |
|
7549 | 664 |
by (ALLGOALS(rtac zmod_zdiv_equality)); |
6992 | 665 |
val lemma = result(); |
666 |
||
6999 | 667 |
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
6992 | 668 |
Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
669 |
by (zdiv_undefined_case_tac "c = Numeral0" 1); |
6992 | 670 |
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
671 |
MRS lemma RS quorem_div]) 1); |
|
672 |
qed "zdiv_zadd1_eq"; |
|
673 |
||
674 |
Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
675 |
by (zdiv_undefined_case_tac "c = Numeral0" 1); |
6992 | 676 |
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
677 |
MRS lemma RS quorem_mod]) 1); |
|
678 |
qed "zmod_zadd1_eq"; |
|
679 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
680 |
Goal "(a mod b) div b = (Numeral0::int)"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
681 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 682 |
by (auto_tac (claset(), |
6999 | 683 |
simpset() addsimps [linorder_neq_iff, |
684 |
pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, |
|
685 |
neg_mod_sign, neg_mod_bound, div_neg_neg_trivial])); |
|
6992 | 686 |
qed "mod_div_trivial"; |
687 |
Addsimps [mod_div_trivial]; |
|
688 |
||
689 |
Goal "(a mod b) mod b = a mod (b::int)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
690 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 691 |
by (auto_tac (claset(), |
6999 | 692 |
simpset() addsimps [linorder_neq_iff, |
693 |
pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, |
|
694 |
neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial])); |
|
6992 | 695 |
qed "mod_mod_trivial"; |
696 |
Addsimps [mod_mod_trivial]; |
|
697 |
||
9509 | 698 |
Goal "(a+b) mod (c::int) = ((a mod c) + b) mod c"; |
699 |
by (rtac (trans RS sym) 1); |
|
700 |
by (rtac zmod_zadd1_eq 1); |
|
701 |
by (Simp_tac 1); |
|
702 |
by (rtac (zmod_zadd1_eq RS sym) 1); |
|
703 |
qed "zmod_zadd_left_eq"; |
|
704 |
||
705 |
Goal "(a+b) mod (c::int) = (a + (b mod c)) mod c"; |
|
706 |
by (rtac (trans RS sym) 1); |
|
707 |
by (rtac zmod_zadd1_eq 1); |
|
708 |
by (Simp_tac 1); |
|
709 |
by (rtac (zmod_zadd1_eq RS sym) 1); |
|
710 |
qed "zmod_zadd_right_eq"; |
|
711 |
||
6992 | 712 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
713 |
Goal "a ~= (Numeral0::int) ==> (a+b) div a = b div a + Numeral1"; |
6992 | 714 |
by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); |
715 |
qed "zdiv_zadd_self1"; |
|
716 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
717 |
Goal "a ~= (Numeral0::int) ==> (b+a) div a = b div a + Numeral1"; |
6992 | 718 |
by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); |
719 |
qed "zdiv_zadd_self2"; |
|
720 |
Addsimps [zdiv_zadd_self1, zdiv_zadd_self2]; |
|
721 |
||
722 |
Goal "(a+b) mod a = b mod (a::int)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
723 |
by (zdiv_undefined_case_tac "a = Numeral0" 1); |
6992 | 724 |
by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
725 |
qed "zmod_zadd_self1"; |
|
726 |
||
727 |
Goal "(b+a) mod a = b mod (a::int)"; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
728 |
by (zdiv_undefined_case_tac "a = Numeral0" 1); |
6992 | 729 |
by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
730 |
qed "zmod_zadd_self2"; |
|
731 |
Addsimps [zmod_zadd_self1, zmod_zadd_self2]; |
|
732 |
||
733 |
||
734 |
(*** proving a div (b*c) = (a div b) div c ***) |
|
735 |
||
736 |
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but |
|
737 |
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
|
738 |
to cause particular problems.*) |
|
739 |
||
740 |
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
|
6917 | 741 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
742 |
Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b*c < b*(q mod c) + r"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
743 |
by (subgoal_tac "b * (c - q mod c) < r * Numeral1" 1); |
6992 | 744 |
by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
745 |
by (rtac order_le_less_trans 1); |
|
746 |
by (etac zmult_zless_mono1 2); |
|
747 |
by (rtac zmult_zle_mono2_neg 1); |
|
748 |
by (auto_tac |
|
749 |
(claset(), |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
750 |
simpset() addsimps zcompare_rls@ |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
751 |
[zadd_commute, add1_zle_eq, pos_mod_bound])); |
6992 | 752 |
val lemma1 = result(); |
753 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
754 |
Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b * (q mod c) + r <= Numeral0"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
755 |
by (subgoal_tac "b * (q mod c) <= Numeral0" 1); |
6992 | 756 |
by (arith_tac 1); |
9063 | 757 |
by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1); |
6992 | 758 |
val lemma2 = result(); |
759 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
760 |
Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> Numeral0 <= b * (q mod c) + r"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
761 |
by (subgoal_tac "Numeral0 <= b * (q mod c)" 1); |
6992 | 762 |
by (arith_tac 1); |
9063 | 763 |
by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1); |
6992 | 764 |
val lemma3 = result(); |
765 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
766 |
Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> b * (q mod c) + r < b * c"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
767 |
by (subgoal_tac "r * Numeral1 < b * (c - q mod c)" 1); |
6992 | 768 |
by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
769 |
by (rtac order_less_le_trans 1); |
|
770 |
by (etac zmult_zless_mono1 1); |
|
771 |
by (rtac zmult_zle_mono2 2); |
|
772 |
by (auto_tac |
|
773 |
(claset(), |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
774 |
simpset() addsimps zcompare_rls@ |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
775 |
[zadd_commute, add1_zle_eq, pos_mod_bound])); |
6992 | 776 |
val lemma4 = result(); |
777 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
778 |
Goal "[| quorem ((a,b), (q,r)); b ~= Numeral0; Numeral0 < c |] \ |
6992 | 779 |
\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; |
8918 | 780 |
by (auto_tac |
6992 | 781 |
(claset(), |
8918 | 782 |
simpset() addsimps zmult_ac@ |
783 |
[zmod_zdiv_equality, quorem_def, linorder_neq_iff, |
|
9063 | 784 |
int_0_less_mult_iff, |
6992 | 785 |
zadd_zmult_distrib2 RS sym, |
786 |
lemma1, lemma2, lemma3, lemma4])); |
|
787 |
val lemma = result(); |
|
788 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
789 |
Goal "(Numeral0::int) < c ==> a div (b*c) = (a div b) div c"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
790 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 791 |
by (force_tac (claset(), |
792 |
simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, |
|
793 |
zmult_eq_0_iff]) 1); |
|
794 |
qed "zdiv_zmult2_eq"; |
|
6917 | 795 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
796 |
Goal "(Numeral0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
797 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 798 |
by (force_tac (claset(), |
799 |
simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, |
|
800 |
zmult_eq_0_iff]) 1); |
|
801 |
qed "zmod_zmult2_eq"; |
|
802 |
||
803 |
||
804 |
(*** Cancellation of common factors in "div" ***) |
|
805 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
806 |
Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; |
6992 | 807 |
by (stac zdiv_zmult2_eq 1); |
808 |
by Auto_tac; |
|
809 |
val lemma1 = result(); |
|
810 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
811 |
Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7086
diff
changeset
|
812 |
by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1); |
6992 | 813 |
by (rtac lemma1 2); |
8918 | 814 |
by Auto_tac; |
6992 | 815 |
val lemma2 = result(); |
816 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
817 |
Goal "c ~= (Numeral0::int) ==> (c*a) div (c*b) = a div b"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
818 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
6992 | 819 |
by (auto_tac |
820 |
(claset(), |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
821 |
simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
6992 | 822 |
lemma1, lemma2])); |
823 |
qed "zdiv_zmult_zmult1"; |
|
6917 | 824 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
825 |
Goal "c ~= (Numeral0::int) ==> (a*c) div (b*c) = a div b"; |
6992 | 826 |
by (dtac zdiv_zmult_zmult1 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
827 |
by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
6992 | 828 |
qed "zdiv_zmult_zmult2"; |
829 |
||
830 |
||
831 |
||
832 |
(*** Distribution of factors over "mod" ***) |
|
833 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
834 |
Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
6992 | 835 |
by (stac zmod_zmult2_eq 1); |
836 |
by Auto_tac; |
|
837 |
val lemma1 = result(); |
|
838 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
839 |
Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7086
diff
changeset
|
840 |
by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1); |
6992 | 841 |
by (rtac lemma1 2); |
8918 | 842 |
by Auto_tac; |
6992 | 843 |
val lemma2 = result(); |
844 |
||
6999 | 845 |
Goal "(c*a) mod (c*b) = (c::int) * (a mod b)"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
846 |
by (zdiv_undefined_case_tac "b = Numeral0" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
847 |
by (zdiv_undefined_case_tac "c = Numeral0" 1); |
6992 | 848 |
by (auto_tac |
849 |
(claset(), |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
850 |
simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
6992 | 851 |
lemma1, lemma2])); |
852 |
qed "zmod_zmult_zmult1"; |
|
853 |
||
6999 | 854 |
Goal "(a*c) mod (b*c) = (a mod b) * (c::int)"; |
855 |
by (cut_inst_tac [("c","c")] zmod_zmult_zmult1 1); |
|
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
856 |
by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
6992 | 857 |
qed "zmod_zmult_zmult2"; |
858 |
||
859 |
||
6999 | 860 |
(*** Speeding up the division algorithm with shifting ***) |
6992 | 861 |
|
7035 | 862 |
(** computing "div" by shifting **) |
6999 | 863 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
864 |
Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) div (# 2*a) = b div a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
865 |
by (zdiv_undefined_case_tac "a = Numeral0" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
866 |
by (subgoal_tac "Numeral1 <= a" 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
867 |
by (arith_tac 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
868 |
by (subgoal_tac "Numeral1 < a * # 2" 1); |
8785 | 869 |
by (arith_tac 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
870 |
by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
871 |
by (rtac zmult_zle_mono2 2); |
6999 | 872 |
by (auto_tac (claset(), |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
873 |
simpset() addsimps [zadd_commute, zmult_commute, |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
874 |
add1_zle_eq, pos_mod_bound])); |
6999 | 875 |
by (stac zdiv_zadd1_eq 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
876 |
by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
877 |
div_pos_pos_trivial]) 1); |
6999 | 878 |
by (stac div_pos_pos_trivial 1); |
8765
1bc30ff5fc54
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
paulson
parents:
8624
diff
changeset
|
879 |
by (asm_simp_tac (simpset() |
8918 | 880 |
addsimps [mod_pos_pos_trivial, |
7549 | 881 |
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
6999 | 882 |
by (auto_tac (claset(), |
883 |
simpset() addsimps [mod_pos_pos_trivial])); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
884 |
by (subgoal_tac "Numeral0 <= b mod a" 1); |
8785 | 885 |
by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
886 |
by (arith_tac 1); |
|
9063 | 887 |
qed "pos_zdiv_mult_2"; |
6999 | 888 |
|
889 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
890 |
Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
891 |
by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1); |
9063 | 892 |
by (rtac pos_zdiv_mult_2 2); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
893 |
by (auto_tac (claset(), |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
894 |
simpset() addsimps [zmult_zminus_right])); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
895 |
by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1); |
6999 | 896 |
by (Simp_tac 2); |
897 |
by (asm_full_simp_tac (HOL_ss |
|
898 |
addsimps [zdiv_zminus_zminus, zdiff_def, |
|
899 |
zminus_zadd_distrib RS sym]) 1); |
|
9063 | 900 |
qed "neg_zdiv_mult_2"; |
6999 | 901 |
|
902 |
||
903 |
(*Not clear why this must be proved separately; probably number_of causes |
|
904 |
simplification problems*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
905 |
Goal "~ Numeral0 <= x ==> x <= (Numeral0::int)"; |
7035 | 906 |
by Auto_tac; |
6999 | 907 |
val lemma = result(); |
908 |
||
909 |
Goal "number_of (v BIT b) div number_of (w BIT False) = \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
910 |
\ (if ~b | (Numeral0::int) <= number_of w \ |
6999 | 911 |
\ then number_of v div (number_of w) \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
912 |
\ else (number_of v + (Numeral1::int)) div (number_of w))"; |
9422 | 913 |
by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
7035 | 914 |
by (asm_simp_tac (simpset() |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
915 |
delsimps [thm "number_of_reorient"]@bin_arith_extra_simps@bin_rel_simps |
10701 | 916 |
addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, |
917 |
neg_zdiv_mult_2]) 1); |
|
6999 | 918 |
qed "zdiv_number_of_BIT"; |
919 |
Addsimps [zdiv_number_of_BIT]; |
|
920 |
||
921 |
||
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
922 |
(** computing "mod" by shifting (proofs resemble those for "div") **) |
7035 | 923 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
924 |
Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
925 |
by (zdiv_undefined_case_tac "a = Numeral0" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
926 |
by (subgoal_tac "Numeral1 <= a" 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
927 |
by (arith_tac 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
928 |
by (subgoal_tac "Numeral1 < a * # 2" 1); |
8785 | 929 |
by (arith_tac 2); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
930 |
by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
931 |
by (rtac zmult_zle_mono2 2); |
7035 | 932 |
by (auto_tac (claset(), |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
933 |
simpset() addsimps [zadd_commute, zmult_commute, |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
934 |
add1_zle_eq, pos_mod_bound])); |
7035 | 935 |
by (stac zmod_zadd1_eq 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
936 |
by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
937 |
mod_pos_pos_trivial]) 1); |
7035 | 938 |
by (rtac mod_pos_pos_trivial 1); |
8765
1bc30ff5fc54
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
paulson
parents:
8624
diff
changeset
|
939 |
by (asm_simp_tac (simpset() |
8918 | 940 |
addsimps [mod_pos_pos_trivial, |
7549 | 941 |
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
7035 | 942 |
by (auto_tac (claset(), |
943 |
simpset() addsimps [mod_pos_pos_trivial])); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
944 |
by (subgoal_tac "Numeral0 <= b mod a" 1); |
8785 | 945 |
by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
946 |
by (arith_tac 1); |
|
9063 | 947 |
qed "pos_zmod_mult_2"; |
7035 | 948 |
|
949 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
950 |
Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1"; |
7035 | 951 |
by (subgoal_tac |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
952 |
"(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1); |
9063 | 953 |
by (rtac pos_zmod_mult_2 2); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
954 |
by (auto_tac (claset(), |
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
955 |
simpset() addsimps [zmult_zminus_right])); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
956 |
by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1); |
7035 | 957 |
by (Simp_tac 2); |
958 |
by (asm_full_simp_tac (HOL_ss |
|
959 |
addsimps [zmod_zminus_zminus, zdiff_def, |
|
960 |
zminus_zadd_distrib RS sym]) 1); |
|
7086 | 961 |
by (dtac (zminus_equation RS iffD1 RS sym) 1); |
8918 | 962 |
by Auto_tac; |
9063 | 963 |
qed "neg_zmod_mult_2"; |
7035 | 964 |
|
965 |
Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |
|
966 |
\ (if b then \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
967 |
\ if (Numeral0::int) <= number_of w \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
968 |
\ then # 2 * (number_of v mod number_of w) + Numeral1 \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
969 |
\ else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
970 |
\ else # 2 * (number_of v mod number_of w))"; |
9422 | 971 |
by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
7035 | 972 |
by (asm_simp_tac (simpset() |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
973 |
delsimps bin_arith_extra_simps@bin_rel_simps |
8787 | 974 |
addsimps [zmod_zmult_zmult1, |
9063 | 975 |
pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1); |
7035 | 976 |
qed "zmod_number_of_BIT"; |
977 |
||
978 |
Addsimps [zmod_number_of_BIT]; |
|
979 |
||
980 |
||
981 |
(** Quotients of signs **) |
|
982 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
983 |
Goal "[| a < (Numeral0::int); Numeral0 < b |] ==> a div b < Numeral0"; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
984 |
by (subgoal_tac "a div b <= # -1" 1); |
7035 | 985 |
by (Force_tac 1); |
986 |
by (rtac order_trans 1); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
987 |
by (res_inst_tac [("a'","# -1")] zdiv_mono1 1); |
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7035
diff
changeset
|
988 |
by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7086
diff
changeset
|
989 |
qed "div_neg_pos_less0"; |
7035 | 990 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
991 |
Goal "[| (Numeral0::int) <= a; b < Numeral0 |] ==> a div b <= Numeral0"; |
7035 | 992 |
by (dtac zdiv_mono1_neg 1); |
993 |
by Auto_tac; |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7086
diff
changeset
|
994 |
qed "div_nonneg_neg_le0"; |
7035 | 995 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
996 |
Goal "(Numeral0::int) < b ==> (Numeral0 <= a div b) = (Numeral0 <= a)"; |
7035 | 997 |
by Auto_tac; |
998 |
by (dtac zdiv_mono1 2); |
|
999 |
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); |
|
1000 |
by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7086
diff
changeset
|
1001 |
by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); |
7035 | 1002 |
qed "pos_imp_zdiv_nonneg_iff"; |
1003 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
1004 |
Goal "b < (Numeral0::int) ==> (Numeral0 <= a div b) = (a <= (Numeral0::int))"; |
7035 | 1005 |
by (stac (zdiv_zminus_zminus RS sym) 1); |
1006 |
by (stac pos_imp_zdiv_nonneg_iff 1); |
|
1007 |
by Auto_tac; |
|
1008 |
qed "neg_imp_zdiv_nonneg_iff"; |
|
1009 |
||
1010 |
(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
1011 |
Goal "(Numeral0::int) < b ==> (a div b < Numeral0) = (a < Numeral0)"; |
7035 | 1012 |
by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1013 |
pos_imp_zdiv_nonneg_iff]) 1); |
|
1014 |
qed "pos_imp_zdiv_neg_iff"; |
|
1015 |
||
1016 |
(*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10701
diff
changeset
|
1017 |
Goal "b < (Numeral0::int) ==> (a div b < Numeral0) = (Numeral0 < a)"; |
7035 | 1018 |
by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1019 |
neg_imp_zdiv_nonneg_iff]) 1); |
|
1020 |
qed "neg_imp_zdiv_neg_iff"; |