diff --git a/thys/Dirichlet_Series/Dirichlet_Misc.thy b/thys/Dirichlet_Series/Dirichlet_Misc.thy --- a/thys/Dirichlet_Series/Dirichlet_Misc.thy +++ b/thys/Dirichlet_Series/Dirichlet_Misc.thy @@ -1,159 +1,145 @@ (* File: Dirichlet_Misc.thy Author: Manuel Eberl, TU München *) section \Miscellaneous auxiliary facts\ theory Dirichlet_Misc imports - Main "HOL-Number_Theory.Number_Theory" begin lemma fixes a k :: nat assumes "a > 1" "k > 0" shows geometric_sum_nat_aux: "(a - 1) * (\iiiiiii n > 0 \ n div d > (0::nat)" - by (auto elim: dvdE) + by auto lemma Set_filter_insert: "Set.filter P (insert x A) = (if P x then insert x (Set.filter P A) else Set.filter P A)" - by (auto simp: Set.filter_def) + by auto lemma Set_filter_union: "Set.filter P (A \ B) = Set.filter P A \ Set.filter P B" - by (auto simp: Set.filter_def) + by auto lemma Set_filter_empty [simp]: "Set.filter P {} = {}" - by (auto simp: Set.filter_def) + by auto lemma Set_filter_image: "Set.filter P (f ` A) = f ` Set.filter (P \ f) A" - by (auto simp: Set.filter_def) + by auto lemma Set_filter_cong [cong]: "(\x. x \ A \ P x \ Q x) \ A = B \ Set.filter P A = Set.filter Q B" - by (auto simp: Set.filter_def) + by auto -lemma finite_Set_filter: "finite A \ finite (Set.filter P A)" - by (auto simp: Set.filter_def) - lemma inj_on_insert': "(\B. B \ A \ x \ B) \ inj_on (insert x) A" by (auto simp: inj_on_def insert_eq_iff) lemma assumes "finite A" "A \ {}" shows card_even_subset_aux: "card {B. B \ A \ even (card B)} = 2 ^ (card A - 1)" and card_odd_subset_aux: "card {B. B \ A \ odd (card B)} = 2 ^ (card A - 1)" and card_even_odd_subset: "card {B. B \ A \ even (card B)} = card {B. B \ A \ odd (card B)}" proof - from assms have *: "2 * card (Set.filter (even \ card) (Pow A)) = 2 ^ card A" proof (induction A rule: finite_ne_induct) case (singleton x) hence "Pow {x} = {{}, {x}}" by auto thus ?case by (simp add: Set_filter_insert) next case (insert x A) note fin = finite_subset[OF _ \finite A\] have "Pow (insert x A) = Pow A \ insert x ` Pow A" by (rule Pow_insert) have "Set.filter (even \ card) (Pow (insert x A)) = Set.filter (even \ card) (Pow A) \ insert x ` Set.filter (even \ card \ insert x) (Pow A)" unfolding Pow_insert Set_filter_union Set_filter_image by blast also have "Set.filter (even \ card \ insert x) (Pow A) = Set.filter (odd \ card) (Pow A)" unfolding o_def by (intro Set_filter_cong refl, subst card_insert_disjoint) (insert insert.hyps, auto dest: finite_subset) also have "card (Set.filter (even \ card) (Pow A) \ insert x ` \) = card (Set.filter (even \ card) (Pow A)) + card (insert x ` \)" (is "card (?A \ ?B) = _") - by (intro card_Un_disjoint finite_Set_filter finite_imageI) (auto simp: insert.hyps) + by (intro card_Un_disjoint finite_filter finite_imageI) (auto simp: insert.hyps) also have "card ?B = card (Set.filter (odd \ card) (Pow A))" using insert.hyps by (intro card_image inj_on_insert') auto also have "Set.filter (odd \ card) (Pow A) = Pow A - Set.filter (even \ card) (Pow A)" by auto also have "card \ = card (Pow A) - card (Set.filter (even \ card) (Pow A))" - using insert.hyps by (subst card_Diff_subset) (auto simp: finite_Set_filter) + using insert.hyps by (subst card_Diff_subset) (auto simp: finite_filter) also have "card (Set.filter (even \ card) (Pow A)) + \ = card (Pow A)" by (intro add_diff_inverse_nat, subst not_less, rule card_mono) (insert insert.hyps, auto) also have "2 * \ = 2 ^ card (insert x A)" using insert.hyps by (simp add: card_Pow) finally show ?case . qed from * show A: "card {B. B \ A \ even (card B)} = 2 ^ (card A - 1)" by (cases "card A") (simp_all add: Set.filter_def) have "Set.filter (odd \ card) (Pow A) = Pow A - Set.filter (even \ card) (Pow A)" by auto also have "2 * card \ = 2 * 2 ^ card A - 2 * card (Set.filter (even \ card) (Pow A))" - using assms by (subst card_Diff_subset) (auto intro!: finite_Set_filter simp: card_Pow) + using assms by (subst card_Diff_subset) (auto intro!: finite_filter simp: card_Pow) also note * also have "2 * 2 ^ card A - 2 ^ card A = (2 ^ card A :: nat)" by simp finally show B: "card {B. B \ A \ odd (card B)} = 2 ^ (card A - 1)" by (cases "card A") (simp_all add: Set.filter_def) from A and B show "card {B. B \ A \ even (card B)} = card {B. B \ A \ odd (card B)}" by simp qed lemma bij_betw_prod_divisors_coprime: assumes "coprime a (b :: nat)" shows "bij_betw (\x. fst x * snd x) ({d. d dvd a} \ {d. d dvd b}) {k. k dvd a * b}" unfolding bij_betw_def proof from assms show "inj_on (\x. fst x * snd x) ({d. d dvd a} \ {d. d dvd b})" by (auto simp: inj_on_def coprime_crossproduct_nat coprime_divisors) show "(\x. fst x * snd x) ` ({d. d dvd a} \ {d. d dvd b}) = {k. k dvd a * b}" proof safe fix x assume "x dvd a * b" then obtain b' c' where "x = b' * c'" "b' dvd a" "c' dvd b" using division_decomp by blast thus "x \ (\x. fst x * snd x) ` ({d. d dvd a} \ {d. d dvd b})" by force qed (insert assms, auto intro: mult_dvd_mono) qed lemma bij_betw_prime_power_divisors: assumes "prime (p :: nat)" shows "bij_betw ((^) p) {..k} {d. d dvd p ^ k}" unfolding bij_betw_def proof from assms have *: "p > 1" by (simp add: prime_gt_Suc_0_nat) show "inj_on ((^) p) {..k}" using assms by (auto simp: inj_on_def prime_gt_Suc_0_nat power_inject_exp[OF *]) show "(^) p ` {..k} = {d. d dvd p ^ k}" using assms by (auto simp: le_imp_power_dvd divides_primepow_nat) qed -lemma power_diff': - assumes "m \ n" "x \ 0" - shows "x ^ (m - n) = (x ^ m div x ^ n :: 'a :: unique_euclidean_semiring)" -proof - - from assms have "x ^ m = x ^ (m - n) * x ^ n" - by (subst power_add [symmetric]) simp - also from assms have "\ div x ^ n = x ^ (m - n)" by simp - finally show ?thesis .. -qed - lemma sum_divisors_coprime_mult: assumes "coprime a (b :: nat)" shows "(\d | d dvd a * b. f d) = (\r | r dvd a. \s | s dvd b. f (r * s))" proof - have "(\r | r dvd a. \s | s dvd b. f (r * s)) = (\z\{r. r dvd a} \ {s. s dvd b}. f (fst z * snd z))" by (subst sum.cartesian_product) (simp add: case_prod_unfold) also have "\ = (\d | d dvd a * b. f d)" by (intro sum.reindex_bij_betw bij_betw_prod_divisors_coprime assms) finally show ?thesis .. qed end diff --git a/thys/Dirichlet_Series/Dirichlet_Product.thy b/thys/Dirichlet_Series/Dirichlet_Product.thy --- a/thys/Dirichlet_Series/Dirichlet_Product.thy +++ b/thys/Dirichlet_Series/Dirichlet_Product.thy @@ -1,552 +1,552 @@ (* File: Dirichlet_Product.thy Author: Manuel Eberl, TU München *) section \Dirichlet convolution\ theory Dirichlet_Product imports Complex_Main Multiplicative_Function begin lemma sum_coprime_dvd_cong: "(\r | r dvd a. \s | s dvd b. f r s) = (\r | r dvd a. \s | s dvd b. g r s)" if "coprime a b" "\r s. coprime r s \ r dvd a \ s dvd b \ f r s = g r s" -using refl proof (rule sum.cong, rule sum.cong) +proof (intro sum.cong) fix r s assume "r \ {r. r dvd a}" and "s \ {s. s dvd b}" then have "r dvd a" and "s dvd b" by simp_all moreover from \coprime a b\ have "coprime r s" using \r dvd a\ \s dvd b\ by (auto intro: coprime_imp_coprime dvd_trans) ultimately show "f r s = g r s" using that by simp -qed +qed auto definition dirichlet_prod :: "(nat \ 'a :: semiring_0) \ (nat \ 'a) \ nat \ 'a" where "dirichlet_prod f g = (\n. \d | d dvd n. f d * g (n div d))" lemma sum_divisors_code: assumes "n > (0::nat)" shows "(\d | d dvd n. f d) = fold_atLeastAtMost_nat (\d acc. if d dvd n then f d + acc else acc) 1 n 0" proof - have "(\d acc. if d dvd n then f d + acc else acc) = (\d acc. (if d dvd n then f d else 0) + acc)" by (simp add: fun_eq_iff) hence "fold_atLeastAtMost_nat (\d acc. if d dvd n then f d + acc else acc) 1 n 0 = fold_atLeastAtMost_nat (\d acc. (if d dvd n then f d else 0) + acc) 1 n 0" by (simp only: ) also have "\ = (\d = 1..n. if d dvd n then f d else 0)" by (rule sum_atLeastAtMost_code [symmetric]) also from assms have "\ = (\d | d dvd n. f d)" by (intro sum.mono_neutral_cong_right) (auto elim: dvdE dest: dvd_imp_le) finally show ?thesis .. qed lemma dirichlet_prod_code [code]: "dirichlet_prod f g n = (if n = 0 then 0 else fold_atLeastAtMost_nat (\d acc. if d dvd n then f d * g (n div d) + acc else acc) 1 n 0)" unfolding dirichlet_prod_def by (simp add: sum_divisors_code) lemma dirichlet_prod_0 [simp]: "dirichlet_prod f g 0 = 0" by (simp add: dirichlet_prod_def) lemma dirichlet_prod_Suc_0 [simp]: "dirichlet_prod f g (Suc 0) = f (Suc 0) * g (Suc 0)" by (simp add: dirichlet_prod_def) lemma dirichlet_prod_cong [cong]: assumes "(\n. n > 0 \ f n = f' n)" "(\n. n > 0 \ g n = g' n)" shows "dirichlet_prod f g = dirichlet_prod f' g'" proof fix n :: nat show "dirichlet_prod f g n = dirichlet_prod f' g' n" proof (cases "n = 0") case False with assms show ?thesis unfolding dirichlet_prod_def by (intro ext sum.cong refl) (auto elim!: dvdE) qed simp_all qed lemma dirichlet_prod_altdef1: "dirichlet_prod f g = (\n. \d | d dvd n. f (n div d) * g d)" proof fix n :: nat show "dirichlet_prod f g n = (\d | d dvd n. f (n div d) * g d)" proof (cases "n = 0") case False hence "dirichlet_prod f g n = (\d | d dvd n. f (n div (n div d)) * g (n div d))" unfolding dirichlet_prod_def by (intro sum.cong refl) (auto elim!: dvdE) also from False have "\ = (\d | d dvd n. f (n div d) * g d)" by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim!: dvdE) finally show ?thesis . qed simp qed lemma dirichlet_prod_altdef2: "dirichlet_prod f g = (\n. \(r,d) | r * d = n. f r * g d)" proof fix n show "dirichlet_prod f g n = (\(r,d) | r * d = n. f r * g d)" proof (cases "n = 0") case True have "(\n::nat. (0, n)) ` UNIV \ {(r,d). r * d = 0}" by auto moreover have "\finite ((\n::nat. (0, n)) ` UNIV)" by (subst finite_image_iff) (auto simp: inj_on_def) ultimately have "infinite {(r,d). r * d = (0::nat)}" by (blast dest: finite_subset) with True show ?thesis by simp next case False have "(\d | d dvd n. f d * g (n div d)) = (\r | r dvd n. (\d | d = n div r. f r * g d))" by (intro sum.cong refl) auto also from False have "\ = (\(r,d)\(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)" by (intro sum.Sigma) auto also from False have "(SIGMA x:{r. r dvd n}. {d. d = n div x}) = {(r,d). r * d = n}" by auto finally show ?thesis by (simp add: dirichlet_prod_def) qed qed lemma dirichlet_prod_commutes: "dirichlet_prod (f :: nat \ 'a :: comm_semiring_0) g = dirichlet_prod g f" proof fix n :: nat show "dirichlet_prod f g n = dirichlet_prod g f n" proof (cases "n = 0") case False have "(\(r,d) | r * d = n. f r * g d) = (\(d,r) | r * d = n. f r * g d)" by (rule sum.reindex_bij_witness [of _ "\(x,y). (y,x)" "\(x,y). (y,x)"]) auto thus ?thesis by (simp add: dirichlet_prod_altdef2 mult.commute) qed (simp add: dirichlet_prod_def) qed lemma finite_divisors_nat': "n > (0 :: nat) \ finite {(a,b). a * b = n}" by (rule finite_subset[of _ "{0<..n} \ {0<..n}"]) auto lemma dirichlet_prod_assoc_aux1: assumes "n > 0" shows "dirichlet_prod f (dirichlet_prod g h) n = (\(a, b, c)\{(a, b, c). a * b * c = n}. f a * g b * h c)" proof - have "dirichlet_prod f (dirichlet_prod g h) n = (\x\{(a,b). a * b = n}. (\(c,d) | c * d = snd x. f (fst x) * g c * h d))" by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_left mult.assoc) also from assms have "\ = (\x\(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}). case x of (x, c, d) \ f (fst x) * g c * h d)" by (intro sum.Sigma finite_divisors_nat' ballI) auto also have "\ = (\(a,b,c) | a * b * c = n. f a * g b * h c)" by (rule sum.reindex_bij_witness [of _ "\(a,b,c). ((a, b*c), (b,c))" "\((a,b),(c,d)). (a, c, d)"]) (auto simp: mult_ac) finally show ?thesis . qed lemma dirichlet_prod_assoc_aux2: assumes "n > 0" shows "dirichlet_prod (dirichlet_prod f g) h n = (\(a, b, c)\{(a, b, c). a * b * c = n}. f a * g b * h c)" proof - have "dirichlet_prod (dirichlet_prod f g) h n = (\x\{(a,b). a * b = n}. (\(c,d) | c * d = fst x. f c * g d * h (snd x)))" by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_right mult.assoc) also from assms have "\ = (\x\(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}). case x of (x, c, d) \ f c * g d * h (snd x))" by (intro sum.Sigma finite_divisors_nat' ballI) auto also have "\ = (\(a,b,c) | a * b * c = n. f a * g b * h c)" by (rule sum.reindex_bij_witness [of _ "\(a,b,c). ((a*b, c), (a,b))" "\((a,b),(c,d)). (c, d, b)"]) (auto simp: mult_ac) finally show ?thesis . qed lemma dirichlet_prod_assoc: "dirichlet_prod (dirichlet_prod f g) h = dirichlet_prod f (dirichlet_prod g h)" proof fix n :: nat show "dirichlet_prod (dirichlet_prod f g) h n = dirichlet_prod f (dirichlet_prod g h) n" by (cases "n = 0") (simp_all add: dirichlet_prod_assoc_aux1 dirichlet_prod_assoc_aux2) qed lemma dirichlet_prod_const_right [simp]: assumes "n > 0" shows "dirichlet_prod f (\n. if n = Suc 0 then c else 0) n = f n * c" proof - have "dirichlet_prod f (\n. if n = Suc 0 then c else 0) n = (\d | d dvd n. (if d = n then f n * c else 0))" unfolding dirichlet_prod_def using assms by (intro sum.cong refl) (auto elim!: dvdE split: if_splits) also have "\ = f n * c" using assms by (subst sum.delta) auto finally show ?thesis . qed lemma dirichlet_prod_const_left [simp]: assumes "n > 0" shows "dirichlet_prod (\n. if n = Suc 0 then c else 0) g n = c * g n" proof - have "dirichlet_prod (\n. if n = Suc 0 then c else 0) g n = (\d | d dvd n. (if d = 1 then c * g n else 0))" unfolding dirichlet_prod_def using assms by (intro sum.cong refl) (auto elim!: dvdE split: if_splits) also have "\ = c * g n" using assms by (subst sum.delta) auto finally show ?thesis . qed fun dirichlet_inverse :: "(nat \ 'a :: comm_ring_1) \ 'a \ nat \ 'a" where "dirichlet_inverse f i n = (if n = 0 then 0 else if n = 1 then i else -i * (\d | d dvd n \ d < n. f (n div d) * dirichlet_inverse f i d))" lemma dirichlet_inverse_induct [case_names 0 1 gt1]: "P 0 \ P (Suc 0) \ (\n. n > 1 \ (\k. k < n \ P k) \ P n) \ P n" by induction_schema (force, rule wf_measure [of id], simp) lemma dirichlet_inverse_0 [simp]: "dirichlet_inverse f i 0 = 0" by simp lemma dirichlet_inverse_Suc_0 [simp]: "dirichlet_inverse f i (Suc 0) = i" by simp declare dirichlet_inverse.simps [simp del] lemma dirichlet_inverse_gt_1: "n > 1 \ dirichlet_inverse f i n = -i * (\d | d dvd n \ d < n. f (n div d) * dirichlet_inverse f i d)" by (simp add: dirichlet_inverse.simps) lemma dirichlet_inverse_cong [cong]: assumes "\n. n > 0 \ f n = f' n" "i = i'" "n = n'" shows "dirichlet_inverse f i n = dirichlet_inverse f' i' n'" proof - have "dirichlet_inverse f i n = dirichlet_inverse f' i n" using assms(1) proof (induction n rule: dirichlet_inverse_induct) case (gt1 n) have *: "dirichlet_inverse f i k = dirichlet_inverse f' i k" if "k dvd n \ k < n" for k using that by (intro gt1) auto have *: "(\d | d dvd n \ d < n. f (n div d) * dirichlet_inverse f i d) = (\d | d dvd n \ d < n. f' (n div d) * dirichlet_inverse f' i d)" by (intro sum.cong refl) (subst gt1.prems, auto elim: dvdE simp: *) consider "n = 0" | "n = 1" | "n > 1" by force thus ?case by cases (insert *, simp_all add: dirichlet_inverse_gt_1 * cong: sum.cong) qed auto with assms(2,3) show ?thesis by simp qed lemma dirichlet_inverse_gt_1': assumes "n > 1" shows "dirichlet_inverse f i n = -i * dirichlet_prod (\n. if n = 1 then 0 else f n) (dirichlet_inverse f i) n" proof - have "dirichlet_prod (\n. if n = 1 then 0 else f n) (dirichlet_inverse f i) n = (\d | d dvd n. (if n div d = Suc 0 then 0 else f (n div d)) * dirichlet_inverse f i d)" by (simp add: dirichlet_prod_altdef1) also from assms have "\ = (\d | d dvd n \ d \ n. f (n div d) * dirichlet_inverse f i d)" by (intro sum.mono_neutral_cong_right) (auto elim: dvdE) also from assms have "{d. d dvd n \ d \ n} = {d. d dvd n \ d < n}" by (auto dest: dvd_imp_le) also from assms have "-i * (\d\\. f (n div d) * dirichlet_inverse f i d) = dirichlet_inverse f i n" by (simp add: dirichlet_inverse_gt_1) finally show ?thesis .. qed lemma of_int_dirichlet_prod: "of_int (dirichlet_prod f g n) = dirichlet_prod (\n. of_int (f n)) (\n. of_int (g n)) n" by (simp add: dirichlet_prod_def) lemma of_int_dirichlet_inverse: "of_int (dirichlet_inverse f i n) = dirichlet_inverse (\n. of_int (f n)) (of_int i) n" proof (induction n rule: dirichlet_inverse_induct) case (gt1 n) from gt1 have "(of_int (dirichlet_inverse f i n) :: 'a) = - (of_int i * (\d | d dvd n \ d < n. of_int (f (n div d) * dirichlet_inverse f i d)))" (is "_ = - (_ * ?A)") by (simp add: dirichlet_inverse_gt_1 of_int_dirichlet_prod) also have "?A = (\d | d dvd n \ d < n. of_int (f (n div d)) * dirichlet_inverse (\n. of_int (f n)) (of_int i) d)" by (intro sum.cong refl) (auto simp: gt1) also have "-(of_int i * \) = dirichlet_inverse (\n. of_int (f n)) (of_int i) n" using gt1.hyps by (simp add: dirichlet_inverse_gt_1) finally show ?case . qed simp_all lemma dirichlet_inverse_code [code]: "dirichlet_inverse f i n = (if n = 0 then 0 else if n = 1 then i else -i * fold_atLeastAtMost_nat (\d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0)" proof - consider "n = 0" | "n = 1" | "n > 1" by force thus ?thesis proof cases assume n: "n > 1" have *: "(\d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) = (\d acc. (if d dvd n then f (n div d) * dirichlet_inverse f i d else 0) + acc)" by (simp add: fun_eq_iff) have "fold_atLeastAtMost_nat (\d acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0 = (\d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else 0)" by (subst *, subst sum_atLeastAtMost_code [symmetric]) simp also from n have "\ = (\d | d dvd n \ d < n. f (n div d) * dirichlet_inverse f i d)" by (intro sum.mono_neutral_cong_right; cases n) (auto dest: dvd_imp_le elim: dvdE simp: Suc_le_eq intro!: Nat.gr0I) also from n have "-i * \ = dirichlet_inverse f i n" by (simp add: dirichlet_inverse_gt_1) finally show ?thesis using n by simp qed auto qed lemma dirichlet_prod_inverse: assumes "f 1 * i = 1" shows "dirichlet_prod f (dirichlet_inverse f i) = (\n. if n = 1 then 1 else 0)" proof fix n :: nat consider "n = 0" | "n = 1" | "n > 1" by force thus "dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1 else 0)" proof cases assume n: "n > 1" have fin: "finite {d. d dvd n \ d \ n}" by (rule finite_subset[of _ "{d. d dvd n}"]) (insert n, auto) have "dirichlet_prod f (dirichlet_inverse f i) n = (\d | d dvd n. f (n div d) * dirichlet_inverse f i d)" by (simp add: dirichlet_prod_altdef1) also have "{d. d dvd n} = insert n {d. d dvd n \ d \ n}" by auto also have "(\d\\. f (n div d) * dirichlet_inverse f i d) = f 1 * dirichlet_inverse f i n + (\d | d dvd n \ d \ n. f (n div d) * dirichlet_inverse f i d)" using fin n by (subst sum.insert) auto also from n have "dirichlet_inverse f i n = - i * (\d | d dvd n \ d < n. f (n div d) * dirichlet_inverse f i d)" by (subst dirichlet_inverse_gt_1) auto also from n have "{d. d dvd n \ d < n} = {d. d dvd n \ d \ n}" by (auto dest: dvd_imp_le) also have "f 1 * (- i * (\d | d dvd n \ d \ n. f (n div d) * dirichlet_inverse f i d)) = -(f 1 * i) * (\d | d dvd n \ d \ n. f (n div d) * dirichlet_inverse f i d)" by (simp add: mult.assoc) also have "f 1 * i = 1" by fact finally show ?thesis using n by simp qed (insert assms, simp_all add: dirichlet_prod_def) qed lemma dirichlet_prod_inverse': assumes "f 1 * i = 1" shows "dirichlet_prod (dirichlet_inverse f i) f = (\n. if n = 1 then 1 else 0)" using dirichlet_prod_inverse[of f] assms by (simp add: dirichlet_prod_commutes) lemma dirichlet_inverse_noninvertible: assumes "f (Suc 0) = (0 :: 'a :: {comm_ring_1})" "i = 0" shows "dirichlet_inverse f i n = 0" using assms by (induction f i n rule: dirichlet_inverse.induct) (auto simp: dirichlet_inverse.simps) lemma multiplicative_dirichlet_prod: assumes "multiplicative_function f" assumes "multiplicative_function g" shows "multiplicative_function (dirichlet_prod f g)" proof - interpret f: multiplicative_function f by fact interpret g: multiplicative_function g by fact show ?thesis proof fix a b :: nat assume "a > 1" "b > 1" and coprime: "coprime a b" hence "dirichlet_prod f g (a * b) = (\r | r dvd a. \s | s dvd b. f (r * s) * g (a * b div (r * s)))" by (simp add: dirichlet_prod_def sum_divisors_coprime_mult) also have "\ = (\r | r dvd a. \s | s dvd b. f r * f s * g (a div r) * g (b div s))" using \coprime a b\ proof (rule sum_coprime_dvd_cong) fix r s assume "coprime r s" and "r dvd a" and "s dvd b" with \a > 1\ \b > 1\ have "r > 0" "s > 0" by (auto intro: ccontr) from \coprime r s\ have "f (r * s) = f r * f s" by (rule f.mult_coprime) moreover from \coprime a b\ have \coprime (a div r) (b div s)\ using \r > 0\ \s > 0\ \r dvd a\ \s dvd b\ dvd_div_iff_mult [of r a] dvd_div_iff_mult [of s b] by (auto dest: coprime_imp_coprime dvd_mult_left) then have "g (a div r * (b div s)) = g (a div r) * g (b div s)" by (rule g.mult_coprime) ultimately show "f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)" using \r dvd a\ \s dvd b\ by (simp add: div_mult_div_if_dvd ac_simps) qed also have "\ = dirichlet_prod f g a * dirichlet_prod f g b" unfolding dirichlet_prod_def by (simp add: sum_product mult_ac) finally show "dirichlet_prod f g (a * b) = \" . qed simp_all qed lemma multiplicative_dirichlet_prodD1: fixes f g :: "nat \ 'a :: comm_semiring_1_cancel" assumes "multiplicative_function (dirichlet_prod f g)" assumes "multiplicative_function f" assumes [simp]: "g 0 = 0" shows "multiplicative_function g" proof - interpret f: multiplicative_function f by fact interpret fg: multiplicative_function "dirichlet_prod f g" by fact show ?thesis proof have "dirichlet_prod f g (Suc 0) = 1" by (rule fg.Suc_0) also have "dirichlet_prod f g (Suc 0) = g 1" by (subst dirichlet_prod_Suc_0) simp finally show "g 1 = 1" by simp next fix a b :: nat assume ab: "a > 1" "b > 1" "coprime a b" hence "a > 0" "b > 0" "coprime a b" by simp_all thus "g (a * b) = g a * g b" proof (induction "a * b" arbitrary: a b rule: less_induct) case (less a b) have "dirichlet_prod f g (a * b) + g a * g b = (\r | r dvd a * b. f r * g (a * b div r)) + g a * g b" by (simp add: dirichlet_prod_def) also have "{r. r dvd a * b} = insert 1 {r. r dvd a * b \ r \ 1}" by auto also have "(\r\\. f r * g (a * b div r)) + g a * g b = g (a * b) + ((\r | r dvd a * b \ r \ 1. f r * g (a * b div r)) + g a * g b)" using less.prems by (subst sum.insert) (auto intro!: finite_subset[OF _ finite_divisors_nat'] simp: add_ac) also have "(\r | r dvd a * b \ r \ 1. f r * g (a * b div r)) = (\r | r dvd a * b. if r = 1 then 0 else f r * g (a * b div r))" using less.prems by (intro sum.mono_neutral_cong_left) (auto intro: finite_divisors_nat') also have "\ = (\r | r dvd a. \d | d dvd b. if r * d = 1 then 0 else f (r * d) * g (a * b div (r * d)))" using \coprime a b\ by (rule sum_divisors_coprime_mult) also have "\ = (\r | r dvd a. \d | d dvd b. if r * d = 1 then 0 else f (r * d) * g ((a div r) * (b div d)))" by (intro sum.cong refl) (auto elim!: dvdE) also have "\ = (\r | r dvd a. \d | d dvd b. if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))" using \coprime a b\ proof (rule sum_coprime_dvd_cong) fix r s assume "coprime r s" and "r dvd a" and "s dvd b" with \a > 0\ \b > 0\ have "r > 0" "s > 0" by (auto intro: ccontr) from \coprime r s\ have f: "f (r * s) = f r * f s" by (rule f.mult_coprime) show "(if r * s = 1 then 0 else f (r * s) * g (a div r * (b div s))) = (if r * s = 1 then 0 else f r * f s * g (a div r) * g (b div s))" proof (cases "r * s = 1") case True then show ?thesis by simp next case False with \r dvd a\ \s dvd b\ less.prems have "(a div r) * (b div s) \ a * b" by (intro notI) (auto elim!: dvdE) moreover from \r dvd a\ \s dvd b\ less.prems have "(a div r) * (b div s) \ a * b" by (intro dvd_imp_le mult_dvd_mono Nat.gr0I) (auto elim!: dvdE) ultimately have "(a div r) * (b div s) < a * b" by arith with \r dvd a\ \s dvd b\ less.prems have g: "g ((a div r) * (b div s)) = g (a div r) * g (b div s)" by (auto intro: less coprime_divisors [OF _ _ \coprime a b\] elim!: dvdE) from False show ?thesis by (auto simp: less f g ac_simps) qed qed also have "\ = (\(r,d)\{r. r dvd a}\{d. d dvd b}. if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))" by (simp add: sum.cartesian_product) also have "\ = (\(r1,r2) \ {r1. r1 dvd a} \ {r2. r2 dvd b} - {(1,1)}. (f r1 * f r2) * g (a div r1) * g (b div r2))" (is "_ = sum ?f ?A") using less.prems by (intro sum.mono_neutral_cong_right) (auto split: if_splits) also have "\ + g a * g b = ?f (1, 1) + sum ?f ?A" by (simp add: add_ac) also have "\ = sum ?f ({r1. r1 dvd a} \ {r2. r2 dvd b})" using less.prems by (intro sum.remove [symmetric]) auto also have "\ = dirichlet_prod f g a * dirichlet_prod f g b" by (simp add: sum.cartesian_product sum_product dirichlet_prod_def mult_ac) also have "g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b = dirichlet_prod f g (a * b) + g (a * b)" using less.prems by (simp add: fg.mult_coprime add_ac) finally show ?case by simp qed qed simp_all qed lemma multiplicative_dirichlet_prodD2: fixes f g :: "nat \ 'a :: comm_semiring_1_cancel" assumes "multiplicative_function (dirichlet_prod f g)" assumes "multiplicative_function g" assumes [simp]: "f 0 = 0" shows "multiplicative_function f" proof - from assms(1) have "multiplicative_function (dirichlet_prod g f)" by (simp add: dirichlet_prod_commutes) from multiplicative_dirichlet_prodD1[OF this assms(2)] show ?thesis by simp qed lemma multiplicative_dirichlet_inverse: assumes "multiplicative_function f" shows "multiplicative_function (dirichlet_inverse f 1)" proof (rule multiplicative_dirichlet_prodD1[OF _ assms]) interpret multiplicative_function f by fact have "multiplicative_function (\n. if n = 1 then 1 else 0)" by standard simp_all thus "multiplicative_function (dirichlet_prod f (dirichlet_inverse f 1))" by (subst dirichlet_prod_inverse) simp_all qed simp_all lemma dirichlet_prod_prime_power: assumes "prime p" shows "dirichlet_prod f g (p ^ k) = (\i\k. f (p ^ i) * g (p ^ (k - i)))" proof - have "dirichlet_prod f g (p ^ k) = (\i\k. f (p ^ i) * g (p ^ k div p ^ i))" unfolding dirichlet_prod_def using assms by (intro sum.reindex_bij_betw [symmetric] bij_betw_prime_power_divisors) also from assms have "\ = (\i\k. f (p ^ i) * g (p ^ (k - i)))" - by (intro sum.cong refl) (auto simp: power_diff') + by (intro sum.cong refl) (auto simp: power_diff) finally show ?thesis . qed lemma dirichlet_prod_prime: assumes "prime p" shows "dirichlet_prod f g p = f 1 * g p + f p * g 1" using dirichlet_prod_prime_power[of p f g 1] assms by simp locale multiplicative_dirichlet_prod = f: multiplicative_function f + g: multiplicative_function g for f g :: "nat \ 'a :: comm_semiring_1" begin sublocale multiplicative_function "dirichlet_prod f g" by (intro multiplicative_dirichlet_prod f.multiplicative_function_axioms g.multiplicative_function_axioms) end locale multiplicative_dirichlet_prod' = f: multiplicative_function' f f_prime_power f_prime + g: multiplicative_function' g g_prime_power g_prime for f g :: "nat \ 'a :: comm_semiring_1" and f_prime_power g_prime_power f_prime g_prime begin sublocale multiplicative_dirichlet_prod f g .. sublocale multiplicative_function' "dirichlet_prod f g" "\p k. f_prime_power p k + g_prime_power p k + (\i\{0<..p. f_prime p + g_prime p" proof (standard, goal_cases) case (1 p k) hence "dirichlet_prod f g (p ^ k) = (\i\k. f (p ^ i) * g (p ^ (k - i)))" by (intro dirichlet_prod_prime_power) also from 1 have "{..k} = insert 0 (insert k {0<..i\\. f (p ^ i) * g (p ^ (k - i))) = f_prime_power p k + g_prime_power p k + (\i\{0<..i\{0<..i\{0<..The M\"{o}bius $\mu$ function\ theory Moebius_Mu imports Main "HOL-Number_Theory.Number_Theory" "HOL-Computational_Algebra.Squarefree" Dirichlet_Series Dirichlet_Misc begin definition moebius_mu :: "nat \ 'a :: comm_ring_1" where "moebius_mu n = (if squarefree n then (-1) ^ card (prime_factors n) else 0)" lemma abs_moebius_mu_le: "abs (moebius_mu n :: 'a :: {linordered_idom}) \ 1" by (auto simp add: moebius_mu_def) -lemma moebius_commute: "x * moebius_mu n = moebius_mu n * x" - by (cases "even (card (prime_factors n))") (auto simp: moebius_mu_def) - -lemma dirichlet_prod_moebius_commute: - "dirichlet_prod f moebius_mu = dirichlet_prod moebius_mu f" - by (subst dirichlet_prod_def, subst dirichlet_prod_altdef1) (simp add: moebius_commute) - -lemma fds_moebius_commute: "x * fds moebius_mu = fds moebius_mu * x" - by (simp add: fds_eq_iff fds_nth_mult dirichlet_prod_moebius_commute) - lemma of_int_moebius_mu [simp]: "of_int (moebius_mu n) = moebius_mu n" by (simp add: moebius_mu_def) lemma minus_1_power_ring_neq_zero [simp]: "(- 1 :: 'a :: ring_1) ^ n \ 0" by (cases "even n") simp_all lemma moebius_mu_0 [simp]: "moebius_mu 0 = 0" by (simp add: moebius_mu_def) lemma fds_nth_fds_moebius_mu [simp]: "fds_nth (fds moebius_mu) = moebius_mu" by (simp add: fun_eq_iff fds_nth_fds) lemma prime_factors_Suc_0 [simp]: "prime_factors (Suc 0) = {}" - by (subst prime_factors_dvd) auto + by simp lemma moebius_mu_Suc_0 [simp]: "moebius_mu (Suc 0) = 1" by (simp add: moebius_mu_def) lemma moebius_mu_1 [simp]: "moebius_mu 1 = 1" by (simp add: moebius_mu_def) lemma moebius_mu_eq_zero_iff: "moebius_mu n = 0 \ \squarefree n" by (simp add: moebius_mu_def) lemma moebius_mu_not_squarefree [simp]: "\squarefree n \ moebius_mu n = 0" by (simp add: moebius_mu_def) lemma moebius_mu_power: assumes "a > 1" "n > 1" shows "moebius_mu (a ^ n) = 0" proof - from assms have "a ^ 2 dvd a ^ n" by (simp add: le_imp_power_dvd) with moebius_mu_eq_zero_iff[of "a ^ n"] and \a > 1\ show ?thesis by (auto simp: squarefree_def) qed lemma moebius_mu_power': "moebius_mu (a ^ n) = (if a = 1 \ n = 0 then 1 else if n = 1 then moebius_mu a else 0)" - by (cases "a = 0") (auto simp: power_0_left moebius_mu_power) + by (simp add: squarefree_power_iff) lemma moebius_mu_squarefree_eq: "squarefree n \ moebius_mu n = (-1) ^ card (prime_factors n)" by (simp add: moebius_mu_def split: if_splits) lemma moebius_mu_squarefree_eq': assumes "squarefree n" shows "moebius_mu n = (-1) ^ size (prime_factorization n)" proof - let ?P = "prime_factorization n" from assms have [simp]: "n > 0" by (auto intro!: Nat.gr0I) have "size ?P = sum (count ?P) (set_mset ?P)" by (rule size_multiset_overloaded_eq) also from assms have "\ = sum (\_. 1) (set_mset ?P)" by (intro sum.cong refl, subst count_prime_factorization_prime) (auto simp: moebius_mu_eq_zero_iff squarefree_factorial_semiring') also have "\ = card (set_mset ?P)" by simp finally show ?thesis by (simp add: moebius_mu_squarefree_eq[OF assms]) qed lemma sum_moebius_mu_divisors: assumes "n > 1" shows "(\d | d dvd n. moebius_mu d) = (0 :: 'a :: comm_ring_1)" proof - have "(\d | d dvd n. moebius_mu d :: int) = (\d \ Prod ` {P. P \ prime_factors n}. moebius_mu d)" proof (rule sum.mono_neutral_right; safe?) fix A assume A: "A \ prime_factors n" from A have [simp]: "finite A" by (rule finite_subset) auto from A have A': "x > 0" "prime x" if "x \ A" for x using that by (auto simp: prime_factors_multiplicity prime_gt_0_nat) from A' have A_nz: "\A \ 0" by (intro notI) auto from A' have "prime_factorization (\A) = sum prime_factorization A" by (subst prime_factorization_prod) (auto dest: finite_subset) also from A' have "\ = sum (\x. {#x#}) A" by (intro sum.cong refl) (auto simp: prime_factorization_prime) also have "\ = mset_set A" by simp also from A have "\ \# mset_set (prime_factors n)" by (rule subset_imp_msubset_mset_set) simp_all also have "\ \# prime_factorization n" by (rule mset_set_set_mset_msubset) finally show "\A dvd n" using A_nz by (intro prime_factorization_subset_imp_dvd) auto next fix x assume x: "x \ Prod ` {P. P \ prime_factors n}" "x dvd n" from x assms have [simp]: "x > 0" by (auto intro!: Nat.gr0I) { assume nz: "moebius_mu x \ 0" have "(\(set_mset (prime_factorization x))) = (\p\prime_factors x. p ^ multiplicity p x)" using nz by (intro prod.cong refl) (auto simp: moebius_mu_eq_zero_iff squarefree_factorial_semiring') also have "\ = x" by (intro Primes.prime_factorization_nat [symmetric]) auto finally have "x = \(prime_factors x)" "prime_factors x \ prime_factors n" using dvd_prime_factors[of n x] assms \x dvd n\ by auto hence "x \ Prod ` {P. P \ prime_factors n}" by blast with x(1) have False by contradiction } thus "moebius_mu x = 0" by blast qed (insert assms, auto) also have "\ = (\P | P \ prime_factors n. moebius_mu (\P))" by (subst sum.reindex) (auto intro!: inj_on_Prod_primes dest: finite_subset) also have "\ = (\P | P \ prime_factors n. (-1) ^ card P)" proof (intro sum.cong refl) fix P assume P: "P \ {P. P \ prime_factors n}" hence [simp]: "finite P" by (auto dest: finite_subset) from P have prime: "prime p" if "p \ P" for p using that by (auto simp: prime_factors_dvd) hence "squarefree (\P)" by (intro squarefree_prod_coprime prime_imp_coprime squarefree_prime) (auto simp: primes_dvd_imp_eq) hence "moebius_mu (\P) = (-1) ^ card (prime_factors (\P))" by (rule moebius_mu_squarefree_eq) also from P have "prime_factors (\P) = P" by (subst prime_factors_prod) (auto simp: prime_factorization_prime prime) finally show "moebius_mu (\P) = (-1) ^ card P" . qed also have "{P. P \ prime_factors n} = {P. P \ prime_factors n \ even (card P)} \ {P. P \ prime_factors n \ odd (card P)}" (is "_ = ?A \ ?B") by blast also have "(\P \ \. (-1) ^ card P) = (\P \ ?A. (-1) ^ card P) + (\P \ ?B. (-1) ^ card P)" by (intro sum.union_disjoint) auto also have "(\P \ ?A. (-1) ^ card P :: int) = (\P \ ?A. 1)" by (intro sum.cong refl) auto also have "\ = int (card ?A)" by simp also have "(\P \ ?B. (-1) ^ card P :: int) = (\P \ ?B. -1)" by (intro sum.cong refl) auto also have "\ = -int (card ?B)" by simp also have "card ?B = card ?A" by (rule card_even_odd_subset [symmetric]) (insert assms, auto simp: prime_factorization_empty_iff) also have "int (card ?A) + (- int (card ?A)) = 0" by simp finally have "(\d | d dvd n. of_int (moebius_mu d) :: 'a) = 0" unfolding of_int_sum [symmetric] by (simp only: of_int_0) thus ?thesis by simp qed lemma sum_moebius_mu_divisors': "(\d | d dvd n. moebius_mu d) = (if n = 1 then 1 else 0)" proof - have "n = 0 \ n = 1 \ n > 1" by force thus ?thesis using sum_moebius_mu_divisors[of n] by auto qed lemma fds_zeta_times_moebius_mu: "fds_zeta * fds moebius_mu = 1" proof fix n :: nat assume n: "n > 0" from n have "fds_nth (fds_zeta * fds moebius_mu :: 'a fds) n = (\d | d dvd n. moebius_mu d)" unfolding fds_nth_mult dirichlet_prod_altdef1 by (intro sum.cong refl) (auto simp: fds_nth_fds elim: dvdE) also have "\ = fds_nth 1 n" by (simp add: sum_moebius_mu_divisors') finally show "fds_nth (fds_zeta * fds moebius_mu :: 'a fds) n = fds_nth 1 n" . qed lemma fds_moebius_inverse_zeta: "fds moebius_mu = inverse (fds_zeta :: 'a :: field fds)" - by (rule fds_right_inverse_unique) (simp add: fds_zeta_times_moebius_mu) + using fds_right_inverse_unique fds_zeta_times_moebius_mu by blast lemma moebius_mu_formula_real: "(moebius_mu n :: real) = dirichlet_inverse (\_. 1) 1 n" proof - have "moebius_mu n = (fds_nth (fds moebius_mu) n :: real)" by simp also have "fds moebius_mu = (inverse fds_zeta :: real fds)" by (fact fds_moebius_inverse_zeta) also have "fds_nth \ n = dirichlet_inverse (fds_nth fds_zeta) 1 n" unfolding fds_nth_inverse by simp also have "\ = dirichlet_inverse (\_. 1) 1 n" by (rule dirichlet_inverse_cong) simp_all finally show ?thesis . qed lemma moebius_mu_formula_int: "moebius_mu n = dirichlet_inverse (\_. 1 :: int) 1 n" proof - have "real_of_int (moebius_mu n) = moebius_mu n" by simp also have "\ = dirichlet_inverse (\_. 1) 1 n" by (fact moebius_mu_formula_real) also have "\ = real_of_int (dirichlet_inverse (\_. 1) 1 n)" by (induction n rule: dirichlet_inverse_induct) (simp_all add: dirichlet_inverse_gt_1) finally show ?thesis by (subst (asm) of_int_eq_iff) qed lemma moebius_mu_formula: "moebius_mu n = dirichlet_inverse (\_. 1) 1 n" by (subst of_int_moebius_mu [symmetric], subst moebius_mu_formula_int) (simp add: of_int_dirichlet_inverse) interpretation moebius_mu: multiplicative_function moebius_mu proof - have "multiplicative_function (dirichlet_inverse (\n. if n = 0 then 0 else 1 :: 'a) 1)" by (rule multiplicative_dirichlet_inverse, standard) simp_all also have "dirichlet_inverse (\n. if n = 0 then 0 else 1 :: 'a) 1 = moebius_mu" by (auto simp: fun_eq_iff moebius_mu_formula) finally show "multiplicative_function (moebius_mu :: nat \ 'a)" . qed interpretation moebius_mu: multiplicative_function' moebius_mu "\p k. if k = 1 then -1 else 0" "\_. -1" proof fix p k :: nat assume "prime p" "k > 0" moreover from this have "moebius_mu p = -1" by (simp add: moebius_mu_def prime_factorization_prime squarefree_prime) ultimately show "moebius_mu (p ^ k) = (if k = 1 then - 1 else 0)" by (auto simp: moebius_mu_power') qed auto lemma moebius_mu_2 [simp]: "moebius_mu 2 = -1" and moebius_mu_3 [simp]: "moebius_mu 3 = -1" by (rule moebius_mu.prime; simp)+ lemma moebius_mu_code [code]: "moebius_mu n = of_int (dirichlet_inverse (\_. 1 :: int) 1 n)" by (subst moebius_mu_formula_int [symmetric]) simp lemma fds_moebius_inversion: "f = fds moebius_mu * g \ g = f * fds_zeta" -proof - assume "g = f * fds_zeta" - hence "g * fds moebius_mu = f * (fds_zeta * fds moebius_mu)" by (simp add: mult_ac) - also have "\ = f" by (simp add: fds_zeta_times_moebius_mu) - finally show "f = fds moebius_mu * g" by (simp add: mult_ac) -next - assume "f = fds moebius_mu * g" - hence "fds_zeta * f = fds_zeta * fds moebius_mu * g" by (simp add: mult_ac) - also have "\ = g" by (simp add: fds_zeta_times_moebius_mu) - finally show "g = f * fds_zeta" by (simp add: mult_ac) -qed + by (metis fds_zeta_times_moebius_mu mult.commute mult.left_commute mult.right_neutral) lemma moebius_inversion: assumes "\n. n > 0 \ g n = (\d | d dvd n. f d)" "n > 0" shows "f n = dirichlet_prod moebius_mu g n" proof - from assms have "fds g = fds f * fds_zeta" by (intro fds_eqI) (simp add: fds_nth_mult dirichlet_prod_def) thus ?thesis using assms by (subst (asm) fds_moebius_inversion [symmetric]) (simp add: fds_eq_iff fds_nth_mult) qed lemma fds_mangoldt: "fds mangoldt = fds moebius_mu * fds (\n. of_real (ln (real n)))" by (subst fds_moebius_inversion) (rule fds_mangoldt_times_zeta [symmetric]) (* 2.18 *) lemma sum_divisors_moebius_mu_times_multiplicative: fixes f :: "nat \ 'a :: {comm_ring_1}" assumes "multiplicative_function f" "n > 0" shows "(\d | d dvd n. moebius_mu d * f d) = (\p\prime_factors n. 1 - f p)" proof - define g where "g = (\n. \d | d dvd n. moebius_mu d * f d)" define g' where "g' = dirichlet_prod (\n. moebius_mu n * f n) (\n. if n = 0 then 0 else 1)" interpret f: multiplicative_function f by fact have "multiplicative_function (\n. if n = 0 then 0 else 1 :: 'a)" by standard auto interpret multiplicative_function g' unfolding g'_def by (intro multiplicative_dirichlet_prod multiplicative_function_mult moebius_mu.multiplicative_function_axioms assms) fact+ have g'_primepow: "g' (p ^ k) = 1 - f p" if "prime p" "k > 0" for p k proof - have "g' (p ^ k) = (\i\k. moebius_mu (p ^ i) * f (p ^ i))" using that by (simp add: g'_def dirichlet_prod_prime_power) also have "\ = (\i\{0, 1}. moebius_mu (p ^ i) * f (p ^ i))" using that by (intro sum.mono_neutral_right) (auto simp: moebius_mu_power') also have "\ = 1 - f p" using that by (simp add: moebius_mu.prime) finally show ?thesis . qed have "g' n = g n" by (simp add: g_def g'_def dirichlet_prod_def) also from assms have "g' n = (\p\prime_factors n. g' (p ^ multiplicity p n))" by (intro prod_prime_factors) auto also have "\ = (\p\prime_factors n. 1 - f p)" by (intro prod.cong) (auto simp: g'_primepow prime_factors_multiplicity) finally show ?thesis by (simp add: g_def) qed (* Theorem 2.17 *) lemma completely_multiplicative_iff_inverse_moebius_mu: fixes f :: "nat \ 'a :: {comm_ring_1, ring_no_zero_divisors}" assumes "multiplicative_function f" defines "g \ dirichlet_inverse f 1" shows "completely_multiplicative_function f \ (\n. g n = moebius_mu n * f n)" proof - interpret multiplicative_function f by fact show ?thesis proof safe assume "completely_multiplicative_function f" then interpret completely_multiplicative_function f . have [simp]: "fds f \ 0" by (auto simp: fds_eq_iff) have "fds (\n. moebius_mu n * f n) * fds f = 1" proof fix n :: nat have "fds_nth (fds (\n. moebius_mu n * f n) * fds f) n = (\(r, d) | r * d = n. moebius_mu r * f (r * d))" by (simp add: fds_eq_iff fds_nth_mult fds_nth_fds dirichlet_prod_altdef2 mult mult.assoc) also have "\ = (\(r, d) | r * d = n. moebius_mu r * f n)" by (intro sum.cong) auto also have "\ = dirichlet_prod moebius_mu (\_. 1) n * f n" by (simp add: dirichlet_prod_altdef2 sum_distrib_right case_prod_unfold mult) also have "dirichlet_prod moebius_mu (\_. 1) n = fds_nth (fds moebius_mu * fds_zeta) n" by (simp add: fds_nth_mult) also have "fds moebius_mu * fds_zeta = 1" by (simp add: mult_ac fds_zeta_times_moebius_mu) also have "fds_nth 1 n * f n = fds_nth 1 n" by (auto simp: fds_eq_iff fds_nth_one) finally show "fds_nth (fds (\n. moebius_mu n * f n) * fds f) n = fds_nth 1 n" . qed also have "1 = fds g * fds f" by (auto simp: fds_eq_iff g_def fds_nth_mult dirichlet_prod_inverse') finally have "fds g = fds (\n. moebius_mu n * f n)" by (subst (asm) mult_cancel_right) auto thus "g n = moebius_mu n * f n" for n by (cases "n = 0") (auto simp: fds_eq_iff g_def) next assume g: "\n. g n = moebius_mu n * f n" show "completely_multiplicative_function f" proof (rule completely_multiplicativeI) fix p k :: nat assume pk: "prime p" "k > 0" show "f (p ^ k) = f p ^ k" proof (induction k) case (Suc k) have eq: "dirichlet_prod g f n = 0" if "n \ 1" for n unfolding g_def using dirichlet_prod_inverse'[of f 1] that by auto have "dirichlet_prod g f (p ^ Suc k) = 0" using pk by (intro eq) auto also have "dirichlet_prod g f (p ^ Suc k) = (\i\Suc k. g (p ^ i) * f (p ^ (Suc k - i)))" by (intro dirichlet_prod_prime_power) fact+ also have "\ = (\i\Suc k. moebius_mu (p ^ i) * f (p ^ i) * f (p ^ (Suc k - i)))" by (intro sum.cong refl, subst g) auto also have "\ = (\i\{0, 1}. moebius_mu (p ^ i) * f (p ^ i) * f (p ^ (Suc k - i)))" using pk by (intro sum.mono_neutral_right) (auto simp: moebius_mu_power') also have "\ = f (p ^ Suc k) - f p ^ Suc k" using pk Suc.IH by (auto simp: moebius_mu.prime) finally show "f (p ^ Suc k) = f p ^ Suc k" by simp qed auto qed qed qed lemma completely_multiplicative_fds_inverse: fixes f :: "nat \ 'a :: field" assumes "completely_multiplicative_function f" shows "inverse (fds f) = fds (\n. moebius_mu n * f n)" proof - interpret completely_multiplicative_function f by fact from assms show ?thesis by (subst (asm) completely_multiplicative_iff_inverse_moebius_mu) (auto simp: inverse_fds_def multiplicative_function_axioms) qed lemma completely_multiplicative_fds_inverse': fixes f :: "'a :: field fds" assumes "completely_multiplicative_function (fds_nth f)" shows "inverse f = fds (\n. moebius_mu n * fds_nth f n)" -proof - - have "f = fds (fds_nth f)" by simp - also have "inverse (fds (fds_nth f)) = fds (\n. moebius_mu n * fds_nth f n)" - by (intro completely_multiplicative_fds_inverse assms) - finally show ?thesis by simp -qed + by (metis assms completely_multiplicative_fds_inverse fds_fds_nth) context includes fds_syntax begin lemma selberg_aux: "(\ n. of_real ((ln n)\<^sup>2)) * fds moebius_mu = (fds mangoldt)\<^sup>2 - fds_deriv (fds mangoldt :: 'a :: {comm_ring_1,real_algebra_1} fds)" proof - have "(\ n. of_real (ln (real n) ^ 2)) = fds_deriv (fds_deriv fds_zeta :: 'a fds)" by (rule fds_eqI) (simp add: fds_nth_fds fds_nth_deriv power2_eq_square scaleR_conv_of_real) also have "\ = (fds mangoldt ^ 2 - fds_deriv (fds mangoldt)) * fds_zeta" by (simp add: fds_deriv_zeta algebra_simps power2_eq_square) also have "\ * fds moebius_mu = ((fds mangoldt)\<^sup>2 - fds_deriv (fds mangoldt)) * (fds_zeta * fds moebius_mu)" by (simp add: mult_ac) also have "fds_zeta * fds moebius_mu = (1 :: 'a fds)" by (fact fds_zeta_times_moebius_mu) finally show ?thesis by simp qed lemma selberg_aux': "mangoldt n * of_real (ln n) + (mangoldt \ mangoldt) n = ((moebius_mu \ (\b. of_real (ln b) ^ 2)) n :: 'a :: {comm_ring_1,real_algebra_1})" if "n > 0" using selberg_aux [symmetric] that by (auto simp add: fds_eq_iff fds_nth_mult power2_eq_square fds_nth_deriv dirichlet_prod_commutes algebra_simps scaleR_conv_of_real) end end diff --git a/thys/Finite_Fields/Card_Irreducible_Polynomials.thy b/thys/Finite_Fields/Card_Irreducible_Polynomials.thy --- a/thys/Finite_Fields/Card_Irreducible_Polynomials.thy +++ b/thys/Finite_Fields/Card_Irreducible_Polynomials.thy @@ -1,231 +1,231 @@ subsection \Gauss Formula\label{sec:card_irred}\ theory Card_Irreducible_Polynomials - imports + imports Dirichlet_Series.Moebius_Mu Card_Irreducible_Polynomials_Aux begin hide_const "Polynomial.order" text \The following theorem is a slightly generalized form of the formula discovered by -Gauss for the number of monic irreducible polynomials over a finite field. He originally verified +Gauss for the number of monic irreducible polynomials over a finite field. He originally verified the result for the case when @{term "R"} is a simple prime field. The version of the formula here for the case where @{term "R"} may be an arbitrary finite field can be found in Chebolu and Min{\'a}{\v{c}}~\<^cite>\"chebolu2010"\.\ theorem (in finite_field) card_irred: assumes "n > 0" - shows "n * card {f. monic_irreducible_poly R f \ degree f = n} = + shows "n * card {f. monic_irreducible_poly R f \ degree f = n} = (\d | d dvd n. moebius_mu d * (order R^(n div d)))" (is "?lhs = ?rhs") proof - have "?lhs = dirichlet_prod moebius_mu (\x. int (order R) ^ x) n" using card_irred_aux - by (intro moebius_inversion assms) (simp flip:of_nat_power) + by (intro moebius_inversion assms) (simp flip:of_nat_power) also have "... = ?rhs" by (simp add:dirichlet_prod_def) finally show ?thesis by simp qed text \In the following an explicit analytic lower bound for the cardinality of monic irreducible -polynomials is shown, with which existence follows. This part deviates from the classic approach, +polynomials is shown, with which existence follows. This part deviates from the classic approach, where existence is verified using a divisibility argument. The reason for the deviation is that an -analytic bound can also be used to estimate the runtime of a randomized algorithm selecting an +analytic bound can also be used to estimate the runtime of a randomized algorithm selecting an irreducible polynomial, by randomly sampling monic polynomials.\ lemma (in finite_field) card_irred_1: - "card {f. monic_irreducible_poly R f \ degree f = 1} = order R" + "card {f. monic_irreducible_poly R f \ degree f = 1} = order R" proof - have "int (1 * card {f. monic_irreducible_poly R f \ degree f = 1}) = int (order R)" by (subst card_irred, auto) thus ?thesis by simp qed lemma (in finite_field) card_irred_2: - "real (card {f. monic_irreducible_poly R f \ degree f = 2}) = - (real (order R)^2 - order R) / 2" + "real (card {f. monic_irreducible_poly R f \ degree f = 2}) = + (real (order R)^2 - order R) / 2" proof - have "x dvd 2 \ x = 1 \ x = 2" for x :: nat - using nat_dvd_not_less[where m="2"] - by (metis One_nat_def even_zero gcd_nat.strict_trans2 + using nat_dvd_not_less[where m="2"] + by (metis One_nat_def even_zero gcd_nat.strict_trans2 less_2_cases nat_neq_iff pos2) - hence a: "{d. d dvd 2} = {1,2::nat}" + hence a: "{d. d dvd 2} = {1,2::nat}" by (auto simp add:set_eq_iff) have "2*real (card {f. monic_irreducible_poly R f \ degree f = 2}) = of_int (2* card {f. monic_irreducible_poly R f \ degree f = 2})" by simp - also have "... = + also have "... = of_int (\d | d dvd 2. moebius_mu d * int (order R) ^ (2 div d))" by (subst card_irred, auto) also have "... = order R^2 - int (order R)" by (subst a, simp) also have "... = real (order R)^2 - order R" by simp - finally have - "2 * real (card {f. monic_irreducible_poly R f \ degree f = 2}) = + finally have + "2 * real (card {f. monic_irreducible_poly R f \ degree f = 2}) = real (order R)^2 - order R" by simp thus ?thesis by simp qed lemma (in finite_field) card_irred_gt_2: assumes "n > 2" - shows "real (order R)^n / (2*real n) \ - card {f. monic_irreducible_poly R f \ degree f = n}" + shows "real (order R)^n / (2*real n) \ + card {f. monic_irreducible_poly R f \ degree f = n}" (is "?lhs \ ?rhs") proof - let ?m = "real (order R)" - have a:"?m \ 2" + have a:"?m \ 2" using finite_field_min_order by simp - have b:"moebius_mu n \ -(1::real)" for n :: nat + have b:"moebius_mu n \ -(1::real)" for n :: nat using abs_moebius_mu_le[where n="n"] - unfolding abs_le_iff by auto + unfolding abs_le_iff by auto have c: "n > 0" using assms by simp have d: "x < n - 1" if d_assms: "x dvd n" "x \ n" for x :: nat proof - - have "x < n" + have "x < n" using d_assms dvd_nat_bounds c by auto - moreover have "\(n-1 dvd n)" using assms - by (metis One_nat_def Suc_diff_Suc c diff_zero - dvd_add_triv_right_iff nat_dvd_1_iff_1 + moreover have "\(n-1 dvd n)" using assms + by (metis One_nat_def Suc_diff_Suc c diff_zero + dvd_add_triv_right_iff nat_dvd_1_iff_1 nat_neq_iff numeral_2_eq_2 plus_1_eq_Suc) hence "x \ n-1" using d_assms by auto ultimately show "x < n-1" by simp qed have "?m^n / 2 = ?m^n - ?m^n/2" by simp also have "... \ ?m^n - ?m^n/?m^1" using a by (intro diff_mono divide_left_mono, simp_all) also have "... \ ?m^n - ?m^(n-1)" - using a c by (subst power_diff, simp_all) + using a c by (subst power_diff, simp_all) also have "... \ ?m^n - (?m^(n-1) - 1)/1" by simp also have "... \ ?m^n - (?m^(n-1)-1)/(?m-1)" - using a by (intro diff_left_mono divide_left_mono, simp_all) + using a by (intro diff_left_mono divide_left_mono, simp_all) also have "... = ?m^n - (\i \ {.. ?m^n - (\i \ {k. k dvd n \ k \ n}. ?m^i)" using d - by (intro diff_mono sum_mono2 subsetI, auto simp add:not_less) + by (intro diff_mono sum_mono2 subsetI, auto simp add:not_less) also have "... = ?m^n + (\i \ {k. k dvd n \ k \ n}. (-1) * ?m^i)" by (subst sum_distrib_left[symmetric], simp) - also have "... \ moebius_mu 1 * ?m^n + + also have "... \ moebius_mu 1 * ?m^n + (\i \ {k. k dvd n \ k \ n}. moebius_mu (n div i) * ?m^i)" using b - by (intro add_mono sum_mono mult_right_mono) - (simp_all add:not_less) + by (intro add_mono sum_mono mult_right_mono) + (simp_all add:not_less) also have "... = (\i \ insert n {k. k dvd n \ k \ n}. moebius_mu (n div i) * ?m^i)" - using c by (subst sum.insert, auto) + using c by (subst sum.insert, auto) also have "... = (\i \ {k. k dvd n}. moebius_mu (n div i) * ?m^i)" by (intro sum.cong, auto simp add:set_eq_iff) - also have "... = dirichlet_prod (\i. ?m^i) moebius_mu n" + also have "... = dirichlet_prod (\i. ?m^i) moebius_mu n" unfolding dirichlet_prod_def by (intro sum.cong, auto) also have "... = dirichlet_prod moebius_mu (\i. ?m^i) n" - using dirichlet_prod_moebius_commute by metis - also have "... = + using dirichlet_prod_commutes by metis + also have "... = of_int (\d | d dvd n. moebius_mu d * order R^(n div d))" unfolding dirichlet_prod_def by simp - also have "... = of_int (n * + also have "... = of_int (n * card {f. monic_irreducible_poly R f \ length f - 1 = n})" using card_irred[OF c] by simp also have "... = n * ?rhs" by simp finally have "?m^n / 2 \ n * ?rhs" by simp hence "?m ^ n \ 2 * n * ?rhs" by simp - hence "?m^n/(2*real n) \ ?rhs" - using c by (subst pos_divide_le_eq, simp_all add:algebra_simps) + hence "?m^n/(2*real n) \ ?rhs" + using c by (subst pos_divide_le_eq, simp_all add:algebra_simps) thus ?thesis by simp qed lemma (in finite_field) exist_irred: assumes "n > 0" obtains f where "monic_irreducible_poly R f" "degree f = n" proof - consider (i) "n = 1" | (ii) "n = 2" | (iii) "n>2" using assms by linarith - then have + then have "card {f. monic_irreducible_poly R f \ degree f = n} > 0" (is "card ?A > 0") proof (cases) case i hence "card ?A = order R" using card_irred_1 by simp also have "... > 0" using finite_field_min_order by simp finally show ?thesis by simp next case ii - have "0 < (real (order R) * (real (order R) - 1)) / 2" + have "0 < (real (order R) * (real (order R) - 1)) / 2" using finite_field_min_order by simp also have "... = (real (order R)^2 - order R) / 2" by (simp add:power2_eq_square algebra_simps) also have "... = real (card ?A)" - using ii by (subst card_irred_2[symmetric], simp) + using ii by (subst card_irred_2[symmetric], simp) finally have " 0 < real (card ?A)" by simp then show ?thesis by simp next case iii have "0 < real (order R)^n / (2*real n)" using finite_field_min_order assms by simp also have "... \ real (card ?A)" using iii card_irred_gt_2 by simp finally have "0 < real (card ?A)" by simp then show ?thesis by simp qed - hence "?A \ {}" + hence "?A \ {}" by (metis card.empty nless_le) then obtain f where "monic_irreducible_poly R f" "degree f = n" by auto thus ?thesis using that by simp qed theorem existence: assumes "n > 0" assumes "Factorial_Ring.prime p" shows "\(F:: int set list set ring). finite_field F \ order F = p^n" proof - interpret zf: finite_field "ZFact (int p)" using zfact_prime_is_finite_field assms by simp interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)" unfolding polynomial_ring_def polynomial_ring_axioms_def using zf.field_axioms zf.carrier_is_subfield by simp have p_gt_0: "p > 0" using prime_gt_0_nat assms(2) by simp - obtain f where f_def: + obtain f where f_def: "monic_irreducible_poly (ZFact (int p)) f" "degree f = n" using zf.exist_irred assms by auto - let ?F = "Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" + let ?F = "Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" have "f \ carrier (poly_ring (ZFact (int p)))" using f_def(1) zf.monic_poly_carr unfolding monic_irreducible_poly_def by simp moreover have "degree f > 0" using assms(1) f_def by simp ultimately have "order ?F = card (carrier (ZFact p))^degree f" by (intro zf.rupture_order[OF zf.carrier_is_subfield]) auto hence a:"order ?F = p^n" unfolding f_def(2) card_zfact_carr[OF p_gt_0] by simp have "field ?F" using f_def(1) zf.monic_poly_carr monic_irreducible_poly_def by (subst zfp.rupture_is_field_iff_pirreducible) auto moreover have "order ?F > 0" unfolding a using assms(1,2) p_gt_0 by simp ultimately have b:"finite_field ?F" using card_ge_0_finite - by (intro finite_fieldI, auto simp add:Coset.order_def) + by (intro finite_fieldI, auto simp add:Coset.order_def) show ?thesis using a b by (intro exI[where x="?F"], simp) qed end diff --git a/thys/Polynomial_Factorization/Missing_List.thy b/thys/Polynomial_Factorization/Missing_List.thy --- a/thys/Polynomial_Factorization/Missing_List.thy +++ b/thys/Polynomial_Factorization/Missing_List.thy @@ -1,1656 +1,1577 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) subsection \Missing List\ text \The provides some standard algorithms and lemmas on lists.\ theory Missing_List imports Matrix.Utility "HOL-Library.Monad_Syntax" begin fun concat_lists :: "'a list list \ 'a list list" where "concat_lists [] = [[]]" | "concat_lists (as # xs) = concat (map (\vec. map (\a. a # vec) as) (concat_lists xs))" lemma concat_lists_listset: "set (concat_lists xs) = listset (map set xs)" by (induct xs, auto simp: set_Cons_def) lemma sum_list_concat: "sum_list (concat ls) = sum_list (map sum_list ls)" by (induct ls, auto) (* TODO: move to src/HOL/List *) lemma listset: "listset xs = { ys. length ys = length xs \ (\ i < length xs. ys ! i \ xs ! i)}" proof (induct xs) case (Cons x xs) let ?n = "length xs" from Cons have "?case = (set_Cons x {ys. length ys = ?n \ (\i < ?n. ys ! i \ xs ! i)} = {ys. length ys = Suc ?n \ ys ! 0 \ x \ (\i < ?n. ys ! Suc i \ xs ! i)})" (is "_ = (?L = ?R)") by (auto simp: all_Suc_conv) also have "?L = ?R" by (auto simp: set_Cons_def, case_tac xa, auto) finally show ?case by simp qed auto lemma set_concat_lists[simp]: "set (concat_lists xs) = {as. length as = length xs \ (\i set (xs ! i))}" unfolding concat_lists_listset listset by simp declare concat_lists.simps[simp del] fun find_map_filter :: "('a \ 'b) \ ('b \ bool) \ 'a list \ 'b option" where "find_map_filter f p [] = None" | "find_map_filter f p (a # as) = (let b = f a in if p b then Some b else find_map_filter f p as)" lemma find_map_filter_Some: "find_map_filter f p as = Some b \ p b \ b \ f ` set as" by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits) lemma find_map_filter_None: "find_map_filter f p as = None \ \ b \ f ` set as. \ p b" by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits) lemma remdups_adj_sorted_distinct[simp]: "sorted xs \ distinct (remdups_adj xs)" by (induct xs rule: remdups_adj.induct) (auto) lemma subseqs_length_simple: assumes "b \ set (subseqs xs)" shows "length b \ length xs" using assms by(induct xs arbitrary:b;auto simp:Let_def Suc_leD) lemma subseqs_length_simple_False: assumes "b \ set (subseqs xs)" " length xs < length b" shows False using assms subseqs_length_simple by fastforce lemma empty_subseqs[simp]: "[] \ set (subseqs xs)" by (induct xs, auto simp: Let_def) lemma full_list_subseqs: "{ys. ys \ set (subseqs xs) \ length ys = length xs} = {xs}" proof (induct xs) case (Cons x xs) have "?case = ({ys \ (#) x ` set (subseqs xs) \ set (subseqs xs). length ys = Suc (length xs)} = (#) x ` {xs})" (is "_ = (?l = ?r)") by (auto simp: Let_def) also have "?l = {ys \ (#) x ` set (subseqs xs). length ys = Suc (length xs)}" using length_subseqs[of xs] using subseqs_length_simple_False by force also have "\ = (#) x ` {ys \ set (subseqs xs). length ys = length xs}" by auto also have "\ = (#) x ` {xs}" unfolding Cons by auto finally show ?case by simp qed simp lemma nth_concat_split: assumes "i < length (concat xs)" shows "\ j k. j < length xs \ k < length (xs ! j) \ concat xs ! i = xs ! j ! k" using assms proof (induct xs arbitrary: i) case (Cons x xs i) define I where "I = i - length x" show ?case proof (cases "i < length x") case True note l = this hence i: "concat (Cons x xs) ! i = x ! i" by (auto simp: nth_append) show ?thesis unfolding i by (rule exI[of _ 0], rule exI[of _ i], insert Cons l, auto) next case False note l = this from l Cons(2) have i: "i = length x + I" "I < length (concat xs)" unfolding I_def by auto hence iI: "concat (Cons x xs) ! i = concat xs ! I" by (auto simp: nth_append) from Cons(1)[OF i(2)] obtain j k where IH: "j < length xs \ k < length (xs ! j) \ concat xs ! I = xs ! j ! k" by auto show ?thesis unfolding iI by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH, auto) qed qed simp lemma nth_concat_diff: assumes "i1 < length (concat xs)" "i2 < length (concat xs)" "i1 \ i2" shows "\ j1 k1 j2 k2. (j1,k1) \ (j2,k2) \ j1 < length xs \ j2 < length xs \ k1 < length (xs ! j1) \ k2 < length (xs ! j2) \ concat xs ! i1 = xs ! j1 ! k1 \ concat xs ! i2 = xs ! j2 ! k2" using assms proof (induct xs arbitrary: i1 i2) case (Cons x xs) define I1 where "I1 = i1 - length x" define I2 where "I2 = i2 - length x" show ?case proof (cases "i1 < length x") case True note l1 = this hence i1: "concat (Cons x xs) ! i1 = x ! i1" by (auto simp: nth_append) show ?thesis proof (cases "i2 < length x") case True note l2 = this hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append) show ?thesis unfolding i1 i2 by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ 0], rule exI[of _ i2], insert Cons(4) l1 l2, auto) next case False note l2 = this from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append) from nth_concat_split[OF i22(2)] obtain j2 k2 where *: "j2 < length xs \ k2 < length (xs ! j2) \ concat xs ! I2 = xs ! j2 ! k2" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ "Suc j2"], rule exI[of _ k2], insert * l1, auto) qed next case False note l1 = this from l1 Cons(2) have i11: "i1 = length x + I1" "I1 < length (concat xs)" unfolding I1_def by auto hence i1: "concat (Cons x xs) ! i1 = concat xs ! I1" by (auto simp: nth_append) show ?thesis proof (cases "i2 < length x") case False note l2 = this from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append) from Cons(4) i11 i22 have diff: "I1 \ I2" by auto from Cons(1)[OF i11(2) i22(2) diff] obtain j1 k1 j2 k2 where IH: "(j1,k1) \ (j2,k2) \ j1 < length xs \ j2 < length xs \ k1 < length (xs ! j1) \ k2 < length (xs ! j2) \ concat xs ! I1 = xs ! j1 ! k1 \ concat xs ! I2 = xs ! j2 ! k2" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ "Suc j2"], rule exI[of _ k2], insert IH, auto) next case True note l2 = this hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append) from nth_concat_split[OF i11(2)] obtain j1 k1 where *: "j1 < length xs \ k1 < length (xs ! j1) \ concat xs ! I1 = xs ! j1 ! k1" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ 0], rule exI[of _ i2], insert * l2, auto) qed qed qed auto lemma list_all2_map_map: "(\ x. x \ set xs \ R (f x) (g x)) \ list_all2 R (map f xs) (map g xs)" by (induct xs, auto) subsection \Partitions\ text \Check whether a list of sets forms a partition, i.e., whether the sets are pairwise disjoint.\ definition is_partition :: "('a set) list \ bool" where "is_partition cs \ (\ji cs ! j = {})" (* and an equivalent but more symmetric version *) definition is_partition_alt :: "('a set) list \ bool" where "is_partition_alt cs \ (\ i j. i < length cs \ j < length cs \ i \ j \ cs!i \ cs!j = {})" lemma is_partition_alt: "is_partition = is_partition_alt" proof (intro ext) fix cs :: "'a set list" { assume "is_partition_alt cs" hence "is_partition cs" unfolding is_partition_def is_partition_alt_def by auto } moreover { assume part: "is_partition cs" have "is_partition_alt cs" unfolding is_partition_alt_def proof (intro allI impI) fix i j assume "i < length cs \ j < length cs \ i \ j" with part show "cs ! i \ cs ! j = {}" unfolding is_partition_def by (cases "i < j", simp, cases "j < i", force, simp) qed } ultimately show "is_partition cs = is_partition_alt cs" by auto qed lemma is_partition_Nil: "is_partition [] = True" unfolding is_partition_def by auto lemma is_partition_Cons: "is_partition (x#xs) \ is_partition xs \ x \ \(set xs) = {}" (is "?l = ?r") proof assume ?l have one: "is_partition xs" proof (unfold is_partition_def, intro allI impI) fix j i assume "j < length xs" and "i < j" hence "Suc j < length(x#xs)" and "Suc i < Suc j" by auto from \?l\[unfolded is_partition_def,THEN spec,THEN mp,THEN spec,THEN mp,OF this] have "(x#xs)!(Suc i) \ (x#xs)!(Suc j) = {}" . thus "xs!i \ xs!j = {}" by simp qed have two: "x \ \(set xs) = {}" proof (rule ccontr) assume "x \ \(set xs) \ {}" then obtain y where "y \ x" and "y \ \(set xs)" by auto then obtain z where "z \ set xs" and "y \ z" by auto then obtain i where "i < length xs" and "xs!i = z" using in_set_conv_nth[of z xs] by auto with \y \ z\ have "y \ (x#xs)!Suc i" by auto moreover with \y \ x\ have "y \ (x#xs)!0" by simp ultimately have "(x#xs)!0 \ (x#xs)!Suc i \ {}" by auto moreover from \i < length xs\ have "Suc i < length(x#xs)" by simp ultimately show False using \?l\[unfolded is_partition_def] by best qed from one two show ?r .. next assume ?r show ?l proof (unfold is_partition_def, intro allI impI) fix j i assume j: "j < length (x # xs)" assume i: "i < j" from i obtain j' where j': "j = Suc j'" by (cases j, auto) with j have j'len: "j' < length xs" and j'elem: "(x # xs) ! j = xs ! j'" by auto show "(x # xs) ! i \ (x # xs) ! j = {}" proof (cases i) case 0 with j'elem have "(x # xs) ! i \ (x # xs) ! j = x \ xs ! j'" by auto also have "\ \ x \ \(set xs)" using j'len by force finally show ?thesis using \?r\ by auto next case (Suc i') with i j' have i'j': "i' < j'" by auto from Suc j' have "(x # xs) ! i \ (x # xs) ! j = xs ! i' \ xs ! j'" by auto with \?r\ i'j' j'len show ?thesis unfolding is_partition_def by auto qed qed qed lemma is_partition_sublist: assumes "is_partition (us @ xs @ ys @ zs @ vs)" shows "is_partition (xs @ zs)" proof (rule ccontr) assume "\ is_partition (xs @ zs)" then obtain i j where j:"j < length (xs @ zs)" and i:"i < j" and *:"(xs @ zs) ! i \ (xs @ zs) ! j \ {}" unfolding is_partition_def by blast then show False proof (cases "j < length xs") case True let ?m = "j + length us" let ?n = "i + length us" from True have "?m < length (us @ xs @ ys @ zs @ vs)" by auto moreover from i have "?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n \ (us @ xs @ ys @ zs @ vs) ! ?m \ {}" using i True * nth_append by (metis (no_types, lifting) add_diff_cancel_right' not_add_less2 order.strict_trans) ultimately show False using assms unfolding is_partition_def by auto next case False let ?m = "j + length us + length ys" from j have m:"?m < length (us @ xs @ ys @ zs @ vs)" by auto have mj:"(us @ (xs @ ys @ zs @ vs)) ! ?m = (xs @ zs) ! j" unfolding nth_append using False j by auto show False proof (cases "i < length xs") case True let ?n = "i + length us" from i have "?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" by (simp add: True nth_append) ultimately show False using * m assms mj unfolding is_partition_def by blast next case False let ?n = "i + length us + length ys" from i have i:"?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" unfolding nth_append using False i j less_diff_conv2 by auto ultimately show False using * m assms mj unfolding is_partition_def by blast qed qed qed lemma is_partition_inj_map: assumes "is_partition xs" and "inj_on f (\x \ set xs. x)" shows "is_partition (map ((`) f) xs)" proof (rule ccontr) assume "\ is_partition (map ((`) f) xs)" then obtain i j where neq:"i \ j" and i:"i < length (map ((`) f) xs)" and j:"j < length (map ((`) f) xs)" and "map ((`) f) xs ! i \ map ((`) f) xs ! j \ {}" unfolding is_partition_alt is_partition_alt_def by auto then obtain x where "x \ map ((`) f) xs ! i" and "x \ map ((`) f) xs ! j" by auto then obtain y z where yi:"y \ xs ! i" and yx:"f y = x" and zj:"z \ xs ! j" and zx:"f z = x" using i j by auto show False proof (cases "y = z") case True with zj yi neq assms(1) i j show ?thesis by (auto simp: is_partition_alt is_partition_alt_def) next case False have "y \ (\x \ set xs. x)" using yi i by force moreover have "z \ (\x \ set xs. x)" using zj j by force ultimately show ?thesis using assms(2) inj_on_def[of f "(\x\set xs. x)"] False zx yx by blast qed qed context begin private fun is_partition_impl :: "'a set list \ 'a set option" where "is_partition_impl [] = Some {}" | "is_partition_impl (as # rest) = do { all \ is_partition_impl rest; if as \ all = {} then Some (all \ as) else None }" lemma is_partition_code[code]: "is_partition as = (is_partition_impl as \ None)" proof - note [simp] = is_partition_Cons is_partition_Nil have "\ bs. (is_partition as = (is_partition_impl as \ None)) \ (is_partition_impl as = Some bs \ bs = \ (set as))" proof (induct as) case (Cons as rest bs) show ?case proof (cases "is_partition rest") case False thus ?thesis using Cons by auto next case True with Cons obtain c where rest: "is_partition_impl rest = Some c" by (cases "is_partition_impl rest", auto) with Cons True show ?thesis by auto qed qed auto thus ?thesis by blast qed end lemma case_prod_partition: "case_prod f (partition p xs) = f (filter p xs) (filter (Not \ p) xs)" by simp lemmas map_id[simp] = list.map_id subsection \merging functions\ definition fun_merge :: "('a \ 'b)list \ 'a set list \ 'a \ 'b" where "fun_merge fs as a \ (fs ! (LEAST i. i < length as \ a \ as ! i)) a" lemma fun_merge: assumes i: "i < length as" and a: "a \ as ! i" and ident: "\ i j a. i < length as \ j < length as \ a \ as ! i \ a \ as ! j \ (fs ! i) a = (fs ! j) a" shows "fun_merge fs as a = (fs ! i) a" proof - let ?p = "\ i. i < length as \ a \ as ! i" let ?l = "LEAST i. ?p i" have p: "?p ?l" by (rule LeastI, insert i a, auto) show ?thesis unfolding fun_merge_def by (rule ident[OF _ i _ a], insert p, auto) qed lemma fun_merge_part: assumes part: "is_partition as" and i: "i < length as" and a: "a \ as ! i" shows "fun_merge fs as a = (fs ! i) a" proof(rule fun_merge[OF i a]) fix i j a assume "i < length as" and "j < length as" and "a \ as ! i" and "a \ as ! j" hence "i = j" using part[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto) thus "(fs ! i) a = (fs ! j) a" by simp qed lemma map_nth_conv: "map f ss = map g ts \ \i < length ss. f(ss!i) = g(ts!i)" proof (intro allI impI) fix i show "map f ss = map g ts \ i < length ss \ f(ss!i) = g(ts!i)" proof (induct ss arbitrary: i ts) case Nil thus ?case by (induct ts) auto next case (Cons s ss) thus ?case by (induct ts, simp, (cases i, auto)) qed qed lemma distinct_take_drop: assumes dist: "distinct vs" and len: "i < length vs" shows "distinct(take i vs @ drop (Suc i) vs)" (is "distinct(?xs@?ys)") proof - from id_take_nth_drop[OF len] have vs[symmetric]: "vs = ?xs @ vs!i # ?ys" . with dist have "distinct ?xs" and "distinct(vs!i#?ys)" and "set ?xs \ set(vs!i#?ys) = {}" using distinct_append[of ?xs "vs!i#?ys"] by auto hence "distinct ?ys" and "set ?xs \ set ?ys = {}" by auto with \distinct ?xs\ show ?thesis using distinct_append[of ?xs ?ys] vs by simp qed lemma map_nth_eq_conv: assumes len: "length xs = length ys" shows "(map f xs = ys) = (\i i < length ys. f (xs ! i) = id (ys ! i))" using map_nth_conv[of f xs id ys] nth_map_conv[OF len, of f id] unfolding len by blast finally show ?thesis by auto qed lemma map_upt_len_conv: "map (\ i . f (xs!i)) [0.. i. f (a + i)) [0.. 'a list \ 'a list list" where "generate_lists n xs \ concat_lists (map (\ _. xs) [0 ..< n])" lemma set_generate_lists[simp]: "set (generate_lists n xs) = {as. length as = n \ set as \ set xs}" proof - { fix as have "(length as = n \ (\i set xs)) = (length as = n \ set as \ set xs)" proof - { assume "length as = n" hence n: "n = length as" by auto have "(\i set xs) = (set as \ set xs)" unfolding n unfolding all_set_conv_all_nth[of as "\ x. x \ set xs", symmetric] by auto } thus ?thesis by auto qed } thus ?thesis unfolding generate_lists_def unfolding set_concat_lists by auto qed lemma nth_append_take: assumes "i \ length xs" shows "(take i xs @ y#ys)!i = y" proof - from assms have a: "length(take i xs) = i" by simp have "(take i xs @ y#ys)!(length(take i xs)) = y" by (rule nth_append_length) thus ?thesis unfolding a . qed lemma nth_append_take_is_nth_conv: assumes "i < j" and "j \ length xs" shows "(take j xs @ ys)!i = xs!i" proof - from assms have "i < length(take j xs)" by simp hence "(take j xs @ ys)!i = take j xs ! i" unfolding nth_append by simp thus ?thesis unfolding nth_take[OF assms(1)] . qed lemma nth_append_drop_is_nth_conv: assumes "j < i" and "j \ length xs" and "i \ length xs" shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i" proof - from \j < i\ obtain n where ij: "Suc(j + n) = i" using less_imp_Suc_add by auto with assms have i: "i = length(take j xs) + Suc n" by auto have len: "Suc j + n \ length xs" using assms i by auto have "(take j xs @ y # drop (Suc j) xs)!i = (y # drop (Suc j) xs)!(i - length(take j xs))" unfolding nth_append i by auto also have "\ = (y # drop (Suc j) xs)!(Suc n)" unfolding i by simp also have "\ = (drop (Suc j) xs)!n" by simp finally show ?thesis using ij len by simp qed lemma nth_append_take_drop_is_nth_conv: assumes "i \ length xs" and "j \ length xs" and "i \ j" shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i" proof - from assms have "i < j \ i > j" by auto thus ?thesis using assms by (auto simp: nth_append_take_is_nth_conv nth_append_drop_is_nth_conv) qed lemma take_drop_imp_nth: "\take i ss @ x # drop (Suc i) ss = ss\ \ x = ss!i" proof (induct ss arbitrary: i) case (Cons s ss) from \take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss)\ show ?case proof (induct i) case (Suc i) from Cons have IH: "take i ss @ x # drop (Suc i) ss = ss \ x = ss!i" by auto from Suc have "take i ss @ x # drop (Suc i) ss = ss" by auto with IH show ?case by auto qed auto qed auto lemma take_drop_update_first: assumes "j < length ds" and "length cs = length ds" shows "(take j ds @ drop j cs)[j := ds ! j] = take (Suc j) ds @ drop (Suc j) cs" using assms proof (induct j arbitrary: ds cs) case 0 then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) show ?case unfolding ds cs by auto next case (Suc j) then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto qed lemma take_drop_update_second: assumes "j < length ds" and "length cs = length ds" shows "(take j ds @ drop j cs)[j := cs ! j] = take j ds @ drop j cs" using assms proof (induct j arbitrary: ds cs) case 0 then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) show ?case unfolding ds cs by auto next case (Suc j) then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto qed lemma nth_take_prefix: "length ys \ length xs \ \i < length ys. xs!i = ys!i \ take (length ys) xs = ys" proof (induct xs ys rule: list_induct2') case (4 x xs y ys) have "take (length ys) xs = ys" by (rule 4(1), insert 4(2-3), auto) moreover from 4(3) have "x = y" by auto ultimately show ?case by auto qed auto lemma take_upt_idx: assumes i: "i < length ls" shows "take i ls = [ ls ! j . j \ [0.. i" by auto show ?thesis using take_upt[OF e] take_map map_nth by (metis (opaque_lifting, no_types) add.left_neutral i nat_less_le take_upt) qed fun distinct_eq :: "('a \ 'a \ bool) \ 'a list \ bool" where "distinct_eq _ [] = True" | "distinct_eq eq (x # xs) = ((\ y \ set xs. \ (eq y x)) \ distinct_eq eq xs)" lemma distinct_eq_append: "distinct_eq eq (xs @ ys) = (distinct_eq eq xs \ distinct_eq eq ys \ (\ x \ set xs. \ y \ set ys. \ (eq y x)))" by (induct xs, auto) lemma append_Cons_nth_left: assumes "i < length xs" shows "(xs @ u # ys) ! i = xs ! i" using assms nth_append[of xs _ i] by simp lemma append_Cons_nth_middle: assumes "i = length xs" shows "(xs @ y # zs) ! i = y" using assms by auto lemma append_Cons_nth_right: assumes "i > length xs" shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i" -proof - - from assms have "i - length xs > 0" by auto - then obtain j where j: "i - length xs = Suc j" by (cases "i - length xs", auto) - thus ?thesis by (simp add: nth_append) -qed + by (simp add: assms nth_append) lemma append_Cons_nth_not_middle: assumes "i \ length xs" shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i" -proof (cases "i < length xs") - case True - thus ?thesis by (simp add: append_Cons_nth_left) -next - case False - with assms have "i > length xs" by arith - thus ?thesis by (rule append_Cons_nth_right) -qed + by (metis assms list_update_length nth_list_update_neq) lemmas append_Cons_nth = append_Cons_nth_middle append_Cons_nth_not_middle lemma concat_all_nth: assumes "length xs = length ys" and "\i. i < length xs \ length (xs ! i) = length (ys ! i)" and "\i j. i < length xs \ j < length (xs ! i) \ P (xs ! i ! j) (ys ! i ! j)" shows "\k j. j < length x \ P (x ! j) (y ! j)" by auto { fix i assume i: "i < length xs" with Cons(3)[of "Suc i"] have len: "length (xs ! i) = length (ys ! i)" by simp from Cons(4)[of "Suc i"] i have "\ j. j < length (xs ! i) \ P (xs ! i ! j) (ys ! i ! j)" by auto note len and this } from Cons(2)[OF this] have ind: "\ k. k < length (concat xs) \ P (concat xs ! k) (concat ys ! k)" by auto show ?case unfolding concat.simps proof (intro allI impI) fix k assume k: "k < length (x @ concat xs)" show "P ((x @ concat xs) ! k) ((y @ concat ys) ! k)" proof (cases "k < length x") case True show ?thesis unfolding nth_append using True xy pxy[OF True] by simp next case False with k have "k - (length x) < length (concat xs)" by auto then obtain n where n: "k - length x = n" and nxs: "n < length (concat xs)" by auto show ?thesis unfolding nth_append n n[unfolded xy] using False xy ind[OF nxs] by auto qed qed qed auto lemma eq_length_concat_nth: assumes "length xs = length ys" and "\i. i < length xs \ length (xs ! i) = length (ys ! i)" shows "length (concat xs) = length (concat ys)" using assms proof (induct xs ys rule: list_induct2) case (Cons x xs y ys) from Cons(3)[of 0] have xy: "length x = length y" by simp { fix i assume "i < length xs" with Cons(3)[of "Suc i"] have "length (xs ! i) = length (ys ! i)" by simp } from Cons(2)[OF this] have ind: "length (concat xs) = length (concat ys)" by simp show ?case using xy ind by auto qed auto primrec list_union :: "'a list \ 'a list \ 'a list" where "list_union [] ys = ys" | "list_union (x # xs) ys = (let zs = list_union xs ys in if x \ set zs then zs else x # zs)" lemma set_list_union[simp]: "set (list_union xs ys) = set xs \ set ys" proof (induct xs) case (Cons x xs) thus ?case by (cases "x \ set (list_union xs ys)") (auto) qed simp declare list_union.simps[simp del] (*Why was list_inter thrown out of List.thy?*) fun list_inter :: "'a list \ 'a list \ 'a list" where "list_inter [] bs = []" | "list_inter (a#as) bs = (if a \ set bs then a # list_inter as bs else list_inter as bs)" lemma set_list_inter[simp]: "set (list_inter xs ys) = set xs \ set ys" by (induct rule: list_inter.induct) simp_all declare list_inter.simps[simp del] primrec list_diff :: "'a list \ 'a list \ 'a list" where "list_diff [] ys = []" | "list_diff (x # xs) ys = (let zs = list_diff xs ys in if x \ set ys then zs else x # zs)" lemma set_list_diff[simp]: "set (list_diff xs ys) = set xs - set ys" proof (induct xs) case (Cons x xs) thus ?case by (cases "x \ set ys") (auto) qed simp declare list_diff.simps[simp del] -lemma nth_drop_0: "0 < length ss \ (ss!0)#drop (Suc 0) ss = ss" by (induct ss) auto +lemma nth_drop_0: "0 < length ss \ (ss!0)#drop (Suc 0) ss = ss" + by (simp add: Cons_nth_drop_Suc) lemma set_foldr_remdups_set_map_conv[simp]: "set (foldr (\x xs. remdups (f x @ xs)) xs []) = \(set (map (set \ f) xs))" by (induct xs) auto lemma subset_set_code[code_unfold]: "set xs \ set ys \ list_all (\x. x \ set ys) xs" unfolding list_all_iff by auto fun union_list_sorted where "union_list_sorted (x # xs) (y # ys) = (if x = y then x # union_list_sorted xs ys else if x < y then x # union_list_sorted xs (y # ys) else y # union_list_sorted (x # xs) ys)" | "union_list_sorted [] ys = ys" | "union_list_sorted xs [] = xs" lemma [simp]: "set (union_list_sorted xs ys) = set xs \ set ys" by (induct xs ys rule: union_list_sorted.induct, auto) fun subtract_list_sorted :: "('a :: linorder) list \ 'a list \ 'a list" where "subtract_list_sorted (x # xs) (y # ys) = (if x = y then subtract_list_sorted xs (y # ys) else if x < y then x # subtract_list_sorted xs (y # ys) else subtract_list_sorted (x # xs) ys)" | "subtract_list_sorted [] ys = []" | "subtract_list_sorted xs [] = xs" lemma set_subtract_list_sorted[simp]: "sorted xs \ sorted ys \ set (subtract_list_sorted xs ys) = set xs - set ys" proof (induct xs ys rule: subtract_list_sorted.induct) case (1 x xs y ys) have xxs: "sorted (x # xs)" by fact have yys: "sorted (y # ys)" by fact have xs: "sorted xs" using xxs by (simp) show ?case proof (cases "x = y") case True thus ?thesis using 1(1)[OF True xs yys] by auto next case False note neq = this note IH = 1(2-3)[OF this] show ?thesis by (cases "x < y", insert IH xxs yys False, auto) qed qed auto lemma subset_subtract_listed_sorted: "set (subtract_list_sorted xs ys) \ set xs" by (induct xs ys rule: subtract_list_sorted.induct, auto) lemma set_subtract_list_distinct[simp]: "distinct xs \ distinct (subtract_list_sorted xs ys)" by (induct xs ys rule: subtract_list_sorted.induct, insert subset_subtract_listed_sorted, auto) definition "remdups_sort xs = remdups_adj (sort xs)" lemma remdups_sort[simp]: "sorted (remdups_sort xs)" "set (remdups_sort xs) = set xs" "distinct (remdups_sort xs)" by (simp_all add: remdups_sort_def) text \maximum and minimum\ lemma max_list_mono: assumes "\ x. x \ set xs - set ys \ \ y. y \ set ys \ x \ y" shows "max_list xs \ max_list ys" using assms proof (induct xs) case (Cons x xs) have "x \ max_list ys" proof (cases "x \ set ys") case True from max_list[OF this] show ?thesis . next case False with Cons(2)[of x] obtain y where y: "y \ set ys" and xy: "x \ y" by auto from xy max_list[OF y] show ?thesis by arith qed moreover have "max_list xs \ max_list ys" by (rule Cons(1)[OF Cons(2)], auto) ultimately show ?case by auto qed auto fun min_list :: "('a :: linorder) list \ 'a" where "min_list [x] = x" | "min_list (x # xs) = min x (min_list xs)" lemma min_list: "(x :: 'a :: linorder) \ set xs \ min_list xs \ x" proof (induct xs) case oCons : (Cons y ys) show ?case proof (cases ys) case Nil thus ?thesis using oCons by auto next case (Cons z zs) - hence id: "min_list (y # ys) = min y (min_list ys)" + hence "min_list (y # ys) = min y (min_list ys)" by auto - show ?thesis - proof (cases "x = y") - case True - show ?thesis unfolding id True by auto - next - case False - have "min y (min_list ys) \ min_list ys" by auto - also have "... \ x" using oCons False by auto - finally show ?thesis unfolding id . - qed + then show ?thesis + using min_le_iff_disj oCons.hyps oCons.prems by auto qed qed simp lemma min_list_Cons: assumes xy: "x \ y" and len: "length xs = length ys" and xsys: "min_list xs \ min_list ys" shows "min_list (x # xs) \ min_list (y # ys)" -proof (cases xs) - case Nil - with len have ys: "ys = []" by simp - with xy Nil show ?thesis by simp -next - case (Cons x' xs') - with len obtain y' ys' where ys: "ys = y' # ys'" by (cases ys, auto) - from Cons have one: "min_list (x # xs) = min x (min_list xs)" by auto - from ys have two: "min_list (y # ys) = min y (min_list ys)" by auto - show ?thesis unfolding one two using xy xsys - unfolding min_def by auto -qed + by (metis min_list.simps len length_greater_0_conv min.mono nth_drop_0 xsys xy) lemma min_list_nth: assumes "length xs = length ys" and "\i. i < length ys \ xs ! i \ ys ! i" shows "min_list xs \ min_list ys" using assms proof (induct xs arbitrary: ys) case (Cons x xs zs) from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto) note Cons = Cons[unfolded zs] from Cons(2) have len: "length xs = length ys" by simp from Cons(3)[of 0] have xy: "x \ y" by simp { fix i assume "i < length xs" with Cons(3)[of "Suc i"] Cons(2) have "xs ! i \ ys ! i" by simp } from Cons(1)[OF len this] Cons(2) have ind: "min_list xs \ min_list ys" by simp show ?case unfolding zs by (rule min_list_Cons[OF xy len ind]) qed auto lemma min_list_ex: assumes "xs \ []" shows "\x\set xs. min_list xs = x" using assms proof (induct xs) case oCons : (Cons x xs) show ?case proof (cases xs) case (Cons y ys) hence id: "min_list (x # xs) = min x (min_list xs)" and nNil: "xs \ []" by auto show ?thesis proof (cases "x \ min_list xs") case True show ?thesis unfolding id by (rule bexI[of _ x], insert True, auto simp: min_def) next case False show ?thesis unfolding id min_def using oCons(1)[OF nNil] False by auto qed qed auto qed auto lemma min_list_subset: assumes subset: "set ys \ set xs" and mem: "min_list xs \ set ys" shows "min_list xs = min_list ys" -proof - - from subset mem have "xs \ []" by auto - from min_list_ex[OF this] obtain x where x: "x \ set xs" and mx: "min_list xs = x" by auto - from min_list[OF mem] have two: "min_list ys \ min_list xs" by auto - from mem have "ys \ []" by auto - from min_list_ex[OF this] obtain y where y: "y \ set ys" and my: "min_list ys = y" by auto - from y subset have "y \ set xs" by auto - from min_list[OF this] have one: "min_list xs \ y" by auto - from one two - show ?thesis unfolding mx my by auto -qed + by (metis antisym empty_iff empty_set mem min_list min_list_ex subset subsetD) text\Apply a permutation to a list.\ primrec permut_aux :: "'a list \ (nat \ nat) \ 'a list \ 'a list" where "permut_aux [] _ _ = []" | "permut_aux (a # as) f bs = (bs ! f 0) # (permut_aux as (\n. f (Suc n)) bs)" definition permut :: "'a list \ (nat \ nat) \ 'a list" where "permut as f = permut_aux as f as" declare permut_def[simp] lemma permut_aux_sound: assumes "i < length as" shows "permut_aux as f bs ! i = bs ! (f i)" using assms proof (induct as arbitrary: i f bs) case (Cons x xs) show ?case proof (cases i) case (Suc j) with Cons(2) have "j < length xs" by simp from Cons(1)[OF this] and Suc show ?thesis by simp qed simp qed simp lemma permut_sound: assumes "i < length as" shows "permut as f ! i = as ! (f i)" using assms and permut_aux_sound by simp lemma permut_aux_length: assumes "bij_betw f {.. 'a) \ ('a \ 'a) \ 'a \ 'a" (infixl "\" 55) assumes "\f g h. f \ (g \ h) = f \ g \ h" shows "foldl (\) (x \ y) zs = x \ foldl (\) y zs" using assms[symmetric] by (induct zs arbitrary: y) simp_all lemma foldr_assoc: assumes "\f g h. b (b f g) h = b f (b g h)" shows "foldr b xs (b y z) = b (foldr b xs y) z" using assms by (induct xs) simp_all lemma foldl_foldr_o_id: "foldl (\) id fs = foldr (\) fs id" proof (induct fs) case (Cons f fs) have "id \ f = f \ id" by simp with Cons [symmetric] show ?case by (simp only: foldl_Cons foldr_Cons o_apply [of _ _ id] foldl_assoc o_assoc) qed simp lemma foldr_o_o_id[simp]: "foldr ((\) \ f) xs id a = foldr f xs a" by (induct xs) simp_all lemma Ex_list_of_length_P: assumes "\ix. P x i" shows "\xs. length xs = n \ (\i i. \ x. i < n \ P x i" by simp from choice[OF this] obtain xs where xs: "\ i. i < n \ P (xs i) i" by auto show ?thesis by (rule exI[of _ "map xs [0 ..< n]"], insert xs, auto) qed lemma ex_set_conv_ex_nth: "(\x\set xs. P x) = (\i set (zip xs ys)" shows "f x = f y" using assms proof (induct xs arbitrary: ys) case (Cons x xs) then show ?case by (cases ys) auto qed simp fun span :: "('a \ bool) \ 'a list \ 'a list \ 'a list" where "span P (x # xs) = (if P x then let (ys, zs) = span P xs in (x # ys, zs) else ([], x # xs))" | "span _ [] = ([], [])" lemma span[simp]: "span P xs = (takeWhile P xs, dropWhile P xs)" by (induct xs, auto) declare span.simps[simp del] lemma parallel_list_update: assumes one_update: "\ xs i y. length xs = n \ i < n \ r (xs ! i) y \ p xs \ p (xs[i := y])" and init: "length xs = n" "p xs" and rel: "length ys = n" "\ i. i < n \ r (xs ! i) (ys ! i)" shows "p ys" proof - note len = rel(1) init(1) { fix i assume "i \ n" hence "p (take i ys @ drop i xs)" proof (induct i) case 0 with init show ?case by simp next case (Suc i) hence IH: "p (take i ys @ drop i xs)" by simp from Suc have i: "i < n" by simp let ?xs = "(take i ys @ drop i xs)" have "length ?xs = n" using i len by simp from one_update[OF this i _ IH, of "ys ! i"] rel(2)[OF i] i len show ?case by (simp add: nth_append take_drop_update_first) qed } from this[of n] show ?thesis using len by auto qed lemma nth_concat_two_lists: "i < length (concat (xs :: 'a list list)) \ length (ys :: 'b list list) = length xs \ (\ i. i < length xs \ length (ys ! i) = length (xs ! i)) \ \ j k. j < length xs \ k < length (xs ! j) \ (concat xs) ! i = xs ! j ! k \ (concat ys) ! i = ys ! j ! k" proof (induct xs arbitrary: i ys) case (Cons x xs i yys) then obtain y ys where yys: "yys = y # ys" by (cases yys, auto) note Cons = Cons[unfolded yys] from Cons(4)[of 0] have [simp]: "length y = length x" by simp show ?case proof (cases "i < length x") case True show ?thesis unfolding yys by (rule exI[of _ 0], rule exI[of _ i], insert True Cons(2-4), auto simp: nth_append) next case False let ?i = "i - length x" from False Cons(2-3) have "?i < length (concat xs)" "length ys = length xs" by auto note IH = Cons(1)[OF this] { fix i assume "i < length xs" with Cons(4)[of "Suc i"] have "length (ys ! i) = length (xs ! i)" by simp } from IH[OF this] obtain j k where IH1: "j < length xs" "k < length (xs ! j)" "concat xs ! ?i = xs ! j ! k" "concat ys ! ?i = ys ! j ! k" by auto show ?thesis unfolding yys by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH1 False, auto simp: nth_append) qed qed simp text \Removing duplicates w.r.t. some function.\ fun remdups_gen :: "('a \ 'b) \ 'a list \ 'a list" where "remdups_gen f [] = []" | "remdups_gen f (x # xs) = x # remdups_gen f [y <- xs. \ f x = f y]" lemma remdups_gen_subset: "set (remdups_gen f xs) \ set xs" by (induct f xs rule: remdups_gen.induct, auto) lemma remdups_gen_elem_imp_elem: "x \ set (remdups_gen f xs) \ x \ set xs" using remdups_gen_subset[of f xs] by blast lemma elem_imp_remdups_gen_elem: "x \ set xs \ \ y \ set (remdups_gen f xs). f x = f y" proof (induct f xs rule: remdups_gen.induct) case (2 f z zs) show ?case proof (cases "f x = f z") case False with 2(2) have "x \ set [y\zs . f z \ f y]" by auto from 2(1)[OF this] show ?thesis by auto qed auto qed auto lemma take_nth_drop_concat: assumes "i < length xss" and "xss ! i = ys" and "j < length ys" and "ys ! j = z" shows "\k < length (concat xss). take k (concat xss) = concat (take i xss) @ take j ys \ concat xss ! k = xss ! i ! j \ drop (Suc k) (concat xss) = drop (Suc j) ys @ concat (drop (Suc i) xss)" using assms(1, 2) proof (induct xss arbitrary: i rule: List.rev_induct) case (snoc xs xss) then show ?case using assms by (cases "i < length xss") (auto simp: nth_append) qed simp lemma concat_map_empty [simp]: "concat (map (\_. []) xs) = []" by simp lemma map_upt_len_same_len_conv: assumes "length xs = length ys" shows "map (\i. f (xs ! i)) [0 ..< length ys] = map f xs" unfolding assms [symmetric] by (rule map_upt_len_conv) lemma concat_map_concat [simp]: "concat (map concat xs) = concat (concat xs)" by (induct xs) simp_all lemma concat_concat_map: "concat (concat (map f xs)) = concat (map (concat \ f) xs)" by (induct xs) simp_all lemma UN_upt_len_conv [simp]: "length xs = n \ (\i \ {0 ..< n}. f (xs ! i)) = \(set (map f xs))" by (force simp: in_set_conv_nth) lemma Ball_at_Least0LessThan_conv [simp]: "length xs = n \ (\i \ {0 ..< n}. P (xs ! i)) \ (\x \ set xs. P x)" by (metis atLeast0LessThan in_set_conv_nth lessThan_iff) lemma sum_list_replicate_length [simp]: "sum_list (replicate (length xs) (Suc 0)) = length xs" by (induct xs) simp_all lemma list_all2_in_set2: assumes "list_all2 P xs ys" and "y \ set ys" obtains x where "x \ set xs" and "P x y" using assms by (induct) auto lemma map_eq_conv': "map f xs = map g ys \ length xs = length ys \ (\i < length xs. f (xs ! i) = g (ys ! i))" -by (auto dest: map_eq_imp_length_eq map_nth_conv simp: nth_map_conv) + using map_equality_iff map_equality_iff nth_map_conv by auto lemma list_3_cases[case_names Nil 1 2]: assumes "xs = [] \ P" and "\x. xs = [x] \ P" and "\x y ys. xs = x#y#ys \ P" shows P - using assms by (cases xs; cases "tl xs", auto) + using assms by (rule remdups_adj.cases) lemma list_4_cases[case_names Nil 1 2 3]: assumes "xs = [] \ P" and "\x. xs = [x] \ P" and "\x y. xs = [x,y] \ P" and "\x y z zs. xs = x # y # z # zs \ P" shows P using assms by (cases xs; cases "tl xs"; cases "tl (tl xs)", auto) lemma foldr_append2 [simp]: "foldr ((@) \ f) xs (ys @ zs) = foldr ((@) \ f) xs ys @ zs" by (induct xs) simp_all lemma foldr_append2_Nil [simp]: "foldr ((@) \ f) xs [] @ zs = foldr ((@) \ f) xs zs" unfolding foldr_append2 [symmetric] by simp lemma UNION_set_zip: "(\x \ set (zip [0..i < length xs. g (i, f (xs ! i)))" -by (auto simp: set_conv_nth) + by (auto simp: set_conv_nth) lemma zip_fst: "p \ set (zip as bs) \ fst p \ set as" - by (cases p, rule set_zip_leftD, simp) + by (metis in_set_zipE prod.collapse) lemma zip_snd: "p \ set (zip as bs) \ snd p \ set bs" - by (cases p, rule set_zip_rightD, simp) + by (metis in_set_zipE prod.collapse) lemma zip_size_aux: "size_list (size o snd) (zip ts ls) \ (size_list size ls)" proof (induct ls arbitrary: ts) case (Cons l ls ts) thus ?case by (cases ts, auto) qed auto text\We definie the function that remove the nth element of a list. It uses take and drop and the soundness is therefore not too hard to prove thanks to the already existing lemmas.\ definition remove_nth :: "nat \ 'a list \ 'a list" where "remove_nth n xs \ (take n xs) @ (drop (Suc n) xs)" declare remove_nth_def[simp] lemma remove_nth_len: assumes i: "i < length xs" shows "length xs = Suc (length (remove_nth i xs))" proof - show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]] unfolding remove_nth_def by simp qed lemma remove_nth_length : assumes n_bd: "n < length xs" shows "length (remove_nth n xs) = length xs - 1" -proof- - from length_take have ll:"n < length xs \ length (take n xs) = n" by auto - from length_drop have lr: "length (drop (Suc n) xs) = length xs - (Suc n)" by simp - from ll and lr and length_append and n_bd show ?thesis by auto -qed + using n_bd by force lemma remove_nth_id : "length xs \ n \ remove_nth n xs = xs" -using take_all drop_all append_Nil2 by simp + by simp lemma remove_nth_sound_l : assumes p_ub: "p < n" shows "(remove_nth n xs) ! p = xs ! p" proof (cases "n < length xs") case True from length_take and True have ltk: "length (take n xs) = n" by simp { assume pltn: "p < n" from this and ltk have plttk: "p < length (take n xs)" by simp with nth_append[of "take n xs" _ p] have "((take n xs) @ (drop (Suc n) xs)) ! p = take n xs ! p" by auto with pltn and nth_take have "((take n xs) @ (drop (Suc n) xs)) ! p = xs ! p" by simp } from this and ltk and p_ub show ?thesis by simp next case False hence "length xs \ n" by arith with remove_nth_id show ?thesis by force qed lemma remove_nth_sound_r : assumes "n \ p" and "p < length xs" shows "(remove_nth n xs) ! p = xs ! (Suc p)" proof- from \n \ p\ and \p < length xs\ have n_ub: "n < length xs" by arith from length_take and n_ub have ltk: "length (take n xs) = n" by simp from \n \ p\ and ltk and nth_append[of "take n xs" _ p] have Hrew: "((take n xs) @ (drop (Suc n) xs)) ! p = drop (Suc n) xs ! (p - n)" by auto from \n \ p\ have idx: "Suc n + (p - n) = Suc p" by arith from \p < length xs\ have Sp_ub: "Suc p \ length xs" by arith from idx and Sp_ub and nth_drop have Hrew': "drop (Suc n) xs ! (p - n) = xs ! (Suc p)" by simp from Hrew and Hrew' show ?thesis by simp qed lemma nth_remove_nth_conv: assumes "i < length (remove_nth n xs)" shows "remove_nth n xs ! i = xs ! (if i < n then i else Suc i)" using assms remove_nth_sound_l remove_nth_sound_r[of n i xs] by auto lemma remove_nth_P_compat : assumes aslbs: "length as = length bs" and Pab: "\i. i < length as \ P (as ! i) (bs ! i)" shows "\i. i < length (remove_nth p as) \ P (remove_nth p as ! i) (remove_nth p bs ! i)" proof (cases "p < length as") case True hence p_ub: "p < length as" by assumption with remove_nth_length have lr_ub: "length (remove_nth p as) = length as - 1" by auto { fix i assume i_ub: "i < length (remove_nth p as)" have "P (remove_nth p as ! i) (remove_nth p bs ! i)" proof (cases "i < p") case True from i_ub and lr_ub have i_ub2: "i < length as" by arith from i_ub2 and Pab have P: "P (as ! i) (bs ! i)" by blast from P and remove_nth_sound_l[OF True, of as] and remove_nth_sound_l[OF True, of bs] show ?thesis by simp next case False hence p_ub2: "p \ i" by arith from i_ub and lr_ub have Si_ub: "Suc i < length as" by arith with Pab have P: "P (as ! Suc i) (bs ! Suc i)" by blast from i_ub and lr_ub have i_uba: "i < length as" by arith from i_uba and aslbs have i_ubb: "i < length bs" by simp from P and p_ub and aslbs and remove_nth_sound_r[OF p_ub2 i_uba] and remove_nth_sound_r[OF p_ub2 i_ubb] show ?thesis by auto qed } thus ?thesis by simp next case False hence p_lba: "length as \ p" by arith with aslbs have p_lbb: "length bs \ p" by simp from remove_nth_id[OF p_lba] and remove_nth_id[OF p_lbb] and Pab show ?thesis by simp qed declare remove_nth_def[simp del] definition adjust_idx :: "nat \ nat \ nat" where "adjust_idx i j \ (if j < i then j else (Suc j))" definition adjust_idx_rev :: "nat \ nat \ nat" where "adjust_idx_rev i j \ (if j < i then j else j - Suc 0)" lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j" - unfolding adjust_idx_def adjust_idx_rev_def by (cases "i < j", auto) + using adjust_idx_def adjust_idx_rev_def by auto lemma adjust_idx_rev2: assumes "j \ i" shows "adjust_idx i (adjust_idx_rev i j) = j" - unfolding adjust_idx_def adjust_idx_rev_def using assms by (cases "i < j", auto) + using adjust_idx_def adjust_idx_rev_def assms by auto lemma adjust_idx_i: "adjust_idx i j \ i" - unfolding adjust_idx_def by (cases "j < i", auto) + using adjust_idx_def lessI less_irrefl_nat by auto lemma adjust_idx_nth: assumes i: "i < length xs" shows "remove_nth i xs ! j = xs ! adjust_idx i j" (is "?l = ?r") proof - let ?j = "adjust_idx i j" from i have ltake: "length (take i xs) = i" by simp note nth_xs = arg_cong[where f = "\ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake] show ?thesis proof (cases "j < i") case True hence j: "?j = j" unfolding adjust_idx_def by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake using True by simp next case False hence j: "?j = Suc j" unfolding adjust_idx_def by simp from i have lxs: "min (length xs) i = i" by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append using False by (simp add: lxs) qed qed lemma adjust_idx_rev_nth: assumes i: "i < length xs" and ji: "j \ i" shows "remove_nth i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r") -proof - - let ?j = "adjust_idx_rev i j" - from i have ltake: "length (take i xs) = i" by simp - note nth_xs = arg_cong[where f = "\ xs. xs ! j", OF id_take_nth_drop[OF i], unfolded nth_append ltake] - show ?thesis - proof (cases "j < i") - case True - hence j: "?j = j" unfolding adjust_idx_rev_def by simp - show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake - using True by simp - next - case False - with ji have ji: "j > i" by auto - hence j: "?j = j - Suc 0" unfolding adjust_idx_rev_def by simp - show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake - using ji by auto - qed -qed + by (simp add: adjust_idx_nth adjust_idx_rev2 i ji) lemma adjust_idx_length: assumes i: "i < length xs" and j: "j < length (remove_nth i xs)" shows "adjust_idx i j < length xs" - using j unfolding remove_nth_len[OF i] adjust_idx_def by (cases "j < i", auto) + using adjust_idx_def i j remove_nth_len by fastforce lemma adjust_idx_rev_length: assumes "i < length xs" and "j < length xs" and "j \ i" shows "adjust_idx_rev i j < length (remove_nth i xs)" - using assms by (cases "j < i") (simp_all add: adjust_idx_rev_def remove_nth_len[OF assms(1)]) + by (metis adjust_idx_def adjust_idx_rev2 assms not_less_eq remove_nth_len) text\If a binary relation holds on two couples of lists, then it holds on the concatenation of the two couples.\ lemma P_as_bs_extend: assumes lab: "length as = length bs" and lcd: "length cs = length ds" and nsab: "\i. i < length bs \ P (as ! i) (bs ! i)" and nscd: "\i. i < length ds \ P (cs ! i) (ds ! i)" shows "\i. i < length (bs @ ds) \ P ((as @ cs) ! i) ((bs @ ds) ! i)" -proof- - { - fix i - assume i_bd: "i < length (bs @ ds)" - have "P ((as @ cs) ! i) ((bs @ ds) ! i)" - proof (cases "i < length as") - case True - with nth_append and nsab and lab - show ?thesis by metis - next - case False - with lab and lcd and i_bd and length_append[of bs ds] - have "(i - length as) < length cs" by arith - with False and nth_append[of _ _ i] and lab and lcd - and nscd[rule_format] show ?thesis by metis - qed - } - thus ?thesis by clarify -qed + by (simp add: lab nsab nscd nth_append) text\Extension of filter and partition to binary relations.\ fun filter2 :: "('a \ 'b \ bool) \ 'a list \ 'b list \ ('a list \ 'b list)" where "filter2 P [] _ = ([], [])" | "filter2 P _ [] = ([], [])" | "filter2 P (a # as) (b # bs) = (if P a b then (a # fst (filter2 P as bs), b # snd (filter2 P as bs)) else filter2 P as bs)" lemma filter2_length: "length (fst (filter2 P as bs)) \ length (snd (filter2 P as bs))" proof (induct as arbitrary: bs) case Nil show ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases bs) case Nil thus ?thesis by simp next case (Cons b bs) thus ?thesis proof (cases "P a b") case True with Cons and IH show ?thesis by simp next case False with Cons and IH show ?thesis by simp qed qed qed lemma filter2_sound: "\i. i < length (fst (filter2 P as bs)) \ P (fst (filter2 P as bs) ! i) (snd (filter2 P as bs) ! i)" proof (induct as arbitrary: bs) case Nil thus ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases bs) case Nil thus ?thesis by simp next case (Cons b bs) thus ?thesis proof (cases "P a b") case False with Cons and IH show ?thesis by simp next case True { fix i assume i_bd: "i < length (fst (filter2 P (a # as) (b # bs)))" have "P (fst (filter2 P (a # as) (b # bs)) ! i) (snd (filter2 P (a # as) (b # bs)) ! i)" proof (cases i) case 0 with True show ?thesis by simp next case (Suc j) with i_bd and True have "j < length (fst (filter2 P as bs))" by auto with Suc and IH and True show ?thesis by simp qed } with Cons show ?thesis by simp qed qed qed definition partition2 :: "('a \ 'b \ bool) \ 'a list \ 'b list \ ('a list \ 'b list) \ ('a list \ 'b list)" where "partition2 P as bs \ ((filter2 P as bs) , (filter2 (\a b. \ (P a b)) as bs))" lemma partition2_sound_P: "\i. i < length (fst (fst (partition2 P as bs))) \ P (fst (fst (partition2 P as bs)) ! i) (snd (fst (partition2 P as bs)) ! i)" -proof- - from filter2_sound show ?thesis unfolding partition2_def by simp -qed + by (simp add: filter2_sound partition2_def) lemma partition2_sound_nP: "\i. i < length (fst (snd (partition2 P as bs))) \ - \ P (fst (snd (partition2 P as bs)) ! i) (snd (snd (partition2 P as bs)) ! i)" -proof- - from filter2_sound show ?thesis unfolding partition2_def by simp -qed + \ P (fst (snd (partition2 P as bs)) ! i) (snd (snd (partition2 P as bs)) ! i)" + by (metis filter2_sound partition2_def snd_conv) text\Membership decision function that actually returns the value of the index where the value can be found.\ fun mem_idx :: "'a \ 'a list \ nat Option.option" where "mem_idx _ [] = None" | "mem_idx x (a # as) = (if x = a then Some 0 else map_option Suc (mem_idx x as))" lemma mem_idx_sound_output: assumes "mem_idx x as = Some i" shows "i < length as \ as ! i = x" using assms proof (induct as arbitrary: i) case Nil thus ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases "x = a") case True with IH(2) show ?thesis by simp next case False note neq_x_a = this show ?thesis proof (cases "mem_idx x as") case None with IH(2) and neq_x_a show ?thesis by simp next case (Some j) with IH(2) and neq_x_a have "i = Suc j" by simp with IH(1) and Some show ?thesis by simp qed qed qed lemma mem_idx_sound_output2: assumes "mem_idx x as = Some i" shows "\j. j < i \ as ! j \ x" using assms proof (induct as arbitrary: i) case Nil thus ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases "x = a") case True with IH show ?thesis by simp next case False note neq_x_a = this show ?thesis proof (cases "mem_idx x as") case None with IH(2) and neq_x_a show ?thesis by simp next case (Some j) with IH(2) and neq_x_a have eq_i_Sj: "i = Suc j" by simp { fix k assume k_bd: "k < i" have "(a # as) ! k \ x" proof (cases k) case 0 with neq_x_a show ?thesis by simp next case (Suc l) with k_bd and eq_i_Sj have l_bd: "l < j" by arith with IH(1) and Some have "as ! l \ x" by simp with Suc show ?thesis by simp qed } thus ?thesis by simp qed qed qed lemma mem_idx_sound: "(x \ set as) = (\i. mem_idx x as = Some i)" proof (induct as) case Nil thus ?case by simp next case (Cons a as) note IH = this show ?case proof (cases "x = a") case True thus ?thesis by simp next case False { assume "x \ set (a # as)" with False have "x \ set as" by simp with IH obtain i where Some_i: "mem_idx x as = Some i" by auto with False have "mem_idx x (a # as) = Some (Suc i)" by simp hence "\i. mem_idx x (a # as) = Some i" by simp } moreover { assume "\i. mem_idx x (a # as) = Some i" then obtain i where Some_i: "mem_idx x (a # as) = Some i" by fast have "x \ set as" proof (cases i) case 0 with mem_idx_sound_output[OF Some_i] and False show ?thesis by simp next case (Suc j) with Some_i and False have "mem_idx x as = Some j" by simp hence "\i. mem_idx x as = Some i" by simp with IH show ?thesis by simp qed hence "x \ set (a # as)" by simp } ultimately show ?thesis by fast qed qed lemma mem_idx_sound2: "(x \ set as) = (mem_idx x as = None)" unfolding mem_idx_sound by auto lemma sum_list_replicate_mono: assumes "w1 \ (w2 :: nat)" shows "sum_list (replicate n w1) \ sum_list (replicate n w2)" proof (induct n) case (Suc n) thus ?case using \w1 \ w2\ by auto qed simp lemma all_gt_0_sum_list_map: assumes *: "\x. f x > (0::nat)" and x: "x \ set xs" and len: "1 < length xs" shows "f x < (\x\xs. f x)" using x len proof (induct xs) case (Cons y xs) show ?case proof (cases "y = x") case True with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto) next case False with Cons(2) have x: "x \ set xs" by auto then obtain z zs where xs: "xs = z # zs" by (cases xs, auto) show ?thesis proof (cases "length zs") case 0 with x xs *[of y] show ?thesis by auto next case (Suc n) with xs have "1 < length xs" by auto from Cons(1)[OF x this] show ?thesis by simp qed qed qed simp lemma finite_distinct: "finite { xs . distinct xs \ set xs = X}" (is "finite (?S X)") proof (cases "finite X") case False with finite_set have id: "?S X = {}" by auto show ?thesis unfolding id by auto next case True show ?thesis proof (induct rule: finite_induct[OF True]) case (2 x X) let ?L = "{0..< card (insert x X)} \ ?S X" from 2(3) have fin: "finite ?L" by auto let ?f = "\ (i,xs). take i xs @ x # drop i xs" show ?case proof (rule finite_surj[OF fin, of _ ?f], rule) fix xs assume "xs \ ?S (insert x X)" hence dis: "distinct xs" and set: "set xs = insert x X" by auto from distinct_card[OF dis] have len: "length xs = card (set xs)" by auto from set[unfolded set_conv_nth] obtain i where x: "x = xs ! i" and i: "i < length xs" by auto from i have min: "min (length xs) i = i" by simp let ?ys = "take i xs @ drop (Suc i) xs" from id_take_nth_drop[OF i] have xsi: "xs = take i xs @ xs ! i # drop (Suc i) xs" . also have "... = ?f (i,?ys)" unfolding split by (simp add: min x) finally have xs: "xs = ?f (i,?ys)" . show "xs \ ?f ` ?L" proof (rule image_eqI, rule xs, rule SigmaI) show "i \ {0.. set ?ys" using disxsi by auto from distinct_take_drop[OF dis i] have disys: "distinct ?ys" . have "insert x (set ?ys) = set xs" unfolding arg_cong[OF xsi, of set] x by simp hence "insert x (set ?ys) = insert x X" unfolding set by simp from this[unfolded insert_eq_iff[OF xys 2(2)]] show "?ys \ ?S X" using disys by auto qed qed qed simp qed lemma finite_distinct_subset: assumes "finite X" shows "finite { xs . distinct xs \ set xs \ X}" (is "finite (?S X)") proof - let ?X = "{ { xs. distinct xs \ set xs = Y} | Y. Y \ X}" have id: "?S X = \ ?X" by blast show ?thesis unfolding id proof (rule finite_Union) show "finite ?X" using assms by auto next fix M assume "M \ ?X" with finite_distinct show "finite M" by auto qed qed lemma map_of_filter: assumes "P x" shows "map_of [(x',y) \ ys. P x'] x = map_of ys x" proof (induct ys) case (Cons xy ys) obtain x' y where xy: "xy = (x',y)" by force show ?case - by (cases "x' = x", insert assms xy Cons, auto) + using assms local.Cons by auto qed simp -lemma set_subset_insertI: "set xs \ set (List.insert x xs)" by auto -lemma set_removeAll_subset: "set (removeAll x xs) \ set xs" by auto +lemma set_subset_insertI: "set xs \ set (List.insert x xs)" + by auto + +lemma set_removeAll_subset: "set (removeAll x xs) \ set xs" + by auto lemma map_of_append_Some: "map_of xs y = Some z \ map_of (xs @ ys) y = Some z" - by (induction xs) auto + by simp lemma map_of_append_None: "map_of xs y = None \ map_of (xs @ ys) y = map_of ys y" - by (induction xs) auto + by (simp add: map_add_def) end