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}"