|
1 (* Title: HOL/Quotient_Examples/Quotient_Int.thy |
|
2 Author: Cezary Kaliszyk |
|
3 Author: Christian Urban |
|
4 |
|
5 Integers based on Quotients. |
|
6 *) |
|
7 theory Quotient_Int |
|
8 imports Quotient_Product Nat |
|
9 begin |
|
10 |
|
11 fun |
|
12 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
|
13 where |
|
14 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
15 |
|
16 quotient_type int = "nat \<times> nat" / intrel |
|
17 by (auto simp add: equivp_def expand_fun_eq) |
|
18 |
|
19 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
|
20 begin |
|
21 |
|
22 quotient_definition |
|
23 "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" |
|
24 |
|
25 quotient_definition |
|
26 "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" |
|
27 |
|
28 fun |
|
29 plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
30 where |
|
31 "plus_int_raw (x, y) (u, v) = (x + u, y + v)" |
|
32 |
|
33 quotient_definition |
|
34 "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" |
|
35 |
|
36 fun |
|
37 uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
38 where |
|
39 "uminus_int_raw (x, y) = (y, x)" |
|
40 |
|
41 quotient_definition |
|
42 "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" |
|
43 |
|
44 definition |
|
45 minus_int_def [code del]: "z - w = z + (-w\<Colon>int)" |
|
46 |
|
47 fun |
|
48 times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
49 where |
|
50 "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
|
51 |
|
52 quotient_definition |
|
53 "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw" |
|
54 |
|
55 fun |
|
56 le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
57 where |
|
58 "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)" |
|
59 |
|
60 quotient_definition |
|
61 le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" |
|
62 |
|
63 definition |
|
64 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
|
65 |
|
66 definition |
|
67 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)" |
|
68 |
|
69 definition |
|
70 zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)" |
|
71 |
|
72 instance .. |
|
73 |
|
74 end |
|
75 |
|
76 lemma [quot_respect]: |
|
77 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw" |
|
78 and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw" |
|
79 and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw" |
|
80 by auto |
|
81 |
|
82 lemma times_int_raw_fst: |
|
83 assumes a: "x \<approx> z" |
|
84 shows "times_int_raw x y \<approx> times_int_raw z y" |
|
85 using a |
|
86 apply(cases x, cases y, cases z) |
|
87 apply(auto simp add: times_int_raw.simps intrel.simps) |
|
88 apply(rename_tac u v w x y z) |
|
89 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
90 apply(simp add: mult_ac) |
|
91 apply(simp add: add_mult_distrib [symmetric]) |
|
92 done |
|
93 |
|
94 lemma times_int_raw_snd: |
|
95 assumes a: "x \<approx> z" |
|
96 shows "times_int_raw y x \<approx> times_int_raw y z" |
|
97 using a |
|
98 apply(cases x, cases y, cases z) |
|
99 apply(auto simp add: times_int_raw.simps intrel.simps) |
|
100 apply(rename_tac u v w x y z) |
|
101 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
102 apply(simp add: mult_ac) |
|
103 apply(simp add: add_mult_distrib [symmetric]) |
|
104 done |
|
105 |
|
106 lemma [quot_respect]: |
|
107 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw" |
|
108 apply(simp only: fun_rel_def) |
|
109 apply(rule allI | rule impI)+ |
|
110 apply(rule equivp_transp[OF int_equivp]) |
|
111 apply(rule times_int_raw_fst) |
|
112 apply(assumption) |
|
113 apply(rule times_int_raw_snd) |
|
114 apply(assumption) |
|
115 done |
|
116 |
|
117 lemma plus_assoc_raw: |
|
118 shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)" |
|
119 by (cases i, cases j, cases k) (simp) |
|
120 |
|
121 lemma plus_sym_raw: |
|
122 shows "plus_int_raw i j \<approx> plus_int_raw j i" |
|
123 by (cases i, cases j) (simp) |
|
124 |
|
125 lemma plus_zero_raw: |
|
126 shows "plus_int_raw (0, 0) i \<approx> i" |
|
127 by (cases i) (simp) |
|
128 |
|
129 lemma plus_minus_zero_raw: |
|
130 shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)" |
|
131 by (cases i) (simp) |
|
132 |
|
133 lemma times_assoc_raw: |
|
134 shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)" |
|
135 by (cases i, cases j, cases k) |
|
136 (simp add: algebra_simps) |
|
137 |
|
138 lemma times_sym_raw: |
|
139 shows "times_int_raw i j \<approx> times_int_raw j i" |
|
140 by (cases i, cases j) (simp add: algebra_simps) |
|
141 |
|
142 lemma times_one_raw: |
|
143 shows "times_int_raw (1, 0) i \<approx> i" |
|
144 by (cases i) (simp) |
|
145 |
|
146 lemma times_plus_comm_raw: |
|
147 shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)" |
|
148 by (cases i, cases j, cases k) |
|
149 (simp add: algebra_simps) |
|
150 |
|
151 lemma one_zero_distinct: |
|
152 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
|
153 by simp |
|
154 |
|
155 text{* The integers form a @{text comm_ring_1}*} |
|
156 |
|
157 instance int :: comm_ring_1 |
|
158 proof |
|
159 fix i j k :: int |
|
160 show "(i + j) + k = i + (j + k)" |
|
161 by (lifting plus_assoc_raw) |
|
162 show "i + j = j + i" |
|
163 by (lifting plus_sym_raw) |
|
164 show "0 + i = (i::int)" |
|
165 by (lifting plus_zero_raw) |
|
166 show "- i + i = 0" |
|
167 by (lifting plus_minus_zero_raw) |
|
168 show "i - j = i + - j" |
|
169 by (simp add: minus_int_def) |
|
170 show "(i * j) * k = i * (j * k)" |
|
171 by (lifting times_assoc_raw) |
|
172 show "i * j = j * i" |
|
173 by (lifting times_sym_raw) |
|
174 show "1 * i = i" |
|
175 by (lifting times_one_raw) |
|
176 show "(i + j) * k = i * k + j * k" |
|
177 by (lifting times_plus_comm_raw) |
|
178 show "0 \<noteq> (1::int)" |
|
179 by (lifting one_zero_distinct) |
|
180 qed |
|
181 |
|
182 lemma plus_int_raw_rsp_aux: |
|
183 assumes a: "a \<approx> b" "c \<approx> d" |
|
184 shows "plus_int_raw a c \<approx> plus_int_raw b d" |
|
185 using a |
|
186 by (cases a, cases b, cases c, cases d) |
|
187 (simp) |
|
188 |
|
189 lemma add_abs_int: |
|
190 "(abs_int (x,y)) + (abs_int (u,v)) = |
|
191 (abs_int (x + u, y + v))" |
|
192 apply(simp add: plus_int_def id_simps) |
|
193 apply(fold plus_int_raw.simps) |
|
194 apply(rule Quotient_rel_abs[OF Quotient_int]) |
|
195 apply(rule plus_int_raw_rsp_aux) |
|
196 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
|
197 done |
|
198 |
|
199 definition int_of_nat_raw: |
|
200 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
|
201 |
|
202 quotient_definition |
|
203 "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" |
|
204 |
|
205 lemma[quot_respect]: |
|
206 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
|
207 by (simp add: equivp_reflp[OF int_equivp]) |
|
208 |
|
209 lemma int_of_nat: |
|
210 shows "of_nat m = int_of_nat m" |
|
211 by (induct m) |
|
212 (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int) |
|
213 |
|
214 lemma le_antisym_raw: |
|
215 shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j" |
|
216 by (cases i, cases j) (simp) |
|
217 |
|
218 lemma le_refl_raw: |
|
219 shows "le_int_raw i i" |
|
220 by (cases i) (simp) |
|
221 |
|
222 lemma le_trans_raw: |
|
223 shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k" |
|
224 by (cases i, cases j, cases k) (simp) |
|
225 |
|
226 lemma le_cases_raw: |
|
227 shows "le_int_raw i j \<or> le_int_raw j i" |
|
228 by (cases i, cases j) |
|
229 (simp add: linorder_linear) |
|
230 |
|
231 instance int :: linorder |
|
232 proof |
|
233 fix i j k :: int |
|
234 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
|
235 by (lifting le_antisym_raw) |
|
236 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
|
237 by (auto simp add: less_int_def dest: antisym) |
|
238 show "i \<le> i" |
|
239 by (lifting le_refl_raw) |
|
240 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
|
241 by (lifting le_trans_raw) |
|
242 show "i \<le> j \<or> j \<le> i" |
|
243 by (lifting le_cases_raw) |
|
244 qed |
|
245 |
|
246 instantiation int :: distrib_lattice |
|
247 begin |
|
248 |
|
249 definition |
|
250 "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min" |
|
251 |
|
252 definition |
|
253 "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max" |
|
254 |
|
255 instance |
|
256 by intro_classes |
|
257 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
|
258 |
|
259 end |
|
260 |
|
261 lemma le_plus_int_raw: |
|
262 shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)" |
|
263 by (cases i, cases j, cases k) (simp) |
|
264 |
|
265 instance int :: ordered_cancel_ab_semigroup_add |
|
266 proof |
|
267 fix i j k :: int |
|
268 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
|
269 by (lifting le_plus_int_raw) |
|
270 qed |
|
271 |
|
272 abbreviation |
|
273 "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)" |
|
274 |
|
275 lemma zmult_zless_mono2_lemma: |
|
276 fixes i j::int |
|
277 and k::nat |
|
278 shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j" |
|
279 apply(induct "k") |
|
280 apply(simp) |
|
281 apply(case_tac "k = 0") |
|
282 apply(simp_all add: left_distrib add_strict_mono) |
|
283 done |
|
284 |
|
285 lemma zero_le_imp_eq_int_raw: |
|
286 fixes k::"(nat \<times> nat)" |
|
287 shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
|
288 apply(cases k) |
|
289 apply(simp add:int_of_nat_raw) |
|
290 apply(auto) |
|
291 apply(rule_tac i="b" and j="a" in less_Suc_induct) |
|
292 apply(auto) |
|
293 done |
|
294 |
|
295 lemma zero_le_imp_eq_int: |
|
296 fixes k::int |
|
297 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
|
298 unfolding less_int_def int_of_nat |
|
299 by (lifting zero_le_imp_eq_int_raw) |
|
300 |
|
301 lemma zmult_zless_mono2: |
|
302 fixes i j k::int |
|
303 assumes a: "i < j" "0 < k" |
|
304 shows "k * i < k * j" |
|
305 using a |
|
306 by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma) |
|
307 |
|
308 text{*The integers form an ordered integral domain*} |
|
309 instance int :: linordered_idom |
|
310 proof |
|
311 fix i j k :: int |
|
312 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
|
313 by (rule zmult_zless_mono2) |
|
314 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
|
315 by (simp only: zabs_def) |
|
316 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
|
317 by (simp only: zsgn_def) |
|
318 qed |
|
319 |
|
320 lemmas int_distrib = |
|
321 left_distrib [of "z1::int" "z2" "w", standard] |
|
322 right_distrib [of "w::int" "z1" "z2", standard] |
|
323 left_diff_distrib [of "z1::int" "z2" "w", standard] |
|
324 right_diff_distrib [of "w::int" "z1" "z2", standard] |
|
325 minus_add_distrib[of "z1::int" "z2", standard] |
|
326 |
|
327 lemma int_induct_raw: |
|
328 assumes a: "P (0::nat, 0)" |
|
329 and b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))" |
|
330 and c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))" |
|
331 shows "P x" |
|
332 proof (cases x, clarify) |
|
333 fix a b |
|
334 show "P (a, b)" |
|
335 proof (induct a arbitrary: b rule: Nat.induct) |
|
336 case zero |
|
337 show "P (0, b)" using assms by (induct b) auto |
|
338 next |
|
339 case (Suc n) |
|
340 then show ?case using assms by auto |
|
341 qed |
|
342 qed |
|
343 |
|
344 lemma int_induct: |
|
345 fixes x :: int |
|
346 assumes a: "P 0" |
|
347 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
|
348 and c: "\<And>i. P i \<Longrightarrow> P (i - 1)" |
|
349 shows "P x" |
|
350 using a b c unfolding minus_int_def |
|
351 by (lifting int_induct_raw) |
|
352 |
|
353 text {* Magnitide of an Integer, as a Natural Number: @{term nat} *} |
|
354 |
|
355 definition |
|
356 "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)" |
|
357 |
|
358 quotient_definition |
|
359 "int_to_nat::int \<Rightarrow> nat" |
|
360 is |
|
361 "int_to_nat_raw" |
|
362 |
|
363 lemma [quot_respect]: |
|
364 shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw" |
|
365 by (auto iff: int_to_nat_raw_def) |
|
366 |
|
367 lemma nat_le_eq_zle_raw: |
|
368 assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z" |
|
369 shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)" |
|
370 using a |
|
371 by (cases w, cases z) (auto simp add: int_to_nat_raw_def) |
|
372 |
|
373 lemma nat_le_eq_zle: |
|
374 fixes w z::"int" |
|
375 shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)" |
|
376 unfolding less_int_def |
|
377 by (lifting nat_le_eq_zle_raw) |
|
378 |
|
379 end |