eliminated some duplication
authorhaftmann
Wed Jul 08 14:01:40 2015 +0200 (2015-07-08)
changeset 6068733dbbcb6a8a3
parent 60686 ea5bc46c11e6
child 60688 01488b559910
eliminated some duplication
src/HOL/GCD.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:39 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
     1.3 @@ -399,7 +399,7 @@
     1.4    by (rule dvd_0_left, rule Gcd_greatest) simp
     1.5  
     1.6  lemma Gcd_0_iff [simp]:
     1.7 -  "Gcd A = 0 \<longleftrightarrow> (\<forall>a\<in>A. a = 0)" (is "?P \<longleftrightarrow> ?Q")
     1.8 +  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
     1.9  proof
    1.10    assume ?P
    1.11    show ?Q
    1.12 @@ -407,7 +407,8 @@
    1.13      fix a
    1.14      assume "a \<in> A"
    1.15      then have "Gcd A dvd a" by (rule Gcd_dvd)
    1.16 -    with \<open>?P\<close> show "a = 0" by simp
    1.17 +    with \<open>?P\<close> have "a = 0" by simp
    1.18 +    then show "a \<in> {0}" by simp
    1.19    qed
    1.20  next
    1.21    assume ?Q
    1.22 @@ -415,7 +416,7 @@
    1.23    proof (rule Gcd_greatest)
    1.24      fix a
    1.25      assume "a \<in> A"
    1.26 -    with \<open>?Q\<close> have "a = 0" by simp
    1.27 +    with \<open>?Q\<close> have "a = 0" by auto
    1.28      then show "0 dvd a" by simp
    1.29    qed
    1.30    then show ?P by simp
    1.31 @@ -424,7 +425,7 @@
    1.32  lemma unit_factor_Gcd:
    1.33    "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
    1.34  proof (cases "Gcd A = 0")
    1.35 -  case True then show ?thesis by simp
    1.36 +  case True then show ?thesis by auto
    1.37  next
    1.38    case False
    1.39    from unit_factor_mult_normalize
    1.40 @@ -432,7 +433,7 @@
    1.41    then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
    1.42    then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
    1.43    with False have "unit_factor (Gcd A) = 1" by simp
    1.44 -  with False show ?thesis by simp
    1.45 +  with False show ?thesis by auto
    1.46  qed
    1.47  
    1.48  lemma Gcd_UNIV [simp]:
    1.49 @@ -473,7 +474,7 @@
    1.50    ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
    1.51      by (rule associatedI)
    1.52    then show ?thesis
    1.53 -    by (rule associated_eqI) (simp_all add: unit_factor_gcd unit_factor_Gcd)
    1.54 +    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
    1.55  qed
    1.56  
    1.57  lemma dvd_Gcd: -- \<open>FIXME remove\<close>
    1.58 @@ -509,7 +510,7 @@
    1.59    then have "associated (Gcd (normalize ` A)) (Gcd A)"
    1.60      by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
    1.61    then show ?thesis
    1.62 -    by (rule associated_eqI) (simp_all add: unit_factor_Gcd)
    1.63 +    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
    1.64  qed
    1.65  
    1.66  lemma Lcm_least:
     2.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:39 2015 +0200
     2.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:40 2015 +0200
     2.3 @@ -753,84 +753,19 @@
     2.4    "lcm a b = normalize (a * b) div gcd a b"
     2.5    by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
     2.6  
     2.7 +subclass semiring_gcd
     2.8 +  apply standard
     2.9 +  using gcd_right_idem
    2.10 +  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
    2.11 +  done
    2.12 +
    2.13  lemma lcm_gcd_prod:
    2.14    "lcm a b * gcd a b = normalize (a * b)"
    2.15    by (simp add: lcm_gcd)
    2.16  
    2.17 -lemma lcm_dvd1 [iff]:
    2.18 -  "a dvd lcm a b"
    2.19 -proof (cases "a*b = 0")
    2.20 -  assume "a * b \<noteq> 0"
    2.21 -  hence "gcd a b \<noteq> 0" by simp
    2.22 -  let ?c = "1 div unit_factor (a * b)"
    2.23 -  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (unit_factor (a * b))" by simp
    2.24 -  from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
    2.25 -    by (simp add: div_mult_swap unit_div_commute)
    2.26 -  hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
    2.27 -  with \<open>gcd a b \<noteq> 0\<close> have "lcm a b = a * ?c * b div gcd a b"
    2.28 -    by (subst (asm) div_mult_self2_is_id, simp_all)
    2.29 -  also have "... = a * (?c * b div gcd a b)"
    2.30 -    by (metis div_mult_swap gcd_dvd2 mult_assoc)
    2.31 -  finally show ?thesis by (rule dvdI)
    2.32 -qed (auto simp add: lcm_gcd)
    2.33 -
    2.34 -lemma lcm_least:
    2.35 -  "\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
    2.36 -proof (cases "k = 0")
    2.37 -  let ?nf = unit_factor
    2.38 -  assume "k \<noteq> 0"
    2.39 -  hence "is_unit (?nf k)" by simp
    2.40 -  hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
    2.41 -  assume A: "a dvd k" "b dvd k"
    2.42 -  hence "gcd a b \<noteq> 0" using \<open>k \<noteq> 0\<close> by auto
    2.43 -  from A obtain r s where ar: "k = a * r" and bs: "k = b * s" 
    2.44 -    unfolding dvd_def by blast
    2.45 -  with \<open>k \<noteq> 0\<close> have "r * s \<noteq> 0"
    2.46 -    by auto (drule sym [of 0], simp)
    2.47 -  hence "is_unit (?nf (r * s))" by simp
    2.48 -  let ?c = "?nf k div ?nf (r*s)"
    2.49 -  from \<open>is_unit (?nf k)\<close> and \<open>is_unit (?nf (r * s))\<close> have "is_unit ?c" by (rule unit_div)
    2.50 -  hence "?c \<noteq> 0" using not_is_unit_0 by fast 
    2.51 -  from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
    2.52 -    by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
    2.53 -  also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
    2.54 -    by (subst (3) \<open>k = a * r\<close>, subst (3) \<open>k = b * s\<close>, simp add: algebra_simps)
    2.55 -  also have "... = ?c * r*s * k * gcd a b" using \<open>r * s \<noteq> 0\<close>
    2.56 -    by (subst gcd_mult_distrib'[symmetric], simp add: algebra_simps unit_simps)
    2.57 -  finally have "(a*r) * (b*s) * gcd s r = ?c * k * r * s * gcd a b"
    2.58 -    by (subst ar[symmetric], subst bs[symmetric], simp add: mult_ac)
    2.59 -  hence "a * b * gcd s r * (r * s) = ?c * k * gcd a b * (r * s)"
    2.60 -    by (simp add: algebra_simps)
    2.61 -  hence "?c * k * gcd a b = a * b * gcd s r" using \<open>r * s \<noteq> 0\<close>
    2.62 -    by (metis div_mult_self2_is_id)
    2.63 -  also have "... = lcm a b * gcd a b * gcd s r * ?nf (a*b)"
    2.64 -    by (subst lcm_gcd_prod[of a b], metis gcd_mult_distrib gcd_mult_distrib') 
    2.65 -  also have "... = lcm a b * gcd s r * ?nf (a*b) * gcd a b"
    2.66 -    by (simp add: algebra_simps)
    2.67 -  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using \<open>gcd a b \<noteq> 0\<close>
    2.68 -    by (metis mult.commute div_mult_self2_is_id)
    2.69 -  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using \<open>?c \<noteq> 0\<close>
    2.70 -    by (metis div_mult_self2_is_id mult_assoc) 
    2.71 -  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using \<open>is_unit ?c\<close>
    2.72 -    by (simp add: unit_simps)
    2.73 -  finally show ?thesis by (rule dvdI)
    2.74 -qed simp
    2.75 -
    2.76  lemma lcm_zero:
    2.77    "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
    2.78 -proof -
    2.79 -  let ?nf = unit_factor
    2.80 -  {
    2.81 -    assume "a \<noteq> 0" "b \<noteq> 0"
    2.82 -    hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
    2.83 -    moreover from \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "gcd a b \<noteq> 0" by simp
    2.84 -    ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
    2.85 -  } moreover {
    2.86 -    assume "a = 0 \<or> b = 0"
    2.87 -    hence "lcm a b = 0" by (elim disjE, simp_all add: lcm_gcd)
    2.88 -  }
    2.89 -  ultimately show ?thesis by blast
    2.90 -qed
    2.91 +  by (fact lcm_eq_0_iff)
    2.92  
    2.93  lemmas lcm_0_iff = lcm_zero
    2.94  
    2.95 @@ -844,46 +779,15 @@
    2.96      by (metis nonzero_mult_divide_cancel_left)
    2.97  qed
    2.98  
    2.99 -lemma unit_factor_lcm [simp]:
   2.100 -  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   2.101 -  by (simp add: dvd_unit_factor_div lcm_gcd)
   2.102 -
   2.103 -lemma lcm_dvd2 [iff]: "b dvd lcm a b"
   2.104 -  using lcm_dvd1 [of b a] by (simp add: lcm_gcd ac_simps)
   2.105 +declare unit_factor_lcm [simp]
   2.106  
   2.107  lemma lcmI:
   2.108    assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   2.109      and "unit_factor c = (if c = 0 then 0 else 1)"
   2.110    shows "c = lcm a b"
   2.111 -  by (rule associated_eqI)
   2.112 -    (auto simp: assms associated_def intro: lcm_least, simp_all add: lcm_gcd)
   2.113 +  by (rule associated_eqI) (auto simp: assms intro: associatedI lcm_least)
   2.114  
   2.115 -sublocale lcm!: abel_semigroup lcm
   2.116 -proof
   2.117 -  fix a b c
   2.118 -  show "lcm (lcm a b) c = lcm a (lcm b c)"
   2.119 -  proof (rule lcmI)
   2.120 -    have "a dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
   2.121 -    then show "a dvd lcm (lcm a b) c" by (rule dvd_trans)
   2.122 -    
   2.123 -    have "b dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
   2.124 -    hence "b dvd lcm (lcm a b) c" by (rule dvd_trans)
   2.125 -    moreover have "c dvd lcm (lcm a b) c" by simp
   2.126 -    ultimately show "lcm b c dvd lcm (lcm a b) c" by (rule lcm_least)
   2.127 -
   2.128 -    fix l assume "a dvd l" and "lcm b c dvd l"
   2.129 -    have "b dvd lcm b c" by simp
   2.130 -    from this and \<open>lcm b c dvd l\<close> have "b dvd l" by (rule dvd_trans)
   2.131 -    have "c dvd lcm b c" by simp
   2.132 -    from this and \<open>lcm b c dvd l\<close> have "c dvd l" by (rule dvd_trans)
   2.133 -    from \<open>a dvd l\<close> and \<open>b dvd l\<close> have "lcm a b dvd l" by (rule lcm_least)
   2.134 -    from this and \<open>c dvd l\<close> show "lcm (lcm a b) c dvd l" by (rule lcm_least)
   2.135 -  qed (simp add: lcm_zero)
   2.136 -next
   2.137 -  fix a b
   2.138 -  show "lcm a b = lcm b a"
   2.139 -    by (simp add: lcm_gcd ac_simps)
   2.140 -qed
   2.141 +sublocale lcm!: abel_semigroup lcm ..
   2.142  
   2.143  lemma dvd_lcm_D1:
   2.144    "lcm m n dvd k \<Longrightarrow> m dvd k"
   2.145 @@ -913,13 +817,9 @@
   2.146    finally show "lcm a b = 1" .
   2.147  qed
   2.148  
   2.149 -lemma lcm_0_left [simp]:
   2.150 -  "lcm 0 a = 0"
   2.151 -  by (rule sym, rule lcmI, simp_all)
   2.152 -
   2.153 -lemma lcm_0 [simp]:
   2.154 +lemma lcm_0:
   2.155    "lcm a 0 = 0"
   2.156 -  by (rule sym, rule lcmI, simp_all)
   2.157 +  by (fact lcm_0_right)
   2.158  
   2.159  lemma lcm_unique:
   2.160    "a dvd d \<and> b dvd d \<and> 
   2.161 @@ -935,14 +835,6 @@
   2.162    "k dvd n \<Longrightarrow> k dvd lcm m n"
   2.163    by (metis lcm_dvd2 dvd_trans)
   2.164  
   2.165 -lemma lcm_1_left [simp]:
   2.166 -  "lcm 1 a = normalize a"
   2.167 -  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   2.168 -
   2.169 -lemma lcm_1_right [simp]:
   2.170 -  "lcm a 1 = normalize a"
   2.171 -  using lcm_1_left [of a] by (simp add: ac_simps)
   2.172 -
   2.173  lemma lcm_coprime:
   2.174    "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   2.175    by (subst lcm_gcd) simp
   2.176 @@ -1119,7 +1011,8 @@
   2.177        qed
   2.178        ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
   2.179          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
   2.180 -      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
   2.181 +      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
   2.182 +        using dvd_euclidean_size_eq_imp_dvd by auto
   2.183        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
   2.184      }
   2.185  
   2.186 @@ -1246,7 +1139,7 @@
   2.187    "Lcm (insert a A) = lcm a (Lcm A)"
   2.188  proof (rule lcmI)
   2.189    fix l assume "a dvd l" and "Lcm A dvd l"
   2.190 -  hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
   2.191 +  then have "\<forall>a\<in>A. a dvd l" by (auto intro: dvd_trans [of _ "Lcm A" l])
   2.192    with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_least)
   2.193  qed (auto intro: Lcm_least dvd_Lcm)
   2.194   
   2.195 @@ -1313,6 +1206,9 @@
   2.196    "normalize (Gcd A) = Gcd A"
   2.197    by (cases "Gcd A = 0") (auto intro: associated_eqI)
   2.198  
   2.199 +subclass semiring_Gcd
   2.200 +  by standard (simp_all add: Gcd_greatest)
   2.201 +
   2.202  lemma GcdI:
   2.203    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"
   2.204      and "unit_factor b = (if b = 0 then 0 else 1)"
   2.205 @@ -1323,28 +1219,12 @@
   2.206    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
   2.207    by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
   2.208  
   2.209 -lemma Gcd_0_iff:
   2.210 -  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
   2.211 -  apply (rule iffI)
   2.212 -  apply (rule subsetI, drule Gcd_dvd, simp)
   2.213 -  apply (auto intro: GcdI[symmetric])
   2.214 -  done
   2.215 -
   2.216 -lemma Gcd_empty [simp]:
   2.217 -  "Gcd {} = 0"
   2.218 -  by (simp add: Gcd_0_iff)
   2.219 +subclass semiring_Lcm
   2.220 +  by standard (simp add: Lcm_Gcd)
   2.221  
   2.222  lemma Gcd_1:
   2.223    "1 \<in> A \<Longrightarrow> Gcd A = 1"
   2.224 -  by (intro GcdI[symmetric]) (auto intro: Gcd_dvd dvd_Gcd)
   2.225 -
   2.226 -lemma Gcd_insert [simp]:
   2.227 -  "Gcd (insert a A) = gcd a (Gcd A)"
   2.228 -proof (rule gcdI)
   2.229 -  fix l assume "l dvd a" and "l dvd Gcd A"
   2.230 -  hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
   2.231 -  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd Gcd_greatest)
   2.232 -qed (auto intro: Gcd_greatest)
   2.233 +  by (auto intro!: Gcd_eq_1_I)
   2.234  
   2.235  lemma Gcd_finite:
   2.236    assumes "finite A"
   2.237 @@ -1357,22 +1237,10 @@
   2.238    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
   2.239  
   2.240  lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
   2.241 -  by (simp add: gcd_0)
   2.242 +  by simp
   2.243  
   2.244  lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
   2.245 -  by (simp add: gcd_0)
   2.246 -
   2.247 -subclass semiring_gcd
   2.248 -  apply standard
   2.249 -  using gcd_right_idem
   2.250 -  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
   2.251 -  done
   2.252 -
   2.253 -subclass semiring_Gcd
   2.254 -  by standard (simp_all add: Gcd_greatest)
   2.255 -
   2.256 -subclass semiring_Lcm
   2.257 -  by standard (simp add: Lcm_Gcd)
   2.258 +  by simp
   2.259  
   2.260  end
   2.261  
   2.262 @@ -1515,4 +1383,19 @@
   2.263  
   2.264  end
   2.265  
   2.266 +(*instance nat :: euclidean_semiring_gcd
   2.267 +proof (standard, auto intro!: ext)
   2.268 +  fix m n :: nat
   2.269 +  show *: "gcd m n = gcd_eucl m n"
   2.270 +  proof (induct m n rule: gcd_eucl_induct)
   2.271 +    case zero then show ?case by (simp add: gcd_eucl_0)
   2.272 +  next
   2.273 +    case (mod m n)
   2.274 +    with gcd_eucl_non_0 [of n m, symmetric]
   2.275 +    show ?case by (simp add: gcd_non_0_nat)
   2.276 +  qed
   2.277 +  show "lcm m n = lcm_eucl m n"
   2.278 +    by (simp add: lcm_eucl_def lcm_gcd * [symmetric] lcm_nat_def)
   2.279 +qed*)
   2.280 +
   2.281  end