dropped various legacy fact bindings
authorhaftmann
Wed Feb 17 21:51:57 2016 +0100 (2016-02-17)
changeset 623489a5f43dac883
parent 62347 2230b7047376
child 62349 7c23469b5118
dropped various legacy fact bindings
NEWS
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Archimedean_Field.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Inequalities.thy
src/HOL/Int.thy
src/HOL/Isar_Examples/Fibonacci.thy
src/HOL/Library/Float.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Matrix_LP/ComputeNumeral.thy
src/HOL/Nat_Transfer.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Presburger.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Word/Word.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Sqrt.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -37,9 +37,72 @@
     1.4  
     1.5  * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
     1.6  
     1.7 -* Lemma generalization:
     1.8 -    realpow_minus_mult ~> power_minus_mult
     1.9 -    realpow_Suc_le_self ~> power_Suc_le_self
    1.10 +* Dropped various legacy fact bindings, whose replacements are often
    1.11 +of a more general type also:
    1.12 +  lcm_left_commute_nat ~> lcm.left_commute
    1.13 +  lcm_left_commute_int ~> lcm.left_commute
    1.14 +  gcd_left_commute_nat ~> gcd.left_commute
    1.15 +  gcd_left_commute_int ~> gcd.left_commute
    1.16 +  gcd_greatest_iff_nat ~> gcd_greatest_iff
    1.17 +  gcd_greatest_iff_int ~> gcd_greatest_iff
    1.18 +  coprime_dvd_mult_nat ~> coprime_dvd_mult
    1.19 +  coprime_dvd_mult_int ~> coprime_dvd_mult
    1.20 +  zpower_numeral_even ~> power_numeral_even
    1.21 +  gcd_mult_cancel_nat ~> gcd_mult_cancel
    1.22 +  gcd_mult_cancel_int ~> gcd_mult_cancel
    1.23 +  div_gcd_coprime_nat ~> div_gcd_coprime
    1.24 +  div_gcd_coprime_int ~> div_gcd_coprime
    1.25 +  zpower_numeral_odd ~> power_numeral_odd
    1.26 +  zero_less_int_conv ~> of_nat_0_less_iff
    1.27 +  gcd_greatest_nat ~> gcd_greatest
    1.28 +  gcd_greatest_int ~> gcd_greatest
    1.29 +  coprime_mult_nat ~> coprime_mult
    1.30 +  coprime_mult_int ~> coprime_mult
    1.31 +  lcm_commute_nat ~> lcm.commute
    1.32 +  lcm_commute_int ~> lcm.commute
    1.33 +  int_less_0_conv ~> of_nat_less_0_iff
    1.34 +  gcd_commute_nat ~> gcd.commute
    1.35 +  gcd_commute_int ~> gcd.commute
    1.36 +  Gcd_insert_nat ~> Gcd_insert
    1.37 +  Gcd_insert_int ~> Gcd_insert
    1.38 +  of_int_int_eq ~> of_int_of_nat_eq
    1.39 +  lcm_least_nat ~> lcm_least
    1.40 +  lcm_least_int ~> lcm_least
    1.41 +  lcm_assoc_nat ~> lcm.assoc
    1.42 +  lcm_assoc_int ~> lcm.assoc
    1.43 +  int_le_0_conv ~> of_nat_le_0_iff
    1.44 +  int_eq_0_conv ~> of_nat_eq_0_iff
    1.45 +  Gcd_empty_nat ~> Gcd_empty
    1.46 +  Gcd_empty_int ~> Gcd_empty
    1.47 +  gcd_assoc_nat ~> gcd.assoc
    1.48 +  gcd_assoc_int ~> gcd.assoc
    1.49 +  zero_zle_int ~> of_nat_0_le_iff
    1.50 +  lcm_dvd2_nat ~> dvd_lcm2
    1.51 +  lcm_dvd2_int ~> dvd_lcm2
    1.52 +  lcm_dvd1_nat ~> dvd_lcm1
    1.53 +  lcm_dvd1_int ~> dvd_lcm1
    1.54 +  gcd_zero_nat ~> gcd_eq_0_iff
    1.55 +  gcd_zero_int ~> gcd_eq_0_iff
    1.56 +  gcd_dvd2_nat ~> gcd_dvd2
    1.57 +  gcd_dvd2_int ~> gcd_dvd2
    1.58 +  gcd_dvd1_nat ~> gcd_dvd1
    1.59 +  gcd_dvd1_int ~> gcd_dvd1
    1.60 +  int_numeral ~> of_nat_numeral
    1.61 +  lcm_ac_nat ~> ac_simps
    1.62 +  lcm_ac_int ~> ac_simps
    1.63 +  gcd_ac_nat ~> ac_simps
    1.64 +  gcd_ac_int ~> ac_simps
    1.65 +  abs_int_eq ~> abs_of_nat
    1.66 +  zless_int ~> of_nat_less_iff
    1.67 +  zdiff_int ~> of_nat_diff
    1.68 +  zadd_int ~> of_nat_add
    1.69 +  int_mult ~> of_nat_mult
    1.70 +  int_Suc ~> of_nat_Suc
    1.71 +  inj_int ~> inj_of_nat
    1.72 +  int_1 ~> of_nat_1
    1.73 +  int_0 ~> of_nat_0
    1.74 +  realpow_minus_mult ~> power_minus_mult
    1.75 +  realpow_Suc_le_self ~> power_Suc_le_self
    1.76  INCOMPATIBILITY.
    1.77  
    1.78  
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
     2.3 @@ -201,7 +201,7 @@
     2.4  apply (drule less_imp_le [of a])
     2.5  apply (drule le_imp_power_dvd)
     2.6  apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
     2.7 -apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2_nat gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10))
     2.8 +apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10))
     2.9  done
    2.10  
    2.11  lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
     3.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Feb 17 21:51:57 2016 +0100
     3.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Feb 17 21:51:57 2016 +0100
     3.3 @@ -251,7 +251,7 @@
     3.4    then obtain x where "1 = x * int p" by best
     3.5    then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
     3.6    then show False
     3.7 -    by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
     3.8 +    by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
     3.9  qed
    3.10  
    3.11  
     4.1 --- a/src/HOL/Archimedean_Field.thy	Wed Feb 17 21:51:57 2016 +0100
     4.2 +++ b/src/HOL/Archimedean_Field.thy	Wed Feb 17 21:51:57 2016 +0100
     4.3 @@ -575,11 +575,10 @@
     4.4  
     4.5  lemma frac_unique_iff:
     4.6    fixes x :: "'a::floor_ceiling"
     4.7 -  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
     4.8 -  apply (auto simp: Ints_def frac_def)
     4.9 -  apply linarith
    4.10 -  apply linarith
    4.11 -  by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
    4.12 +  shows  "frac x = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
    4.13 +  apply (auto simp: Ints_def frac_def algebra_simps floor_unique)
    4.14 +  apply linarith+
    4.15 +  done
    4.16  
    4.17  lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
    4.18    by (simp add: frac_unique_iff)
     5.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Wed Feb 17 21:51:57 2016 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Wed Feb 17 21:51:57 2016 +0100
     5.3 @@ -27,7 +27,7 @@
     5.4        (let g = gcd a b
     5.5         in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
     5.6  
     5.7 -declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
     5.8 +declare gcd_dvd1[presburger] gcd_dvd2[presburger]
     5.9  
    5.10  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    5.11  proof -
    5.12 @@ -51,7 +51,7 @@
    5.13      from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
    5.14      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    5.15      from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    5.16 -    from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    5.17 +    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
    5.18      from ab consider "b < 0" | "b > 0" by arith
    5.19      then show ?thesis
    5.20      proof cases
    5.21 @@ -142,7 +142,7 @@
    5.22  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    5.23    apply (simp add: Ninv_def isnormNum_def split_def)
    5.24    apply (cases "fst x = 0")
    5.25 -  apply (auto simp add: gcd_commute_int)
    5.26 +  apply (auto simp add: gcd.commute)
    5.27    done
    5.28  
    5.29  lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
    5.30 @@ -197,7 +197,7 @@
    5.31        by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    5.32      from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
    5.33      have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
    5.34 -      by (simp_all add: x y isnormNum_def add: gcd_commute_int)
    5.35 +      by (simp_all add: x y isnormNum_def add: gcd.commute)
    5.36      from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
    5.37        apply -
    5.38        apply algebra
    5.39 @@ -205,8 +205,8 @@
    5.40        apply simp
    5.41        apply algebra
    5.42        done
    5.43 -    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    5.44 -        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
    5.45 +    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
    5.46 +        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
    5.47        have eq1: "b = b'" using pos by arith
    5.48        with eq have "a = a'" using pos by simp
    5.49        with eq1 show ?thesis by (simp add: x y)
    5.50 @@ -551,7 +551,7 @@
    5.51  qed
    5.52  
    5.53  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
    5.54 -  by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute)
    5.55 +  by (simp add: Nmul_def split_def Let_def gcd.commute mult.commute)
    5.56  
    5.57  lemma Nmul_assoc:
    5.58    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
     6.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Feb 17 21:51:57 2016 +0100
     6.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Feb 17 21:51:57 2016 +0100
     6.3 @@ -62,13 +62,14 @@
     6.4      val simpset1 =
     6.5        put_simpset HOL_basic_ss ctxt
     6.6        addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
     6.7 -        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int}
     6.8 +        map (fn r => r RS sym) @{thms of_nat_numeral [where ?'a = int] int_int_eq zle_int of_nat_less_iff [where ?'a = int]}
     6.9        |> Splitter.add_split @{thm zdiff_int_split}
    6.10      (*simp rules for elimination of int n*)
    6.11  
    6.12      val simpset2 =
    6.13        put_simpset HOL_basic_ss ctxt
    6.14 -      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}]
    6.15 +      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *),
    6.16 +        @{thm of_nat_0 [where ?'a = int]}, @{thm of_nat_1  [where ?'a = int]}]
    6.17        |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    6.18      (* simp rules for elimination of abs *)
    6.19      val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
     7.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Feb 17 21:51:57 2016 +0100
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Feb 17 21:51:57 2016 +0100
     7.3 @@ -88,13 +88,13 @@
     7.4      (* Simp rules for changing (n::int) to int n *)
     7.5      val simpset1 = put_simpset HOL_basic_ss ctxt
     7.6        addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ 
     7.7 -          map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm nat_numeral}]
     7.8 +          map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
     7.9        |> Splitter.add_split @{thm "zdiff_int_split"}
    7.10      (*simp rules for elimination of int n*)
    7.11  
    7.12      val simpset2 = put_simpset HOL_basic_ss ctxt
    7.13        addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, 
    7.14 -                @{thm "int_0"}, @{thm "int_1"}]
    7.15 +                @{thm "of_nat_0"}, @{thm "of_nat_1"}]
    7.16        |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    7.17      (* simp rules for elimination of abs *)
    7.18      val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
     8.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     8.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     8.3 @@ -1736,7 +1736,7 @@
     8.4  
     8.5  lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
     8.6    unfolding lcm_int_def gcd_int_def
     8.7 -  apply (subst int_mult [symmetric])
     8.8 +  apply (subst of_nat_mult [symmetric])
     8.9    apply (subst prod_gcd_lcm_nat [symmetric])
    8.10    apply (subst nat_abs_mult_distrib [symmetric])
    8.11    apply (simp, simp add: abs_mult)
    8.12 @@ -2057,42 +2057,6 @@
    8.13  
    8.14  text \<open>Fact aliasses\<close>
    8.15  
    8.16 -lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
    8.17 -lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
    8.18 -lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
    8.19 -lemmas gcd_commute_int = gcd.commute [where ?'a = int]
    8.20 -lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
    8.21 -lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
    8.22 -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    8.23 -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    8.24 -lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
    8.25 -lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
    8.26 -lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
    8.27 -lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
    8.28 -lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
    8.29 -lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
    8.30 -lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
    8.31 -lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
    8.32 -lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
    8.33 -lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
    8.34 -lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
    8.35 -lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
    8.36 -
    8.37 -lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
    8.38 -lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
    8.39 -lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
    8.40 -lemmas lcm_commute_int = lcm.commute [where ?'a = int]
    8.41 -lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
    8.42 -lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
    8.43 -lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
    8.44 -lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
    8.45 -lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
    8.46 -lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
    8.47 -lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
    8.48 -lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
    8.49 -lemmas lcm_least_nat = lcm_least [where ?'a = nat]
    8.50 -lemmas lcm_least_int = lcm_least [where ?'a = int]
    8.51 -
    8.52  lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
    8.53    by (fact lcm_eq_0_iff)
    8.54  
    8.55 @@ -2111,13 +2075,6 @@
    8.56  lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
    8.57    by (fact dvd_lcmI2)
    8.58  
    8.59 -lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
    8.60 -lemmas coprime_mult_int = coprime_mult [where ?'a = int]
    8.61 -lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
    8.62 -lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
    8.63 -lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
    8.64 -lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
    8.65 -
    8.66  lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
    8.67      (k dvd m * n) = (k dvd m)"
    8.68    by (fact coprime_dvd_mult_iff)
    8.69 @@ -2136,10 +2093,6 @@
    8.70  lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
    8.71  lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
    8.72  lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
    8.73 -lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
    8.74 -lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
    8.75 -lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
    8.76 -lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
    8.77  
    8.78  lemma dvd_Lcm_int [simp]:
    8.79    fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
     9.1 --- a/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
     9.2 +++ b/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
     9.3 @@ -999,14 +999,17 @@
     9.4  apply (simp add: algebra_simps)
     9.5  done
     9.6  
     9.7 -lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
     9.8 -by (simp add: less_diff_eq)
     9.9 +lemma diff_gt_0_iff_gt [simp]:
    9.10 +  "a - b > 0 \<longleftrightarrow> a > b"
    9.11 +  by (simp add: less_diff_eq)
    9.12  
    9.13 -lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    9.14 -by (auto simp add: le_less diff_less_eq )
    9.15 +lemma diff_le_eq [algebra_simps, field_simps]:
    9.16 +  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    9.17 +  by (auto simp add: le_less diff_less_eq )
    9.18  
    9.19 -lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    9.20 -by (auto simp add: le_less less_diff_eq)
    9.21 +lemma le_diff_eq [algebra_simps, field_simps]:
    9.22 +  "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    9.23 +  by (auto simp add: le_less less_diff_eq)
    9.24  
    9.25  lemma diff_le_0_iff_le [simp]:
    9.26    "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
    9.27 @@ -1014,6 +1017,10 @@
    9.28  
    9.29  lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
    9.30  
    9.31 +lemma diff_ge_0_iff_ge [simp]:
    9.32 +  "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
    9.33 +  by (simp add: le_diff_eq)
    9.34 +
    9.35  lemma diff_eq_diff_less:
    9.36    "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
    9.37    by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
    10.1 --- a/src/HOL/Inequalities.thy	Wed Feb 17 21:51:57 2016 +0100
    10.2 +++ b/src/HOL/Inequalities.thy	Wed Feb 17 21:51:57 2016 +0100
    10.3 @@ -31,7 +31,7 @@
    10.4    have "m*(m-1) \<le> n*(n + 1)"
    10.5     using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    10.6    hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    10.7 -    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
    10.8 +    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_setsum
    10.9            split: zdiff_int_split)
   10.10    thus ?thesis
   10.11      using of_nat_eq_iff by blast
   10.12 @@ -64,7 +64,7 @@
   10.13    { fix i j::nat assume "i<n" "j<n"
   10.14      hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"
   10.15        using assms by (cases "i \<le> j") (auto simp: algebra_simps)
   10.16 -  } hence "?S \<le> 0"
   10.17 +  } then have "?S \<le> 0"
   10.18      by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
   10.19    finally show ?thesis by (simp add: algebra_simps)
   10.20  qed
    11.1 --- a/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
    11.2 +++ b/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
    11.3 @@ -570,15 +570,19 @@
    11.4  lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
    11.5  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
    11.6  
    11.7 -lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
    11.8 -proof -
    11.9 -  have "(w \<le> z) = (0 \<le> z - w)"
   11.10 -    by (simp only: le_diff_eq add_0_left)
   11.11 -  also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   11.12 -    by (auto elim: zero_le_imp_eq_int)
   11.13 -  also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   11.14 -    by (simp only: algebra_simps)
   11.15 -  finally show ?thesis .
   11.16 +lemma zle_iff_zadd:
   11.17 +  "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" (is "?P \<longleftrightarrow> ?Q")
   11.18 +proof
   11.19 +  assume ?Q
   11.20 +  then show ?P by auto
   11.21 +next
   11.22 +  assume ?P
   11.23 +  then have "0 \<le> z - w" by simp
   11.24 +  then obtain n where "z - w = int n"
   11.25 +    using zero_le_imp_eq_int [of "z - w"] by blast
   11.26 +  then have "z = w + int n"
   11.27 +    by simp
   11.28 +  then show ?Q ..
   11.29  qed
   11.30  
   11.31  lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   11.32 @@ -1725,34 +1729,9 @@
   11.33  hide_const (open) Pos Neg sub dup
   11.34  
   11.35  
   11.36 -subsection \<open>Legacy theorems\<close>
   11.37 -
   11.38 -lemmas inj_int = inj_of_nat [where 'a=int]
   11.39 -lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   11.40 -lemmas int_mult = of_nat_mult [where 'a=int]
   11.41 -lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
   11.42 -lemmas zless_int = of_nat_less_iff [where 'a=int]
   11.43 -lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
   11.44 -lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   11.45 -lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   11.46 -lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
   11.47 -lemmas int_0 = of_nat_0 [where 'a=int]
   11.48 -lemmas int_1 = of_nat_1 [where 'a=int]
   11.49 -lemmas int_Suc = of_nat_Suc [where 'a=int]
   11.50 -lemmas int_numeral = of_nat_numeral [where 'a=int]
   11.51 -lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
   11.52 -lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   11.53 -lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   11.54 -lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
   11.55 -lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
   11.56 -
   11.57  text \<open>De-register \<open>int\<close> as a quotient type:\<close>
   11.58  
   11.59  lifting_update int.lifting
   11.60  lifting_forget int.lifting
   11.61  
   11.62 -text\<open>Also the class for fields with characteristic zero.\<close>
   11.63 -class field_char_0 = field + ring_char_0
   11.64 -subclass (in linordered_field) field_char_0 ..
   11.65 -
   11.66  end
    12.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy	Wed Feb 17 21:51:57 2016 +0100
    12.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy	Wed Feb 17 21:51:57 2016 +0100
    12.3 @@ -82,7 +82,7 @@
    12.4    also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
    12.5      by (rule gcd_add2_nat)
    12.6    also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
    12.7 -    by (simp add: gcd_commute_nat)
    12.8 +    by (simp add: gcd.commute)
    12.9    also assume "\<dots> = 1"
   12.10    finally show "?P (n + 2)" .
   12.11  qed
   12.12 @@ -104,16 +104,16 @@
   12.13  next
   12.14    case (Suc k)
   12.15    then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
   12.16 -    by (simp add: gcd_commute_nat)
   12.17 +    by (simp add: gcd.commute)
   12.18    also have "fib (n + k + 1)
   12.19        = fib (k + 1) * fib (n + 1) + fib k * fib n"
   12.20      by (rule fib_add)
   12.21    also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
   12.22      by (simp add: gcd_mult_add)
   12.23    also have "\<dots> = gcd (fib n) (fib (k + 1))"
   12.24 -    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
   12.25 +    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
   12.26    also have "\<dots> = gcd (fib m) (fib n)"
   12.27 -    using Suc by (simp add: gcd_commute_nat)
   12.28 +    using Suc by (simp add: gcd.commute)
   12.29    finally show ?thesis .
   12.30  qed
   12.31  
   12.32 @@ -171,7 +171,7 @@
   12.33    also from n have "\<dots> = gcd (fib n) (fib m)"
   12.34      by (rule gcd_fib_mod)
   12.35    also have "\<dots> = gcd (fib m) (fib n)"
   12.36 -    by (rule gcd_commute_nat)
   12.37 +    by (rule gcd.commute)
   12.38    finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
   12.39  qed
   12.40  
    13.1 --- a/src/HOL/Library/Float.thy	Wed Feb 17 21:51:57 2016 +0100
    13.2 +++ b/src/HOL/Library/Float.thy	Wed Feb 17 21:51:57 2016 +0100
    13.3 @@ -1261,7 +1261,7 @@
    13.4      case True
    13.5      def x' \<equiv> "x * 2 ^ nat l"
    13.6      have "int x * 2 ^ nat l = x'"
    13.7 -      by (simp add: x'_def int_mult of_nat_power)
    13.8 +      by (simp add: x'_def of_nat_mult of_nat_power)
    13.9      moreover have "real x * 2 powr l = real x'"
   13.10        by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
   13.11      ultimately show ?thesis
   13.12 @@ -1274,7 +1274,7 @@
   13.13      case False
   13.14      def y' \<equiv> "y * 2 ^ nat (- l)"
   13.15      from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
   13.16 -    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power)
   13.17 +    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def of_nat_mult of_nat_power)
   13.18      moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
   13.19        using \<open>\<not> 0 \<le> l\<close>
   13.20        by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
    14.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Feb 17 21:51:57 2016 +0100
    14.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Feb 17 21:51:57 2016 +0100
    14.3 @@ -230,7 +230,7 @@
    14.4             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    14.5             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    14.6  apply (rule mod_type.intro)
    14.7 -apply (simp add: int_mult type_definition_bit0)
    14.8 +apply (simp add: of_nat_mult type_definition_bit0)
    14.9  apply (rule one_less_int_card)
   14.10  apply (rule zero_bit0_def)
   14.11  apply (rule one_bit0_def)
   14.12 @@ -245,7 +245,7 @@
   14.13             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   14.14             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   14.15  apply (rule mod_type.intro)
   14.16 -apply (simp add: int_mult type_definition_bit1)
   14.17 +apply (simp add: of_nat_mult type_definition_bit1)
   14.18  apply (rule one_less_int_card)
   14.19  apply (rule zero_bit1_def)
   14.20  apply (rule one_bit1_def)
    15.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Wed Feb 17 21:51:57 2016 +0100
    15.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Wed Feb 17 21:51:57 2016 +0100
    15.3 @@ -469,7 +469,7 @@
    15.4      "int (n * m) = int n * int m"
    15.5      "int (n div m) = int n div int m"
    15.6      "int (n mod m) = int n mod int m"
    15.7 -    by (auto simp add: int_mult zdiv_int zmod_int)}
    15.8 +    by (auto simp add: of_nat_mult zdiv_int zmod_int)}
    15.9  
   15.10    val int_if = mk_meta_eq @{lemma
   15.11      "int (if P then n else m) = (if P then int n else int m)"
   15.12 @@ -479,7 +479,7 @@
   15.13      let
   15.14        val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   15.15        val tac =
   15.16 -        Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
   15.17 +        Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm of_nat_numeral}]) 1
   15.18      in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
   15.19  
   15.20    fun ite_conv cv1 cv2 =
    16.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Feb 17 21:51:57 2016 +0100
    16.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Feb 17 21:51:57 2016 +0100
    16.3 @@ -155,8 +155,8 @@
    16.4  
    16.5  lemma not_true_eq_false: "(~ True) = False" by simp
    16.6  
    16.7 -lemmas powerarith = nat_numeral zpower_numeral_even
    16.8 -  zpower_numeral_odd zpower_Pls
    16.9 +lemmas powerarith = nat_numeral power_numeral_even
   16.10 +  power_numeral_odd zpower_Pls
   16.11  
   16.12  definition float :: "(int \<times> int) \<Rightarrow> real" where
   16.13    "float = (\<lambda>(a, b). real_of_int a * 2 powr real_of_int b)"
    17.1 --- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Wed Feb 17 21:51:57 2016 +0100
    17.2 +++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Wed Feb 17 21:51:57 2016 +0100
    17.3 @@ -42,7 +42,7 @@
    17.4    nat_numeral nat_0 nat_neg_numeral
    17.5    of_int_numeral of_int_neg_numeral of_int_0
    17.6  
    17.7 -lemmas zpowerarith = zpower_numeral_even zpower_numeral_odd zpower_Pls int_pow_1
    17.8 +lemmas zpowerarith = power_numeral_even power_numeral_odd zpower_Pls int_pow_1
    17.9  
   17.10  (* div, mod *)
   17.11  
    18.1 --- a/src/HOL/Nat_Transfer.thy	Wed Feb 17 21:51:57 2016 +0100
    18.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Feb 17 21:51:57 2016 +0100
    18.3 @@ -286,7 +286,7 @@
    18.4      "(int x) * (int y) = int (x * y)"
    18.5      "tsub (int x) (int y) = int (x - y)"
    18.6      "(int x)^n = int (x^n)"
    18.7 -  by (auto simp add: int_mult tsub_def of_nat_power)
    18.8 +  by (auto simp add: of_nat_mult tsub_def of_nat_power)
    18.9  
   18.10  lemma transfer_int_nat_function_closures:
   18.11      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
    19.1 --- a/src/HOL/Num.thy	Wed Feb 17 21:51:57 2016 +0100
    19.2 +++ b/src/HOL/Num.thy	Wed Feb 17 21:51:57 2016 +0100
    19.3 @@ -833,6 +833,11 @@
    19.4  
    19.5  end
    19.6  
    19.7 +text\<open>Also the class for fields with characteristic zero.\<close>
    19.8 +
    19.9 +class field_char_0 = field + ring_char_0
   19.10 +
   19.11 +
   19.12  subsubsection \<open>
   19.13    Structures with negation and order: class \<open>linordered_idom\<close>
   19.14  \<close>
   19.15 @@ -1099,6 +1104,8 @@
   19.16  context linordered_field
   19.17  begin
   19.18  
   19.19 +subclass field_char_0 ..
   19.20 +
   19.21  lemma half_gt_zero_iff:
   19.22    "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
   19.23    by (auto simp add: field_simps)
    20.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
    20.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
    20.3 @@ -557,13 +557,13 @@
    20.4  lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
    20.5      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
    20.6    apply (cases "y \<le> x")
    20.7 -  apply (metis cong_altdef_nat lcm_least_nat)
    20.8 +  apply (metis cong_altdef_nat lcm_least)
    20.9    apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
   20.10    done
   20.11  
   20.12  lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
   20.13      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   20.14 -  by (auto simp add: cong_altdef_int lcm_least_int) [1]
   20.15 +  by (auto simp add: cong_altdef_int lcm_least) [1]
   20.16  
   20.17  lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   20.18      (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   20.19 @@ -591,7 +591,7 @@
   20.20    from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   20.21      by auto
   20.22    from a have b: "coprime m2 m1"
   20.23 -    by (subst gcd_commute_nat)
   20.24 +    by (subst gcd.commute)
   20.25    from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   20.26      by auto
   20.27    have "[m1 * x1 = 0] (mod m1)"
   20.28 @@ -610,7 +610,7 @@
   20.29    from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   20.30      by auto
   20.31    from a have b: "coprime m2 m1"
   20.32 -    by (subst gcd_commute_int)
   20.33 +    by (subst gcd.commute)
   20.34    from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   20.35      by auto
   20.36    have "[m1 * x1 = 0] (mod m1)"
    21.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:57 2016 +0100
    21.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:57 2016 +0100
    21.3 @@ -1200,7 +1200,7 @@
    21.4  qed
    21.5  
    21.6  subclass semiring_Gcd
    21.7 -  by standard (simp_all add: Gcd_greatest)
    21.8 +  by standard (auto intro: Gcd_greatest Lcm_least)
    21.9  
   21.10  lemma GcdI:
   21.11    assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
   21.12 @@ -1212,9 +1212,6 @@
   21.13    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
   21.14    by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
   21.15  
   21.16 -subclass semiring_Lcm
   21.17 -  by standard (simp add: Lcm_Gcd)
   21.18 -
   21.19  lemma Gcd_1:
   21.20    "1 \<in> A \<Longrightarrow> Gcd A = 1"
   21.21    by (auto intro!: Gcd_eq_1_I)
    22.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Feb 17 21:51:57 2016 +0100
    22.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Feb 17 21:51:57 2016 +0100
    22.3 @@ -344,13 +344,13 @@
    22.4    then have *: "is_prime (nat \<bar>p\<bar>)" by simp
    22.5    assume "p dvd k * l"
    22.6    then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
    22.7 -    by (simp add: dvd_int_iff)
    22.8 +    by (simp add: dvd_int_unfold_dvd_nat)
    22.9    then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
   22.10      by (simp add: abs_mult nat_mult_distrib)
   22.11    with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
   22.12      using is_primeD [of "nat \<bar>p\<bar>"] by auto
   22.13    then show "p dvd k \<or> p dvd l"
   22.14 -    by (simp add: dvd_int_iff)
   22.15 +    by (simp add: dvd_int_unfold_dvd_nat)
   22.16  next
   22.17    fix k :: int
   22.18    assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
    23.1 --- a/src/HOL/Number_Theory/Fib.thy	Wed Feb 17 21:51:57 2016 +0100
    23.2 +++ b/src/HOL/Number_Theory/Fib.thy	Wed Feb 17 21:51:57 2016 +0100
    23.3 @@ -63,11 +63,11 @@
    23.4    done
    23.5  
    23.6  lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
    23.7 -  apply (simp add: gcd_commute_nat [of "fib m"])
    23.8 +  apply (simp add: gcd.commute [of "fib m"])
    23.9    apply (cases m)
   23.10    apply (auto simp add: fib_add)
   23.11 -  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
   23.12 -    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
   23.13 +  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
   23.14 +    gcd_add_mult_nat gcd_mult_cancel gcd.commute)
   23.15    done
   23.16  
   23.17  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   23.18 @@ -98,7 +98,7 @@
   23.19  
   23.20  lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
   23.21      -- \<open>Law 6.111\<close>
   23.22 -  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
   23.23 +  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
   23.24  
   23.25  theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   23.26    by (induct n rule: nat.induct) (auto simp add:  field_simps)
    24.1 --- a/src/HOL/Number_Theory/Gauss.thy	Wed Feb 17 21:51:57 2016 +0100
    24.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Wed Feb 17 21:51:57 2016 +0100
    24.3 @@ -117,7 +117,7 @@
    24.4          order_le_less_trans [of x "(int p - 1) div 2" p]
    24.5          order_le_less_trans [of y "(int p - 1) div 2" p] 
    24.6      have "x = y"
    24.7 -      by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
    24.8 +      by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
    24.9      } note xy = this
   24.10    show ?thesis
   24.11      apply (insert p_ge_2 p_a_relprime p_minus_one_l)
   24.12 @@ -141,12 +141,12 @@
   24.13      by (metis cong_int_def)
   24.14    with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
   24.15    have "[x = y](mod p)" 
   24.16 -    by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int)
   24.17 +    by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int)
   24.18    with cong_less_imp_eq_int [of x y p] p_minus_one_l
   24.19      order_le_less_trans [of x "(int p - 1) div 2" p]
   24.20      order_le_less_trans [of y "(int p - 1) div 2" p] 
   24.21    have "x = y"
   24.22 -    by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
   24.23 +    by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
   24.24    then have False
   24.25      by (simp add: f)}
   24.26    then show ?thesis
    25.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
    25.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
    25.3 @@ -649,7 +649,7 @@
    25.4        have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
    25.5        then have pS: "Suc (p - 1) = p" by arith
    25.6        from b have d: "n dvd a^((n - 1) div p)" unfolding b0
    25.7 -        by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left 
    25.8 +        by (metis b0 diff_0_eq_0 gcd_dvd2 gcd_lcm_complete_lattice_nat.inf_bot_left 
    25.9                     gcd_lcm_complete_lattice_nat.inf_top_left) 
   25.10        from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
   25.11        have False
    26.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
    26.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
    26.3 @@ -64,7 +64,7 @@
    26.4  
    26.5  lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
    26.6    apply (unfold prime_def)
    26.7 -  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
    26.8 +  apply (metis gcd_dvd1 gcd_dvd2)
    26.9    done
   26.10  
   26.11  lemma prime_int_altdef:
   26.12 @@ -72,22 +72,22 @@
   26.13      m = 1 \<or> m = p))"
   26.14    apply (simp add: prime_def)
   26.15    apply (auto simp add: )
   26.16 -  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
   26.17 +  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
   26.18    apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
   26.19    done
   26.20  
   26.21  lemma prime_imp_coprime_int:
   26.22    fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   26.23    apply (unfold prime_int_altdef)
   26.24 -  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   26.25 +  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   26.26    done
   26.27  
   26.28  lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   26.29 -  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   26.30 +  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
   26.31  
   26.32  lemma prime_dvd_mult_int:
   26.33    fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   26.34 -  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   26.35 +  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
   26.36  
   26.37  lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
   26.38      p dvd m * n = (p dvd m \<or> p dvd n)"
   26.39 @@ -198,20 +198,20 @@
   26.40      { assume pa: "p dvd a"
   26.41        from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   26.42        with p have "coprime b p"
   26.43 -        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   26.44 +        by (subst gcd.commute, intro prime_imp_coprime_nat)
   26.45        then have pnb: "coprime (p^n) b"
   26.46 -        by (subst gcd_commute_nat, rule coprime_exp_nat)
   26.47 -      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   26.48 +        by (subst gcd.commute, rule coprime_exp_nat)
   26.49 +      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
   26.50      moreover
   26.51      { assume pb: "p dvd b"
   26.52        have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
   26.53        from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   26.54          by auto
   26.55        with p have "coprime a p"
   26.56 -        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   26.57 +        by (subst gcd.commute, intro prime_imp_coprime_nat)
   26.58        then have pna: "coprime (p^n) a"
   26.59 -        by (subst gcd_commute_nat, rule coprime_exp_nat)
   26.60 -      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   26.61 +        by (subst gcd.commute, rule coprime_exp_nat)
   26.62 +      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
   26.63      ultimately have ?thesis by blast }
   26.64    ultimately show ?thesis by blast
   26.65  qed
    27.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Feb 17 21:51:57 2016 +0100
    27.2 +++ b/src/HOL/Number_Theory/Residues.thy	Wed Feb 17 21:51:57 2016 +0100
    27.3 @@ -209,7 +209,7 @@
    27.4  sublocale residues_prime < residues p
    27.5    apply (unfold R_def residues_def)
    27.6    using p_prime apply auto
    27.7 -  apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
    27.8 +  apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
    27.9    done
   27.10  
   27.11  context residues_prime
   27.12 @@ -221,7 +221,7 @@
   27.13    apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
   27.14    apply (rule classical)
   27.15    apply (erule notE)
   27.16 -  apply (subst gcd_commute_int)
   27.17 +  apply (subst gcd.commute)
   27.18    apply (rule prime_imp_coprime_int)
   27.19    apply (rule p_prime)
   27.20    apply (rule notI)
   27.21 @@ -232,7 +232,7 @@
   27.22  lemma res_prime_units_eq: "Units R = {1..p - 1}"
   27.23    apply (subst res_units_eq)
   27.24    apply auto
   27.25 -  apply (subst gcd_commute_int)
   27.26 +  apply (subst gcd.commute)
   27.27    apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
   27.28    done
   27.29  
   27.30 @@ -256,8 +256,8 @@
   27.31    apply (rule bij_betw_same_card [of nat])
   27.32    apply (auto simp add: inj_on_def bij_betw_def image_def)
   27.33    apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
   27.34 -  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int
   27.35 -    transfer_int_nat_gcd(1) zless_int)
   27.36 +  apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
   27.37 +    transfer_int_nat_gcd(1) of_nat_less_iff)
   27.38    done
   27.39  
   27.40  lemma prime_phi:
   27.41 @@ -370,7 +370,7 @@
   27.42    assumes "prime p" and "\<not> p dvd a"
   27.43    shows "[a ^ (p - 1) = 1] (mod p)"
   27.44    using fermat_theorem [of p a] assms
   27.45 -  by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
   27.46 +  by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
   27.47  
   27.48  
   27.49  subsection \<open>Wilson's theorem\<close>
    28.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
    28.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
    28.3 @@ -98,14 +98,14 @@
    28.4    finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
    28.5    moreover
    28.6    have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
    28.7 -    apply (subst gcd_commute_nat)
    28.8 +    apply (subst gcd.commute)
    28.9      apply (rule setprod_coprime_nat)
   28.10      apply (rule primes_imp_powers_coprime_nat)
   28.11      using assms True
   28.12      apply auto
   28.13      done
   28.14    ultimately have "a ^ count M a dvd a ^ count N a"
   28.15 -    by (elim coprime_dvd_mult_nat)
   28.16 +    by (elim coprime_dvd_mult)
   28.17    with a show ?thesis
   28.18      using power_dvd_imp_le prime_def by blast
   28.19  next
   28.20 @@ -661,7 +661,7 @@
   28.21    fixes x y :: int
   28.22    shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
   28.23      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   28.24 -  by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
   28.25 +  by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int
   28.26      zero_le_imp_eq_int zero_less_imp_eq_int)
   28.27  
   28.28  lemma dvd_multiplicity_eq_nat:
    29.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Feb 17 21:51:57 2016 +0100
    29.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Feb 17 21:51:57 2016 +0100
    29.3 @@ -602,7 +602,7 @@
    29.4    from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
    29.5      unfolding dvd_def by blast
    29.6    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
    29.7 -  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
    29.8 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: of_nat_mult)
    29.9    then show ?thesis
   29.10      apply (subst abs_dvd_iff [symmetric])
   29.11      apply (subst dvd_abs_iff [symmetric])
    30.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
    30.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
    30.3 @@ -823,7 +823,7 @@
    30.4     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
    30.5  apply(auto simp add:inj_on_def)
    30.6  apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
    30.7 -apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right)
    30.8 +apply (metis coprime_commute coprime_divprod dvd_triv_right gcd_semilattice_nat.dual_order.strict_trans2)
    30.9  done
   30.10  
   30.11  declare power_Suc0[simp del]
    31.1 --- a/src/HOL/Presburger.thy	Wed Feb 17 21:51:57 2016 +0100
    31.2 +++ b/src/HOL/Presburger.thy	Wed Feb 17 21:51:57 2016 +0100
    31.3 @@ -376,7 +376,7 @@
    31.4  
    31.5  lemma zdiff_int_split: "P (int (x - y)) =
    31.6    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    31.7 -  by (cases "y \<le> x") (simp_all add: zdiff_int)
    31.8 +  by (cases "y \<le> x") (simp_all add: of_nat_diff)
    31.9  
   31.10  text \<open>
   31.11    \medskip Specific instances of congruence rules, to prevent
    32.1 --- a/src/HOL/Rat.thy	Wed Feb 17 21:51:57 2016 +0100
    32.2 +++ b/src/HOL/Rat.thy	Wed Feb 17 21:51:57 2016 +0100
    32.3 @@ -78,7 +78,7 @@
    32.4    from \<open>q = Fract a b\<close> \<open>b \<noteq> 0\<close> \<open>?b \<noteq> 0\<close> have q: "q = Fract ?a ?b"
    32.5      by (simp add: eq_rat dvd_div_mult mult.commute [of a])
    32.6    from \<open>b \<noteq> 0\<close> have coprime: "coprime ?a ?b"
    32.7 -    by (auto intro: div_gcd_coprime_int)
    32.8 +    by (auto intro: div_gcd_coprime)
    32.9    show C proof (cases "b > 0")
   32.10      case True
   32.11      note assms
   32.12 @@ -287,7 +287,7 @@
   32.13      split:split_if_asm)
   32.14  
   32.15  lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
   32.16 -  by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
   32.17 +  by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime
   32.18      split:split_if_asm)
   32.19  
   32.20  lemma normalize_stable [simp]:
    33.1 --- a/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
    33.2 +++ b/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
    33.3 @@ -1282,7 +1282,7 @@
    33.4        @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
    33.5        @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
    33.6        @{thm of_int_mult}, @{thm of_int_of_nat_eq},
    33.7 -      @{thm of_nat_numeral}, @{thm int_numeral}, @{thm of_int_neg_numeral}]
    33.8 +      @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
    33.9    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"})
   33.10    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"}))
   33.11  \<close>
    34.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 17 21:51:57 2016 +0100
    34.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 17 21:51:57 2016 +0100
    34.3 @@ -812,14 +812,14 @@
    34.4    simpset_of (put_simpset comp_ss @{context}
    34.5      addsimps @{thms simp_thms} @ 
    34.6              [@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] 
    34.7 -        @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}]
    34.8 +        @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
    34.9      |> Splitter.add_split @{thm "zdiff_int_split"})
   34.10  
   34.11  val ss2 =
   34.12    simpset_of (put_simpset HOL_basic_ss @{context}
   34.13 -    addsimps [@{thm "nat_0_le"}, @{thm "int_numeral"},
   34.14 +    addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"},
   34.15                @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, 
   34.16 -              @{thm "le_numeral_extra"(3)}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   34.17 +              @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}]
   34.18      |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}])
   34.19  val div_mod_ss =
   34.20    simpset_of (put_simpset HOL_basic_ss @{context}
    35.1 --- a/src/HOL/Word/Word.thy	Wed Feb 17 21:51:57 2016 +0100
    35.2 +++ b/src/HOL/Word/Word.thy	Wed Feb 17 21:51:57 2016 +0100
    35.3 @@ -1416,7 +1416,7 @@
    35.4    apply (unfold udvd_def)
    35.5    apply safe
    35.6     apply (simp add: unat_def nat_mult_distrib)
    35.7 -  apply (simp add: uint_nat int_mult)
    35.8 +  apply (simp add: uint_nat of_nat_mult)
    35.9    apply (rule exI)
   35.10    apply safe
   35.11     prefer 2
   35.12 @@ -3295,7 +3295,7 @@
   35.13    apply (unfold dvd_def) 
   35.14    apply auto 
   35.15    apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
   35.16 -  apply (simp add : int_mult of_nat_power)
   35.17 +  apply (simp add : of_nat_mult of_nat_power)
   35.18    apply (simp add : nat_mult_distrib nat_power_eq)
   35.19    done
   35.20  
   35.21 @@ -4240,9 +4240,10 @@
   35.22    apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
   35.23    apply (rule rotater_eqs)
   35.24    apply (simp add: word_size nat_mod_distrib)
   35.25 -  apply (rule int_eq_0_conv [THEN iffD1])
   35.26 -  apply (simp only: zmod_int of_nat_add)
   35.27 -  apply (simp add: rdmods)
   35.28 +  apply (rule of_nat_eq_0_iff [THEN iffD1])
   35.29 +  apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
   35.30 +  using mod_mod_trivial zmod_eq_dvd_iff
   35.31 +  apply blast
   35.32    done
   35.33  
   35.34  lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
    36.1 --- a/src/HOL/ex/LocaleTest2.thy	Wed Feb 17 21:51:57 2016 +0100
    36.2 +++ b/src/HOL/ex/LocaleTest2.thy	Wed Feb 17 21:51:57 2016 +0100
    36.3 @@ -599,7 +599,7 @@
    36.4      apply (rule_tac x = "gcd x y" in exI)
    36.5      apply auto [1]
    36.6      apply (rule_tac x = "lcm x y" in exI)
    36.7 -    apply (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
    36.8 +    apply (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
    36.9      done
   36.10    then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
   36.11    txt \<open>Interpretation to ease use of definitions, which are
   36.12 @@ -613,7 +613,7 @@
   36.13      apply (unfold nat_dvd.join_def)
   36.14      apply (rule the_equality)
   36.15      apply (unfold nat_dvd.is_sup_def)
   36.16 -    by (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
   36.17 +    by (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
   36.18  qed
   36.19  
   36.20  text \<open>Interpreted theorems from the locales, involving defined terms.\<close>
    37.1 --- a/src/HOL/ex/NatSum.thy	Wed Feb 17 21:51:57 2016 +0100
    37.2 +++ b/src/HOL/ex/NatSum.thy	Wed Feb 17 21:51:57 2016 +0100
    37.3 @@ -98,7 +98,7 @@
    37.4    "30 * int (\<Sum>i=0..<m. i * i * i * i) =
    37.5      int m * (int m - 1) * (int(2 * m) - 1) *
    37.6      (int(3 * m * m) - int(3 * m) - 1)"
    37.7 -  by (induct m) (simp_all add: int_mult)
    37.8 +  by (induct m) (simp_all add: of_nat_mult)
    37.9  
   37.10  lemma of_nat_sum_of_fourth_powers:
   37.11    "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
    38.1 --- a/src/HOL/ex/Sqrt.thy	Wed Feb 17 21:51:57 2016 +0100
    38.2 +++ b/src/HOL/ex/Sqrt.thy	Wed Feb 17 21:51:57 2016 +0100
    38.3 @@ -77,7 +77,7 @@
    38.4    with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
    38.5    then have "p dvd n\<^sup>2" ..
    38.6    with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
    38.7 -  with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
    38.8 +  with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
    38.9    with \<open>coprime m n\<close> have "p = 1" by simp
   38.10    with p show False by simp
   38.11  qed
    39.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Wed Feb 17 21:51:57 2016 +0100
    39.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Wed Feb 17 21:51:57 2016 +0100
    39.3 @@ -40,10 +40,10 @@
    39.4    unfolding rel_fun_def ZN_def by simp
    39.5  
    39.6  lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
    39.7 -  unfolding rel_fun_def ZN_def by (simp add: int_mult)
    39.8 +  unfolding rel_fun_def ZN_def by (simp add: of_nat_mult)
    39.9  
   39.10  lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
   39.11 -  unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
   39.12 +  unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff)
   39.13  
   39.14  lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
   39.15    unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
   39.16 @@ -65,7 +65,7 @@
   39.17  
   39.18  lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
   39.19    unfolding rel_fun_def ZN_def Bex_def atLeast_iff
   39.20 -  by (metis zero_le_imp_eq_int zero_zle_int)
   39.21 +  by (metis zero_le_imp_eq_int of_nat_0_le_iff)
   39.22  
   39.23  lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
   39.24    unfolding rel_fun_def ZN_def by simp