# HG changeset patch
# User blanchet
# Date 1467839968 -7200
# Node ID 89dd1345a04f71cb5ebb0b8a56de7d6e604566cf
# Parent  32866eff1843cd0f10d0128f922969efaf46ad3d
leverage new 'order' type class instantiation in multiset

diff -r 32866eff1843 -r 89dd1345a04f NEWS
--- a/NEWS	Wed Jul 06 23:19:27 2016 +0200
+++ b/NEWS	Wed Jul 06 23:19:28 2016 +0200
@@ -316,11 +316,13 @@
     #\<subset># ~> <
     le_multiset ~> less_eq_multiset
     less_multiset ~> le_multiset
-INCOMPATIBILITY
+INCOMPATIBILITY.
 
 * The prefix multiset_order has been discontinued: the theorems can be directly
-accessed.
-INCOMPATILBITY
+accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset"
+have been discontinued, and the interpretations "multiset_linorder" and
+"multiset_wellorder" have been replaced by instantiations.
+INCOMPATIBILITY.
 
 * Some theorems about the multiset ordering have been renamed:
     le_multiset_def ~> less_eq_multiset_def
@@ -346,7 +348,7 @@
     le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
     less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
     less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
-INCOMPATIBILITY
+INCOMPATIBILITY.
 
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
diff -r 32866eff1843 -r 89dd1345a04f src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Jul 06 23:19:27 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Jul 06 23:19:28 2016 +0200
@@ -223,30 +223,20 @@
 lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M < N}"
   unfolding less_multiset_def by (auto intro: wf_mult wf)
 
-lemma order_multiset: "class.order
-  (op \<le> :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
-  (op < :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
-  by unfold_locales
-
-lemma linorder_multiset: "class.linorder
-  (op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
-  (op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
-  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O less_eq_multiset_def not_less_iff_gr_or_eq)
+instantiation multiset :: (linorder) linorder
+begin
+  instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
+end
 
-interpretation multiset_linorder: linorder
-  "op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
-  "op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
-  by (rule linorder_multiset)
-
-interpretation multiset_wellorder: wellorder
-  "op \<le> :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
-  "op < :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
-  by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
+instantiation multiset :: (wellorder) wellorder
+begin
+  instance by standard (metis less_multiset_def wf wf_def wf_mult)
+end
 
 lemma less_eq_multiset_total:
   fixes M N :: "('a :: linorder) multiset"
   shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
-  by (metis multiset_linorder.le_cases)
+  by simp
 
 lemma subset_eq_imp_le_multiset:
   fixes M N :: "('a :: linorder) multiset"
@@ -256,7 +246,7 @@
 
 lemma le_multiset_right_total:
   fixes M :: "('a :: linorder) multiset"
-  shows "M < M + {#undefined#}"
+  shows "M < M + {#x#}"
   unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
 
 lemma less_eq_multiset_empty_left[simp]:
@@ -294,7 +284,7 @@
   unfolding less_multiset\<^sub>H\<^sub>O by auto
 
 lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
-  by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
+  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
 
 lemma
   fixes M N :: "('a :: linorder) multiset"