wenzelm@10249: (* Title: HOL/Library/Multiset.thy wenzelm@10249: ID: $Id$ wenzelm@10249: Author: Tobias Nipkow, TU Muenchen wenzelm@10249: Author: Markus Wenzel, TU Muenchen wenzelm@10249: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@10249: *) wenzelm@10249: wenzelm@10249: header {* wenzelm@10249: \title{Multisets} wenzelm@10249: \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson} wenzelm@10249: *} wenzelm@10249: wenzelm@10249: theory Multiset = Accessible_Part: wenzelm@10249: wenzelm@10249: subsection {* The type of multisets *} wenzelm@10249: wenzelm@10249: typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" wenzelm@10249: proof wenzelm@10277: 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@10249: constdefs wenzelm@10249: Mempty :: "'a multiset" ("{#}") wenzelm@10249: "{#} == Abs_multiset (\a. 0)" wenzelm@10249: wenzelm@10249: single :: "'a => 'a multiset" ("{#_#}") wenzelm@10249: "{#a#} == Abs_multiset (\b. if b = a then 1 else 0)" wenzelm@10249: wenzelm@10249: count :: "'a multiset => 'a => nat" wenzelm@10249: "count == Rep_multiset" wenzelm@10249: wenzelm@10249: MCollect :: "'a multiset => ('a => bool) => 'a multiset" wenzelm@10249: "MCollect M P == Abs_multiset (\x. if P x then Rep_multiset M x else 0)" wenzelm@10249: wenzelm@10249: syntax wenzelm@10249: "_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) wenzelm@10249: "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") wenzelm@10249: translations wenzelm@10249: "a :# M" == "0 < count M a" wenzelm@10249: "{#x:M. P#}" == "MCollect M (\x. P)" wenzelm@10249: wenzelm@10249: constdefs wenzelm@10249: set_of :: "'a multiset => 'a set" wenzelm@10249: "set_of M == {x. x :# M}" wenzelm@10249: wenzelm@10249: instance multiset :: ("term") plus by intro_classes wenzelm@10249: instance multiset :: ("term") minus by intro_classes wenzelm@10249: instance multiset :: ("term") zero by intro_classes wenzelm@10249: wenzelm@10249: defs (overloaded) wenzelm@10249: union_def: "M + N == Abs_multiset (\a. Rep_multiset M a + Rep_multiset N a)" wenzelm@10249: diff_def: "M - N == Abs_multiset (\a. Rep_multiset M a - Rep_multiset N a)" wenzelm@10249: Zero_def [simp]: "0 == {#}" wenzelm@10249: size_def: "size M == setsum (count M) (set_of M)" wenzelm@10249: wenzelm@10249: wenzelm@10249: text {* wenzelm@10249: \medskip Preservation of the representing set @{term multiset}. wenzelm@10249: *} wenzelm@10249: wenzelm@10249: lemma const0_in_multiset [simp]: "(\a. 0) \ multiset" wenzelm@10249: apply (simp add: multiset_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma only1_in_multiset [simp]: "(\b. if b = a then 1 else 0) \ multiset" wenzelm@10249: apply (simp add: multiset_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma union_preserves_multiset [simp]: wenzelm@10249: "M \ multiset ==> N \ multiset ==> (\a. M a + N a) \ multiset" wenzelm@10249: apply (unfold multiset_def) wenzelm@10249: apply simp wenzelm@10249: apply (drule finite_UnI) wenzelm@10249: apply assumption wenzelm@10249: apply (simp del: finite_Un add: Un_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma diff_preserves_multiset [simp]: wenzelm@10249: "M \ multiset ==> (\a. M a - N a) \ multiset" wenzelm@10249: apply (unfold multiset_def) wenzelm@10249: apply simp wenzelm@10249: apply (rule finite_subset) wenzelm@10249: prefer 2 wenzelm@10249: apply assumption wenzelm@10249: 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@10249: theorem union_empty [simp]: "M + {#} = M \ {#} + M = M" wenzelm@10249: apply (simp add: union_def Mempty_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_commute: "M + N = N + (M::'a multiset)" wenzelm@10249: apply (simp add: union_def add_ac) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_assoc: "(M + N) + K = M + (N + (K::'a multiset))" wenzelm@10249: apply (simp add: union_def add_ac) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))" wenzelm@10249: apply (rule union_commute [THEN trans]) wenzelm@10249: apply (rule union_assoc [THEN trans]) wenzelm@10249: apply (rule union_commute [THEN arg_cong]) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorems union_ac = union_assoc union_commute union_lcomm wenzelm@10249: wenzelm@10277: instance multiset :: ("term") plus_ac0 wenzelm@10277: apply intro_classes wenzelm@10277: apply (rule union_commute) wenzelm@10277: apply (rule union_assoc) wenzelm@10277: apply simp wenzelm@10277: done wenzelm@10277: wenzelm@10249: wenzelm@10249: subsubsection {* Difference *} wenzelm@10249: wenzelm@10249: theorem diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" wenzelm@10249: apply (simp add: Mempty_def diff_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M" wenzelm@10249: apply (simp add: union_def diff_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Count of elements *} wenzelm@10249: wenzelm@10249: theorem count_empty [simp]: "count {#} a = 0" wenzelm@10249: apply (simp add: count_def Mempty_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" wenzelm@10249: apply (simp add: count_def single_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem count_union [simp]: "count (M + N) a = count M a + count N a" wenzelm@10249: apply (simp add: count_def union_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem count_diff [simp]: "count (M - N) a = count M a - count N a" wenzelm@10249: apply (simp add: count_def diff_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Set of elements *} wenzelm@10249: wenzelm@10249: theorem set_of_empty [simp]: "set_of {#} = {}" wenzelm@10249: apply (simp add: set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem set_of_single [simp]: "set_of {#b#} = {b}" wenzelm@10249: apply (simp add: set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem set_of_union [simp]: "set_of (M + N) = set_of M \ set_of N" wenzelm@10249: apply (auto simp add: set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" wenzelm@10249: apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" wenzelm@10249: apply (auto simp add: set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Size *} wenzelm@10249: wenzelm@10249: theorem size_empty [simp]: "size {#} = 0" wenzelm@10249: apply (simp add: size_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem size_single [simp]: "size {#b#} = 1" wenzelm@10249: apply (simp add: size_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem finite_set_of [iff]: "finite (set_of M)" wenzelm@10249: apply (cut_tac x = M in Rep_multiset) wenzelm@10249: apply (simp add: multiset_def set_of_def count_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem setsum_count_Int: wenzelm@10249: "finite A ==> setsum (count N) (A \ set_of N) = setsum (count N) A" wenzelm@10249: apply (erule finite_induct) wenzelm@10249: apply simp wenzelm@10249: apply (simp add: Int_insert_left set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" wenzelm@10249: apply (unfold size_def) wenzelm@10249: apply (subgoal_tac "count (M + N) = (\a. count M a + count N a)") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule ext) wenzelm@10249: apply simp wenzelm@10249: apply (simp (no_asm_simp) add: setsum_Un 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@10249: theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" wenzelm@10249: apply (unfold size_def Mempty_def count_def) wenzelm@10249: apply auto wenzelm@10249: apply (simp add: set_of_def count_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \a. a :# M" wenzelm@10249: apply (unfold size_def) wenzelm@10249: apply (drule setsum_SucD) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Equality of multisets *} wenzelm@10249: wenzelm@10249: theorem multiset_eq_conv_count_eq: "(M = N) = (\a. count M a = count N a)" wenzelm@10249: apply (simp add: count_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" wenzelm@10249: apply (simp add: single_def Mempty_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" wenzelm@10249: apply (auto simp add: single_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \ N = {#})" wenzelm@10249: apply (auto simp add: union_def Mempty_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \ N = {#})" wenzelm@10249: apply (auto simp add: union_def Mempty_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" wenzelm@10249: apply (simp add: union_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" wenzelm@10249: apply (simp add: union_def expand_fun_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_is_single: wenzelm@10249: "(M + N = {#a#}) = (M = {#a#} \ N={#} \ M = {#} \ N = {#a#})" wenzelm@10249: apply (unfold Mempty_def single_def union_def) wenzelm@10249: apply (simp add: add_is_1 expand_fun_eq) wenzelm@10249: apply blast wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem single_is_union: wenzelm@10249: "({#a#} = M + N) = wenzelm@10249: ({#a#} = M \ N = {#} \ M = {#} \ {#a#} = N)" wenzelm@10249: apply (unfold Mempty_def single_def union_def) wenzelm@10249: apply (simp add: one_is_add expand_fun_eq) wenzelm@10249: apply (blast dest: sym) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem add_eq_conv_diff: wenzelm@10249: "(M + {#a#} = N + {#b#}) = wenzelm@10249: (M = N \ a = b \ wenzelm@10249: M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#})" wenzelm@10249: apply (unfold single_def union_def diff_def) wenzelm@10249: apply (simp (no_asm) add: expand_fun_eq) wenzelm@10249: apply (rule conjI) wenzelm@10249: apply force wenzelm@10249: apply clarify wenzelm@10249: apply (rule conjI) wenzelm@10249: apply blast wenzelm@10249: apply clarify wenzelm@10249: apply (rule iffI) wenzelm@10249: apply (rule conjI) wenzelm@10249: apply clarify wenzelm@10249: apply (rule conjI) wenzelm@10249: apply (simp add: eq_sym_conv) (* FIXME blast fails !? *) wenzelm@10249: apply fast wenzelm@10249: apply simp wenzelm@10249: apply force wenzelm@10249: done wenzelm@10249: wenzelm@10249: (* wenzelm@10249: val prems = Goal wenzelm@10249: "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; wenzelm@10249: by (res_inst_tac [("a","F"),("f","\A. if finite A then card A else 0")] wenzelm@10249: measure_induct 1); wenzelm@10249: by (Clarify_tac 1); wenzelm@10249: by (resolve_tac prems 1); wenzelm@10249: by (assume_tac 1); wenzelm@10249: by (Clarify_tac 1); wenzelm@10249: by (subgoal_tac "finite G" 1); wenzelm@10249: by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); wenzelm@10249: by (etac allE 1); wenzelm@10249: by (etac impE 1); wenzelm@10249: by (Blast_tac 2); wenzelm@10249: by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); wenzelm@10249: no_qed(); wenzelm@10249: val lemma = result(); wenzelm@10249: wenzelm@10249: val prems = Goal wenzelm@10249: "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F"; wenzelm@10249: by (rtac (lemma RS mp) 1); wenzelm@10249: by (REPEAT(ares_tac prems 1)); wenzelm@10249: qed "finite_psubset_induct"; wenzelm@10249: wenzelm@10249: Better: use wf_finite_psubset in WF_Rel wenzelm@10249: *) wenzelm@10249: wenzelm@10249: wenzelm@10249: subsection {* Induction over multisets *} wenzelm@10249: wenzelm@10249: lemma setsum_decr: wenzelm@10249: "finite F ==> 0 < f a ==> wenzelm@10249: setsum (f (a := f a - 1)) F = (if a \ F then setsum f F - 1 else setsum f F)" wenzelm@10249: apply (erule finite_induct) wenzelm@10249: apply auto wenzelm@10249: apply (drule_tac a = a in mk_disjoint_insert) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma Rep_multiset_induct_aux: wenzelm@10249: "P (\a. 0) ==> (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))) wenzelm@10249: ==> \f. f \ multiset --> setsum f {x. 0 < f x} = n --> P f" wenzelm@10249: proof - wenzelm@10249: case antecedent wenzelm@10249: note prems = this [unfolded multiset_def] wenzelm@10249: show ?thesis wenzelm@10249: apply (unfold multiset_def) wenzelm@10249: apply (induct_tac n) wenzelm@10249: apply simp wenzelm@10249: apply clarify wenzelm@10249: apply (subgoal_tac "f = (\a.0)") wenzelm@10249: apply simp wenzelm@10249: apply (rule prems) wenzelm@10249: apply (rule ext) wenzelm@10249: apply force wenzelm@10249: apply clarify wenzelm@10249: apply (frule setsum_SucD) wenzelm@10249: apply clarify wenzelm@10249: apply (rename_tac a) wenzelm@10249: apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule finite_subset) wenzelm@10249: prefer 2 wenzelm@10249: apply assumption wenzelm@10249: apply simp wenzelm@10249: apply blast wenzelm@10249: apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule ext) wenzelm@10249: apply (simp (no_asm_simp)) wenzelm@10249: apply (erule ssubst, rule prems) wenzelm@10249: apply blast wenzelm@10249: apply (erule allE, erule impE, erule_tac [2] mp) wenzelm@10249: apply blast wenzelm@10249: apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply) wenzelm@10249: apply (subgoal_tac "{x. x \ a --> 0 < f x} = {x. 0 < f x}") wenzelm@10249: prefer 2 wenzelm@10249: apply blast wenzelm@10249: apply (subgoal_tac "{x. x \ a \ 0 < f x} = {x. 0 < f x} - {a}") wenzelm@10249: prefer 2 wenzelm@10249: apply blast wenzelm@10249: apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong) wenzelm@10249: done wenzelm@10249: qed wenzelm@10249: wenzelm@10249: theorem Rep_multiset_induct: wenzelm@10249: "f \ multiset ==> P (\a. 0) ==> wenzelm@10249: (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" wenzelm@10249: apply (insert Rep_multiset_induct_aux) wenzelm@10249: apply blast wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem multiset_induct [induct type: multiset]: wenzelm@10249: "P {#} ==> (!!M x. P M ==> P (M + {#x#})) ==> P M" wenzelm@10249: proof - wenzelm@10249: note defns = union_def single_def Mempty_def wenzelm@10249: assume prem1 [unfolded defns]: "P {#}" wenzelm@10249: assume prem2 [unfolded defns]: "!!M x. P M ==> P (M + {#x#})" wenzelm@10249: show ?thesis wenzelm@10249: apply (rule Rep_multiset_inverse [THEN subst]) wenzelm@10249: apply (rule Rep_multiset [THEN Rep_multiset_induct]) wenzelm@10249: apply (rule prem1) wenzelm@10249: 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@10249: apply (erule Abs_multiset_inverse [THEN subst]) wenzelm@10249: apply (erule prem2 [simplified]) wenzelm@10249: done wenzelm@10249: qed wenzelm@10249: wenzelm@10249: wenzelm@10249: lemma MCollect_preserves_multiset: wenzelm@10249: "M \ multiset ==> (\x. if P x then M x else 0) \ multiset" wenzelm@10249: apply (simp add: multiset_def) wenzelm@10249: apply (rule finite_subset) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem count_MCollect [simp]: wenzelm@10249: "count {# x:M. P x #} a = (if P a then count M a else 0)" wenzelm@10249: apply (unfold count_def MCollect_def) wenzelm@10249: apply (simp add: MCollect_preserves_multiset) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \ {x. P x}" wenzelm@10249: apply (auto simp add: set_of_def) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \ P x #}" wenzelm@10249: apply (subst multiset_eq_conv_count_eq) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10277: declare Rep_multiset_inject [symmetric, simp del] wenzelm@10249: declare multiset_typedef [simp del] wenzelm@10249: wenzelm@10249: theorem add_eq_conv_ex: wenzelm@10249: "(M + {#a#} = N + {#b#}) = wenzelm@10249: (M = N \ a = b \ (\K. M = K + {#b#} \ N = K + {#a#}))" wenzelm@10249: apply (auto simp add: add_eq_conv_diff) wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsection {* Multiset orderings *} wenzelm@10249: wenzelm@10249: subsubsection {* Well-foundedness *} wenzelm@10249: wenzelm@10249: constdefs wenzelm@10249: mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" wenzelm@10249: "mult1 r == wenzelm@10249: {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ wenzelm@10249: (\b. b :# K --> (b, a) \ r)}" wenzelm@10249: wenzelm@10249: mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" wenzelm@10249: "mult r == (mult1 r)^+" wenzelm@10249: wenzelm@10249: lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" wenzelm@10277: by (simp add: mult1_def) wenzelm@10249: wenzelm@10249: lemma less_add: "(N, M0 + {#a#}) \ mult1 r ==> wenzelm@10249: (\M. (M, M0) \ mult1 r \ N = M + {#a#}) \ wenzelm@10249: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K)" wenzelm@10249: (concl is "?case1 (mult1 r) \ ?case2") wenzelm@10249: proof (unfold mult1_def) wenzelm@10249: let ?r = "\K a. \b. b :# K --> (b, a) \ r" wenzelm@10249: let ?R = "\N M. \a M0 K. M = M0 + {#a#} \ N = M0 + K \ ?r K a" wenzelm@10249: let ?case1 = "?case1 {(N, M). ?R N M}" wenzelm@10249: wenzelm@10249: assume "(N, M0 + {#a#}) \ {(N, M). ?R N M}" wenzelm@10249: hence "\a' M0' K. wenzelm@10249: M0 + {#a#} = M0' + {#a'#} \ N = M0' + K \ ?r K a'" by simp wenzelm@10249: thus "?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@10249: hence "M0 = M0' \ a = a' \ wenzelm@10249: (\K'. M0 = K' + {#a'#} \ M0' = K' + {#a#})" wenzelm@10249: by (simp only: add_eq_conv_ex) wenzelm@10249: thus ?thesis wenzelm@10249: proof (elim disjE conjE exE) wenzelm@10249: assume "M0 = M0'" "a = a'" wenzelm@10249: with N r have "?r K a \ N = M0 + K" by simp wenzelm@10249: hence ?case2 .. thus ?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@10249: with n have ?case1 by simp thus ?thesis .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: wenzelm@10249: 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 wenzelm@10249: assume M0: "M0 \ ?W" wenzelm@10249: and wf_hyp: "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" wenzelm@10249: and acc_hyp: "\M. (M, M0) \ ?R --> M + {#a#} \ ?W" wenzelm@10249: have "M0 + {#a#} \ ?W" wenzelm@10249: proof (rule accI [of "M0 + {#a#}"]) wenzelm@10249: fix N wenzelm@10249: assume "(N, M0 + {#a#}) \ ?R" wenzelm@10249: hence "((\M. (M, M0) \ ?R \ N = M + {#a#}) \ wenzelm@10249: (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K))" wenzelm@10249: by (rule less_add) wenzelm@10249: thus "N \ ?W" wenzelm@10249: proof (elim exE disjE conjE) wenzelm@10249: fix M assume "(M, M0) \ ?R" and N: "N = M + {#a#}" wenzelm@10249: from acc_hyp have "(M, M0) \ ?R --> M + {#a#} \ ?W" .. wenzelm@10249: hence "M + {#a#} \ ?W" .. wenzelm@10249: thus "N \ ?W" by (simp only: N) wenzelm@10249: next wenzelm@10249: fix K wenzelm@10249: assume N: "N = M0 + K" wenzelm@10249: assume "\b. b :# K --> (b, a) \ r" wenzelm@10249: have "?this --> M0 + K \ ?W" (is "?P K") wenzelm@10249: proof (induct K) wenzelm@10249: from M0 have "M0 + {#} \ ?W" by simp wenzelm@10249: thus "?P {#}" .. wenzelm@10249: wenzelm@10249: fix K x assume hyp: "?P K" wenzelm@10249: show "?P (K + {#x#})" wenzelm@10249: proof wenzelm@10249: assume a: "\b. b :# (K + {#x#}) --> (b, a) \ r" wenzelm@10249: hence "(x, a) \ r" by simp wenzelm@10249: with wf_hyp have b: "\M \ ?W. M + {#x#} \ ?W" by blast wenzelm@10249: wenzelm@10249: from a hyp have "M0 + K \ ?W" by simp wenzelm@10249: with b have "(M0 + K) + {#x#} \ ?W" .. wenzelm@10249: thus "M0 + (K + {#x#}) \ ?W" by (simp only: union_assoc) wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: hence "M0 + K \ ?W" .. wenzelm@10249: thus "N \ ?W" by (simp only: N) wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: } note tedious_reasoning = this wenzelm@10249: wenzelm@10249: assume wf: "wf r" wenzelm@10249: fix M wenzelm@10249: show "M \ ?W" wenzelm@10249: proof (induct M) wenzelm@10249: show "{#} \ ?W" wenzelm@10249: proof (rule accI) wenzelm@10249: fix b assume "(b, {#}) \ ?R" wenzelm@10249: with not_less_empty show "b \ ?W" by contradiction wenzelm@10249: qed wenzelm@10249: wenzelm@10249: fix M a assume "M \ ?W" wenzelm@10249: from wf have "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof induct wenzelm@10249: fix a wenzelm@10249: assume "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" wenzelm@10249: show "\M \ ?W. M + {#a#} \ ?W" wenzelm@10249: proof wenzelm@10249: fix M assume "M \ ?W" wenzelm@10249: thus "M + {#a#} \ ?W" wenzelm@10249: by (rule acc_induct) (rule tedious_reasoning) wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: thus "M + {#a#} \ ?W" .. wenzelm@10249: qed wenzelm@10249: qed wenzelm@10249: wenzelm@10249: theorem wf_mult1: "wf r ==> wf (mult1 r)" wenzelm@10249: by (rule acc_wfI, rule all_accessible) wenzelm@10249: wenzelm@10249: theorem wf_mult: "wf r ==> wf (mult r)" wenzelm@10249: by (unfold mult_def, 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@10249: apply (simp add: multiset_eq_conv_count_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: text {* One direction. *} wenzelm@10249: wenzelm@10249: lemma mult_implies_one_step: wenzelm@10249: "trans r ==> (M, N) \ mult r ==> wenzelm@10249: \I J K. N = I + J \ M = I + K \ J \ {#} \ wenzelm@10249: (\k \ set_of K. \j \ set_of J. (k, j) \ r)" wenzelm@10249: apply (unfold mult_def mult1_def set_of_def) wenzelm@10249: apply (erule converse_trancl_induct) wenzelm@10249: apply clarify wenzelm@10249: apply (rule_tac x = M0 in exI) wenzelm@10249: apply simp wenzelm@10249: apply clarify wenzelm@10249: apply (case_tac "a :# K") wenzelm@10249: apply (rule_tac x = I in exI) wenzelm@10249: apply (simp (no_asm)) wenzelm@10249: apply (rule_tac x = "(K - {#a#}) + Ka" in exI) wenzelm@10249: apply (simp (no_asm_simp) add: union_assoc [symmetric]) wenzelm@10249: 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) wenzelm@10249: apply (drule_tac f = "\M. M - {#a#}" in arg_cong) wenzelm@10249: apply 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@10249: apply (simp add: multiset_eq_conv_count_eq) wenzelm@10249: done wenzelm@10249: wenzelm@10249: 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]) wenzelm@10249: apply (drule elem_imp_eq_diff_union) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: lemma one_step_implies_mult_aux: wenzelm@10249: "trans r ==> wenzelm@10249: \I J K. (size J = n \ J \ {#} \ (\k \ set_of K. \j \ set_of J. (k, j) \ r)) wenzelm@10249: --> (I + K, I + J) \ mult r" wenzelm@10249: apply (induct_tac n) wenzelm@10249: apply auto wenzelm@10249: apply (frule size_eq_Suc_imp_eq_union) wenzelm@10249: apply clarify wenzelm@10249: apply (rename_tac "J'") wenzelm@10249: apply simp wenzelm@10249: apply (erule notE) wenzelm@10249: apply auto wenzelm@10249: apply (case_tac "J' = {#}") wenzelm@10249: apply (simp add: mult_def) wenzelm@10249: apply (rule r_into_trancl) wenzelm@10249: apply (simp add: mult1_def set_of_def) wenzelm@10249: apply blast wenzelm@10249: txt {* Now we know @{term "J' \ {#}"}. *} wenzelm@10249: apply (cut_tac M = K and P = "\x. (x, a) \ r" in multiset_partition) wenzelm@10249: apply (erule_tac P = "\k \ set_of K. ?P k" in rev_mp) wenzelm@10249: apply (erule ssubst) wenzelm@10249: apply (simp add: Ball_def) wenzelm@10249: apply auto wenzelm@10249: apply (subgoal_tac wenzelm@10249: "((I + {# x : K. (x, a) \ r #}) + {# x : K. (x, a) \ r #}, wenzelm@10249: (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) wenzelm@10249: apply (erule trancl_trans) wenzelm@10249: 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@10249: theorem one_step_implies_mult: wenzelm@10249: "trans r ==> J \ {#} ==> \k \ set_of K. \j \ set_of J. (k, j) \ r wenzelm@10249: ==> (I + K, I + J) \ mult r" wenzelm@10249: apply (insert one_step_implies_mult_aux) wenzelm@10249: apply blast wenzelm@10249: done wenzelm@10249: wenzelm@10249: wenzelm@10249: subsubsection {* Partial-order properties *} wenzelm@10249: wenzelm@10249: instance multiset :: ("term") ord by intro_classes wenzelm@10249: wenzelm@10249: defs (overloaded) wenzelm@10249: less_multiset_def: "M' < M == (M', M) \ mult {(x', x). x' < x}" wenzelm@10249: le_multiset_def: "M' <= M == M' = M \ M' < (M::'a multiset)" wenzelm@10249: wenzelm@10249: lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" wenzelm@10249: apply (unfold trans_def) wenzelm@10249: apply (blast intro: order_less_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: text {* wenzelm@10249: \medskip Irreflexivity. wenzelm@10249: *} wenzelm@10249: wenzelm@10249: lemma mult_irrefl_aux: wenzelm@10249: "finite A ==> (\x \ A. \y \ A. x < (y::'a::order)) --> A = {}" wenzelm@10249: apply (erule finite_induct) wenzelm@10249: apply (auto intro: order_less_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mult_less_not_refl: "\ M < (M::'a::order multiset)" wenzelm@10249: apply (unfold less_multiset_def) wenzelm@10249: apply auto wenzelm@10249: apply (drule trans_base_order [THEN mult_implies_one_step]) wenzelm@10249: apply 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@10249: apply (insert mult_less_not_refl) wenzelm@10249: apply blast wenzelm@10249: done 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)" wenzelm@10249: apply (unfold less_multiset_def mult_def) wenzelm@10249: apply (blast intro: trancl_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: text {* Asymmetry. *} wenzelm@10249: wenzelm@10249: 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]) wenzelm@10249: apply (erule mult_less_trans) wenzelm@10249: apply assumption wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mult_less_asym: wenzelm@10249: "M < N ==> (\ P ==> N < (M::'a::order multiset)) ==> P" wenzelm@10249: apply (insert mult_less_not_sym) wenzelm@10249: apply blast wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)" wenzelm@10249: apply (unfold le_multiset_def) wenzelm@10249: apply auto wenzelm@10249: done 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@10249: apply (unfold le_multiset_def) wenzelm@10249: apply (blast dest: mult_less_not_sym) wenzelm@10249: done 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@10249: apply (unfold le_multiset_def) wenzelm@10249: apply (blast intro: mult_less_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem mult_less_le: "M < N = (M <= N \ M \ (N::'a::order multiset))" wenzelm@10249: apply (unfold le_multiset_def) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10277: text {* Partial order. *} wenzelm@10277: wenzelm@10277: instance multiset :: (order) order wenzelm@10277: apply intro_classes wenzelm@10277: apply (rule mult_le_refl) wenzelm@10277: apply (erule mult_le_trans) wenzelm@10277: apply assumption wenzelm@10277: apply (erule mult_le_antisym) wenzelm@10277: apply assumption wenzelm@10277: apply (rule mult_less_le) wenzelm@10277: done wenzelm@10277: wenzelm@10249: wenzelm@10249: subsubsection {* Monotonicity of multiset union *} wenzelm@10249: wenzelm@10249: theorem mult1_union: wenzelm@10249: "(B, D) \ mult1 r ==> trans r ==> (C + B, C + D) \ mult1 r" wenzelm@10249: apply (unfold mult1_def) wenzelm@10249: apply 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) wenzelm@10249: apply (erule trancl_induct) wenzelm@10249: apply (blast intro: mult1_union transI order_less_trans r_into_trancl) wenzelm@10249: 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@10249: theorem 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@10249: theorem union_le_mono: wenzelm@10249: "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" wenzelm@10249: apply (unfold le_multiset_def) wenzelm@10249: apply (blast intro: union_less_mono union_less_mono1 union_less_mono2) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem 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 wenzelm@10249: apply (subgoal_tac "({#} + {#}, {#} + M) \ mult (Collect (split op <))") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule one_step_implies_mult) wenzelm@10249: apply (simp only: trans_def) wenzelm@10249: apply auto wenzelm@10249: apply (blast intro: order_less_trans) wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_upper1: "A <= A + (B::'a::order multiset)" wenzelm@10249: apply (subgoal_tac "A + {#} <= A + B") wenzelm@10249: prefer 2 wenzelm@10249: apply (rule union_le_mono) wenzelm@10249: apply auto wenzelm@10249: done wenzelm@10249: wenzelm@10249: theorem union_upper2: "B <= A + (B::'a::order multiset)" wenzelm@10249: apply (subst union_commute, rule union_upper1) wenzelm@10249: done wenzelm@10249: wenzelm@10249: end