--- a/src/HOL/GCD.thy Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/GCD.thy Tue Jul 21 14:08:58 2009 +0200
@@ -1507,6 +1507,252 @@
lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
+subsubsection {* The complete divisibility lattice *}
+
+
+interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
+proof
+ case goal3 thus ?case by(metis gcd_unique_nat)
+qed auto
+
+interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
+proof
+ case goal3 thus ?case by(metis lcm_unique_nat)
+qed auto
+
+interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
+
+text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
+GCD is defined via LCM to facilitate the proof that we have a complete lattice.
+Later on we show that GCD and Gcd coincide on finite sets.
+*}
+context gcd
+begin
+
+definition Gcd :: "'a set \<Rightarrow> 'a"
+where "Gcd = fold gcd 0"
+
+definition Lcm :: "'a set \<Rightarrow> 'a"
+where "Lcm = fold lcm 1"
+
+definition LCM :: "'a set \<Rightarrow> 'a" where
+"LCM M = (if finite M then Lcm M else 0)"
+
+definition GCD :: "'a set \<Rightarrow> 'a" where
+"GCD M = LCM(INT m:M. {d. d dvd m})"
+
+end
+
+lemma Gcd_empty[simp]: "Gcd {} = 0"
+by(simp add:Gcd_def)
+
+lemma Lcm_empty[simp]: "Lcm {} = 1"
+by(simp add:Lcm_def)
+
+lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
+by(simp add:GCD_def LCM_def)
+
+lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
+by(simp add:LCM_def)
+
+lemma Lcm_insert_nat [simp]:
+ assumes "finite N"
+ shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
+proof -
+ interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
+ by (rule fun_left_comm_idem_lcm_nat)
+ from assms show ?thesis by(simp add: Lcm_def)
+qed
+
+lemma Lcm_insert_int [simp]:
+ assumes "finite N"
+ shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
+proof -
+ interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
+ by (rule fun_left_comm_idem_lcm_int)
+ from assms show ?thesis by(simp add: Lcm_def)
+qed
+
+lemma Gcd_insert_nat [simp]:
+ assumes "finite N"
+ shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
+proof -
+ interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
+ by (rule fun_left_comm_idem_gcd_nat)
+ from assms show ?thesis by(simp add: Gcd_def)
+qed
+
+lemma Gcd_insert_int [simp]:
+ assumes "finite N"
+ shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
+proof -
+ interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
+ by (rule fun_left_comm_idem_gcd_int)
+ from assms show ?thesis by(simp add: Gcd_def)
+qed
+
+lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
+by(induct rule:finite_ne_induct) auto
+
+lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
+by (metis Lcm0_iff empty_iff)
+
+lemma Gcd_dvd_nat [simp]:
+ assumes "finite M" and "(m::nat) \<in> M"
+ shows "Gcd M dvd m"
+proof -
+ show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
+qed
+
+lemma dvd_Gcd_nat[simp]:
+ assumes "finite M" and "ALL (m::nat) : M. n dvd m"
+ shows "n dvd Gcd M"
+proof -
+ show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
+qed
+
+lemma dvd_Lcm_nat [simp]:
+ assumes "finite M" and "(m::nat) \<in> M"
+ shows "m dvd Lcm M"
+proof -
+ show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
+qed
+
+lemma Lcm_dvd_nat[simp]:
+ assumes "finite M" and "ALL (m::nat) : M. m dvd n"
+ shows "Lcm M dvd n"
+proof -
+ show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
+qed
+
+interpretation gcd_lcm_complete_lattice_nat:
+ complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
+proof
+ case goal1 show ?case by simp
+next
+ case goal2 show ?case by simp
+next
+ case goal5 thus ?case by (auto simp: LCM_def)
+next
+ case goal6 thus ?case
+ by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
+next
+ case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
+next
+ case goal4 thus ?case by(auto simp: LCM_def GCD_def)
+qed
+
+text{* Alternative characterizations of Gcd and GCD: *}
+
+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})"
+apply(rule antisym)
+ apply(rule Max_ge)
+ apply (metis all_not_in_conv finite_divisors_nat finite_INT)
+ apply simp
+apply (rule Max_le_iff[THEN iffD2])
+ apply (metis all_not_in_conv finite_divisors_nat finite_INT)
+ apply fastsimp
+apply clarsimp
+apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
+done
+
+lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
+apply(induct pred:finite)
+ apply simp
+apply(case_tac "x=0")
+ apply simp
+apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
+ apply simp
+apply blast
+done
+
+lemma Lcm_in_lcm_closed_set_nat:
+ "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
+apply(induct rule:finite_linorder_min_induct)
+ apply simp
+apply simp
+apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
+ apply simp
+ apply(case_tac "A={}")
+ apply simp
+ apply simp
+apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
+done
+
+lemma Lcm_eq_Max_nat:
+ "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"
+apply(rule antisym)
+ apply(rule Max_ge, assumption)
+ apply(erule (2) Lcm_in_lcm_closed_set_nat)
+apply clarsimp
+apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
+done
+
+text{* Finally GCD is Gcd: *}
+
+lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
+proof-
+ 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
+ show ?thesis
+ proof cases
+ assume "M={}" thus ?thesis by simp
+ next
+ assume "M\<noteq>{}"
+ show ?thesis
+ proof cases
+ assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
+ next
+ assume "M\<noteq>{0}"
+ with `M\<noteq>{}` assms show ?thesis
+ apply(subst Gcd_remove0_nat[OF assms])
+ apply(simp add:GCD_def)
+ apply(subst divisors_remove0_nat)
+ apply(simp add:LCM_def)
+ apply rule
+ apply rule
+ apply(subst Gcd_eq_Max)
+ apply simp
+ apply blast
+ apply blast
+ apply(rule Lcm_eq_Max_nat)
+ apply simp
+ apply blast
+ apply fastsimp
+ apply clarsimp
+ apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
+ done
+ qed
+ qed
+qed
+
+lemma Lcm_set_nat [code_unfold]:
+ "Lcm (set ns) = foldl lcm (1::nat) ns"
+proof -
+ interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
+ show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
+qed
+
+lemma Lcm_set_int [code_unfold]:
+ "Lcm (set is) = foldl lcm (1::int) is"
+proof -
+ interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
+ show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
+qed
+
+lemma Gcd_set_nat [code_unfold]:
+ "Gcd (set ns) = foldl gcd (0::nat) ns"
+proof -
+ interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
+ show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
+qed
+
+lemma Gcd_set_int [code_unfold]:
+ "Gcd (set ns) = foldl gcd (0::int) ns"
+proof -
+ interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
+ show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
+qed
+
subsection {* Primes *}