This instance will be upgraded to Heptapod 0.23.2 on 2021-08-05 at 11:00 UTC+2 (a few minutes of down time)

Commit 248e2b3e authored by haftmann's avatar haftmann
Browse files

get rid of traditional predicate

parent ec187af6fd41
......@@ -37,7 +37,7 @@ using assms by (auto simp add: sum.remove[where x=k])
subsection \<open>Additions to Multiset Theory\<close>
lemma set_mset_Abs_multiset:
assumes "f \<in> 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
......
......@@ -211,11 +211,11 @@ proof (rule bij_betw_byWitness[where f'="Abs_multiset"])
show "\<forall>N\<in>{N. number_partition n N \<and> size N = k}. Abs_multiset (count N) = N"
using count_inverse by blast
show "\<forall>p\<in>{p. p partitions n \<and> 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 \<and> size N = k} \<subseteq> {p. p partitions n \<and> sum p {..n} = k}"
by (auto simp add: count_partitions_iff size_nat_multiset_eq)
show "Abs_multiset ` {p. p partitions n \<and> sum p {..n} = k} \<subseteq> {N. number_partition n N \<and> 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:
......@@ -224,11 +224,11 @@ proof (rule bij_betw_byWitness[where f'="Abs_multiset"])
show "\<forall>N\<in>{N. number_partition n N \<and> size N \<le> k}. Abs_multiset (count N) = N"
using count_inverse by blast
show "\<forall>p\<in>{p. p partitions n \<and> sum p {..n} \<le> 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 \<and> size N \<le> k} \<subseteq> {p. p partitions n \<and> sum p {..n} \<le> k}"
by (auto simp add: count_partitions_iff size_nat_multiset_eq)
show "Abs_multiset ` {p. p partitions n \<and> sum p {..n} \<le> k} \<subseteq> {N. number_partition n N\<and> size N \<le> 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:
......
......@@ -43,11 +43,6 @@ proof -
using rev_finite_subset by blast
qed
lemma partitions_imp_multiset:
assumes "p partitions n"
shows "p \<in> multiset"
using assms partitions_imp_finite_elements multiset_def by auto
lemma partitions_bounds:
assumes "p partitions n"
shows "p i \<le> n"
......@@ -299,7 +294,8 @@ proof -
also have "... = (\<Sum>i\<in>Suc ` {..m}. p i * (i - 1))"
by (auto simp add: sum.reindex)
also have "... = (\<Sum>i\<le>Suc m. p i * (i - 1))"
using \<open>p 0 = 0\<close> by (simp add: atMost_Suc_eq_insert_0 zero_notin_Suc_image)
using \<open>p 0 = 0\<close>
by (simp add: atMost_Suc_eq_insert_0)
also have "... = (\<Sum>i\<le>m. p i * (i - 1))"
using p by (auto elim!: partitionsE)
also have "... = (\<Sum>i\<le>m. p i * i - p i)"
......@@ -448,16 +444,15 @@ proof
from this have bounds: "(\<forall>i. p i \<noteq> 0 \<longrightarrow> 1 \<le> i \<and> i \<le> n)"
and sum: "(\<Sum>i\<le>n. p i * i) = n"
unfolding partitions_def by auto
from \<open>p partitions n\<close> have "p \<in> multiset" by (rule partitions_imp_multiset)
from \<open>p partitions n\<close> have "finite {x. 0 < p x}"
by (rule partitions_imp_finite_elements)
moreover from \<open>p \<in> multiset\<close> bounds have "\<not> 0 \<in># Abs_multiset p"
moreover from \<open>finite {x. 0 < p x}\<close> bounds have "\<not> 0 \<in># Abs_multiset p"
using count_eq_zero_iff by force
moreover from \<open>p \<in> multiset\<close> this sum have "sum_mset (Abs_multiset p) = n"
moreover from \<open>finite {x. 0 < p x}\<close> this sum have "sum_mset (Abs_multiset p) = n"
proof -
have "(\<Sum>i\<in>{x. 0 < p x}. p i * i) = (\<Sum>i\<le>n. p i * i)"
using bounds by (auto intro: sum.mono_neutral_cong_left)
from \<open>p \<in> multiset\<close> this sum show "sum_mset (Abs_multiset p) = n"
from \<open>finite {x. 0 < p x}\<close> 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} \<and> number_partition n (Abs_multiset p)"
......@@ -466,15 +461,14 @@ next
assume "finite {x. 0 < p x} \<and> number_partition n (Abs_multiset p)"
from this have "finite {x. 0 < p x}" "0 \<notin># Abs_multiset p" "sum_mset (Abs_multiset p) = n"
unfolding number_partition_def by auto
from \<open>finite {x. 0 < p x}\<close> have "p \<in> multiset" by (simp add: multiset_def)
from \<open>p \<in> multiset\<close> have "(\<Sum>i\<in>{x. 0 < p x}. p i * i) = n"
from \<open>finite {x. 0 < p x}\<close> have "(\<Sum>i\<in>{x. 0 < p x}. p i * i) = n"
using \<open> sum_mset (Abs_multiset p) = n\<close>
by (simp add: sum_mset_sum_count set_mset_Abs_multiset)
have bounds: "\<And>i. p i \<noteq> 0 \<Longrightarrow> 1 \<le> i \<and> i \<le> n"
proof
fix i
assume "p i \<noteq> 0"
from \<open>\<not> 0 \<in># Abs_multiset p\<close> \<open>p \<in> multiset\<close> have "p 0 = 0"
from \<open>\<not> 0 \<in># Abs_multiset p\<close> \<open>finite {x. 0 < p x}\<close> have "p 0 = 0"
using count_inI by force
from this \<open>p i \<noteq> 0\<close> show "1 \<le> i"
by (metis One_nat_def leI less_Suc0)
......
......@@ -88,8 +88,8 @@ 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)
......
......@@ -314,11 +314,11 @@ 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 \<Rightarrow> 'a multiset" is "\<lambda>(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 \<Rightarrow> 'a multiset" is "\<lambda>(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
......
......@@ -197,9 +197,9 @@ lift_definition poly_roots_mset :: "('a :: idom) poly \<Rightarrow> 'a multiset"
"\<lambda>p x. if p = 0 then 0 else Polynomial.order x p"
proof -
fix p :: "'a poly"
show "(\<lambda>x. if p = 0 then 0 else order x p) \<in> 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 = {#}"
......
......@@ -273,8 +273,8 @@ lift_definition poly_roots :: "'a :: idom poly \<Rightarrow> 'a multiset" is
"\<lambda>p x. if p = 0 then 0 else order x p"
proof -
fix p :: "'a poly"
show "(\<lambda>x. if p = 0 then 0 else order x p) \<in> 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 = {#}"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment