src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 60688 01488b559910 parent 60687 33dbbcb6a8a3 child 60690 a9e45c9588c3
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:40 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
1.3 @@ -228,16 +228,15 @@
1.4    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
1.5    by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
1.6
1.7 -lemma unit_factor_gcd [simp]:
1.8 -  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
1.9 -  by (induct a b rule: gcd_eucl_induct)
1.10 -    (auto simp add: gcd_0 gcd_non_0)
1.11 +lemma normalize_gcd [simp]:
1.12 +  "normalize (gcd a b) = gcd a b"
1.13 +  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_0 gcd_non_0)
1.14
1.15  lemma gcdI:
1.16    assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
1.17 -    and "unit_factor c = (if c = 0 then 0 else 1)"
1.18 +    and "normalize c = c"
1.19    shows "c = gcd a b"
1.20 -  by (rule associated_eqI) (auto simp: assms associated_def intro: gcd_greatest)
1.21 +  by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
1.22
1.23  sublocale gcd!: abel_semigroup gcd
1.24  proof
1.25 @@ -251,10 +250,10 @@
1.26      moreover have "gcd (gcd a b) c dvd c" by simp
1.27      ultimately show "gcd (gcd a b) c dvd gcd b c"
1.28        by (rule gcd_greatest)
1.29 -    show "unit_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
1.30 +    show "normalize (gcd (gcd a b) c) = gcd (gcd a b) c"
1.31        by auto
1.32      fix l assume "l dvd a" and "l dvd gcd b c"
1.33 -    with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
1.34 +    with dvd_trans [OF _ gcd_dvd1] and dvd_trans [OF _ gcd_dvd2]
1.35        have "l dvd b" and "l dvd c" by blast+
1.36      with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
1.37        by (intro gcd_greatest)
1.38 @@ -266,9 +265,9 @@
1.39  qed
1.40
1.41  lemma gcd_unique: "d dvd a \<and> d dvd b \<and>
1.42 -    unit_factor d = (if d = 0 then 0 else 1) \<and>
1.43 +    normalize d = d \<and>
1.44      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
1.45 -  by (rule, auto intro: gcdI simp: gcd_greatest)
1.46 +  by rule (auto intro: gcdI simp: gcd_greatest)
1.47
1.48  lemma gcd_dvd_prod: "gcd a b dvd k * b"
1.49    using mult_dvd_mono [of 1] by auto
1.50 @@ -378,10 +377,9 @@
1.51
1.52  lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
1.53    apply (rule gcdI)
1.54 +  apply simp_all
1.55    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
1.56 -  apply (rule gcd_dvd2)
1.57    apply (rule gcd_greatest, simp add: unit_simps, assumption)
1.58 -  apply (subst unit_factor_gcd, simp add: gcd_0)
1.59    done
1.60
1.61  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
1.62 @@ -461,7 +459,7 @@
1.63    with A show "gcd a b dvd c" by (rule dvd_trans)
1.64    have "gcd c d dvd d" by simp
1.65    with A show "gcd a b dvd d" by (rule dvd_trans)
1.66 -  show "unit_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
1.67 +  show "normalize (gcd a b) = gcd a b"
1.68      by simp
1.69    fix l assume "l dvd c" and "l dvd d"
1.70    hence "l dvd gcd c d" by (rule gcd_greatest)
1.71 @@ -484,22 +482,27 @@
1.72
1.73  lemma coprime_crossproduct:
1.74    assumes [simp]: "gcd a d = 1" "gcd b c = 1"
1.75 -  shows "associated (a * c) (b * d) \<longleftrightarrow> associated a b \<and> associated c d" (is "?lhs \<longleftrightarrow> ?rhs")
1.76 +  shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
1.77 +    (is "?lhs \<longleftrightarrow> ?rhs")
1.78  proof
1.79 -  assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
1.80 +  assume ?rhs
1.81 +  then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd)
1.82 +  then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+
1.83 +  then show ?lhs by (simp add: associated_iff_dvd)
1.84  next
1.85    assume ?lhs
1.86 -  from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left)
1.87 +  then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd)
1.88 +  then have "a dvd b * d" by (metis dvd_mult_left)
1.89    hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
1.90 -  moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
1.91 +  moreover from dvd have "b dvd a * c" by (metis dvd_mult_left)
1.92    hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
1.93 -  moreover from \<open>?lhs\<close> have "c dvd d * b"
1.94 -    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.95 +  moreover from dvd have "c dvd d * b"
1.96 +    by (auto dest: dvd_mult_right simp add: ac_simps)
1.97    hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.98 -  moreover from \<open>?lhs\<close> have "d dvd c * a"
1.99 -    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.100 +  moreover from dvd have "d dvd c * a"
1.101 +    by (auto dest: dvd_mult_right simp add: ac_simps)
1.102    hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.103 -  ultimately show ?rhs unfolding associated_def by simp
1.104 +  ultimately show ?rhs by (simp add: associated_iff_dvd)
1.105  qed
1.106
1.107  lemma gcd_add1 [simp]:
1.108 @@ -616,19 +619,29 @@
1.109    apply assumption
1.110    done
1.111
1.112 +lemma lcm_gcd:
1.113 +  "lcm a b = normalize (a * b) div gcd a b"
1.114 +  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
1.115 +
1.116 +subclass semiring_gcd
1.117 +  apply standard
1.118 +  using gcd_right_idem
1.119 +  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
1.120 +  done
1.121 +
1.122  lemma gcd_exp:
1.123 -  "gcd (a^n) (b^n) = (gcd a b) ^ n"
1.124 +  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
1.125  proof (cases "a = 0 \<and> b = 0")
1.126 -  assume "a = 0 \<and> b = 0"
1.127 -  then show ?thesis by (cases n, simp_all add: gcd_0_left)
1.128 +  case True
1.129 +  then show ?thesis by (cases n) simp_all
1.130  next
1.131 -  assume A: "\<not>(a = 0 \<and> b = 0)"
1.132 -  hence "1 = gcd ((a div gcd a b)^n) ((b div gcd a b)^n)"
1.133 -    using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime)
1.134 -  hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp
1.135 +  case False
1.136 +  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
1.137 +    using div_gcd_coprime by (subst sym) (auto simp: div_gcd_coprime)
1.138 +  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
1.139    also note gcd_mult_distrib
1.140 -  also have "unit_factor ((gcd a b)^n) = 1"
1.141 -    by (simp add: unit_factor_power A)
1.142 +  also have "unit_factor (gcd a b ^ n) = 1"
1.143 +    using False by (auto simp add: unit_factor_power unit_factor_gcd)
1.144    also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
1.145      by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
1.146    also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
1.147 @@ -749,16 +762,6 @@
1.148      by (simp add: ac_simps)
1.149  qed
1.150
1.151 -lemma lcm_gcd:
1.152 -  "lcm a b = normalize (a * b) div gcd a b"
1.153 -  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
1.154 -
1.155 -subclass semiring_gcd
1.156 -  apply standard
1.157 -  using gcd_right_idem
1.158 -  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
1.159 -  done
1.160 -
1.161  lemma lcm_gcd_prod:
1.162    "lcm a b * gcd a b = normalize (a * b)"
1.163    by (simp add: lcm_gcd)
1.164 @@ -783,9 +786,9 @@
1.165
1.166  lemma lcmI:
1.167    assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
1.168 -    and "unit_factor c = (if c = 0 then 0 else 1)"
1.169 +    and "normalize c = c"
1.170    shows "c = lcm a b"
1.171 -  by (rule associated_eqI) (auto simp: assms intro: associatedI lcm_least)
1.172 +  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
1.173
1.174  sublocale lcm!: abel_semigroup lcm ..
1.175
1.176 @@ -823,9 +826,9 @@
1.177
1.178  lemma lcm_unique:
1.179    "a dvd d \<and> b dvd d \<and>
1.180 -  unit_factor d = (if d = 0 then 0 else 1) \<and>
1.181 +  normalize d = d \<and>
1.182    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1.183 -  by (rule, auto intro: lcmI simp: lcm_least lcm_zero)
1.184 +  by rule (auto intro: lcmI simp: lcm_least lcm_zero)
1.185
1.186  lemma dvd_lcm_I1 [simp]:
1.187    "k dvd m \<Longrightarrow> k dvd lcm m n"
1.188 @@ -906,7 +909,7 @@
1.189    apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
1.190    apply (rule lcm_dvd2)
1.191    apply (rule lcm_least, simp add: unit_simps, assumption)
1.192 -  apply (subst unit_factor_lcm, simp add: lcm_zero)
1.193 +  apply simp
1.194    done
1.195
1.196  lemma lcm_mult_unit2:
1.197 @@ -1035,12 +1038,19 @@
1.198
1.199  lemma normalize_Lcm [simp]:
1.200    "normalize (Lcm A) = Lcm A"
1.201 -  by (cases "Lcm A = 0") (auto intro: associated_eqI)
1.202 +proof (cases "Lcm A = 0")
1.203 +  case True then show ?thesis by simp
1.204 +next
1.205 +  case False
1.206 +  have "unit_factor (Lcm A) * normalize (Lcm A) = Lcm A"
1.207 +    by (fact unit_factor_mult_normalize)
1.208 +  with False show ?thesis by simp
1.209 +qed
1.210
1.211  lemma LcmI:
1.212    assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
1.213 -    and "unit_factor b = (if b = 0 then 0 else 1)" shows "b = Lcm A"
1.214 -  by (rule associated_eqI) (auto simp: assms associated_def intro: Lcm_least)
1.215 +    and "normalize b = b" shows "b = Lcm A"
1.216 +  by (rule associated_eqI) (auto simp: assms intro: Lcm_least)
1.217
1.218  lemma Lcm_subset:
1.219    "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
1.220 @@ -1204,16 +1214,23 @@
1.221
1.222  lemma normalize_Gcd [simp]:
1.223    "normalize (Gcd A) = Gcd A"
1.224 -  by (cases "Gcd A = 0") (auto intro: associated_eqI)
1.225 +proof (cases "Gcd A = 0")
1.226 +  case True then show ?thesis by simp
1.227 +next
1.228 +  case False
1.229 +  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A"
1.230 +    by (fact unit_factor_mult_normalize)
1.231 +  with False show ?thesis by simp
1.232 +qed
1.233
1.234  subclass semiring_Gcd
1.235    by standard (simp_all add: Gcd_greatest)
1.236
1.237  lemma GcdI:
1.238    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"
1.239 -    and "unit_factor b = (if b = 0 then 0 else 1)"
1.240 +    and "normalize b = b"
1.241    shows "b = Gcd A"
1.242 -  by (rule associated_eqI) (auto simp: assms associated_def intro: Gcd_greatest)
1.243 +  by (rule associated_eqI) (auto simp: assms intro: Gcd_greatest)
1.244
1.245  lemma Lcm_Gcd:
1.246    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
```