# HG changeset patch
# User haftmann
# Date 1266594720 -3600
# Node ID 04673275441a1c33d1bdb9f77844008ef6b2701a
# Parent  8dfd816713c662fd3ecbe7ffa053f8398d8d5c70
switched notations for pointwise and multiset order

diff -r 8dfd816713c6 -r 04673275441a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 19 14:47:01 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 19 16:52:00 2010 +0100
@@ -176,64 +176,6 @@
   by (simp add: multiset_eq_conv_count_eq)
 
 
-subsubsection {* Intersection *}
-
-definition multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
-  "multiset_inter A B = A - (A - B)"
-
-lemma multiset_inter_count:
-  "count (A #\<inter> B) x = min (count A x) (count B x)"
-  by (simp add: multiset_inter_def multiset_typedef)
-
-lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
-  by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
-  by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
-  by (rule multi_count_ext) (simp add: multiset_inter_count)
-
-lemmas multiset_inter_ac =
-  multiset_inter_commute
-  multiset_inter_assoc
-  multiset_inter_left_commute
-
-lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
-  by (rule multi_count_ext) (auto simp add: multiset_inter_count)
-
-lemma multiset_union_diff_commute:
-  assumes "B #\<inter> C = {#}"
-  shows "A + B - C = A - C + B"
-proof (rule multi_count_ext)
-  fix x
-  from assms have "min (count B x) (count C x) = 0"
-    by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
-  then have "count B x = 0 \<or> count C x = 0"
-    by auto
-  then show "count (A + B - C) x = count (A - C + B) x"
-    by auto
-qed
-
-
-subsubsection {* Comprehension (filter) *}
-
-lemma count_MCollect [simp]:
-  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
-  by (simp add: MCollect_def in_multiset multiset_typedef)
-
-lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
-  by (rule multi_count_ext) simp
-
-lemma MCollect_single [simp]:
-  "MCollect {#x#} P = (if P x then {#x#} else {#})"
-  by (rule multi_count_ext) simp
-
-lemma MCollect_union [simp]:
-  "MCollect (M + N) f = MCollect M f + MCollect N f"
-  by (rule multi_count_ext) simp
-
-
 subsubsection {* Equality of multisets *}
 
 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
@@ -335,64 +277,61 @@
 
 subsubsection {* Pointwise ordering induced by count *}
 
-definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
-  "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
+instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
+begin
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
 
-definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
-  "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
 
-notation mset_le  (infix "\<subseteq>#" 50)
-notation mset_less  (infix "\<subset>#" 50)
+instance proof
+qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
+
+end
 
 lemma mset_less_eqI:
-  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<subseteq># B"
+  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
   by (simp add: mset_le_def)
 
-lemma mset_le_refl[simp]: "A \<le># A"
-unfolding mset_le_def by auto
-
-lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
-unfolding mset_le_def by (fast intro: order_trans)
-
-lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
-apply (unfold mset_le_def)
-apply (rule multiset_eq_conv_count_eq [THEN iffD2])
-apply (blast intro: order_antisym)
-done
-
-lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
+lemma mset_le_exists_conv:
+  "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
 apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
 apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
 done
 
-lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
-unfolding mset_le_def by auto
+lemma mset_le_mono_add_right_cancel [simp]:
+  "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
+  by (fact add_le_cancel_right)
 
-lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
-unfolding mset_le_def by auto
+lemma mset_le_mono_add_left_cancel [simp]:
+  "C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B"
+  by (fact add_le_cancel_left)
+
+lemma mset_le_mono_add:
+  "(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D"
+  by (fact add_mono)
 
-lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
-apply (unfold mset_le_def)
-apply auto
-apply (erule_tac x = a in allE)+
-apply auto
-done
+lemma mset_le_add_left [simp]:
+  "(A::'a multiset) \<le> A + B"
+  unfolding mset_le_def by auto
+
+lemma mset_le_add_right [simp]:
+  "B \<le> (A::'a multiset) + B"
+  unfolding mset_le_def by auto
 
-lemma mset_le_add_left[simp]: "A \<le># A + B"
-unfolding mset_le_def by auto
-
-lemma mset_le_add_right[simp]: "B \<le># A + B"
-unfolding mset_le_def by auto
+lemma mset_le_single:
+  "a :# B \<Longrightarrow> {#a#} \<le> B"
+  by (simp add: mset_le_def)
 
-lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
-by (simp add: mset_le_def)
-
-lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
-by (simp add: multiset_eq_conv_count_eq mset_le_def)
+lemma multiset_diff_union_assoc:
+  "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
+  by (simp add: multiset_eq_conv_count_eq mset_le_def)
 
 lemma mset_le_multiset_union_diff_commute:
-assumes "B \<le># A"
-shows "A - B + C = A + C - B"
+  assumes "B \<le> A"
+  shows "(A::'a multiset) - B + C = A + C - B"
 proof -
   from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
   from this obtain D where "A = B + D" ..
@@ -410,31 +349,19 @@
     done
 qed
 
-interpretation mset_order: order "op \<le>#" "op <#"
-proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
-  mset_le_trans simp: mset_less_def)
-
-interpretation mset_order_cancel_semigroup:
-  ordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
-proof qed (erule mset_le_mono_add [OF mset_le_refl])
-
-interpretation mset_order_semigroup_cancel:
-  ordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
-proof qed simp
-
-lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: mset_le_def mset_less_def)
 apply (erule_tac x=x in allE)
 apply auto
 done
 
-lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: mset_le_def mset_less_def)
 apply (erule_tac x = x in allE)
 apply auto
 done
   
-lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
+lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
 apply (rule conjI)
  apply (simp add: mset_lessD)
 apply (clarsimp simp: mset_le_def mset_less_def)
@@ -443,30 +370,90 @@
  apply (auto split: split_if_asm)
 done
 
-lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
+lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)"
 apply (rule conjI)
  apply (simp add: mset_leD)
 apply (force simp: mset_le_def mset_less_def split: split_if_asm)
 done
 
-lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
+lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
   by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
 
-lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
-by (auto simp: mset_le_def mset_less_def)
+lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
+  by (auto simp: mset_le_def mset_less_def)
 
-lemma multi_psub_self[simp]: "A \<subset># A = False"
-by (auto simp: mset_le_def mset_less_def)
+lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
+  by simp
 
 lemma mset_less_add_bothsides:
-  "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
-by (auto simp: mset_le_def mset_less_def)
+  "T + {#x#} < S + {#x#} \<Longrightarrow> T < S"
+  by (fact add_less_imp_less_right)
+
+lemma mset_less_empty_nonempty:
+  "{#} < S \<longleftrightarrow> S \<noteq> {#}"
+  by (auto simp: mset_le_def mset_less_def)
+
+lemma mset_less_diff_self:
+  "c \<in># B \<Longrightarrow> B - {#c#} < B"
+  by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+
+
+subsubsection {* Intersection *}
+
+instantiation multiset :: (type) semilattice_inf
+begin
+
+definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+  multiset_inter_def: "inf_multiset A B = A - (A - B)"
+
+instance proof -
+  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
+  show "OFCLASS('a multiset, semilattice_inf_class)" proof
+  qed (auto simp add: multiset_inter_def mset_le_def aux)
+qed
+
+end
+
+abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
+  "multiset_inter \<equiv> inf"
 
-lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
-by (auto simp: mset_le_def mset_less_def)
+lemma multiset_inter_count:
+  "count (A #\<inter> B) x = min (count A x) (count B x)"
+  by (simp add: multiset_inter_def multiset_typedef)
+
+lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
+  by (rule multi_count_ext) (auto simp add: multiset_inter_count)
 
-lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
-  by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+lemma multiset_union_diff_commute:
+  assumes "B #\<inter> C = {#}"
+  shows "A + B - C = A - C + B"
+proof (rule multi_count_ext)
+  fix x
+  from assms have "min (count B x) (count C x) = 0"
+    by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
+  then have "count B x = 0 \<or> count C x = 0"
+    by auto
+  then show "count (A + B - C) x = count (A - C + B) x"
+    by auto
+qed
+
+
+subsubsection {* Comprehension (filter) *}
+
+lemma count_MCollect [simp]:
+  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
+  by (simp add: MCollect_def in_multiset multiset_typedef)
+
+lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
+  by (rule multi_count_ext) simp
+
+lemma MCollect_single [simp]:
+  "MCollect {#x#} P = (if P x then {#x#} else {#})"
+  by (rule multi_count_ext) simp
+
+lemma MCollect_union [simp]:
+  "MCollect (M + N) f = MCollect M f + MCollect N f"
+  by (rule multi_count_ext) simp
 
 
 subsubsection {* Set of elements *}
@@ -657,7 +644,7 @@
 apply auto
 done
 
-lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
+lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
   case (empty M)
   then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
@@ -666,12 +653,12 @@
   then show ?case by simp
 next
   case (add S x T)
-  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
-  have SxsubT: "S + {#x#} \<subset># T" by fact
-  then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
+  have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
+  have SxsubT: "S + {#x#} < T" by fact
+  then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
   then obtain T' where T: "T = T' + {#x#}" 
     by (blast dest: multi_member_split)
-  then have "S \<subset># T'" using SxsubT 
+  then have "S < T'" using SxsubT 
     by (blast intro: mset_less_add_bothsides)
   then have "size S < size T'" using IH by simp
   then show ?case using T by simp
@@ -686,7 +673,7 @@
 
 definition
   mset_less_rel :: "('a multiset * 'a multiset) set" where
-  "mset_less_rel = {(A,B). A \<subset># B}"
+  "mset_less_rel = {(A,B). A < B}"
 
 lemma multiset_add_sub_el_shuffle: 
   assumes "c \<in># B" and "b \<noteq> c" 
@@ -709,29 +696,29 @@
 text {* The induction rules: *}
 
 lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
 shows "P B"
 apply (rule wf_mset_less_rel [THEN wf_induct])
 apply (rule ih, auto simp: mset_less_rel_def)
 done
 
 lemma multi_subset_induct [consumes 2, case_names empty add]:
-assumes "F \<subseteq># A"
+assumes "F \<le> A"
   and empty: "P {#}"
   and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
 shows "P F"
 proof -
-  from `F \<subseteq># A`
+  from `F \<le> A`
   show ?thesis
   proof (induct F)
     show "P {#}" by fact
   next
     fix x F
-    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
+    assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> A"
     show "P (F + {#x#})"
     proof (rule insert)
       from i show "x \<in># A" by (auto dest: mset_le_insertD)
-      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
+      from i have "F \<le> A" by (auto dest: mset_le_insertD)
       with P show "P F" .
     qed
   qed
@@ -875,12 +862,8 @@
     by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
 qed
 
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
-apply (induct xs)
- apply auto
-apply (rule mset_le_trans)
- apply auto
-done
+lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
+  by (induct xs) (auto intro: order_trans)
 
 lemma multiset_of_update:
   "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
@@ -969,7 +952,7 @@
   by (simp add: multiset_eq_conv_count_eq count_of_filter)
 
 lemma mset_less_eq_Bag [code]:
-  "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
+  "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs then show ?rhs
@@ -990,10 +973,10 @@
 begin
 
 definition
-  "HOL.eq A B \<longleftrightarrow> A \<subseteq># B \<and> B \<subseteq># A"
+  "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
 
 instance proof
-qed (simp add: eq_multiset_def mset_order.eq_iff)
+qed (simp add: eq_multiset_def eq_iff)
 
 end
 
@@ -1223,76 +1206,43 @@
 
 subsubsection {* Partial-order properties *}
 
-instantiation multiset :: (order) order
-begin
-
-definition less_multiset_def:
-  "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset_def:
-  "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
-
-lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
-unfolding trans_def by (blast intro: order_less_trans)
-
-text {*
- \medskip Irreflexivity.
-*}
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
+  "M' \<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
 
-lemma mult_irrefl_aux:
-  "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
-by (induct rule: finite_induct) (auto intro: order_less_trans)
-
-lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
-apply (unfold less_multiset_def, auto)
-apply (drule trans_base_order [THEN mult_implies_one_step], auto)
-apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
-apply (simp add: set_of_eq_empty_iff)
-done
-
-lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
-using insert mult_less_not_refl by fast
-
-
-text {* Transitivity. *}
+definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
+  "M' \<subseteq># M \<longleftrightarrow> M' \<subset># M \<or> M' = M"
 
-theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
-unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-
-text {* Asymmetry. *}
-
-theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
-apply auto
-apply (rule mult_less_not_refl [THEN notE])
-apply (erule mult_less_trans, assumption)
-done
-
-theorem mult_less_asym:
-  "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
-using mult_less_not_sym by blast
-
-theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
-unfolding le_multiset_def by auto
+interpretation multiset_order: order le_multiset less_multiset
+proof -
+  have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
+  proof
+    fix M :: "'a multiset"
+    assume "M \<subset># M"
+    then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
+    have "trans {(x'::'a, x). x' < x}"
+      by (rule transI) simp
+    moreover note MM
+    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
+      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+      by (rule mult_implies_one_step)
+    then obtain I J K where "M = I + J" and "M = I + K"
+      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
+    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
+    have "finite (set_of K)" by simp
+    moreover note aux2
+    ultimately have "set_of K = {}"
+      by (induct rule: finite_induct) (auto intro: order_less_trans)
+    with aux1 show False by simp
+  qed
+  have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
+    unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
+  show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+  qed (auto simp add: le_multiset_def irrefl dest: trans)
+qed
 
-text {* Anti-symmetry. *}
-
-theorem mult_le_antisym:
-  "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
-unfolding le_multiset_def by (blast dest: mult_less_not_sym)
-
-text {* Transitivity. *}
-
-theorem mult_le_trans:
-  "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
-unfolding le_multiset_def by (blast intro: mult_less_trans)
-
-theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
-unfolding le_multiset_def by auto
-
-instance proof
-qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans)
-
-end
+lemma mult_less_irrefl [elim!]:
+  "M \<subset># (M::'a::order multiset) ==> R"
+  by (simp add: multiset_order.less_irrefl)
 
 
 subsubsection {* Monotonicity of multiset union *}
@@ -1306,52 +1256,26 @@
 apply (simp add: add_assoc)
 done
 
-lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
+lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
 apply (unfold less_multiset_def mult_def)
 apply (erule trancl_induct)
  apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
 apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
 done
 
-lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
+lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"
 apply (subst add_commute [of B C])
 apply (subst add_commute [of D C])
 apply (erule union_less_mono2)
 done
 
 lemma union_less_mono:
-  "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
-by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
-
-lemma union_le_mono:
-  "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
-unfolding le_multiset_def
-by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
+  "A \<subset># C ==> B \<subset># D ==> A + B \<subset># C + (D::'a::order multiset)"
+  by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
 
-lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
-apply (unfold le_multiset_def less_multiset_def)
-apply (case_tac "M = {#}")
- prefer 2
- apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
-  prefer 2
-  apply (rule one_step_implies_mult)
-    apply (simp only: trans_def)
-    apply auto
-done
-
-lemma union_upper1: "A <= A + (B::'a::order multiset)"
-proof -
-  have "A + {#} <= A + B" by (blast intro: union_le_mono)
-  then show ?thesis by simp
-qed
-
-lemma union_upper2: "B <= A + (B::'a::order multiset)"
-by (subst add_commute) (rule union_upper1)
-
-instance multiset :: (order) ordered_ab_semigroup_add
-apply intro_classes
-apply (erule union_le_mono[OF mult_le_refl])
-done
+interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
+proof
+qed (auto simp add: le_multiset_def intro: union_less_mono2)
 
 
 subsection {* The fold combinator *}
@@ -1406,7 +1330,7 @@
   "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
 proof (induct arbitrary: x y z rule: full_multiset_induct)
   case (less M x\<^isub>1 x\<^isub>2 Z)
-  have IH: "\<forall>A. A \<subset># M \<longrightarrow> 
+  have IH: "\<forall>A. A < M \<longrightarrow> 
     (\<forall>x x' x''. fold_msetG f x'' A x \<longrightarrow> fold_msetG f x'' A x'
                \<longrightarrow> x' = x)" by fact
   have Mfoldx\<^isub>1: "fold_msetG f Z M x\<^isub>1" and Mfoldx\<^isub>2: "fold_msetG f Z M x\<^isub>2" by fact+
@@ -1426,8 +1350,8 @@
       fix C c v
       assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v"
       then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
-      then have CsubM: "C \<subset># M" by simp
-      from MBb have BsubM: "B \<subset># M" by simp
+      then have CsubM: "C < M" by simp
+      from MBb have BsubM: "B < M" by simp
       show ?case
       proof cases
         assume "b=c"
@@ -1438,8 +1362,8 @@
         let ?D = "B - {#c#}"
         have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
           by (auto intro: insert_noteq_member dest: sym)
-        have "B - {#c#} \<subset># B" using cinB by (rule mset_less_diff_self)
-        then have DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_order.less_trans)
+        have "B - {#c#} < B" using cinB by (rule mset_less_diff_self)
+        then have DsubM: "?D < M" using BsubM by (blast intro: order_less_trans)
         from MBb MCc have "B + {#b#} = C + {#c#}" by blast
         then have [simp]: "B + {#b#} - {#c#} = C"
           using MBb MCc binC cinB by auto
@@ -1769,6 +1693,37 @@
 lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   by (fact add_imp_eq)
 
-lemmas mset_less_trans = mset_order.less_trans
+lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
+  by (fact order_less_trans)
+
+lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
+  by (fact inf.commute)
+
+lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
+  by (fact inf.assoc [symmetric])
+
+lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
+  by (fact inf.left_commute)
+
+lemmas multiset_inter_ac =
+  multiset_inter_commute
+  multiset_inter_assoc
+  multiset_inter_left_commute
+
+lemma mult_less_not_refl:
+  "\<not> M \<subset># (M::'a::order multiset)"
+  by (fact multiset_order.less_irrefl)
+
+lemma mult_less_trans:
+  "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
+  by (fact multiset_order.less_trans)
+    
+lemma mult_less_not_sym:
+  "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
+  by (fact multiset_order.less_not_sym)
+
+lemma mult_less_asym:
+  "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
+  by (fact multiset_order.less_asym)
 
 end
\ No newline at end of file