added 'supset' variants for new '<#' etc. symbols on multisets
--- a/NEWS Wed Jan 20 13:16:58 2016 +0100
+++ b/NEWS Wed Jan 20 17:14:53 2016 +0100
@@ -648,10 +648,15 @@
* Library/Multiset:
- Renamed multiset inclusion operators:
< ~> <#
+ > ~> >#
\<subset> ~> \<subset>#
+ \<supset> ~> \<supset>#
<= ~> <=#
+ >= ~> >=#
\<le> ~> \<le>#
+ \<ge> ~> \<ge>#
\<subseteq> ~> \<subseteq>#
+ \<supseteq> ~> \<supseteq>#
INCOMPATIBILITY.
- "'a multiset" is no longer an instance of the "order",
"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
--- a/src/HOL/Library/Multiset.thy Wed Jan 20 13:16:58 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Jan 20 17:14:53 2016 +0100
@@ -271,12 +271,23 @@
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
+abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "supseteq_mset A B == B \<subseteq># A"
+
+abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "supset_mset A B == B \<subset># A"
+
notation (input)
- subseteq_mset (infix "\<le>#" 50)
+ subseteq_mset (infix "\<le>#" 50) and
+ supseteq_mset (infix "\<ge>#" 50) and
+ supseteq_mset (infix "\<supseteq>#" 50) and
+ supset_mset (infix "\<supset>#" 50)
notation (ASCII)
subseteq_mset (infix "<=#" 50) and
- subset_mset (infix "<#" 50)
+ subset_mset (infix "<#" 50) and
+ supseteq_mset (infix ">=#" 50) and
+ supset_mset (infix ">#" 50)
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)