146 |
146 |
147 abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" |
147 abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" |
148 where "Melem a M \<equiv> a \<in> set_mset M" |
148 where "Melem a M \<equiv> a \<in> set_mset M" |
149 |
149 |
150 notation |
150 notation |
151 Melem ("op \<in>#") and |
151 Melem ("'(\<in>#')") and |
152 Melem ("(_/ \<in># _)" [51, 51] 50) |
152 Melem ("(_/ \<in># _)" [51, 51] 50) |
153 |
153 |
154 notation (ASCII) |
154 notation (ASCII) |
155 Melem ("op :#") and |
155 Melem ("'(:#')") and |
156 Melem ("(_/ :# _)" [51, 51] 50) |
156 Melem ("(_/ :# _)" [51, 51] 50) |
157 |
157 |
158 abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" |
158 abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" |
159 where "not_Melem a M \<equiv> a \<notin> set_mset M" |
159 where "not_Melem a M \<equiv> a \<notin> set_mset M" |
160 |
160 |
161 notation |
161 notation |
162 not_Melem ("op \<notin>#") and |
162 not_Melem ("'(\<notin>#')") and |
163 not_Melem ("(_/ \<notin># _)" [51, 51] 50) |
163 not_Melem ("(_/ \<notin># _)" [51, 51] 50) |
164 |
164 |
165 notation (ASCII) |
165 notation (ASCII) |
166 not_Melem ("op ~:#") and |
166 not_Melem ("'(~:#')") and |
167 not_Melem ("(_/ ~:# _)" [51, 51] 50) |
167 not_Melem ("(_/ ~:# _)" [51, 51] 50) |
168 |
168 |
169 context |
169 context |
170 begin |
170 begin |
171 |
171 |
531 subseteq_mset (infix "<=#" 50) and |
531 subseteq_mset (infix "<=#" 50) and |
532 subset_mset (infix "<#" 50) and |
532 subset_mset (infix "<#" 50) and |
533 supseteq_mset (infix ">=#" 50) and |
533 supseteq_mset (infix ">=#" 50) and |
534 supset_mset (infix ">#" 50) |
534 supset_mset (infix ">#" 50) |
535 |
535 |
536 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#" |
536 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\<subseteq>#)" "(\<subset>#)" |
537 by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) |
537 by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) |
538 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
538 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
539 |
539 |
540 interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#" |
540 interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\<subseteq>#)" "(\<subset>#)" |
541 by standard |
541 by standard |
542 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
542 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
543 |
543 |
544 lemma mset_subset_eqI: |
544 lemma mset_subset_eqI: |
545 "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B" |
545 "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B" |
554 apply (rule iffI) |
554 apply (rule iffI) |
555 apply (rule exI [where x = "B - A"]) |
555 apply (rule exI [where x = "B - A"]) |
556 apply (auto intro: multiset_eq_iff [THEN iffD2]) |
556 apply (auto intro: multiset_eq_iff [THEN iffD2]) |
557 done |
557 done |
558 |
558 |
559 interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -" |
559 interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)" |
560 by standard (simp, fact mset_subset_eq_exists_conv) |
560 by standard (simp, fact mset_subset_eq_exists_conv) |
561 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
561 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
562 |
562 |
563 declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp] |
563 declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp] |
564 |
564 |
688 subsubsection \<open>Intersection and bounded union\<close> |
688 subsubsection \<open>Intersection and bounded union\<close> |
689 |
689 |
690 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where |
690 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where |
691 multiset_inter_def: "inf_subset_mset A B = A - (A - B)" |
691 multiset_inter_def: "inf_subset_mset A B = A - (A - B)" |
692 |
692 |
693 interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#" |
693 interpretation subset_mset: semilattice_inf inf_subset_mset "(\<subseteq>#)" "(\<subset>#)" |
694 proof - |
694 proof - |
695 have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat |
695 have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat |
696 by arith |
696 by arith |
697 show "class.semilattice_inf op \<inter># op \<subseteq># op \<subset>#" |
697 show "class.semilattice_inf (\<inter>#) (\<subseteq>#) (\<subset>#)" |
698 by standard (auto simp add: multiset_inter_def subseteq_mset_def) |
698 by standard (auto simp add: multiset_inter_def subseteq_mset_def) |
699 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
699 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
700 |
700 |
701 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70) |
701 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70) |
702 where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close> |
702 where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close> |
703 |
703 |
704 interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#" |
704 interpretation subset_mset: semilattice_sup sup_subset_mset "(\<subseteq>#)" "(\<subset>#)" |
705 proof - |
705 proof - |
706 have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat |
706 have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat |
707 by arith |
707 by arith |
708 show "class.semilattice_sup op \<union># op \<subseteq># op \<subset>#" |
708 show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)" |
709 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
709 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
710 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
710 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
711 |
711 |
712 interpretation subset_mset: bounded_lattice_bot "op \<inter>#" "op \<subseteq>#" "op \<subset>#" |
712 interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" |
713 "op \<union>#" "{#}" |
713 "(\<union>#)" "{#}" |
714 by standard auto |
714 by standard auto |
715 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
715 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
716 |
716 |
717 |
717 |
718 subsubsection \<open>Additional intersection facts\<close> |
718 subsubsection \<open>Additional intersection facts\<close> |
1118 assumes "A \<noteq> {}" "subset_mset.bdd_above A" |
1118 assumes "A \<noteq> {}" "subset_mset.bdd_above A" |
1119 shows "count (Sup A) x = (SUP X:A. count X x)" |
1119 shows "count (Sup A) x = (SUP X:A. count X x)" |
1120 using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset) |
1120 using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset) |
1121 |
1121 |
1122 |
1122 |
1123 interpretation subset_mset: conditionally_complete_lattice Inf Sup "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#" |
1123 interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)" |
1124 proof |
1124 proof |
1125 fix X :: "'a multiset" and A |
1125 fix X :: "'a multiset" and A |
1126 assume "X \<in> A" |
1126 assume "X \<in> A" |
1127 show "Inf A \<subseteq># X" |
1127 show "Inf A \<subseteq># X" |
1128 proof (rule mset_subset_eqI) |
1128 proof (rule mset_subset_eqI) |
1242 have "subset_mset.bdd_above A" |
1242 have "subset_mset.bdd_above A" |
1243 by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded) |
1243 by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded) |
1244 with assms show ?thesis by (simp add: in_Sup_multiset_iff) |
1244 with assms show ?thesis by (simp add: in_Sup_multiset_iff) |
1245 qed |
1245 qed |
1246 |
1246 |
1247 interpretation subset_mset: distrib_lattice "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#" |
1247 interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)" |
1248 proof |
1248 proof |
1249 fix A B C :: "'a multiset" |
1249 fix A B C :: "'a multiset" |
1250 show "A \<union># (B \<inter># C) = A \<union># B \<inter># (A \<union># C)" |
1250 show "A \<union># (B \<inter># C) = A \<union># B \<inter># (A \<union># C)" |
1251 by (intro multiset_eqI) simp_all |
1251 by (intro multiset_eqI) simp_all |
1252 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
1252 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
2267 by (induction A) (auto simp: ac_simps) |
2267 by (induction A) (auto simp: ac_simps) |
2268 |
2268 |
2269 end |
2269 end |
2270 end |
2270 end |
2271 |
2271 |
2272 lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)" |
2272 lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute ((+) :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)" |
2273 by standard (simp add: add_ac comp_def) |
2273 by standard (simp add: add_ac comp_def) |
2274 |
2274 |
2275 declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp] |
2275 declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp] |
2276 |
2276 |
2277 lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)" |
2277 lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (+) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)" |
2278 by (induct NN) auto |
2278 by (induct NN) auto |
2279 |
2279 |
2280 context comm_monoid_add |
2280 context comm_monoid_add |
2281 begin |
2281 begin |
2282 |
2282 |
2624 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
2624 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
2625 with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp |
2625 with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp |
2626 have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto |
2626 have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto |
2627 then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] = |
2627 then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] = |
2628 [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp |
2628 [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp |
2629 note *** = this [of "op <"] this [of "op >"] this [of "op ="] |
2629 note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"] |
2630 show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" |
2630 show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" |
2631 proof (cases "f l" ?pivot rule: linorder_cases) |
2631 proof (cases "f l" ?pivot rule: linorder_cases) |
2632 case less |
2632 case less |
2633 then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto |
2633 then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto |
2634 with less show ?thesis |
2634 with less show ?thesis |
2996 subsection \<open>Quasi-executable version of the multiset extension\<close> |
2996 subsection \<open>Quasi-executable version of the multiset extension\<close> |
2997 |
2997 |
2998 text \<open> |
2998 text \<open> |
2999 Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are |
2999 Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are |
3000 executable whenever the given predicate \<open>P\<close> is. Together with the standard |
3000 executable whenever the given predicate \<open>P\<close> is. Together with the standard |
3001 code equations for \<open>op \<inter>#\<close> and \<open>op -\<close> this should yield quadratic |
3001 code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic |
3002 (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>. |
3002 (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>. |
3003 \<close> |
3003 \<close> |
3004 |
3004 |
3005 definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
3005 definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
3006 "multp P N M = |
3006 "multp P N M = |
3344 let |
3344 let |
3345 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) (Const _ $ t') = |
3345 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) (Const _ $ t') = |
3346 let |
3346 let |
3347 val (maybe_opt, ps) = |
3347 val (maybe_opt, ps) = |
3348 Nitpick_Model.dest_plain_fun t' |
3348 Nitpick_Model.dest_plain_fun t' |
3349 ||> op ~~ |
3349 ||> (~~) |
3350 ||> map (apsnd (snd o HOLogic.dest_number)) |
3350 ||> map (apsnd (snd o HOLogic.dest_number)) |
3351 fun elems_for t = |
3351 fun elems_for t = |
3352 (case AList.lookup (op =) ps t of |
3352 (case AList.lookup (=) ps t of |
3353 SOME n => replicate n t |
3353 SOME n => replicate n t |
3354 | NONE => [Const (maybe_name, elem_T --> elem_T) $ t]) |
3354 | NONE => [Const (maybe_name, elem_T --> elem_T) $ t]) |
3355 in |
3355 in |
3356 (case maps elems_for (all_values elem_T) @ |
3356 (case maps elems_for (all_values elem_T) @ |
3357 (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of |
3357 (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of |
3436 |
3436 |
3437 declare size_mset [code] |
3437 declare size_mset [code] |
3438 |
3438 |
3439 fun subset_eq_mset_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where |
3439 fun subset_eq_mset_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where |
3440 "subset_eq_mset_impl [] ys = Some (ys \<noteq> [])" |
3440 "subset_eq_mset_impl [] ys = Some (ys \<noteq> [])" |
3441 | "subset_eq_mset_impl (Cons x xs) ys = (case List.extract (op = x) ys of |
3441 | "subset_eq_mset_impl (Cons x xs) ys = (case List.extract ((=) x) ys of |
3442 None \<Rightarrow> None |
3442 None \<Rightarrow> None |
3443 | Some (ys1,_,ys2) \<Rightarrow> subset_eq_mset_impl xs (ys1 @ ys2))" |
3443 | Some (ys1,_,ys2) \<Rightarrow> subset_eq_mset_impl xs (ys1 @ ys2))" |
3444 |
3444 |
3445 lemma subset_eq_mset_impl: "(subset_eq_mset_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<subseteq># mset ys) \<and> |
3445 lemma subset_eq_mset_impl: "(subset_eq_mset_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<subseteq># mset ys) \<and> |
3446 (subset_eq_mset_impl xs ys = Some True \<longleftrightarrow> mset xs \<subset># mset ys) \<and> |
3446 (subset_eq_mset_impl xs ys = Some True \<longleftrightarrow> mset xs \<subset># mset ys) \<and> |
3449 case (Nil ys) |
3449 case (Nil ys) |
3450 show ?case by (auto simp: subset_mset.zero_less_iff_neq_zero) |
3450 show ?case by (auto simp: subset_mset.zero_less_iff_neq_zero) |
3451 next |
3451 next |
3452 case (Cons x xs ys) |
3452 case (Cons x xs ys) |
3453 show ?case |
3453 show ?case |
3454 proof (cases "List.extract (op = x) ys") |
3454 proof (cases "List.extract ((=) x) ys") |
3455 case None |
3455 case None |
3456 hence x: "x \<notin> set ys" by (simp add: extract_None_iff) |
3456 hence x: "x \<notin> set ys" by (simp add: extract_None_iff) |
3457 { |
3457 { |
3458 assume "mset (x # xs) \<subseteq># mset ys" |
3458 assume "mset (x # xs) \<subseteq># mset ys" |
3459 from set_mset_mono[OF this] x have False by simp |
3459 from set_mset_mono[OF this] x have False by simp |
3508 by (induct xs) (simp_all add: ac_simps) |
3508 by (induct xs) (simp_all add: ac_simps) |
3509 then show ?thesis by simp |
3509 then show ?thesis by simp |
3510 qed |
3510 qed |
3511 |
3511 |
3512 text \<open> |
3512 text \<open> |
3513 Exercise for the casual reader: add implementations for @{term "op \<le>"} |
3513 Exercise for the casual reader: add implementations for @{term "(\<le>)"} |
3514 and @{term "op <"} (multiset order). |
3514 and @{term "(<)"} (multiset order). |
3515 \<close> |
3515 \<close> |
3516 |
3516 |
3517 text \<open>Quickcheck generators\<close> |
3517 text \<open>Quickcheck generators\<close> |
3518 |
3518 |
3519 definition (in term_syntax) |
3519 definition (in term_syntax) |
3666 by (rule image_mset.id) |
3666 by (rule image_mset.id) |
3667 show "image_mset (g \<circ> f) = image_mset g \<circ> image_mset f" for f g |
3667 show "image_mset (g \<circ> f) = image_mset g \<circ> image_mset f" for f g |
3668 unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality) |
3668 unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality) |
3669 show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X |
3669 show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X |
3670 by (induct X) simp_all |
3670 by (induct X) simp_all |
3671 show "set_mset \<circ> image_mset f = op ` f \<circ> set_mset" for f |
3671 show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f |
3672 by auto |
3672 by auto |
3673 show "card_order natLeq" |
3673 show "card_order natLeq" |
3674 by (rule natLeq_card_order) |
3674 by (rule natLeq_card_order) |
3675 show "BNF_Cardinal_Arithmetic.cinfinite natLeq" |
3675 show "BNF_Cardinal_Arithmetic.cinfinite natLeq" |
3676 by (rule natLeq_cinfinite) |
3676 by (rule natLeq_cinfinite) |