standardized notation
authorhaftmann
Sat Dec 17 15:22:13 2016 +0100 (2016-12-17)
changeset 645878355a6e2df79
parent 64586 1d25ca718790
child 64588 293ab573d034
standardized notation
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -15,16 +15,16 @@
     1.4    where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
     1.5  
     1.6  definition
     1.7 -  l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
     1.8 -  where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
     1.9 +  l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "\<subset>#\<index>" 60)
    1.10 +  where "a \<subset>#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
    1.11  
    1.12  definition
    1.13    RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    1.14    where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
    1.15  
    1.16  definition
    1.17 -  set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    1.18 -  where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
    1.19 +  set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "\<subset>#>\<index>" 60)
    1.20 +  where "H \<subset>#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
    1.21  
    1.22  definition
    1.23    SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    1.24 @@ -32,7 +32,7 @@
    1.25  
    1.26  
    1.27  locale normal = subgroup + group +
    1.28 -  assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
    1.29 +  assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x \<subset># H)"
    1.30  
    1.31  abbreviation
    1.32    normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
    1.33 @@ -287,7 +287,7 @@
    1.34  lemma (in monoid) set_mult_closed:
    1.35    assumes Acarr: "A \<subseteq> carrier G"
    1.36        and Bcarr: "B \<subseteq> carrier G"
    1.37 -  shows "A <#> B \<subseteq> carrier G"
    1.38 +  shows "A \<subset>#> B \<subseteq> carrier G"
    1.39  apply rule apply (simp add: set_mult_def, clarsimp)
    1.40  proof -
    1.41    fix a b
    1.42 @@ -306,7 +306,7 @@
    1.43  lemma (in comm_group) mult_subgroups:
    1.44    assumes subH: "subgroup H G"
    1.45        and subK: "subgroup K G"
    1.46 -  shows "subgroup (H <#> K) G"
    1.47 +  shows "subgroup (H \<subset>#> K) G"
    1.48  apply (rule subgroup.intro)
    1.49     apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
    1.50    apply (simp add: set_mult_def) apply clarsimp defer 1
    1.51 @@ -351,7 +351,7 @@
    1.52    assumes "group G"
    1.53    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    1.54        and xixH: "(inv x \<otimes> x') \<in> H"
    1.55 -  shows "x' \<in> x <# H"
    1.56 +  shows "x' \<in> x \<subset># H"
    1.57  proof -
    1.58    interpret group G by fact
    1.59    from xixH
    1.60 @@ -375,7 +375,7 @@
    1.61        have "x \<otimes> h = x'" by simp
    1.62  
    1.63    from this[symmetric] and hH
    1.64 -      show "x' \<in> x <# H"
    1.65 +      show "x' \<in> x \<subset># H"
    1.66        unfolding l_coset_def
    1.67        by fast
    1.68  qed
    1.69 @@ -387,7 +387,7 @@
    1.70    by (simp add: normal_def subgroup_def)
    1.71  
    1.72  lemma (in group) normalI: 
    1.73 -  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
    1.74 +  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x \<subset># H) \<Longrightarrow> H \<lhd> G"
    1.75    by (simp add: normal_def normal_axioms_def is_group)
    1.76  
    1.77  lemma (in normal) inv_op_closed1:
    1.78 @@ -460,18 +460,18 @@
    1.79  
    1.80  lemma (in group) lcos_m_assoc:
    1.81       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    1.82 -      ==> g <# (h <# M) = (g \<otimes> h) <# M"
    1.83 +      ==> g \<subset># (h \<subset># M) = (g \<otimes> h) \<subset># M"
    1.84  by (force simp add: l_coset_def m_assoc)
    1.85  
    1.86 -lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
    1.87 +lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> \<subset># M = M"
    1.88  by (force simp add: l_coset_def)
    1.89  
    1.90  lemma (in group) l_coset_subset_G:
    1.91 -     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
    1.92 +     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x \<subset># H \<subseteq> carrier G"
    1.93  by (auto simp add: l_coset_def subsetD)
    1.94  
    1.95  lemma (in group) l_coset_swap:
    1.96 -     "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
    1.97 +     "\<lbrakk>y \<in> x \<subset># H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y \<subset># H"
    1.98  proof (simp add: l_coset_def)
    1.99    assume "\<exists>h\<in>H. y = x \<otimes> h"
   1.100      and x: "x \<in> carrier G"
   1.101 @@ -487,13 +487,13 @@
   1.102  qed
   1.103  
   1.104  lemma (in group) l_coset_carrier:
   1.105 -     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
   1.106 +     "[| y \<in> x \<subset># H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
   1.107  by (auto simp add: l_coset_def m_assoc
   1.108                     subgroup.subset [THEN subsetD] subgroup.m_closed)
   1.109  
   1.110  lemma (in group) l_repr_imp_subset:
   1.111 -  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   1.112 -  shows "y <# H \<subseteq> x <# H"
   1.113 +  assumes y: "y \<in> x \<subset># H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   1.114 +  shows "y \<subset># H \<subseteq> x \<subset># H"
   1.115  proof -
   1.116    from y
   1.117    obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
   1.118 @@ -503,20 +503,20 @@
   1.119  qed
   1.120  
   1.121  lemma (in group) l_repr_independence:
   1.122 -  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   1.123 -  shows "x <# H = y <# H"
   1.124 +  assumes y: "y \<in> x \<subset># H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   1.125 +  shows "x \<subset># H = y \<subset># H"
   1.126  proof
   1.127 -  show "x <# H \<subseteq> y <# H"
   1.128 +  show "x \<subset># H \<subseteq> y \<subset># H"
   1.129      by (rule l_repr_imp_subset,
   1.130          (blast intro: l_coset_swap l_coset_carrier y x sb)+)
   1.131 -  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
   1.132 +  show "y \<subset># H \<subseteq> x \<subset># H" by (rule l_repr_imp_subset [OF y x sb])
   1.133  qed
   1.134  
   1.135  lemma (in group) setmult_subset_G:
   1.136 -     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
   1.137 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H \<subset>#> K \<subseteq> carrier G"
   1.138  by (auto simp add: set_mult_def subsetD)
   1.139  
   1.140 -lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
   1.141 +lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H \<subset>#> H = H"
   1.142  apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def)
   1.143  apply (rule_tac x = x in bexI)
   1.144  apply (rule bexI [of _ "\<one>"])
   1.145 @@ -549,41 +549,41 @@
   1.146  qed
   1.147  
   1.148  
   1.149 -subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
   1.150 +subsubsection \<open>Theorems for \<open>\<subset>#>\<close> with \<open>#>\<close> or \<open>\<subset>#\<close>.\<close>
   1.151  
   1.152  lemma (in group) setmult_rcos_assoc:
   1.153       "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   1.154 -      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
   1.155 +      \<Longrightarrow> H \<subset>#> (K #> x) = (H \<subset>#> K) #> x"
   1.156  by (force simp add: r_coset_def set_mult_def m_assoc)
   1.157  
   1.158  lemma (in group) rcos_assoc_lcos:
   1.159       "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   1.160 -      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
   1.161 +      \<Longrightarrow> (H #> x) \<subset>#> K = H \<subset>#> (x \<subset># K)"
   1.162  by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
   1.163  
   1.164  lemma (in normal) rcos_mult_step1:
   1.165       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   1.166 -      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   1.167 +      \<Longrightarrow> (H #> x) \<subset>#> (H #> y) = (H \<subset>#> (x \<subset># H)) #> y"
   1.168  by (simp add: setmult_rcos_assoc subset
   1.169                r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
   1.170  
   1.171  lemma (in normal) rcos_mult_step2:
   1.172       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   1.173 -      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   1.174 +      \<Longrightarrow> (H \<subset>#> (x \<subset># H)) #> y = (H \<subset>#> (H #> x)) #> y"
   1.175  by (insert coset_eq, simp add: normal_def)
   1.176  
   1.177  lemma (in normal) rcos_mult_step3:
   1.178       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   1.179 -      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   1.180 +      \<Longrightarrow> (H \<subset>#> (H #> x)) #> y = H #> (x \<otimes> y)"
   1.181  by (simp add: setmult_rcos_assoc coset_mult_assoc
   1.182                subgroup_mult_id normal.axioms subset normal_axioms)
   1.183  
   1.184  lemma (in normal) rcos_sum:
   1.185       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   1.186 -      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   1.187 +      \<Longrightarrow> (H #> x) \<subset>#> (H #> y) = H #> (x \<otimes> y)"
   1.188  by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   1.189  
   1.190 -lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   1.191 +lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H \<subset>#> M = M"
   1.192    \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
   1.193    by (auto simp add: RCOSETS_def subset
   1.194          setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
   1.195 @@ -645,7 +645,7 @@
   1.196  lemma (in subgroup) l_coset_eq_rcong:
   1.197    assumes "group G"
   1.198    assumes a: "a \<in> carrier G"
   1.199 -  shows "a <# H = rcong H `` {a}"
   1.200 +  shows "a \<subset># H = rcong H `` {a}"
   1.201  proof -
   1.202    interpret group G by fact
   1.203    show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   1.204 @@ -684,7 +684,7 @@
   1.205  text \<open>The relation is a congruence\<close>
   1.206  
   1.207  lemma (in normal) congruent_rcong:
   1.208 -  shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
   1.209 +  shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b \<subset># H)"
   1.210  proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
   1.211    fix a b c
   1.212    assume abrcong: "(a, b) \<in> rcong H"
   1.213 @@ -712,10 +712,10 @@
   1.214    ultimately
   1.215        have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
   1.216    from carr and this
   1.217 -     have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
   1.218 +     have "(b \<otimes> c) \<in> (a \<otimes> c) \<subset># H"
   1.219       by (simp add: lcos_module_rev[OF is_group])
   1.220    from carr and this and is_subgroup
   1.221 -     show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
   1.222 +     show "(a \<otimes> c) \<subset># H = (b \<otimes> c) \<subset># H" by (intro l_repr_independence, simp+)
   1.223  next
   1.224    fix a b c
   1.225    assume abrcong: "(a, b) \<in> rcong H"
   1.226 @@ -746,10 +746,10 @@
   1.227        have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
   1.228  
   1.229    from carr and this
   1.230 -     have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
   1.231 +     have "(c \<otimes> b) \<in> (c \<otimes> a) \<subset># H"
   1.232       by (simp add: lcos_module_rev[OF is_group])
   1.233    from carr and this and is_subgroup
   1.234 -     show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
   1.235 +     show "(c \<otimes> a) \<subset># H = (c \<otimes> b) \<subset># H" by (intro l_repr_independence, simp+)
   1.236  qed
   1.237  
   1.238  
   1.239 @@ -835,7 +835,7 @@
   1.240     where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   1.241  
   1.242  lemma (in normal) setmult_closed:
   1.243 -     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   1.244 +     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 \<subset>#> K2 \<in> rcosets H"
   1.245  by (auto simp add: rcos_sum RCOSETS_def)
   1.246  
   1.247  lemma (in normal) setinv_closed:
   1.248 @@ -844,7 +844,7 @@
   1.249  
   1.250  lemma (in normal) rcosets_assoc:
   1.251       "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   1.252 -      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   1.253 +      \<Longrightarrow> M1 \<subset>#> M2 \<subset>#> M3 = M1 \<subset>#> (M2 \<subset>#> M3)"
   1.254  by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   1.255  
   1.256  lemma (in subgroup) subgroup_in_rcosets:
   1.257 @@ -859,7 +859,7 @@
   1.258  qed
   1.259  
   1.260  lemma (in normal) rcosets_inv_mult_group_eq:
   1.261 -     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   1.262 +     "M \<in> rcosets H \<Longrightarrow> set_inv M \<subset>#> M = H"
   1.263  by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
   1.264  
   1.265  theorem (in normal) factorgroup_is_group:
   1.266 @@ -874,7 +874,7 @@
   1.267  apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
   1.268  done
   1.269  
   1.270 -lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   1.271 +lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X \<subset>#>\<^bsub>G\<^esub> X'"
   1.272    by (simp add: FactGroup_def) 
   1.273  
   1.274  lemma (in normal) inv_FactGroup:
   1.275 @@ -951,11 +951,11 @@
   1.276    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   1.277      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   1.278      by (force simp add: kernel_def r_coset_def image_def)+
   1.279 -  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   1.280 +  hence "h ` (X \<subset>#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   1.281      by (auto dest!: FactGroup_nonempty intro!: image_eqI
   1.282               simp add: set_mult_def 
   1.283                         subsetD [OF Xsub] subsetD [OF X'sub]) 
   1.284 -  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   1.285 +  then show "the_elem (h ` (X \<subset>#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   1.286      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   1.287  qed
   1.288  
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Sat Dec 17 15:22:00 2016 +0100
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sat Dec 17 15:22:13 2016 +0100
     2.3 @@ -1918,7 +1918,7 @@
     2.4      and afs: "wfactors G as a"
     2.5      and bfs: "wfactors G bs b"
     2.6      and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
     2.7 -  shows "fmset G as \<le># fmset G bs"
     2.8 +  shows "fmset G as \<subseteq># fmset G bs"
     2.9    using ab
    2.10  proof (elim dividesE)
    2.11    fix c
    2.12 @@ -1935,7 +1935,7 @@
    2.13  qed
    2.14  
    2.15  lemma (in comm_monoid_cancel) fmsubset_divides:
    2.16 -  assumes msubset: "fmset G as \<le># fmset G bs"
    2.17 +  assumes msubset: "fmset G as \<subseteq># fmset G bs"
    2.18      and afs: "wfactors G as a"
    2.19      and bfs: "wfactors G bs b"
    2.20      and acarr: "a \<in> carrier G"
    2.21 @@ -1988,7 +1988,7 @@
    2.22      and "b \<in> carrier G"
    2.23      and "set as \<subseteq> carrier G"
    2.24      and "set bs \<subseteq> carrier G"
    2.25 -  shows "a divides b = (fmset G as \<le># fmset G bs)"
    2.26 +  shows "a divides b = (fmset G as \<subseteq># fmset G bs)"
    2.27    using assms
    2.28    by (blast intro: divides_fmsubset fmsubset_divides)
    2.29  
    2.30 @@ -1996,7 +1996,7 @@
    2.31  text \<open>Proper factors on multisets\<close>
    2.32  
    2.33  lemma (in factorial_monoid) fmset_properfactor:
    2.34 -  assumes asubb: "fmset G as \<le># fmset G bs"
    2.35 +  assumes asubb: "fmset G as \<subseteq># fmset G bs"
    2.36      and anb: "fmset G as \<noteq> fmset G bs"
    2.37      and "wfactors G as a"
    2.38      and "wfactors G bs b"
    2.39 @@ -2009,7 +2009,7 @@
    2.40     apply (rule fmsubset_divides[of as bs], fact+)
    2.41  proof
    2.42    assume "b divides a"
    2.43 -  then have "fmset G bs \<le># fmset G as"
    2.44 +  then have "fmset G bs \<subseteq># fmset G as"
    2.45      by (rule divides_fmsubset) fact+
    2.46    with asubb have "fmset G as = fmset G bs"
    2.47      by (rule subset_mset.antisym)
    2.48 @@ -2024,7 +2024,7 @@
    2.49      and "b \<in> carrier G"
    2.50      and "set as \<subseteq> carrier G"
    2.51      and "set bs \<subseteq> carrier G"
    2.52 -  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
    2.53 +  shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
    2.54    using pf
    2.55    apply (elim properfactorE)
    2.56    apply rule
    2.57 @@ -2334,11 +2334,11 @@
    2.58    have "c gcdof a b"
    2.59    proof (simp add: isgcd_def, safe)
    2.60      from csmset
    2.61 -    have "fmset G cs \<le># fmset G as"
    2.62 +    have "fmset G cs \<subseteq># fmset G as"
    2.63        by (simp add: multiset_inter_def subset_mset_def)
    2.64      then show "c divides a" by (rule fmsubset_divides) fact+
    2.65    next
    2.66 -    from csmset have "fmset G cs \<le># fmset G bs"
    2.67 +    from csmset have "fmset G cs \<subseteq># fmset G bs"
    2.68        by (simp add: multiset_inter_def subseteq_mset_def, force)
    2.69      then show "c divides b"
    2.70        by (rule fmsubset_divides) fact+
    2.71 @@ -2350,14 +2350,14 @@
    2.72        by blast
    2.73  
    2.74      assume "y divides a"
    2.75 -    then have ya: "fmset G ys \<le># fmset G as"
    2.76 +    then have ya: "fmset G ys \<subseteq># fmset G as"
    2.77        by (rule divides_fmsubset) fact+
    2.78  
    2.79      assume "y divides b"
    2.80 -    then have yb: "fmset G ys \<le># fmset G bs"
    2.81 +    then have yb: "fmset G ys \<subseteq># fmset G bs"
    2.82        by (rule divides_fmsubset) fact+
    2.83  
    2.84 -    from ya yb csmset have "fmset G ys \<le># fmset G cs"
    2.85 +    from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"
    2.86        by (simp add: subset_mset_def)
    2.87      then show "y divides c"
    2.88        by (rule fmsubset_divides) fact+
    2.89 @@ -2420,12 +2420,12 @@
    2.90  
    2.91    have "c lcmof a b"
    2.92    proof (simp add: islcm_def, safe)
    2.93 -    from csmset have "fmset G as \<le># fmset G cs"
    2.94 +    from csmset have "fmset G as \<subseteq># fmset G cs"
    2.95        by (simp add: subseteq_mset_def, force)
    2.96      then show "a divides c"
    2.97        by (rule fmsubset_divides) fact+
    2.98    next
    2.99 -    from csmset have "fmset G bs \<le># fmset G cs"
   2.100 +    from csmset have "fmset G bs \<subseteq># fmset G cs"
   2.101        by (simp add: subset_mset_def)
   2.102      then show "b divides c"
   2.103        by (rule fmsubset_divides) fact+
   2.104 @@ -2437,14 +2437,14 @@
   2.105        by blast
   2.106  
   2.107      assume "a divides y"
   2.108 -    then have ya: "fmset G as \<le># fmset G ys"
   2.109 +    then have ya: "fmset G as \<subseteq># fmset G ys"
   2.110        by (rule divides_fmsubset) fact+
   2.111  
   2.112      assume "b divides y"
   2.113 -    then have yb: "fmset G bs \<le># fmset G ys"
   2.114 +    then have yb: "fmset G bs \<subseteq># fmset G ys"
   2.115        by (rule divides_fmsubset) fact+
   2.116  
   2.117 -    from ya yb csmset have "fmset G cs \<le># fmset G ys"
   2.118 +    from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"
   2.119        apply (simp add: subseteq_mset_def, clarify)
   2.120        apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
   2.121         apply simp
     3.1 --- a/src/HOL/Library/DAList_Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
     3.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     3.3 @@ -228,17 +228,17 @@
     3.4    by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
     3.5  
     3.6  
     3.7 -lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
     3.8 +lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
     3.9    by (metis equal_multiset_def subset_mset.eq_iff)
    3.10  
    3.11  text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
    3.12  With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
    3.13  Here is a more efficient version:\<close>
    3.14 -lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
    3.15 +lemma mset_less[code]: "xs \<subset># (ys :: 'a multiset) \<longleftrightarrow> xs \<subseteq># ys \<and> \<not> ys \<subseteq># xs"
    3.16    by (rule subset_mset.less_le_not_le)
    3.17  
    3.18  lemma mset_less_eq_Bag0:
    3.19 -  "Bag xs \<le># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    3.20 +  "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    3.21      (is "?lhs \<longleftrightarrow> ?rhs")
    3.22  proof
    3.23    assume ?lhs
    3.24 @@ -255,7 +255,7 @@
    3.25  qed
    3.26  
    3.27  lemma mset_less_eq_Bag [code]:
    3.28 -  "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    3.29 +  "Bag xs \<subseteq># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    3.30  proof -
    3.31    {
    3.32      fix x n
     4.1 --- a/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     4.3 @@ -528,7 +528,7 @@
     4.4    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     4.5      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
     4.6  
     4.7 -interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
     4.8 +interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
     4.9    by standard
    4.10      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    4.11  
    4.12 @@ -547,7 +547,7 @@
    4.13     apply (auto intro: multiset_eq_iff [THEN iffD2])
    4.14    done
    4.15  
    4.16 -interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
    4.17 +interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
    4.18    by standard (simp, fact mset_subset_eq_exists_conv)
    4.19      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    4.20  
    4.21 @@ -628,8 +628,8 @@
    4.22  lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
    4.23    by (simp only: subset_mset.not_less_zero)
    4.24  
    4.25 -lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
    4.26 -by(auto intro: subset_mset.gr_zeroI)
    4.27 +lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
    4.28 +  by (auto intro: subset_mset.gr_zeroI)
    4.29  
    4.30  lemma empty_le: "{#} \<subseteq># A"
    4.31    by (fact subset_mset.zero_le)
     5.1 --- a/src/HOL/Library/Multiset_Order.thy	Sat Dec 17 15:22:00 2016 +0100
     5.2 +++ b/src/HOL/Library/Multiset_Order.thy	Sat Dec 17 15:22:13 2016 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4  
     5.5  definition less_multiset\<^sub>D\<^sub>M where
     5.6    "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
     5.7 -   (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
     5.8 +   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
     5.9  
    5.10  
    5.11  text \<open>The Huet--Oppen ordering:\<close>
    5.12 @@ -123,11 +123,11 @@
    5.13  proof -
    5.14    assume "less_multiset\<^sub>D\<^sub>M M N"
    5.15    then obtain X Y where
    5.16 -    "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.17 +    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.18      unfolding less_multiset\<^sub>D\<^sub>M_def by blast
    5.19    then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
    5.20      by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
    5.21 -  with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
    5.22 +  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
    5.23      by (metis subset_mset.diff_add)
    5.24  qed
    5.25  
    5.26 @@ -140,7 +140,7 @@
    5.27    define X where "X = N - M"
    5.28    define Y where "Y = M - N"
    5.29    from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
    5.30 -  from z show "X \<le># N" unfolding X_def by auto
    5.31 +  from z show "X \<subseteq># N" unfolding X_def by auto
    5.32    show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
    5.33    show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.34    proof (intro allI impI)
    5.35 @@ -175,7 +175,7 @@
    5.36  lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
    5.37  
    5.38  lemma subset_eq_imp_le_multiset:
    5.39 -  shows "M \<le># N \<Longrightarrow> M \<le> N"
    5.40 +  shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
    5.41    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
    5.42    by (simp add: less_le_not_le subseteq_mset_def)
    5.43  
    5.44 @@ -201,7 +201,7 @@
    5.45  lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
    5.46    using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
    5.47  
    5.48 -lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    5.49 +lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    5.50    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    5.51  
    5.52  instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
     6.1 --- a/src/HOL/Library/Permutation.thy	Sat Dec 17 15:22:00 2016 +0100
     6.2 +++ b/src/HOL/Library/Permutation.thy	Sat Dec 17 15:22:13 2016 +0100
     6.3 @@ -134,7 +134,7 @@
     6.4    apply simp
     6.5    done
     6.6  
     6.7 -proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     6.8 +proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     6.9    apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
    6.10    apply (insert surj_mset)
    6.11    apply (drule surjD)