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