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