equal
deleted
inserted
replaced
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 :: linordered_ring |
|
333 proof |
|
334 (* fix k :: int |
|
335 show "abs k = sup k (- k)" |
|
336 by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*) |
|
337 qed |
|
338 |
|
339 lemmas int_distrib = |
332 lemmas int_distrib = |
340 left_distrib [of "z1::int" "z2" "w", standard] |
333 left_distrib [of "z1::int" "z2" "w", standard] |
341 right_distrib [of "w::int" "z1" "z2", standard] |
334 right_distrib [of "w::int" "z1" "z2", standard] |
342 left_diff_distrib [of "z1::int" "z2" "w", standard] |
335 left_diff_distrib [of "z1::int" "z2" "w", standard] |
343 right_diff_distrib [of "w::int" "z1" "z2", standard] |
336 right_diff_distrib [of "w::int" "z1" "z2", standard] |