18 done |
18 done |
19 |
19 |
20 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
20 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
21 begin |
21 begin |
22 |
22 |
23 quotient_def |
23 quotient_def |
24 zero_qnt::"int" |
24 zero_int::"0 :: int" |
25 where |
25 where |
26 "zero_qnt \<equiv> (0::nat, 0::nat)" |
26 "(0::nat, 0::nat)" |
27 |
27 |
28 definition Zero_int_def[code del]: |
28 thm zero_int_def |
29 "0 = zero_qnt" |
29 |
30 |
30 quotient_def |
31 quotient_def |
31 one_int::"1 :: int" |
32 one_qnt::"int" |
32 where |
33 where |
33 "(1::nat, 0::nat)" |
34 "one_qnt \<equiv> (1::nat, 0::nat)" |
|
35 |
|
36 definition One_int_def[code del]: |
|
37 "1 = one_qnt" |
|
38 |
34 |
39 fun |
35 fun |
40 plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
36 plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
41 where |
37 where |
42 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
38 "plus_raw (x, y) (u, v) = (x + u, y + v)" |
43 |
39 |
44 quotient_def |
40 quotient_def |
45 plus_qnt::"int \<Rightarrow> int \<Rightarrow> int" |
41 plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" |
46 where |
42 where |
47 "plus_qnt \<equiv> plus_raw" |
43 "plus_raw" |
48 |
|
49 definition add_int_def[code del]: |
|
50 "z + w = plus_qnt z w" |
|
51 |
44 |
52 fun |
45 fun |
53 minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
46 minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
54 where |
47 where |
55 "minus_raw (x, y) = (y, x)" |
48 "minus_raw (x, y) = (y, x)" |
56 |
49 |
57 quotient_def |
50 quotient_def |
58 minus_qnt::"int \<Rightarrow> int" |
51 uminus_int::"(uminus :: (int \<Rightarrow> int))" |
59 where |
52 where |
60 "minus_qnt \<equiv> minus_raw" |
53 "minus_raw" |
61 |
54 |
62 definition minus_int_def [code del]: |
55 definition |
63 "- z = minus_qnt z" |
56 minus_int_def [code del]: "z - w = z + (-w::int)" |
64 |
57 |
65 definition |
58 fun |
66 diff_int_def [code del]: "z - w = z + (-w::int)" |
59 times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
67 |
60 where |
68 fun |
61 "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
69 mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
62 |
70 where |
63 quotient_def |
71 "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
64 times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" |
72 |
65 where |
73 quotient_def |
66 "times_raw" |
74 mult_qnt::"int \<Rightarrow> int \<Rightarrow> int" |
67 |
75 where |
68 fun |
76 "mult_qnt \<equiv> mult_raw" |
69 less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
77 |
70 where |
78 definition |
71 "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)" |
79 mult_int_def [code del]: "z * w = mult_qnt z w" |
72 |
80 |
73 quotient_def |
81 fun |
74 less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" |
82 le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
75 where |
83 where |
76 "less_eq_raw" |
84 "le_raw (x, y) (u, v) = (x+v \<le> u+y)" |
|
85 |
|
86 quotient_def |
|
87 le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool" |
|
88 where |
|
89 "le_qnt \<equiv> le_raw" |
|
90 |
|
91 definition |
|
92 le_int_def [code del]: |
|
93 "z \<le> w = le_qnt z w" |
|
94 |
77 |
95 definition |
78 definition |
96 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
79 less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)" |
97 |
80 |
98 definition |
81 definition |
99 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)" |
82 abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)" |
100 |
83 |
101 definition |
84 |
102 zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
85 definition |
|
86 sgn_int_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
103 |
87 |
104 instance .. |
88 instance .. |
105 |
89 |
106 end |
90 end |
107 |
91 |
137 |
121 |
138 lemma plus_minus_zero_raw: |
122 lemma plus_minus_zero_raw: |
139 shows "plus_raw (minus_raw i) i \<approx> (0, 0)" |
123 shows "plus_raw (minus_raw i) i \<approx> (0, 0)" |
140 by (cases i) (simp) |
124 by (cases i) (simp) |
141 |
125 |
142 lemma mult_assoc_raw: |
126 lemma times_assoc_raw: |
143 shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)" |
127 shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)" |
144 by (cases i, cases j, cases k) |
128 by (cases i, cases j, cases k) |
145 (simp add: algebra_simps) |
129 (simp add: algebra_simps) |
146 |
130 |
147 lemma mult_sym_raw: |
131 lemma times_sym_raw: |
148 shows "mult_raw i j \<approx> mult_raw j i" |
132 shows "times_raw i j \<approx> times_raw j i" |
149 by (cases i, cases j) (simp add: algebra_simps) |
133 by (cases i, cases j) (simp add: algebra_simps) |
150 |
134 |
151 lemma mult_one_raw: |
135 lemma times_one_raw: |
152 shows "mult_raw (1, 0) i \<approx> i" |
136 shows "times_raw (1, 0) i \<approx> i" |
153 by (cases i) (simp) |
137 by (cases i) (simp) |
154 |
138 |
155 lemma mult_plus_comm_raw: |
139 lemma times_plus_comm_raw: |
156 shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)" |
140 shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)" |
157 by (cases i, cases j, cases k) |
141 by (cases i, cases j, cases k) |
158 (simp add: algebra_simps) |
142 (simp add: algebra_simps) |
159 |
143 |
160 lemma one_zero_distinct: |
144 lemma one_zero_distinct: |
161 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
145 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
162 by simp |
146 by simp |
163 |
147 |
164 text{*The integers form a @{text comm_ring_1}*} |
148 text{*The integers form a @{text comm_ring_1}*} |
165 |
149 |
|
150 print_quotconsts |
|
151 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
|
152 |
|
153 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
|
154 ML {* @{term "0 :: int"} *} |
|
155 |
|
156 thm plus_assoc_raw |
166 |
157 |
167 instance int :: comm_ring_1 |
158 instance int :: comm_ring_1 |
168 proof |
159 proof |
169 fix i j k :: int |
160 fix i j k :: int |
170 show "(i + j) + k = i + (j + k)" |
161 show "(i + j) + k = i + (j + k)" |
171 unfolding add_int_def |
162 by (lifting plus_assoc_raw) |
172 by (lifting plus_assoc_raw) |
|
173 show "i + j = j + i" |
163 show "i + j = j + i" |
174 unfolding add_int_def |
|
175 by (lifting plus_sym_raw) |
164 by (lifting plus_sym_raw) |
176 show "0 + i = (i::int)" |
165 show "0 + i = (i::int)" |
177 unfolding add_int_def Zero_int_def |
|
178 by (lifting plus_zero_raw) |
166 by (lifting plus_zero_raw) |
179 show "- i + i = 0" |
167 show "- i + i = 0" |
180 unfolding add_int_def minus_int_def Zero_int_def |
|
181 by (lifting plus_minus_zero_raw) |
168 by (lifting plus_minus_zero_raw) |
182 show "i - j = i + - j" |
169 show "i - j = i + - j" |
183 by (simp add: diff_int_def) |
170 by (simp add: minus_int_def) |
184 show "(i * j) * k = i * (j * k)" |
171 show "(i * j) * k = i * (j * k)" |
185 unfolding mult_int_def |
172 by (lifting times_assoc_raw) |
186 by (lifting mult_assoc_raw) |
|
187 show "i * j = j * i" |
173 show "i * j = j * i" |
188 unfolding mult_int_def |
174 by (lifting times_sym_raw) |
189 by (lifting mult_sym_raw) |
|
190 show "1 * i = i" |
175 show "1 * i = i" |
191 unfolding mult_int_def One_int_def |
176 by (lifting times_one_raw) |
192 by (lifting mult_one_raw) |
|
193 show "(i + j) * k = i * k + j * k" |
177 show "(i + j) * k = i * k + j * k" |
194 unfolding mult_int_def add_int_def |
178 by (lifting times_plus_comm_raw) |
195 by (lifting mult_plus_comm_raw) |
|
196 show "0 \<noteq> (1::int)" |
179 show "0 \<noteq> (1::int)" |
197 unfolding Zero_int_def One_int_def |
|
198 by (lifting one_zero_distinct) |
180 by (lifting one_zero_distinct) |
199 qed |
181 qed |
200 |
182 |
201 term of_nat |
183 term of_nat |
202 thm of_nat_def |
184 thm of_nat_def |
203 |
185 |
204 lemma int_def: "of_nat m = ABS_int (m, 0)" |
186 lemma int_def: "of_nat m = ABS_int (m, 0)" |
205 apply(induct m) |
187 apply(induct m) |
206 apply(simp add: Zero_int_def zero_qnt_def) |
188 apply(simp add: zero_int_def) |
207 apply(simp) |
189 apply(simp) |
208 apply(simp add: add_int_def One_int_def) |
190 apply(simp add: plus_int_def one_int_def) |
209 apply(simp add: plus_qnt_def one_qnt_def) |
|
210 oops |
191 oops |
211 |
192 |
212 lemma le_antisym_raw: |
193 lemma le_antisym_raw: |
213 shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j" |
194 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
214 by (cases i, cases j) (simp) |
195 by (cases i, cases j) (simp) |
215 |
196 |
216 lemma le_refl_raw: |
197 lemma le_refl_raw: |
217 shows "le_raw i i" |
198 shows "less_eq_raw i i" |
218 by (cases i) (simp) |
199 by (cases i) (simp) |
219 |
200 |
220 lemma le_trans_raw: |
201 lemma le_trans_raw: |
221 shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k" |
202 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k" |
222 by (cases i, cases j, cases k) (simp) |
203 by (cases i, cases j, cases k) (simp) |
223 |
204 |
224 lemma le_cases_raw: |
205 lemma le_cases_raw: |
225 shows "le_raw i j \<or> le_raw j i" |
206 shows "less_eq_raw i j \<or> less_eq_raw j i" |
226 by (cases i, cases j) |
207 by (cases i, cases j) |
227 (simp add: linorder_linear) |
208 (simp add: linorder_linear) |
228 |
209 |
229 instance int :: linorder |
210 instance int :: linorder |
230 proof |
211 proof |
231 fix i j k :: int |
212 fix i j k :: int |
232 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
213 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
233 unfolding le_int_def |
|
234 by (lifting le_antisym_raw) |
214 by (lifting le_antisym_raw) |
235 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
215 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
236 by (auto simp add: less_int_def dest: antisym) |
216 by (auto simp add: less_int_def dest: antisym) |
237 show "i \<le> i" |
217 show "i \<le> i" |
238 unfolding le_int_def |
|
239 by (lifting le_refl_raw) |
218 by (lifting le_refl_raw) |
240 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
219 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
241 unfolding le_int_def |
|
242 by (lifting le_trans_raw) |
220 by (lifting le_trans_raw) |
243 show "i \<le> j \<or> j \<le> i" |
221 show "i \<le> j \<or> j \<le> i" |
244 unfolding le_int_def |
|
245 by (lifting le_cases_raw) |
222 by (lifting le_cases_raw) |
246 qed |
223 qed |
247 |
224 |
248 instantiation int :: distrib_lattice |
225 instantiation int :: distrib_lattice |
249 begin |
226 begin |
259 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
236 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) |
260 |
237 |
261 end |
238 end |
262 |
239 |
263 lemma le_plus_raw: |
240 lemma le_plus_raw: |
264 shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)" |
241 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)" |
265 by (cases i, cases j, cases k) (simp) |
242 by (cases i, cases j, cases k) (simp) |
266 |
243 |
267 |
244 |
268 instance int :: pordered_cancel_ab_semigroup_add |
245 instance int :: pordered_cancel_ab_semigroup_add |
269 proof |
246 proof |
270 fix i j k :: int |
247 fix i j k :: int |
271 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
248 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
272 unfolding le_int_def add_int_def |
|
273 by (lifting le_plus_raw) |
249 by (lifting le_plus_raw) |
274 qed |
250 qed |
275 |
251 |
276 lemma test: |
252 lemma test: |
277 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
253 "\<lbrakk>less_eq_raw i j \<and> \<not>i \<approx> j; less_eq_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
278 \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j" |
254 \<Longrightarrow> less_eq_raw (times_raw k i) (times_raw k j) \<and> \<not>times_raw k i \<approx> times_raw k j" |
279 apply(cases i, cases j, cases k) |
255 apply(cases i, cases j, cases k) |
280 apply(auto simp add: algebra_simps) |
256 apply(auto simp add: algebra_simps) |
281 sorry |
257 sorry |
282 |
258 |
283 |
259 |
284 text{*The integers form an ordered integral domain*} |
260 text{*The integers form an ordered integral domain*} |
285 instance int :: ordered_idom |
261 instance int :: ordered_idom |
286 proof |
262 proof |
287 fix i j k :: int |
263 fix i j k :: int |
288 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
264 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
289 unfolding mult_int_def le_int_def less_int_def Zero_int_def |
265 unfolding less_int_def |
290 by (lifting test) |
266 by (lifting test) |
291 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
267 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
292 by (simp only: zabs_def) |
268 by (simp only: abs_int_def) |
293 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
269 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
294 by (simp only: zsgn_def) |
270 by (simp only: sgn_int_def) |
295 qed |
271 qed |
296 |
272 |
297 instance int :: lordered_ring |
273 instance int :: lordered_ring |
298 proof |
274 proof |
299 fix k :: int |
275 fix k :: int |
300 show "abs k = sup k (- k)" |
276 show "abs k = sup k (- k)" |
301 by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric]) |
277 by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric]) |
302 qed |
278 qed |
303 |
279 |
304 lemmas int_distrib = |
280 lemmas int_distrib = |
305 left_distrib [of "z1::int" "z2" "w", standard] |
281 left_distrib [of "z1::int" "z2" "w", standard] |
306 right_distrib [of "w::int" "z1" "z2", standard] |
282 right_distrib [of "w::int" "z1" "z2", standard] |