equal
deleted
inserted
replaced
21 |
21 |
22 quotient_def |
22 quotient_def |
23 zero_int::"0 :: int" |
23 zero_int::"0 :: int" |
24 where |
24 where |
25 "(0::nat, 0::nat)" |
25 "(0::nat, 0::nat)" |
26 |
|
27 thm zero_int_def |
|
28 |
26 |
29 quotient_def |
27 quotient_def |
30 one_int::"1 :: int" |
28 one_int::"1 :: int" |
31 where |
29 where |
32 "(1::nat, 0::nat)" |
30 "(1::nat, 0::nat)" |
170 |
168 |
171 lemma one_zero_distinct: |
169 lemma one_zero_distinct: |
172 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
170 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
173 by simp |
171 by simp |
174 |
172 |
175 text{*The integers form a @{text comm_ring_1}*} |
173 text{* The integers form a @{text comm_ring_1}*} |
176 |
174 |
177 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
175 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
178 |
|
179 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
176 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
180 ML {* @{term "0 :: int"} *} |
177 ML {* @{term "0 :: int"} *} |
181 |
|
182 thm plus_assoc_raw |
|
183 |
178 |
184 instance int :: comm_ring_1 |
179 instance int :: comm_ring_1 |
185 proof |
180 proof |
186 fix i j k :: int |
181 fix i j k :: int |
187 show "(i + j) + k = i + (j + k)" |
182 show "(i + j) + k = i + (j + k)" |
204 by (lifting times_plus_comm_raw) |
199 by (lifting times_plus_comm_raw) |
205 show "0 \<noteq> (1::int)" |
200 show "0 \<noteq> (1::int)" |
206 by (lifting one_zero_distinct) |
201 by (lifting one_zero_distinct) |
207 qed |
202 qed |
208 |
203 |
209 term of_nat |
204 |
210 thm of_nat_def |
205 lemma add: |
|
206 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
|
207 (ABS_int (x+u, y+v))" |
|
208 apply(simp add: plus_int_def) |
|
209 sorry |
211 |
210 |
212 lemma int_def: "of_nat m = ABS_int (m, 0)" |
211 lemma int_def: "of_nat m = ABS_int (m, 0)" |
213 apply(induct m) |
212 apply(induct m) |
214 apply(simp add: zero_int_def) |
213 apply(simp add: zero_int_def) |
215 apply(simp) |
214 apply(simp add: one_int_def add) |
216 apply(simp add: plus_int_def one_int_def) |
215 done |
217 oops |
|
218 |
216 |
219 lemma le_antisym_raw: |
217 lemma le_antisym_raw: |
220 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
218 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
221 by (cases i, cases j) (simp) |
219 by (cases i, cases j) (simp) |
222 |
220 |
273 fix i j k :: int |
271 fix i j k :: int |
274 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
272 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
275 by (lifting le_plus_raw) |
273 by (lifting le_plus_raw) |
276 qed |
274 qed |
277 |
275 |
|
276 abbreviation |
|
277 "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)" |
|
278 |
|
279 |
278 lemma test: |
280 lemma test: |
279 "\<lbrakk>less_eq_raw i j \<and> \<not>i \<approx> j; less_eq_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
281 "\<lbrakk>less_raw i j; less_raw (0, 0) k\<rbrakk> |
280 \<Longrightarrow> less_eq_raw (times_raw k i) (times_raw k j) \<and> \<not>times_raw k i \<approx> times_raw k j" |
282 \<Longrightarrow> less_raw (times_raw k i) (times_raw k j)" |
281 apply(cases i, cases j, cases k) |
283 apply(cases i, cases j, cases k) |
282 apply(auto simp add: algebra_simps) |
284 apply(simp only: less_eq_raw.simps times_raw.simps) |
|
285 apply(simp) |
|
286 apply(rename_tac u v w x y z) |
|
287 apply(rule conjI) |
|
288 apply(subgoal_tac "y*u + y*x \<le> y*w + y*v & z*v \<le> y*v") |
|
289 apply(simp add: ) |
283 sorry |
290 sorry |
284 |
291 |
285 |
292 |
286 text{*The integers form an ordered integral domain*} |
293 text{*The integers form an ordered integral domain*} |
287 instance int :: ordered_idom |
294 instance int :: ordered_idom |