# HG changeset patch # User haftmann # Date 1450946569 -3600 # Node ID b8e242e52c9717e4e24710440ca7744e7cbb9cf2 # Parent 8796d5edd29cad85d2ccb5b58b928c8e67ea0831 tuned proofs and augmented lemmas diff -r 8796d5edd29c -r b8e242e52c97 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Dec 24 12:50:12 2015 +0100 +++ b/src/HOL/GCD.thy Thu Dec 24 09:42:49 2015 +0100 @@ -445,17 +445,6 @@ "Gcd (set as) = foldr gcd as 0" by (induct as) simp_all -end - -class semiring_Lcm = semiring_Gcd + - assumes Lcm_Gcd: "Lcm A = Gcd {b. \a\A. a dvd b}" -begin - -lemma dvd_Lcm: - assumes "a \ A" - shows "a dvd Lcm A" - using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd) - lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A" proof - @@ -473,6 +462,17 @@ by (auto intro: associated_eqI) qed +end + +class semiring_Lcm = semiring_Gcd + + assumes Lcm_Gcd: "Lcm A = Gcd {b. \a\A. a dvd b}" +begin + +lemma dvd_Lcm: + assumes "a \ A" + shows "a dvd Lcm A" + using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd) + lemma Lcm_least: assumes "\b. b \ A \ b dvd a" shows "Lcm A dvd a" @@ -493,11 +493,38 @@ with False show ?thesis by simp qed - + +lemma Gcd_Lcm: + "Gcd A = Lcm {b. \a\A. b dvd a}" + by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) + lemma Lcm_empty [simp]: "Lcm {} = 1" by (simp add: Lcm_Gcd) +lemma Lcm_insert [simp]: + "Lcm (insert a A) = lcm a (Lcm A)" +proof (rule sym) + have "lcm a (Lcm A) dvd Lcm (insert a A)" + by (auto intro: dvd_Lcm Lcm_least) + moreover have "Lcm (insert a A) dvd lcm a (Lcm A)" + proof (rule Lcm_least) + fix b + assume "b \ insert a A" + then show "b dvd lcm a (Lcm A)" + proof + assume "b = a" then show ?thesis by simp + next + assume "b \ A" + then have "b dvd Lcm A" by (rule dvd_Lcm) + moreover have "Lcm A dvd lcm a (Lcm A)" by simp + ultimately show ?thesis by (blast intro: dvd_trans) + qed + qed + ultimately show "lcm a (Lcm A) = Lcm (insert a A)" + by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) +qed + lemma Lcm_1_iff [simp]: "Lcm A = 1 \ (\a\A. is_unit a)" (is "?P \ ?Q") proof @@ -521,15 +548,6 @@ by simp qed -lemma Lcm_UNIV [simp]: - "Lcm UNIV = 0" -proof - - have "0 dvd Lcm UNIV" - by (rule dvd_Lcm) simp - then show ?thesis - by simp -qed - lemma Lcm_eq_0_I: assumes "0 \ A" shows "Lcm A = 0" @@ -540,34 +558,21 @@ by simp qed -lemma Gcd_Lcm: - "Gcd A = Lcm {b. \a\A. b dvd a}" - by (rule associated_eqI) (auto intro: associatedI Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least - simp add: unit_factor_Gcd unit_factor_Lcm) +lemma Lcm_UNIV [simp]: + "Lcm UNIV = 0" + by (rule Lcm_eq_0_I) simp -lemma Lcm_insert [simp]: - "Lcm (insert a A) = lcm a (Lcm A)" -proof (rule sym) - have "lcm a (Lcm A) dvd Lcm (insert a A)" - by (auto intro: dvd_Lcm Lcm_least) - moreover have "Lcm (insert a A) dvd lcm a (Lcm A)" - proof (rule Lcm_least) - fix b - assume "b \ insert a A" - then show "b dvd lcm a (Lcm A)" - proof - assume "b = a" then show ?thesis by simp - next - assume "b \ A" - then have "b dvd Lcm A" by (rule dvd_Lcm) - moreover have "Lcm A dvd lcm a (Lcm A)" by simp - ultimately show ?thesis by (blast intro: dvd_trans) - qed - qed - ultimately show "lcm a (Lcm A) = Lcm (insert a A)" - by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) +lemma Lcm_0_iff: + assumes "finite A" + shows "Lcm A = 0 \ 0 \ A" +proof (cases "A = {}") + case True then show ?thesis by simp +next + case False with assms show ?thesis + by (induct A rule: finite_ne_induct) + (auto simp add: lcm_eq_0_iff) qed - + lemma Lcm_set [code_unfold]: "Lcm (set as) = foldr lcm as 1" by (induct as) simp_all @@ -1940,14 +1945,10 @@ instantiation nat :: Gcd begin -definition - "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)" - interpretation semilattice_neutr_set lcm "1::nat" .. -lemma Lcm_nat_infinite: - "\ finite M \ Lcm M = (0::nat)" - by (simp add: Lcm_nat_def) +definition + "Lcm (M::nat set) = (if finite M then F M else 0)" lemma Lcm_nat_empty: "Lcm {} = (1::nat)" @@ -1955,7 +1956,36 @@ lemma Lcm_nat_insert: "Lcm (insert n M) = lcm (n::nat) (Lcm M)" - by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def) + by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def) + +lemma Lcm_nat_infinite: + "infinite M \ Lcm M = (0::nat)" + by (simp add: Lcm_nat_def) + +lemma dvd_Lcm_nat [simp]: + fixes M :: "nat set" + assumes "m \ M" + shows "m dvd Lcm M" +proof - + from assms have "insert m M = M" by auto + moreover have "m dvd Lcm (insert m M)" + by (simp add: Lcm_nat_insert) + ultimately show ?thesis by simp +qed + +lemma Lcm_dvd_nat [simp]: + fixes M :: "nat set" + assumes "\m\M. m dvd n" + shows "Lcm M dvd n" +proof (cases "n = 0") + case True then show ?thesis by simp +next + case False + then have "finite {d. d dvd n}" by (rule finite_divisors_nat) + moreover have "M \ {d. d dvd n}" using assms by fast + ultimately have "finite M" by (rule rev_finite_subset) + then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert) +qed definition "Gcd (M::nat set) = Lcm {d. \m\M. d dvd m}" @@ -1964,27 +1994,21 @@ end -lemma dvd_Lcm_nat [simp]: - fixes M :: "nat set" - assumes "m \ M" - shows "m dvd Lcm M" -proof (cases "finite M") - case False then show ?thesis by (simp add: Lcm_nat_infinite) -next - case True then show ?thesis using assms by (induct M) (auto simp add: Lcm_nat_insert) -qed +instance nat :: semiring_Gcd +proof + show "Gcd N dvd n" if "n \ N" for N and n :: nat + using that by (induct N rule: infinite_finite_induct) + (auto simp add: Gcd_nat_def) + show "n dvd Gcd N" if "\m. m \ N \ n dvd m" for N and n :: nat + using that by (induct N rule: infinite_finite_induct) + (auto simp add: Gcd_nat_def) +qed simp -lemma Lcm_dvd_nat [simp]: - fixes M :: "nat set" - assumes "\m\M. m dvd n" - shows "Lcm M dvd n" -proof (cases "n = 0") - assume "n \ 0" - hence "finite {d. d dvd n}" by (rule finite_divisors_nat) - moreover have "M \ {d. d dvd n}" using assms by fast - ultimately have "finite M" by (rule rev_finite_subset) - then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert) -qed simp +instance nat :: semiring_Lcm +proof + show "Lcm N = Gcd {m. \n\N. n dvd m}" for N :: "nat set" + by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest) +qed interpretation gcd_lcm_complete_lattice_nat: complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" @@ -2002,42 +2026,6 @@ declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del] declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del] -instance nat :: semiring_Gcd -proof - show "Gcd N dvd n" if "n \ N" for N and n :: nat - using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower) -next - show "n dvd Gcd N" if "\m. m \ N \ n dvd m" for N and n :: nat - using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest) -next - show "normalize (Gcd N) = Gcd N" for N :: "nat set" - by simp -qed - -instance nat :: semiring_Lcm -proof - have uf: "unit_factor (Lcm N) = 1" if "0 < Lcm N" for N :: "nat set" - proof (cases "finite N") - case False with that show ?thesis by (simp add: Lcm_nat_infinite) - next - case True then show ?thesis - using that proof (induct N) - case empty then show ?case by simp - next - case (insert n N) - have "lcm n (Lcm N) \ 0 \ n \ 0 \ Lcm N \ 0" - using lcm_eq_0_iff [of n "Lcm N"] by simp - then have "lcm n (Lcm N) > 0 \ n > 0 \ Lcm N > 0" - unfolding neq0_conv . - with insert show ?case - by (simp add: Lcm_nat_insert unit_factor_lcm) - qed - qed - show "Lcm N = Gcd {m. \n\N. n dvd m}" for N :: "nat set" - by (rule associated_eqI) (auto intro!: associatedI Gcd_dvd Gcd_greatest - simp add: unit_factor_Gcd uf) -qed - lemma Lcm_empty_nat: "Lcm {} = (1::nat)" by (fact Lcm_empty) @@ -2051,8 +2039,10 @@ by (rule Lcm_eq_0_I) lemma Lcm0_iff [simp]: - "finite (M::nat set) \ M \ {} \ Lcm M = 0 \ 0 \ M" - by (induct rule: finite_ne_induct) auto + fixes M :: "nat set" + assumes "finite M" and "M \ {}" + shows "Lcm M = 0 \ 0 \ M" + using assms by (simp add: Lcm_0_iff) text\Alternative characterizations of Gcd:\