src/HOL/IntDef.thy
 changeset 23431 25ca91279a9b parent 23402 6472c689664f child 23438 dd824e86fa8a
```     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 20 05:06:56 2007 +0200
1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 20 05:18:39 2007 +0200
1.3 @@ -365,9 +365,6 @@
1.4  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
1.5  by simp
1.6
1.7 -lemma int_Suc: "int (Suc m) = 1 + (int m)"
1.8 -by simp
1.9 -
1.10  lemma int_Suc0_eq_1: "int (Suc 0) = 1"
1.11  by simp
1.12
1.13 @@ -506,7 +503,7 @@
1.14  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
1.15  apply (cases w, cases z)
1.16  apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
1.19  done
1.20
1.21  lemma of_int_le_iff [simp]:
1.22 @@ -645,7 +642,7 @@
1.23
1.24  lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
1.25    apply (cases "finite A")
1.26 -  apply (erule finite_induct, auto)
1.27 +  apply (erule finite_induct, auto simp add: of_nat_mult)
1.28    done
1.29
1.30  lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
1.31 @@ -712,41 +709,41 @@
1.32
1.33  subsection {* Legacy theorems *}
1.34
1.35 -lemmas zminus_zminus = minus_minus [where 'a=int]
1.36 +lemmas zminus_zminus = minus_minus [of "?z::int"]
1.37  lemmas zminus_0 = minus_zero [where 'a=int]
1.47  lemmas zmult_ac = OrderedGroup.mult_ac
1.50 -lemmas zadd_zminus_inverse2 = left_minus [where 'a=int]
1.51 -lemmas zmult_zminus = mult_minus_left [where 'a=int]
1.52 -lemmas zmult_commute = mult_commute [where 'a=int]
1.53 -lemmas zmult_assoc = mult_assoc [where 'a=int]
1.54 -lemmas zadd_zmult_distrib = left_distrib [where 'a=int]
1.55 -lemmas zadd_zmult_distrib2 = right_distrib [where 'a=int]
1.56 -lemmas zdiff_zmult_distrib = left_diff_distrib [where 'a=int]
1.57 -lemmas zdiff_zmult_distrib2 = right_diff_distrib [where 'a=int]
1.60 +lemmas zadd_zminus_inverse2 = left_minus [of "?z::int"]
1.61 +lemmas zmult_zminus = mult_minus_left [of "?z::int" "?w"]
1.62 +lemmas zmult_commute = mult_commute [of "?z::int" "?w"]
1.63 +lemmas zmult_assoc = mult_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
1.64 +lemmas zadd_zmult_distrib = left_distrib [of "?z1.0::int" "?z2.0" "?w"]
1.65 +lemmas zadd_zmult_distrib2 = right_distrib [of "?w::int" "?z1.0" "?z2.0"]
1.66 +lemmas zdiff_zmult_distrib = left_diff_distrib [of "?z1.0::int" "?z2.0" "?w"]
1.67 +lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "?w::int" "?z1.0" "?z2.0"]
1.68
1.69  lemmas int_distrib =
1.71    zdiff_zmult_distrib zdiff_zmult_distrib2
1.72
1.73 -lemmas zmult_1 = mult_1_left [where 'a=int]
1.74 -lemmas zmult_1_right = mult_1_right [where 'a=int]
1.75 +lemmas zmult_1 = mult_1_left [of "?z::int"]
1.76 +lemmas zmult_1_right = mult_1_right [of "?z::int"]
1.77
1.78 -lemmas zle_refl = order_refl [where 'a=int]
1.79 +lemmas zle_refl = order_refl [of "?w::int"]
1.80  lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
1.81 -lemmas zle_anti_sym = order_antisym [where 'a=int]
1.82 -lemmas zle_linear = linorder_linear [where 'a=int]
1.83 +lemmas zle_anti_sym = order_antisym [of "?z::int" "?w"]
1.84 +lemmas zle_linear = linorder_linear [of "?z::int" "?w"]
1.85  lemmas zless_linear = linorder_less_linear [where 'a = int]
1.86
1.93
1.94  lemmas int_0_less_1 = zero_less_one [where 'a=int]
1.95  lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
1.96 @@ -756,16 +753,17 @@
1.98  lemmas int_mult = of_nat_mult [where 'a=int]
1.99  lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
1.100 -lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
1.101 +lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="?n"]
1.102  lemmas zless_int = of_nat_less_iff [where 'a=int]
1.103 -lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
1.104 +lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="?k"]
1.105  lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
1.106  lemmas zle_int = of_nat_le_iff [where 'a=int]
1.107  lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1.108 -lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
1.109 +lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
1.110  lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
1.111  lemmas int_1 = of_nat_1 [where 'a=int]
1.112 -lemmas abs_int_eq = abs_of_nat [where 'a=int]
1.113 +lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
1.114 +lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
1.115  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1.116  lemmas int_setsum = of_nat_setsum [where 'a=int]
1.117  lemmas int_setprod = of_nat_setprod [where 'a=int]
```