|
1 theory IntEx2 |
|
2 imports "../Quotient" "../Quotient_Product" Nat |
|
3 (*uses |
|
4 ("Tools/numeral.ML") |
|
5 ("Tools/numeral_syntax.ML") |
|
6 ("Tools/int_arith.ML")*) |
|
7 begin |
|
8 |
|
9 fun |
|
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
|
11 where |
|
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
13 |
|
14 quotient_type int = "nat \<times> nat" / intrel |
|
15 unfolding equivp_def |
|
16 by (auto simp add: mem_def expand_fun_eq) |
|
17 |
|
18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
|
19 begin |
|
20 |
|
21 ML {* @{term "0 \<Colon> int"} *} |
|
22 |
|
23 quotient_definition |
|
24 "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" |
|
25 |
|
26 quotient_definition |
|
27 "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" |
|
28 |
|
29 fun |
|
30 plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
31 where |
|
32 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
|
33 |
|
34 quotient_definition |
|
35 "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw" |
|
36 |
|
37 fun |
|
38 uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
39 where |
|
40 "uminus_raw (x, y) = (y, x)" |
|
41 |
|
42 quotient_definition |
|
43 "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw" |
|
44 |
|
45 definition |
|
46 minus_int_def [code del]: "z - w = z + (-w\<Colon>int)" |
|
47 |
|
48 fun |
|
49 mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
50 where |
|
51 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
|
52 |
|
53 quotient_definition |
|
54 mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw" |
|
55 |
|
56 fun |
|
57 le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
58 where |
|
59 "le_raw (x, y) (u, v) = (x+v \<le> u+y)" |
|
60 |
|
61 quotient_definition |
|
62 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw" |
|
63 |
|
64 definition |
|
65 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
|
66 |
|
67 definition |
|
68 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)" |
|
69 |
|
70 definition |
|
71 zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)" |
|
72 |
|
73 instance .. |
|
74 |
|
75 end |
|
76 |
|
77 lemma plus_raw_rsp[quot_respect]: |
|
78 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
|
79 by auto |
|
80 |
|
81 lemma uminus_raw_rsp[quot_respect]: |
|
82 shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw" |
|
83 by auto |
|
84 |
|
85 lemma mult_raw_fst: |
|
86 assumes a: "x \<approx> z" |
|
87 shows "mult_raw x y \<approx> mult_raw z y" |
|
88 using a |
|
89 apply(cases x, cases y, cases z) |
|
90 apply(auto simp add: mult_raw.simps intrel.simps) |
|
91 apply(rename_tac u v w x y z) |
|
92 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
93 apply(simp add: mult_ac) |
|
94 apply(simp add: add_mult_distrib [symmetric]) |
|
95 done |
|
96 |
|
97 lemma mult_raw_snd: |
|
98 assumes a: "x \<approx> z" |
|
99 shows "mult_raw y x \<approx> mult_raw y z" |
|
100 using a |
|
101 apply(cases x, cases y, cases z) |
|
102 apply(auto simp add: mult_raw.simps intrel.simps) |
|
103 apply(rename_tac u v w x y z) |
|
104 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
105 apply(simp add: mult_ac) |
|
106 apply(simp add: add_mult_distrib [symmetric]) |
|
107 done |
|
108 |
|
109 lemma mult_raw_rsp[quot_respect]: |
|
110 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
|
111 apply(simp only: fun_rel_def) |
|
112 apply(rule allI | rule impI)+ |
|
113 apply(rule equivp_transp[OF int_equivp]) |
|
114 apply(rule mult_raw_fst) |
|
115 apply(assumption) |
|
116 apply(rule mult_raw_snd) |
|
117 apply(assumption) |
|
118 done |
|
119 |
|
120 lemma le_raw_rsp[quot_respect]: |
|
121 shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw" |
|
122 by auto |
|
123 |
|
124 lemma plus_assoc_raw: |
|
125 shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)" |
|
126 by (cases i, cases j, cases k) (simp) |
|
127 |
|
128 lemma plus_sym_raw: |
|
129 shows "plus_raw i j \<approx> plus_raw j i" |
|
130 by (cases i, cases j) (simp) |
|
131 |
|
132 lemma plus_zero_raw: |
|
133 shows "plus_raw (0, 0) i \<approx> i" |
|
134 by (cases i) (simp) |
|
135 |
|
136 lemma plus_minus_zero_raw: |
|
137 shows "plus_raw (uminus_raw i) i \<approx> (0, 0)" |
|
138 by (cases i) (simp) |
|
139 |
|
140 lemma times_assoc_raw: |
|
141 shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)" |
|
142 by (cases i, cases j, cases k) |
|
143 (simp add: algebra_simps) |
|
144 |
|
145 lemma times_sym_raw: |
|
146 shows "mult_raw i j \<approx> mult_raw j i" |
|
147 by (cases i, cases j) (simp add: algebra_simps) |
|
148 |
|
149 lemma times_one_raw: |
|
150 shows "mult_raw (1, 0) i \<approx> i" |
|
151 by (cases i) (simp) |
|
152 |
|
153 lemma times_plus_comm_raw: |
|
154 shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)" |
|
155 by (cases i, cases j, cases k) |
|
156 (simp add: algebra_simps) |
|
157 |
|
158 lemma one_zero_distinct: |
|
159 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
|
160 by simp |
|
161 |
|
162 text{* The integers form a @{text comm_ring_1}*} |
|
163 |
|
164 instance int :: comm_ring_1 |
|
165 proof |
|
166 fix i j k :: int |
|
167 show "(i + j) + k = i + (j + k)" |
|
168 by (lifting plus_assoc_raw) |
|
169 show "i + j = j + i" |
|
170 by (lifting plus_sym_raw) |
|
171 show "0 + i = (i::int)" |
|
172 by (lifting plus_zero_raw) |
|
173 show "- i + i = 0" |
|
174 by (lifting plus_minus_zero_raw) |
|
175 show "i - j = i + - j" |
|
176 by (simp add: minus_int_def) |
|
177 show "(i * j) * k = i * (j * k)" |
|
178 by (lifting times_assoc_raw) |
|
179 show "i * j = j * i" |
|
180 by (lifting times_sym_raw) |
|
181 show "1 * i = i" |
|
182 by (lifting times_one_raw) |
|
183 show "(i + j) * k = i * k + j * k" |
|
184 by (lifting times_plus_comm_raw) |
|
185 show "0 \<noteq> (1::int)" |
|
186 by (lifting one_zero_distinct) |
|
187 qed |
|
188 |
|
189 lemma plus_raw_rsp_aux: |
|
190 assumes a: "a \<approx> b" "c \<approx> d" |
|
191 shows "plus_raw a c \<approx> plus_raw b d" |
|
192 using a |
|
193 by (cases a, cases b, cases c, cases d) |
|
194 (simp) |
|
195 |
|
196 lemma add: |
|
197 "(abs_int (x,y)) + (abs_int (u,v)) = |
|
198 (abs_int (x + u, y + v))" |
|
199 apply(simp add: plus_int_def id_simps) |
|
200 apply(fold plus_raw.simps) |
|
201 apply(rule Quotient_rel_abs[OF Quotient_int]) |
|
202 apply(rule plus_raw_rsp_aux) |
|
203 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
|
204 done |
|
205 |
|
206 definition int_of_nat_raw: |
|
207 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
|
208 |
|
209 quotient_definition |
|
210 "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" |
|
211 |
|
212 lemma[quot_respect]: |
|
213 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
|
214 by (simp add: equivp_reflp[OF int_equivp]) |
|
215 |
|
216 lemma int_of_nat: |
|
217 shows "of_nat m = int_of_nat m" |
|
218 apply (induct m) |
|
219 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add) |
|
220 done |
|
221 |
|
222 lemma le_antisym_raw: |
|
223 shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j" |
|
224 by (cases i, cases j) (simp) |
|
225 |
|
226 lemma le_refl_raw: |
|
227 shows "le_raw i i" |
|
228 by (cases i) (simp) |
|
229 |
|
230 lemma le_trans_raw: |
|
231 shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k" |
|
232 by (cases i, cases j, cases k) (simp) |
|
233 |
|
234 lemma le_cases_raw: |
|
235 shows "le_raw i j \<or> le_raw j i" |
|
236 by (cases i, cases j) |
|
237 (simp add: linorder_linear) |
|
238 |
|
239 instance int :: linorder |
|
240 proof |
|
241 fix i j k :: int |
|
242 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
|
243 by (lifting le_antisym_raw) |
|
244 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
|
245 by (auto simp add: less_int_def dest: antisym) |
|
246 show "i \<le> i" |
|
247 by (lifting le_refl_raw) |
|
248 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
|
249 by (lifting le_trans_raw) |
|
250 show "i \<le> j \<or> j \<le> i" |
|
251 by (lifting le_cases_raw) |
|
252 qed |
|
253 |
|
254 instantiation int :: distrib_lattice |
|
255 begin |
|
256 |
|
257 definition |
|
258 "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min" |
|
259 |
|
260 definition |
|
261 "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max" |
|
262 |
|
263 instance |
|
264 by intro_classes |
|
265 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
|
266 |
|
267 end |
|
268 |
|
269 lemma le_plus_raw: |
|
270 shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)" |
|
271 by (cases i, cases j, cases k) (simp) |
|
272 |
|
273 |
|
274 instance int :: ordered_cancel_ab_semigroup_add |
|
275 proof |
|
276 fix i j k :: int |
|
277 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
|
278 by (lifting le_plus_raw) |
|
279 qed |
|
280 |
|
281 abbreviation |
|
282 "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)" |
|
283 |
|
284 lemma zmult_zless_mono2_lemma: |
|
285 fixes i j::int |
|
286 and k::nat |
|
287 shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j" |
|
288 apply(induct "k") |
|
289 apply(simp) |
|
290 apply(case_tac "k = 0") |
|
291 apply(simp_all add: left_distrib add_strict_mono) |
|
292 done |
|
293 |
|
294 lemma zero_le_imp_eq_int_raw: |
|
295 fixes k::"(nat \<times> nat)" |
|
296 shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
|
297 apply(cases k) |
|
298 apply(simp add:int_of_nat_raw) |
|
299 apply(auto) |
|
300 apply(rule_tac i="b" and j="a" in less_Suc_induct) |
|
301 apply(auto) |
|
302 done |
|
303 |
|
304 lemma zero_le_imp_eq_int: |
|
305 fixes k::int |
|
306 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
|
307 unfolding less_int_def int_of_nat |
|
308 by (lifting zero_le_imp_eq_int_raw) |
|
309 |
|
310 lemma zmult_zless_mono2: |
|
311 fixes i j k::int |
|
312 assumes a: "i < j" "0 < k" |
|
313 shows "k * i < k * j" |
|
314 using a |
|
315 using a |
|
316 apply(drule_tac zero_le_imp_eq_int) |
|
317 apply(auto simp add: zmult_zless_mono2_lemma) |
|
318 done |
|
319 |
|
320 text{*The integers form an ordered integral domain*} |
|
321 instance int :: linordered_idom |
|
322 proof |
|
323 fix i j k :: int |
|
324 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
|
325 by (rule zmult_zless_mono2) |
|
326 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
|
327 by (simp only: zabs_def) |
|
328 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
|
329 by (simp only: zsgn_def) |
|
330 qed |
|
331 |
|
332 lemmas int_distrib = |
|
333 left_distrib [of "z1::int" "z2" "w", standard] |
|
334 right_distrib [of "w::int" "z1" "z2", standard] |
|
335 left_diff_distrib [of "z1::int" "z2" "w", standard] |
|
336 right_diff_distrib [of "w::int" "z1" "z2", standard] |
|
337 |
|
338 |
|
339 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} |
|
340 |
|
341 (* |
|
342 context ring_1 |
|
343 begin |
|
344 |
|
345 |
|
346 definition |
|
347 of_int :: "int \<Rightarrow> 'a" |
|
348 where |
|
349 "of_int |
|
350 *) |
|
351 |
|
352 |
|
353 subsection {* Binary representation *} |
|
354 |
|
355 text {* |
|
356 This formalization defines binary arithmetic in terms of the integers |
|
357 rather than using a datatype. This avoids multiple representations (leading |
|
358 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text |
|
359 int_of_binary}, for the numerical interpretation. |
|
360 |
|
361 The representation expects that @{text "(m mod 2)"} is 0 or 1, |
|
362 even if m is negative; |
|
363 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus |
|
364 @{text "-5 = (-3)*2 + 1"}. |
|
365 |
|
366 This two's complement binary representation derives from the paper |
|
367 "An Efficient Representation of Arithmetic for Term Rewriting" by |
|
368 Dave Cohen and Phil Watson, Rewriting Techniques and Applications, |
|
369 Springer LNCS 488 (240-251), 1991. |
|
370 *} |
|
371 |
|
372 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} |
|
373 |
|
374 definition |
|
375 Pls :: int where |
|
376 [code del]: "Pls = 0" |
|
377 |
|
378 definition |
|
379 Min :: int where |
|
380 [code del]: "Min = - 1" |
|
381 |
|
382 definition |
|
383 Bit0 :: "int \<Rightarrow> int" where |
|
384 [code del]: "Bit0 k = k + k" |
|
385 |
|
386 definition |
|
387 Bit1 :: "int \<Rightarrow> int" where |
|
388 [code del]: "Bit1 k = 1 + k + k" |
|
389 |
|
390 class number = -- {* for numeric types: nat, int, real, \dots *} |
|
391 fixes number_of :: "int \<Rightarrow> 'a" |
|
392 |
|
393 (*use "~~/src/HOL/Tools/numeral.ML" |
|
394 |
|
395 syntax |
|
396 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") |
|
397 |
|
398 use "~~/src/HOL/Tools/numeral_syntax.ML" |
|
399 |
|
400 setup NumeralSyntax.setup |
|
401 |
|
402 abbreviation |
|
403 "Numeral0 \<equiv> number_of Pls" |
|
404 |
|
405 abbreviation |
|
406 "Numeral1 \<equiv> number_of (Bit1 Pls)" |
|
407 |
|
408 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" |
|
409 -- {* Unfold all @{text let}s involving constants *} |
|
410 unfolding Let_def .. |
|
411 |
|
412 definition |
|
413 succ :: "int \<Rightarrow> int" where |
|
414 [code del]: "succ k = k + 1" |
|
415 |
|
416 definition |
|
417 pred :: "int \<Rightarrow> int" where |
|
418 [code del]: "pred k = k - 1" |
|
419 |
|
420 lemmas |
|
421 max_number_of [simp] = max_def |
|
422 [of "number_of u" "number_of v", standard, simp] |
|
423 and |
|
424 min_number_of [simp] = min_def |
|
425 [of "number_of u" "number_of v", standard, simp] |
|
426 -- {* unfolding @{text minx} and @{text max} on numerals *} |
|
427 |
|
428 lemmas numeral_simps = |
|
429 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def |
|
430 |
|
431 text {* Removal of leading zeroes *} |
|
432 |
|
433 lemma Bit0_Pls [simp, code_post]: |
|
434 "Bit0 Pls = Pls" |
|
435 unfolding numeral_simps by simp |
|
436 |
|
437 lemma Bit1_Min [simp, code_post]: |
|
438 "Bit1 Min = Min" |
|
439 unfolding numeral_simps by simp |
|
440 |
|
441 lemmas normalize_bin_simps = |
|
442 Bit0_Pls Bit1_Min |
|
443 *) |
|
444 |
|
445 end |