src/HOL/Library/Multiset.thy
changeset 15072 4861bf6af0b4
parent 14981 e73f8140af78
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Jul 21 16:35:38 2004 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jul 22 10:33:26 2004 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Library/Multiset.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson
     1.7 +    Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
     1.8  *)
     1.9  
    1.10  header {* Multisets *}
    1.11 @@ -56,26 +56,21 @@
    1.12  *}
    1.13  
    1.14  lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
    1.15 -  apply (simp add: multiset_def)
    1.16 -  done
    1.17 +by (simp add: multiset_def)
    1.18  
    1.19  lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
    1.20 -  apply (simp add: multiset_def)
    1.21 -  done
    1.22 +by (simp add: multiset_def)
    1.23  
    1.24  lemma union_preserves_multiset [simp]:
    1.25      "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
    1.26 -  apply (unfold multiset_def)
    1.27 -  apply simp
    1.28 -  apply (drule finite_UnI)
    1.29 -   apply assumption
    1.30 +  apply (unfold multiset_def, simp)
    1.31 +  apply (drule finite_UnI, assumption)
    1.32    apply (simp del: finite_Un add: Un_def)
    1.33    done
    1.34  
    1.35  lemma diff_preserves_multiset [simp]:
    1.36      "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
    1.37 -  apply (unfold multiset_def)
    1.38 -  apply simp
    1.39 +  apply (unfold multiset_def, simp)
    1.40    apply (rule finite_subset)
    1.41     prefer 2
    1.42     apply assumption
    1.43 @@ -88,16 +83,13 @@
    1.44  subsubsection {* Union *}
    1.45  
    1.46  theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
    1.47 -  apply (simp add: union_def Mempty_def)
    1.48 -  done
    1.49 +by (simp add: union_def Mempty_def)
    1.50  
    1.51  theorem union_commute: "M + N = N + (M::'a multiset)"
    1.52 -  apply (simp add: union_def add_ac)
    1.53 -  done
    1.54 +by (simp add: union_def add_ac)
    1.55  
    1.56  theorem union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
    1.57 -  apply (simp add: union_def add_ac)
    1.58 -  done
    1.59 +by (simp add: union_def add_ac)
    1.60  
    1.61  theorem union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
    1.62    apply (rule union_commute [THEN trans])
    1.63 @@ -119,65 +111,52 @@
    1.64  subsubsection {* Difference *}
    1.65  
    1.66  theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
    1.67 -  apply (simp add: Mempty_def diff_def)
    1.68 -  done
    1.69 +by (simp add: Mempty_def diff_def)
    1.70  
    1.71  theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
    1.72 -  apply (simp add: union_def diff_def)
    1.73 -  done
    1.74 +by (simp add: union_def diff_def)
    1.75  
    1.76  
    1.77  subsubsection {* Count of elements *}
    1.78  
    1.79  theorem count_empty [simp]: "count {#} a = 0"
    1.80 -  apply (simp add: count_def Mempty_def)
    1.81 -  done
    1.82 +by (simp add: count_def Mempty_def)
    1.83  
    1.84  theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    1.85 -  apply (simp add: count_def single_def)
    1.86 -  done
    1.87 +by (simp add: count_def single_def)
    1.88  
    1.89  theorem count_union [simp]: "count (M + N) a = count M a + count N a"
    1.90 -  apply (simp add: count_def union_def)
    1.91 -  done
    1.92 +by (simp add: count_def union_def)
    1.93  
    1.94  theorem count_diff [simp]: "count (M - N) a = count M a - count N a"
    1.95 -  apply (simp add: count_def diff_def)
    1.96 -  done
    1.97 +by (simp add: count_def diff_def)
    1.98  
    1.99  
   1.100  subsubsection {* Set of elements *}
   1.101  
   1.102  theorem set_of_empty [simp]: "set_of {#} = {}"
   1.103 -  apply (simp add: set_of_def)
   1.104 -  done
   1.105 +by (simp add: set_of_def)
   1.106  
   1.107  theorem set_of_single [simp]: "set_of {#b#} = {b}"
   1.108 -  apply (simp add: set_of_def)
   1.109 -  done
   1.110 +by (simp add: set_of_def)
   1.111  
   1.112  theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
   1.113 -  apply (auto simp add: set_of_def)
   1.114 -  done
   1.115 +by (auto simp add: set_of_def)
   1.116  
   1.117  theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
   1.118 -  apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
   1.119 -  done
   1.120 +by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
   1.121  
   1.122  theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
   1.123 -  apply (auto simp add: set_of_def)
   1.124 -  done
   1.125 +by (auto simp add: set_of_def)
   1.126  
   1.127  
   1.128  subsubsection {* Size *}
   1.129  
   1.130  theorem size_empty [simp]: "size {#} = 0"
   1.131 -  apply (simp add: size_def)
   1.132 -  done
   1.133 +by (simp add: size_def)
   1.134  
   1.135  theorem size_single [simp]: "size {#b#} = 1"
   1.136 -  apply (simp add: size_def)
   1.137 -  done
   1.138 +by (simp add: size_def)
   1.139  
   1.140  theorem finite_set_of [iff]: "finite (set_of M)"
   1.141    apply (cut_tac x = M in Rep_multiset)
   1.142 @@ -186,8 +165,7 @@
   1.143  
   1.144  theorem setsum_count_Int:
   1.145      "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
   1.146 -  apply (erule finite_induct)
   1.147 -   apply simp
   1.148 +  apply (erule finite_induct, simp)
   1.149    apply (simp add: Int_insert_left set_of_def)
   1.150    done
   1.151  
   1.152 @@ -195,66 +173,54 @@
   1.153    apply (unfold size_def)
   1.154    apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
   1.155     prefer 2
   1.156 -   apply (rule ext)
   1.157 -   apply simp
   1.158 +   apply (rule ext, simp)
   1.159    apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int)
   1.160    apply (subst Int_commute)
   1.161    apply (simp (no_asm_simp) add: setsum_count_Int)
   1.162    done
   1.163  
   1.164  theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
   1.165 -  apply (unfold size_def Mempty_def count_def)
   1.166 -  apply auto
   1.167 +  apply (unfold size_def Mempty_def count_def, auto)
   1.168    apply (simp add: set_of_def count_def expand_fun_eq)
   1.169    done
   1.170  
   1.171  theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
   1.172    apply (unfold size_def)
   1.173 -  apply (drule setsum_SucD)
   1.174 -  apply auto
   1.175 +  apply (drule setsum_SucD, auto)
   1.176    done
   1.177  
   1.178  
   1.179  subsubsection {* Equality of multisets *}
   1.180  
   1.181  theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
   1.182 -  apply (simp add: count_def expand_fun_eq)
   1.183 -  done
   1.184 +by (simp add: count_def expand_fun_eq)
   1.185  
   1.186  theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   1.187 -  apply (simp add: single_def Mempty_def expand_fun_eq)
   1.188 -  done
   1.189 +by (simp add: single_def Mempty_def expand_fun_eq)
   1.190  
   1.191  theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
   1.192 -  apply (auto simp add: single_def expand_fun_eq)
   1.193 -  done
   1.194 +by (auto simp add: single_def expand_fun_eq)
   1.195  
   1.196  theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
   1.197 -  apply (auto simp add: union_def Mempty_def expand_fun_eq)
   1.198 -  done
   1.199 +by (auto simp add: union_def Mempty_def expand_fun_eq)
   1.200  
   1.201  theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
   1.202 -  apply (auto simp add: union_def Mempty_def expand_fun_eq)
   1.203 -  done
   1.204 +by (auto simp add: union_def Mempty_def expand_fun_eq)
   1.205  
   1.206  theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
   1.207 -  apply (simp add: union_def expand_fun_eq)
   1.208 -  done
   1.209 +by (simp add: union_def expand_fun_eq)
   1.210  
   1.211  theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
   1.212 -  apply (simp add: union_def expand_fun_eq)
   1.213 -  done
   1.214 +by (simp add: union_def expand_fun_eq)
   1.215  
   1.216  theorem union_is_single:
   1.217      "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
   1.218 -  apply (unfold Mempty_def single_def union_def)
   1.219 -  apply (simp add: add_is_1 expand_fun_eq)
   1.220 +  apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq)
   1.221    apply blast
   1.222    done
   1.223  
   1.224  theorem single_is_union:
   1.225 -  "({#a#} = M + N) =
   1.226 -    ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   1.227 +     "({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   1.228    apply (unfold Mempty_def single_def union_def)
   1.229    apply (simp add: add_is_1 one_is_add expand_fun_eq)
   1.230    apply (blast dest: sym)
   1.231 @@ -262,14 +228,10 @@
   1.232  
   1.233  theorem add_eq_conv_diff:
   1.234    "(M + {#a#} = N + {#b#}) =
   1.235 -    (M = N \<and> a = b \<or>
   1.236 -      M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   1.237 +   (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   1.238    apply (unfold single_def union_def diff_def)
   1.239    apply (simp (no_asm) add: expand_fun_eq)
   1.240 -  apply (rule conjI)
   1.241 -   apply force
   1.242 -  apply safe
   1.243 -  apply simp_all
   1.244 +  apply (rule conjI, force, safe, simp_all)
   1.245    apply (simp add: eq_sym_conv)
   1.246    done
   1.247  
   1.248 @@ -278,15 +240,15 @@
   1.249   "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   1.250  by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")]
   1.251       measure_induct 1);
   1.252 -by (Clarify_tac 1);
   1.253 -by (resolve_tac prems 1);
   1.254 - by (assume_tac 1);
   1.255 -by (Clarify_tac 1);
   1.256 -by (subgoal_tac "finite G" 1);
   1.257 +by (Clarify_tac 1)
   1.258 +by (resolve_tac prems 1)
   1.259 + by (assume_tac 1)
   1.260 +by (Clarify_tac 1)
   1.261 +by (subgoal_tac "finite G" 1)
   1.262   by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   1.263 -by (etac allE 1);
   1.264 -by (etac impE 1);
   1.265 - by (Blast_tac 2);
   1.266 +by (etac allE 1)
   1.267 +by (etac impE 1)
   1.268 + by (Blast_tac 2)
   1.269  by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   1.270  no_qed();
   1.271  val lemma = result();
   1.272 @@ -305,11 +267,9 @@
   1.273  
   1.274  lemma setsum_decr:
   1.275    "finite F ==> (0::nat) < f a ==>
   1.276 -    setsum (f (a := f a - 1)) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
   1.277 -  apply (erule finite_induct)
   1.278 -   apply auto
   1.279 -  apply (drule_tac a = a in mk_disjoint_insert)
   1.280 -  apply auto
   1.281 +    setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
   1.282 +  apply (erule finite_induct, auto)
   1.283 +  apply (drule_tac a = a in mk_disjoint_insert, auto)
   1.284    done
   1.285  
   1.286  lemma rep_multiset_induct_aux:
   1.287 @@ -320,17 +280,12 @@
   1.288    note premises = this [unfolded multiset_def]
   1.289    show ?thesis
   1.290      apply (unfold multiset_def)
   1.291 -    apply (induct_tac n)
   1.292 -     apply simp
   1.293 -     apply clarify
   1.294 +    apply (induct_tac n, simp, clarify)
   1.295       apply (subgoal_tac "f = (\<lambda>a.0)")
   1.296        apply simp
   1.297        apply (rule premises)
   1.298 -     apply (rule ext)
   1.299 -     apply force
   1.300 -    apply clarify
   1.301 -    apply (frule setsum_SucD)
   1.302 -    apply clarify
   1.303 +     apply (rule ext, force, clarify)
   1.304 +    apply (frule setsum_SucD, clarify)
   1.305      apply (rename_tac a)
   1.306      apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
   1.307       prefer 2
   1.308 @@ -343,10 +298,8 @@
   1.309       prefer 2
   1.310       apply (rule ext)
   1.311       apply (simp (no_asm_simp))
   1.312 -     apply (erule ssubst, rule premises)
   1.313 -     apply blast
   1.314 -    apply (erule allE, erule impE, erule_tac [2] mp)
   1.315 -     apply blast
   1.316 +     apply (erule ssubst, rule premises, blast)
   1.317 +    apply (erule allE, erule impE, erule_tac [2] mp, blast)
   1.318      apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
   1.319      apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
   1.320       prefer 2
   1.321 @@ -361,9 +314,7 @@
   1.322  theorem rep_multiset_induct:
   1.323    "f \<in> multiset ==> P (\<lambda>a. 0) ==>
   1.324      (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
   1.325 -  apply (insert rep_multiset_induct_aux)
   1.326 -  apply blast
   1.327 -  done
   1.328 +  by (insert rep_multiset_induct_aux, blast)
   1.329  
   1.330  theorem multiset_induct [induct type: multiset]:
   1.331    "P {#} ==> (!!M x. P M ==> P (M + {#x#})) ==> P M"
   1.332 @@ -375,7 +326,7 @@
   1.333      apply (rule Rep_multiset_inverse [THEN subst])
   1.334      apply (rule Rep_multiset [THEN rep_multiset_induct])
   1.335       apply (rule prem1)
   1.336 -    apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))")
   1.337 +    apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
   1.338       prefer 2
   1.339       apply (simp add: expand_fun_eq)
   1.340      apply (erule ssubst)
   1.341 @@ -388,33 +339,26 @@
   1.342  lemma MCollect_preserves_multiset:
   1.343      "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
   1.344    apply (simp add: multiset_def)
   1.345 -  apply (rule finite_subset)
   1.346 -   apply auto
   1.347 +  apply (rule finite_subset, auto)
   1.348    done
   1.349  
   1.350  theorem count_MCollect [simp]:
   1.351      "count {# x:M. P x #} a = (if P a then count M a else 0)"
   1.352 -  apply (unfold count_def MCollect_def)
   1.353 -  apply (simp add: MCollect_preserves_multiset)
   1.354 -  done
   1.355 +  by (simp add: count_def MCollect_def MCollect_preserves_multiset)
   1.356  
   1.357  theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
   1.358 -  apply (auto simp add: set_of_def)
   1.359 -  done
   1.360 +by (auto simp add: set_of_def)
   1.361  
   1.362  theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
   1.363 -  apply (subst multiset_eq_conv_count_eq)
   1.364 -  apply auto
   1.365 -  done
   1.366 +by (subst multiset_eq_conv_count_eq, auto)
   1.367  
   1.368  declare Rep_multiset_inject [symmetric, simp del]
   1.369  declare multiset_typedef [simp del]
   1.370  
   1.371  theorem add_eq_conv_ex:
   1.372 -  "(M + {#a#} = N + {#b#}) =
   1.373 -    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.374 -  apply (auto simp add: add_eq_conv_diff)
   1.375 -  done
   1.376 +      "(M + {#a#} = N + {#b#}) =
   1.377 +       (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.378 +  by (auto simp add: add_eq_conv_diff)
   1.379  
   1.380  
   1.381  subsection {* Multiset orderings *}
   1.382 @@ -557,8 +501,7 @@
   1.383  (*Badly needed: a linear arithmetic procedure for multisets*)
   1.384  
   1.385  lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
   1.386 -  apply (simp add: multiset_eq_conv_count_eq)
   1.387 -  done
   1.388 +by (simp add: multiset_eq_conv_count_eq)
   1.389  
   1.390  text {* One direction. *}
   1.391  
   1.392 @@ -567,11 +510,8 @@
   1.393      \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
   1.394      (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   1.395    apply (unfold mult_def mult1_def set_of_def)
   1.396 -  apply (erule converse_trancl_induct)
   1.397 -  apply clarify
   1.398 -   apply (rule_tac x = M0 in exI)
   1.399 -   apply simp
   1.400 -  apply clarify
   1.401 +  apply (erule converse_trancl_induct, clarify)
   1.402 +   apply (rule_tac x = M0 in exI, simp, clarify)
   1.403    apply (case_tac "a :# K")
   1.404     apply (rule_tac x = I in exI)
   1.405     apply (simp (no_asm))
   1.406 @@ -588,8 +528,7 @@
   1.407     apply (rule conjI)
   1.408      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   1.409     apply (rule conjI)
   1.410 -    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
   1.411 -    apply simp
   1.412 +    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
   1.413      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   1.414     apply (simp (no_asm_use) add: trans_def)
   1.415     apply blast
   1.416 @@ -599,38 +538,30 @@
   1.417    done
   1.418  
   1.419  lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
   1.420 -  apply (simp add: multiset_eq_conv_count_eq)
   1.421 -  done
   1.422 +by (simp add: multiset_eq_conv_count_eq)
   1.423  
   1.424  lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
   1.425    apply (erule size_eq_Suc_imp_elem [THEN exE])
   1.426 -  apply (drule elem_imp_eq_diff_union)
   1.427 -  apply auto
   1.428 +  apply (drule elem_imp_eq_diff_union, auto)
   1.429    done
   1.430  
   1.431  lemma one_step_implies_mult_aux:
   1.432    "trans r ==>
   1.433      \<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))
   1.434        --> (I + K, I + J) \<in> mult r"
   1.435 -  apply (induct_tac n)
   1.436 -   apply auto
   1.437 -  apply (frule size_eq_Suc_imp_eq_union)
   1.438 -  apply clarify
   1.439 -  apply (rename_tac "J'")
   1.440 -  apply simp
   1.441 -  apply (erule notE)
   1.442 -   apply auto
   1.443 +  apply (induct_tac n, auto)
   1.444 +  apply (frule size_eq_Suc_imp_eq_union, clarify)
   1.445 +  apply (rename_tac "J'", simp)
   1.446 +  apply (erule notE, auto)
   1.447    apply (case_tac "J' = {#}")
   1.448     apply (simp add: mult_def)
   1.449     apply (rule r_into_trancl)
   1.450 -   apply (simp add: mult1_def set_of_def)
   1.451 -   apply blast
   1.452 +   apply (simp add: mult1_def set_of_def, blast)
   1.453    txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   1.454    apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   1.455    apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   1.456    apply (erule ssubst)
   1.457 -  apply (simp add: Ball_def)
   1.458 -  apply auto
   1.459 +  apply (simp add: Ball_def, auto)
   1.460    apply (subgoal_tac
   1.461      "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
   1.462        (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
   1.463 @@ -648,8 +579,7 @@
   1.464  theorem one_step_implies_mult:
   1.465    "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
   1.466      ==> (I + K, I + J) \<in> mult r"
   1.467 -  apply (insert one_step_implies_mult_aux)
   1.468 -  apply blast
   1.469 +  apply (insert one_step_implies_mult_aux, blast)
   1.470    done
   1.471  
   1.472  
   1.473 @@ -677,18 +607,14 @@
   1.474    done
   1.475  
   1.476  theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
   1.477 -  apply (unfold less_multiset_def)
   1.478 -  apply auto
   1.479 -  apply (drule trans_base_order [THEN mult_implies_one_step])
   1.480 -  apply auto
   1.481 +  apply (unfold less_multiset_def, auto)
   1.482 +  apply (drule trans_base_order [THEN mult_implies_one_step], auto)
   1.483    apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
   1.484    apply (simp add: set_of_eq_empty_iff)
   1.485    done
   1.486  
   1.487  lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   1.488 -  apply (insert mult_less_not_refl)
   1.489 -  apply fast
   1.490 -  done
   1.491 +by (insert mult_less_not_refl, fast)
   1.492  
   1.493  
   1.494  text {* Transitivity. *}
   1.495 @@ -703,20 +629,15 @@
   1.496  theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
   1.497    apply auto
   1.498    apply (rule mult_less_not_refl [THEN notE])
   1.499 -  apply (erule mult_less_trans)
   1.500 -  apply assumption
   1.501 +  apply (erule mult_less_trans, assumption)
   1.502    done
   1.503  
   1.504  theorem mult_less_asym:
   1.505      "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
   1.506 -  apply (insert mult_less_not_sym)
   1.507 -  apply blast
   1.508 -  done
   1.509 +  by (insert mult_less_not_sym, blast)
   1.510  
   1.511  theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
   1.512 -  apply (unfold le_multiset_def)
   1.513 -  apply auto
   1.514 -  done
   1.515 +by (unfold le_multiset_def, auto)
   1.516  
   1.517  text {* Anti-symmetry. *}
   1.518  
   1.519 @@ -735,19 +656,15 @@
   1.520    done
   1.521  
   1.522  theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   1.523 -  apply (unfold le_multiset_def)
   1.524 -  apply auto
   1.525 -  done
   1.526 +by (unfold le_multiset_def, auto)
   1.527  
   1.528  text {* Partial order. *}
   1.529  
   1.530  instance multiset :: (order) order
   1.531    apply intro_classes
   1.532       apply (rule mult_le_refl)
   1.533 -    apply (erule mult_le_trans)
   1.534 -    apply assumption
   1.535 -   apply (erule mult_le_antisym)
   1.536 -   apply assumption
   1.537 +    apply (erule mult_le_trans, assumption)
   1.538 +   apply (erule mult_le_antisym, assumption)
   1.539    apply (rule mult_less_le)
   1.540    done
   1.541  
   1.542 @@ -756,8 +673,7 @@
   1.543  
   1.544  theorem mult1_union:
   1.545      "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
   1.546 -  apply (unfold mult1_def)
   1.547 -  apply auto
   1.548 +  apply (unfold mult1_def, auto)
   1.549    apply (rule_tac x = a in exI)
   1.550    apply (rule_tac x = "C + M0" in exI)
   1.551    apply (simp add: union_assoc)
   1.552 @@ -794,19 +710,123 @@
   1.553     apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
   1.554      prefer 2
   1.555      apply (rule one_step_implies_mult)
   1.556 -      apply (simp only: trans_def)
   1.557 -      apply auto
   1.558 +      apply (simp only: trans_def, auto)
   1.559    done
   1.560  
   1.561  theorem union_upper1: "A <= A + (B::'a::order multiset)"
   1.562 -  apply (subgoal_tac "A + {#} <= A + B")
   1.563 -   prefer 2
   1.564 -   apply (rule union_le_mono)
   1.565 -    apply auto
   1.566 +proof -
   1.567 +  have "A + {#} <= A + B" by (blast intro: union_le_mono) 
   1.568 +  thus ?thesis by simp
   1.569 +qed
   1.570 +
   1.571 +theorem union_upper2: "B <= A + (B::'a::order multiset)"
   1.572 +by (subst union_commute, rule union_upper1)
   1.573 +
   1.574 +
   1.575 +subsection {* Link with lists *} 
   1.576 +
   1.577 +consts 
   1.578 +  multiset_of :: "'a list \<Rightarrow> 'a multiset"
   1.579 +primrec
   1.580 +  "multiset_of [] = {#}"
   1.581 +  "multiset_of (a # x) = multiset_of x + {# a #}"
   1.582 +
   1.583 +lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
   1.584 +  by (induct_tac x, auto) 
   1.585 +
   1.586 +lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   1.587 +  by (induct_tac x, auto)
   1.588 +
   1.589 +lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
   1.590 + by (induct_tac x, auto) 
   1.591 +
   1.592 +lemma multset_of_append[simp]: 
   1.593 +  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   1.594 +  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
   1.595 +
   1.596 +lemma surj_multiset_of: "surj multiset_of"
   1.597 +  apply (unfold surj_def, rule allI) 
   1.598 +  apply (rule_tac M=y in multiset_induct, auto) 
   1.599 +  apply (rule_tac x = "x # xa" in exI, auto) 
   1.600    done
   1.601  
   1.602 -theorem union_upper2: "B <= A + (B::'a::order multiset)"
   1.603 -  apply (subst union_commute, rule union_upper1)
   1.604 +lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
   1.605 +  by (induct_tac x, auto)  
   1.606 +
   1.607 +lemma distinct_count_atmost_1: 
   1.608 +   "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
   1.609 +   apply ( induct_tac x, simp, rule iffI, simp_all)
   1.610 +   apply (rule conjI)  
   1.611 +   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
   1.612 +   apply (erule_tac x=a in allE, simp, clarify)
   1.613 +   apply (erule_tac x=aa in allE, simp) 
   1.614 +   done
   1.615 +
   1.616 +lemma set_eq_iff_multiset_of_eq_distinct: 
   1.617 +  "\<lbrakk>distinct x; distinct y\<rbrakk> 
   1.618 +   \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
   1.619 +  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
   1.620 +
   1.621 +lemma set_eq_iff_multiset_of_remdups_eq: 
   1.622 +   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   1.623 +  apply (rule iffI) 
   1.624 +  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
   1.625 +  apply (drule distinct_remdups[THEN distinct_remdups 
   1.626 +                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
   1.627 +  apply simp
   1.628    done
   1.629  
   1.630 +
   1.631 +subsection {* Pointwise ordering induced by count *}
   1.632 +
   1.633 +consts 
   1.634 +  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
   1.635 +
   1.636 +syntax 
   1.637 +  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50) 
   1.638 +translations 
   1.639 +  "x \<le># y" == "mset_le x y"
   1.640 +
   1.641 +defs 
   1.642 +  mset_le_def:   "xs \<le># ys  == (! a. count xs a \<le> count ys a)"
   1.643 +
   1.644 +lemma mset_le_refl[simp]: "xs \<le># xs"
   1.645 +  by (unfold mset_le_def, auto) 
   1.646 +
   1.647 +lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
   1.648 +  by (unfold mset_le_def, fast intro: order_trans) 
   1.649 +
   1.650 +lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
   1.651 +  apply (unfold mset_le_def) 
   1.652 +  apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 
   1.653 +  apply (blast intro: order_antisym)
   1.654 +  done
   1.655 +
   1.656 +lemma mset_le_exists_conv: 
   1.657 +  "(xs \<le># ys) = (? zs. ys = xs + zs)"
   1.658 +  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) 
   1.659 +  apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   1.660 +  done
   1.661 +
   1.662 +lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
   1.663 +  by (unfold mset_le_def, auto) 
   1.664 +
   1.665 +lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
   1.666 +  by (unfold mset_le_def, auto) 
   1.667 +
   1.668 +lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
   1.669 +  apply (unfold mset_le_def, auto) 
   1.670 +  apply (erule_tac x=a in allE)+
   1.671 +  apply auto
   1.672 +  done
   1.673 +
   1.674 +lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
   1.675 +  by (unfold mset_le_def, auto) 
   1.676 +
   1.677 +lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
   1.678 +  by (unfold mset_le_def, auto)
   1.679 +
   1.680 +lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
   1.681 +  by (induct_tac x, auto, rule mset_le_trans, auto)
   1.682 +
   1.683  end