# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1467905679 -7200
# Node ID 9789ccc2a477724791d0cd4607976426dd32a7d0
# Parent  3f3223b90239a1d2d801ce973e34c947cb757aea
more instantiations for multiset

diff -r 3f3223b90239 -r 9789ccc2a477 NEWS
--- a/NEWS	Thu Jul 07 09:24:03 2016 +0200
+++ b/NEWS	Thu Jul 07 17:34:39 2016 +0200
@@ -350,6 +350,16 @@
     less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
 INCOMPATIBILITY.
 
+* Some typeclass constraints about multisets have been reduced from ordered or
+linordered to preorder. Multisets have the additional typeclasses order_bot,
+no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
+and linordered_cancel_ab_semigroup_add.
+INCOMPATIBILITY.
+
+* There are some new simplification rules about multisets and the multiset
+ordering.
+INCOMPATIBILITY.
+
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
 
diff -r 3f3223b90239 -r 9789ccc2a477 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Jul 07 17:34:39 2016 +0200
@@ -2488,7 +2488,7 @@
 
 subsubsection \<open>Partial-order properties\<close>
 
-lemma (in order) mult1_lessE:
+lemma (in preorder) mult1_lessE:
   assumes "(N, M) \<in> mult1 {(a, b). a < b}"
   obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
     "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
@@ -2499,7 +2499,7 @@
   ultimately show thesis by (auto intro: that)
 qed
 
-instantiation multiset :: (order) order
+instantiation multiset :: (preorder) order
 begin
 
 definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
@@ -2515,7 +2515,7 @@
     assume "M < 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
+      by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
     moreover note MM
     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
       \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
@@ -2537,7 +2537,7 @@
 end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
 
 lemma mset_le_irrefl [elim!]:
-  fixes M :: "'a::order multiset"
+  fixes M :: "'a::preorder multiset"
   shows "M < M \<Longrightarrow> R"
   by simp
 
@@ -2552,25 +2552,25 @@
 apply (simp add: add.assoc)
 done
 
-lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order multiset)"
+lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
 apply (unfold less_multiset_def mult_def)
 apply (erule trancl_induct)
  apply (blast intro: mult1_union)
 apply (blast intro: mult1_union trancl_trans)
 done
 
-lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
+lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
 apply (subst add.commute [of B C])
 apply (subst add.commute [of D C])
 apply (erule union_le_mono2)
 done
 
 lemma union_less_mono:
-  fixes A B C D :: "'a::order multiset"
+  fixes A B C D :: "'a::preorder multiset"
   shows "A < C \<Longrightarrow> B < D \<Longrightarrow> A + B < C + D"
   by (blast intro!: union_le_mono1 union_le_mono2 less_trans)
 
-instantiation multiset :: (order) ordered_ab_semigroup_add
+instantiation multiset :: (preorder) ordered_ab_semigroup_add
 begin
 instance
   by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
@@ -2769,16 +2769,16 @@
   multiset_inter_assoc
   multiset_inter_left_commute
 
-lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
+lemma mset_le_not_refl: "\<not> M < (M::'a::preorder multiset)"
   by (fact less_irrefl)
 
-lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
+lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::preorder multiset)"
   by (fact less_trans)
 
-lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
+lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::preorder multiset)"
   by (fact less_not_sym)
 
-lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
+lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::preorder multiset)) \<Longrightarrow> P"
   by (fact less_asym)
 
 declaration \<open>
diff -r 3f3223b90239 -r 9789ccc2a477 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 17:34:39 2016 +0200
@@ -11,29 +11,9 @@
 
 subsection \<open>Alternative characterizations\<close>
 
-context order
+context preorder
 begin
 
-lemma reflp_le: "reflp (op \<le>)"
-  unfolding reflp_def by simp
-
-lemma antisymP_le: "antisymP (op \<le>)"
-  unfolding antisym_def by auto
-
-lemma transp_le: "transp (op \<le>)"
-  unfolding transp_def by auto
-
-lemma irreflp_less: "irreflp (op <)"
-  unfolding irreflp_def by simp
-
-lemma antisymP_less: "antisymP (op <)"
-  unfolding antisym_def by auto
-
-lemma transp_less: "transp (op <)"
-  unfolding transp_def by auto
-
-lemmas le_trans = transp_le[unfolded transp_def, rule_format]
-
 lemma order_mult: "class.order
   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
   (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
@@ -43,7 +23,7 @@
   proof
     fix M :: "'a multiset"
     have "trans {(x'::'a, x). x' < x}"
-      by (rule transI) simp
+      by (rule transI) (blast intro: less_trans)
     moreover
     assume "(M, M) \<in> mult {(x, y). x < y}"
     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
@@ -91,7 +71,7 @@
   from step(2) obtain M0 a K where
     *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     by (blast elim: mult1_lessE)
-  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
+  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
   moreover
   { assume "count P a \<le> count M a"
     with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
@@ -99,7 +79,7 @@
       with ** obtain z where z: "z > a" "count M z < count N z"
         by blast
       with * have "count N z \<le> count P z" 
-        by (force simp add: not_in_iff)
+        by (auto elim: less_asym intro: count_inI)
       with z have "\<exists>z > a. count M z < count P z" by auto
   } note count_a = this
   { fix y
@@ -186,27 +166,6 @@
 
 end
 
-context linorder
-begin
-
-lemma total_le: "total {(a :: 'a, b). a \<le> b}"
-  unfolding total_on_def by auto
-
-lemma total_less: "total {(a :: 'a, b). a < b}"
-  unfolding total_on_def by auto
-
-lemma linorder_mult: "class.linorder
-  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
-  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
-proof -
-  interpret o: order
-    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
-    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
-    by (rule order_mult)
-  show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
-qed
-
-end
 
 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
   "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
@@ -248,34 +207,28 @@
 lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
   by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
 
-instantiation multiset :: (linorder) linorder
+instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
 begin
 
 lemma less_eq_multiset\<^sub>H\<^sub>O:
   "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
   by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
 
-instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
-
-lemma less_eq_multiset_total:
-  fixes M N :: "'a multiset"
-  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
-  by simp
+instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
 
 lemma
   fixes M N :: "'a multiset"
   shows
     less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
     less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
-  using [[metis_verbose = false]]
-  by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
+  using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
 
 lemma
   fixes M N :: "'a multiset"
   shows
-    le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
-    le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
-  unfolding less_multiset\<^sub>H\<^sub>O by auto
+    le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
+    le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
+  by simp_all
 
 lemma
   fixes M N :: "'a multiset"
@@ -285,12 +238,21 @@
   using [[metis_verbose = false]]
   by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
 
+end
+
 lemma ex_gt_count_imp_le_multiset:
-  "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
+  "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   unfolding less_multiset\<^sub>H\<^sub>O
-  by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
+  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
+
 
-end
+instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
+  by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
+
+lemma less_eq_multiset_total:
+  fixes M N :: "'a :: linorder multiset"
+  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
+  by simp
 
 instantiation multiset :: (wellorder) wellorder
 begin
@@ -302,4 +264,26 @@
 
 end
 
+instantiation multiset :: (preorder) order_bot
+begin
+
+definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"
+
+instance by standard (simp add: bot_multiset_def)
+
 end
+
+instance multiset :: (preorder) no_top
+proof standard
+  fix x :: "'a multiset"
+  obtain a :: 'a where True by simp
+  have "x < x + (x + {#a#})"
+    by simp
+  then show "\<exists>y. x < y"
+    by blast
+qed
+
+instance multiset :: (preorder) ordered_cancel_comm_monoid_add
+  by standard
+
+end
diff -r 3f3223b90239 -r 9789ccc2a477 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 17:34:39 2016 +0200
@@ -36,17 +36,12 @@
 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
   by (fact mset_append)
 
-lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
-unfolding less_eq_multiset_def apply (cases B; simp)
-apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
-done
-
 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
 apply (rule monoI)
 apply (unfold prefix_def)
 apply (erule genPrefix.induct, simp_all add: add_right_mono)
 apply (erule order_trans)
-apply (simp add: subseteq_le_multiset)
+apply simp
 done
 
 (** setsum **)