wenzelm@10249: (* Title: HOL/Library/Multiset.thy wenzelm@10249: ID: $Id$ paulson@15072: Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker wenzelm@10249: *) wenzelm@10249: wenzelm@14706: header {* Multisets *} wenzelm@10249: nipkow@15131: theory Multiset krauss@19564: imports Main nipkow@15131: begin wenzelm@10249: wenzelm@10249: subsection {* The type of multisets *} wenzelm@10249: nipkow@25162: typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}" wenzelm@10249: proof nipkow@11464: show "(\x. 0::nat) \ ?multiset" by simp wenzelm@10249: qed wenzelm@10249: wenzelm@10249: lemmas multiset_typedef [simp] = wenzelm@10277: Abs_multiset_inverse Rep_multiset_inverse Rep_multiset wenzelm@10277: and [simp] = Rep_multiset_inject [symmetric] wenzelm@10249: wenzelm@19086: definition wenzelm@21404: Mempty :: "'a multiset" ("{#}") where wenzelm@19086: "{#} = Abs_multiset (\a. 0)" wenzelm@10249: wenzelm@21404: definition nipkow@25507: single :: "'a => 'a multiset" where nipkow@25507: "single a = Abs_multiset (\b. if b = a then 1 else 0)" wenzelm@10249: wenzelm@21404: definition wenzelm@21404: count :: "'a multiset => 'a => nat" where wenzelm@19086: "count = Rep_multiset" wenzelm@10249: wenzelm@21404: definition wenzelm@21404: MCollect :: "'a multiset => ('a => bool) => 'a multiset" where wenzelm@19086: "MCollect M P = Abs_multiset (\x. if P x then Rep_multiset M x else 0)" wenzelm@19086: wenzelm@19363: abbreviation wenzelm@21404: Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where nipkow@25162: "a :# M == count M a > 0" wenzelm@10249: wenzelm@10249: syntax wenzelm@10249: "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") wenzelm@10249: translations wenzelm@20770: "{#x:M. P#}" == "CONST MCollect M (\x. P)" wenzelm@10249: wenzelm@19086: definition wenzelm@21404: set_of :: "'a multiset => 'a set" where wenzelm@19086: "set_of M = {x. x :# M}" wenzelm@10249: haftmann@21417: instance multiset :: (type) "{plus, minus, zero, size}" nipkow@11464: union_def: "M + N == Abs_multiset (\a. Rep_multiset M a + Rep_multiset N a)" nipkow@11464: diff_def: "M - N == Abs_multiset (\a. Rep_multiset M a - Rep_multiset N a)" wenzelm@11701: Zero_multiset_def [simp]: "0 == {#}" haftmann@21417: size_def: "size M == setsum (count M) (set_of M)" .. wenzelm@10249: wenzelm@19086: definition wenzelm@21404: multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where wenzelm@19086: "multiset_inter A B = A - (A - B)" kleing@15869: nipkow@25507: syntax -- "Multiset Enumeration" nipkow@25507: "@multiset" :: "args => 'a multiset" ("{#(_)#}") nipkow@25507: nipkow@25507: translations nipkow@25507: "{#x, xs#}" == "{#x#} + {#xs#}" nipkow@25507: "{#x#}" == "CONST single x" nipkow@25507: wenzelm@10249: wenzelm@10249: text {* wenzelm@10249: \medskip Preservation of the representing set @{term multiset}. wenzelm@10249: *} wenzelm@10249: nipkow@11464: lemma const0_in_multiset [simp]: "(\a. 0) \ multiset" wenzelm@17161: by (simp add: multiset_def) wenzelm@10249: wenzelm@11701: lemma only1_in_multiset [simp]: "(\b. if b = a then 1 else 0) \ multiset" wenzelm@17161: by (simp add: multiset_def) wenzelm@10249: wenzelm@10249: lemma union_preserves_multiset [simp]: nipkow@11464: "M \ multiset ==> N \ multiset ==> (\a. M a + N a) \ multiset" wenzelm@17161: apply (simp add: multiset_def) wenzelm@17161: apply (drule (1) finite_UnI) wenzelm@10249: apply (simp del: finite_Un add: Un_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma diff_preserves_multiset [simp]: nipkow@11464: "M \ multiset ==> (\a. M a - N a) \ multiset" wenzelm@17161: apply (simp add: multiset_def) wenzelm@10249: apply (rule finite_subset) wenzelm@17161: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsection {* Algebraic properties of multisets *} wenzelm@10249: wenzelm@10249: subsubsection {* Union *} wenzelm@10249: wenzelm@17161: lemma union_empty [simp]: "M + {#} = M \ {#} + M = M" wenzelm@17161: by (simp add: union_def Mempty_def) wenzelm@10249: wenzelm@17161: lemma union_commute: "M + N = N + (M::'a multiset)" wenzelm@17161: by (simp add: union_def add_ac) wenzelm@17161: wenzelm@17161: lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))" wenzelm@17161: by (simp add: union_def add_ac) wenzelm@10249: wenzelm@17161: lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))" wenzelm@17161: proof - wenzelm@17161: have "M + (N + K) = (N + K) + M" wenzelm@17161: by (rule union_commute) wenzelm@17161: also have "\ = N + (K + M)" wenzelm@17161: by (rule union_assoc) wenzelm@17161: also have "K + M = M + K" wenzelm@17161: by (rule union_commute) wenzelm@17161: finally show ?thesis . wenzelm@17161: qed wenzelm@10249: wenzelm@17161: lemmas union_ac = union_assoc union_commute union_lcomm wenzelm@10249: obua@14738: instance multiset :: (type) comm_monoid_add wenzelm@17200: proof obua@14722: fix a b c :: "'a multiset" obua@14722: show "(a + b) + c = a + (b + c)" by (rule union_assoc) obua@14722: show "a + b = b + a" by (rule union_commute) obua@14722: show "0 + a = a" by simp obua@14722: qed wenzelm@10277: wenzelm@10249: wenzelm@10249: subsubsection {* Difference *} wenzelm@10249: wenzelm@17161: lemma diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" wenzelm@17161: by (simp add: Mempty_def diff_def) wenzelm@10249: wenzelm@17161: lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M" wenzelm@17161: by (simp add: union_def diff_def) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Count of elements *} wenzelm@10249: wenzelm@17161: lemma count_empty [simp]: "count {#} a = 0" wenzelm@17161: by (simp add: count_def Mempty_def) wenzelm@10249: wenzelm@17161: lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" wenzelm@17161: by (simp add: count_def single_def) wenzelm@10249: wenzelm@17161: lemma count_union [simp]: "count (M + N) a = count M a + count N a" wenzelm@17161: by (simp add: count_def union_def) wenzelm@10249: wenzelm@17161: lemma count_diff [simp]: "count (M - N) a = count M a - count N a" wenzelm@17161: by (simp add: count_def diff_def) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Set of elements *} wenzelm@10249: wenzelm@17161: lemma set_of_empty [simp]: "set_of {#} = {}" wenzelm@17161: by (simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_single [simp]: "set_of {#b#} = {b}" wenzelm@17161: by (simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_union [simp]: "set_of (M + N) = set_of M \ set_of N" wenzelm@17161: by (auto simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" wenzelm@17161: by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" wenzelm@17161: by (auto simp add: set_of_def) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Size *} wenzelm@10249: wenzelm@17161: lemma size_empty [simp]: "size {#} = 0" wenzelm@17161: by (simp add: size_def) wenzelm@10249: wenzelm@17161: lemma size_single [simp]: "size {#b#} = 1" wenzelm@17161: by (simp add: size_def) wenzelm@10249: wenzelm@17161: lemma finite_set_of [iff]: "finite (set_of M)" wenzelm@17161: using Rep_multiset [of M] wenzelm@17161: by (simp add: multiset_def set_of_def count_def) wenzelm@10249: wenzelm@17161: lemma setsum_count_Int: nipkow@11464: "finite A ==> setsum (count N) (A \ set_of N) = setsum (count N) A" wenzelm@18258: apply (induct rule: finite_induct) wenzelm@17161: apply simp wenzelm@10249: apply (simp add: Int_insert_left set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" wenzelm@10249: apply (unfold size_def) nipkow@11464: apply (subgoal_tac "count (M + N) = (\a. count M a + count N a)") wenzelm@10249: prefer 2 paulson@15072: apply (rule ext, simp) nipkow@15402: apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int) wenzelm@10249: apply (subst Int_commute) wenzelm@10249: apply (simp (no_asm_simp) add: setsum_count_Int) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" paulson@15072: apply (unfold size_def Mempty_def count_def, auto) wenzelm@10249: apply (simp add: set_of_def count_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \a. a :# M" wenzelm@10249: apply (unfold size_def) paulson@15072: apply (drule setsum_SucD, auto) wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Equality of multisets *} wenzelm@10249: wenzelm@17161: lemma multiset_eq_conv_count_eq: "(M = N) = (\a. count M a = count N a)" wenzelm@17161: by (simp add: count_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" wenzelm@17161: by (simp add: single_def Mempty_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" wenzelm@17161: by (auto simp add: single_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \ N = {#})" wenzelm@17161: by (auto simp add: union_def Mempty_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \ N = {#})" wenzelm@17161: by (auto simp add: union_def Mempty_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" wenzelm@17161: by (simp add: union_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" wenzelm@17161: by (simp add: union_def expand_fun_eq) wenzelm@10249: wenzelm@17161: lemma union_is_single: nipkow@11464: "(M + N = {#a#}) = (M = {#a#} \ N={#} \ M = {#} \ N = {#a#})" paulson@15072: apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq) wenzelm@10249: apply blast wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma single_is_union: paulson@15072: "({#a#} = M + N) = ({#a#} = M \ N = {#} \ M = {#} \ {#a#} = N)" wenzelm@10249: apply (unfold Mempty_def single_def union_def) nipkow@11464: apply (simp add: add_is_1 one_is_add expand_fun_eq) wenzelm@10249: apply (blast dest: sym) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma add_eq_conv_diff: wenzelm@10249: "(M + {#a#} = N + {#b#}) = paulson@15072: (M = N \ a = b \ M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#})" wenzelm@24035: using [[simproc del: neq]] wenzelm@10249: apply (unfold single_def union_def diff_def) wenzelm@10249: apply (simp (no_asm) add: expand_fun_eq) paulson@15072: apply (rule conjI, force, safe, simp_all) berghofe@13601: apply (simp add: eq_sym_conv) wenzelm@10249: done wenzelm@10249: kleing@15869: declare Rep_multiset_inject [symmetric, simp del] kleing@15869: nipkow@23611: instance multiset :: (type) cancel_ab_semigroup_add nipkow@23611: proof nipkow@23611: fix a b c :: "'a multiset" nipkow@23611: show "a + b = a + c \ b = c" by simp nipkow@23611: qed kleing@15869: kleing@15869: subsubsection {* Intersection *} kleing@15869: kleing@15869: lemma multiset_inter_count: wenzelm@17161: "count (A #\ B) x = min (count A x) (count B x)" wenzelm@17161: by (simp add: multiset_inter_def min_def) kleing@15869: kleing@15869: lemma multiset_inter_commute: "A #\ B = B #\ A" wenzelm@17200: by (simp add: multiset_eq_conv_count_eq multiset_inter_count haftmann@21214: min_max.inf_commute) kleing@15869: kleing@15869: lemma multiset_inter_assoc: "A #\ (B #\ C) = A #\ B #\ C" wenzelm@17200: by (simp add: multiset_eq_conv_count_eq multiset_inter_count haftmann@21214: min_max.inf_assoc) kleing@15869: kleing@15869: lemma multiset_inter_left_commute: "A #\ (B #\ C) = B #\ (A #\ C)" kleing@15869: by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def) kleing@15869: wenzelm@17161: lemmas multiset_inter_ac = wenzelm@17161: multiset_inter_commute wenzelm@17161: multiset_inter_assoc wenzelm@17161: multiset_inter_left_commute kleing@15869: kleing@15869: lemma multiset_union_diff_commute: "B #\ C = {#} \ A + B - C = A - C + B" wenzelm@17200: apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def wenzelm@17161: split: split_if_asm) kleing@15869: apply clarsimp wenzelm@17161: apply (erule_tac x = a in allE) kleing@15869: apply auto kleing@15869: done kleing@15869: wenzelm@10249: wenzelm@10249: subsection {* Induction over multisets *} wenzelm@10249: wenzelm@10249: lemma setsum_decr: wenzelm@11701: "finite F ==> (0::nat) < f a ==> paulson@15072: setsum (f (a := f a - 1)) F = (if a\F then setsum f F - 1 else setsum f F)" wenzelm@18258: apply (induct rule: finite_induct) wenzelm@18258: apply auto paulson@15072: apply (drule_tac a = a in mk_disjoint_insert, auto) wenzelm@10249: done wenzelm@10249: wenzelm@10313: lemma rep_multiset_induct_aux: wenzelm@18730: assumes 1: "P (\a. (0::nat))" wenzelm@18730: and 2: "!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))" nipkow@25134: shows "\f. f \ multiset --> setsum f {x. f x \ 0} = n --> P f" wenzelm@18730: apply (unfold multiset_def) wenzelm@18730: apply (induct_tac n, simp, clarify) wenzelm@18730: apply (subgoal_tac "f = (\a.0)") wenzelm@18730: apply simp wenzelm@18730: apply (rule 1) wenzelm@18730: apply (rule ext, force, clarify) wenzelm@18730: apply (frule setsum_SucD, clarify) wenzelm@18730: apply (rename_tac a) nipkow@25162: apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}") wenzelm@18730: prefer 2 wenzelm@18730: apply (rule finite_subset) wenzelm@18730: prefer 2 wenzelm@18730: apply assumption wenzelm@18730: apply simp wenzelm@18730: apply blast wenzelm@18730: apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)") wenzelm@18730: prefer 2 wenzelm@18730: apply (rule ext) wenzelm@18730: apply (simp (no_asm_simp)) wenzelm@18730: apply (erule ssubst, rule 2 [unfolded multiset_def], blast) wenzelm@18730: apply (erule allE, erule impE, erule_tac [2] mp, blast) wenzelm@18730: apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def) nipkow@25134: apply (subgoal_tac "{x. x \ a --> f x \ 0} = {x. f x \ 0}") wenzelm@18730: prefer 2 wenzelm@18730: apply blast nipkow@25134: apply (subgoal_tac "{x. x \ a \ f x \ 0} = {x. f x \ 0} - {a}") wenzelm@18730: prefer 2 wenzelm@18730: apply blast wenzelm@18730: apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong) wenzelm@18730: done wenzelm@10249: wenzelm@10313: theorem rep_multiset_induct: nipkow@11464: "f \ multiset ==> P (\a. 0) ==> wenzelm@11701: (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" wenzelm@17161: using rep_multiset_induct_aux by blast wenzelm@10249: wenzelm@18258: theorem multiset_induct [case_names empty add, induct type: multiset]: wenzelm@18258: assumes empty: "P {#}" wenzelm@18258: and add: "!!M x. P M ==> P (M + {#x#})" wenzelm@17161: shows "P M" wenzelm@10249: proof - wenzelm@10249: note defns = union_def single_def Mempty_def wenzelm@10249: show ?thesis wenzelm@10249: apply (rule Rep_multiset_inverse [THEN subst]) wenzelm@10313: apply (rule Rep_multiset [THEN rep_multiset_induct]) wenzelm@18258: apply (rule empty [unfolded defns]) paulson@15072: apply (subgoal_tac "f(b := f b + 1) = (\a. f a + (if a=b then 1 else 0))") wenzelm@10249: prefer 2 wenzelm@10249: apply (simp add: expand_fun_eq) wenzelm@10249: apply (erule ssubst) wenzelm@17200: apply (erule Abs_multiset_inverse [THEN subst]) wenzelm@18258: apply (erule add [unfolded defns, simplified]) wenzelm@10249: done wenzelm@10249: qed wenzelm@10249: wenzelm@10249: lemma MCollect_preserves_multiset: nipkow@11464: "M \ multiset ==> (\x. if P x then M x else 0) \ multiset" wenzelm@10249: apply (simp add: multiset_def) paulson@15072: apply (rule finite_subset, auto) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma count_MCollect [simp]: wenzelm@10249: "count {# x:M. P x #} a = (if P a then count M a else 0)" paulson@15072: by (simp add: count_def MCollect_def MCollect_preserves_multiset) wenzelm@10249: wenzelm@17161: lemma set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \ {x. P x}" wenzelm@17161: by (auto simp add: set_of_def) wenzelm@10249: wenzelm@17161: lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \ P x #}" wenzelm@17161: by (subst multiset_eq_conv_count_eq, auto) wenzelm@10249: wenzelm@17161: lemma add_eq_conv_ex: wenzelm@17161: "(M + {#a#} = N + {#b#}) = wenzelm@17161: (M = N \ a = b \ (\K. M = K + {#b#} \ N = K + {#a#}))" paulson@15072: by (auto simp add: add_eq_conv_diff) wenzelm@10249: kleing@15869: declare multiset_typedef [simp del] wenzelm@10249: wenzelm@17161: wenzelm@10249: subsection {* Multiset orderings *} wenzelm@10249: wenzelm@10249: subsubsection {* Well-foundedness *} wenzelm@10249: wenzelm@19086: definition berghofe@23751: mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where wenzelm@19086: "mult1 r = berghofe@23751: {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ berghofe@23751: (\b. b :# K --> (b, a) \ r)}" wenzelm@10249: wenzelm@21404: definition berghofe@23751: mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where berghofe@23751: "mult r = (mult1 r)\<^sup>+" wenzelm@10249: berghofe@23751: lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" wenzelm@10277: by (simp add: mult1_def) wenzelm@10249: berghofe@23751: lemma less_add: "(N, M0 + {#a#}) \ mult1 r ==> berghofe@23751: (\M. (M, M0) \ mult1 r \ N = M + {#a#}) \ berghofe@23751: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K)" wenzelm@19582: (is "_ \ ?case1 (mult1 r) \ ?case2") wenzelm@10249: proof (unfold mult1_def) berghofe@23751: let ?r = "\K a. \b. b :# K --> (b, a) \ r" nipkow@11464: let ?R = "\N M. \a M0 K. M = M0 + {#a#} \ N = M0 + K \ ?r K a" berghofe@23751: let ?case1 = "?case1 {(N, M). ?R N M}" wenzelm@10249: berghofe@23751: assume "(N, M0 + {#a#}) \ {(N, M). ?R N M}" wenzelm@18258: then have "\a' M0' K. nipkow@11464: M0 + {#a#} = M0' + {#a'#} \ N = M0' + K \ ?r K a'" by simp wenzelm@18258: then show "?case1 \ ?case2" wenzelm@10249: proof (elim exE conjE) wenzelm@10249: fix a' M0' K wenzelm@10249: assume N: "N = M0' + K" and r: "?r K a'" wenzelm@10249: assume "M0 + {#a#} = M0' + {#a'#}" wenzelm@18258: then have "M0 = M0' \ a = a' \ nipkow@11464: (\K'. M0 = K' + {#a'#} \ M0' = K' + {#a#})" wenzelm@10249: by (simp only: add_eq_conv_ex) wenzelm@18258: then show ?thesis wenzelm@10249: proof (elim disjE conjE exE) wenzelm@10249: assume "M0 = M0'" "a = a'" nipkow@11464: with N r have "?r K a \ N = M0 + K" by simp wenzelm@18258: then have ?case2 .. then show ?thesis .. wenzelm@10249: next wenzelm@10249: fix K' wenzelm@10249: assume "M0' = K' + {#a#}" wenzelm@10249: with N have n: "N = K' + K + {#a#}" by (simp add: union_ac) wenzelm@10249: wenzelm@10249: assume "M0 = K' + {#a'#}" wenzelm@10249: with r have "?R (K' + K) M0" by blast wenzelm@18258: with n have ?case1 by simp then show ?thesis .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: berghofe@23751: lemma all_accessible: "wf r ==> \M. M \ acc (mult1 r)" wenzelm@10249: proof wenzelm@10249: let ?R = "mult1 r" wenzelm@10249: let ?W = "acc ?R" wenzelm@10249: { wenzelm@10249: fix M M0 a berghofe@23751: assume M0: "M0 \ ?W" berghofe@23751: and wf_hyp: "!!b. (b, a) \ r ==> (\M \ ?W. M + {#b#} \ ?W)" berghofe@23751: and acc_hyp: "\M. (M, M0) \ ?R --> M + {#a#} \ ?W" berghofe@23751: have "M0 + {#a#} \ ?W" berghofe@23751: proof (rule accI [of "M0 + {#a#}"]) wenzelm@10249: fix N berghofe@23751: assume "(N, M0 + {#a#}) \ ?R" berghofe@23751: then have "((\M. (M, M0) \ ?R \ N = M + {#a#}) \ berghofe@23751: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K))" wenzelm@10249: by (rule less_add) berghofe@23751: then show "N \ ?W" wenzelm@10249: proof (elim exE disjE conjE) berghofe@23751: fix M assume "(M, M0) \ ?R" and N: "N = M + {#a#}" berghofe@23751: from acc_hyp have "(M, M0) \ ?R --> M + {#a#} \ ?W" .. berghofe@23751: from this and `(M, M0) \ ?R` have "M + {#a#} \ ?W" .. berghofe@23751: then show "N \ ?W" by (simp only: N) wenzelm@10249: next wenzelm@10249: fix K wenzelm@10249: assume N: "N = M0 + K" berghofe@23751: assume "\b. b :# K --> (b, a) \ r" berghofe@23751: then have "M0 + K \ ?W" wenzelm@10249: proof (induct K) wenzelm@18730: case empty berghofe@23751: from M0 show "M0 + {#} \ ?W" by simp wenzelm@18730: next wenzelm@18730: case (add K x) berghofe@23751: from add.prems have "(x, a) \ r" by simp berghofe@23751: with wf_hyp have "\M \ ?W. M + {#x#} \ ?W" by blast berghofe@23751: moreover from add have "M0 + K \ ?W" by simp berghofe@23751: ultimately have "(M0 + K) + {#x#} \ ?W" .. berghofe@23751: then show "M0 + (K + {#x#}) \ ?W" by (simp only: union_assoc) wenzelm@10249: qed berghofe@23751: then show "N \ ?W" by (simp only: N) wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: } note tedious_reasoning = this wenzelm@10249: berghofe@23751: assume wf: "wf r" wenzelm@10249: fix M berghofe@23751: show "M \ ?W" wenzelm@10249: proof (induct M) berghofe@23751: show "{#} \ ?W" wenzelm@10249: proof (rule accI) berghofe@23751: fix b assume "(b, {#}) \ ?R" berghofe@23751: with not_less_empty show "b \ ?W" by contradiction wenzelm@10249: qed wenzelm@10249: berghofe@23751: fix M a assume "M \ ?W" berghofe@23751: from wf have "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof induct wenzelm@10249: fix a berghofe@23751: assume r: "!!b. (b, a) \ r ==> (\M \ ?W. M + {#b#} \ ?W)" berghofe@23751: show "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof berghofe@23751: fix M assume "M \ ?W" berghofe@23751: then show "M + {#a#} \ ?W" wenzelm@23373: by (rule acc_induct) (rule tedious_reasoning [OF _ r]) wenzelm@10249: qed wenzelm@10249: qed berghofe@23751: from this and `M \ ?W` show "M + {#a#} \ ?W" .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: berghofe@23751: theorem wf_mult1: "wf r ==> wf (mult1 r)" wenzelm@23373: by (rule acc_wfI) (rule all_accessible) wenzelm@10249: berghofe@23751: theorem wf_mult: "wf r ==> wf (mult r)" berghofe@23751: unfolding mult_def by (rule wf_trancl) (rule wf_mult1) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Closure-free presentation *} wenzelm@10249: wenzelm@10249: (*Badly needed: a linear arithmetic procedure for multisets*) wenzelm@10249: wenzelm@10249: lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})" wenzelm@23373: by (simp add: multiset_eq_conv_count_eq) wenzelm@10249: wenzelm@10249: text {* One direction. *} wenzelm@10249: wenzelm@10249: lemma mult_implies_one_step: berghofe@23751: "trans r ==> (M, N) \ mult r ==> nipkow@11464: \I J K. N = I + J \ M = I + K \ J \ {#} \ berghofe@23751: (\k \ set_of K. \j \ set_of J. (k, j) \ r)" wenzelm@10249: apply (unfold mult_def mult1_def set_of_def) berghofe@23751: apply (erule converse_trancl_induct, clarify) paulson@15072: apply (rule_tac x = M0 in exI, simp, clarify) berghofe@23751: apply (case_tac "a :# K") wenzelm@10249: apply (rule_tac x = I in exI) wenzelm@10249: apply (simp (no_asm)) berghofe@23751: apply (rule_tac x = "(K - {#a#}) + Ka" in exI) wenzelm@10249: apply (simp (no_asm_simp) add: union_assoc [symmetric]) nipkow@11464: apply (drule_tac f = "\M. M - {#a#}" in arg_cong) wenzelm@10249: apply (simp add: diff_union_single_conv) wenzelm@10249: apply (simp (no_asm_use) add: trans_def) wenzelm@10249: apply blast wenzelm@10249: apply (subgoal_tac "a :# I") wenzelm@10249: apply (rule_tac x = "I - {#a#}" in exI) wenzelm@10249: apply (rule_tac x = "J + {#a#}" in exI) wenzelm@10249: apply (rule_tac x = "K + Ka" in exI) wenzelm@10249: apply (rule conjI) wenzelm@10249: apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) wenzelm@10249: apply (rule conjI) paulson@15072: apply (drule_tac f = "\M. M - {#a#}" in arg_cong, simp) wenzelm@10249: apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) wenzelm@10249: apply (simp (no_asm_use) add: trans_def) wenzelm@10249: apply blast wenzelm@10277: apply (subgoal_tac "a :# (M0 + {#a#})") wenzelm@10249: apply simp wenzelm@10249: apply (simp (no_asm)) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}" wenzelm@23373: by (simp add: multiset_eq_conv_count_eq) wenzelm@10249: nipkow@11464: lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \a N. M = N + {#a#}" wenzelm@10249: apply (erule size_eq_Suc_imp_elem [THEN exE]) paulson@15072: apply (drule elem_imp_eq_diff_union, auto) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma one_step_implies_mult_aux: berghofe@23751: "trans r ==> berghofe@23751: \I J K. (size J = n \ J \ {#} \ (\k \ set_of K. \j \ set_of J. (k, j) \ r)) berghofe@23751: --> (I + K, I + J) \ mult r" paulson@15072: apply (induct_tac n, auto) paulson@15072: apply (frule size_eq_Suc_imp_eq_union, clarify) paulson@15072: apply (rename_tac "J'", simp) paulson@15072: apply (erule notE, auto) wenzelm@10249: apply (case_tac "J' = {#}") wenzelm@10249: apply (simp add: mult_def) berghofe@23751: apply (rule r_into_trancl) paulson@15072: apply (simp add: mult1_def set_of_def, blast) nipkow@11464: txt {* Now we know @{term "J' \ {#}"}. *} berghofe@23751: apply (cut_tac M = K and P = "\x. (x, a) \ r" in multiset_partition) nipkow@11464: apply (erule_tac P = "\k \ set_of K. ?P k" in rev_mp) wenzelm@10249: apply (erule ssubst) paulson@15072: apply (simp add: Ball_def, auto) wenzelm@10249: apply (subgoal_tac berghofe@23751: "((I + {# x : K. (x, a) \ r #}) + {# x : K. (x, a) \ r #}, berghofe@23751: (I + {# x : K. (x, a) \ r #}) + J') \ mult r") wenzelm@10249: prefer 2 wenzelm@10249: apply force wenzelm@10249: apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def) berghofe@23751: apply (erule trancl_trans) berghofe@23751: apply (rule r_into_trancl) wenzelm@10249: apply (simp add: mult1_def set_of_def) wenzelm@10249: apply (rule_tac x = a in exI) wenzelm@10249: apply (rule_tac x = "I + J'" in exI) wenzelm@10249: apply (simp add: union_ac) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma one_step_implies_mult: berghofe@23751: "trans r ==> J \ {#} ==> \k \ set_of K. \j \ set_of J. (k, j) \ r berghofe@23751: ==> (I + K, I + J) \ mult r" wenzelm@23373: using one_step_implies_mult_aux by blast wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Partial-order properties *} wenzelm@10249: wenzelm@12338: instance multiset :: (type) ord .. wenzelm@10249: wenzelm@10249: defs (overloaded) berghofe@23751: less_multiset_def: "M' < M == (M', M) \ mult {(x', x). x' < x}" nipkow@11464: le_multiset_def: "M' <= M == M' = M \ M' < (M::'a multiset)" wenzelm@10249: berghofe@23751: lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" wenzelm@18730: unfolding trans_def by (blast intro: order_less_trans) wenzelm@10249: wenzelm@10249: text {* wenzelm@10249: \medskip Irreflexivity. wenzelm@10249: *} wenzelm@10249: wenzelm@10249: lemma mult_irrefl_aux: wenzelm@18258: "finite A ==> (\x \ A. \y \ A. x < (y::'a::order)) \ A = {}" wenzelm@23373: by (induct rule: finite_induct) (auto intro: order_less_trans) wenzelm@10249: wenzelm@17161: lemma mult_less_not_refl: "\ M < (M::'a::order multiset)" paulson@15072: apply (unfold less_multiset_def, auto) paulson@15072: apply (drule trans_base_order [THEN mult_implies_one_step], auto) wenzelm@10249: apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]]) wenzelm@10249: apply (simp add: set_of_eq_empty_iff) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R" wenzelm@23373: using insert mult_less_not_refl by fast wenzelm@10249: wenzelm@10249: wenzelm@10249: text {* Transitivity. *} wenzelm@10249: wenzelm@10249: theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)" berghofe@23751: unfolding less_multiset_def mult_def by (blast intro: trancl_trans) wenzelm@10249: wenzelm@10249: text {* Asymmetry. *} wenzelm@10249: nipkow@11464: theorem mult_less_not_sym: "M < N ==> \ N < (M::'a::order multiset)" wenzelm@10249: apply auto wenzelm@10249: apply (rule mult_less_not_refl [THEN notE]) paulson@15072: apply (erule mult_less_trans, assumption) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mult_less_asym: nipkow@11464: "M < N ==> (\ P ==> N < (M::'a::order multiset)) ==> P" paulson@15072: by (insert mult_less_not_sym, blast) wenzelm@10249: wenzelm@10249: theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)" wenzelm@18730: unfolding le_multiset_def by auto wenzelm@10249: wenzelm@10249: text {* Anti-symmetry. *} wenzelm@10249: wenzelm@10249: theorem mult_le_antisym: wenzelm@10249: "M <= N ==> N <= M ==> M = (N::'a::order multiset)" wenzelm@18730: unfolding le_multiset_def by (blast dest: mult_less_not_sym) wenzelm@10249: wenzelm@10249: text {* Transitivity. *} wenzelm@10249: wenzelm@10249: theorem mult_le_trans: wenzelm@10249: "K <= M ==> M <= N ==> K <= (N::'a::order multiset)" wenzelm@18730: unfolding le_multiset_def by (blast intro: mult_less_trans) wenzelm@10249: wenzelm@11655: theorem mult_less_le: "(M < N) = (M <= N \ M \ (N::'a::order multiset))" wenzelm@18730: unfolding le_multiset_def by auto wenzelm@10249: wenzelm@10277: text {* Partial order. *} wenzelm@10277: wenzelm@10277: instance multiset :: (order) order wenzelm@10277: apply intro_classes berghofe@23751: apply (rule mult_less_le) berghofe@23751: apply (rule mult_le_refl) berghofe@23751: apply (erule mult_le_trans, assumption) berghofe@23751: apply (erule mult_le_antisym, assumption) wenzelm@10277: done wenzelm@10277: wenzelm@10249: wenzelm@10249: subsubsection {* Monotonicity of multiset union *} wenzelm@10249: wenzelm@17161: lemma mult1_union: berghofe@23751: "(B, D) \ mult1 r ==> trans r ==> (C + B, C + D) \ mult1 r" paulson@15072: apply (unfold mult1_def, auto) wenzelm@10249: apply (rule_tac x = a in exI) wenzelm@10249: apply (rule_tac x = "C + M0" in exI) wenzelm@10249: apply (simp add: union_assoc) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)" wenzelm@10249: apply (unfold less_multiset_def mult_def) berghofe@23751: apply (erule trancl_induct) berghofe@23751: apply (blast intro: mult1_union transI order_less_trans r_into_trancl) berghofe@23751: apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)" wenzelm@10249: apply (subst union_commute [of B C]) wenzelm@10249: apply (subst union_commute [of D C]) wenzelm@10249: apply (erule union_less_mono2) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma union_less_mono: wenzelm@10249: "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)" wenzelm@10249: apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma union_le_mono: wenzelm@10249: "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" wenzelm@18730: unfolding le_multiset_def wenzelm@18730: by (blast intro: union_less_mono union_less_mono1 union_less_mono2) wenzelm@10249: wenzelm@17161: lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)" wenzelm@10249: apply (unfold le_multiset_def less_multiset_def) wenzelm@10249: apply (case_tac "M = {#}") wenzelm@10249: prefer 2 berghofe@23751: apply (subgoal_tac "({#} + {#}, {#} + M) \ mult (Collect (split op <))") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule one_step_implies_mult) berghofe@23751: apply (simp only: trans_def, auto) wenzelm@10249: done wenzelm@10249: wenzelm@17161: lemma union_upper1: "A <= A + (B::'a::order multiset)" paulson@15072: proof - wenzelm@17200: have "A + {#} <= A + B" by (blast intro: union_le_mono) wenzelm@18258: then show ?thesis by simp paulson@15072: qed paulson@15072: wenzelm@17161: lemma union_upper2: "B <= A + (B::'a::order multiset)" wenzelm@18258: by (subst union_commute) (rule union_upper1) paulson@15072: nipkow@23611: instance multiset :: (order) pordered_ab_semigroup_add nipkow@23611: apply intro_classes nipkow@23611: apply(erule union_le_mono[OF mult_le_refl]) nipkow@23611: done paulson@15072: wenzelm@17200: subsection {* Link with lists *} paulson@15072: wenzelm@17200: consts paulson@15072: multiset_of :: "'a list \ 'a multiset" paulson@15072: primrec paulson@15072: "multiset_of [] = {#}" paulson@15072: "multiset_of (a # x) = multiset_of x + {# a #}" paulson@15072: paulson@15072: lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])" wenzelm@18258: by (induct x) auto paulson@15072: paulson@15072: lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])" wenzelm@18258: by (induct x) auto paulson@15072: paulson@15072: lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x" wenzelm@18258: by (induct x) auto kleing@15867: kleing@15867: lemma mem_set_multiset_eq: "x \ set xs = (x :# multiset_of xs)" kleing@15867: by (induct xs) auto paulson@15072: wenzelm@18258: lemma multiset_of_append [simp]: wenzelm@18258: "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" wenzelm@20503: by (induct xs arbitrary: ys) (auto simp: union_ac) wenzelm@18730: paulson@15072: lemma surj_multiset_of: "surj multiset_of" wenzelm@17200: apply (unfold surj_def, rule allI) wenzelm@17200: apply (rule_tac M=y in multiset_induct, auto) wenzelm@17200: apply (rule_tac x = "x # xa" in exI, auto) wenzelm@10249: done wenzelm@10249: nipkow@25162: lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" wenzelm@18258: by (induct x) auto paulson@15072: wenzelm@17200: lemma distinct_count_atmost_1: paulson@15072: "distinct x = (! a. count (multiset_of x) a = (if a \ set x then 1 else 0))" wenzelm@18258: apply (induct x, simp, rule iffI, simp_all) wenzelm@17200: apply (rule conjI) wenzelm@17200: apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) paulson@15072: apply (erule_tac x=a in allE, simp, clarify) wenzelm@17200: apply (erule_tac x=aa in allE, simp) paulson@15072: done paulson@15072: wenzelm@17200: lemma multiset_of_eq_setD: kleing@15867: "multiset_of xs = multiset_of ys \ set xs = set ys" kleing@15867: by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0) kleing@15867: wenzelm@17200: lemma set_eq_iff_multiset_of_eq_distinct: wenzelm@17200: "\distinct x; distinct y\ paulson@15072: \ (set x = set y) = (multiset_of x = multiset_of y)" wenzelm@17200: by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) paulson@15072: wenzelm@17200: lemma set_eq_iff_multiset_of_remdups_eq: paulson@15072: "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" wenzelm@17200: apply (rule iffI) wenzelm@17200: apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) wenzelm@17200: apply (drule distinct_remdups[THEN distinct_remdups wenzelm@17200: [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) paulson@15072: apply simp wenzelm@10249: done wenzelm@10249: wenzelm@18258: lemma multiset_of_compl_union [simp]: nipkow@23281: "multiset_of [x\xs. P x] + multiset_of [x\xs. \P x] = multiset_of xs" kleing@15630: by (induct xs) (auto simp: union_ac) paulson@15072: wenzelm@17200: lemma count_filter: nipkow@23281: "count (multiset_of xs) x = length [y \ xs. y = x]" wenzelm@18258: by (induct xs) auto kleing@15867: kleing@15867: paulson@15072: subsection {* Pointwise ordering induced by count *} paulson@15072: wenzelm@19086: definition nipkow@23611: mset_le :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where nipkow@23611: "(A \# B) = (\a. count A a \ count B a)" nipkow@23611: definition nipkow@23611: mset_less :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where nipkow@23611: "(A <# B) = (A \# B \ A \ B)" paulson@15072: nipkow@23611: lemma mset_le_refl[simp]: "A \# A" wenzelm@18730: unfolding mset_le_def by auto paulson@15072: nipkow@23611: lemma mset_le_trans: "\ A \# B; B \# C \ \ A \# C" wenzelm@18730: unfolding mset_le_def by (fast intro: order_trans) paulson@15072: nipkow@23611: lemma mset_le_antisym: "\ A \# B; B \# A \ \ A = B" wenzelm@17200: apply (unfold mset_le_def) wenzelm@17200: apply (rule multiset_eq_conv_count_eq[THEN iffD2]) paulson@15072: apply (blast intro: order_antisym) paulson@15072: done paulson@15072: wenzelm@17200: lemma mset_le_exists_conv: nipkow@23611: "(A \# B) = (\C. B = A + C)" nipkow@23611: apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI) paulson@15072: apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) paulson@15072: done paulson@15072: nipkow@23611: lemma mset_le_mono_add_right_cancel[simp]: "(A + C \# B + C) = (A \# B)" wenzelm@18730: unfolding mset_le_def by auto paulson@15072: nipkow@23611: lemma mset_le_mono_add_left_cancel[simp]: "(C + A \# C + B) = (A \# B)" wenzelm@18730: unfolding mset_le_def by auto paulson@15072: nipkow@23611: lemma mset_le_mono_add: "\ A \# B; C \# D \ \ A + C \# B + D" wenzelm@17200: apply (unfold mset_le_def) wenzelm@17200: apply auto paulson@15072: apply (erule_tac x=a in allE)+ paulson@15072: apply auto paulson@15072: done paulson@15072: nipkow@23611: lemma mset_le_add_left[simp]: "A \# A + B" wenzelm@18730: unfolding mset_le_def by auto paulson@15072: nipkow@23611: lemma mset_le_add_right[simp]: "B \# A + B" wenzelm@18730: unfolding mset_le_def by auto paulson@15072: nipkow@23611: lemma multiset_of_remdups_le: "multiset_of (remdups xs) \# multiset_of xs" nipkow@23611: apply (induct xs) nipkow@23611: apply auto nipkow@23611: apply (rule mset_le_trans) nipkow@23611: apply auto nipkow@23611: done nipkow@23611: haftmann@25208: interpretation mset_order: haftmann@25208: order ["op \#" "op <#"] haftmann@25208: by (auto intro: order.intro mset_le_refl mset_le_antisym haftmann@25208: mset_le_trans simp: mset_less_def) nipkow@23611: nipkow@23611: interpretation mset_order_cancel_semigroup: haftmann@25208: pordered_cancel_ab_semigroup_add ["op \#" "op <#" "op +"] haftmann@25208: by unfold_locales (erule mset_le_mono_add [OF mset_le_refl]) nipkow@23611: nipkow@23611: interpretation mset_order_semigroup_cancel: haftmann@25208: pordered_ab_semigroup_add_imp_le ["op \#" "op <#" "op +"] haftmann@25208: by (unfold_locales) simp paulson@15072: wenzelm@10249: end