--- a/src/HOL/Algebra/Coset.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Algebra/Coset.thy Sat Dec 17 15:22:13 2016 +0100
@@ -15,16 +15,16 @@
where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
definition
- l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60)
- where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
+ l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "\<subset>#\<index>" 60)
+ where "a \<subset>#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
definition
RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80)
where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
definition
- set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
- where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
+ set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "\<subset>#>\<index>" 60)
+ where "H \<subset>#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
definition
SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("set'_inv\<index> _" [81] 80)
@@ -32,7 +32,7 @@
locale normal = subgroup + group +
- assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
+ assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x \<subset># H)"
abbreviation
normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where
@@ -287,7 +287,7 @@
lemma (in monoid) set_mult_closed:
assumes Acarr: "A \<subseteq> carrier G"
and Bcarr: "B \<subseteq> carrier G"
- shows "A <#> B \<subseteq> carrier G"
+ shows "A \<subset>#> B \<subseteq> carrier G"
apply rule apply (simp add: set_mult_def, clarsimp)
proof -
fix a b
@@ -306,7 +306,7 @@
lemma (in comm_group) mult_subgroups:
assumes subH: "subgroup H G"
and subK: "subgroup K G"
- shows "subgroup (H <#> K) G"
+ shows "subgroup (H \<subset>#> K) G"
apply (rule subgroup.intro)
apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
apply (simp add: set_mult_def) apply clarsimp defer 1
@@ -351,7 +351,7 @@
assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
and xixH: "(inv x \<otimes> x') \<in> H"
- shows "x' \<in> x <# H"
+ shows "x' \<in> x \<subset># H"
proof -
interpret group G by fact
from xixH
@@ -375,7 +375,7 @@
have "x \<otimes> h = x'" by simp
from this[symmetric] and hH
- show "x' \<in> x <# H"
+ show "x' \<in> x \<subset># H"
unfolding l_coset_def
by fast
qed
@@ -387,7 +387,7 @@
by (simp add: normal_def subgroup_def)
lemma (in group) normalI:
- "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
+ "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x \<subset># H) \<Longrightarrow> H \<lhd> G"
by (simp add: normal_def normal_axioms_def is_group)
lemma (in normal) inv_op_closed1:
@@ -460,18 +460,18 @@
lemma (in group) lcos_m_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> g <# (h <# M) = (g \<otimes> h) <# M"
+ ==> g \<subset># (h \<subset># M) = (g \<otimes> h) \<subset># M"
by (force simp add: l_coset_def m_assoc)
-lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
+lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> \<subset># M = M"
by (force simp add: l_coset_def)
lemma (in group) l_coset_subset_G:
- "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
+ "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x \<subset># H \<subseteq> carrier G"
by (auto simp add: l_coset_def subsetD)
lemma (in group) l_coset_swap:
- "\<lbrakk>y \<in> x <# H; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
+ "\<lbrakk>y \<in> x \<subset># H; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y \<subset># H"
proof (simp add: l_coset_def)
assume "\<exists>h\<in>H. y = x \<otimes> h"
and x: "x \<in> carrier G"
@@ -487,13 +487,13 @@
qed
lemma (in group) l_coset_carrier:
- "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> y \<in> carrier G"
+ "[| y \<in> x \<subset># H; x \<in> carrier G; subgroup H G |] ==> y \<in> carrier G"
by (auto simp add: l_coset_def m_assoc
subgroup.subset [THEN subsetD] subgroup.m_closed)
lemma (in group) l_repr_imp_subset:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
- shows "y <# H \<subseteq> x <# H"
+ assumes y: "y \<in> x \<subset># H" and x: "x \<in> carrier G" and sb: "subgroup H G"
+ shows "y \<subset># H \<subseteq> x \<subset># H"
proof -
from y
obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
@@ -503,20 +503,20 @@
qed
lemma (in group) l_repr_independence:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
- shows "x <# H = y <# H"
+ assumes y: "y \<in> x \<subset># H" and x: "x \<in> carrier G" and sb: "subgroup H G"
+ shows "x \<subset># H = y \<subset># H"
proof
- show "x <# H \<subseteq> y <# H"
+ show "x \<subset># H \<subseteq> y \<subset># H"
by (rule l_repr_imp_subset,
(blast intro: l_coset_swap l_coset_carrier y x sb)+)
- show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
+ show "y \<subset># H \<subseteq> x \<subset># H" by (rule l_repr_imp_subset [OF y x sb])
qed
lemma (in group) setmult_subset_G:
- "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H \<subset>#> K \<subseteq> carrier G"
by (auto simp add: set_mult_def subsetD)
-lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
+lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H \<subset>#> H = H"
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
@@ -549,41 +549,41 @@
qed
-subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
+subsubsection \<open>Theorems for \<open>\<subset>#>\<close> with \<open>#>\<close> or \<open>\<subset>#\<close>.\<close>
lemma (in group) setmult_rcos_assoc:
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
- \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
+ \<Longrightarrow> H \<subset>#> (K #> x) = (H \<subset>#> K) #> x"
by (force simp add: r_coset_def set_mult_def m_assoc)
lemma (in group) rcos_assoc_lcos:
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
+ \<Longrightarrow> (H #> x) \<subset>#> K = H \<subset>#> (x \<subset># K)"
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
lemma (in normal) rcos_mult_step1:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+ \<Longrightarrow> (H #> x) \<subset>#> (H #> y) = (H \<subset>#> (x \<subset># H)) #> y"
by (simp add: setmult_rcos_assoc subset
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
lemma (in normal) rcos_mult_step2:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
+ \<Longrightarrow> (H \<subset>#> (x \<subset># H)) #> y = (H \<subset>#> (H #> x)) #> y"
by (insert coset_eq, simp add: normal_def)
lemma (in normal) rcos_mult_step3:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
+ \<Longrightarrow> (H \<subset>#> (H #> x)) #> y = H #> (x \<otimes> y)"
by (simp add: setmult_rcos_assoc coset_mult_assoc
subgroup_mult_id normal.axioms subset normal_axioms)
lemma (in normal) rcos_sum:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
+ \<Longrightarrow> (H #> x) \<subset>#> (H #> y) = H #> (x \<otimes> y)"
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
-lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
+lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H \<subset>#> M = M"
\<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
by (auto simp add: RCOSETS_def subset
setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
@@ -645,7 +645,7 @@
lemma (in subgroup) l_coset_eq_rcong:
assumes "group G"
assumes a: "a \<in> carrier G"
- shows "a <# H = rcong H `` {a}"
+ shows "a \<subset># H = rcong H `` {a}"
proof -
interpret group G by fact
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
@@ -684,7 +684,7 @@
text \<open>The relation is a congruence\<close>
lemma (in normal) congruent_rcong:
- shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
+ shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b \<subset># H)"
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
fix a b c
assume abrcong: "(a, b) \<in> rcong H"
@@ -712,10 +712,10 @@
ultimately
have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
from carr and this
- have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
+ have "(b \<otimes> c) \<in> (a \<otimes> c) \<subset># H"
by (simp add: lcos_module_rev[OF is_group])
from carr and this and is_subgroup
- show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
+ show "(a \<otimes> c) \<subset># H = (b \<otimes> c) \<subset># H" by (intro l_repr_independence, simp+)
next
fix a b c
assume abrcong: "(a, b) \<in> rcong H"
@@ -746,10 +746,10 @@
have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
from carr and this
- have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
+ have "(c \<otimes> b) \<in> (c \<otimes> a) \<subset># H"
by (simp add: lcos_module_rev[OF is_group])
from carr and this and is_subgroup
- show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
+ show "(c \<otimes> a) \<subset># H = (c \<otimes> b) \<subset># H" by (intro l_repr_independence, simp+)
qed
@@ -835,7 +835,7 @@
where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
lemma (in normal) setmult_closed:
- "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
+ "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 \<subset>#> K2 \<in> rcosets H"
by (auto simp add: rcos_sum RCOSETS_def)
lemma (in normal) setinv_closed:
@@ -844,7 +844,7 @@
lemma (in normal) rcosets_assoc:
"\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
- \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
+ \<Longrightarrow> M1 \<subset>#> M2 \<subset>#> M3 = M1 \<subset>#> (M2 \<subset>#> M3)"
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
lemma (in subgroup) subgroup_in_rcosets:
@@ -859,7 +859,7 @@
qed
lemma (in normal) rcosets_inv_mult_group_eq:
- "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
+ "M \<in> rcosets H \<Longrightarrow> set_inv M \<subset>#> M = H"
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
theorem (in normal) factorgroup_is_group:
@@ -874,7 +874,7 @@
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
done
-lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
+lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X \<subset>#>\<^bsub>G\<^esub> X'"
by (simp add: FactGroup_def)
lemma (in normal) inv_FactGroup:
@@ -951,11 +951,11 @@
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
by (force simp add: kernel_def r_coset_def image_def)+
- hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
+ hence "h ` (X \<subset>#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
by (auto dest!: FactGroup_nonempty intro!: image_eqI
simp add: set_mult_def
subsetD [OF Xsub] subsetD [OF X'sub])
- then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+ then show "the_elem (h ` (X \<subset>#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
qed
--- a/src/HOL/Algebra/Divisibility.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Sat Dec 17 15:22:13 2016 +0100
@@ -1918,7 +1918,7 @@
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G"
- shows "fmset G as \<le># fmset G bs"
+ shows "fmset G as \<subseteq># fmset G bs"
using ab
proof (elim dividesE)
fix c
@@ -1935,7 +1935,7 @@
qed
lemma (in comm_monoid_cancel) fmsubset_divides:
- assumes msubset: "fmset G as \<le># fmset G bs"
+ assumes msubset: "fmset G as \<subseteq># fmset G bs"
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and acarr: "a \<in> carrier G"
@@ -1988,7 +1988,7 @@
and "b \<in> carrier G"
and "set as \<subseteq> carrier G"
and "set bs \<subseteq> carrier G"
- shows "a divides b = (fmset G as \<le># fmset G bs)"
+ shows "a divides b = (fmset G as \<subseteq># fmset G bs)"
using assms
by (blast intro: divides_fmsubset fmsubset_divides)
@@ -1996,7 +1996,7 @@
text \<open>Proper factors on multisets\<close>
lemma (in factorial_monoid) fmset_properfactor:
- assumes asubb: "fmset G as \<le># fmset G bs"
+ assumes asubb: "fmset G as \<subseteq># fmset G bs"
and anb: "fmset G as \<noteq> fmset G bs"
and "wfactors G as a"
and "wfactors G bs b"
@@ -2009,7 +2009,7 @@
apply (rule fmsubset_divides[of as bs], fact+)
proof
assume "b divides a"
- then have "fmset G bs \<le># fmset G as"
+ then have "fmset G bs \<subseteq># fmset G as"
by (rule divides_fmsubset) fact+
with asubb have "fmset G as = fmset G bs"
by (rule subset_mset.antisym)
@@ -2024,7 +2024,7 @@
and "b \<in> carrier G"
and "set as \<subseteq> carrier G"
and "set bs \<subseteq> carrier G"
- shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+ shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
using pf
apply (elim properfactorE)
apply rule
@@ -2334,11 +2334,11 @@
have "c gcdof a b"
proof (simp add: isgcd_def, safe)
from csmset
- have "fmset G cs \<le># fmset G as"
+ have "fmset G cs \<subseteq># fmset G as"
by (simp add: multiset_inter_def subset_mset_def)
then show "c divides a" by (rule fmsubset_divides) fact+
next
- from csmset have "fmset G cs \<le># fmset G bs"
+ from csmset have "fmset G cs \<subseteq># fmset G bs"
by (simp add: multiset_inter_def subseteq_mset_def, force)
then show "c divides b"
by (rule fmsubset_divides) fact+
@@ -2350,14 +2350,14 @@
by blast
assume "y divides a"
- then have ya: "fmset G ys \<le># fmset G as"
+ then have ya: "fmset G ys \<subseteq># fmset G as"
by (rule divides_fmsubset) fact+
assume "y divides b"
- then have yb: "fmset G ys \<le># fmset G bs"
+ then have yb: "fmset G ys \<subseteq># fmset G bs"
by (rule divides_fmsubset) fact+
- from ya yb csmset have "fmset G ys \<le># fmset G cs"
+ from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"
by (simp add: subset_mset_def)
then show "y divides c"
by (rule fmsubset_divides) fact+
@@ -2420,12 +2420,12 @@
have "c lcmof a b"
proof (simp add: islcm_def, safe)
- from csmset have "fmset G as \<le># fmset G cs"
+ from csmset have "fmset G as \<subseteq># fmset G cs"
by (simp add: subseteq_mset_def, force)
then show "a divides c"
by (rule fmsubset_divides) fact+
next
- from csmset have "fmset G bs \<le># fmset G cs"
+ from csmset have "fmset G bs \<subseteq># fmset G cs"
by (simp add: subset_mset_def)
then show "b divides c"
by (rule fmsubset_divides) fact+
@@ -2437,14 +2437,14 @@
by blast
assume "a divides y"
- then have ya: "fmset G as \<le># fmset G ys"
+ then have ya: "fmset G as \<subseteq># fmset G ys"
by (rule divides_fmsubset) fact+
assume "b divides y"
- then have yb: "fmset G bs \<le># fmset G ys"
+ then have yb: "fmset G bs \<subseteq># fmset G ys"
by (rule divides_fmsubset) fact+
- from ya yb csmset have "fmset G cs \<le># fmset G ys"
+ from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"
apply (simp add: subseteq_mset_def, clarify)
apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
apply simp
--- a/src/HOL/Library/DAList_Multiset.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Sat Dec 17 15:22:13 2016 +0100
@@ -228,17 +228,17 @@
by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
-lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
+lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
by (metis equal_multiset_def subset_mset.eq_iff)
text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
With equality implemented by \<open>\<le>\<close>, this leads to three calls of \<open>\<le>\<close>.
Here is a more efficient version:\<close>
-lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
+lemma mset_less[code]: "xs \<subset># (ys :: 'a multiset) \<longleftrightarrow> xs \<subseteq># ys \<and> \<not> ys \<subseteq># xs"
by (rule subset_mset.less_le_not_le)
lemma mset_less_eq_Bag0:
- "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)"
+ "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)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs
@@ -255,7 +255,7 @@
qed
lemma mset_less_eq_Bag [code]:
- "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
+ "Bag xs \<subseteq># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
proof -
{
fix x n
--- a/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:13 2016 +0100
@@ -528,7 +528,7 @@
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
-interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
+interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
by standard
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -547,7 +547,7 @@
apply (auto intro: multiset_eq_iff [THEN iffD2])
done
-interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
by standard (simp, fact mset_subset_eq_exists_conv)
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -628,8 +628,8 @@
lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
by (simp only: subset_mset.not_less_zero)
-lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
-by(auto intro: subset_mset.gr_zeroI)
+lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
+ by (auto intro: subset_mset.gr_zeroI)
lemma empty_le: "{#} \<subseteq># A"
by (fact subset_mset.zero_le)
--- a/src/HOL/Library/Multiset_Order.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sat Dec 17 15:22:13 2016 +0100
@@ -49,7 +49,7 @@
definition less_multiset\<^sub>D\<^sub>M where
"less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
- (\<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)))"
+ (\<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)))"
text \<open>The Huet--Oppen ordering:\<close>
@@ -123,11 +123,11 @@
proof -
assume "less_multiset\<^sub>D\<^sub>M M N"
then obtain X Y where
- "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)"
+ "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)"
unfolding less_multiset\<^sub>D\<^sub>M_def by blast
then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
- with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
+ with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
by (metis subset_mset.diff_add)
qed
@@ -140,7 +140,7 @@
define X where "X = N - M"
define Y where "Y = M - N"
from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
- from z show "X \<le># N" unfolding X_def by auto
+ from z show "X \<subseteq># N" unfolding X_def by auto
show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
proof (intro allI impI)
@@ -175,7 +175,7 @@
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
lemma subset_eq_imp_le_multiset:
- shows "M \<le># N \<Longrightarrow> M \<le> N"
+ shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
by (simp add: less_le_not_le subseteq_mset_def)
@@ -201,7 +201,7 @@
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
-lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
+lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
--- a/src/HOL/Library/Permutation.thy Sat Dec 17 15:22:00 2016 +0100
+++ b/src/HOL/Library/Permutation.thy Sat Dec 17 15:22:13 2016 +0100
@@ -134,7 +134,7 @@
apply simp
done
-proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
apply (insert surj_mset)
apply (drule surjD)