# HG changeset patch # User haftmann # Date 1455742318 -3600 # Node ID 7f927120b5a2f11fe728125e87e5a8cec4180216 # Parent 35a9e1cbb5b345cca9921973b58abd26151dfb6a dropped various legacy fact bindings and tuned proofs diff -r 35a9e1cbb5b3 -r 7f927120b5a2 NEWS --- a/NEWS Wed Feb 17 21:51:58 2016 +0100 +++ b/NEWS Wed Feb 17 21:51:58 2016 +0100 @@ -107,8 +107,32 @@ inj_int ~> inj_of_nat int_1 ~> of_nat_1 int_0 ~> of_nat_0 + Lcm_empty_nat ~> Lcm_empty + Lcm_empty_int ~> Lcm_empty + Lcm_insert_nat ~> Lcm_insert + Lcm_insert_int ~> Lcm_insert + comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd + comp_fun_idem_gcd_int ~> comp_fun_idem_gcd + comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm + comp_fun_idem_lcm_int ~> comp_fun_idem_lcm + Lcm_eq_0 ~> Lcm_eq_0_I + Lcm0_iff ~> Lcm_0_iff + Lcm_dvd_int ~> Lcm_least + divides_mult_nat ~> divides_mult + divides_mult_int ~> divides_mult + lcm_0_nat ~> lcm_0_right + lcm_0_int ~> lcm_0_right + lcm_0_left_nat ~> lcm_0_left + lcm_0_left_int ~> lcm_0_left + dvd_gcd_D1_nat ~> dvd_gcdD1 + dvd_gcd_D1_int ~> dvd_gcdD1 + dvd_gcd_D2_nat ~> dvd_gcdD2 + dvd_gcd_D2_int ~> dvd_gcdD2 + coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff + coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff realpow_minus_mult ~> power_minus_mult realpow_Suc_le_self ~> power_Suc_le_self + dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest INCOMPATIBILITY. diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Feb 17 21:51:58 2016 +0100 +++ b/src/HOL/GCD.thy Wed Feb 17 21:51:58 2016 +0100 @@ -585,10 +585,6 @@ (auto simp add: lcm_eq_0_iff) qed -lemma dvd_Gcd: \ \FIXME remove\ - "\b\A. a dvd b \ a dvd Gcd A" - by (blast intro: Gcd_greatest) - lemma Gcd_set [code_unfold]: "Gcd (set as) = foldr gcd as 0" by (induct as) simp_all @@ -715,16 +711,16 @@ lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y" by (simp add: gcd_int_def) -lemma abs_gcd_int[simp]: "\gcd (x::int) y\ = gcd x y" +lemma abs_gcd_int [simp]: "\gcd (x::int) y\ = gcd x y" by(simp add: gcd_int_def) lemma gcd_abs_int: "gcd (x::int) y = gcd \x\ \y\" by (simp add: gcd_int_def) -lemma gcd_abs1_int[simp]: "gcd \x\ (y::int) = gcd x y" +lemma gcd_abs1_int [simp]: "gcd \x\ (y::int) = gcd x y" by (metis abs_idempotent gcd_abs_int) -lemma gcd_abs2_int[simp]: "gcd x \y::int\ = gcd x y" +lemma gcd_abs2_int [simp]: "gcd x \y::int\ = gcd x y" by (metis abs_idempotent gcd_abs_int) lemma gcd_cases_int: @@ -751,10 +747,10 @@ lemma abs_lcm_int [simp]: "\lcm i j::int\ = lcm i j" by (simp add:lcm_int_def) -lemma lcm_abs1_int[simp]: "lcm \x\ (y::int) = lcm x y" +lemma lcm_abs1_int [simp]: "lcm \x\ (y::int) = lcm x y" by (metis abs_idempotent lcm_int_def) -lemma lcm_abs2_int[simp]: "lcm x \y::int\ = lcm x y" +lemma lcm_abs2_int [simp]: "lcm x \y::int\ = lcm x y" by (metis abs_idempotent lcm_int_def) lemma lcm_cases_int: @@ -1047,38 +1043,44 @@ (* to do: add the three variations of these, and for ints? *) -lemma finite_divisors_nat[simp]: - assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}" +lemma finite_divisors_nat [simp]: -- \FIXME move\ + fixes m :: nat + assumes "m > 0" + shows "finite {d. d dvd m}" proof- - have "finite{d. d <= m}" - by (blast intro: bounded_nat_set_is_finite) - from finite_subset[OF _ this] show ?thesis using assms - by (metis Collect_mono dvd_imp_le neq0_conv) + from assms have "{d. d dvd m} \ {d. d \ m}" + by (auto dest: dvd_imp_le) + then show ?thesis + using finite_Collect_le_nat by (rule finite_subset) qed -lemma finite_divisors_int[simp]: - assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" -proof- - have "{d. \d\ <= \i\} = {- \i\ .. \i\}" by(auto simp:abs_if) - hence "finite {d. \d\ <= \i\}" by simp - from finite_subset[OF _ this] show ?thesis using assms +lemma finite_divisors_int [simp]: + fixes i :: int + assumes "i \ 0" + shows "finite {d. d dvd i}" +proof - + have "{d. \d\ \ \i\} = {- \i\..\i\}" + by (auto simp: abs_if) + then have "finite {d. \d\ <= \i\}" + by simp + from finite_subset [OF _ this] show ?thesis using assms by (simp add: dvd_imp_le_int subset_iff) qed -lemma Max_divisors_self_nat[simp]: "n\0 \ Max{d::nat. d dvd n} = n" +lemma Max_divisors_self_nat [simp]: "n\0 \ Max{d::nat. d dvd n} = n" apply(rule antisym) apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) apply simp done -lemma Max_divisors_self_int[simp]: "n\0 \ Max{d::int. d dvd n} = \n\" +lemma Max_divisors_self_int [simp]: "n\0 \ Max{d::int. d dvd n} = \n\" apply(rule antisym) apply(rule Max_le_iff [THEN iffD2]) apply (auto intro: abs_le_D1 dvd_imp_le_int) done lemma gcd_is_Max_divisors_nat: - "m ~= 0 \ n ~= 0 \ gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" + "m > 0 \ n > 0 \ gcd (m::nat) n = Max {d. d dvd m \ d dvd n}" apply(rule Max_eqI[THEN sym]) apply (metis finite_Collect_conjI finite_divisors_nat) apply simp @@ -1438,35 +1440,33 @@ ultimately show ?thesis by blast qed -lemma pow_divides_eq_nat [simp]: "n ~= 0 \ ((a::nat)^n dvd b^n) = (a dvd b)" +lemma pow_divides_eq_nat [simp]: + "n > 0 \ (a::nat) ^ n dvd b ^ n \ a dvd b" by (auto intro: pow_divides_pow_nat dvd_power_same) -lemma pow_divides_eq_int [simp]: "n ~= 0 \ ((a::int)^n dvd b^n) = (a dvd b)" +lemma pow_divides_eq_int [simp]: + "n ~= 0 \ (a::int) ^ n dvd b ^ n \ a dvd b" by (auto intro: pow_divides_pow_int dvd_power_same) -lemma divides_mult_nat: - assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" - shows "m * n dvd r" +context semiring_gcd +begin + +lemma divides_mult: + assumes "a dvd c" and nr: "b dvd c" and "coprime a b" + shows "a * b dvd c" proof- - from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" - unfolding dvd_def by blast - from mr n' have "m dvd n'*n" by (simp add: mult.commute) - hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp - then obtain k where k: "n' = m*k" unfolding dvd_def by blast - from n' k show ?thesis unfolding dvd_def by auto + from \b dvd c\ obtain b' where"c = b * b'" .. + with \a dvd c\ have "a dvd b' * b" + by (simp add: ac_simps) + with \coprime a b\ have "a dvd b'" + by (simp add: coprime_dvd_mult_iff) + then obtain a' where "b' = a * a'" .. + with \c = b * b'\ have "c = (a * b) * a'" + by (simp add: ac_simps) + then show ?thesis .. qed -lemma divides_mult_int: - assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" - shows "m * n dvd r" -proof- - from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" - unfolding dvd_def by blast - from mr n' have "m dvd n'*n" by (simp add: mult.commute) - hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp - then obtain k where k: "n' = m*k" unfolding dvd_def by blast - from n' k show ?thesis unfolding dvd_def by auto -qed +end lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" by (simp add: gcd.commute del: One_nat_def) @@ -1773,18 +1773,6 @@ apply (simp, simp add: abs_mult) done -lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" - unfolding lcm_nat_def by simp - -lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" - unfolding lcm_int_def by simp - -lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0" - unfolding lcm_nat_def by simp - -lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" - unfolding lcm_int_def by simp - lemma lcm_pos_nat: "(m::nat) > 0 \ n>0 \ lcm m n > 0" by (metis gr0I mult_is_0 prod_gcd_lcm_nat) @@ -1796,7 +1784,7 @@ apply auto done -lemma dvd_pos_nat: +lemma dvd_pos_nat: -- \FIXME move\ fixes n m :: nat assumes "n > 0" and "m dvd n" shows "m > 0" @@ -1828,16 +1816,16 @@ lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \ lcm y x = \y\" by (subst lcm.commute, erule lcm_proj2_if_dvd_int) -lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \ n dvd m" +lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \ n dvd m" by (metis lcm_proj1_if_dvd_nat lcm_unique_nat) -lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \ m dvd n" +lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \ m dvd n" by (metis lcm_proj2_if_dvd_nat lcm_unique_nat) -lemma lcm_proj1_iff_int[simp]: "lcm m n = \m::int\ \ n dvd m" +lemma lcm_proj1_iff_int [simp]: "lcm m n = \m::int\ \ n dvd m" by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int) -lemma lcm_proj2_iff_int[simp]: "lcm m n = \n::int\ \ m dvd n" +lemma lcm_proj2_iff_int [simp]: "lcm m n = \n::int\ \ m dvd n" by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int) lemma (in semiring_gcd) comp_fun_idem_gcd: @@ -1848,10 +1836,12 @@ "comp_fun_idem lcm" by standard (simp_all add: fun_eq_iff ac_simps) -lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \ m=1 \ n=1" - by (simp only: lcm_eq_1_iff) simp +lemma lcm_1_iff_nat [simp]: + "lcm (m::nat) n = Suc 0 \ m = Suc 0 \ n = Suc 0" + using lcm_eq_1_iff [of m n] by simp -lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \ (m=1 \ m = -1) \ (n=1 \ n = -1)" +lemma lcm_1_iff_int [simp]: + "lcm (m::int) n = 1 \ (m=1 \ m = -1) \ (n=1 \ n = -1)" by auto @@ -1897,14 +1887,15 @@ 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 +proof (cases "n > 0") + case False then show ?thesis by simp next - case False + case True 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) + then show ?thesis using assms + by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert) qed definition @@ -1933,17 +1924,25 @@ text\Alternative characterizations of Gcd:\ -lemma Gcd_eq_Max: "finite(M::nat set) \ M \ {} \ 0 \ M \ Gcd M = Max(\m\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 add: Gcd_dvd) -apply (rule Max_le_iff[THEN iffD2]) - apply (metis all_not_in_conv finite_divisors_nat finite_INT) - apply fastforce -apply clarsimp -apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0) -done +lemma Gcd_eq_Max: + fixes M :: "nat set" + assumes "finite (M::nat set)" and "M \ {}" and "0 \ M" + shows "Gcd M = Max (\m\M. {d. d dvd m})" +proof (rule antisym) + from assms obtain m where "m \ M" and "m > 0" + by auto + from \m > 0\ have "finite {d. d dvd m}" + by (blast intro: finite_divisors_nat) + with \m \ M\ have fin: "finite (\m\M. {d. d dvd m})" + by blast + from fin show "Gcd M \ Max (\m\M. {d. d dvd m})" + by (auto intro: Max_ge Gcd_dvd) + from fin show "Max (\m\M. {d. d dvd m}) \ Gcd M" + apply (rule Max.boundedI) + apply auto + apply (meson Gcd_dvd Gcd_greatest \0 < m\ \m \ M\ dvd_imp_le dvd_pos_nat) + done +qed lemma Gcd_remove0_nat: "finite M \ Gcd M = Gcd (M - {0::nat})" apply(induct pred:finite) @@ -2088,7 +2087,7 @@ text \Fact aliasses\ -lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \ m = 0 \ n= 0" +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \ m = 0 \ n = 0" by (fact lcm_eq_0_iff) lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \ m = 0 \ n = 0" @@ -2103,17 +2102,9 @@ lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \ i dvd lcm m n" by (fact dvd_lcmI1) -lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \ i dvd lcm m n" +lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \ i dvd lcm m n" by (fact dvd_lcmI2) -lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \ - (k dvd m * n) = (k dvd m)" - by (fact coprime_dvd_mult_iff) - -lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \ - (k dvd m * n) = (k dvd m)" - by (fact coprime_dvd_mult_iff) - lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \ coprime (a^n) (b^m)" by (fact coprime_exp2) @@ -2122,29 +2113,13 @@ lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat] lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int] -lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat] -lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int] +lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat] +lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int] lemma dvd_Lcm_int [simp]: fixes M :: "int set" assumes "m \ M" shows "m dvd Lcm M" using assms by (fact dvd_Lcm) -lemma Lcm_empty_nat: - "Lcm {} = (1::nat)" - by (fact Lcm_empty) - -lemma Lcm_empty_int: - "Lcm {} = (1::int)" - by (fact Lcm_empty) - -lemma Lcm_insert_nat: - "Lcm (insert (n::nat) N) = lcm n (Lcm N)" - by (fact Lcm_insert) - -lemma Lcm_insert_int: - "Lcm (insert (n::int) N) = lcm n (Lcm N)" - by (fact Lcm_insert) - lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x" by (fact gcd_neg1_int) @@ -2159,43 +2134,8 @@ lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \ gcd x y = y" by (fact gcd_nat.absorb2) -lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\nat\nat)" - by (fact comp_fun_idem_gcd) - -lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\int\int)" - by (fact comp_fun_idem_gcd) - -lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\nat\nat)" - by (fact comp_fun_idem_lcm) - -lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\int\int)" - by (fact comp_fun_idem_lcm) - -lemma Lcm_eq_0 [simp]: - "finite (M::nat set) \ 0 \ M \ Lcm M = 0" - by (rule Lcm_eq_0_I) - -lemma Lcm0_iff [simp]: - fixes M :: "nat set" - assumes "finite M" and "M \ {}" - shows "Lcm M = 0 \ 0 \ M" - using assms by (simp add: Lcm_0_iff) - -lemma Lcm_dvd_int [simp]: - fixes M :: "int set" - assumes "\m\M. m dvd n" shows "Lcm M dvd n" - using assms by (auto intro: Lcm_least) - -lemma dvd_gcd_D1_nat: "k dvd gcd m n \ (k::nat) dvd m" - by (fact dvd_gcdD1) - -lemma dvd_gcd_D2_nat: "k dvd gcd m n \ (k::nat) dvd n" - by (fact dvd_gcdD2) - -lemma dvd_gcd_D1_int: "i dvd gcd m n \ (i::int) dvd m" - by (fact dvd_gcdD1) - -lemma dvd_gcd_D2_int: "i dvd gcd m n \ (i::int) dvd n" - by (fact dvd_gcdD2) +lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat] +lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat] +lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int] end diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Wed Feb 17 21:51:58 2016 +0100 +++ b/src/HOL/Number_Theory/Cong.thy Wed Feb 17 21:51:58 2016 +0100 @@ -267,7 +267,7 @@ lemma cong_mult_rcancel_int: "coprime k (m::int) \ [a * k = b * k] (mod m) = [a = b] (mod m)" - by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute) + by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute) lemma cong_mult_rcancel_nat: "coprime k (m::nat) \ [a * k = b * k] (mod m) = [a = b] (mod m)" @@ -285,7 +285,7 @@ lemma coprime_cong_mult_int: "[(a::int) = b] (mod m) \ [a = b] (mod n) \ coprime m n \ [a = b] (mod m * n)" -by (metis divides_mult_int cong_altdef_int) +by (metis divides_mult cong_altdef_int) lemma coprime_cong_mult_nat: assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:58 2016 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:58 2016 +0100 @@ -1064,11 +1064,11 @@ "Lcm {} = 1" by (simp add: Lcm_1_iff) -lemma Lcm_eq_0 [simp]: +lemma Lcm_eq_0_I [simp]: "0 \ A \ Lcm A = 0" by (drule dvd_Lcm) simp -lemma Lcm0_iff': +lemma Lcm_0_iff': "Lcm A = 0 \ \(\l. l \ 0 \ (\a\A. a dvd l))" proof assume "Lcm A = 0" @@ -1092,7 +1092,7 @@ qed qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) -lemma Lcm0_iff [simp]: +lemma Lcm_0_iff [simp]: "finite A \ Lcm A = 0 \ 0 \ A" proof - assume "finite A" @@ -1108,7 +1108,7 @@ done moreover from \finite A\ have "\a\A. a dvd \A" by blast ultimately have "\l. l \ 0 \ (\a\A. a dvd l)" by blast - with Lcm0_iff' have "Lcm A \ 0" by simp + with Lcm_0_iff' have "Lcm A \ 0" by simp } ultimately show "Lcm A = 0 \ 0 \ A" by blast qed @@ -1210,7 +1210,7 @@ lemma Lcm_Gcd: "Lcm A = Gcd {m. \a\A. a dvd m}" - by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest) + by (rule LcmI[symmetric]) (auto intro: Gcd_greatest Gcd_greatest) lemma Gcd_1: "1 \ A \ Gcd A = 1"