diff --git a/thys/Card_Number_Partitions/Additions_to_Main.thy b/thys/Card_Number_Partitions/Additions_to_Main.thy --- a/thys/Card_Number_Partitions/Additions_to_Main.thy +++ b/thys/Card_Number_Partitions/Additions_to_Main.thy @@ -1,82 +1,82 @@ (* Author: Lukas Bulwahn *) section \Additions to Isabelle's Main Theories\ theory Additions_to_Main imports "HOL-Library.Multiset" begin subsection \Addition to Finite-Set Theory\ lemma bound_domain_and_range_impl_finitely_many_functions: "finite {f::nat\nat. (\i. f i \ n) \ (\i\m. f i = 0)}" proof (induct m) case 0 have eq: "{f. (\i. f i \ n) \ (\i. f i = 0)} = {(\_. 0)}" by auto from this show ?case by auto (subst eq; auto) next case (Suc m) let ?S = "(\(y, f). f(m := y)) ` ({0..n} \ {f. (\i. f i \ n) \ (\i\m. f i = 0)})" { fix g assume "\i. g i \ n" "\i\Suc m. g i = 0" from this have "g \ ?S" by (auto intro: image_eqI[where x="(g m, g(m:=0))"]) } from this have "{f. (\i. f i \ n) \ (\i\Suc m. f i = 0)} = ?S" by auto from this Suc show ?case by simp qed subsection \Addition to Set-Interval Theory\ lemma sum_atMost_remove_nat: assumes "k \ (n :: nat)" shows "(\i\n. f i) = f k + (\i\{..n}-{k}. f i)" using assms by (auto simp add: sum.remove[where x=k]) subsection \Additions to Multiset Theory\ lemma set_mset_Abs_multiset: - assumes "f \ multiset" + assumes "finite {x. f x > 0}" shows "set_mset (Abs_multiset f) = {x. f x > 0}" using assms unfolding set_mset_def by simp lemma sum_mset_sum_count: "sum_mset M = (\i\set_mset M. count M i * i)" proof (induct M) show "sum_mset {#} = (\i\set_mset {#}. count {#} i * i)" by simp next fix M x assume hyp: "sum_mset M = (\i\set_mset M. count M i * i)" show "sum_mset (add_mset x M) = (\i\set_mset (add_mset x M). count (add_mset x M) i * i)" proof (cases "x \# M") assume a: "\ x \# M" from this have "count M x = 0" by (meson count_inI) from \\ x \# M\ this hyp show ?thesis by (auto intro!: sum.cong) next assume "x \# M" have "sum_mset (add_mset x M) = (\i\set_mset M. count M i * i) + x" using hyp by simp also have "\ = (\i\set_mset M - {x}. count M i * i) + count M x * x + x" using \x \# M\ by (simp add: sum.remove[of _ x]) also have "\ = count (add_mset x M) x * x + (\i\set_mset (add_mset x M) - {x}. count (add_mset x M) i * i)" by simp also have "\ = (\i\set_mset (add_mset x M). count (add_mset x M) i * i)" using \x \# M\ by (simp add: sum.remove[of _ x]) finally show ?thesis . qed qed lemma sum_mset_eq_sum_on_supersets: assumes "finite A" "set_mset M \ A" shows "(\i\set_mset M. count M i * i) = (\i\A. count M i * i)" proof - note \finite A\ \set_mset M \ A\ moreover have "\i\A - set_mset M. count M i * i = 0" using count_inI by fastforce ultimately show ?thesis by (auto intro: sum.mono_neutral_cong_left) qed end diff --git a/thys/Card_Number_Partitions/Card_Number_Partitions.thy b/thys/Card_Number_Partitions/Card_Number_Partitions.thy --- a/thys/Card_Number_Partitions/Card_Number_Partitions.thy +++ b/thys/Card_Number_Partitions/Card_Number_Partitions.thy @@ -1,309 +1,309 @@ (* Author: Lukas Bulwahn *) section \Cardinality of Number Partitions\ theory Card_Number_Partitions imports Number_Partition begin subsection \The Partition Function\ fun Partition :: "nat \ nat \ nat" where "Partition 0 0 = 1" | "Partition 0 (Suc k) = 0" | "Partition (Suc m) 0 = 0" | "Partition (Suc m) (Suc k) = Partition m k + Partition (m - k) (Suc k)" lemma Partition_less: assumes "m < k" shows "Partition m k = 0" using assms by (induct m k rule: Partition.induct) auto lemma Partition_sum_Partition_diff: assumes "k \ m" shows "Partition m k = (\i\k. Partition (m - k) i)" using assms by (induct m k rule: Partition.induct) auto lemma Partition_parts1: "Partition (Suc m) (Suc 0) = 1" by (induct m) auto lemma Partition_diag: "Partition (Suc m) (Suc m) = 1" by (induct m) auto lemma Partition_diag1: "Partition (Suc (Suc m)) (Suc m) = 1" by (induct m) auto lemma Partition_parts2: shows "Partition m 2 = m div 2" proof (induct m rule: nat_less_induct) fix m assume hypothesis: "\n m = 1) \ m \ 2" by auto from this show "Partition m 2 = m div 2" proof assume "m = 0 \ m = 1" from this show ?thesis by (auto simp add: numerals(2)) next assume "2 \ m" from this obtain m' where m': "m = Suc (Suc m')" by (metis add_2_eq_Suc le_Suc_ex) from hypothesis this have "Partition m' 2 = m' div 2" by simp from this m' show ?thesis using Partition_parts1 Partition.simps(4)[of "Suc m'" "Suc 0"] div2_Suc_Suc by (simp add: numerals(2) del: Partition.simps) qed qed subsection \Cardinality of Number Partitions\ lemma set_rewrite1: "{p. p partitions Suc m \ sum p {..Suc m} = Suc k \ p 1 \ 0} = (\p. p(1 := p 1 + 1)) ` {p. p partitions m \ sum p {..m} = k}" (is "?S = ?T") proof { fix p assume assms: "p partitions Suc m" "sum p {..Suc m} = Suc k" "0 < p 1" have "p(1 := p 1 - 1) partitions m" using assms by (metis partitions_remove1 diff_Suc_1) moreover have "(\i\m. (p(1 := p 1 - 1)) i) = k" using assms by (metis count_remove1 diff_Suc_1) ultimately have "p(1 := p 1 - 1) \ {p. p partitions m \ sum p {..m} = k}" by simp moreover have "p = p(1 := p 1 - 1, 1 := (p(1 := p 1 - 1)) 1 + 1)" using \0 < p 1\ by auto ultimately have "p \ (\p. p(1 := p 1 + 1)) ` {p. p partitions m \ sum p {..m} = k}" by blast } from this show "?S \ ?T" by blast next { fix p assume assms: "p partitions m" "sum p {..m} = k" have "(p(1 := p 1 + 1)) partitions Suc m" (is ?g1) using assms by (metis partitions_insert1 Suc_eq_plus1 zero_less_one) moreover have "sum (p(1 := p 1 + 1)) {..Suc m} = Suc k" (is ?g2) using assms by (metis count_insert1 Suc_eq_plus1) moreover have "(p(1 := p 1 + 1)) 1 \ 0" (is ?g3) by auto ultimately have "?g1 \ ?g2 \ ?g3" by simp } from this show "?T \ ?S" by auto qed lemma set_rewrite2: "{p. p partitions m \ sum p {..m} = k \ p 1 = 0} = (\p. (\i. p (i - 1))) ` {p. p partitions (m - k) \ sum p {..m - k} = k}" (is "?S = ?T") proof { fix p assume assms: "p partitions m" "sum p {..m} = k" "p 1 = 0" have "(\i. p (i + 1)) partitions m - k" using assms partitions_decrease1 by blast moreover from assms have "sum (\i. p (i + 1)) {..m - k} = k" using assms count_decrease1 by blast ultimately have "(\i. p (i + 1)) \ {p. p partitions m - k \ sum p {..m - k} = k}" by simp moreover have "p = (\i. p ((i - 1) + 1))" proof (rule ext) fix i show "p i = p (i - 1 + 1)" using assms by (cases i) (auto elim!: partitionsE) qed ultimately have "p \ (\p. (\i. p (i - 1))) ` {p. p partitions m - k \ sum p {..m - k} = k}" by auto } from this show "?S \ ?T" by auto next { fix p assume assms: "p partitions m - k" "sum p {..m - k} = k" from assms have "(\i. p (i - 1)) partitions m" (is ?g1) using partitions_increase1 by blast moreover from assms have "(\i\m. p (i - 1)) = k" (is ?g2) using count_increase1 by blast moreover from assms have "p 0 = 0" (is ?g3) by (auto elim!: partitionsE) ultimately have "?g1 \ ?g2 \ ?g3" by simp } from this show "?T \ ?S" by auto qed theorem card_partitions_k_parts: "card {p. p partitions n \ (\i\n. p i) = k} = Partition n k" proof (induct n k rule: Partition.induct) case 1 have eq: "{p. p = (\x. 0) \ p 0 = 0} = {(\x. 0)}" by auto show "card {p. p partitions 0 \ sum p {..0} = 0} = Partition 0 0" by (simp add: partitions_zero eq) next case (2 k) have eq: "{p. p = (\x. 0) \ p 0 = Suc k} = {}" by auto show "card {p. p partitions 0 \ sum p {..0} = Suc k} = Partition 0 (Suc k)" by (simp add: partitions_zero eq) next case (3 m) have eq: "{p. p partitions Suc m \ sum p {..Suc m} = 0} = {}" by (fastforce elim!: partitionsE simp add: le_Suc_eq) from this show "card {p. p partitions Suc m \ sum p {..Suc m} = 0} = Partition (Suc m) 0" by (simp only: Partition.simps card.empty) next case (4 m k) let ?set1 = "{p. p partitions Suc m \ sum p {..Suc m} = Suc k \ p 1 \ 0}" let ?set2 = "{p. p partitions Suc m \ sum p {..Suc m} = Suc k \ p 1 = 0}" have "finite {p. p partitions Suc m}" by (simp add: finite_partitions) from this have finite_sets: "finite ?set1" "finite ?set2" by simp+ have set_eq: "{p. p partitions Suc m \ sum p {..Suc m} = Suc k} = ?set1 \ ?set2" by auto have disjoint: "?set1 \ ?set2 = {}" by auto have inj1: "inj_on (\p. p(1 := p 1 + 1)) {p. p partitions m \ sum p {..m} = k}" by (auto intro!: inj_onI) (metis diff_Suc_1 fun_upd_idem_iff fun_upd_upd) have inj2: "inj_on (\p i. p (i - 1)) {p. p partitions m - k \ sum p {..m - k} = Suc k}" by (auto intro!: inj_onI simp add: fun_eq_iff) (metis add_diff_cancel_right') have card1: "card ?set1 = Partition m k" using inj1 4(1) by (simp only: set_rewrite1 card_image) have card2: "card ?set2 = Partition (m - k) (Suc k)" using inj2 4(2) by (simp only: set_rewrite2 card_image diff_Suc_Suc) have "card {p. p partitions Suc m \ sum p {..Suc m} = Suc k} = Partition m k + Partition (m - k) (Suc k)" using finite_sets disjoint by (simp only: set_eq card_Un_disjoint card1 card2) from this show "card {p. p partitions Suc m \ sum p {..Suc m} = Suc k} = Partition (Suc m) (Suc k)" by auto qed theorem card_partitions: "card {p. p partitions n} = (\k\n. Partition n k)" proof - have seteq: "{p. p partitions n} = \((\k. {p. p partitions n \ (\i\n. p i) = k}) ` {..n})" by (auto intro: partitions_parts_bounded) have finite: "\k. finite {p. p partitions n \ sum p {..n} = k}" by (simp add: finite_partitions) have "card {p. p partitions n} = card (\((\k. {p. p partitions n \ (\i\n. p i) = k}) ` {..n}))" using finite by (simp add: seteq) also have "... = (\x\n. card {p. p partitions n \ sum p {..n} = x})" using finite by (subst card_UN_disjoint) auto also have "... = (\k\n. Partition n k)" by (simp add: card_partitions_k_parts) finally show ?thesis . qed lemma card_partitions_atmost_k_parts: "card {p. p partitions n \ sum p {..n} \ k} = Partition (n + k) k" proof - have "card {p. p partitions n \ sum p {..n} \ k} = card (\((\k'. {p. p partitions n \ sum p {..n} = k'}) ` {..k}))" proof - have "{p. p partitions n \ sum p {..n} \ k} = (\k'\k. {p. p partitions n \ sum p {..n} = k'})" by auto from this show ?thesis by simp qed also have "card (\((\k'. {p. p partitions n \ sum p {..n} = k'}) ` {..k})) = sum (\k'. card {p. p partitions n \ sum p {..n} = k'}) {..k}" using finite_partitions_k_parts by (subst card_UN_disjoint) auto also have "\ = sum (\k'. Partition n k') {..k}" using card_partitions_k_parts by simp also have "\ = Partition (n + k) k" using Partition_sum_Partition_diff by simp finally show ?thesis . qed subsection \Cardinality of Number Partitions as Multisets of Natural Numbers\ lemma bij_betw_multiset_number_partition_with_size: "bij_betw count {N. number_partition n N \ size N = k} {p. p partitions n \ sum p {..n} = k}" proof (rule bij_betw_byWitness[where f'="Abs_multiset"]) show "\N\{N. number_partition n N \ size N = k}. Abs_multiset (count N) = N" using count_inverse by blast show "\p\{p. p partitions n \ sum p {..n} = k}. count (Abs_multiset p) = p" - by (auto simp add: multiset_def partitions_imp_finite_elements) + by (auto simp add: partitions_imp_finite_elements) show "count ` {N. number_partition n N \ size N = k} \ {p. p partitions n \ sum p {..n} = k}" by (auto simp add: count_partitions_iff size_nat_multiset_eq) show "Abs_multiset ` {p. p partitions n \ sum p {..n} = k} \ {N. number_partition n N \ size N = k}" - using partitions_iff_Abs_multiset size_nat_multiset_eq partitions_imp_multiset by fastforce + using partitions_iff_Abs_multiset size_nat_multiset_eq by fastforce qed lemma bij_betw_multiset_number_partition_with_atmost_size: "bij_betw count {N. number_partition n N \ size N \ k} {p. p partitions n \ sum p {..n} \ k}" proof (rule bij_betw_byWitness[where f'="Abs_multiset"]) show "\N\{N. number_partition n N \ size N \ k}. Abs_multiset (count N) = N" using count_inverse by blast show "\p\{p. p partitions n \ sum p {..n} \ k}. count (Abs_multiset p) = p" - by (auto simp add: multiset_def partitions_imp_finite_elements) + by (auto simp add: partitions_imp_finite_elements) show "count ` {N. number_partition n N \ size N \ k} \ {p. p partitions n \ sum p {..n} \ k}" by (auto simp add: count_partitions_iff size_nat_multiset_eq) show "Abs_multiset ` {p. p partitions n \ sum p {..n} \ k} \ {N. number_partition n N\ size N \ k}" - using partitions_iff_Abs_multiset size_nat_multiset_eq partitions_imp_multiset by fastforce + using partitions_iff_Abs_multiset size_nat_multiset_eq by fastforce qed theorem card_number_partitions_with_atmost_k_parts: shows "card {N. number_partition n N \ size N \ x} = Partition (n + x) x" proof - have "bij_betw count {N. number_partition n N \ size N \ x} {p. p partitions n \ sum p {..n} \ x}" by (rule bij_betw_multiset_number_partition_with_atmost_size) from this have "card {N. number_partition n N \ size N \ x} = card {p. p partitions n \ sum p {..n} \ x}" by (rule bij_betw_same_card) also have "card {p. p partitions n \ sum p {..n} \ x} = Partition (n + x) x" by (rule card_partitions_atmost_k_parts) finally show ?thesis . qed theorem card_partitions_with_k_parts: "card {N. number_partition n N \ size N = k} = Partition n k" proof - have "bij_betw count {N. number_partition n N \ size N = k} {p. p partitions n \ sum p {..n} = k}" by (rule bij_betw_multiset_number_partition_with_size) from this have "card {N. number_partition n N \ size N = k} = card {p. p partitions n \ sum p {..n} = k}" by (rule bij_betw_same_card) also have "\ = Partition n k" by (rule card_partitions_k_parts) finally show ?thesis . qed subsection \Cardinality of Number Partitions with only 1-parts\ lemma number_partition1_eq_replicate_mset: "{N. (\n. n\# N \ n = 1) \ number_partition n N} = {replicate_mset n 1}" proof show "{N. (\n. n \# N \ n = 1) \ number_partition n N} \ {replicate_mset n 1}" proof fix N assume N: "N \ {N. (\n. n \# N \ n = 1) \ number_partition n N}" have "N = replicate_mset n 1" proof (rule multiset_eqI) fix i have "count N 1 = sum_mset N" proof cases assume "N = {#}" from this show ?thesis by auto next assume "N \ {#}" from this N have "1 \# N" by blast from this N show ?thesis by (auto simp add: sum_mset_sum_count sum.remove[where x="1"] simp del: One_nat_def) qed from N this show "count N i = count (replicate_mset n 1) i" unfolding number_partition_def by (auto intro: count_inI) qed from this show "N \ {replicate_mset n 1}" by simp qed next show "{replicate_mset n 1} \ {N. (\n. n \# N \ n = 1) \ number_partition n N}" unfolding number_partition_def by auto qed lemma card_number_partitions_with_only_parts_1_eq_1: assumes "n \ x" shows "card {N. (\n. n\# N \ n = 1) \ number_partition n N \ size N \ x} = 1" (is "card ?N = _") proof - have "\N \ {N. (\n. n \# N \ n = 1) \ number_partition n N}. size N = n" unfolding number_partition1_eq_replicate_mset by simp from this number_partition1_eq_replicate_mset \n \ x\ have "?N = {replicate_mset n 1}" by auto from this show ?thesis by simp qed lemma card_number_partitions_with_only_parts_1_eq_0: assumes "x < n" shows "card {N. (\n. n\# N \ n = 1) \ number_partition n N \ size N \ x} = 0" (is "card ?N = _") proof - have "\N \ {N. (\n. n \# N \ n = 1) \ number_partition n N}. size N = n" unfolding number_partition1_eq_replicate_mset by simp from this number_partition1_eq_replicate_mset\x < n\ have "?N = {}" by auto from this show ?thesis by (simp only: card.empty) qed end diff --git a/thys/Card_Number_Partitions/Number_Partition.thy b/thys/Card_Number_Partitions/Number_Partition.thy --- a/thys/Card_Number_Partitions/Number_Partition.thy +++ b/thys/Card_Number_Partitions/Number_Partition.thy @@ -1,523 +1,517 @@ (* Author: Lukas Bulwahn *) section \Number Partitions\ theory Number_Partition imports Additions_to_Main begin subsection \Number Partitions as @{typ "nat => nat"} Functions\ definition partitions :: "(nat \ nat) \ nat \ bool" (infix "partitions" 50) where "p partitions n = ((\i. p i \ 0 \ 1 \ i \ i \ n) \ (\i\n. p i * i) = n)" lemma partitionsI: assumes "\i. p i \ 0 \ 1 \ i \ i \ n" assumes "(\i\n. p i * i) = n" shows "p partitions n" using assms unfolding partitions_def by auto lemma partitionsE: assumes "p partitions n" obtains "\i. p i \ 0 \ 1 \ i \ i \ n" "(\i\n. p i * i) = n" using assms unfolding partitions_def by auto lemma partitions_zero: "p partitions 0 \ p = (\i. 0)" unfolding partitions_def by auto lemma partitions_one: "p partitions (Suc 0) \ p = (\i. 0)(1 := 1)" unfolding partitions_def by (auto split: if_split_asm) (auto simp add: fun_eq_iff) subsection \Bounds and Finiteness of Number Partitions\ lemma partitions_imp_finite_elements: assumes "p partitions n" shows "finite {i. 0 < p i}" proof - from assms have "{i. 0 < p i} \ {..n}" by (auto elim: partitionsE) from this show ?thesis using rev_finite_subset by blast qed -lemma partitions_imp_multiset: - assumes "p partitions n" - shows "p \ multiset" -using assms partitions_imp_finite_elements multiset_def by auto - lemma partitions_bounds: assumes "p partitions n" shows "p i \ n" proof - from assms have index_bounds: "(\i. p i \ 0 \ 1 \ i \ i \ n)" and sum: "(\i\n. p i * i) = n" unfolding partitions_def by auto show ?thesis proof (cases "1 \ i \ i \ n") case True from True have "{..n} = insert i {i'. i' \ n \ i' \ i}" by blast from sum[unfolded this] have "p i * i + (\i\{i'. i' \ n \ i' \ i}. p i * i) = n" by auto from this have "p i * i \ n" by linarith from this True show ?thesis using dual_order.trans by fastforce next case False from this index_bounds show ?thesis by fastforce qed qed lemma partitions_parts_bounded: assumes "p partitions n" shows "sum p {..n} \ n" proof - { fix i assume "i \ n" from assms have "p i \ p i * i" by (auto elim!: partitionsE) } from this have "sum p {..n} \ (\i\n. p i * i)" by (auto intro: sum_mono) also from assms have n: "(\i\n. p i * i) = n" by (auto elim!: partitionsE) finally show ?thesis . qed lemma finite_partitions: "finite {p. p partitions n}" proof - have "{p. p partitions n} \ {f. (\i. f i \ n) \ (\i. n + 1 \ i \ f i = 0)}" by (auto elim: partitions_bounds) (auto simp add: partitions_def) from this bound_domain_and_range_impl_finitely_many_functions[of n "n + 1"] show ?thesis by (simp add: finite_subset) qed lemma finite_partitions_k_parts: "finite {p. p partitions n \ sum p {..n} = k}" by (simp add: finite_partitions) lemma partitions_remaining_Max_part: assumes "p partitions n" assumes "0 < p k" shows "\i. n - k < i \ i \ k \ p i = 0" proof (clarify) fix i assume "n - k < i" "i \ k" show "p i = 0" proof (cases "i \ n") assume "i \ n" from assms have n: "(\i\n. p i * i) = n" and "k \ n" by (auto elim: partitionsE) have "(\i\n. p i * i) = p k * k + (\i\{..n}-{k}. p i * i)" using \k \ n\ sum_atMost_remove_nat by blast also have "... = p i * i + p k * k + (\i\{..n}-{i, k}. p i * i)" using \i \ n\ \i \ k\ by (auto simp add: sum.remove[where x="i"]) (metis Diff_insert) finally have eq: "(\i\n. p i * i) = p i * i + p k * k + (\i\{..n} - {i, k}. p i * i)" . show "p i = 0" proof (rule ccontr) assume "p i \ 0" have upper_bound: "p i * i + p k * k \ n" using eq n by auto have lower_bound: "p i * i + p k * k > n" using \n - k < i\ \0 < p k\ \k \ n\ \p i \ 0\ mult_eq_if not_less by auto from upper_bound lower_bound show False by simp qed next assume "\ (i \ n)" from this show "p i = 0" using assms(1) by (auto elim: partitionsE) qed qed subsection \Operations of Number Partitions\ lemma partitions_remove1_bounds: assumes partitions: "p partitions n" assumes gr0: "0 < p k" assumes neq: "(p(k := p k - 1)) i \ 0" shows "1 \ i \ i \ n - k" proof from partitions neq show "1 \ i" by (auto elim!: partitionsE split: if_split_asm) next from partitions gr0 have n: "(\i\n. p i * i) = n" and "k \ n" by (auto elim: partitionsE) show "i \ n - k" proof cases assume "k \ n - k" from \k \ n - k\ neq show ?thesis using partitions_remaining_Max_part[OF partitions gr0] not_le by force next assume "\ k \ n - k" from this have "2 * k > n" by auto have "p k = 1" proof (rule ccontr) assume "p k \ 1" with gr0 have "p k \ 2" by auto from this have "p k * k \ 2 * k" by simp with \2 * k > n\ have "p k * k > n" by linarith from \k \ n\ this have "(\i\n. p i * i) > n" by (simp add: sum_atMost_remove_nat[of k]) from this n show "False" by auto qed from neq this show ?thesis using partitions_remaining_Max_part[OF partitions gr0] leI by (auto split: if_split_asm) force qed qed lemma partitions_remove1: assumes partitions: "p partitions n" assumes gr0: "0 < p k" shows "p(k := p k - 1) partitions (n - k)" proof (rule partitionsI) fix i assume "(p(k := p k - 1)) i \ 0" from this show "1 \ i \ i \ n - k" using partitions_remove1_bounds partitions gr0 by blast next from partitions gr0 have "k \ n" by (auto elim: partitionsE) have "(\i\n - k. (p(k := p k - 1)) i * i) = (\i\n. (p(k := p k - 1)) i * i)" using partitions_remove1_bounds partitions gr0 by (auto intro!: sum.mono_neutral_left) also have "... = (p k - 1) * k + (\i\{..n} - {k}. (p(k := p k - 1)) i * i)" using \k \ n\ by (simp add: sum_atMost_remove_nat[where k="k"]) also have "... = p k * k + (\i\{..n} - {k}. p i * i) - k" using gr0 by (simp add: diff_mult_distrib) also have "... = (\i\n. p i * i) - k" using \k \ n\ by (simp add: sum_atMost_remove_nat[of k]) also from partitions have "... = n - k" by (auto elim: partitionsE) finally show "(\i\n - k. (p(k := p k - 1)) i * i) = n - k" . qed lemma partitions_insert1: assumes p: "p partitions n" assumes "k > 0" shows "(p(k := p k + 1)) partitions (n + k)" proof (rule partitionsI) fix i assume "(p(k := p k + 1)) i \ 0" from p this \k > 0\ show "1 \ i \ i \ n + k" by (auto elim!: partitionsE) next have "(\i\n + k. (p(k := p k + 1)) i * i) = p k * k + (\i\{..n + k} - {k}. p i * i) + k" by (simp add: sum_atMost_remove_nat[of k]) also have "... = p k * k + (\i\{..n} - {k}. p i * i) + k" using p by (auto intro!: sum.mono_neutral_right elim!: partitionsE) also have "... = (\i\n. p i * i) + k" using p by (cases "k \ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE) also have "... = n + k" using p by (auto elim: partitionsE) finally show "(\i\n + k. (p(k := p k + 1)) i * i) = n + k" . qed lemma count_remove1: assumes "p partitions n" assumes "0 < p k" shows "(\i\n - k. (p(k := p k - 1)) i) = (\i\n. p i) - 1" proof - have "k \ n" using assms by (auto elim: partitionsE) have "(\i\n - k. (p(k := p k - 1)) i) = (\i\n. (p(k := p k - 1)) i)" using partitions_remove1_bounds assms by (auto intro!: sum.mono_neutral_left) also have "(\i\n. (p(k := p k - 1)) i) = p k + (\i\{..n} - {k}. p i) - 1" using \0 < p k\ \k \ n\ by (simp add: sum_atMost_remove_nat[of k]) also have "... = (\i\{..n}. p i) - 1" using \k \ n\ by (simp add: sum_atMost_remove_nat[of k]) finally show ?thesis . qed lemma count_insert1: assumes "p partitions n" shows "sum (p(k := p k + 1)) {..n + k} = (\i\n. p i) + 1" proof - have "(\i\n + k. (p(k := p k + 1)) i) = p k + (\i\{..n + k} - {k}. p i) + 1" by (simp add: sum_atMost_remove_nat[of k]) also have "... = p k + (\i\{..n} - {k}. p i) + 1" using assms by (auto intro!: sum.mono_neutral_right elim!: partitionsE) also have "... = (\i\n. p i) + 1" using assms by (cases "k \ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE) finally show ?thesis . qed lemma partitions_decrease1: assumes p: "p partitions m" assumes sum: "sum p {..m} = k" assumes "p 1 = 0" shows "(\i. p (i + 1)) partitions m - k" proof - from p have "p 0 = 0" by (auto elim!: partitionsE) { fix i assume neq: "p (i + 1) \ 0" from p this \p 1 = 0\ have "1 \ i" by (fastforce elim!: partitionsE simp add: le_Suc_eq) moreover have "i \ m - k" proof (rule ccontr) assume i_greater: "\ i \ m - k" from p have s: "(\i\m. p i * i) = m" by (auto elim!: partitionsE) from p sum have "k \ m" using partitions_parts_bounded by fastforce from neq p have "i + 1 \ m" by (auto elim!: partitionsE) from i_greater have "i > m - k" by simp have ineq1: "i + 1 > (m - k) + 1" using i_greater by simp have ineq21: "(\j\m. (p(i + 1 := p (i + 1) - 1)) j * j) \ (\j\m. (p(i + 1 := p (i + 1) - 1)) j)" using \p 0 = 0\ not_less by (fastforce intro!: sum_mono) have ineq22a: "(\j\m. (p(i + 1 := p (i + 1) - 1)) j) = (\j\m. p j) - 1" using \i + 1 \ m\ neq by (simp add: sum.remove[where x="i + 1"]) have ineq22: "(\j\m. (p(i + 1 := p (i + 1) - 1)) j) \ k - 1" using sum neq ineq22a by auto have ineq2: "(\j\m. (p(i + 1 := p (i + 1) - 1)) j * j) \ k - 1" using ineq21 ineq22 by auto have "(\i\m. p i * i) = p (i + 1) * (i + 1) + (\i\{..m} - {i + 1}. p i * i)" using \i + 1 \ m\ neq by (subst sum.remove[where x="i + 1"]) auto also have "... = (i + 1) + (\j\m. (p(i + 1 := p (i + 1) - 1)) j * j)" using \i + 1 \ m\ neq by (subst sum.remove[where x="i + 1" and g="\j. (p(i + 1 := p (i + 1) - 1)) j * j"]) (auto simp add: mult_eq_if) finally have "(\i\m. p i * i) = i + 1 + (\j\m. (p(i + 1 := p (i + 1) - 1)) j * j)" . moreover have "... > m" using ineq1 ineq2 \k \ m\ \p (i + 1) \ 0\ by linarith ultimately have "(\i\m. p i * i) > m" by simp from s this show False by simp qed ultimately have "1 \ i \ i \ m - k" .. } note bounds = this show "(\i. p (i + 1)) partitions m - k" proof (rule partitionsI) fix i assume "p (i + 1) \ 0" from bounds this show "1 \ i \ i \ m - k" . next have geq: "\i. p i * i \ p i" using \p 0 = 0\ not_less by fastforce have "(\i\m - k. p (i + 1) * i) = (\i\m. p (i + 1) * i)" using bounds by (auto intro: sum.mono_neutral_left) also have "... = (\i\Suc ` {..m}. p i * (i - 1))" by (auto simp add: sum.reindex) also have "... = (\i\Suc m. p i * (i - 1))" - using \p 0 = 0\ by (simp add: atMost_Suc_eq_insert_0 zero_notin_Suc_image) + using \p 0 = 0\ + by (simp add: atMost_Suc_eq_insert_0) also have "... = (\i\m. p i * (i - 1))" using p by (auto elim!: partitionsE) also have "... = (\i\m. p i * i - p i)" by (simp add: diff_mult_distrib2) also have "... = (\i\m. p i * i) - (\i\m. p i)" using geq by (simp only: sum_subtractf_nat) also have "... = m - k" using sum p by (auto elim!: partitionsE) finally show "(\i\m - k. p (i + 1) * i) = m - k" . qed qed lemma partitions_increase1: assumes partitions: "p partitions m - k" assumes k: "sum p {..m - k} = k" shows "(\i. p (i - 1)) partitions m" proof (rule partitionsI) fix i assume "p (i - 1) \ 0" from partitions this k show "1 \ i \ i \ m" by (cases k) (auto elim!: partitionsE) next from k partitions have "k \ m" using linear partitions_zero by force have eq_0: "\i>m - k. p i = 0" using partitions by (auto elim!: partitionsE) from partitions have s: "(\i\m - k. p i * i) = m - k" by (auto elim!: partitionsE) have "(\i\m. p (i - 1) * i) = (\i\Suc m. p (i - 1) * i)" using partitions k by (cases k) (auto elim!: partitionsE) also have "(\i\Suc m. p (i - 1) * i) = (\i\m. p i * (i + 1))" by (subst sum.atMost_Suc_shift) simp also have "... = (\i\m - k. p i * (i + 1))" using eq_0 by (auto intro: sum.mono_neutral_right) also have "... = (\i\m - k. p i * i) + (\i\m - k. p i)" by (simp add: sum.distrib) also have "... = m - k + k" using s k by simp also have "... = m" using \k \ m\ by simp finally show "(\i\m. p (i - 1) * i) = m" . qed lemma count_decrease1: assumes p: "p partitions m" assumes sum: "sum p {..m} = k" assumes "p 1 = 0" shows "sum (\i. p (i + 1)) {..m - k} = k" proof - from p have "p 0 = 0" by (auto elim!: partitionsE) have "sum (\i. p (i + 1)) {..m - k} = sum (\i. p (i + 1)) {..m}" using partitions_decrease1[OF assms] by (auto intro: sum.mono_neutral_left elim!: partitionsE) also have "\ = sum (\i. p (i + 1)) {0..m}" by (simp add: atLeast0AtMost) also have "\ = sum (\i. p i) {Suc 0.. Suc m}" by (simp only: One_nat_def add_Suc_right add_0_right sum.shift_bounds_cl_Suc_ivl) also have "\ = sum (\i. p i) {.. Suc m}" using \p 0 = 0\ by (simp add: atLeast0AtMost sum_shift_lb_Suc0_0) also have "\ = sum (\i. p i) {.. m}" using p by (auto elim!: partitionsE) also have "\ = k" using sum by simp finally show ?thesis . qed lemma count_increase1: assumes partitions: "p partitions m - k" assumes k: "sum p {..m - k} = k" shows "(\i\m. p (i - 1)) = k" proof - have "p 0 = 0" using partitions by (auto elim!: partitionsE) have "(\i\m. p (i - 1)) = (\i\{1..m}. p (i - 1))" using \p 0 = 0\ by (auto intro: sum.mono_neutral_cong_right) also have "(\i\{1..m}. p (i - 1)) = (\i\m - 1. p i)" proof (cases m) case 0 from this show ?thesis using \p 0 = 0\ by simp next case (Suc m') { fix x assume "Suc 0 \ x" "x \ m" from this Suc have "x \ Suc ` {..m'}" by (auto intro!: image_eqI[where x="x - 1"]) } from this Suc show ?thesis by (intro sum.reindex_cong[of Suc]) auto qed also have "(\i\m - 1. p i) = (\i\m. p i)" proof - { fix i assume "0 < p i" "i \ m" from assms this have "i \ m - 1" using \p 0 = 0\ partitions_increase1 by (cases k) (auto elim!: partitionsE) } from this show ?thesis by (auto intro: sum.mono_neutral_cong_left) qed also have "... = (\i\m - k. p i)" using partitions by (auto intro: sum.mono_neutral_right elim!: partitionsE) also have "... = k" using k by auto finally show ?thesis . qed subsection \Number Partitions as Multisets on Natural Numbers\ definition number_partition :: "nat \ nat multiset \ bool" where "number_partition n N = (sum_mset N = n \ 0 \# N)" subsubsection \Relationship to Definition on Functions\ lemma count_partitions_iff: "count N partitions n \ number_partition n N" proof assume "count N partitions n" from this have "(\i. count N i \ 0 \ 1 \ i \ i \ n)" "(\i\n. count N i * i) = n" unfolding Number_Partition.partitions_def by auto moreover from this have "set_mset N \ {..n}" by auto moreover have "finite {..n}" by auto ultimately have "sum_mset N = n" using sum_mset_sum_count sum_mset_eq_sum_on_supersets by presburger moreover have "0 \# N" using \\i. count N i \ 0 \ 1 \ i \ i \ n\ by auto ultimately show "number_partition n N" unfolding number_partition_def by auto next assume "number_partition n N" from this have "sum_mset N = n" and "0 \# N" unfolding number_partition_def by auto { fix i assume "count N i \ 0" have "1 \ i \ i \ n" proof from \0 \# N\ \count N i \ 0\ show "1 \ i" using Suc_le_eq by auto from \sum_mset N = n\ \count N i \ 0\ show "i \ n" using multi_member_split by fastforce qed } moreover from \sum_mset N = n\ have "(\i\n. count N i * i) = n" by (metis atMost_iff calculation finite_atMost not_in_iff subsetI sum_mset_eq_sum_on_supersets sum_mset_sum_count) ultimately show "count N partitions n" by (rule partitionsI) auto qed lemma partitions_iff_Abs_multiset: "p partitions n \ finite {x. 0 < p x} \ number_partition n (Abs_multiset p)" proof assume "p partitions n" from this have bounds: "(\i. p i \ 0 \ 1 \ i \ i \ n)" and sum: "(\i\n. p i * i) = n" unfolding partitions_def by auto - from \p partitions n\ have "p \ multiset" by (rule partitions_imp_multiset) from \p partitions n\ have "finite {x. 0 < p x}" by (rule partitions_imp_finite_elements) - moreover from \p \ multiset\ bounds have "\ 0 \# Abs_multiset p" + moreover from \finite {x. 0 < p x}\ bounds have "\ 0 \# Abs_multiset p" using count_eq_zero_iff by force - moreover from \p \ multiset\ this sum have "sum_mset (Abs_multiset p) = n" + moreover from \finite {x. 0 < p x}\ this sum have "sum_mset (Abs_multiset p) = n" proof - have "(\i\{x. 0 < p x}. p i * i) = (\i\n. p i * i)" using bounds by (auto intro: sum.mono_neutral_cong_left) - from \p \ multiset\ this sum show "sum_mset (Abs_multiset p) = n" + from \finite {x. 0 < p x}\ this sum show "sum_mset (Abs_multiset p) = n" by (simp add: sum_mset_sum_count set_mset_Abs_multiset) qed ultimately show "finite {x. 0 < p x} \ number_partition n (Abs_multiset p)" unfolding number_partition_def by auto next assume "finite {x. 0 < p x} \ number_partition n (Abs_multiset p)" from this have "finite {x. 0 < p x}" "0 \# Abs_multiset p" "sum_mset (Abs_multiset p) = n" unfolding number_partition_def by auto - from \finite {x. 0 < p x}\ have "p \ multiset" by (simp add: multiset_def) - from \p \ multiset\ have "(\i\{x. 0 < p x}. p i * i) = n" + from \finite {x. 0 < p x}\ have "(\i\{x. 0 < p x}. p i * i) = n" using \ sum_mset (Abs_multiset p) = n\ by (simp add: sum_mset_sum_count set_mset_Abs_multiset) have bounds: "\i. p i \ 0 \ 1 \ i \ i \ n" proof fix i assume "p i \ 0" - from \\ 0 \# Abs_multiset p\ \p \ multiset\ have "p 0 = 0" + from \\ 0 \# Abs_multiset p\ \finite {x. 0 < p x}\ have "p 0 = 0" using count_inI by force from this \p i \ 0\ show "1 \ i" by (metis One_nat_def leI less_Suc0) show "i \ n" proof (rule ccontr) assume "\ i \ n" from this have "i > n" using le_less_linear by blast from this \p i \ 0\ have "p i * i > n" by (auto simp add: less_le_trans) from \p i \ 0\ have "(\i\{x. 0 < p x}. p i * i) = p i * i + (\i\{x. 0 < p x} - {i}. p i * i)" using \finite {x. 0 < p x}\ by (subst sum.insert_remove[symmetric]) (auto simp add: insert_absorb) also from \p i * i > n\ have "\ > n" by auto finally show False using \(\i\{x. 0 < p x}. p i * i) = n\ by blast qed qed moreover have "(\i\n. p i * i) = n" proof - have "(\i\n. p i * i) = (\i\{x. 0 < p x}. p i * i)" using bounds by (auto intro: sum.mono_neutral_cong_right) from this show ?thesis using \(\i\{x. 0 < p x}. p i * i) = n\ by simp qed ultimately show "p partitions n" by (auto intro: partitionsI) qed lemma size_nat_multiset_eq: fixes N :: "nat multiset" assumes "number_partition n N" shows "size N = sum (count N) {..n}" proof - have "set_mset N \ {..sum_mset N}" by (auto dest: multi_member_split) have "size N = sum (count N) (set_mset N)" by (rule size_multiset_overloaded_eq) also have "\ = sum (count N) {..sum_mset N}" using \set_mset N \ {..sum_mset N}\ by (auto intro: sum.mono_neutral_cong_left count_inI) finally show ?thesis using \number_partition n N\ unfolding number_partition_def by auto qed end diff --git a/thys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy b/thys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy --- a/thys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy +++ b/thys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy @@ -1,175 +1,175 @@ (* Title: Signed Hereditar(il)y (Finite) Multisets Author: Jasmin Blanchette , 2016 Author: Dmitriy Traytel , 2016 Maintainer: Jasmin Blanchette *) section \Signed Hereditar(il)y (Finite) Multisets\ theory Signed_Hereditary_Multiset imports Signed_Multiset Hereditary_Multiset begin subsection \Type Definition\ typedef zhmultiset = "UNIV :: hmultiset zmultiset set" morphisms zhmsetmset ZHMSet by simp lemmas ZHMSet_inverse[simp] = ZHMSet_inverse[OF UNIV_I] lemmas ZHMSet_inject[simp] = ZHMSet_inject[OF UNIV_I UNIV_I] declare zhmsetmset_inverse [simp] zhmsetmset_inject [simp] setup_lifting type_definition_zhmultiset subsection \Multiset Order\ instantiation zhmultiset :: linorder begin lift_definition less_zhmultiset :: "zhmultiset \ zhmultiset \ bool" is "(<)" . lift_definition less_eq_zhmultiset :: "zhmultiset \ zhmultiset \ bool" is "(\)" . instance by (intro_classes; transfer) auto end lemmas ZHMSet_less[simp] = less_zhmultiset.abs_eq lemmas ZHMSet_le[simp] = less_eq_zhmultiset.abs_eq lemmas zhmsetmset_less[simp] = less_zhmultiset.rep_eq[symmetric] lemmas zhmsetmset_le[simp] = less_eq_zhmultiset.rep_eq[symmetric] subsection \Embedding and Projections of Syntactic Ordinals\ abbreviation zhmset_of :: "hmultiset \ zhmultiset" where "zhmset_of M \ ZHMSet (zmset_of (hmsetmset M))" lemma zhmset_of_inject[simp]: "zhmset_of M = zhmset_of N \ M = N" by simp lemma zhmset_of_less: "zhmset_of M < zhmset_of N \ M < N" by (simp add: zmset_of_less) lemma zhmset_of_le: "zhmset_of M \ zhmset_of N \ M \ N" by (simp add: zmset_of_le) abbreviation hmset_pos :: "zhmultiset \ hmultiset" where "hmset_pos M \ HMSet (mset_pos (zhmsetmset M))" abbreviation hmset_neg :: "zhmultiset \ hmultiset" where "hmset_neg M \ HMSet (mset_neg (zhmsetmset M))" subsection \Disjoint Union and Difference\ instantiation zhmultiset :: cancel_comm_monoid_add begin lift_definition zero_zhmultiset :: zhmultiset is "{#}\<^sub>z" . lift_definition plus_zhmultiset :: "zhmultiset \ zhmultiset \ zhmultiset" is "\A B. A + B" . lift_definition minus_zhmultiset :: "zhmultiset \ zhmultiset \ zhmultiset" is "\A B. A - B" . lemmas ZHMSet_plus = plus_zhmultiset.abs_eq[symmetric] lemmas ZHMSet_diff = minus_zhmultiset.abs_eq[symmetric] lemmas zhmsetmset_plus = plus_zhmultiset.rep_eq lemmas zhmsetmset_diff = minus_zhmultiset.rep_eq lemma zhmset_of_plus: "zhmset_of (A + B) = zhmset_of A + zhmset_of B" by (simp add: hmsetmset_plus ZHMSet_plus zmset_of_plus) -lemma hmsetmset_0[simp]: "hmsetmset 0 = {#}" - by (rule hmultiset.inject[THEN iffD1]) (simp add: zero_hmultiset_def) +lemma hmsetmset_0: "hmsetmset 0 = {#}" + by (fact hmsetmset_0) instance by (intro_classes; transfer) (auto intro: mult.assoc add.commute) end lemma zhmset_of_0: "zhmset_of 0 = 0" by (simp add: zero_zhmultiset_def) lemma hmset_pos_plus: "hmset_pos (A + B) = (hmset_pos A - hmset_neg B) + (hmset_pos B - hmset_neg A)" by (simp add: HMSet_diff HMSet_plus zhmsetmset_plus) lemma hmset_neg_plus: "hmset_neg (A + B) = (hmset_neg A - hmset_pos B) + (hmset_neg B - hmset_pos A)" by (simp add: HMSet_diff HMSet_plus zhmsetmset_plus) lemma zhmset_pos_neg_partition: "M = zhmset_of (hmset_pos M) - zhmset_of (hmset_neg M)" by (cases M, simp add: ZHMSet_diff[symmetric], rule mset_pos_neg_partition) lemma zhmset_pos_as_neg: "zhmset_of (hmset_pos M) = zhmset_of (hmset_neg M) + M" using mset_pos_as_neg zhmsetmset_plus zhmsetmset_inject by fastforce lemma zhmset_neg_as_pos: "zhmset_of (hmset_neg M) = zhmset_of (hmset_pos M) - M" using zhmsetmset_diff mset_neg_as_pos zhmsetmset_inject by fastforce lemma hmset_pos_neg_dual: "hmset_pos a + hmset_pos b + (hmset_neg a - hmset_pos b) + (hmset_neg b - hmset_pos a) = hmset_neg a + hmset_neg b + (hmset_pos a - hmset_neg b) + (hmset_pos b - hmset_neg a)" by (simp add: HMSet_plus[symmetric] HMSet_diff[symmetric]) (rule mset_pos_neg_dual) lemma zhmset_of_sum_list: "zhmset_of (sum_list Ms) = sum_list (map zhmset_of Ms)" by (induct Ms) (auto simp: zero_zhmultiset_def zhmset_of_plus) lemma less_hmset_zhmsetE: assumes m_lt_n: "M < N" obtains A B C where "M = zhmset_of A + C" and "N = zhmset_of B + C" and "A < B" by (rule less_mset_zmsetE[OF m_lt_n[folded zhmsetmset_less]]) (metis hmsetmset_less hmultiset.sel ZHMSet_plus zhmsetmset_inverse) lemma less_eq_hmset_zhmsetE: assumes m_le_n: "M \ N" obtains A B C where "M = zhmset_of A + C" and "N = zhmset_of B + C" and "A \ B" by (rule less_eq_mset_zmsetE[OF m_le_n[folded zhmsetmset_le]]) (metis hmsetmset_le hmultiset.sel ZHMSet_plus zhmsetmset_inverse) instantiation zhmultiset :: ab_group_add begin lift_definition uminus_zhmultiset :: "zhmultiset \ zhmultiset" is "\A. - A" . lemmas ZHMSet_uminus = uminus_zhmultiset.abs_eq[symmetric] lemmas zhmsetmset_uminus = uminus_zhmultiset.rep_eq instance by (intro_classes; transfer; simp) end subsection \Infimum and Supremum\ instance zhmultiset :: ordered_cancel_comm_monoid_add by (intro_classes; transfer) (auto simp: add_left_mono) instance zhmultiset :: ordered_ab_group_add by (intro_classes; transfer; simp) instantiation zhmultiset :: distrib_lattice begin definition inf_zhmultiset :: "zhmultiset \ zhmultiset \ zhmultiset" where "inf_zhmultiset A B = (if A < B then A else B)" definition sup_zhmultiset :: "zhmultiset \ zhmultiset \ zhmultiset" where "sup_zhmultiset A B = (if B > A then B else A)" instance by intro_classes (auto simp: inf_zhmultiset_def sup_zhmultiset_def) end end diff --git a/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy b/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy --- a/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy +++ b/thys/Nested_Multisets_Ordinals/Signed_Multiset.thy @@ -1,878 +1,878 @@ (* Title: Signed (Finite) Multisets Author: Jasmin Blanchette , 2016 Maintainer: Jasmin Blanchette *) section \Signed (Finite) Multisets\ theory Signed_Multiset imports Multiset_More abbrevs "!z" = "\<^sub>z" begin subsection \Definition of Signed Multisets\ definition equiv_zmset :: "'a multiset \ 'a multiset \ 'a multiset \ 'a multiset \ bool" where "equiv_zmset = (\(Mp, Mn) (Np, Nn). Mp + Nn = Np + Mn)" quotient_type 'a zmultiset = "'a multiset \ 'a multiset" / equiv_zmset by (rule equivpI, simp_all add: equiv_zmset_def reflp_def symp_def transp_def) (metis multi_union_self_other_eq union_lcomm) subsection \Basic Operations on Signed Multisets\ instantiation zmultiset :: (type) cancel_comm_monoid_add begin lift_definition zero_zmultiset :: "'a zmultiset" is "({#}, {#})" . abbreviation empty_zmset :: "'a zmultiset" ("{#}\<^sub>z") where "empty_zmset \ 0" lift_definition minus_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" is "\(Mp, Mn) (Np, Nn). (Mp + Nn, Mn + Np)" by (auto simp: equiv_zmset_def union_commute union_lcomm) lift_definition plus_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" is "\(Mp, Mn) (Np, Nn). (Mp + Np, Mn + Nn)" by (auto simp: equiv_zmset_def union_commute union_lcomm) instance by (intro_classes; transfer) (auto simp: equiv_zmset_def) end instantiation zmultiset :: (type) group_add begin lift_definition uminus_zmultiset :: "'a zmultiset \ 'a zmultiset" is "\(Mp, Mn). (Mn, Mp)" by (auto simp: equiv_zmset_def add.commute) instance by (intro_classes; transfer) (auto simp: equiv_zmset_def) end lift_definition zcount :: "'a zmultiset \ 'a \ int" is "\(Mp, Mn) x. int (count Mp x) - int (count Mn x)" by (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff diff_eq_eq diff_add_eq eq_diff_eq of_nat_add[symmetric]) lemma zcount_inject: "zcount M = zcount N \ M = N" by transfer (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff diff_eq_eq diff_add_eq eq_diff_eq of_nat_add[symmetric]) lemma zmultiset_eq_iff: "M = N \ (\a. zcount M a = zcount N a)" by (simp only: zcount_inject[symmetric] fun_eq_iff) lemma zmultiset_eqI: "(\x. zcount A x = zcount B x) \ A = B" using zmultiset_eq_iff by auto lemma zcount_uminus[simp]: "zcount (- A) x = - zcount A x" by transfer auto lift_definition add_zmset :: "'a \ 'a zmultiset \ 'a zmultiset" is "\x (Mp, Mn). (add_mset x Mp, Mn)" by (auto simp: equiv_zmset_def) syntax "_zmultiset" :: "args \ 'a zmultiset" ("{#(_)#}\<^sub>z") translations "{#x, xs#}\<^sub>z" == "CONST add_zmset x {#xs#}\<^sub>z" "{#x#}\<^sub>z" == "CONST add_zmset x {#}\<^sub>z" lemma zcount_empty[simp]: "zcount {#}\<^sub>z a = 0" by transfer auto lemma zcount_add_zmset[simp]: "zcount (add_zmset b A) a = (if b = a then zcount A a + 1 else zcount A a)" by transfer auto lemma zcount_single: "zcount {#b#}\<^sub>z a = (if b = a then 1 else 0)" by simp lemma add_add_same_iff_zmset[simp]: "add_zmset a A = add_zmset a B \ A = B" by (auto simp: zmultiset_eq_iff) lemma add_zmset_commute: "add_zmset x (add_zmset y M) = add_zmset y (add_zmset x M)" by (auto simp: zmultiset_eq_iff) lemma singleton_ne_empty_zmset[simp]: "{#x#}\<^sub>z \ {#}\<^sub>z" and empty_ne_singleton_zmset[simp]: "{#}\<^sub>z \ {#x#}\<^sub>z" by (auto dest!: arg_cong2[of _ _ x _ zcount]) lemma singleton_ne_uminus_singleton_zmset[simp]: "{#x#}\<^sub>z \ - {#y#}\<^sub>z" and uminus_singleton_ne_singleton_zmset[simp]: "- {#x#}\<^sub>z \ {#y#}\<^sub>z" by (auto dest!: arg_cong2[of _ _ x x zcount] split: if_splits) subsubsection \Conversion to Set and Membership\ definition set_zmset :: "'a zmultiset \ 'a set" where "set_zmset M = {x. zcount M x \ 0}" abbreviation elem_zmset :: "'a \ 'a zmultiset \ bool" where "elem_zmset a M \ a \ set_zmset M" notation elem_zmset ("'(\#\<^sub>z')") and elem_zmset ("(_/ \#\<^sub>z _)" [51, 51] 50) notation (ASCII) elem_zmset ("'(:#z')") and elem_zmset ("(_/ :#z _)" [51, 51] 50) abbreviation not_elem_zmset :: "'a \ 'a zmultiset \ bool" where "not_elem_zmset a M \ a \ set_zmset M" notation not_elem_zmset ("'(\#\<^sub>z')") and not_elem_zmset ("(_/ \#\<^sub>z _)" [51, 51] 50) notation (ASCII) not_elem_zmset ("'(~:#z')") and not_elem_zmset ("(_/ ~:#z _)" [51, 51] 50) context begin qualified abbreviation Ball :: "'a zmultiset \ ('a \ bool) \ bool" where "Ball M \ Set.Ball (set_zmset M)" qualified abbreviation Bex :: "'a zmultiset \ ('a \ bool) \ bool" where "Bex M \ Set.Bex (set_zmset M)" end syntax "_ZMBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#\<^sub>z_./ _)" [0, 0, 10] 10) "_ZMBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#\<^sub>z_./ _)" [0, 0, 10] 10) syntax (ASCII) "_ZMBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#\<^sub>z_./ _)" [0, 0, 10] 10) "_ZMBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#\<^sub>z_./ _)" [0, 0, 10] 10) translations "\x\#\<^sub>zA. P" \ "CONST Signed_Multiset.Ball A (\x. P)" "\x\#\<^sub>zA. P" \ "CONST Signed_Multiset.Bex A (\x. P)" lemma zcount_eq_zero_iff: "zcount M x = 0 \ x \#\<^sub>z M" by (auto simp add: set_zmset_def) lemma not_in_iff_zmset: "x \#\<^sub>z M \ zcount M x = 0" by (auto simp add: zcount_eq_zero_iff) lemma zcount_ne_zero_iff[simp]: "zcount M x \ 0 \ x \#\<^sub>z M" by (auto simp add: set_zmset_def) lemma zcount_inI: assumes "zcount M x = 0 \ False" shows "x \#\<^sub>z M" proof (rule ccontr) assume "x \#\<^sub>z M" with assms show False by (simp add: not_in_iff_zmset) qed lemma set_zmset_empty[simp]: "set_zmset {#}\<^sub>z = {}" by (simp add: set_zmset_def) lemma set_zmset_single: "set_zmset {#b#}\<^sub>z = {b}" by (simp add: set_zmset_def) lemma set_zmset_eq_empty_iff[simp]: "set_zmset M = {} \ M = {#}\<^sub>z" by (auto simp add: zmultiset_eq_iff zcount_eq_zero_iff) lemma finite_count_ne: "finite {x. count M x \ count N x}" proof - have "{x. count M x \ count N x} \ set_mset M \ set_mset N" by (auto simp: not_in_iff) moreover have "finite (set_mset M \ set_mset N)" by (rule finite_UnI[OF finite_set_mset finite_set_mset]) ultimately show ?thesis by (rule finite_subset) qed lemma finite_set_zmset[iff]: "finite (set_zmset M)" unfolding set_zmset_def by transfer (auto intro: finite_count_ne) lemma zmultiset_nonemptyE[elim]: assumes "A \ {#}\<^sub>z" obtains x where "x \#\<^sub>z A" proof - have "\x. x \#\<^sub>z A" by (rule ccontr) (insert assms, auto) with that show ?thesis by blast qed subsubsection \Union\ lemma zcount_union[simp]: "zcount (M + N) a = zcount M a + zcount N a" by transfer auto lemma union_add_left_zmset[simp]: "add_zmset a A + B = add_zmset a (A + B)" by (auto simp: zmultiset_eq_iff) lemma union_zmset_add_zmset_right[simp]: "A + add_zmset a B = add_zmset a (A + B)" by (auto simp: zmultiset_eq_iff) lemma add_zmset_add_single: \add_zmset a A = A + {#a#}\<^sub>z\ by (subst union_zmset_add_zmset_right, subst add.comm_neutral) (rule refl) subsubsection \Difference\ lemma zcount_diff[simp]: "zcount (M - N) a = zcount M a - zcount N a" by transfer auto lemma add_zmset_diff_bothsides: \add_zmset a M - add_zmset a A = M - A\ by (auto simp: zmultiset_eq_iff) lemma in_diff_zcount: "a \#\<^sub>z M - N \ zcount N a \ zcount M a" by (fastforce simp: set_zmset_def) lemma diff_add_zmset: fixes M N Q :: "'a zmultiset" shows "M - (N + Q) = M - N - Q" by (rule sym) (fact diff_diff_add) lemma insert_Diff_zmset[simp]: "add_zmset x (M - {#x#}\<^sub>z) = M" by (clarsimp simp: zmultiset_eq_iff) lemma diff_union_swap_zmset: "add_zmset b (M - {#a#}\<^sub>z) = add_zmset b M - {#a#}\<^sub>z" by (auto simp add: zmultiset_eq_iff) lemma diff_add_zmset_swap[simp]: "add_zmset b M - A = add_zmset b (M - A)" by (auto simp add: zmultiset_eq_iff) lemma diff_diff_add_zmset[simp]: "(M :: 'a zmultiset) - N - P = M - (N + P)" by (rule diff_diff_add) lemma zmset_add[elim?]: obtains B where "A = add_zmset a B" proof - have "A = add_zmset a (A - {#a#}\<^sub>z)" by simp with that show thesis . qed subsubsection \Equality of Signed Multisets\ lemma single_eq_single_zmset[simp]: "{#a#}\<^sub>z = {#b#}\<^sub>z \ a = b" by (auto simp add: zmultiset_eq_iff) lemma multi_self_add_other_not_self_zmset[simp]: "M = add_zmset x M \ False" by (auto simp add: zmultiset_eq_iff) lemma add_zmset_remove_trivial: \add_zmset x M - {#x#}\<^sub>z = M\ by simp lemma diff_single_eq_union_zmset: "M - {#x#}\<^sub>z = N \ M = add_zmset x N" by auto lemma union_single_eq_diff_zmset: "add_zmset x M = N \ M = N - {#x#}\<^sub>z" unfolding add_zmset_add_single[of _ M] by (fact add_implies_diff) lemma add_zmset_eq_conv_diff: "add_zmset a M = add_zmset b N \ M = N \ a = b \ M = add_zmset b (N - {#a#}\<^sub>z) \ N = add_zmset a (M - {#b#}\<^sub>z)" by (simp add: zmultiset_eq_iff) fastforce lemma add_zmset_eq_conv_ex: "(add_zmset a M = add_zmset b N) = (M = N \ a = b \ (\K. M = add_zmset b K \ N = add_zmset a K))" by (auto simp add: add_zmset_eq_conv_diff) lemma multi_member_split: "\A. M = add_zmset x A" by (rule exI[where x = "M - {#x#}\<^sub>z"]) simp subsection \Conversions from and to Multisets\ lift_definition zmset_of :: "'a multiset \ 'a zmultiset" is "\f. (Abs_multiset f, {#})" . lemma zmset_of_inject[simp]: "zmset_of M = zmset_of N \ M = N" by (simp add: zmset_of_def, transfer, auto simp: equiv_zmset_def) lemma zmset_of_empty[simp]: "zmset_of {#} = {#}\<^sub>z" by (simp add: zmset_of_def zero_zmultiset_def) lemma zmset_of_add_mset[simp]: "zmset_of (add_mset x M) = add_zmset x (zmset_of M)" by transfer (auto simp: equiv_zmset_def add_mset_def cong: if_cong) lemma zcount_of_mset[simp]: "zcount (zmset_of M) x = int (count M x)" by (induct M) auto lemma zmset_of_plus: "zmset_of (M + N) = zmset_of M + zmset_of N" by (transfer, auto simp: equiv_zmset_def eq_onp_same_args plus_multiset.abs_eq)+ lift_definition mset_pos :: "'a zmultiset \ 'a multiset" is "\(Mp, Mn). count (Mp - Mn)" - by (clarsimp simp: equiv_zmset_def intro!: arg_cong[of _ _ count]) + by (auto simp add: equiv_zmset_def simp flip: set_mset_diff) (metis add.commute add_diff_cancel_right) lift_definition mset_neg :: "'a zmultiset \ 'a multiset" is "\(Mp, Mn). count (Mn - Mp)" - by (clarsimp simp: equiv_zmset_def intro!: arg_cong[of _ _ count]) + by (auto simp add: equiv_zmset_def simp flip: set_mset_diff) (metis add.commute add_diff_cancel_right) lemma zmset_of_inverse[simp]: "mset_pos (zmset_of M) = M" and minus_zmset_of_inverse[simp]: "mset_neg (- zmset_of M) = M" by (transfer, simp)+ lemma neg_zmset_pos[simp]: "mset_neg (zmset_of M) = {#}" by (rule zmset_of_inject[THEN iffD1], simp, transfer, auto simp: equiv_zmset_def)+ lemma count_mset_pos[simp]: "count (mset_pos M) x = nat (zcount M x)" and count_mset_neg[simp]: "count (mset_neg M) x = nat (- zcount M x)" by (transfer; auto)+ lemma mset_pos_empty[simp]: "mset_pos {#}\<^sub>z = {#}" and mset_neg_empty[simp]: "mset_neg {#}\<^sub>z = {#}" by (rule multiset_eqI, simp)+ lemma mset_pos_singleton[simp]: "mset_pos {#x#}\<^sub>z = {#x#}" and mset_neg_singleton[simp]: "mset_neg {#x#}\<^sub>z = {#}" by (rule multiset_eqI, simp)+ lemma mset_pos_neg_partition: "M = zmset_of (mset_pos M) - zmset_of (mset_neg M)" and mset_pos_as_neg: "zmset_of (mset_pos M) = zmset_of (mset_neg M) + M" and mset_neg_as_pos: "zmset_of (mset_neg M) = zmset_of (mset_pos M) - M" by (rule zmultiset_eqI, simp)+ lemma mset_pos_uminus[simp]: "mset_pos (- A) = mset_neg A" by (rule multiset_eqI) simp lemma mset_neg_uminus[simp]: "mset_neg (- A) = mset_pos A" by (rule multiset_eqI) simp lemma mset_pos_plus[simp]: "mset_pos (A + B) = (mset_pos A - mset_neg B) + (mset_pos B - mset_neg A)" by (rule multiset_eqI) simp lemma mset_neg_plus[simp]: "mset_neg (A + B) = (mset_neg A - mset_pos B) + (mset_neg B - mset_pos A)" by (rule multiset_eqI) simp lemma mset_pos_diff[simp]: "mset_pos (A - B) = (mset_pos A - mset_pos B) + (mset_neg B - mset_neg A)" by (rule mset_pos_plus[of A "- B", simplified]) lemma mset_neg_diff[simp]: "mset_neg (A - B) = (mset_neg A - mset_neg B) + (mset_pos B - mset_pos A)" by (rule mset_neg_plus[of A "- B", simplified]) lemma mset_pos_neg_dual: "mset_pos a + mset_pos b + (mset_neg a - mset_pos b) + (mset_neg b - mset_pos a) = mset_neg a + mset_neg b + (mset_pos a - mset_neg b) + (mset_pos b - mset_neg a)" using [[linarith_split_limit = 20]] by (rule multiset_eqI) simp lemma decompose_zmset_of2: obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" proof let ?A = "zmset_of (mset_pos M + mset_neg N)" let ?B = "zmset_of (mset_pos N + mset_neg M)" let ?C = "- (zmset_of (mset_neg M) + zmset_of (mset_neg N))" show "M = ?A + ?C" by (simp add: zmset_of_plus mset_pos_neg_partition) show "N = ?B + ?C" by (simp add: zmset_of_plus diff_add_zmset mset_pos_neg_partition) qed subsubsection \Pointwise Ordering Induced by @{const zcount}\ definition subseteq_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "A \#\<^sub>z B \ (\a. zcount A a \ zcount B a)" definition subset_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "A \#\<^sub>z B \ A \#\<^sub>z B \ A \ B" abbreviation (input) supseteq_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "supseteq_zmset A B \ B \#\<^sub>z A" abbreviation (input) supset_zmset :: "'a zmultiset \ 'a zmultiset \ bool" (infix "\#\<^sub>z" 50) where "supset_zmset A B \ B \#\<^sub>z A" notation (input) subseteq_zmset (infix "\#\<^sub>z" 50) and supseteq_zmset (infix "\#\<^sub>z" 50) notation (ASCII) subseteq_zmset (infix "\#\<^sub>z" 50) and subset_zmset (infix "\#\<^sub>z" 50) and supseteq_zmset (infix "\#\<^sub>z" 50) and supset_zmset (infix ">#\<^sub>z" 50) interpretation subset_zmset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales (auto simp add: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff intro: order_trans antisym) interpretation subset_zmset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales lemma zmset_subset_eqI: "(\a. zcount A a \ zcount B a) \ A \#\<^sub>z B" by (simp add: subseteq_zmset_def) lemma zmset_subset_eq_zcount: "A \#\<^sub>z B \ zcount A a \ zcount B a" by (simp add: subseteq_zmset_def) lemma zmset_subset_eq_add_zmset_cancel: \add_zmset a A \#\<^sub>z add_zmset a B \ A \#\<^sub>z B\ unfolding add_zmset_add_single[of _ A] add_zmset_add_single[of _ B] by (rule subset_zmset.add_le_cancel_right) lemma zmset_subset_eq_zmultiset_union_diff_commute: "A - B + C = A + C - B" for A B C :: "'a zmultiset" by (simp add: add.commute add_diff_eq) lemma zmset_subset_eq_insertD: "add_zmset x A \#\<^sub>z B \ A \#\<^sub>z B" unfolding subset_zmset_def subseteq_zmset_def by (metis (no_types) add.commute add_le_same_cancel2 zcount_add_zmset dual_order.trans le_cases le_numeral_extra(2)) lemma zmset_subset_insertD: "add_zmset x A \#\<^sub>z B \ A \#\<^sub>z B" by (rule zmset_subset_eq_insertD) (rule subset_zmset.less_imp_le) lemma subset_eq_diff_conv_zmset: "A - C \#\<^sub>z B \ A \#\<^sub>z B + C" by (simp add: subseteq_zmset_def ordered_ab_group_add_class.diff_le_eq) lemma multi_psub_of_add_self_zmset[simp]: "A \#\<^sub>z add_zmset x A" by (auto simp: subset_zmset_def subseteq_zmset_def) lemma multi_psub_self_zmset: "A \#\<^sub>z A = False" by simp lemma zmset_subset_add_zmset[simp]: "add_zmset x N \#\<^sub>z add_zmset x M \ N \#\<^sub>z M" unfolding add_zmset_add_single[of _ N] add_zmset_add_single[of _ M] by (fact subset_zmset.add_less_cancel_right) lemma zmset_of_subseteq_iff[simp]: "zmset_of M \#\<^sub>z zmset_of N \ M \# N" by (simp add: subseteq_zmset_def subseteq_mset_def) lemma zmset_of_subset_iff[simp]: "zmset_of M \#\<^sub>z zmset_of N \ M \# N" by (simp add: subset_zmset_def subset_mset_def) lemma mset_pos_supset: "A \#\<^sub>z zmset_of (mset_pos A)" and mset_neg_supset: "- A \#\<^sub>z zmset_of (mset_neg A)" by (auto intro: zmset_subset_eqI) lemma subset_mset_zmsetE: assumes "M \#\<^sub>z N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \# B" by (metis assms decompose_zmset_of2 subset_zmset.add_less_cancel_right zmset_of_subset_iff) lemma subseteq_mset_zmsetE: assumes "M \#\<^sub>z N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \# B" by (metis assms add.commute add.right_neutral subset_mset.order_refl subset_mset_def subset_mset_zmsetE subset_zmset_def zmset_of_empty) subsubsection \Subset is an Order\ interpretation subset_zmset: order "(\#\<^sub>z)" "(\#\<^sub>z)" by unfold_locales subsection \Replicate and Repeat Operations\ definition replicate_zmset :: "nat \ 'a \ 'a zmultiset" where "replicate_zmset n x = (add_zmset x ^^ n) {#}\<^sub>z" lemma replicate_zmset_0[simp]: "replicate_zmset 0 x = {#}\<^sub>z" unfolding replicate_zmset_def by simp lemma replicate_zmset_Suc[simp]: "replicate_zmset (Suc n) x = add_zmset x (replicate_zmset n x)" unfolding replicate_zmset_def by (induct n) (auto intro: add.commute) lemma count_replicate_zmset[simp]: "zcount (replicate_zmset n x) y = (if y = x then of_nat n else 0)" unfolding replicate_zmset_def by (induct n) auto fun repeat_zmset :: "nat \ 'a zmultiset \ 'a zmultiset" where "repeat_zmset 0 _ = {#}\<^sub>z" | "repeat_zmset (Suc n) A = A + repeat_zmset n A" lemma count_repeat_zmset[simp]: "zcount (repeat_zmset i A) a = of_nat i * zcount A a" by (induct i) (auto simp: semiring_normalization_rules(3)) lemma repeat_zmset_right[simp]: "repeat_zmset a (repeat_zmset b A) = repeat_zmset (a * b) A" by (auto simp: zmultiset_eq_iff left_diff_distrib') lemma left_diff_repeat_zmset_distrib': \i \ j \ repeat_zmset (i - j) u = repeat_zmset i u - repeat_zmset j u\ by (auto simp: zmultiset_eq_iff int_distrib(3) of_nat_diff) lemma left_add_mult_distrib_zmset: "repeat_zmset i u + (repeat_zmset j u + k) = repeat_zmset (i+j) u + k" by (auto simp: zmultiset_eq_iff add_mult_distrib int_distrib(1)) lemma repeat_zmset_distrib: "repeat_zmset (m + n) A = repeat_zmset m A + repeat_zmset n A" by (auto simp: zmultiset_eq_iff Nat.add_mult_distrib int_distrib(1)) lemma repeat_zmset_distrib2[simp]: "repeat_zmset n (A + B) = repeat_zmset n A + repeat_zmset n B" by (auto simp: zmultiset_eq_iff add_mult_distrib2 int_distrib(2)) lemma repeat_zmset_replicate_zmset[simp]: "repeat_zmset n {#a#}\<^sub>z = replicate_zmset n a" by (auto simp: zmultiset_eq_iff) lemma repeat_zmset_distrib_add_zmset[simp]: "repeat_zmset n (add_zmset a A) = replicate_zmset n a + repeat_zmset n A" by (auto simp: zmultiset_eq_iff int_distrib(2)) lemma repeat_zmset_empty[simp]: "repeat_zmset n {#}\<^sub>z = {#}\<^sub>z" by (induct n) simp_all subsubsection \Filter (with Comprehension Syntax)\ lift_definition filter_zmset :: "('a \ bool) \ 'a zmultiset \ 'a zmultiset" is "\P (Mp, Mn). (filter_mset P Mp, filter_mset P Mn)" by (auto simp del: filter_union_mset simp: equiv_zmset_def filter_union_mset[symmetric]) syntax (ASCII) "_ZMCollect" :: "pttrn \ 'a zmultiset \ bool \ 'a zmultiset" ("(1{#_ :#z _./ _#})") syntax "_ZMCollect" :: "pttrn \ 'a zmultiset \ bool \ 'a zmultiset" ("(1{#_ \#\<^sub>z _./ _#})") translations "{#x \#\<^sub>z M. P#}" == "CONST filter_zmset (\x. P) M" lemma count_filter_zmset[simp]: "zcount (filter_zmset P M) a = (if P a then zcount M a else 0)" by transfer auto lemma filter_empty_zmset[simp]: "filter_zmset P {#}\<^sub>z = {#}\<^sub>z" by (rule zmultiset_eqI) simp lemma filter_single_zmset: "filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)" by (rule zmultiset_eqI) simp lemma filter_union_zmset[simp]: "filter_zmset P (M + N) = filter_zmset P M + filter_zmset P N" by (rule zmultiset_eqI) simp lemma filter_diff_zmset[simp]: "filter_zmset P (M - N) = filter_zmset P M - filter_zmset P N" by (rule zmultiset_eqI) simp lemma filter_add_zmset[simp]: "filter_zmset P (add_zmset x A) = (if P x then add_zmset x (filter_zmset P A) else filter_zmset P A)" by (auto simp: zmultiset_eq_iff) lemma zmultiset_filter_mono: assumes "A \#\<^sub>z B" shows "filter_zmset f A \#\<^sub>z filter_zmset f B" using assms by (simp add: subseteq_zmset_def) lemma filter_filter_zmset: "filter_zmset P (filter_zmset Q M) = {#x \#\<^sub>z M. Q x \ P x#}" by (auto simp: zmultiset_eq_iff) lemma filter_zmset_True[simp]: "{#y \#\<^sub>z M. True#} = M" and filter_zmset_False[simp]: "{#y \#\<^sub>z M. False#} = {#}\<^sub>z" by (auto simp: zmultiset_eq_iff) subsection \Uncategorized\ lemma multi_drop_mem_not_eq_zmset: "B - {#c#}\<^sub>z \ B" by (simp add: diff_single_eq_union_zmset) lemma zmultiset_partition: "M = {#x \#\<^sub>z M. P x #} + {#x \#\<^sub>z M. \ P x#}" by (subst zmultiset_eq_iff) auto subsection \Image\ definition image_zmset :: "('a \ 'b) \ 'a zmultiset \ 'b zmultiset" where "image_zmset f M = zmset_of (fold_mset (add_mset \ f) {#} (mset_pos M)) - zmset_of (fold_mset (add_mset \ f) {#} (mset_neg M))" subsection \Multiset Order\ instantiation zmultiset :: (preorder) order begin lift_definition less_zmultiset :: "'a zmultiset \ 'a zmultiset \ bool" is "\(Mp, Mn) (Np, Nn). Mp + Nn < Mn + Np" proof (clarsimp simp: equiv_zmset_def) fix A1 B2 B1 A2 C1 D2 D1 C2 :: "'a multiset" assume ab: "A1 + A2 = B1 + B2" and cd: "C1 + C2 = D1 + D2" have "A1 + D2 < B2 + C1 \ A1 + A2 + D2 < A2 + B2 + C1" by simp also have "\ \ B1 + B2 + D2 < A2 + B2 + C1" unfolding ab by (rule refl) also have "\ \ B1 + D2 < A2 + C1" by simp also have "\ \ B1 + D1 + D2 < A2 + C1 + D1" by simp also have "\ \ B1 + C1 + C2 < A2 + C1 + D1" using cd by (simp add: add.assoc) also have "\ \ B1 + C2 < A2 + D1" by simp finally show "A1 + D2 < B2 + C1 \ B1 + C2 < A2 + D1" by assumption qed definition less_eq_zmultiset :: "'a zmultiset \ 'a zmultiset \ bool" where "less_eq_zmultiset M' M \ M' < M \ M' = M" instance proof ((intro_classes; unfold less_eq_zmultiset_def; transfer), auto simp: equiv_zmset_def union_commute) fix A1 B1 D C B2 A2 :: "'a multiset" assume ab: "A1 + A2 \ B1 + B2" { assume ab1: "A1 + C < B1 + D" { assume ab2: "D + A2 < C + B2" show "A1 + A2 < B1 + B2" proof - have f1: "\m. D + A2 + m < C + B2 + m" using ab2 add_less_cancel_right by blast have "\m. C + (A1 + m) < D + (B1 + m)" by (simp add: ab1 add.commute) then have "D + (A2 + A1) < D + (B1 + B2)" using f1 by (metis add.assoc add.commute mset_le_trans) then show ?thesis by (simp add: add.commute) qed } { assume ab2: "D + A2 = C + B2" show "A1 + A2 < B1 + B2" proof - have "\m. C + A1 + m < D + B1 + m" by (simp add: ab1 add.commute) then have "D + (A2 + A1) < D + (B1 + B2)" by (metis (no_types) ab2 add.assoc add.commute) then show ?thesis by (simp add: add.commute) qed } } { assume ab1: "A1 + C = B1 + D" { assume ab2: "D + A2 < C + B2" show "A1 + A2 < B1 + B2" proof - have "A1 + (D + A2) < B1 + (D + B2)" by (metis (no_types) ab1 ab2 add.assoc add_less_cancel_left) then show ?thesis by simp qed } { assume ab2: "D + A2 = C + B2" have False by (metis (no_types) ab ab1 ab2 add.assoc add.commute add_diff_cancel_right') thus "A1 + A2 < B1 + B2" by sat } } qed end instance zmultiset :: (preorder) ordered_cancel_comm_monoid_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def) instance zmultiset :: (preorder) ordered_ab_group_add by (intro_classes; transfer; auto simp: equiv_zmset_def) instantiation zmultiset :: (linorder) distrib_lattice begin definition inf_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" where "inf_zmultiset A B = (if A < B then A else B)" definition sup_zmultiset :: "'a zmultiset \ 'a zmultiset \ 'a zmultiset" where "sup_zmultiset A B = (if B > A then B else A)" lemma not_lt_iff_ge_zmset: "\ x < y \ x \ y" for x y :: "'a zmultiset" by (unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def algebra_simps) instance by intro_classes (auto simp: less_eq_zmultiset_def inf_zmultiset_def sup_zmultiset_def dest!: not_lt_iff_ge_zmset[THEN iffD1]) end lemma zmset_of_less: "zmset_of M < zmset_of N \ M < N" by (clarsimp simp: zmset_of_def, transfer, simp)+ lemma zmset_of_le: "zmset_of M \ zmset_of N \ M \ N" by (simp_all add: less_eq_zmultiset_def zmset_of_def; transfer; auto simp: equiv_zmset_def) instance zmultiset :: (preorder) ordered_ab_semigroup_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def) lemma uminus_add_conv_diff_mset[cancelation_simproc_pre]: \-a + b = b - a\ for a :: \'a zmultiset\ by (simp add: add.commute) lemma uminus_add_add_uminus[cancelation_simproc_pre]: \b -a + c = b + c - a\ for a :: \'a zmultiset\ by (simp add: uminus_add_conv_diff_mset zmset_subset_eq_zmultiset_union_diff_commute) lemma add_zmset_eq_add_NO_MATCH[cancelation_simproc_pre]: \NO_MATCH {#}\<^sub>z H \ add_zmset a H = {#a#}\<^sub>z + H\ by auto lemma repeat_zmset_iterate_add: \repeat_zmset n M = iterate_add n M\ unfolding iterate_add_def by (induction n) auto declare repeat_zmset_iterate_add[cancelation_simproc_pre] declare repeat_zmset_iterate_add[symmetric, cancelation_simproc_post] simproc_setup zmseteq_cancel_numerals ("(l::'a zmultiset) + m = n" | "(l::'a zmultiset) = m + n" | "add_zmset a m = n" | "m = add_zmset a n" | "replicate_zmset p a = n" | "m = replicate_zmset p a" | "repeat_zmset p m = n" | "m = repeat_zmset p m") = \fn phi => Cancel_Simprocs.eq_cancel\ lemma zmset_subseteq_add_iff1: \j \ i \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m \#\<^sub>z n)\ by (simp add: add.commute add_diff_eq left_diff_repeat_zmset_distrib' subset_eq_diff_conv_zmset) lemma zmset_subseteq_add_iff2: \i \ j \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (m \#\<^sub>z repeat_zmset (j - i) u + n)\ proof - assume "i \ j" then have "\z. repeat_zmset j (z::'a zmultiset) - repeat_zmset i z = repeat_zmset (j - i) z" by (simp add: left_diff_repeat_zmset_distrib') then show ?thesis by (metis add.commute diff_diff_eq2 subset_eq_diff_conv_zmset) qed lemma zmset_subset_add_iff1: \j \ i \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m \#\<^sub>z n)\ by (simp add: subset_zmset.less_le_not_le zmset_subseteq_add_iff1 zmset_subseteq_add_iff2) lemma zmset_subset_add_iff2: \i \ j \ (repeat_zmset i u + m \#\<^sub>z repeat_zmset j u + n) = (m \#\<^sub>z repeat_zmset (j - i) u + n)\ by (simp add: subset_zmset.less_le_not_le zmset_subseteq_add_iff1 zmset_subseteq_add_iff2) ML_file \zmultiset_simprocs.ML\ simproc_setup zmsetsubset_cancel ("(l::'a zmultiset) + m \#\<^sub>z n" | "(l::'a zmultiset) \#\<^sub>z m + n" | "add_zmset a m \#\<^sub>z n" | "m \#\<^sub>z add_zmset a n" | "replicate_zmset p a \#\<^sub>z n" | "m \#\<^sub>z replicate_zmset p a" | "repeat_zmset p m \#\<^sub>z n" | "m \#\<^sub>z repeat_zmset p m") = \fn phi => ZMultiset_Simprocs.subset_cancel_zmsets\ simproc_setup zmsetsubseteq_cancel ("(l::'a zmultiset) + m \#\<^sub>z n" | "(l::'a zmultiset) \#\<^sub>z m + n" | "add_zmset a m \#\<^sub>z n" | "m \#\<^sub>z add_zmset a n" | "replicate_zmset p a \#\<^sub>z n" | "m \#\<^sub>z replicate_zmset p a" | "repeat_zmset p m \#\<^sub>z n" | "m \#\<^sub>z repeat_zmset p m") = \fn phi => ZMultiset_Simprocs.subseteq_cancel_zmsets\ instance zmultiset :: (preorder) ordered_ab_semigroup_add_imp_le by (intro_classes; unfold less_eq_zmultiset_def; transfer; auto) simproc_setup zmsetless_cancel ("(l::'a::preorder zmultiset) + m < n" | "(l::'a zmultiset) < m + n" | "add_zmset a m < n" | "m < add_zmset a n" | "replicate_zmset p a < n" | "m < replicate_zmset p a" | "repeat_zmset p m < n" | "m < repeat_zmset p m") = \fn phi => Cancel_Simprocs.less_cancel\ simproc_setup zmsetless_eq_cancel ("(l::'a::preorder zmultiset) + m \ n" | "(l::'a zmultiset) \ m + n" | "add_zmset a m \ n" | "m \ add_zmset a n" | "replicate_zmset p a \ n" | "m \ replicate_zmset p a" | "repeat_zmset p m \ n" | "m \ repeat_zmset p m") = \fn phi => Cancel_Simprocs.less_eq_cancel\ simproc_setup zmsetdiff_cancel ("n + (l::'a zmultiset)" | "(l::'a zmultiset) - m" | "add_zmset a m - n" | "m - add_zmset a n" | "replicate_zmset p r - n" | "m - replicate_zmset p r" | "repeat_zmset p m - n" | "m - repeat_zmset p m") = \fn phi => Cancel_Simprocs.diff_cancel\ instance zmultiset :: (linorder) linordered_cancel_ab_semigroup_add by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def add.commute) lemma less_mset_zmsetE: assumes "M < N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A < B" by (metis add_less_imp_less_right assms decompose_zmset_of2 zmset_of_less) lemma less_eq_mset_zmsetE: assumes "M \ N" obtains A B C where "M = zmset_of A + C" and "N = zmset_of B + C" and "A \ B" by (metis add.commute add.right_neutral assms le_neq_trans less_imp_le less_mset_zmsetE order_refl zmset_of_empty) lemma subset_eq_imp_le_zmset: "M \#\<^sub>z N \ M \ N" by (metis (no_types) add_mono_thms_linordered_semiring(3) subset_eq_imp_le_multiset subseteq_mset_zmsetE zmset_of_le) lemma subset_imp_less_zmset: "M \#\<^sub>z N \ M < N" by (metis le_neq_trans subset_eq_imp_le_zmset subset_zmset_def) lemma lt_imp_ex_zcount_lt: assumes m_lt_n: "M < N" shows "\y. zcount M y < zcount N y" proof (rule ccontr, clarsimp) assume "\y. \ zcount M y < zcount N y" hence "\y. zcount M y \ zcount N y" by (simp add: leI) hence "M \#\<^sub>z N" by (simp add: zmset_subset_eqI) hence "M \ N" by (simp add: subset_eq_imp_le_zmset) thus False using m_lt_n by simp qed instance zmultiset :: (preorder) no_top proof fix M :: \'a zmultiset\ obtain a :: 'a where True by fast let ?M = \zmset_of (mset_pos M) + zmset_of (mset_neg M)\ have \M < add_zmset a ?M + ?M\ by (subst mset_pos_neg_partition) (auto simp: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff intro!: subset_imp_less_zmset) then show \\N. M < N\ by blast qed end diff --git a/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy b/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy --- a/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy +++ b/thys/Pi_Transcendental/Pi_Transcendental_Polynomial_Library.thy @@ -1,381 +1,381 @@ (* File: Pi_Transcendental_Polynomial_Library Author: Manuel Eberl, TU München Various facts about univariate polynomials and some other things that probably belong in the distribution. *) section \Preliminary facts\ theory Pi_Transcendental_Polynomial_Library imports "HOL-Computational_Algebra.Computational_Algebra" begin (* TODO: Move all this *) lemma Ints_sum: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto lemma Ints_prod: "(\x. x \ A \ f x \ \) \ prod f A \ \" by (induction A rule: infinite_finite_induct) auto lemma sum_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto lemma prod_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ prod f A \ \" by (induction A rule: infinite_finite_induct) auto lemma poly_cnj: "cnj (poly p z) = poly (map_poly cnj p) (cnj z)" by (simp add: poly_altdef degree_map_poly coeff_map_poly) lemma poly_cnj_real: assumes "\n. poly.coeff p n \ \" shows "cnj (poly p z) = poly p (cnj z)" proof - from assms have "map_poly cnj p = p" by (intro poly_eqI) (auto simp: coeff_map_poly Reals_cnj_iff) with poly_cnj[of p z] show ?thesis by simp qed lemma real_poly_cnj_root_iff: assumes "\n. poly.coeff p n \ \" shows "poly p (cnj z) = 0 \ poly p z = 0" proof - have "poly p (cnj z) = cnj (poly p z)" by (simp add: poly_cnj_real assms) also have "\ = 0 \ poly p z = 0" by simp finally show ?thesis . qed lemma coeff_pcompose_linear: fixes p :: "'a :: comm_semiring_1 poly" shows "coeff (pcompose p [:0, c:]) i = c ^ i * coeff p i" by (induction p arbitrary: i) (auto simp: pcompose_pCons coeff_pCons mult_ac split: nat.splits) lemma coeff_pCons': "poly.coeff (pCons c p) n = (if n = 0 then c else poly.coeff p (n - 1))" by transfer'(auto split: nat.splits) lemma prod_smult: "(\x\A. Polynomial.smult (c x) (p x)) = Polynomial.smult (prod c A) (prod p A)" by (induction A rule: infinite_finite_induct) (auto simp: mult_ac) lemma degree_higher_pderiv: "Polynomial.degree ((pderiv ^^ n) p) = Polynomial.degree p - n" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" by (induction n) (auto simp: degree_pderiv) lemma sum_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" by (induction A rule: infinite_finite_induct) auto lemma diff_to_poly: "[:c:] - [:d:] = [:c - d:]" by (simp add: poly_eq_iff mult_ac) lemma mult_to_poly: "[:c:] * [:d:] = [:c * d:]" by (simp add: poly_eq_iff mult_ac) lemma prod_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" by (induction A rule: infinite_finite_induct) (auto simp: mult_to_poly mult_ac) lemma coeff_mult_0: "poly.coeff (p * q) 0 = poly.coeff p 0 * poly.coeff q 0" by (simp add: coeff_mult) lemma card_poly_roots_bound: fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" assumes "p \ 0" shows "card {x. poly p x = 0} \ degree p" using assms proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "\x. poly p x = 0") case False hence "{x. poly p x = 0} = {}" by blast thus ?thesis by simp next case True then obtain x where x: "poly p x = 0" by blast hence "[:-x, 1:] dvd p" by (subst (asm) poly_eq_0_iff_dvd) then obtain q where q: "p = [:-x, 1:] * q" by (auto simp: dvd_def) with \p \ 0\ have [simp]: "q \ 0" by auto have deg: "degree p = Suc (degree q)" by (subst q, subst degree_mult_eq) auto have "card {x. poly p x = 0} \ card (insert x {x. poly q x = 0})" by (intro card_mono) (auto intro: poly_roots_finite simp: q) also have "\ \ Suc (card {x. poly q x = 0})" by (rule card_insert_le_m1) auto also from deg have "card {x. poly q x = 0} \ degree q" using \p \ 0\ and q by (intro less) auto also have "Suc \ = degree p" by (simp add: deg) finally show ?thesis by - simp_all qed qed lemma poly_eqI_degree: fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" assumes "\x. x \ A \ poly p x = poly q x" assumes "card A > degree p" "card A > degree q" shows "p = q" proof (rule ccontr) assume neq: "p \ q" have "degree (p - q) \ max (degree p) (degree q)" by (rule degree_diff_le_max) also from assms have "\ < card A" by linarith also have "\ \ card {x. poly (p - q) x = 0}" using neq and assms by (intro card_mono poly_roots_finite) auto finally have "degree (p - q) < card {x. poly (p - q) x = 0}" . moreover have "degree (p - q) \ card {x. poly (p - q) x = 0}" using neq by (intro card_poly_roots_bound) auto ultimately show False by linarith qed lemma poly_root_order_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes "P 0" "\p. (\x. poly p x \ 0) \ P p" "\p x n. n > 0 \ poly p x \ 0 \ P p \ P ([:-x, 1:] ^ n * p)" shows "P p" proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) consider "p = 0" | "p \ 0" "\x. poly p x = 0" | "\x. poly p x \ 0" by blast thus ?case proof cases case 3 with assms(2)[of p] show ?thesis by simp next case 2 then obtain x where x: "poly p x = 0" by auto have "[:-x, 1:] ^ order x p dvd p" by (intro order_1) then obtain q where q: "p = [:-x, 1:] ^ order x p * q" by (auto simp: dvd_def) with 2 have [simp]: "q \ 0" by auto have order_pos: "order x p > 0" using \p \ 0\ and x by (auto simp: order_root) have "order x p = order x p + order x q" by (subst q, subst order_mult) (auto simp: order_power_n_n) hence [simp]: "order x q = 0" by simp have deg: "degree p = order x p + degree q" by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq) with order_pos have "degree q < degree p" by simp hence "P q" by (rule less) with order_pos have "P ([:-x, 1:] ^ order x p * q)" by (intro assms(3)) (auto simp: order_root) with q show ?thesis by simp qed (simp_all add: assms(1)) qed lemma complex_poly_decompose: "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:] ^ order z p) = (p :: complex poly)" proof (induction p rule: poly_root_order_induct) case (no_roots p) show ?case proof (cases "degree p = 0") case False hence "\constant (poly p)" by (subst constant_degree) with fundamental_theorem_of_algebra and no_roots show ?thesis by blast qed (auto elim!: degree_eq_zeroE) next case (root p x n) from root have *: "{z. poly ([:- x, 1:] ^ n * p) z = 0} = insert x {z. poly p z = 0}" by auto have "smult (lead_coeff ([:-x, 1:] ^ n * p)) (\z|poly ([:-x,1:] ^ n * p) z = 0. [:-z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = [:- x, 1:] ^ order x ([:- x, 1:] ^ n * p) * smult (lead_coeff p) (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p))" by (subst *, subst prod.insert) (insert root, auto intro: poly_roots_finite simp: mult_ac lead_coeff_mult lead_coeff_power) also have "order x ([:- x, 1:] ^ n * p) = n" using root by (subst order_mult) (auto simp: order_power_n_n order_0I) also have "(\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z p)" proof (intro prod.cong refl, goal_cases) case (1 y) with root have "order y ([:-x,1:] ^ n) = 0" by (intro order_0I) auto thus ?case using root by (subst order_mult) auto qed also note root.IH finally show ?case . qed simp_all lemma order_pos_iff: "p \ 0 \ order a p > 0 \ poly p a = 0" using order_root[of p a] by auto lift_definition poly_roots_mset :: "('a :: idom) poly \ 'a multiset" is "\p x. if p = 0 then 0 else Polynomial.order x p" proof - fix p :: "'a poly" - show "(\x. if p = 0 then 0 else order x p) \ multiset" + show "finite {x. 0 < (if p = 0 then 0 else order x p)}" by (cases "p = 0") - (auto simp: multiset_def order_pos_iff intro: finite_subset[OF _ poly_roots_finite[of p]]) + (auto simp: order_pos_iff intro: finite_subset[OF _ poly_roots_finite[of p]]) qed lemma poly_roots_mset_0 [simp]: "poly_roots_mset 0 = {#}" by transfer' auto lemma count_poly_roots_mset [simp]: "p \ 0 \ count (poly_roots_mset p) a = order a p" by transfer' auto lemma set_count_poly_roots_mset [simp]: "p \ 0 \ set_mset (poly_roots_mset p) = {x. poly p x = 0}" by (auto simp: set_mset_def order_pos_iff) lemma image_prod_mset_multiplicity: "prod_mset (image_mset f M) = prod (\x. f x ^ count M x) (set_mset M)" proof (induction M) case (add x M) show ?case proof (cases "x \ set_mset M") case True have "(\y\set_mset (add_mset x M). f y ^ count (add_mset x M) y) = (\y\set_mset M. (if y = x then f x else 1) * f y ^ count M y)" using True add by (intro prod.cong) auto also have "\ = f x * (\y\set_mset M. f y ^ count M y)" using True by (subst prod.distrib) auto also note add.IH [symmetric] finally show ?thesis using True by simp next case False hence "(\y\set_mset (add_mset x M). f y ^ count (add_mset x M) y) = f x * (\y\set_mset M. f y ^ count (add_mset x M) y)" by (auto simp: not_in_iff) also have "(\y\set_mset M. f y ^ count (add_mset x M) y) = (\y\set_mset M. f y ^ count M y)" using False by (intro prod.cong) auto also note add.IH [symmetric] finally show ?thesis by simp qed qed auto lemma complex_poly_decompose_multiset: "smult (lead_coeff p) (\x\#poly_roots_mset p. [:-x, 1:]) = (p :: complex poly)" proof (cases "p = 0") case False hence "(\x\#poly_roots_mset p. [:-x, 1:]) = (\x | poly p x = 0. [:-x, 1:] ^ order x p)" by (subst image_prod_mset_multiplicity) simp_all also have "smult (lead_coeff p) \ = p" by (rule complex_poly_decompose) finally show ?thesis . qed auto lemma (in monoid_add) prod_list_prod_nth: "prod_list xs = (\i=0..i. xs ! i) [0.. = (\i=0.. prod f A = 0 \ (\x\A. f x = 0)" for f :: "'a \ 'b :: {comm_semiring_1, semiring_no_zero_divisors}" by (induction A rule: infinite_finite_induct) auto lemma degree_prod_eq: "(\x. x \ A \ f x \ 0) \ degree (prod f A) = (\x\A. degree (f x))" for f :: "'a \ 'b::{comm_semiring_1, semiring_no_zero_divisors} poly" by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq prod_zero_iff') lemma lead_coeff_prod: "(\x. x \ A \ f x \ 0) \ lead_coeff (prod f A) = (\x\A. lead_coeff (f x))" for f :: "'a \ 'b :: {comm_semiring_1, semiring_no_zero_divisors} poly" by (induction A rule: infinite_finite_induct) (auto simp: lead_coeff_mult prod_zero_iff') lemma complex_poly_decompose': obtains root where "smult (lead_coeff p) (\ix\#poly_roots_mset p. [:-x, 1:])" by (rule complex_poly_decompose_multiset [symmetric]) also have "(\x\#poly_roots_mset p. [:-x, 1:]) = (\x\roots. [:-x, 1:])" by (subst prod_mset_prod_list [symmetric]) (simp add: roots) also have "\ = (\iii. roots ! i"]) auto qed lemma rsquarefree_root_order: assumes "rsquarefree p" "poly p z = 0" "p \ 0" shows "order z p = 1" proof - from assms have "order z p \ {0, 1}" by (auto simp: rsquarefree_def) moreover from assms have "order z p > 0" by (auto simp: order_root) ultimately show "order z p = 1" by auto qed lemma complex_poly_decompose_rsquarefree: assumes "rsquarefree p" shows "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:]) = (p :: complex poly)" proof (cases "p = 0") case False have "(\z|poly p z = 0. [:-z, 1:]) = (\z|poly p z = 0. [:-z, 1:] ^ order z p)" using assms False by (intro prod.cong) (auto simp: rsquarefree_root_order) also have "smult (lead_coeff p) \ = p" by (rule complex_poly_decompose) finally show ?thesis . qed auto lemma pcompose_conjugates_integer: assumes "\i. poly.coeff p i \ \" shows "poly.coeff (pcompose p [:0, \:] * pcompose p [:0, -\:]) i \ \" proof - let ?c = "\i. poly.coeff p i :: complex" have "poly.coeff (pcompose p [:0, \:] * pcompose p [:0, -\:]) i = \ ^ i * (\k\i. (-1) ^ (i - k) * ?c k * ?c (i - k))" unfolding coeff_mult sum_distrib_left by (intro sum.cong) (auto simp: coeff_mult coeff_pcompose_linear power_minus' power_diff field_simps intro!: Ints_sum) also have "(\k\i. (-1) ^ (i - k) * ?c k * ?c (i - k)) = (\k\i. (-1) ^ k * ?c k * ?c (i - k))" (is "?S1 = ?S2") by (intro sum.reindex_bij_witness[of _ "\k. i - k" "\k. i - k"]) (auto simp: mult_ac) hence "?S1 = (?S1 + ?S2) / 2" by simp also have "\ = (\k\i. ((-1) ^ k + (-1) ^ (i - k)) / 2 * ?c k * ?c (i - k))" by (simp add: ring_distribs sum.distrib sum_divide_distrib [symmetric]) also have "\ = (\k\i. (1 + (-1) ^ i) / 2 * (-1) ^ k * ?c k * ?c (i - k))" by (intro sum.cong) (auto simp: power_add power_diff field_simps) also have "\ ^ i * \ \ \" proof (cases "even i") case True thus ?thesis by (intro Ints_mult Ints_sum assms) (auto elim!: evenE simp: power_mult) next case False hence "1 + (-1) ^ i = (0 :: complex)" by (auto elim!: oddE simp: power_mult) thus ?thesis by simp qed finally show ?thesis . qed lemma algebraic_times_i: assumes "algebraic x" shows "algebraic (\ * x)" "algebraic (-\ * x)" proof - from assms obtain p where p: "poly p x = 0" "\i. coeff p i \ \" "p \ 0" by (auto elim!: algebraicE) define p' where "p' = pcompose p [:0, \:] * pcompose p [:0, -\:]" have p': "poly p' (\ * x) = 0" "poly p' (-\ * x) = 0" "p' \ 0" by (auto simp: p'_def poly_pcompose algebra_simps p dest: pcompose_eq_0) moreover have "\i. poly.coeff p' i \ \" using p unfolding p'_def by (intro allI pcompose_conjugates_integer) auto ultimately show "algebraic (\ * x)" "algebraic (-\ * x)" by (intro algebraicI[of p']; simp)+ qed lemma algebraic_times_i_iff: "algebraic (\ * x) \ algebraic x" using algebraic_times_i[of x] algebraic_times_i[of "\ * x"] by auto lemma ratpolyE: assumes "\i. poly.coeff p i \ \" obtains q where "p = map_poly of_rat q" proof - have "\i\{..Polynomial.degree p}. \x. poly.coeff p i = of_rat x" using assms by (auto simp: Rats_def) from bchoice[OF this] obtain f where f: "\i. i \ Polynomial.degree p \ poly.coeff p i = of_rat (f i)" by blast define q where "q = Poly (map f [0..Auxiliary material\ theory Power_Sum_Polynomials_Library imports "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized" "Symmetric_Polynomials.Symmetric_Polynomials" "HOL-Computational_Algebra.Computational_Algebra" begin subsection \Miscellaneous\ lemma atLeastAtMost_nat_numeral: "atLeastAtMost m (numeral k :: nat) = (if m \ numeral k then insert (numeral k) (atLeastAtMost m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastAtMostSuc_conv) lemma sum_in_Rats [intro]: "(\x. x \ A \ f x \ \) \ sum f A \ \" by (induction A rule: infinite_finite_induct) auto (* TODO Move *) lemma (in monoid_mult) prod_list_distinct_conv_prod_set: "distinct xs \ prod_list (map f xs) = prod f (set xs)" by (induct xs) simp_all lemma (in monoid_mult) interv_prod_list_conv_prod_set_nat: "prod_list (map f [m..i = 0..< length xs. xs ! i)" using interv_prod_list_conv_prod_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth) lemma gcd_poly_code_aux_reduce: "gcd_poly_code_aux p 0 = normalize p" "q \ 0 \ gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))" by (subst gcd_poly_code_aux.simps; simp)+ lemma coprimeI_primes: fixes a b :: "'a :: factorial_semiring" assumes "a \ 0 \ b \ 0" assumes "\p. prime p \ p dvd a \ p dvd b \ False" shows "coprime a b" proof (rule coprimeI) fix d assume d: "d dvd a" "d dvd b" with assms(1) have [simp]: "d \ 0" by auto show "is_unit d" proof (rule ccontr) assume "\is_unit d" then obtain p where p: "prime p" "p dvd d" using prime_divisor_exists[of d] by auto from assms(2)[of p] and p and d show False using dvd_trans by auto qed qed lemma coprime_pderiv_imp_squarefree: assumes "coprime p (pderiv p)" shows "squarefree p" proof (rule squarefreeI) fix d assume d: "d ^ 2 dvd p" then obtain q where q: "p = d ^ 2 * q" by (elim dvdE) hence "d dvd p" "d dvd pderiv p" by (auto simp: pderiv_mult pderiv_power_Suc numeral_2_eq_2) with assms show "is_unit d" using not_coprimeI by blast qed lemma squarefree_field_poly_iff: fixes p :: "'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly" assumes [simp]: "p \ 0" shows "squarefree p \ coprime p (pderiv p)" proof assume "squarefree p" show "coprime p (pderiv p)" proof (rule coprimeI_primes) fix d assume d: "d dvd p" "d dvd pderiv p" "prime d" from d(1) obtain q where q: "p = d * q" by (elim dvdE) from d(2) and q have "d dvd q * pderiv d" by (simp add: pderiv_mult dvd_add_right_iff) with \prime d\ have "d dvd q \ d dvd pderiv d" using prime_dvd_mult_iff by blast thus False proof assume "d dvd q" hence "d ^ 2 dvd p" by (auto simp: q power2_eq_square) with \squarefree p\ show False using d(3) not_prime_unit squarefreeD by blast next assume "d dvd pderiv d" hence "Polynomial.degree d = 0" by simp moreover have "d \ 0" using d by auto ultimately show False using d(3) is_unit_iff_degree not_prime_unit by blast qed qed auto qed (use coprime_pderiv_imp_squarefree[of p] in auto) lemma coprime_pderiv_imp_rsquarefree: assumes "coprime (p :: 'a :: field_char_0 poly) (pderiv p)" shows "rsquarefree p" unfolding rsquarefree_roots proof safe fix x assume "poly p x = 0" "poly (pderiv p) x = 0" hence "[:-x, 1:] dvd p" "[:-x, 1:] dvd pderiv p" by (auto simp: poly_eq_0_iff_dvd) with assms have "is_unit [:-x, 1:]" using not_coprimeI by blast thus False by auto qed lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n" by (induction n) auto lemma poly_of_int [simp]: "poly (of_int n) x = of_int n" by (cases n) auto lemma order_eq_0_iff: "p \ 0 \ order x p = 0 \ poly p x \ 0" by (auto simp: order_root) lemma order_pos_iff: "p \ 0 \ order x p > 0 \ poly p x = 0" by (auto simp: order_root) lemma order_prod: assumes "\x. x \ A \ f x \ 0" shows "order x (\y\A. f y) = (\y\A. order x (f y))" using assms by (induction A rule: infinite_finite_induct) (auto simp: order_mult) lemma order_prod_mset: assumes "0 \# A" shows "order x (prod_mset A) = sum_mset (image_mset (order x) A)" using assms by (induction A) (auto simp: order_mult) lemma order_prod_list: assumes "0 \ set xs" shows "order x (prod_list xs) = sum_list (map (order x) xs)" using assms by (induction xs) (auto simp: order_mult) lemma order_power: "p \ 0 \ order x (p ^ n) = n * order x p" by (induction n) (auto simp: order_mult) lemma smult_0_right [simp]: "MPoly_Type.smult p 0 = 0" by (transfer, transfer) auto lemma mult_smult_right [simp]: fixes c :: "'a :: comm_semiring_0" shows "p * MPoly_Type.smult c q = MPoly_Type.smult c (p * q)" by (simp add: smult_conv_mult mult_ac) lemma mapping_single_eq_iff [simp]: "Poly_Mapping.single a b = Poly_Mapping.single c d \ b = 0 \ d = 0 \ a = c \ b = d" by transfer (unfold fun_eq_iff when_def, metis) lemma monom_of_set_plus_monom_of_set: assumes "A \ B = {}" "finite A" "finite B" shows "monom_of_set A + monom_of_set B = monom_of_set (A \ B)" using assms by transfer (auto simp: fun_eq_iff) lemma mpoly_monom_0_eq_Const: "monom 0 c = Const c" by (intro mpoly_eqI) (auto simp: coeff_monom when_def mpoly_coeff_Const) lemma mpoly_Const_0 [simp]: "Const 0 = 0" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_0) lemma mpoly_Const_1 [simp]: "Const 1 = 1" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1) lemma mpoly_Const_uminus: "Const (-a) = -Const a" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) lemma mpoly_Const_add: "Const (a + b) = Const a + Const b" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) lemma mpoly_Const_mult: "Const (a * b) = Const a * Const b" unfolding mpoly_monom_0_eq_Const [symmetric] mult_monom by simp lemma mpoly_Const_power: "Const (a ^ n) = Const a ^ n" by (induction n) (auto simp: mpoly_Const_mult) lemma of_nat_mpoly_eq: "of_nat n = Const (of_nat n)" proof (induction n) case 0 have "0 = (Const 0 :: 'a mpoly)" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const) thus ?case by simp next case (Suc n) have "1 + Const (of_nat n) = Const (1 + of_nat n)" by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1) thus ?case using Suc by auto qed lemma insertion_of_nat [simp]: "insertion f (of_nat n) = of_nat n" by (simp add: of_nat_mpoly_eq) lemma insertion_monom_of_set [simp]: "insertion f (monom (monom_of_set X) c) = c * (\i\X. f i)" proof (cases "finite X") case [simp]: True have "insertion f (monom (monom_of_set X) c) = c * (\a. f a ^ (if a \ X then 1 else 0))" by (auto simp: lookup_monom_of_set) also have "(\a. f a ^ (if a \ X then 1 else 0)) = (\i\X. f i ^ (if i \ X then 1 else 0))" by (intro Prod_any.expand_superset) auto also have "\ = (\i\X. f i)" by (intro prod.cong) auto finally show ?thesis . qed (auto simp: lookup_monom_of_set) (* TODO: Move! Version in AFP is too weak! *) lemma symmetric_mpoly_symmetric_sum: assumes "\\. \ permutes A \ g \ permutes X" assumes "\x \. x \ X \ \ permutes A \ mpoly_map_vars \ (f x) = f (g \ x)" shows "symmetric_mpoly A (\x\X. f x)" unfolding symmetric_mpoly_def proof safe fix \ assume \: "\ permutes A" have "mpoly_map_vars \ (sum f X) = (\x\X. mpoly_map_vars \ (f x))" by simp also have "\ = (\x\X. f (g \ x))" by (intro sum.cong assms \ refl) also have "\ = (\x\g \`X. f x)" using assms(1)[OF \] by (subst sum.reindex) (auto simp: permutes_inj_on) also have "g \ ` X = X" using assms(1)[OF \] by (simp add: permutes_image) finally show "mpoly_map_vars \ (sum f X) = sum f X" . qed lemma sym_mpoly_0 [simp]: assumes "finite A" shows "sym_mpoly A 0 = 1" using assms by (transfer, transfer) (auto simp: fun_eq_iff when_def) lemma sym_mpoly_eq_0 [simp]: assumes "k > card A" shows "sym_mpoly A k = 0" proof (transfer fixing: A k, transfer fixing: A k, intro ext) fix mon have "\(finite A \ (\Y\A. card Y = k \ mon = monom_of_set Y))" proof safe fix Y assume Y: "finite A" "Y \ A" "k = card Y" "mon = monom_of_set Y" hence "card Y \ card A" by (intro card_mono) auto with Y and assms show False by simp qed thus "(if finite A \ (\Y\A. card Y = k \ mon = monom_of_set Y) then 1 else 0) = 0" by auto qed lemma coeff_sym_mpoly_monom_of_set_eq_0: assumes "finite X" "Y \ X" "card Y \ k" shows "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0" using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) lemma coeff_sym_mpoly_monom_of_set_eq_0': assumes "finite X" "\Y \ X" "finite Y" shows "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0" using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) subsection \The set of roots of a univariate polynomial\ lift_definition poly_roots :: "'a :: idom poly \ 'a multiset" is "\p x. if p = 0 then 0 else order x p" proof - fix p :: "'a poly" - show "(\x. if p = 0 then 0 else order x p) \ multiset" - by (cases "p = 0") (auto simp: multiset_def order_pos_iff poly_roots_finite) + show "finite {x. 0 < (if p = 0 then 0 else order x p)}" + by (cases "p = 0") (auto simp: order_pos_iff poly_roots_finite) qed lemma poly_roots_0 [simp]: "poly_roots 0 = {#}" by transfer auto lemma poly_roots_1 [simp]: "poly_roots 1 = {#}" by transfer auto lemma count_poly_roots [simp]: assumes "p \ 0" shows "count (poly_roots p) x = order x p" using assms by transfer auto lemma in_poly_roots_iff [simp]: "p \ 0 \ x \# poly_roots p \ poly p x = 0" by (subst count_greater_zero_iff [symmetric], subst count_poly_roots) (auto simp: order_pos_iff) lemma set_mset_poly_roots: "p \ 0 \ set_mset (poly_roots p) = {x. poly p x = 0}" using in_poly_roots_iff[of p] by blast lemma count_poly_roots': "count (poly_roots p) x = (if p = 0 then 0 else order x p)" by transfer' auto lemma poly_roots_const [simp]: "poly_roots [:c:] = {#}" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff) lemma poly_roots_linear [simp]: "poly_roots [:-x, 1:] = {#x#}" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff) lemma poly_roots_monom [simp]: "c \ 0 \ poly_roots (Polynomial.monom c n) = replicate_mset n 0" by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff poly_monom) lemma poly_roots_smult [simp]: "c \ 0 \ poly_roots (Polynomial.smult c p) = poly_roots p" by (intro multiset_eqI) (auto simp: count_poly_roots' order_smult) lemma poly_roots_mult: "p \ 0 \ q \ 0 \ poly_roots (p * q) = poly_roots p + poly_roots q" by (intro multiset_eqI) (auto simp: count_poly_roots' order_mult) lemma poly_roots_prod: assumes "\x. x \ A \ f x \ 0" shows "poly_roots (prod f A) = (\x\A. poly_roots (f x))" using assms by (induction A rule: infinite_finite_induct) (auto simp: poly_roots_mult) lemma poly_roots_prod_mset: assumes "0 \# A" shows "poly_roots (prod_mset A) = sum_mset (image_mset poly_roots A)" using assms by (induction A) (auto simp: poly_roots_mult) lemma poly_roots_prod_list: assumes "0 \ set xs" shows "poly_roots (prod_list xs) = sum_list (map poly_roots xs)" using assms by (induction xs) (auto simp: poly_roots_mult) lemma poly_roots_power: "p \ 0 \ poly_roots (p ^ n) = repeat_mset n (poly_roots p)" by (induction n) (auto simp: poly_roots_mult) lemma rsquarefree_poly_roots_eq: assumes "rsquarefree p" shows "poly_roots p = mset_set {x. poly p x = 0}" proof (rule multiset_eqI) fix x :: 'a from assms show "count (poly_roots p) x = count (mset_set {x. poly p x = 0}) x" by (cases "poly p x = 0") (auto simp: poly_roots_finite order_eq_0_iff rsquarefree_def) qed lemma rsquarefree_imp_distinct_roots: assumes "rsquarefree p" and "mset xs = poly_roots p" shows "distinct xs" proof (cases "p = 0") case [simp]: False have *: "mset xs = mset_set {x. poly p x = 0}" using assms by (simp add: rsquarefree_poly_roots_eq) hence "set_mset (mset xs) = set_mset (mset_set {x. poly p x = 0})" by (simp only: ) hence [simp]: "set xs = {x. poly p x = 0}" by (simp add: poly_roots_finite) from * show ?thesis by (subst distinct_count_atmost_1) (auto simp: poly_roots_finite) qed (use assms in auto) lemma poly_roots_factorization: fixes p c A assumes [simp]: "c \ 0" defines "p \ Polynomial.smult c (prod_mset (image_mset (\x. [:-x, 1:]) A))" shows "poly_roots p = A" proof - have "poly_roots p = poly_roots (\x\#A. [:-x, 1:])" by (auto simp: p_def) also have "\ = A" by (subst poly_roots_prod_mset) (auto simp: image_mset.compositionality o_def) finally show ?thesis . qed lemma fundamental_theorem_algebra_factorized': fixes p :: "complex poly" shows "p = Polynomial.smult (Polynomial.lead_coeff p) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots p)))" proof (cases "p = 0") case [simp]: False obtain xs where xs: "Polynomial.smult (Polynomial.lead_coeff p) (\x\xs. [:-x, 1:]) = p" "length xs = Polynomial.degree p" using fundamental_theorem_algebra_factorized[of p] by auto define A where "A = mset xs" note xs(1) also have "(\x\xs. [:-x, 1:]) = prod_mset (image_mset (\x. [:-x, 1:]) A)" unfolding A_def by (induction xs) auto finally have *: "Polynomial.smult (Polynomial.lead_coeff p) (\x\#A. [:- x, 1:]) = p" . also have "A = poly_roots p" using poly_roots_factorization[of "Polynomial.lead_coeff p" A] by (subst * [symmetric]) auto finally show ?thesis .. qed auto lemma poly_roots_eq_imp_eq: fixes p q :: "complex poly" assumes "Polynomial.lead_coeff p = Polynomial.lead_coeff q" assumes "poly_roots p = poly_roots q" shows "p = q" proof (cases "p = 0 \ q = 0") case False hence [simp]: "p \ 0" "q \ 0" by auto have "p = Polynomial.smult (Polynomial.lead_coeff p) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots p)))" by (rule fundamental_theorem_algebra_factorized') also have "\ = Polynomial.smult (Polynomial.lead_coeff q) (prod_mset (image_mset (\x. [:-x, 1:]) (poly_roots q)))" by (simp add: assms) also have "\ = q" by (rule fundamental_theorem_algebra_factorized' [symmetric]) finally show ?thesis . qed (use assms in auto) lemma Sum_any_zeroI': "(\x. P x \ f x = 0) \ Sum_any (\x. f x when P x) = 0" by (auto simp: Sum_any.expand_set) (* TODO: This was not really needed here, but it is important nonetheless. It should go in the Symmetric_Polynomials entry. *) lemma sym_mpoly_insert: assumes "finite X" "x \ X" shows "(sym_mpoly (insert x X) (Suc k) :: 'a :: semiring_1 mpoly) = monom (monom_of_set {x}) 1 * sym_mpoly X k + sym_mpoly X (Suc k)" (is "?lhs = ?A + ?B") proof (rule mpoly_eqI) fix mon show "coeff ?lhs mon = coeff (?A + ?B) mon" proof (cases "\i. lookup mon i \ 1 \ (i \ insert x X \ lookup mon i = 0)") case False then obtain i where i: "lookup mon i > 1 \ i \ insert x X \ lookup mon i > 0" by (auto simp: not_le) have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1)) (coeff (sym_mpoly X k)) mon" by (simp add: coeff_mpoly_times) also have "\ = (\l. \q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q when mon = l + q)" unfolding prod_fun_def by (intro Sum_any.cong, subst Sum_any_right_distrib, force) (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong) also have "\ = 0" proof (rule Sum_any_zeroI, rule Sum_any_zeroI') fix ma mb assume *: "mon = ma + mb" show "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0" proof (cases "i = x") case [simp]: True show ?thesis proof (cases "lookup mb i > 0") case True hence "coeff (sym_mpoly X k) mb = 0" using \x \ X\ by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits) thus ?thesis using mult_not_zero by blast next case False hence "coeff (monom (monom_of_set {x}) 1) ma = 0" using i by (auto simp: coeff_monom when_def * lookup_add) thus ?thesis using mult_not_zero by blast qed next case [simp]: False show ?thesis proof (cases "lookup ma i > 0") case False hence "lookup mb i = lookup mon i" using * by (auto simp: lookup_add) hence "coeff (sym_mpoly X k) mb = 0" using i by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits) thus ?thesis using mult_not_zero by blast next case True hence "coeff (monom (monom_of_set {x}) 1) ma = 0" using i by (auto simp: coeff_monom when_def * lookup_add) thus ?thesis using mult_not_zero by blast qed qed qed finally have "coeff ?A mon = 0" . moreover from False have "coeff ?lhs mon = 0" by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits) moreover from False have "coeff (sym_mpoly X (Suc k)) mon = 0" by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits) ultimately show ?thesis by auto next case True define A where "A = keys mon" have A: "A \ insert x X" using True by (auto simp: A_def) have [simp]: "mon = monom_of_set A" unfolding A_def using True by transfer (force simp: fun_eq_iff le_Suc_eq) have "finite A" using finite_subset A assms by blast show ?thesis proof (cases "x \ A") case False have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1)) (coeff (sym_mpoly X k)) (monom_of_set A)" by (simp add: coeff_mpoly_times) also have "\ = (\l. \q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q when monom_of_set A = l + q)" unfolding prod_fun_def by (intro Sum_any.cong, subst Sum_any_right_distrib, force) (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong) also have "\ = 0" proof (rule Sum_any_zeroI, rule Sum_any_zeroI') fix ma mb assume *: "monom_of_set A = ma + mb" hence "keys ma \ A" using \finite A\ by transfer (auto simp: fun_eq_iff split: if_splits) thus "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0" using \x \ A\ by (auto simp: coeff_monom when_def) qed finally show ?thesis using False A assms finite_subset[of _ "insert x X"] finite_subset[of _ X] by (auto simp: coeff_sym_mpoly) next case True have "mon = monom_of_set {x} + monom_of_set (A - {x})" using \x \ A\ \finite A\ by (auto simp: monom_of_set_plus_monom_of_set) also have "coeff ?A \ = coeff (sym_mpoly X k) (monom_of_set (A - {x}))" by (subst coeff_monom_mult) auto also have "\ = (if card A = Suc k then 1 else 0)" proof (cases "card A = Suc k") case True thus ?thesis using assms \finite A\ \x \ A\ A by (subst coeff_sym_mpoly_monom_of_set) auto next case False thus ?thesis using assms \x \ A\ A \finite A\ card_Suc_Diff1[of A x] by (subst coeff_sym_mpoly_monom_of_set_eq_0) auto qed moreover have "coeff ?B (monom_of_set A) = 0" using assms \x \ A\ \finite A\ by (subst coeff_sym_mpoly_monom_of_set_eq_0') auto moreover have "coeff ?lhs (monom_of_set A) = (if card A = Suc k then 1 else 0)" using assms A \finite A\ finite_subset[of _ "insert x X"] by (auto simp: coeff_sym_mpoly) ultimately show ?thesis by simp qed qed qed end \ No newline at end of file