src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 60436 77e694c0c919 parent 60433 720f210c5b1d child 60437 63edc650cf67
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 13 00:33:14 2015 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:52:48 2015 +0200
1.3 @@ -6,6 +6,29 @@
1.4  imports Complex_Main
1.5  begin
1.7 +context semidom_divide
1.8 +begin
1.9 +
1.10 +lemma mult_cancel_right [simp]:
1.11 +  "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
1.12 +proof (cases "c = 0")
1.13 +  case True then show ?thesis by simp
1.14 +next
1.15 +  case False
1.16 +  { assume "a * c = b * c"
1.17 +    then have "a * c div c = b * c div c"
1.18 +      by simp
1.19 +    with False have "a = b"
1.20 +      by simp
1.21 +  } then show ?thesis by auto
1.22 +qed
1.23 +
1.24 +lemma mult_cancel_left [simp]:
1.25 +  "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
1.26 +  using mult_cancel_right [of a c b] by (simp add: ac_simps)
1.27 +
1.28 +end
1.29 +
1.30  context semiring_div
1.31  begin
1.33 @@ -144,13 +167,7 @@
1.34  lemma unit_mult_left_cancel:
1.35    assumes "is_unit a"
1.36    shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
1.37 -proof
1.38 -  assume ?Q then show ?P by simp
1.39 -next
1.40 -  assume ?P then have "a * b div a = a * c div a" by simp
1.41 -  moreover from assms have "a \<noteq> 0" by auto
1.42 -  ultimately show ?Q by simp
1.43 -qed
1.44 +  using assms mult_cancel_left [of a b c] by auto
1.46  lemma unit_mult_right_cancel:
1.47    "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
1.48 @@ -217,34 +234,33 @@
1.49    "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
1.50    using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
1.52 -lemma associated_iff_div_unit:
1.53 -  "associated a b \<longleftrightarrow> (\<exists>c. is_unit c \<and> a = c * b)"
1.54 -proof
1.55 -  assume "associated a b"
1.56 -  show "\<exists>c. is_unit c \<and> a = c * b"
1.57 -  proof (cases "a = 0")
1.58 -    assume "a = 0"
1.59 -    then show "\<exists>c. is_unit c \<and> a = c * b" using `associated a b`
1.60 -        by (intro exI[of _ 1], simp add: associated_def)
1.61 -  next
1.62 -    assume [simp]: "a \<noteq> 0"
1.63 -    hence [simp]: "a dvd b" "b dvd a" using `associated a b`
1.64 -        unfolding associated_def by simp_all
1.65 -    hence "1 = a div b * (b div a)"
1.66 -      by (simp add: div_mult_swap)
1.67 -    hence "is_unit (a div b)" ..
1.68 -    moreover have "a = (a div b) * b" by simp
1.69 -    ultimately show ?thesis by blast
1.70 -  qed
1.71 -next
1.72 -  assume "\<exists>c. is_unit c \<and> a = c * b"
1.73 -  then obtain c where "is_unit c" and "a = c * b" by blast
1.74 -  hence "b = a * (1 div c)" by (simp add: algebra_simps)
1.75 -  hence "a dvd b" by simp
1.76 -  moreover from `a = c * b` have "b dvd a" by simp
1.77 -  ultimately show "associated a b" unfolding associated_def by simp
1.78 +lemma is_unit_associatedI:
1.79 +  assumes "is_unit c" and "a = c * b"
1.80 +  shows "associated a b"
1.81 +proof (rule associatedI)
1.82 +  from `a = c * b` show "b dvd a" by auto
1.83 +  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
1.84 +  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
1.85 +  ultimately have "b = a * d" by (simp add: ac_simps)
1.86 +  then show "a dvd b" ..
1.87  qed
1.89 +lemma associated_is_unitE:
1.90 +  assumes "associated a b"
1.91 +  obtains c where "is_unit c" and "a = c * b"
1.92 +proof (cases "b = 0")
1.93 +  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
1.94 +  with that show thesis .
1.95 +next
1.96 +  case False
1.97 +  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
1.98 +  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
1.99 +  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
1.100 +  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
1.101 +  then have "is_unit c" by auto
1.102 +  with `a = c * b` that show thesis by blast
1.103 +qed
1.105  lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
1.106    dvd_div_unit_iff unit_div_mult_swap unit_div_commute
1.107    unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
1.108 @@ -343,11 +359,12 @@
1.109      done
1.110    with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>c. is_unit c \<and> a = c * b"
1.111      by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
1.112 -  with associated_iff_div_unit show "associated a b" by simp
1.113 +  then obtain c where "is_unit c" and "a = c * b" by blast
1.114 +  then show "associated a b" by (rule is_unit_associatedI)
1.115  next
1.116    let ?nf = normalisation_factor
1.117    assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
1.118 -  with associated_iff_div_unit obtain c where "is_unit c" and "a = c * b" by blast
1.119 +  then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
1.120    then show "a div ?nf a = b div ?nf b"
1.121      apply (simp only: `a = c * b` normalisation_factor_mult normalisation_factor_unit)
1.122      apply (rule div_mult_mult1, force)