src/HOL/GCD.thy
changeset 32112 6da9c2a49fed
parent 32111 7c39fcfffd61
child 32415 1dddf2f64266
     1.1 --- a/src/HOL/GCD.thy	Tue Jul 21 11:01:07 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Jul 21 14:08:58 2009 +0200
     1.3 @@ -1507,6 +1507,252 @@
     1.4  lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
     1.5  by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
     1.6  
     1.7 +subsubsection {* The complete divisibility lattice *}
     1.8 +
     1.9 +
    1.10 +interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
    1.11 +proof
    1.12 +  case goal3 thus ?case by(metis gcd_unique_nat)
    1.13 +qed auto
    1.14 +
    1.15 +interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
    1.16 +proof
    1.17 +  case goal3 thus ?case by(metis lcm_unique_nat)
    1.18 +qed auto
    1.19 +
    1.20 +interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
    1.21 +
    1.22 +text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
    1.23 +GCD is defined via LCM to facilitate the proof that we have a complete lattice.
    1.24 +Later on we show that GCD and Gcd coincide on finite sets.
    1.25 +*}
    1.26 +context gcd
    1.27 +begin
    1.28 +
    1.29 +definition Gcd :: "'a set \<Rightarrow> 'a"
    1.30 +where "Gcd = fold gcd 0"
    1.31 +
    1.32 +definition Lcm :: "'a set \<Rightarrow> 'a"
    1.33 +where "Lcm = fold lcm 1"
    1.34 +
    1.35 +definition LCM :: "'a set \<Rightarrow> 'a" where
    1.36 +"LCM M = (if finite M then Lcm M else 0)"
    1.37 +
    1.38 +definition GCD :: "'a set \<Rightarrow> 'a" where
    1.39 +"GCD M = LCM(INT m:M. {d. d dvd m})"
    1.40 +
    1.41 +end
    1.42 +
    1.43 +lemma Gcd_empty[simp]: "Gcd {} = 0"
    1.44 +by(simp add:Gcd_def)
    1.45 +
    1.46 +lemma Lcm_empty[simp]: "Lcm {} = 1"
    1.47 +by(simp add:Lcm_def)
    1.48 +
    1.49 +lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
    1.50 +by(simp add:GCD_def LCM_def)
    1.51 +
    1.52 +lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
    1.53 +by(simp add:LCM_def)
    1.54 +
    1.55 +lemma Lcm_insert_nat [simp]:
    1.56 +  assumes "finite N"
    1.57 +  shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
    1.58 +proof -
    1.59 +  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.60 +    by (rule fun_left_comm_idem_lcm_nat)
    1.61 +  from assms show ?thesis by(simp add: Lcm_def)
    1.62 +qed
    1.63 +
    1.64 +lemma Lcm_insert_int [simp]:
    1.65 +  assumes "finite N"
    1.66 +  shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
    1.67 +proof -
    1.68 +  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
    1.69 +    by (rule fun_left_comm_idem_lcm_int)
    1.70 +  from assms show ?thesis by(simp add: Lcm_def)
    1.71 +qed
    1.72 +
    1.73 +lemma Gcd_insert_nat [simp]:
    1.74 +  assumes "finite N"
    1.75 +  shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
    1.76 +proof -
    1.77 +  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.78 +    by (rule fun_left_comm_idem_gcd_nat)
    1.79 +  from assms show ?thesis by(simp add: Gcd_def)
    1.80 +qed
    1.81 +
    1.82 +lemma Gcd_insert_int [simp]:
    1.83 +  assumes "finite N"
    1.84 +  shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
    1.85 +proof -
    1.86 +  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
    1.87 +    by (rule fun_left_comm_idem_gcd_int)
    1.88 +  from assms show ?thesis by(simp add: Gcd_def)
    1.89 +qed
    1.90 +
    1.91 +lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
    1.92 +by(induct rule:finite_ne_induct) auto
    1.93 +
    1.94 +lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
    1.95 +by (metis Lcm0_iff empty_iff)
    1.96 +
    1.97 +lemma Gcd_dvd_nat [simp]:
    1.98 +  assumes "finite M" and "(m::nat) \<in> M"
    1.99 +  shows "Gcd M dvd m"
   1.100 +proof -
   1.101 +  show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
   1.102 +qed
   1.103 +
   1.104 +lemma dvd_Gcd_nat[simp]:
   1.105 +  assumes "finite M" and "ALL (m::nat) : M. n dvd m"
   1.106 +  shows "n dvd Gcd M"
   1.107 +proof -
   1.108 +  show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
   1.109 +qed
   1.110 +
   1.111 +lemma dvd_Lcm_nat [simp]:
   1.112 +  assumes "finite M" and "(m::nat) \<in> M"
   1.113 +  shows "m dvd Lcm M"
   1.114 +proof -
   1.115 +  show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
   1.116 +qed
   1.117 +
   1.118 +lemma Lcm_dvd_nat[simp]:
   1.119 +  assumes "finite M" and "ALL (m::nat) : M. m dvd n"
   1.120 +  shows "Lcm M dvd n"
   1.121 +proof -
   1.122 +  show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
   1.123 +qed
   1.124 +
   1.125 +interpretation gcd_lcm_complete_lattice_nat:
   1.126 +  complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
   1.127 +proof
   1.128 +  case goal1 show ?case by simp
   1.129 +next
   1.130 +  case goal2 show ?case by simp
   1.131 +next
   1.132 +  case goal5 thus ?case by (auto simp: LCM_def)
   1.133 +next
   1.134 +  case goal6 thus ?case
   1.135 +    by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
   1.136 +next
   1.137 +  case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
   1.138 +next
   1.139 +  case goal4 thus ?case by(auto simp: LCM_def GCD_def)
   1.140 +qed
   1.141 +
   1.142 +text{* Alternative characterizations of Gcd and GCD: *}
   1.143 +
   1.144 +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.145 +apply(rule antisym)
   1.146 + apply(rule Max_ge)
   1.147 +  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   1.148 + apply simp
   1.149 +apply (rule Max_le_iff[THEN iffD2])
   1.150 +  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   1.151 + apply fastsimp
   1.152 +apply clarsimp
   1.153 +apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
   1.154 +done
   1.155 +
   1.156 +lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
   1.157 +apply(induct pred:finite)
   1.158 + apply simp
   1.159 +apply(case_tac "x=0")
   1.160 + apply simp
   1.161 +apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
   1.162 + apply simp
   1.163 +apply blast
   1.164 +done
   1.165 +
   1.166 +lemma Lcm_in_lcm_closed_set_nat:
   1.167 +  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
   1.168 +apply(induct rule:finite_linorder_min_induct)
   1.169 + apply simp
   1.170 +apply simp
   1.171 +apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
   1.172 + apply simp
   1.173 + apply(case_tac "A={}")
   1.174 +  apply simp
   1.175 + apply simp
   1.176 +apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
   1.177 +done
   1.178 +
   1.179 +lemma Lcm_eq_Max_nat:
   1.180 +  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M = Max M"
   1.181 +apply(rule antisym)
   1.182 + apply(rule Max_ge, assumption)
   1.183 + apply(erule (2) Lcm_in_lcm_closed_set_nat)
   1.184 +apply clarsimp
   1.185 +apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
   1.186 +done
   1.187 +
   1.188 +text{* Finally GCD is Gcd: *}
   1.189 +
   1.190 +lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
   1.191 +proof-
   1.192 +  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.193 +  show ?thesis
   1.194 +  proof cases
   1.195 +    assume "M={}" thus ?thesis by simp
   1.196 +  next
   1.197 +    assume "M\<noteq>{}"
   1.198 +    show ?thesis
   1.199 +    proof cases
   1.200 +      assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
   1.201 +    next
   1.202 +      assume "M\<noteq>{0}"
   1.203 +      with `M\<noteq>{}` assms show ?thesis
   1.204 +	apply(subst Gcd_remove0_nat[OF assms])
   1.205 +	apply(simp add:GCD_def)
   1.206 +	apply(subst divisors_remove0_nat)
   1.207 +	apply(simp add:LCM_def)
   1.208 +	apply rule
   1.209 +	 apply rule
   1.210 +	 apply(subst Gcd_eq_Max)
   1.211 +	    apply simp
   1.212 +	   apply blast
   1.213 +	  apply blast
   1.214 +	 apply(rule Lcm_eq_Max_nat)
   1.215 +	    apply simp
   1.216 +	   apply blast
   1.217 +	  apply fastsimp
   1.218 +	 apply clarsimp
   1.219 +	apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
   1.220 +	done
   1.221 +    qed
   1.222 +  qed
   1.223 +qed
   1.224 +
   1.225 +lemma Lcm_set_nat [code_unfold]:
   1.226 +  "Lcm (set ns) = foldl lcm (1::nat) ns"
   1.227 +proof -
   1.228 +  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
   1.229 +  show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
   1.230 +qed
   1.231 +
   1.232 +lemma Lcm_set_int [code_unfold]:
   1.233 +  "Lcm (set is) = foldl lcm (1::int) is"
   1.234 +proof -
   1.235 +  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
   1.236 +  show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
   1.237 +qed
   1.238 +
   1.239 +lemma Gcd_set_nat [code_unfold]:
   1.240 +  "Gcd (set ns) = foldl gcd (0::nat) ns"
   1.241 +proof -
   1.242 +  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
   1.243 +  show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
   1.244 +qed
   1.245 +
   1.246 +lemma Gcd_set_int [code_unfold]:
   1.247 +  "Gcd (set ns) = foldl gcd (0::int) ns"
   1.248 +proof -
   1.249 +  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
   1.250 +  show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
   1.251 +qed
   1.252 +
   1.253  
   1.254  subsection {* Primes *}
   1.255