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.6  
     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.32  
    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.45  
    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.51  
    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.88  
    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.104 +  
   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)