# HG changeset patch
# User blanchet
# Date 1428499280 -7200
# Node ID 4538d41e8e540184da647f18e08268b7b0391d67
# Parent  5031030aaebe6f2a7c4580eb10f565c1bde2bf3c
renamed multiset ordering to free up nice <# etc. symbols for the standard subset

diff -r 5031030aaebe -r 4538d41e8e54 NEWS
--- a/NEWS	Wed Apr 08 15:04:06 2015 +0200
+++ b/NEWS	Wed Apr 08 15:21:20 2015 +0200
@@ -330,6 +330,12 @@
   - Introduced "replicate_mset" operation.
   - Introduced alternative characterizations of the multiset ordering in
     "Library/Multiset_Order".
+  - Renamed multiset ordering:
+      <# ~> #<#
+      <=# ~> #<=#
+      \<subset># ~> #\<subset>#
+      \<subseteq># ~> #\<subseteq>#
+    INCOMPATIBILITY.
   - Renamed
       in_multiset_of ~> in_multiset_in_set
     INCOMPATIBILITY.
diff -r 5031030aaebe -r 4538d41e8e54 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 08 15:04:06 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Apr 08 15:21:20 2015 +0200
@@ -1778,21 +1778,21 @@
 
 subsubsection {* Partial-order properties *}
 
-definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
-  "M' <# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
-  "M' <=# M \<longleftrightarrow> M' <# M \<or> M' = M"
-
-notation (xsymbols) less_multiset (infix "\<subset>#" 50)
-notation (xsymbols) le_multiset (infix "\<subseteq>#" 50)
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
+  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition le_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
+  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
+
+notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
+notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
 
 interpretation multiset_order: order le_multiset less_multiset
 proof -
-  have irrefl: "\<And>M :: 'a multiset. \<not> M \<subset># M"
+  have irrefl: "\<And>M :: 'a multiset. \<not> M #\<subset># M"
   proof
     fix M :: "'a multiset"
-    assume "M \<subset># M"
+    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
@@ -1809,13 +1809,13 @@
       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"
+  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 "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
     by default (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
-lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
+lemma mult_less_irrefl [elim!]: "M #\<subset># (M::'a::order multiset) ==> R"
   by simp
 
 
@@ -1829,21 +1829,21 @@
 apply (simp add: add.assoc)
 done
 
-lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># 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)
 apply (blast intro: mult1_union trancl_trans)
 done
 
-lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># 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 \<subset># C ==> B \<subset># D ==> A + B \<subset># C + (D::'a::order multiset)"
+  "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)
 
 interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
@@ -2044,19 +2044,19 @@
   multiset_inter_left_commute
 
 lemma mult_less_not_refl:
-  "\<not> M \<subset># (M::'a::order multiset)"
+  "\<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)"
+  "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)"
+  "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"
+  "M #\<subset># N ==> (\<not> P ==> N #\<subset># (M::'a::order multiset)) ==> P"
   by (fact multiset_order.less_asym)
 
 ML {*
diff -r 5031030aaebe -r 4538d41e8e54 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:04:06 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Apr 08 15:21:20 2015 +0200
@@ -198,7 +198,7 @@
 end
 
 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
-  "M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+  "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
   unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
 
 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
@@ -206,10 +206,10 @@
 
 lemma le_multiset\<^sub>H\<^sub>O:
   fixes M N :: "('a \<Colon> linorder) multiset"
-  shows "M \<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
+  shows "M #\<subseteq># 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: le_multiset_def less_multiset\<^sub>H\<^sub>O)
 
-lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
+lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}"
   unfolding less_multiset_def by (auto intro: wf_mult wf)
 
 lemma order_multiset: "class.order
@@ -234,52 +234,52 @@
 
 lemma le_multiset_total:
   fixes M N :: "('a \<Colon> linorder) multiset"
-  shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
+  shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
   by (metis multiset_linorder.le_cases)
 
 lemma less_eq_imp_le_multiset:
   fixes M N :: "('a \<Colon> linorder) multiset"
-  shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
+  shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
   by (auto dest: leD simp add: less_eq_multiset.rep_eq)
 
 lemma less_multiset_right_total:
   fixes M :: "('a \<Colon> linorder) multiset"
-  shows "M \<subset># M + {#undefined#}"
+  shows "M #\<subset># M + {#undefined#}"
   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
 
 lemma le_multiset_empty_left[simp]:
   fixes M :: "('a \<Colon> linorder) multiset"
-  shows "{#} \<subseteq># M"
+  shows "{#} #\<subseteq># M"
   by (simp add: less_eq_imp_le_multiset)
 
 lemma le_multiset_empty_right[simp]:
   fixes M :: "('a \<Colon> linorder) multiset"
-  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
+  shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
   by (metis le_multiset_empty_left multiset_order.antisym)
 
 lemma less_multiset_empty_left[simp]:
   fixes M :: "('a \<Colon> linorder) multiset"
-  shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
+  shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
   by (simp add: less_multiset\<^sub>H\<^sub>O)
 
 lemma less_multiset_empty_right[simp]:
   fixes M :: "('a \<Colon> linorder) multiset"
-  shows "\<not> M \<subset># {#}"
+  shows "\<not> M #\<subset># {#}"
   using le_empty less_multiset\<^sub>D\<^sub>M by blast
 
 lemma
   fixes M N :: "('a \<Colon> linorder) multiset"
   shows
-    le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
-    le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
+    le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
+    le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
   using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
 
 lemma
   fixes M N :: "('a \<Colon> linorder) multiset"
   shows
-    less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
-    less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
+    less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
+    less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
   unfolding less_multiset\<^sub>H\<^sub>O by auto
 
 lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
@@ -288,21 +288,21 @@
 lemma
   fixes M N :: "('a \<Colon> linorder) multiset"
   shows
-    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
-    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
+    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
+    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
   using [[metis_verbose = false]]
   by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
     add.commute)+
 
-lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M \<subset># N"
+lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
   unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
 
 lemma ex_gt_count_imp_less_multiset:
-  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M \<subset># N"
+  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
   unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
     less_not_sym mset_leD mset_le_add_left)  
 
-lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
+lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
   by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
 
 end