--- a/src/HOL/Divides.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Divides.thy Wed Jul 08 20:19:12 2015 +0200
@@ -118,8 +118,8 @@
lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
using mod_mult_self1 [of 0 a b] by simp
-lemma div_by_1 [simp]: "a div 1 = a"
- using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
+lemma div_by_1: "a div 1 = a"
+ by (fact divide_1)
lemma mod_by_1 [simp]: "a mod 1 = 0"
proof -
@@ -378,20 +378,6 @@
lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
by (fact mod_mult_mult1 [symmetric])
-lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
- assumes "c \<noteq> 0"
- shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
-proof -
- have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
- using assms by (simp add: mod_mult_mult1)
- then show ?thesis by (simp add: mod_eq_0_iff_dvd)
-qed
-
-lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
- assumes "c \<noteq> 0"
- shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
- using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
-
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
unfolding dvd_def by (auto simp add: mod_mult_mult1)
--- a/src/HOL/Fields.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Fields.thy Wed Jul 08 20:19:12 2015 +0200
@@ -145,9 +145,6 @@
lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
by (simp add: divide_inverse algebra_simps)
-lemma divide_1 [simp]: "a / 1 = a"
- by (simp add: divide_inverse)
-
lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
by (simp add: divide_inverse mult.assoc)
--- a/src/HOL/GCD.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/GCD.thy Wed Jul 08 20:19:12 2015 +0200
@@ -31,51 +31,6 @@
imports Main
begin
-context semidom_divide
-begin
-
-lemma divide_1 [simp]:
- "a div 1 = a"
- using nonzero_mult_divide_cancel_left [of 1 a] by simp
-
-lemma dvd_mult_cancel_left [simp]:
- assumes "a \<noteq> 0"
- shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?P then obtain d where "a * c = a * b * d" ..
- with assms have "c = b * d" by (simp add: ac_simps)
- then show ?Q ..
-next
- assume ?Q then obtain d where "c = b * d" ..
- then have "a * c = a * b * d" by (simp add: ac_simps)
- then show ?P ..
-qed
-
-lemma dvd_mult_cancel_right [simp]:
- assumes "a \<noteq> 0"
- shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
-using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps)
-
-lemma div_dvd_iff_mult:
- assumes "b \<noteq> 0" and "b dvd a"
- shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
-proof -
- from \<open>b dvd a\<close> obtain d where "a = b * d" ..
- with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
-qed
-
-lemma dvd_div_iff_mult:
- assumes "c \<noteq> 0" and "c dvd b"
- shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
-proof -
- from \<open>c dvd b\<close> obtain d where "b = c * d" ..
- with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
-qed
-
-end
-
-declare One_nat_def [simp del]
-
subsection {* GCD and LCM definitions *}
class gcd = zero + one + dvd +
@@ -145,6 +100,10 @@
with False show ?thesis by simp
qed
+lemma is_unit_gcd [simp]:
+ "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+ by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
+
sublocale gcd!: abel_semigroup gcd
proof
fix a b c
@@ -772,7 +731,7 @@
by simp
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
- by (simp add: One_nat_def)
+ by simp
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
by (simp add: gcd_int_def)
@@ -928,23 +887,29 @@
apply auto
done
-lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
- apply (insert gcd_mult_distrib_nat [of m k n])
- apply simp
- apply (erule_tac t = m in ssubst)
- apply simp
- done
+context semiring_gcd
+begin
-lemma coprime_dvd_mult_int:
- "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
-apply (subst abs_dvd_iff [symmetric])
-apply (subst dvd_abs_iff [symmetric])
-apply (subst (asm) gcd_abs_int)
-apply (rule coprime_dvd_mult_nat [transferred])
- prefer 4 apply assumption
- apply auto
-apply (subst abs_mult [symmetric], auto)
-done
+lemma coprime_dvd_mult:
+ assumes "coprime a b" and "a dvd c * b"
+ shows "a dvd c"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ then have unit: "is_unit (unit_factor c)" by simp
+ from \<open>coprime a b\<close> mult_gcd_left [of c a b]
+ have "gcd (c * a) (c * b) * unit_factor c = c"
+ by (simp add: ac_simps)
+ moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
+ by (simp add: dvd_mult_unit_iff unit)
+ ultimately show ?thesis by simp
+qed
+
+end
+
+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)"
@@ -954,21 +919,22 @@
(k dvd m * n) = (k dvd m)"
by (auto intro: coprime_dvd_mult_int)
-lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
- apply (rule dvd_antisym)
+context semiring_gcd
+begin
+
+lemma gcd_mult_cancel:
+ "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
+ apply (rule associated_eqI)
apply (rule gcd_greatest)
- apply (rule_tac n = k in coprime_dvd_mult_nat)
- apply (simp add: gcd_assoc_nat)
- apply (simp add: gcd_commute_nat)
- apply (simp_all add: mult.commute)
-done
+ apply (rule_tac b = c in coprime_dvd_mult)
+ apply (simp add: gcd.assoc)
+ apply (simp_all add: ac_simps)
+ done
-lemma gcd_mult_cancel_int:
- "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
-apply (subst (1 2) gcd_abs_int)
-apply (subst abs_mult)
-apply (rule gcd_mult_cancel_nat [transferred], auto)
-done
+end
+
+lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat]
+lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int]
lemma coprime_crossproduct_nat:
fixes a b c d :: nat
@@ -1121,8 +1087,11 @@
subsection {* Coprimality *}
-lemma div_gcd_coprime_nat:
- assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
+context semiring_gcd
+begin
+
+lemma div_gcd_coprime:
+ assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
shows "coprime (a div gcd a b) (b div gcd a b)"
proof -
let ?g = "gcd a b"
@@ -1140,29 +1109,22 @@
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
have "?g \<noteq> 0" using nz by simp
- then have gp: "?g > 0" by arith
- from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
- with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
+ moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+ thm dvd_mult_cancel_left
+ ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
qed
-lemma div_gcd_coprime_int:
- assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
- shows "coprime (a div gcd a b) (b div gcd a b)"
-apply (subst (1 2 3) gcd_abs_int)
-apply (subst (1 2) abs_div)
- apply simp
- apply simp
-apply(subst (1 2) abs_gcd_int)
-apply (rule div_gcd_coprime_nat [transferred])
-using nz apply (auto simp add: gcd_abs_int [symmetric])
-done
+end
+
+lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
+lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
using gcd_unique_nat[of 1 a b, simplified] by auto
lemma coprime_Suc_0_nat:
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
- using coprime_nat by (simp add: One_nat_def)
+ using coprime_nat by simp
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
@@ -1211,22 +1173,23 @@
using z apply force
done
-lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
- shows "coprime d (a * b)"
- apply (subst gcd_commute_nat)
- using da apply (subst gcd_mult_cancel_nat)
- apply (subst gcd_commute_nat, assumption)
- apply (subst gcd_commute_nat, rule db)
-done
+context semiring_gcd
+begin
-lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
- shows "coprime d (a * b)"
- apply (subst gcd_commute_int)
- using da apply (subst gcd_mult_cancel_int)
- apply (subst gcd_commute_int, assumption)
- apply (subst gcd_commute_int, rule db)
-done
+lemma coprime_mult:
+ assumes da: "coprime d a" and db: "coprime d b"
+ shows "coprime d (a * b)"
+ apply (subst gcd.commute)
+ using da apply (subst gcd_mult_cancel)
+ apply (subst gcd.commute, assumption)
+ apply (subst gcd.commute, rule db)
+ done
+end
+
+lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
+lemmas coprime_mult_int = coprime_mult [where ?'a = int]
+
lemma coprime_lmult_nat:
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
proof -
@@ -1305,20 +1268,41 @@
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
by (induct n) (simp_all add: coprime_mult_int)
+context semiring_gcd
+begin
+
+lemma coprime_exp_left:
+ assumes "coprime a b"
+ shows "coprime (a ^ n) b"
+ using assms by (induct n) (simp_all add: gcd_mult_cancel)
+
+lemma coprime_exp2:
+ assumes "coprime a b"
+ shows "coprime (a ^ n) (b ^ m)"
+proof (rule coprime_exp_left)
+ from assms show "coprime a (b ^ m)"
+ by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
+qed
+
+end
+
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
- by (simp add: coprime_exp_nat ac_simps)
+ by (fact coprime_exp2)
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
- by (simp add: coprime_exp_int ac_simps)
+ by (fact coprime_exp2)
-lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
-proof (cases)
- assume "a = 0 & b = 0"
- thus ?thesis by simp
- next assume "~(a = 0 & b = 0)"
- hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
- by (auto simp:div_gcd_coprime_nat)
- hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
+lemma gcd_exp_nat:
+ "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0")
+ case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
+next
+ case False
+ then have "coprime (a div gcd a b) (b div gcd a b)"
+ by (auto simp: div_gcd_coprime)
+ then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+ by (simp add: coprime_exp2)
+ then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
@@ -1373,7 +1357,7 @@
with dc have th0: "a' dvd b*c"
using dvd_trans[of a' a "b*c"] by simp
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
- hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
+ hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
with z have th_1: "a' dvd b' * c" by auto
from coprime_dvd_mult_int[OF ab'(3)] th_1
have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
@@ -1471,10 +1455,10 @@
qed
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
- by (simp add: gcd.commute)
+ by (simp add: gcd.commute del: One_nat_def)
lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
- using coprime_plus_one_nat by (simp add: One_nat_def)
+ using coprime_plus_one_nat by simp
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
by (simp add: gcd.commute)
@@ -1850,7 +1834,7 @@
interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
- by standard simp_all
+ by standard (simp_all del: One_nat_def)
interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
@@ -1950,11 +1934,11 @@
lemma Lcm_nat_empty:
"Lcm {} = (1::nat)"
- by (simp add: Lcm_nat_def)
+ by (simp add: Lcm_nat_def del: One_nat_def)
lemma Lcm_nat_insert:
"Lcm (insert n M) = lcm (n::nat) (Lcm M)"
- by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
+ by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
definition
"Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -2107,7 +2091,7 @@
lemma mult_inj_if_coprime_nat:
"inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
\<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
-apply(auto simp add:inj_on_def)
+apply (auto simp add: inj_on_def simp del: One_nat_def)
apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
dvd.neq_le_trans dvd_triv_right mult.commute)
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jul 08 20:19:12 2015 +0200
@@ -794,15 +794,15 @@
lemma dvd_lcm_D1:
"lcm m n dvd k \<Longrightarrow> m dvd k"
- by (rule dvd_trans, rule lcm_dvd1, assumption)
+ by (rule dvd_trans, rule dvd_lcm1, assumption)
lemma dvd_lcm_D2:
"lcm m n dvd k \<Longrightarrow> n dvd k"
- by (rule dvd_trans, rule lcm_dvd2, assumption)
+ by (rule dvd_trans, rule dvd_lcm2, assumption)
lemma gcd_dvd_lcm [simp]:
"gcd a b dvd lcm a b"
- by (metis dvd_trans gcd_dvd2 lcm_dvd2)
+ using gcd_dvd2 by (rule dvd_lcmI2)
lemma lcm_1_iff:
"lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
@@ -830,14 +830,6 @@
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
by rule (auto intro: lcmI simp: lcm_least lcm_zero)
-lemma dvd_lcm_I1 [simp]:
- "k dvd m \<Longrightarrow> k dvd lcm m n"
- by (metis lcm_dvd1 dvd_trans)
-
-lemma dvd_lcm_I2 [simp]:
- "k dvd n \<Longrightarrow> k dvd lcm m n"
- by (metis lcm_dvd2 dvd_trans)
-
lemma lcm_coprime:
"gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
by (subst lcm_gcd) simp
@@ -874,8 +866,8 @@
assumes "a \<noteq> 0" and "b \<noteq> 0"
shows "euclidean_size a \<le> euclidean_size (lcm a b)"
proof -
- have "a dvd lcm a b" by (rule lcm_dvd1)
- then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
+ have "a dvd lcm a b" by (rule dvd_lcm1)
+ then obtain c where A: "lcm a b = a * c" ..
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
then show ?thesis by (subst A, intro size_mult_mono)
qed
@@ -905,12 +897,7 @@
lemma lcm_mult_unit1:
"is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
- apply (rule lcmI)
- apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
- apply (rule lcm_dvd2)
- apply (rule lcm_least, simp add: unit_simps, assumption)
- apply simp
- done
+ by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
lemma lcm_mult_unit2:
"is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
@@ -944,22 +931,11 @@
lemma lcm_left_idem:
"lcm a (lcm a b) = lcm a b"
- apply (rule lcmI)
- apply simp
- apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
- apply (rule lcm_least, assumption)
- apply (erule (1) lcm_least)
- apply (auto simp: lcm_zero)
- done
+ by (rule associated_eqI) simp_all
lemma lcm_right_idem:
"lcm (lcm a b) b = lcm a b"
- apply (rule lcmI)
- apply (subst lcm.assoc, rule lcm_dvd1)
- apply (rule lcm_dvd2)
- apply (rule lcm_least, erule (1) lcm_least, assumption)
- apply (auto simp: lcm_zero)
- done
+ by (rule associated_eqI) simp_all
lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
proof
@@ -1012,10 +988,10 @@
also note \<open>euclidean_size l = n\<close>
finally show "euclidean_size (gcd l l') \<le> n" .
qed
- ultimately have "euclidean_size l = euclidean_size (gcd l l')"
+ ultimately have *: "euclidean_size l = euclidean_size (gcd l l')"
by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
- with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
- using dvd_euclidean_size_eq_imp_dvd by auto
+ from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
+ by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
hence "l dvd l'" by (blast dest: dvd_gcd_D2)
}
--- a/src/HOL/Rings.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Rings.thy Wed Jul 08 20:19:12 2015 +0200
@@ -629,6 +629,44 @@
then show ?thesis by simp
qed
+lemma divide_1 [simp]:
+ "a div 1 = a"
+ using nonzero_mult_divide_cancel_left [of 1 a] by simp
+
+lemma dvd_times_left_cancel_iff [simp]:
+ assumes "a \<noteq> 0"
+ shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P then obtain d where "a * c = a * b * d" ..
+ with assms have "c = b * d" by (simp add: ac_simps)
+ then show ?Q ..
+next
+ assume ?Q then obtain d where "c = b * d" ..
+ then have "a * c = a * b * d" by (simp add: ac_simps)
+ then show ?P ..
+qed
+
+lemma dvd_times_right_cancel_iff [simp]:
+ assumes "a \<noteq> 0"
+ shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
+
+lemma div_dvd_iff_mult:
+ assumes "b \<noteq> 0" and "b dvd a"
+ shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
+proof -
+ from \<open>b dvd a\<close> obtain d where "a = b * d" ..
+ with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
+qed
+
+lemma dvd_div_iff_mult:
+ assumes "c \<noteq> 0" and "c dvd b"
+ shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
+proof -
+ from \<open>c dvd b\<close> obtain d where "b = c * d" ..
+ with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
+qed
+
end
class idom_divide = idom + semidom_divide
--- a/src/HOL/ex/Sqrt.thy Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/ex/Sqrt.thy Wed Jul 08 20:19:12 2015 +0200
@@ -18,7 +18,7 @@
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
- and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+ and "coprime m n" by (rule Rats_abs_nat_div_natE)
have eq: "m\<^sup>2 = p * n\<^sup>2"
proof -
from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
@@ -38,9 +38,8 @@
then have "p dvd n\<^sup>2" ..
with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
qed
- then have "p dvd gcd m n" ..
- with gcd have "p dvd 1" by simp
- then have "p \<le> 1" by (simp add: dvd_imp_le)
+ then have "p dvd gcd m n" by simp
+ with \<open>coprime m n\<close> have "p = 1" by simp
with p show False by simp
qed
@@ -64,7 +63,7 @@
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
- and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+ and "coprime m n" by (rule Rats_abs_nat_div_natE)
from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
by (auto simp add: power2_eq_square)
@@ -79,8 +78,7 @@
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 gcd have "p dvd 1" by simp
- then have "p \<le> 1" by (simp add: dvd_imp_le)
+ with \<open>coprime m n\<close> have "p = 1" by simp
with p show False by simp
qed