--- a/NEWS Wed Feb 17 21:51:57 2016 +0100
+++ b/NEWS Wed Feb 17 21:51:57 2016 +0100
@@ -37,9 +37,72 @@
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
-* Lemma generalization:
- realpow_minus_mult ~> power_minus_mult
- realpow_Suc_le_self ~> power_Suc_le_self
+* Dropped various legacy fact bindings, whose replacements are often
+of a more general type also:
+ lcm_left_commute_nat ~> lcm.left_commute
+ lcm_left_commute_int ~> lcm.left_commute
+ gcd_left_commute_nat ~> gcd.left_commute
+ gcd_left_commute_int ~> gcd.left_commute
+ gcd_greatest_iff_nat ~> gcd_greatest_iff
+ gcd_greatest_iff_int ~> gcd_greatest_iff
+ coprime_dvd_mult_nat ~> coprime_dvd_mult
+ coprime_dvd_mult_int ~> coprime_dvd_mult
+ zpower_numeral_even ~> power_numeral_even
+ gcd_mult_cancel_nat ~> gcd_mult_cancel
+ gcd_mult_cancel_int ~> gcd_mult_cancel
+ div_gcd_coprime_nat ~> div_gcd_coprime
+ div_gcd_coprime_int ~> div_gcd_coprime
+ zpower_numeral_odd ~> power_numeral_odd
+ zero_less_int_conv ~> of_nat_0_less_iff
+ gcd_greatest_nat ~> gcd_greatest
+ gcd_greatest_int ~> gcd_greatest
+ coprime_mult_nat ~> coprime_mult
+ coprime_mult_int ~> coprime_mult
+ lcm_commute_nat ~> lcm.commute
+ lcm_commute_int ~> lcm.commute
+ int_less_0_conv ~> of_nat_less_0_iff
+ gcd_commute_nat ~> gcd.commute
+ gcd_commute_int ~> gcd.commute
+ Gcd_insert_nat ~> Gcd_insert
+ Gcd_insert_int ~> Gcd_insert
+ of_int_int_eq ~> of_int_of_nat_eq
+ lcm_least_nat ~> lcm_least
+ lcm_least_int ~> lcm_least
+ lcm_assoc_nat ~> lcm.assoc
+ lcm_assoc_int ~> lcm.assoc
+ int_le_0_conv ~> of_nat_le_0_iff
+ int_eq_0_conv ~> of_nat_eq_0_iff
+ Gcd_empty_nat ~> Gcd_empty
+ Gcd_empty_int ~> Gcd_empty
+ gcd_assoc_nat ~> gcd.assoc
+ gcd_assoc_int ~> gcd.assoc
+ zero_zle_int ~> of_nat_0_le_iff
+ lcm_dvd2_nat ~> dvd_lcm2
+ lcm_dvd2_int ~> dvd_lcm2
+ lcm_dvd1_nat ~> dvd_lcm1
+ lcm_dvd1_int ~> dvd_lcm1
+ gcd_zero_nat ~> gcd_eq_0_iff
+ gcd_zero_int ~> gcd_eq_0_iff
+ gcd_dvd2_nat ~> gcd_dvd2
+ gcd_dvd2_int ~> gcd_dvd2
+ gcd_dvd1_nat ~> gcd_dvd1
+ gcd_dvd1_int ~> gcd_dvd1
+ int_numeral ~> of_nat_numeral
+ lcm_ac_nat ~> ac_simps
+ lcm_ac_int ~> ac_simps
+ gcd_ac_nat ~> ac_simps
+ gcd_ac_int ~> ac_simps
+ abs_int_eq ~> abs_of_nat
+ zless_int ~> of_nat_less_iff
+ zdiff_int ~> of_nat_diff
+ zadd_int ~> of_nat_add
+ int_mult ~> of_nat_mult
+ int_Suc ~> of_nat_Suc
+ inj_int ~> inj_of_nat
+ int_1 ~> of_nat_1
+ int_0 ~> of_nat_0
+ realpow_minus_mult ~> power_minus_mult
+ realpow_Suc_le_self ~> power_Suc_le_self
INCOMPATIBILITY.
--- a/src/HOL/Algebra/Exponent.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Algebra/Exponent.thy Wed Feb 17 21:51:57 2016 +0100
@@ -201,7 +201,7 @@
apply (drule less_imp_le [of a])
apply (drule le_imp_power_dvd)
apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
-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))
+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))
done
lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
--- a/src/HOL/Algebra/IntRing.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Algebra/IntRing.thy Wed Feb 17 21:51:57 2016 +0100
@@ -251,7 +251,7 @@
then obtain x where "1 = x * int p" by best
then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
then show False
- by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
+ by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
qed
--- a/src/HOL/Archimedean_Field.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Archimedean_Field.thy Wed Feb 17 21:51:57 2016 +0100
@@ -575,11 +575,10 @@
lemma frac_unique_iff:
fixes x :: "'a::floor_ceiling"
- shows "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
- apply (auto simp: Ints_def frac_def)
- apply linarith
- apply linarith
- by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
+ shows "frac x = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
+ apply (auto simp: Ints_def frac_def algebra_simps floor_unique)
+ apply linarith+
+ done
lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
by (simp add: frac_unique_iff)
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Wed Feb 17 21:51:57 2016 +0100
@@ -27,7 +27,7 @@
(let g = gcd a b
in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
-declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
+declare gcd_dvd1[presburger] gcd_dvd2[presburger]
lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
proof -
@@ -51,7 +51,7 @@
from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
- from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
+ from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
from ab consider "b < 0" | "b > 0" by arith
then show ?thesis
proof cases
@@ -142,7 +142,7 @@
lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
apply (simp add: Ninv_def isnormNum_def split_def)
apply (cases "fst x = 0")
- apply (auto simp add: gcd_commute_int)
+ apply (auto simp add: gcd.commute)
done
lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
@@ -197,7 +197,7 @@
by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
- by (simp_all add: x y isnormNum_def add: gcd_commute_int)
+ by (simp_all add: x y isnormNum_def add: gcd.commute)
from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
apply -
apply algebra
@@ -205,8 +205,8 @@
apply simp
apply algebra
done
- from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
- coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
+ from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
+ coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
have eq1: "b = b'" using pos by arith
with eq have "a = a'" using pos by simp
with eq1 show ?thesis by (simp add: x y)
@@ -551,7 +551,7 @@
qed
lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
- by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute)
+ by (simp add: Nmul_def split_def Let_def gcd.commute mult.commute)
lemma Nmul_assoc:
assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 17 21:51:57 2016 +0100
@@ -62,13 +62,14 @@
val simpset1 =
put_simpset HOL_basic_ss ctxt
addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
- map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int}
+ 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]}
|> Splitter.add_split @{thm zdiff_int_split}
(*simp rules for elimination of int n*)
val simpset2 =
put_simpset HOL_basic_ss ctxt
- 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}]
+ addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *),
+ @{thm of_nat_0 [where ?'a = int]}, @{thm of_nat_1 [where ?'a = int]}]
|> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
(* simp rules for elimination of abs *)
val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 17 21:51:57 2016 +0100
@@ -88,13 +88,13 @@
(* Simp rules for changing (n::int) to int n *)
val simpset1 = put_simpset HOL_basic_ss ctxt
addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
- map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm nat_numeral}]
+ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
|> Splitter.add_split @{thm "zdiff_int_split"}
(*simp rules for elimination of int n*)
val simpset2 = put_simpset HOL_basic_ss ctxt
addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral},
- @{thm "int_0"}, @{thm "int_1"}]
+ @{thm "of_nat_0"}, @{thm "of_nat_1"}]
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
(* simp rules for elimination of abs *)
val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
--- a/src/HOL/GCD.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/GCD.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1736,7 +1736,7 @@
lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
unfolding lcm_int_def gcd_int_def
- apply (subst int_mult [symmetric])
+ apply (subst of_nat_mult [symmetric])
apply (subst prod_gcd_lcm_nat [symmetric])
apply (subst nat_abs_mult_distrib [symmetric])
apply (simp, simp add: abs_mult)
@@ -2057,42 +2057,6 @@
text \<open>Fact aliasses\<close>
-lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
-lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
-lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
-lemmas gcd_commute_int = gcd.commute [where ?'a = int]
-lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
-lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
-lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
-lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
-lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
-lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
-lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
-lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
-lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
-lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
-lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat]
-lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int]
-lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
-lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
-lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
-lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
-
-lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
-lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
-lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
-lemmas lcm_commute_int = lcm.commute [where ?'a = int]
-lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
-lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
-lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
-lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
-lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
-lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
-lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
-lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
-lemmas lcm_least_nat = lcm_least [where ?'a = nat]
-lemmas lcm_least_int = lcm_least [where ?'a = int]
-
lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
by (fact lcm_eq_0_iff)
@@ -2111,13 +2075,6 @@
lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
by (fact dvd_lcmI2)
-lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
-lemmas coprime_mult_int = coprime_mult [where ?'a = int]
-lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
-lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
-lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
-lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
-
lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
(k dvd m * n) = (k dvd m)"
by (fact coprime_dvd_mult_iff)
@@ -2136,10 +2093,6 @@
lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
-lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
-lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
-lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
-lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
lemma dvd_Lcm_int [simp]:
fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
--- a/src/HOL/Groups.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Groups.thy Wed Feb 17 21:51:57 2016 +0100
@@ -999,14 +999,17 @@
apply (simp add: algebra_simps)
done
-lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
-by (simp add: less_diff_eq)
+lemma diff_gt_0_iff_gt [simp]:
+ "a - b > 0 \<longleftrightarrow> a > b"
+ by (simp add: less_diff_eq)
-lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
-by (auto simp add: le_less diff_less_eq )
+lemma diff_le_eq [algebra_simps, field_simps]:
+ "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+ by (auto simp add: le_less diff_less_eq )
-lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
-by (auto simp add: le_less less_diff_eq)
+lemma le_diff_eq [algebra_simps, field_simps]:
+ "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
+ by (auto simp add: le_less less_diff_eq)
lemma diff_le_0_iff_le [simp]:
"a - b \<le> 0 \<longleftrightarrow> a \<le> b"
@@ -1014,6 +1017,10 @@
lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+lemma diff_ge_0_iff_ge [simp]:
+ "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
+ by (simp add: le_diff_eq)
+
lemma diff_eq_diff_less:
"a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
--- a/src/HOL/Inequalities.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Inequalities.thy Wed Feb 17 21:51:57 2016 +0100
@@ -31,7 +31,7 @@
have "m*(m-1) \<le> n*(n + 1)"
using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
- by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
+ by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_setsum
split: zdiff_int_split)
thus ?thesis
using of_nat_eq_iff by blast
@@ -64,7 +64,7 @@
{ fix i j::nat assume "i<n" "j<n"
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"
using assms by (cases "i \<le> j") (auto simp: algebra_simps)
- } hence "?S \<le> 0"
+ } then have "?S \<le> 0"
by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
finally show ?thesis by (simp add: algebra_simps)
qed
--- a/src/HOL/Int.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Int.thy Wed Feb 17 21:51:57 2016 +0100
@@ -570,15 +570,19 @@
lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
-lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
-proof -
- have "(w \<le> z) = (0 \<le> z - w)"
- by (simp only: le_diff_eq add_0_left)
- also have "\<dots> = (\<exists>n. z - w = of_nat n)"
- by (auto elim: zero_le_imp_eq_int)
- also have "\<dots> = (\<exists>n. z = w + of_nat n)"
- by (simp only: algebra_simps)
- finally show ?thesis .
+lemma zle_iff_zadd:
+ "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then show ?P by auto
+next
+ assume ?P
+ then have "0 \<le> z - w" by simp
+ then obtain n where "z - w = int n"
+ using zero_le_imp_eq_int [of "z - w"] by blast
+ then have "z = w + int n"
+ by simp
+ then show ?Q ..
qed
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
@@ -1725,34 +1729,9 @@
hide_const (open) Pos Neg sub dup
-subsection \<open>Legacy theorems\<close>
-
-lemmas inj_int = inj_of_nat [where 'a=int]
-lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
-lemmas int_mult = of_nat_mult [where 'a=int]
-lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
-lemmas zless_int = of_nat_less_iff [where 'a=int]
-lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
-lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
-lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
-lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
-lemmas int_0 = of_nat_0 [where 'a=int]
-lemmas int_1 = of_nat_1 [where 'a=int]
-lemmas int_Suc = of_nat_Suc [where 'a=int]
-lemmas int_numeral = of_nat_numeral [where 'a=int]
-lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
-lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
-lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
-lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
-lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
-
text \<open>De-register \<open>int\<close> as a quotient type:\<close>
lifting_update int.lifting
lifting_forget int.lifting
-text\<open>Also the class for fields with characteristic zero.\<close>
-class field_char_0 = field + ring_char_0
-subclass (in linordered_field) field_char_0 ..
-
end
--- a/src/HOL/Isar_Examples/Fibonacci.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Wed Feb 17 21:51:57 2016 +0100
@@ -82,7 +82,7 @@
also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
by (rule gcd_add2_nat)
also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
- by (simp add: gcd_commute_nat)
+ by (simp add: gcd.commute)
also assume "\<dots> = 1"
finally show "?P (n + 2)" .
qed
@@ -104,16 +104,16 @@
next
case (Suc k)
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
- by (simp add: gcd_commute_nat)
+ by (simp add: gcd.commute)
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
also have "\<dots> = gcd (fib n) (fib (k + 1))"
- by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
+ by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
also have "\<dots> = gcd (fib m) (fib n)"
- using Suc by (simp add: gcd_commute_nat)
+ using Suc by (simp add: gcd.commute)
finally show ?thesis .
qed
@@ -171,7 +171,7 @@
also from n have "\<dots> = gcd (fib n) (fib m)"
by (rule gcd_fib_mod)
also have "\<dots> = gcd (fib m) (fib n)"
- by (rule gcd_commute_nat)
+ by (rule gcd.commute)
finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed
--- a/src/HOL/Library/Float.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Library/Float.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1261,7 +1261,7 @@
case True
def x' \<equiv> "x * 2 ^ nat l"
have "int x * 2 ^ nat l = x'"
- by (simp add: x'_def int_mult of_nat_power)
+ by (simp add: x'_def of_nat_mult of_nat_power)
moreover have "real x * 2 powr l = real x'"
by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
ultimately show ?thesis
@@ -1274,7 +1274,7 @@
case False
def y' \<equiv> "y * 2 ^ nat (- l)"
from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
- have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power)
+ have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def of_nat_mult of_nat_power)
moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
using \<open>\<not> 0 \<le> l\<close>
by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
--- a/src/HOL/Library/Numeral_Type.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Wed Feb 17 21:51:57 2016 +0100
@@ -230,7 +230,7 @@
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
apply (rule mod_type.intro)
-apply (simp add: int_mult type_definition_bit0)
+apply (simp add: of_nat_mult type_definition_bit0)
apply (rule one_less_int_card)
apply (rule zero_bit0_def)
apply (rule one_bit0_def)
@@ -245,7 +245,7 @@
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
apply (rule mod_type.intro)
-apply (simp add: int_mult type_definition_bit1)
+apply (simp add: of_nat_mult type_definition_bit1)
apply (rule one_less_int_card)
apply (rule zero_bit1_def)
apply (rule one_bit1_def)
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Wed Feb 17 21:51:57 2016 +0100
@@ -469,7 +469,7 @@
"int (n * m) = int n * int m"
"int (n div m) = int n div int m"
"int (n mod m) = int n mod int m"
- by (auto simp add: int_mult zdiv_int zmod_int)}
+ by (auto simp add: of_nat_mult zdiv_int zmod_int)}
val int_if = mk_meta_eq @{lemma
"int (if P then n else m) = (if P then int n else int m)"
@@ -479,7 +479,7 @@
let
val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
val tac =
- Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1
+ Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm of_nat_numeral}]) 1
in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
fun ite_conv cv1 cv2 =
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Wed Feb 17 21:51:57 2016 +0100
@@ -155,8 +155,8 @@
lemma not_true_eq_false: "(~ True) = False" by simp
-lemmas powerarith = nat_numeral zpower_numeral_even
- zpower_numeral_odd zpower_Pls
+lemmas powerarith = nat_numeral power_numeral_even
+ power_numeral_odd zpower_Pls
definition float :: "(int \<times> int) \<Rightarrow> real" where
"float = (\<lambda>(a, b). real_of_int a * 2 powr real_of_int b)"
--- a/src/HOL/Matrix_LP/ComputeNumeral.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy Wed Feb 17 21:51:57 2016 +0100
@@ -42,7 +42,7 @@
nat_numeral nat_0 nat_neg_numeral
of_int_numeral of_int_neg_numeral of_int_0
-lemmas zpowerarith = zpower_numeral_even zpower_numeral_odd zpower_Pls int_pow_1
+lemmas zpowerarith = power_numeral_even power_numeral_odd zpower_Pls int_pow_1
(* div, mod *)
--- a/src/HOL/Nat_Transfer.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Nat_Transfer.thy Wed Feb 17 21:51:57 2016 +0100
@@ -286,7 +286,7 @@
"(int x) * (int y) = int (x * y)"
"tsub (int x) (int y) = int (x - y)"
"(int x)^n = int (x^n)"
- by (auto simp add: int_mult tsub_def of_nat_power)
+ by (auto simp add: of_nat_mult tsub_def of_nat_power)
lemma transfer_int_nat_function_closures:
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
--- a/src/HOL/Num.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Num.thy Wed Feb 17 21:51:57 2016 +0100
@@ -833,6 +833,11 @@
end
+text\<open>Also the class for fields with characteristic zero.\<close>
+
+class field_char_0 = field + ring_char_0
+
+
subsubsection \<open>
Structures with negation and order: class \<open>linordered_idom\<close>
\<close>
@@ -1099,6 +1104,8 @@
context linordered_field
begin
+subclass field_char_0 ..
+
lemma half_gt_zero_iff:
"0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
by (auto simp add: field_simps)
--- a/src/HOL/Number_Theory/Cong.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Wed Feb 17 21:51:57 2016 +0100
@@ -557,13 +557,13 @@
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
apply (cases "y \<le> x")
- apply (metis cong_altdef_nat lcm_least_nat)
+ apply (metis cong_altdef_nat lcm_least)
apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
done
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
- by (auto simp add: cong_altdef_int lcm_least_int) [1]
+ by (auto simp add: cong_altdef_int lcm_least) [1]
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -591,7 +591,7 @@
from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst gcd_commute_nat)
+ by (subst gcd.commute)
from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
@@ -610,7 +610,7 @@
from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst gcd_commute_int)
+ by (subst gcd.commute)
from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1200,7 +1200,7 @@
qed
subclass semiring_Gcd
- by standard (simp_all add: Gcd_greatest)
+ by standard (auto intro: Gcd_greatest Lcm_least)
lemma GcdI:
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"
@@ -1212,9 +1212,6 @@
"Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
-subclass semiring_Lcm
- by standard (simp add: Lcm_Gcd)
-
lemma Gcd_1:
"1 \<in> A \<Longrightarrow> Gcd A = 1"
by (auto intro!: Gcd_eq_1_I)
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Wed Feb 17 21:51:57 2016 +0100
@@ -344,13 +344,13 @@
then have *: "is_prime (nat \<bar>p\<bar>)" by simp
assume "p dvd k * l"
then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
- by (simp add: dvd_int_iff)
+ by (simp add: dvd_int_unfold_dvd_nat)
then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
by (simp add: abs_mult nat_mult_distrib)
with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
using is_primeD [of "nat \<bar>p\<bar>"] by auto
then show "p dvd k \<or> p dvd l"
- by (simp add: dvd_int_iff)
+ by (simp add: dvd_int_unfold_dvd_nat)
next
fix k :: int
assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
--- a/src/HOL/Number_Theory/Fib.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Fib.thy Wed Feb 17 21:51:57 2016 +0100
@@ -63,11 +63,11 @@
done
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
- apply (simp add: gcd_commute_nat [of "fib m"])
+ apply (simp add: gcd.commute [of "fib m"])
apply (cases m)
apply (auto simp add: fib_add)
- apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
- gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
+ apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
+ gcd_add_mult_nat gcd_mult_cancel gcd.commute)
done
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
@@ -98,7 +98,7 @@
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
-- \<open>Law 6.111\<close>
- by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
+ by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
by (induct n rule: nat.induct) (auto simp add: field_simps)
--- a/src/HOL/Number_Theory/Gauss.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Wed Feb 17 21:51:57 2016 +0100
@@ -117,7 +117,7 @@
order_le_less_trans [of x "(int p - 1) div 2" p]
order_le_less_trans [of y "(int p - 1) div 2" p]
have "x = y"
- by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
+ by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
} note xy = this
show ?thesis
apply (insert p_ge_2 p_a_relprime p_minus_one_l)
@@ -141,12 +141,12 @@
by (metis cong_int_def)
with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
have "[x = y](mod p)"
- by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int)
+ by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int)
with cong_less_imp_eq_int [of x y p] p_minus_one_l
order_le_less_trans [of x "(int p - 1) div 2" p]
order_le_less_trans [of y "(int p - 1) div 2" p]
have "x = y"
- by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
+ by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
then have False
by (simp add: f)}
then show ?thesis
--- a/src/HOL/Number_Theory/Pocklington.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy Wed Feb 17 21:51:57 2016 +0100
@@ -649,7 +649,7 @@
have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
then have pS: "Suc (p - 1) = p" by arith
from b have d: "n dvd a^((n - 1) div p)" unfolding b0
- by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left
+ by (metis b0 diff_0_eq_0 gcd_dvd2 gcd_lcm_complete_lattice_nat.inf_bot_left
gcd_lcm_complete_lattice_nat.inf_top_left)
from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
have False
--- a/src/HOL/Number_Theory/Primes.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Wed Feb 17 21:51:57 2016 +0100
@@ -64,7 +64,7 @@
lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_def)
- apply (metis gcd_dvd1_nat gcd_dvd2_nat)
+ apply (metis gcd_dvd1 gcd_dvd2)
done
lemma prime_int_altdef:
@@ -72,22 +72,22 @@
m = 1 \<or> m = p))"
apply (simp add: prime_def)
apply (auto simp add: )
- apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
+ apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
done
lemma prime_imp_coprime_int:
fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_int_altdef)
- apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
+ apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
done
lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
+ by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
lemma prime_dvd_mult_int:
fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
+ by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
p dvd m * n = (p dvd m \<or> p dvd n)"
@@ -198,20 +198,20 @@
{ assume pa: "p dvd a"
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
with p have "coprime b p"
- by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+ by (subst gcd.commute, intro prime_imp_coprime_nat)
then have pnb: "coprime (p^n) b"
- by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
+ by (subst gcd.commute, rule coprime_exp_nat)
+ from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
moreover
{ assume pb: "p dvd b"
have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
by auto
with p have "coprime a p"
- by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+ by (subst gcd.commute, intro prime_imp_coprime_nat)
then have pna: "coprime (p^n) a"
- by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
+ by (subst gcd.commute, rule coprime_exp_nat)
+ from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed
--- a/src/HOL/Number_Theory/Residues.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Wed Feb 17 21:51:57 2016 +0100
@@ -209,7 +209,7 @@
sublocale residues_prime < residues p
apply (unfold R_def residues_def)
using p_prime apply auto
- apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
+ apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
done
context residues_prime
@@ -221,7 +221,7 @@
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
apply (rule classical)
apply (erule notE)
- apply (subst gcd_commute_int)
+ apply (subst gcd.commute)
apply (rule prime_imp_coprime_int)
apply (rule p_prime)
apply (rule notI)
@@ -232,7 +232,7 @@
lemma res_prime_units_eq: "Units R = {1..p - 1}"
apply (subst res_units_eq)
apply auto
- apply (subst gcd_commute_int)
+ apply (subst gcd.commute)
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
done
@@ -256,8 +256,8 @@
apply (rule bij_betw_same_card [of nat])
apply (auto simp add: inj_on_def bij_betw_def image_def)
apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
- apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int
- transfer_int_nat_gcd(1) zless_int)
+ apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
+ transfer_int_nat_gcd(1) of_nat_less_iff)
done
lemma prime_phi:
@@ -370,7 +370,7 @@
assumes "prime p" and "\<not> p dvd a"
shows "[a ^ (p - 1) = 1] (mod p)"
using fermat_theorem [of p a] assms
- by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
+ by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
subsection \<open>Wilson's theorem\<close>
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Feb 17 21:51:57 2016 +0100
@@ -98,14 +98,14 @@
finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
moreover
have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
- apply (subst gcd_commute_nat)
+ apply (subst gcd.commute)
apply (rule setprod_coprime_nat)
apply (rule primes_imp_powers_coprime_nat)
using assms True
apply auto
done
ultimately have "a ^ count M a dvd a ^ count N a"
- by (elim coprime_dvd_mult_nat)
+ by (elim coprime_dvd_mult)
with a show ?thesis
using power_dvd_imp_le prime_def by blast
next
@@ -661,7 +661,7 @@
fixes x y :: int
shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
- by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
+ by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int
zero_le_imp_eq_int zero_less_imp_eq_int)
lemma dvd_multiplicity_eq_nat:
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Wed Feb 17 21:51:57 2016 +0100
@@ -602,7 +602,7 @@
from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
unfolding dvd_def by blast
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
- then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
+ then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: of_nat_mult)
then show ?thesis
apply (subst abs_dvd_iff [symmetric])
apply (subst dvd_abs_iff [symmetric])
--- a/src/HOL/Old_Number_Theory/Primes.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy Wed Feb 17 21:51:57 2016 +0100
@@ -823,7 +823,7 @@
\<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
apply(auto simp add:inj_on_def)
apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
-apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right)
+apply (metis coprime_commute coprime_divprod dvd_triv_right gcd_semilattice_nat.dual_order.strict_trans2)
done
declare power_Suc0[simp del]
--- a/src/HOL/Presburger.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Presburger.thy Wed Feb 17 21:51:57 2016 +0100
@@ -376,7 +376,7 @@
lemma zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
- by (cases "y \<le> x") (simp_all add: zdiff_int)
+ by (cases "y \<le> x") (simp_all add: of_nat_diff)
text \<open>
\medskip Specific instances of congruence rules, to prevent
--- a/src/HOL/Rat.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Rat.thy Wed Feb 17 21:51:57 2016 +0100
@@ -78,7 +78,7 @@
from \<open>q = Fract a b\<close> \<open>b \<noteq> 0\<close> \<open>?b \<noteq> 0\<close> have q: "q = Fract ?a ?b"
by (simp add: eq_rat dvd_div_mult mult.commute [of a])
from \<open>b \<noteq> 0\<close> have coprime: "coprime ?a ?b"
- by (auto intro: div_gcd_coprime_int)
+ by (auto intro: div_gcd_coprime)
show C proof (cases "b > 0")
case True
note assms
@@ -287,7 +287,7 @@
split:split_if_asm)
lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
- by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
+ by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime
split:split_if_asm)
lemma normalize_stable [simp]:
--- a/src/HOL/Real.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Real.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1282,7 +1282,7 @@
@{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
@{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
@{thm of_int_mult}, @{thm of_int_of_nat_eq},
- @{thm of_nat_numeral}, @{thm int_numeral}, @{thm of_int_neg_numeral}]
+ @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
#> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"})
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"}))
\<close>
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Feb 17 21:51:57 2016 +0100
@@ -812,14 +812,14 @@
simpset_of (put_simpset comp_ss @{context}
addsimps @{thms simp_thms} @
[@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}]
- @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}]
+ @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
|> Splitter.add_split @{thm "zdiff_int_split"})
val ss2 =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps [@{thm "nat_0_le"}, @{thm "int_numeral"},
+ addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"},
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"},
- @{thm "le_numeral_extra"(3)}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
+ @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}]
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}])
val div_mod_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
--- a/src/HOL/Word/Word.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Word/Word.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1416,7 +1416,7 @@
apply (unfold udvd_def)
apply safe
apply (simp add: unat_def nat_mult_distrib)
- apply (simp add: uint_nat int_mult)
+ apply (simp add: uint_nat of_nat_mult)
apply (rule exI)
apply safe
prefer 2
@@ -3295,7 +3295,7 @@
apply (unfold dvd_def)
apply auto
apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
- apply (simp add : int_mult of_nat_power)
+ apply (simp add : of_nat_mult of_nat_power)
apply (simp add : nat_mult_distrib nat_power_eq)
done
@@ -4240,9 +4240,10 @@
apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
apply (rule rotater_eqs)
apply (simp add: word_size nat_mod_distrib)
- apply (rule int_eq_0_conv [THEN iffD1])
- apply (simp only: zmod_int of_nat_add)
- apply (simp add: rdmods)
+ apply (rule of_nat_eq_0_iff [THEN iffD1])
+ apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
+ using mod_mod_trivial zmod_eq_dvd_iff
+ apply blast
done
lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
--- a/src/HOL/ex/LocaleTest2.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Wed Feb 17 21:51:57 2016 +0100
@@ -599,7 +599,7 @@
apply (rule_tac x = "gcd x y" in exI)
apply auto [1]
apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
+ apply (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
done
then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
txt \<open>Interpretation to ease use of definitions, which are
@@ -613,7 +613,7 @@
apply (unfold nat_dvd.join_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_sup_def)
- by (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
+ by (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
qed
text \<open>Interpreted theorems from the locales, involving defined terms.\<close>
--- a/src/HOL/ex/NatSum.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/ex/NatSum.thy Wed Feb 17 21:51:57 2016 +0100
@@ -98,7 +98,7 @@
"30 * int (\<Sum>i=0..<m. i * i * i * i) =
int m * (int m - 1) * (int(2 * m) - 1) *
(int(3 * m * m) - int(3 * m) - 1)"
- by (induct m) (simp_all add: int_mult)
+ by (induct m) (simp_all add: of_nat_mult)
lemma of_nat_sum_of_fourth_powers:
"30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
--- a/src/HOL/ex/Sqrt.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/ex/Sqrt.thy Wed Feb 17 21:51:57 2016 +0100
@@ -77,7 +77,7 @@
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
then have "p dvd n\<^sup>2" ..
with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
- with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
+ with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
with \<open>coprime m n\<close> have "p = 1" by simp
with p show False by simp
qed
--- a/src/HOL/ex/Transfer_Int_Nat.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Wed Feb 17 21:51:57 2016 +0100
@@ -40,10 +40,10 @@
unfolding rel_fun_def ZN_def by simp
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
- unfolding rel_fun_def ZN_def by (simp add: int_mult)
+ unfolding rel_fun_def ZN_def by (simp add: of_nat_mult)
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
- unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
+ unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff)
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
@@ -65,7 +65,7 @@
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
unfolding rel_fun_def ZN_def Bex_def atLeast_iff
- by (metis zero_le_imp_eq_int zero_zle_int)
+ by (metis zero_le_imp_eq_int of_nat_0_le_iff)
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
unfolding rel_fun_def ZN_def by simp