1.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 28 09:21:35 2005 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 28 12:02:49 2005 +0200
     1.3 @@ -52,6 +52,10 @@
     1.4    Zero_multiset_def [simp]: "0 == {#}"
     1.5    size_def: "size M == setsum (count M) (set_of M)"
     1.6  
     1.7 +constdefs 
     1.8 + multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
     1.9 + "multiset_inter A B \<equiv> A - (A - B)"
    1.10 +
    1.11  
    1.12  text {*
    1.13   \medskip Preservation of the representing set @{term multiset}.
    1.14 @@ -264,6 +268,37 @@
    1.15  Better: use wf_finite_psubset in WF_Rel
    1.16  *)
    1.17  
    1.18 +declare Rep_multiset_inject [symmetric, simp del]
    1.19 +
    1.20 +
    1.21 +subsubsection {* Intersection *}
    1.22 +
    1.23 +lemma multiset_inter_count:
    1.24 +  "count (A #\<inter> B) x = min (count A x) (count B x)"
    1.25 +  by (simp add:multiset_inter_def min_def)
    1.26 +
    1.27 +lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
    1.28 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
    1.29 +                min_max.below_inf.inf_commute)
    1.30 +
    1.31 +lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
    1.32 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
    1.33 +                min_max.below_inf.inf_assoc)
    1.34 +
    1.35 +lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
    1.36 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
    1.37 +
    1.38 +lemmas multiset_inter_ac = multiset_inter_commute multiset_inter_assoc
    1.39 +                           multiset_inter_left_commute
    1.40 +
    1.41 +lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
    1.42 +  apply (simp add:multiset_eq_conv_count_eq multiset_inter_count min_def 
    1.43 +              split:split_if_asm)
    1.44 +  apply clarsimp
    1.45 +  apply (erule_tac x="a" in allE)
    1.46 +  apply auto
    1.47 +  done
    1.48 +
    1.49  
    1.50  subsection {* Induction over multisets *}
    1.51  
    1.52 @@ -332,7 +367,7 @@
    1.53       prefer 2
    1.54       apply (simp add: expand_fun_eq)
    1.55      apply (erule ssubst)
    1.56 -    apply (erule Abs_multiset_inverse [THEN subst])
    1.57 +    apply (erule Abs_multiset_inverse [THEN subst]) 
    1.58      apply (erule prem2 [simplified])
    1.59      done
    1.60  qed
    1.61 @@ -354,14 +389,12 @@
    1.62  theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
    1.63  by (subst multiset_eq_conv_count_eq, auto)
    1.64  
    1.65 -declare Rep_multiset_inject [symmetric, simp del]
    1.66 -declare multiset_typedef [simp del]
    1.67 -
    1.68  theorem add_eq_conv_ex:
    1.69        "(M + {#a#} = N + {#b#}) =
    1.70         (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
    1.71    by (auto simp add: add_eq_conv_diff)
    1.72  
    1.73 +declare multiset_typedef [simp del]
    1.74  
    1.75  subsection {* Multiset orderings *}
    1.76