src/HOL/Library/Multiset.thy
author wenzelm
Wed Oct 18 23:28:33 2000 +0200 (2000-10-18)
changeset 10249 e4d13d8a9011
child 10277 081c8641aa11
permissions -rw-r--r--
Multisets (from HOL/Induct/Multiset and friends);
     1 (*  Title:      HOL/Library/Multiset.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, TU Muenchen
     4     Author:     Markus Wenzel, TU Muenchen
     5     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6 *)
     7 
     8 header {*
     9  \title{Multisets}
    10  \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson}
    11 *}
    12 
    13 theory Multiset = Accessible_Part:
    14 
    15 subsection {* The type of multisets *}
    16 
    17 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
    18 proof
    19   show "(\<lambda>x. 0::nat) \<in> {f. finite {x. 0 < f x}}"
    20     by simp
    21 qed
    22 
    23 lemmas multiset_typedef [simp] =
    24   Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
    25 
    26 constdefs
    27   Mempty :: "'a multiset"    ("{#}")
    28   "{#} == Abs_multiset (\<lambda>a. 0)"
    29 
    30   single :: "'a => 'a multiset"    ("{#_#}")
    31   "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    32 
    33   count :: "'a multiset => 'a => nat"
    34   "count == Rep_multiset"
    35 
    36   MCollect :: "'a multiset => ('a => bool) => 'a multiset"
    37   "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
    38 
    39 syntax
    40   "_Melem" :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
    41   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
    42 translations
    43   "a :# M" == "0 < count M a"
    44   "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
    45 
    46 constdefs
    47   set_of :: "'a multiset => 'a set"
    48   "set_of M == {x. x :# M}"
    49 
    50 instance multiset :: ("term") plus by intro_classes
    51 instance multiset :: ("term") minus by intro_classes
    52 instance multiset :: ("term") zero by intro_classes
    53 
    54 defs (overloaded)
    55   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    56   diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
    57   Zero_def [simp]: "0 == {#}"
    58   size_def: "size M == setsum (count M) (set_of M)"
    59 
    60 
    61 text {*
    62  \medskip Preservation of the representing set @{term multiset}.
    63 *}
    64 
    65 lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
    66   apply (simp add: multiset_def)
    67   done
    68 
    69 lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
    70   apply (simp add: multiset_def)
    71   done
    72 
    73 lemma union_preserves_multiset [simp]:
    74     "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
    75   apply (unfold multiset_def)
    76   apply simp
    77   apply (drule finite_UnI)
    78    apply assumption
    79   apply (simp del: finite_Un add: Un_def)
    80   done
    81 
    82 lemma diff_preserves_multiset [simp]:
    83     "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
    84   apply (unfold multiset_def)
    85   apply simp
    86   apply (rule finite_subset)
    87    prefer 2
    88    apply assumption
    89   apply auto
    90   done
    91 
    92 text {*
    93  \medskip Injectivity of @{term Rep_multiset}.
    94 *}  (* FIXME typedef package (!?) *)
    95 
    96 lemma multiset_eq_conv_Rep_eq [simp]:
    97     "(M = N) = (Rep_multiset M = Rep_multiset N)"
    98   apply (rule iffI)
    99    apply simp
   100   apply (drule_tac f = Abs_multiset in arg_cong)
   101   apply simp
   102   done
   103 
   104 (* FIXME
   105 Goal
   106  "[| f : multiset; g : multiset |] ==> \
   107 \ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
   108 by (rtac iffI 1);
   109  by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
   110  by (Asm_full_simp_tac 1);
   111 by (subgoal_tac "f = g" 1);
   112  by (Asm_simp_tac 1);
   113 by (rtac ext 1);
   114 by (Blast_tac 1);
   115 qed "Abs_multiset_eq";
   116 Addsimps [Abs_multiset_eq];
   117 *)
   118 
   119 
   120 subsection {* Algebraic properties of multisets *}
   121 
   122 subsubsection {* Union *}
   123 
   124 theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
   125   apply (simp add: union_def Mempty_def)
   126   done
   127 
   128 theorem union_commute: "M + N = N + (M::'a multiset)"
   129   apply (simp add: union_def add_ac)
   130   done
   131 
   132 theorem union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
   133   apply (simp add: union_def add_ac)
   134   done
   135 
   136 theorem union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
   137   apply (rule union_commute [THEN trans])
   138   apply (rule union_assoc [THEN trans])
   139   apply (rule union_commute [THEN arg_cong])
   140   done
   141 
   142 theorems union_ac = union_assoc union_commute union_lcomm
   143 
   144 
   145 subsubsection {* Difference *}
   146 
   147 theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
   148   apply (simp add: Mempty_def diff_def)
   149   done
   150 
   151 theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
   152   apply (simp add: union_def diff_def)
   153   done
   154 
   155 
   156 subsubsection {* Count of elements *}
   157 
   158 theorem count_empty [simp]: "count {#} a = 0"
   159   apply (simp add: count_def Mempty_def)
   160   done
   161 
   162 theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
   163   apply (simp add: count_def single_def)
   164   done
   165 
   166 theorem count_union [simp]: "count (M + N) a = count M a + count N a"
   167   apply (simp add: count_def union_def)
   168   done
   169 
   170 theorem count_diff [simp]: "count (M - N) a = count M a - count N a"
   171   apply (simp add: count_def diff_def)
   172   done
   173 
   174 
   175 subsubsection {* Set of elements *}
   176 
   177 theorem set_of_empty [simp]: "set_of {#} = {}"
   178   apply (simp add: set_of_def)
   179   done
   180 
   181 theorem set_of_single [simp]: "set_of {#b#} = {b}"
   182   apply (simp add: set_of_def)
   183   done
   184 
   185 theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
   186   apply (auto simp add: set_of_def)
   187   done
   188 
   189 theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
   190   apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
   191   done
   192 
   193 theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
   194   apply (auto simp add: set_of_def)
   195   done
   196 
   197 
   198 subsubsection {* Size *}
   199 
   200 theorem size_empty [simp]: "size {#} = 0"
   201   apply (simp add: size_def)
   202   done
   203 
   204 theorem size_single [simp]: "size {#b#} = 1"
   205   apply (simp add: size_def)
   206   done
   207 
   208 theorem finite_set_of [iff]: "finite (set_of M)"
   209   apply (cut_tac x = M in Rep_multiset)
   210   apply (simp add: multiset_def set_of_def count_def)
   211   done
   212 
   213 theorem setsum_count_Int:
   214     "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
   215   apply (erule finite_induct)
   216    apply simp
   217   apply (simp add: Int_insert_left set_of_def)
   218   done
   219 
   220 theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N"
   221   apply (unfold size_def)
   222   apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
   223    prefer 2
   224    apply (rule ext)
   225    apply simp
   226   apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int)
   227   apply (subst Int_commute)
   228   apply (simp (no_asm_simp) add: setsum_count_Int)
   229   done
   230 
   231 theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
   232   apply (unfold size_def Mempty_def count_def)
   233   apply auto
   234   apply (simp add: set_of_def count_def expand_fun_eq)
   235   done
   236 
   237 theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
   238   apply (unfold size_def)
   239   apply (drule setsum_SucD)
   240   apply auto
   241   done
   242 
   243 
   244 subsubsection {* Equality of multisets *}
   245 
   246 theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
   247   apply (simp add: count_def expand_fun_eq)
   248   done
   249 
   250 theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   251   apply (simp add: single_def Mempty_def expand_fun_eq)
   252   done
   253 
   254 theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
   255   apply (auto simp add: single_def expand_fun_eq)
   256   done
   257 
   258 theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
   259   apply (auto simp add: union_def Mempty_def expand_fun_eq)
   260   done
   261 
   262 theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
   263   apply (auto simp add: union_def Mempty_def expand_fun_eq)
   264   done
   265 
   266 theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
   267   apply (simp add: union_def expand_fun_eq)
   268   done
   269 
   270 theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
   271   apply (simp add: union_def expand_fun_eq)
   272   done
   273 
   274 theorem union_is_single:
   275     "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
   276   apply (unfold Mempty_def single_def union_def)
   277   apply (simp add: add_is_1 expand_fun_eq)
   278   apply blast
   279   done
   280 
   281 theorem single_is_union:
   282   "({#a#} = M + N) =
   283     ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   284   apply (unfold Mempty_def single_def union_def)
   285   apply (simp add: one_is_add expand_fun_eq)
   286   apply (blast dest: sym)
   287   done
   288 
   289 theorem add_eq_conv_diff:
   290   "(M + {#a#} = N + {#b#}) =
   291     (M = N \<and> a = b \<or>
   292       M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   293   apply (unfold single_def union_def diff_def)
   294   apply (simp (no_asm) add: expand_fun_eq)
   295   apply (rule conjI)
   296    apply force
   297   apply clarify
   298   apply (rule conjI)
   299    apply blast
   300   apply clarify
   301   apply (rule iffI)
   302    apply (rule conjI)
   303     apply clarify
   304     apply (rule conjI)
   305      apply (simp add: eq_sym_conv)   (* FIXME blast fails !? *)
   306     apply fast
   307    apply simp
   308   apply force
   309   done
   310 
   311 (*
   312 val prems = Goal
   313  "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   314 by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")]
   315      measure_induct 1);
   316 by (Clarify_tac 1);
   317 by (resolve_tac prems 1);
   318  by (assume_tac 1);
   319 by (Clarify_tac 1);
   320 by (subgoal_tac "finite G" 1);
   321  by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   322 by (etac allE 1);
   323 by (etac impE 1);
   324  by (Blast_tac 2);
   325 by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   326 no_qed();
   327 val lemma = result();
   328 
   329 val prems = Goal
   330  "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
   331 by (rtac (lemma RS mp) 1);
   332 by (REPEAT(ares_tac prems 1));
   333 qed "finite_psubset_induct";
   334 
   335 Better: use wf_finite_psubset in WF_Rel
   336 *)
   337 
   338 
   339 subsection {* Induction over multisets *}
   340 
   341 lemma setsum_decr:
   342   "finite F ==> 0 < f a ==>
   343     setsum (f (a := f a - 1)) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
   344   apply (erule finite_induct)
   345    apply auto
   346   apply (drule_tac a = a in mk_disjoint_insert)
   347   apply auto
   348   done
   349 
   350 lemma Rep_multiset_induct_aux:
   351   "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1)))
   352     ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
   353 proof -
   354   case antecedent
   355   note prems = this [unfolded multiset_def]
   356   show ?thesis
   357     apply (unfold multiset_def)
   358     apply (induct_tac n)
   359      apply simp
   360      apply clarify
   361      apply (subgoal_tac "f = (\<lambda>a.0)")
   362       apply simp
   363       apply (rule prems)
   364      apply (rule ext)
   365      apply force
   366     apply clarify
   367     apply (frule setsum_SucD)
   368     apply clarify
   369     apply (rename_tac a)
   370     apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
   371      prefer 2
   372      apply (rule finite_subset)
   373       prefer 2
   374       apply assumption
   375      apply simp
   376      apply blast
   377     apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
   378      prefer 2
   379      apply (rule ext)
   380      apply (simp (no_asm_simp))
   381      apply (erule ssubst, rule prems)
   382      apply blast
   383     apply (erule allE, erule impE, erule_tac [2] mp)
   384      apply blast
   385     apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply)
   386     apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
   387      prefer 2
   388      apply blast
   389     apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
   390      prefer 2
   391      apply blast
   392     apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong)
   393     done
   394 qed
   395 
   396 theorem Rep_multiset_induct:
   397   "f \<in> multiset ==> P (\<lambda>a. 0) ==>
   398     (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
   399   apply (insert Rep_multiset_induct_aux)
   400   apply blast
   401   done
   402 
   403 theorem multiset_induct [induct type: multiset]:
   404   "P {#} ==> (!!M x. P M ==> P (M + {#x#})) ==> P M"
   405 proof -
   406   note defns = union_def single_def Mempty_def
   407   assume prem1 [unfolded defns]: "P {#}"
   408   assume prem2 [unfolded defns]: "!!M x. P M ==> P (M + {#x#})"
   409   show ?thesis
   410     apply (rule Rep_multiset_inverse [THEN subst])
   411     apply (rule Rep_multiset [THEN Rep_multiset_induct])
   412      apply (rule prem1)
   413     apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))")
   414      prefer 2
   415      apply (simp add: expand_fun_eq)
   416     apply (erule ssubst)
   417     apply (erule Abs_multiset_inverse [THEN subst])
   418     apply (erule prem2 [simplified])
   419     done
   420 qed
   421 
   422 
   423 lemma MCollect_preserves_multiset:
   424     "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
   425   apply (simp add: multiset_def)
   426   apply (rule finite_subset)
   427    apply auto
   428   done
   429 
   430 theorem count_MCollect [simp]:
   431     "count {# x:M. P x #} a = (if P a then count M a else 0)"
   432   apply (unfold count_def MCollect_def)
   433   apply (simp add: MCollect_preserves_multiset)
   434   done
   435 
   436 theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
   437   apply (auto simp add: set_of_def)
   438   done
   439 
   440 theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
   441   apply (subst multiset_eq_conv_count_eq)
   442   apply auto
   443   done
   444 
   445 declare multiset_eq_conv_Rep_eq [simp del]
   446 declare multiset_typedef [simp del]
   447 
   448 theorem add_eq_conv_ex:
   449   "(M + {#a#} = N + {#b#}) =
   450     (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   451   apply (auto simp add: add_eq_conv_diff)
   452   done
   453 
   454 
   455 subsection {* Multiset orderings *}
   456 
   457 subsubsection {* Well-foundedness *}
   458 
   459 constdefs
   460   mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
   461   "mult1 r ==
   462     {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   463       (\<forall>b. b :# K --> (b, a) \<in> r)}"
   464 
   465   mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
   466   "mult r == (mult1 r)^+"
   467 
   468 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   469   apply (simp add: mult1_def)
   470   done
   471 
   472 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
   473     (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
   474     (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
   475   (concl is "?case1 (mult1 r) \<or> ?case2")
   476 proof (unfold mult1_def)
   477   let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
   478   let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
   479   let ?case1 = "?case1 {(N, M). ?R N M}"
   480 
   481   assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
   482   hence "\<exists>a' M0' K.
   483       M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp
   484   thus "?case1 \<or> ?case2"
   485   proof (elim exE conjE)
   486     fix a' M0' K
   487     assume N: "N = M0' + K" and r: "?r K a'"
   488     assume "M0 + {#a#} = M0' + {#a'#}"
   489     hence "M0 = M0' \<and> a = a' \<or>
   490         (\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})"
   491       by (simp only: add_eq_conv_ex)
   492     thus ?thesis
   493     proof (elim disjE conjE exE)
   494       assume "M0 = M0'" "a = a'"
   495       with N r have "?r K a \<and> N = M0 + K" by simp
   496       hence ?case2 .. thus ?thesis ..
   497     next
   498       fix K'
   499       assume "M0' = K' + {#a#}"
   500       with N have n: "N = K' + K + {#a#}" by (simp add: union_ac)
   501 
   502       assume "M0 = K' + {#a'#}"
   503       with r have "?R (K' + K) M0" by blast
   504       with n have ?case1 by simp thus ?thesis ..
   505     qed
   506   qed
   507 qed
   508 
   509 lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
   510 proof
   511   let ?R = "mult1 r"
   512   let ?W = "acc ?R"
   513   {
   514     fix M M0 a
   515     assume M0: "M0 \<in> ?W"
   516       and wf_hyp: "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
   517       and acc_hyp: "\<forall>M. (M, M0) \<in> ?R --> M + {#a#} \<in> ?W"
   518     have "M0 + {#a#} \<in> ?W"
   519     proof (rule accI [of "M0 + {#a#}"])
   520       fix N
   521       assume "(N, M0 + {#a#}) \<in> ?R"
   522       hence "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
   523           (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K))"
   524         by (rule less_add)
   525       thus "N \<in> ?W"
   526       proof (elim exE disjE conjE)
   527         fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
   528         from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
   529         hence "M + {#a#} \<in> ?W" ..
   530         thus "N \<in> ?W" by (simp only: N)
   531       next
   532         fix K
   533         assume N: "N = M0 + K"
   534         assume "\<forall>b. b :# K --> (b, a) \<in> r"
   535         have "?this --> M0 + K \<in> ?W" (is "?P K")
   536         proof (induct K)
   537           from M0 have "M0 + {#} \<in> ?W" by simp
   538           thus "?P {#}" ..
   539 
   540           fix K x assume hyp: "?P K"
   541           show "?P (K + {#x#})"
   542           proof
   543             assume a: "\<forall>b. b :# (K + {#x#}) --> (b, a) \<in> r"
   544             hence "(x, a) \<in> r" by simp
   545             with wf_hyp have b: "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
   546 
   547             from a hyp have "M0 + K \<in> ?W" by simp
   548             with b have "(M0 + K) + {#x#} \<in> ?W" ..
   549             thus "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
   550           qed
   551         qed
   552         hence "M0 + K \<in> ?W" ..
   553         thus "N \<in> ?W" by (simp only: N)
   554       qed
   555     qed
   556   } note tedious_reasoning = this
   557 
   558   assume wf: "wf r"
   559   fix M
   560   show "M \<in> ?W"
   561   proof (induct M)
   562     show "{#} \<in> ?W"
   563     proof (rule accI)
   564       fix b assume "(b, {#}) \<in> ?R"
   565       with not_less_empty show "b \<in> ?W" by contradiction
   566     qed
   567 
   568     fix M a assume "M \<in> ?W"
   569     from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
   570     proof induct
   571       fix a
   572       assume "\<forall>b. (b, a) \<in> r --> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
   573       show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
   574       proof
   575         fix M assume "M \<in> ?W"
   576         thus "M + {#a#} \<in> ?W"
   577           by (rule acc_induct) (rule tedious_reasoning)
   578       qed
   579     qed
   580     thus "M + {#a#} \<in> ?W" ..
   581   qed
   582 qed
   583 
   584 theorem wf_mult1: "wf r ==> wf (mult1 r)"
   585   by (rule acc_wfI, rule all_accessible)
   586 
   587 theorem wf_mult: "wf r ==> wf (mult r)"
   588   by (unfold mult_def, rule wf_trancl, rule wf_mult1)
   589 
   590 
   591 subsubsection {* Closure-free presentation *}
   592 
   593 (*Badly needed: a linear arithmetic procedure for multisets*)
   594 
   595 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
   596   apply (simp add: multiset_eq_conv_count_eq)
   597   done
   598 
   599 text {* One direction. *}
   600 
   601 lemma mult_implies_one_step:
   602   "trans r ==> (M, N) \<in> mult r ==>
   603     \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
   604     (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   605   apply (unfold mult_def mult1_def set_of_def)
   606   apply (erule converse_trancl_induct)
   607   apply clarify
   608    apply (rule_tac x = M0 in exI)
   609    apply simp
   610   apply clarify
   611   apply (case_tac "a :# K")
   612    apply (rule_tac x = I in exI)
   613    apply (simp (no_asm))
   614    apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
   615    apply (simp (no_asm_simp) add: union_assoc [symmetric])
   616    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
   617    apply (simp add: diff_union_single_conv)
   618    apply (simp (no_asm_use) add: trans_def)
   619    apply blast
   620   apply (subgoal_tac "a :# I")
   621    apply (rule_tac x = "I - {#a#}" in exI)
   622    apply (rule_tac x = "J + {#a#}" in exI)
   623    apply (rule_tac x = "K + Ka" in exI)
   624    apply (rule conjI)
   625     apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   626    apply (rule conjI)
   627     apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
   628     apply simp
   629     apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   630    apply (simp (no_asm_use) add: trans_def)
   631    apply blast
   632   apply (subgoal_tac "a :# (M0 +{#a#})")
   633    apply simp
   634   apply (simp (no_asm))
   635   done
   636 
   637 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
   638   apply (simp add: multiset_eq_conv_count_eq)
   639   done
   640 
   641 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
   642   apply (erule size_eq_Suc_imp_elem [THEN exE])
   643   apply (drule elem_imp_eq_diff_union)
   644   apply auto
   645   done
   646 
   647 lemma one_step_implies_mult_aux:
   648   "trans r ==>
   649     \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
   650       --> (I + K, I + J) \<in> mult r"
   651   apply (induct_tac n)
   652    apply auto
   653   apply (frule size_eq_Suc_imp_eq_union)
   654   apply clarify
   655   apply (rename_tac "J'")
   656   apply simp
   657   apply (erule notE)
   658    apply auto
   659   apply (case_tac "J' = {#}")
   660    apply (simp add: mult_def)
   661    apply (rule r_into_trancl)
   662    apply (simp add: mult1_def set_of_def)
   663    apply blast
   664   txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   665   apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   666   apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   667   apply (erule ssubst)
   668   apply (simp add: Ball_def)
   669   apply auto
   670   apply (subgoal_tac
   671     "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
   672       (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
   673    prefer 2
   674    apply force
   675   apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
   676   apply (erule trancl_trans)
   677   apply (rule r_into_trancl)
   678   apply (simp add: mult1_def set_of_def)
   679   apply (rule_tac x = a in exI)
   680   apply (rule_tac x = "I + J'" in exI)
   681   apply (simp add: union_ac)
   682   done
   683 
   684 theorem one_step_implies_mult:
   685   "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
   686     ==> (I + K, I + J) \<in> mult r"
   687   apply (insert one_step_implies_mult_aux)
   688   apply blast
   689   done
   690 
   691 
   692 subsubsection {* Partial-order properties *}
   693 
   694 instance multiset :: ("term") ord by intro_classes
   695 
   696 defs (overloaded)
   697   less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
   698   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
   699 
   700 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
   701   apply (unfold trans_def)
   702   apply (blast intro: order_less_trans)
   703   done
   704 
   705 text {*
   706  \medskip Irreflexivity.
   707 *}
   708 
   709 lemma mult_irrefl_aux:
   710     "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) --> A = {}"
   711   apply (erule finite_induct)
   712    apply (auto intro: order_less_trans)
   713   done
   714 
   715 theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
   716   apply (unfold less_multiset_def)
   717   apply auto
   718   apply (drule trans_base_order [THEN mult_implies_one_step])
   719   apply auto
   720   apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
   721   apply (simp add: set_of_eq_empty_iff)
   722   done
   723 
   724 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   725   apply (insert mult_less_not_refl)
   726   apply blast
   727   done
   728 
   729 
   730 text {* Transitivity. *}
   731 
   732 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
   733   apply (unfold less_multiset_def mult_def)
   734   apply (blast intro: trancl_trans)
   735   done
   736 
   737 text {* Asymmetry. *}
   738 
   739 theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
   740   apply auto
   741   apply (rule mult_less_not_refl [THEN notE])
   742   apply (erule mult_less_trans)
   743   apply assumption
   744   done
   745 
   746 theorem mult_less_asym:
   747     "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
   748   apply (insert mult_less_not_sym)
   749   apply blast
   750   done
   751 
   752 theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
   753   apply (unfold le_multiset_def)
   754   apply auto
   755   done
   756 
   757 text {* Anti-symmetry. *}
   758 
   759 theorem mult_le_antisym:
   760     "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
   761   apply (unfold le_multiset_def)
   762   apply (blast dest: mult_less_not_sym)
   763   done
   764 
   765 text {* Transitivity. *}
   766 
   767 theorem mult_le_trans:
   768     "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
   769   apply (unfold le_multiset_def)
   770   apply (blast intro: mult_less_trans)
   771   done
   772 
   773 theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   774   apply (unfold le_multiset_def)
   775   apply auto
   776   done
   777 
   778 
   779 subsubsection {* Monotonicity of multiset union *}
   780 
   781 theorem mult1_union:
   782     "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
   783   apply (unfold mult1_def)
   784   apply auto
   785   apply (rule_tac x = a in exI)
   786   apply (rule_tac x = "C + M0" in exI)
   787   apply (simp add: union_assoc)
   788   done
   789 
   790 lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
   791   apply (unfold less_multiset_def mult_def)
   792   apply (erule trancl_induct)
   793    apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
   794   apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
   795   done
   796 
   797 lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
   798   apply (subst union_commute [of B C])
   799   apply (subst union_commute [of D C])
   800   apply (erule union_less_mono2)
   801   done
   802 
   803 theorem union_less_mono:
   804     "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
   805   apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
   806   done
   807 
   808 theorem union_le_mono:
   809     "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
   810   apply (unfold le_multiset_def)
   811   apply (blast intro: union_less_mono union_less_mono1 union_less_mono2)
   812   done
   813 
   814 theorem empty_leI [iff]: "{#} <= (M::'a::order multiset)"
   815   apply (unfold le_multiset_def less_multiset_def)
   816   apply (case_tac "M = {#}")
   817    prefer 2
   818    apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
   819     prefer 2
   820     apply (rule one_step_implies_mult)
   821       apply (simp only: trans_def)
   822       apply auto
   823   apply (blast intro: order_less_trans)
   824   done
   825 
   826 theorem union_upper1: "A <= A + (B::'a::order multiset)"
   827   apply (subgoal_tac "A + {#} <= A + B")
   828    prefer 2
   829    apply (rule union_le_mono)
   830     apply auto
   831   done
   832 
   833 theorem union_upper2: "B <= A + (B::'a::order multiset)"
   834   apply (subst union_commute, rule union_upper1)
   835   done
   836 
   837 instance multiset :: (order) order
   838   apply intro_classes
   839      apply (rule mult_le_refl)
   840     apply (erule mult_le_trans)
   841     apply assumption
   842    apply (erule mult_le_antisym)
   843    apply assumption
   844   apply (rule mult_less_le)
   845   done
   846 
   847 instance multiset :: ("term") plus_ac0
   848   apply intro_classes
   849     apply (rule union_commute)
   850    apply (rule union_assoc)
   851   apply simp
   852   done
   853 
   854 end