Int.thy: discontinued some legacy theorems
authorhuffman
Sun Oct 09 11:13:53 2011 +0200 (2011-10-09 ago)
changeset 4512249e305100097
parent 45121 5e495ccf6e56
child 45124 d78ec6c10fa1
Int.thy: discontinued some legacy theorems
NEWS
src/HOL/Int.thy
     1.1 --- a/NEWS	Sun Oct 09 08:30:48 2011 +0200
     1.2 +++ b/NEWS	Sun Oct 09 11:13:53 2011 +0200
     1.3 @@ -4,6 +4,45 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Theory Int: Discontinued many legacy theorems specific to type int.
    1.10 +  INCOMPATIBILITY, use the corresponding generic theorems instead.
    1.11 +
    1.12 +  zminus_zminus ~> minus_minus
    1.13 +  zminus_0 ~> minus_zero
    1.14 +  zminus_zadd_distrib ~> minus_add_distrib
    1.15 +  zadd_commute ~> add_commute
    1.16 +  zadd_assoc ~> add_assoc
    1.17 +  zadd_left_commute ~> add_left_commute
    1.18 +  zmult_ac ~> mult_ac
    1.19 +  zadd_0 ~> add_0_left
    1.20 +  zadd_0_right ~> add_0_right
    1.21 +  zadd_zminus_inverse2 ~> left_minus
    1.22 +  zmult_zminus ~> mult_minus_left
    1.23 +  zmult_commute ~> mult_commute
    1.24 +  zmult_assoc ~> mult_assoc
    1.25 +  zadd_zmult_distrib ~> left_distrib
    1.26 +  zadd_zmult_distrib2 ~> right_distrib
    1.27 +  zdiff_zmult_distrib ~> left_diff_distrib
    1.28 +  zdiff_zmult_distrib2 ~> right_diff_distrib
    1.29 +  zmult_1 ~> mult_1_left
    1.30 +  zmult_1_right ~> mult_1_right
    1.31 +  zle_refl ~> order_refl
    1.32 +  zle_trans ~> order_trans
    1.33 +  zle_antisym ~> order_antisym
    1.34 +  zle_linear ~> linorder_linear
    1.35 +  zless_linear ~> linorder_less_linear
    1.36 +  zadd_left_mono ~> add_left_mono
    1.37 +  zadd_strict_right_mono ~> add_strict_right_mono
    1.38 +  zadd_zless_mono ~> add_less_le_mono
    1.39 +  int_0_less_1 ~> zero_less_one
    1.40 +  int_0_neq_1 ~> zero_neq_one
    1.41 +  zless_le ~> less_le
    1.42 +  zpower_zadd_distrib ~> power_add
    1.43 +  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
    1.44 +  zero_le_zpower_abs ~> zero_le_power_abs
    1.45 +
    1.46  
    1.47  
    1.48  New in Isabelle2011-1 (October 2011)
     2.1 --- a/src/HOL/Int.thy	Sun Oct 09 08:30:48 2011 +0200
     2.2 +++ b/src/HOL/Int.thy	Sun Oct 09 11:13:53 2011 +0200
     2.3 @@ -2431,40 +2431,8 @@
     2.4  
     2.5  subsection {* Legacy theorems *}
     2.6  
     2.7 -lemmas zminus_zminus = minus_minus [of "z::int", standard]
     2.8 -lemmas zminus_0 = minus_zero [where 'a=int]
     2.9 -lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
    2.10 -lemmas zadd_commute = add_commute [of "z::int" "w", standard]
    2.11 -lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
    2.12 -lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
    2.13 -lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
    2.14 -lemmas zmult_ac = mult_ac
    2.15 -lemmas zadd_0 = add_0_left [of "z::int", standard]
    2.16 -lemmas zadd_0_right = add_0_right [of "z::int", standard]
    2.17 -lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
    2.18 -lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
    2.19 -lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
    2.20 -lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
    2.21 -lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
    2.22 -lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
    2.23 -lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
    2.24 -lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
    2.25 -
    2.26 -lemmas zmult_1 = mult_1_left [of "z::int", standard]
    2.27 -lemmas zmult_1_right = mult_1_right [of "z::int", standard]
    2.28 -
    2.29 -lemmas zle_refl = order_refl [of "w::int", standard]
    2.30 -lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
    2.31 -lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
    2.32 -lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
    2.33 -lemmas zless_linear = linorder_less_linear [where 'a = int]
    2.34 -
    2.35 -lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
    2.36 -lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
    2.37 -lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
    2.38 -
    2.39 -lemmas int_0_less_1 = zero_less_one [where 'a=int]
    2.40 -lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
    2.41 +(* used by Tools/Qelim/cooper.ML *)
    2.42 +lemmas zadd_ac = add_ac [where 'a=int]
    2.43  
    2.44  lemmas inj_int = inj_of_nat [where 'a=int]
    2.45  lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
    2.46 @@ -2482,19 +2450,6 @@
    2.47  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
    2.48  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
    2.49  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
    2.50 -lemmas zless_le = less_int_def
    2.51 -lemmas int_eq_of_nat = TrueI
    2.52 -
    2.53 -lemma zpower_zadd_distrib:
    2.54 -  "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
    2.55 -  by (rule power_add)
    2.56 -
    2.57 -lemma zero_less_zpower_abs_iff:
    2.58 -  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
    2.59 -  by (rule zero_less_power_abs_iff)
    2.60 -
    2.61 -lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
    2.62 -  by (rule zero_le_power_abs)
    2.63  
    2.64  lemma zpower_zpower:
    2.65    "(x ^ y) ^ z = (x ^ (y * z)::int)"