src/HOL/GCD.thy
 changeset 51489 f738e6dbd844 parent 49962 a8cc904a6820 child 51547 604d73671fa7
1.1 --- a/src/HOL/GCD.thy	Sat Mar 23 17:11:06 2013 +0100
1.2 +++ b/src/HOL/GCD.thy	Sat Mar 23 20:50:39 2013 +0100
1.3 @@ -1462,6 +1462,10 @@
1.5  subsection {* The complete divisibility lattice *}
1.7 +lemma semilattice_neutr_set_lcm_one_nat:
1.8 +  "semilattice_neutr_set lcm (1::nat)"
1.9 +  by default simp_all
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    case goal3 thus ?case by(metis gcd_unique_nat)
1.14 @@ -1486,33 +1490,62 @@
1.15  begin
1.17  definition
1.18 -  "Lcm (M::nat set) = (if finite M then Finite_Set.fold lcm 1 M else 0)"
1.19 +  "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
1.20 +
1.21 +lemma Lcm_nat_infinite:
1.22 +  "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
1.23 +  by (simp add: Lcm_nat_def)
1.24 +
1.25 +lemma Lcm_nat_empty:
1.26 +  "Lcm {} = (1::nat)"
1.27 +proof -
1.28 +  interpret semilattice_neutr_set lcm "1::nat"
1.29 +    by (fact semilattice_neutr_set_lcm_one_nat)
1.30 +  show ?thesis by (simp add: Lcm_nat_def)
1.31 +qed
1.32 +
1.33 +lemma Lcm_nat_insert:
1.34 +  "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
1.35 +proof (cases "finite M")
1.36 +  interpret semilattice_neutr_set lcm "1::nat"
1.37 +    by (fact semilattice_neutr_set_lcm_one_nat)
1.38 +  case True
1.39 +  then show ?thesis by (simp add: Lcm_nat_def)
1.40 +next
1.41 +  case False then show ?thesis by (simp add: Lcm_nat_infinite)
1.42 +qed
1.44  definition
1.45    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
1.47  instance ..
1.48 +
1.49  end
1.51  lemma dvd_Lcm_nat [simp]:
1.52 -  fixes M :: "nat set" assumes "m \<in> M" shows "m dvd Lcm M"
1.53 -  using lcm_semilattice_nat.sup_le_fold_sup[OF _ assms, of 1]
1.54 -  by (simp add: Lcm_nat_def)
1.55 +  fixes M :: "nat set"
1.56 +  assumes "m \<in> M"
1.57 +  shows "m dvd Lcm M"
1.58 +proof (cases "finite M")
1.59 +  case False then show ?thesis by (simp add: Lcm_nat_infinite)
1.60 +next
1.61 +  case True then show ?thesis using assms by (induct M) (auto simp add: Lcm_nat_insert)
1.62 +qed
1.64  lemma Lcm_dvd_nat [simp]:
1.65 -  fixes M :: "nat set" assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
1.66 +  fixes M :: "nat set"
1.67 +  assumes "\<forall>m\<in>M. m dvd n"
1.68 +  shows "Lcm M dvd n"
1.69  proof (cases "n = 0")
1.70    assume "n \<noteq> 0"
1.71    hence "finite {d. d dvd n}" by (rule finite_divisors_nat)
1.72    moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
1.73    ultimately have "finite M" by (rule rev_finite_subset)
1.74 -  thus ?thesis
1.75 -    using lcm_semilattice_nat.fold_sup_le_sup [OF _ assms, of 1]
1.76 -    by (simp add: Lcm_nat_def)
1.77 +  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
1.78  qed simp
1.80  interpretation gcd_lcm_complete_lattice_nat:
1.81 -  complete_lattice Gcd Lcm gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
1.82 +  complete_lattice Gcd Lcm gcd "op dvd" "\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m" lcm 1 0
1.83  proof
1.84    case goal1 show ?case by simp
1.85  next