merge Gcd/GCD and Lcm/LCM
authorhuffman
Tue Oct 25 12:00:52 2011 +0200 (2011-10-25)
changeset 452643b2c770f6631
parent 45263 93ac73160d78
child 45265 521508e85c0d
merge Gcd/GCD and Lcm/LCM
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Tue Oct 25 08:48:36 2011 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Oct 25 12:00:52 2011 +0200
     1.3 @@ -1460,8 +1460,7 @@
     1.4  by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
     1.5  
     1.6  
     1.7 -subsubsection {* The complete divisibility lattice *}
     1.8 -
     1.9 +subsection {* The complete divisibility lattice *}
    1.10  
    1.11  interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    1.12  proof
    1.13 @@ -1475,74 +1474,76 @@
    1.14  
    1.15  interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    1.16  
    1.17 -text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
    1.18 -GCD is defined via LCM to facilitate the proof that we have a complete lattice.
    1.19 -Later on we show that GCD and Gcd coincide on finite sets.
    1.20 +text{* Lifting gcd and lcm to sets (Gcd/Lcm).
    1.21 +Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
    1.22  *}
    1.23 -context gcd
    1.24 +
    1.25 +class Gcd = gcd +
    1.26 +  fixes Gcd :: "'a set \<Rightarrow> 'a"
    1.27 +  fixes Lcm :: "'a set \<Rightarrow> 'a"
    1.28 +
    1.29 +instantiation nat :: Gcd
    1.30  begin
    1.31  
    1.32 -definition Gcd :: "'a set \<Rightarrow> 'a"
    1.33 -where "Gcd = fold gcd 0"
    1.34 -
    1.35 -definition Lcm :: "'a set \<Rightarrow> 'a"
    1.36 -where "Lcm = fold lcm 1"
    1.37 +definition
    1.38 +  "Lcm (M::nat set) = (if finite M then fold lcm 1 M else 0)"
    1.39  
    1.40 -definition LCM :: "'a set \<Rightarrow> 'a" where
    1.41 -"LCM M = (if finite M then Lcm M else 0)"
    1.42 +definition
    1.43 +  "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
    1.44  
    1.45 -definition GCD :: "'a set \<Rightarrow> 'a" where
    1.46 -"GCD M = LCM(INT m:M. {d. d dvd m})"
    1.47 -
    1.48 +instance ..
    1.49  end
    1.50  
    1.51 -lemma Gcd_empty[simp]: "Gcd {} = 0"
    1.52 -by(simp add:Gcd_def)
    1.53 +lemma dvd_Lcm_nat [simp]:
    1.54 +  fixes M :: "nat set" assumes "m \<in> M" shows "m dvd Lcm M"
    1.55 +  using lcm_semilattice_nat.sup_le_fold_sup[OF _ assms, of 1]
    1.56 +  by (simp add: Lcm_nat_def)
    1.57  
    1.58 -lemma Lcm_empty[simp]: "Lcm {} = 1"
    1.59 -by(simp add:Lcm_def)
    1.60 +lemma Lcm_dvd_nat [simp]:
    1.61 +  fixes M :: "nat set" assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
    1.62 +proof (cases "n = 0")
    1.63 +  assume "n \<noteq> 0"
    1.64 +  hence "finite {d. d dvd n}" by (rule finite_divisors_nat)
    1.65 +  moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
    1.66 +  ultimately have "finite M" by (rule rev_finite_subset)
    1.67 +  thus ?thesis
    1.68 +    using lcm_semilattice_nat.fold_sup_le_sup [OF _ assms, of 1]
    1.69 +    by (simp add: Lcm_nat_def)
    1.70 +qed simp
    1.71  
    1.72 -lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
    1.73 -by(simp add:GCD_def LCM_def)
    1.74 +interpretation gcd_lcm_complete_lattice_nat:
    1.75 +  complete_lattice Gcd Lcm gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
    1.76 +proof
    1.77 +  case goal1 show ?case by simp
    1.78 +next
    1.79 +  case goal2 show ?case by simp
    1.80 +next
    1.81 +  case goal5 thus ?case by (rule dvd_Lcm_nat)
    1.82 +next
    1.83 +  case goal6 thus ?case by simp
    1.84 +next
    1.85 +  case goal3 thus ?case by (simp add: Gcd_nat_def)
    1.86 +next
    1.87 +  case goal4 thus ?case by (simp add: Gcd_nat_def)
    1.88 +qed
    1.89 +(* bh: This interpretation generates many lemmas about
    1.90 +"complete_lattice.SUPR Lcm" and "complete_lattice.INFI Gcd".
    1.91 +Should we define binder versions of LCM and GCD to correspond
    1.92 +with these? *)
    1.93  
    1.94 -lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
    1.95 -by(simp add:LCM_def)
    1.96 +lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
    1.97 +  by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
    1.98 +
    1.99 +lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
   1.100 +  by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
   1.101  
   1.102  lemma Lcm_insert_nat [simp]:
   1.103 -  assumes "finite N"
   1.104    shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   1.105 -proof -
   1.106 -  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
   1.107 -    by (rule comp_fun_idem_lcm_nat)
   1.108 -  from assms show ?thesis by(simp add: Lcm_def)
   1.109 -qed
   1.110 -
   1.111 -lemma Lcm_insert_int [simp]:
   1.112 -  assumes "finite N"
   1.113 -  shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.114 -proof -
   1.115 -  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
   1.116 -    by (rule comp_fun_idem_lcm_int)
   1.117 -  from assms show ?thesis by(simp add: Lcm_def)
   1.118 -qed
   1.119 +  by (fact gcd_lcm_complete_lattice_nat.Sup_insert)
   1.120  
   1.121  lemma Gcd_insert_nat [simp]:
   1.122 -  assumes "finite N"
   1.123    shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
   1.124 -proof -
   1.125 -  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
   1.126 -    by (rule comp_fun_idem_gcd_nat)
   1.127 -  from assms show ?thesis by(simp add: Gcd_def)
   1.128 -qed
   1.129 -
   1.130 -lemma Gcd_insert_int [simp]:
   1.131 -  assumes "finite N"
   1.132 -  shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
   1.133 -proof -
   1.134 -  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
   1.135 -    by (rule comp_fun_idem_gcd_int)
   1.136 -  from assms show ?thesis by(simp add: Gcd_def)
   1.137 -qed
   1.138 +  by (fact gcd_lcm_complete_lattice_nat.Inf_insert)
   1.139  
   1.140  lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
   1.141  by(induct rule:finite_ne_induct) auto
   1.142 @@ -1551,51 +1552,16 @@
   1.143  by (metis Lcm0_iff empty_iff)
   1.144  
   1.145  lemma Gcd_dvd_nat [simp]:
   1.146 -  assumes "finite M" and "(m::nat) \<in> M"
   1.147 -  shows "Gcd M dvd m"
   1.148 -proof -
   1.149 -  show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
   1.150 -qed
   1.151 +  fixes M :: "nat set"
   1.152 +  assumes "m \<in> M" shows "Gcd M dvd m"
   1.153 +  using assms by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
   1.154  
   1.155  lemma dvd_Gcd_nat[simp]:
   1.156 -  assumes "finite M" and "ALL (m::nat) : M. n dvd m"
   1.157 -  shows "n dvd Gcd M"
   1.158 -proof -
   1.159 -  show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
   1.160 -qed
   1.161 -
   1.162 -lemma dvd_Lcm_nat [simp]:
   1.163 -  assumes "finite M" and "(m::nat) \<in> M"
   1.164 -  shows "m dvd Lcm M"
   1.165 -proof -
   1.166 -  show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
   1.167 -qed
   1.168 +  fixes M :: "nat set"
   1.169 +  assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
   1.170 +  using assms by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
   1.171  
   1.172 -lemma Lcm_dvd_nat[simp]:
   1.173 -  assumes "finite M" and "ALL (m::nat) : M. m dvd n"
   1.174 -  shows "Lcm M dvd n"
   1.175 -proof -
   1.176 -  show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
   1.177 -qed
   1.178 -
   1.179 -interpretation gcd_lcm_complete_lattice_nat:
   1.180 -  complete_lattice GCD LCM gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
   1.181 -proof
   1.182 -  case goal1 show ?case by simp
   1.183 -next
   1.184 -  case goal2 show ?case by simp
   1.185 -next
   1.186 -  case goal5 thus ?case by (auto simp: LCM_def)
   1.187 -next
   1.188 -  case goal6 thus ?case
   1.189 -    by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
   1.190 -next
   1.191 -  case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
   1.192 -next
   1.193 -  case goal4 thus ?case by(auto simp: LCM_def GCD_def)
   1.194 -qed
   1.195 -
   1.196 -text{* Alternative characterizations of Gcd and GCD: *}
   1.197 +text{* Alternative characterizations of Gcd: *}
   1.198  
   1.199  lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
   1.200  apply(rule antisym)
   1.201 @@ -1641,71 +1607,13 @@
   1.202  apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
   1.203  done
   1.204  
   1.205 -text{* Finally GCD is Gcd: *}
   1.206 -
   1.207 -lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
   1.208 -proof-
   1.209 -  have divisors_remove0_nat: "(\<Inter>m\<in>M. {d::nat. d dvd m}) = (\<Inter>m\<in>M-{0}. {d::nat. d dvd m})" by auto
   1.210 -  show ?thesis
   1.211 -  proof cases
   1.212 -    assume "M={}" thus ?thesis by simp
   1.213 -  next
   1.214 -    assume "M\<noteq>{}"
   1.215 -    show ?thesis
   1.216 -    proof cases
   1.217 -      assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
   1.218 -    next
   1.219 -      assume "M\<noteq>{0}"
   1.220 -      with `M\<noteq>{}` assms show ?thesis
   1.221 -        apply(subst Gcd_remove0_nat[OF assms])
   1.222 -        apply(simp add:GCD_def)
   1.223 -        apply(subst divisors_remove0_nat)
   1.224 -        apply(simp add:LCM_def)
   1.225 -        apply rule
   1.226 -         apply rule
   1.227 -         apply(subst Gcd_eq_Max)
   1.228 -            apply simp
   1.229 -           apply blast
   1.230 -          apply blast
   1.231 -         apply(rule Lcm_eq_Max_nat)
   1.232 -            apply simp
   1.233 -           apply blast
   1.234 -          apply fastforce
   1.235 -         apply clarsimp
   1.236 -        apply(fastforce intro: finite_divisors_nat intro!: finite_INT)
   1.237 -        done
   1.238 -    qed
   1.239 -  qed
   1.240 -qed
   1.241 -
   1.242  lemma Lcm_set_nat [code_unfold]:
   1.243    "Lcm (set ns) = foldl lcm (1::nat) ns"
   1.244 -proof -
   1.245 -  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_lcm_nat)
   1.246 -  show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
   1.247 -qed
   1.248 -
   1.249 -lemma Lcm_set_int [code_unfold]:
   1.250 -  "Lcm (set is) = foldl lcm (1::int) is"
   1.251 -proof -
   1.252 -  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_lcm_int)
   1.253 -  show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
   1.254 -qed
   1.255 +  by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
   1.256  
   1.257  lemma Gcd_set_nat [code_unfold]:
   1.258    "Gcd (set ns) = foldl gcd (0::nat) ns"
   1.259 -proof -
   1.260 -  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_gcd_nat)
   1.261 -  show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
   1.262 -qed
   1.263 -
   1.264 -lemma Gcd_set_int [code_unfold]:
   1.265 -  "Gcd (set ns) = foldl gcd (0::int) ns"
   1.266 -proof -
   1.267 -  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_gcd_int)
   1.268 -  show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
   1.269 -qed
   1.270 -
   1.271 +  by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
   1.272  
   1.273  lemma mult_inj_if_coprime_nat:
   1.274    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
   1.275 @@ -1725,4 +1633,62 @@
   1.276  lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
   1.277  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
   1.278  
   1.279 +subsubsection {* Setwise gcd and lcm for integers *}
   1.280 +
   1.281 +instantiation int :: Gcd
   1.282 +begin
   1.283 +
   1.284 +definition
   1.285 +  "Lcm M = int (Lcm (nat ` abs ` M))"
   1.286 +
   1.287 +definition
   1.288 +  "Gcd M = int (Gcd (nat ` abs ` M))"
   1.289 +
   1.290 +instance ..
   1.291  end
   1.292 +
   1.293 +lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
   1.294 +  by (simp add: Lcm_int_def)
   1.295 +
   1.296 +lemma Gcd_empty_int [simp]: "Gcd {} = (0::int)"
   1.297 +  by (simp add: Gcd_int_def)
   1.298 +
   1.299 +lemma Lcm_insert_int [simp]:
   1.300 +  shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.301 +  by (simp add: Lcm_int_def lcm_int_def)
   1.302 +
   1.303 +lemma Gcd_insert_int [simp]:
   1.304 +  shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
   1.305 +  by (simp add: Gcd_int_def gcd_int_def)
   1.306 +
   1.307 +lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
   1.308 +  by (simp add: zdvd_int)
   1.309 +
   1.310 +lemma dvd_Lcm_int [simp]:
   1.311 +  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   1.312 +  using assms by (simp add: Lcm_int_def dvd_int_iff)
   1.313 +
   1.314 +lemma Lcm_dvd_int [simp]:
   1.315 +  fixes M :: "int set"
   1.316 +  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   1.317 +  using assms by (simp add: Lcm_int_def dvd_int_iff)
   1.318 +
   1.319 +lemma Gcd_dvd_int [simp]:
   1.320 +  fixes M :: "int set"
   1.321 +  assumes "m \<in> M" shows "Gcd M dvd m"
   1.322 +  using assms by (simp add: Gcd_int_def dvd_int_iff)
   1.323 +
   1.324 +lemma dvd_Gcd_int[simp]:
   1.325 +  fixes M :: "int set"
   1.326 +  assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
   1.327 +  using assms by (simp add: Gcd_int_def dvd_int_iff)
   1.328 +
   1.329 +lemma Lcm_set_int [code_unfold]:
   1.330 +  "Lcm (set xs) = foldl lcm (1::int) xs"
   1.331 +  by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
   1.332 +
   1.333 +lemma Gcd_set_int [code_unfold]:
   1.334 +  "Gcd (set xs) = foldl gcd (0::int) xs"
   1.335 +  by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
   1.336 +
   1.337 +end