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.4  
     1.5  subsection {* The complete divisibility lattice *}
     1.6  
     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.16  
    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.43  
    1.44  definition
    1.45    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
    1.46  
    1.47  instance ..
    1.48 +
    1.49  end
    1.50  
    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.63  
    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.79  
    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