Many new theorems about multisets and their ordering, including basic
laws like {#} <= M. Renamed union_comm to union_commute. Introduced the
collection operator {# x:M. P x #}.

--- a/src/HOL/Induct/Multiset.ML	Fri Jun 02 15:19:18 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Fri Jun 02 17:42:43 2000 +0200
@@ -46,6 +46,7 @@
 qed "multiset_eq_conv_Rep_eq";
 Addsimps [multiset_eq_conv_Rep_eq];
 Addsimps [expand_fun_eq];
+
 (*
 Goal
  "[| f : multiset; g : multiset |] ==> \
@@ -74,7 +75,7 @@
 Goalw [union_def]
  "(M::'a multiset) + N = N + M";
 by (simp_tac (simpset() addsimps add_ac) 1);
-qed "union_comm";
+qed "union_commute";
 
 Goalw [union_def]
  "((M::'a multiset)+N)+K = M+(N+K)";
@@ -82,10 +83,10 @@
 qed "union_assoc";
 
 qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
- (fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1,
-           rtac (union_comm RS arg_cong) 1]);
+ (fn _ => [rtac (union_commute RS trans) 1, rtac (union_assoc RS trans) 1,
+           rtac (union_commute RS arg_cong) 1]);
 
-bind_thms ("union_ac", [union_assoc, union_comm, union_lcomm]);
+bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]);
 
 (* diff *)
 
@@ -150,6 +151,10 @@
 by Auto_tac;
 qed "set_of_eq_empty_iff";
 
+Goalw [set_of_def] "(x : set_of M) = (x :# M)";
+by Auto_tac; 
+qed "mem_set_of_iff";
+
 (* size *)
 
 Goalw [size_def] "size {#} = 0";
@@ -186,6 +191,17 @@
 qed "size_union";
 Addsimps [size_union];
 
+Goalw [size_def, empty_def, count_def] "(size M = 0) = (M = {#})";
+by Auto_tac; 
+by (asm_full_simp_tac (simpset() addsimps [set_of_def, count_def]) 1); 
+qed "size_eq_0_iff_empty";
+AddIffs [size_eq_0_iff_empty];
+
+Goalw [size_def] "size M = Suc n ==> EX a. a :# M";
+by (dtac setsum_SucD 1);
+by Auto_tac; 
+qed "size_eq_Suc_imp_elem";
+
 
 (* equalities *)
 
@@ -290,6 +306,7 @@
 Better: use wf_finite_psubset in WF_Rel
 *)
 
+
 (** Towards the induction rule **)
 
 Goal "[| finite F; 0 < f a |] ==> \
@@ -362,6 +379,29 @@
 by (etac(simplify (simpset()) prem2)1);
 qed "multiset_induct";
 
+Goal "M : multiset ==> (%x. if P x then M x else 0) : multiset";
+by (asm_full_simp_tac (simpset() addsimps [multiset_def]) 1);
+by (rtac finite_subset 1);
+by Auto_tac; 
+qed "MCollect_preserves_multiset";
+
+Goalw [count_def,MCollect_def]
+ "count {# x:M. P x #} a = (if P a then count M a else 0)";
+by (asm_full_simp_tac (simpset() addsimps [MCollect_preserves_multiset]) 1); 
+qed "count_MCollect";
+Addsimps [count_MCollect];
+
+Goalw [set_of_def]
+ "set_of {# x:M. P x #} = set_of M Int {x. P x}";
+by Auto_tac; 
+qed "set_of_MCollect";
+Addsimps [set_of_MCollect];
+
+Goal "M = {# x:M. P x #} + {# x:M. ~ P x #}";
+by (stac multiset_eq_conv_count_eq 1);
+by Auto_tac; 
+qed "multiset_partition";
+
 Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
 Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
 
@@ -381,7 +421,7 @@
 Goalw [mult1_def]
  "(N,M0 + {#a#}) : mult1(r) = \
 \ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
-\  (? K. (!b. K :# b --> (b,a) : r) & N = M0 + K))";
+\  (? K. (!b. b :# K --> (b,a) : r) & N = M0 + K))";
 by (rtac iffI 1);
  by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
  by (Clarify_tac 1);
@@ -455,7 +495,7 @@
 
 (* Badly needed: a linear arithmetic tactic for multisets *)
 
-Goal "J :# a ==> I+J - {#a#} = I + (J-{#a#})";
+Goal "a :# J ==> I+J - {#a#} = I + (J-{#a#})";
 by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
 qed "diff_union_single_conv";
 
@@ -469,7 +509,7 @@
  by (res_inst_tac [("x","M0")] exI 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (case_tac "K :# a" 1);
+by (case_tac "a :# K" 1);
  by (res_inst_tac [("x","I")] exI 1);
  by (Simp_tac 1);
  by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
@@ -478,7 +518,7 @@
  by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
  by (full_simp_tac (simpset() addsimps [trans_def]) 1);
  by (Blast_tac 1);
-by (subgoal_tac "I :# a" 1);
+by (subgoal_tac "a :# I" 1);
  by (res_inst_tac [("x","I-{#a#}")] exI 1);
  by (res_inst_tac [("x","J+{#a#}")] exI 1);
  by (res_inst_tac [("x","K + Ka")] exI 1);
@@ -492,11 +532,64 @@
                              addsplits [nat_diff_split]) 1);
  by (full_simp_tac (simpset() addsimps [trans_def]) 1);
  by (Blast_tac 1);
-by (subgoal_tac "(M0 +{#a#}) :# a" 1);
+by (subgoal_tac "a :# (M0 +{#a#})" 1);
  by (Asm_full_simp_tac 1);
 by (Simp_tac 1);
 qed "mult_implies_one_step";
 
+Goal "a :# M ==> M = M - {#a#} + {#a#}";
+by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
+qed "elem_imp_eq_diff_union";
+
+Goal "size M = Suc n ==> EX a N. M = N + {#a#}";
+by (etac (size_eq_Suc_imp_elem RS exE) 1);
+by (dtac elem_imp_eq_diff_union 1); 
+by Auto_tac; 
+qed "size_eq_Suc_imp_eq_union";
+
+
+Goal  "trans r ==> \
+\ ALL I J K. \
+\  (size J = n & J ~= {#} & \
+\   (! k : set_of K. ? j : set_of J. (k,j) : r)) --> (I+K, I+J) : mult r";
+by (induct_tac "n" 1);
+by Auto_tac; 
+by (ftac size_eq_Suc_imp_eq_union 1);
+by (Clarify_tac 1); 
+ren "J'" 1;
+by (Asm_full_simp_tac 1); 
+by (etac notE 1); 
+by Auto_tac; 
+by (case_tac "J' = {#}" 1);
+ by (asm_full_simp_tac (simpset() addsimps [mult_def]) 1); 
+ by (rtac r_into_trancl 1); 
+ by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1);
+ by (Blast_tac 1); 
+(*Now we know J' ~= {#}*)
+by (cut_inst_tac [("M","K"),("P", "%x. (x,a):r")] multiset_partition 1);
+by (eres_inst_tac [("P", "ALL k : set_of K. ?P k")] rev_mp 1); 
+by (etac ssubst 1); 
+by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); 
+by Auto_tac; 
+by (subgoal_tac "((I + {# x : K. (x, a) : r#}) + {# x : K. (x, a) ~: r#}, \
+\                 (I + {# x : K. (x, a) : r#}) + J') : mult r" 1);
+ by (Force_tac 2);
+by (full_simp_tac (simpset() addsimps [union_assoc RS sym, mult_def]) 1); 
+by (etac trancl_trans 1); 
+by (rtac r_into_trancl 1); 
+by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); 
+by (res_inst_tac [("x", "a")] exI 1); 
+by (res_inst_tac [("x", "I + J'")] exI 1); 
+by (asm_simp_tac (simpset() addsimps union_ac) 1); 
+qed_spec_mp "one_step_implies_mult_lemma";
+
+Goal  "[| trans r;  J ~= {#};  \
+\         ALL k : set_of K. EX j : set_of J. (k,j) : r |] \
+\      ==> (I+K, I+J) : mult r";
+by (rtac one_step_implies_mult_lemma 1); 
+by Auto_tac; 
+qed "one_step_implies_mult";
+
 
 (** Proving that multisets are partially ordered **)
 
@@ -532,7 +625,7 @@
 (*asymmetry*)
 Goal "M < N ==> ~ N < (M :: ('a::order)multiset)";
 by Auto_tac;
-br (mult_less_not_refl RS notE) 1;
+by (rtac (mult_less_not_refl RS notE) 1);
 by (etac mult_less_trans 1);
 by (assume_tac 1);
 qed "mult_less_not_sym";
@@ -543,6 +636,7 @@
 Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)";
 by Auto_tac;
 qed "mult_le_refl";
+AddIffs [mult_le_refl];
 
 (*anti-symmetry*)
 Goalw [mult_le_def] "[| M <= N;  N <= M |] ==> M = (N :: ('a::order)multiset)";
@@ -558,3 +652,63 @@
 Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))";
 by Auto_tac;
 qed "mult_less_le";
+
+
+(** Monotonicity of multiset union **)
+
+Goalw [mult1_def]
+     "[| (B,D) : mult1 r; trans r |] ==> (C + B, C + D) : mult1 r";
+by Auto_tac; 
+by (res_inst_tac [("x", "a")] exI 1); 
+by (res_inst_tac [("x", "C+M0")] exI 1); 
+by (asm_simp_tac (simpset() addsimps [union_assoc]) 1); 
+qed "mult1_union";
+
+Goalw [mult_less_def, mult_def]
+     "!!C:: ('a::order) multiset. B<D ==> C+B < C+D";
+by (etac trancl_induct 1); 
+by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
+                               r_into_trancl]) 1); 
+by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
+                               r_into_trancl, trancl_trans]) 1); 
+qed "union_less_mono2";
+
+Goal "!!C:: ('a::order) multiset. B<D ==> B+C < D+C";
+by (simp_tac (simpset() addsimps [union_commute]) 1); 
+by (etac union_less_mono2 1); 
+qed "union_less_mono1";
+
+Goal "!!C:: ('a::order) multiset. [| A<C; B<D |] ==> A+B < C+D";
+by (blast_tac (claset() addIs [union_less_mono1, union_less_mono2,
+                               mult_less_trans]) 1); 
+qed "union_less_mono";
+
+Goalw [mult_le_def]
+     "!!D:: ('a::order) multiset. [| A<=C;  B<=D |] ==> A+B <= C+D";
+by (blast_tac (claset() addIs [union_less_mono, union_less_mono1, 
+                               union_less_mono2]) 1); 
+qed "union_le_mono";
+
+
+
+Goalw [mult_le_def, mult_less_def]
+     "{#} <= (M :: ('a::order) multiset)";
+by (case_tac "M={#}" 1);
+by (subgoal_tac "({#} + {#}, {#} + M) : mult(Collect (split op <))" 2);
+by (rtac one_step_implies_mult 3);
+bw trans_def;
+by Auto_tac; 
+by (blast_tac (claset() addIs [order_less_trans]) 1); 
+qed "empty_leI";
+AddIffs [empty_leI];
+
+
+Goal "!!A:: ('a::order) multiset. A <= A+B";
+by (subgoal_tac "A+{#} <= A+B" 1);
+by (rtac union_le_mono 2); 
+by Auto_tac; 
+qed "union_upper1";
+
+Goal "!!A:: ('a::order) multiset. B <= A+B";
+by (stac union_commute 1 THEN rtac union_upper1 1);
+qed "union_upper2";

--- a/src/HOL/Induct/Multiset.thy	Fri Jun 02 15:19:18 2000 +0200
+++ b/src/HOL/Induct/Multiset.thy	Fri Jun 02 17:42:43 2000 +0200
@@ -21,12 +21,16 @@
   single :: 'a                => 'a multiset   ("{#_#}")
   count  :: ['a multiset, 'a] => nat
   set_of :: 'a multiset => 'a set
+  MCollect :: ['a multiset, 'a => bool] => 'a multiset (*comprehension*)
+
 
 syntax
-  elem   :: ['a multiset, 'a] => bool          ("(_/ :# _)" [50, 51] 50)
+  elem     :: ['a, 'a multiset] => bool              ("(_/ :# _)" [50, 51] 50)
+  "@MColl" :: [pttrn, 'a multiset, bool] => 'a multiset ("(1{# _ : _./ _#})")
 
 translations
-  "M :# a" == "0 < count M a"
+  "a :# M"     == "0 < count M a"
+  "{#x:M. P#}" == "MCollect M (%x. P)"
 
 defs
   count_def  "count == Rep_multiset"
@@ -34,14 +38,16 @@
   single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)"
   union_def  "M+N   == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)"
   diff_def   "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
-  set_of_def "set_of M == {x. M :# x}"
+  MCollect_def "MCollect M P ==
+		Abs_multiset(%x. if P x then Rep_multiset M x else 0)"
+  set_of_def "set_of M == {x. x :# M}"
   size_def   "size (M) == setsum (count M) (set_of M)"
   Zero_def   "0 == {#}"
 
 constdefs
   mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set"
  "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K &
-                                 (!b. K :# b --> (b,a) : r)}"
+                                 (!b. b :# K --> (b,a) : r)}"
 
   mult :: "('a * 'a)set => ('a multiset * 'a multiset)set"
  "mult(r) == (mult1 r)^+"

--- a/src/HOL/Induct/MultisetOrder.thy	Fri Jun 02 15:19:18 2000 +0200
+++ b/src/HOL/Induct/MultisetOrder.thy	Fri Jun 02 17:42:43 2000 +0200
@@ -11,5 +11,5 @@
 instance multiset :: (order) order
     (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le)
 
-instance multiset :: (term) plus_ac0 (union_comm,union_assoc) {|Auto_tac|}
+instance multiset :: (term) plus_ac0 (union_commute,union_assoc) {|Auto_tac|}
 end