269 lemma le_plus_raw: |
269 lemma le_plus_raw: |
270 shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)" |
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) |
271 by (cases i, cases j, cases k) (simp) |
272 |
272 |
273 |
273 |
274 instance int :: pordered_cancel_ab_semigroup_add |
274 instance int :: ordered_cancel_ab_semigroup_add |
275 proof |
275 proof |
276 fix i j k :: int |
276 fix i j k :: int |
277 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
277 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
278 by (lifting le_plus_raw) |
278 by (lifting le_plus_raw) |
279 qed |
279 qed |
316 apply(drule_tac zero_le_imp_eq_int) |
316 apply(drule_tac zero_le_imp_eq_int) |
317 apply(auto simp add: zmult_zless_mono2_lemma) |
317 apply(auto simp add: zmult_zless_mono2_lemma) |
318 done |
318 done |
319 |
319 |
320 text{*The integers form an ordered integral domain*} |
320 text{*The integers form an ordered integral domain*} |
321 instance int :: ordered_idom |
321 instance int :: linordered_idom |
322 proof |
322 proof |
323 fix i j k :: int |
323 fix i j k :: int |
324 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
324 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
325 by (rule zmult_zless_mono2) |
325 by (rule zmult_zless_mono2) |
326 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
326 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
327 by (simp only: zabs_def) |
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)" |
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) |
329 by (simp only: zsgn_def) |
330 qed |
330 qed |
331 |
331 |
332 instance int :: lordered_ring |
332 instance int :: linordered_ring |
333 proof |
333 proof |
334 fix k :: int |
334 (* fix k :: int |
335 show "abs k = sup k (- k)" |
335 show "abs k = sup k (- k)" |
336 by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric]) |
336 by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*) |
337 qed |
337 qed |
338 |
338 |
339 lemmas int_distrib = |
339 lemmas int_distrib = |
340 left_distrib [of "z1::int" "z2" "w", standard] |
340 left_distrib [of "z1::int" "z2" "w", standard] |
341 right_distrib [of "w::int" "z1" "z2", standard] |
341 right_distrib [of "w::int" "z1" "z2", standard] |