# HG changeset patch # User haftmann # Date 1481984533 -3600 # Node ID 8355a6e2df79a562656ceebafaff04e429f88554 # Parent 1d25ca7187905f3a8bf1225c337774daccd688e6 standardized notation diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Algebra/Coset.thy --- 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 = (\h\H. {h \\<^bsub>G\<^esub> a})" definition - l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<#\" 60) - where "a <#\<^bsub>G\<^esub> H = (\h\H. {a \\<^bsub>G\<^esub> h})" + l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "\#\" 60) + where "a \#\<^bsub>G\<^esub> H = (\h\H. {a \\<^bsub>G\<^esub> h})" definition RCOSETS :: "[_, 'a set] \ ('a set)set" ("rcosets\ _" [81] 80) where "rcosets\<^bsub>G\<^esub> H = (\a\carrier G. {H #>\<^bsub>G\<^esub> a})" definition - set_mult :: "[_, 'a set ,'a set] \ 'a set" (infixl "<#>\" 60) - where "H <#>\<^bsub>G\<^esub> K = (\h\H. \k\K. {h \\<^bsub>G\<^esub> k})" + set_mult :: "[_, 'a set ,'a set] \ 'a set" (infixl "\#>\" 60) + where "H \#>\<^bsub>G\<^esub> K = (\h\H. \k\K. {h \\<^bsub>G\<^esub> k})" definition SET_INV :: "[_,'a set] \ 'a set" ("set'_inv\ _" [81] 80) @@ -32,7 +32,7 @@ locale normal = subgroup + group + - assumes coset_eq: "(\x \ carrier G. H #> x = x <# H)" + assumes coset_eq: "(\x \ carrier G. H #> x = x \# H)" abbreviation normal_rel :: "['a set, ('a, 'b) monoid_scheme] \ bool" (infixl "\" 60) where @@ -287,7 +287,7 @@ lemma (in monoid) set_mult_closed: assumes Acarr: "A \ carrier G" and Bcarr: "B \ carrier G" - shows "A <#> B \ carrier G" + shows "A \#> B \ 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 \#> 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 \ carrier G" "x' \ carrier G" and xixH: "(inv x \ x') \ H" - shows "x' \ x <# H" + shows "x' \ x \# H" proof - interpret group G by fact from xixH @@ -375,7 +375,7 @@ have "x \ h = x'" by simp from this[symmetric] and hH - show "x' \ x <# H" + show "x' \ x \# 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 \ (\x \ carrier G. H #> x = x <# H) \ H \ G" + "subgroup H G \ (\x \ carrier G. H #> x = x \# H) \ H \ 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 \ carrier G; g \ carrier G; h \ carrier G |] - ==> g <# (h <# M) = (g \ h) <# M" + ==> g \# (h \# M) = (g \ h) \# M" by (force simp add: l_coset_def m_assoc) -lemma (in group) lcos_mult_one: "M \ carrier G ==> \ <# M = M" +lemma (in group) lcos_mult_one: "M \ carrier G ==> \ \# M = M" by (force simp add: l_coset_def) lemma (in group) l_coset_subset_G: - "[| H \ carrier G; x \ carrier G |] ==> x <# H \ carrier G" + "[| H \ carrier G; x \ carrier G |] ==> x \# H \ carrier G" by (auto simp add: l_coset_def subsetD) lemma (in group) l_coset_swap: - "\y \ x <# H; x \ carrier G; subgroup H G\ \ x \ y <# H" + "\y \ x \# H; x \ carrier G; subgroup H G\ \ x \ y \# H" proof (simp add: l_coset_def) assume "\h\H. y = x \ h" and x: "x \ carrier G" @@ -487,13 +487,13 @@ qed lemma (in group) l_coset_carrier: - "[| y \ x <# H; x \ carrier G; subgroup H G |] ==> y \ carrier G" + "[| y \ x \# H; x \ carrier G; subgroup H G |] ==> y \ 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 \ x <# H" and x: "x \ carrier G" and sb: "subgroup H G" - shows "y <# H \ x <# H" + assumes y: "y \ x \# H" and x: "x \ carrier G" and sb: "subgroup H G" + shows "y \# H \ x \# H" proof - from y obtain h' where "h' \ H" "x \ h' = y" by (auto simp add: l_coset_def) @@ -503,20 +503,20 @@ qed lemma (in group) l_repr_independence: - assumes y: "y \ x <# H" and x: "x \ carrier G" and sb: "subgroup H G" - shows "x <# H = y <# H" + assumes y: "y \ x \# H" and x: "x \ carrier G" and sb: "subgroup H G" + shows "x \# H = y \# H" proof - show "x <# H \ y <# H" + show "x \# H \ y \# H" by (rule l_repr_imp_subset, (blast intro: l_coset_swap l_coset_carrier y x sb)+) - show "y <# H \ x <# H" by (rule l_repr_imp_subset [OF y x sb]) + show "y \# H \ x \# H" by (rule l_repr_imp_subset [OF y x sb]) qed lemma (in group) setmult_subset_G: - "\H \ carrier G; K \ carrier G\ \ H <#> K \ carrier G" + "\H \ carrier G; K \ carrier G\ \ H \#> K \ carrier G" by (auto simp add: set_mult_def subsetD) -lemma (in group) subgroup_mult_id: "subgroup H G \ H <#> H = H" +lemma (in group) subgroup_mult_id: "subgroup H G \ H \#> 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 _ "\"]) @@ -549,41 +549,41 @@ qed -subsubsection \Theorems for \<#>\ with \#>\ or \<#\.\ +subsubsection \Theorems for \\#>\ with \#>\ or \\#\.\ lemma (in group) setmult_rcos_assoc: "\H \ carrier G; K \ carrier G; x \ carrier G\ - \ H <#> (K #> x) = (H <#> K) #> x" + \ H \#> (K #> x) = (H \#> K) #> x" by (force simp add: r_coset_def set_mult_def m_assoc) lemma (in group) rcos_assoc_lcos: "\H \ carrier G; K \ carrier G; x \ carrier G\ - \ (H #> x) <#> K = H <#> (x <# K)" + \ (H #> x) \#> K = H \#> (x \# K)" by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc) lemma (in normal) rcos_mult_step1: "\x \ carrier G; y \ carrier G\ - \ (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" + \ (H #> x) \#> (H #> y) = (H \#> (x \# 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: "\x \ carrier G; y \ carrier G\ - \ (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y" + \ (H \#> (x \# H)) #> y = (H \#> (H #> x)) #> y" by (insert coset_eq, simp add: normal_def) lemma (in normal) rcos_mult_step3: "\x \ carrier G; y \ carrier G\ - \ (H <#> (H #> x)) #> y = H #> (x \ y)" + \ (H \#> (H #> x)) #> y = H #> (x \ y)" by (simp add: setmult_rcos_assoc coset_mult_assoc subgroup_mult_id normal.axioms subset normal_axioms) lemma (in normal) rcos_sum: "\x \ carrier G; y \ carrier G\ - \ (H #> x) <#> (H #> y) = H #> (x \ y)" + \ (H #> x) \#> (H #> y) = H #> (x \ y)" by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3) -lemma (in normal) rcosets_mult_eq: "M \ rcosets H \ H <#> M = M" +lemma (in normal) rcosets_mult_eq: "M \ rcosets H \ H \#> M = M" \ \generalizes \subgroup_mult_id\\ 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 \ carrier G" - shows "a <# H = rcong H `` {a}" + shows "a \# 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 \The relation is a congruence\ lemma (in normal) congruent_rcong: - shows "congruent2 (rcong H) (rcong H) (\a b. a \ b <# H)" + shows "congruent2 (rcong H) (rcong H) (\a b. a \ b \# H)" proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group) fix a b c assume abrcong: "(a, b) \ rcong H" @@ -712,10 +712,10 @@ ultimately have "(inv (a \ c)) \ (b \ c) \ H" by simp from carr and this - have "(b \ c) \ (a \ c) <# H" + have "(b \ c) \ (a \ c) \# H" by (simp add: lcos_module_rev[OF is_group]) from carr and this and is_subgroup - show "(a \ c) <# H = (b \ c) <# H" by (intro l_repr_independence, simp+) + show "(a \ c) \# H = (b \ c) \# H" by (intro l_repr_independence, simp+) next fix a b c assume abrcong: "(a, b) \ rcong H" @@ -746,10 +746,10 @@ have "inv (c \ a) \ (c \ b) \ H" by simp from carr and this - have "(c \ b) \ (c \ a) <# H" + have "(c \ b) \ (c \ a) \# H" by (simp add: lcos_module_rev[OF is_group]) from carr and this and is_subgroup - show "(c \ a) <# H = (c \ b) <# H" by (intro l_repr_independence, simp+) + show "(c \ a) \# H = (c \ b) \# H" by (intro l_repr_independence, simp+) qed @@ -835,7 +835,7 @@ where "FactGroup G H = \carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\" lemma (in normal) setmult_closed: - "\K1 \ rcosets H; K2 \ rcosets H\ \ K1 <#> K2 \ rcosets H" + "\K1 \ rcosets H; K2 \ rcosets H\ \ K1 \#> K2 \ rcosets H" by (auto simp add: rcos_sum RCOSETS_def) lemma (in normal) setinv_closed: @@ -844,7 +844,7 @@ lemma (in normal) rcosets_assoc: "\M1 \ rcosets H; M2 \ rcosets H; M3 \ rcosets H\ - \ M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)" + \ M1 \#> M2 \#> M3 = M1 \#> (M2 \#> 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 \ rcosets H \ set_inv M <#> M = H" + "M \ rcosets H \ set_inv M \#> 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 \\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'" +lemma mult_FactGroup [simp]: "X \\<^bsub>(G Mod H)\<^esub> X' = X \#>\<^bsub>G\<^esub> X'" by (simp add: FactGroup_def) lemma (in normal) inv_FactGroup: @@ -951,11 +951,11 @@ hence all: "\x\X. h x = h g" "\x\X'. h x = h g'" and Xsub: "X \ carrier G" and X'sub: "X' \ carrier G" by (force simp add: kernel_def r_coset_def image_def)+ - hence "h ` (X <#> X') = {h g \\<^bsub>H\<^esub> h g'}" using X X' + hence "h ` (X \#> X') = {h g \\<^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) \\<^bsub>H\<^esub> the_elem (h ` X')" + then show "the_elem (h ` (X \#> X')) = the_elem (h ` X) \\<^bsub>H\<^esub> the_elem (h ` X')" by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique) qed diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Algebra/Divisibility.thy --- 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 \ carrier G" "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" - shows "fmset G as \# fmset G bs" + shows "fmset G as \# 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 \# fmset G bs" + assumes msubset: "fmset G as \# fmset G bs" and afs: "wfactors G as a" and bfs: "wfactors G bs b" and acarr: "a \ carrier G" @@ -1988,7 +1988,7 @@ and "b \ carrier G" and "set as \ carrier G" and "set bs \ carrier G" - shows "a divides b = (fmset G as \# fmset G bs)" + shows "a divides b = (fmset G as \# fmset G bs)" using assms by (blast intro: divides_fmsubset fmsubset_divides) @@ -1996,7 +1996,7 @@ text \Proper factors on multisets\ lemma (in factorial_monoid) fmset_properfactor: - assumes asubb: "fmset G as \# fmset G bs" + assumes asubb: "fmset G as \# fmset G bs" and anb: "fmset G as \ 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 \# fmset G as" + then have "fmset G bs \# 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 \ carrier G" and "set as \ carrier G" and "set bs \ carrier G" - shows "fmset G as \# fmset G bs \ fmset G as \ fmset G bs" + shows "fmset G as \# fmset G bs \ fmset G as \ 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 \# fmset G as" + have "fmset G cs \# 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 \# fmset G bs" + from csmset have "fmset G cs \# 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 \# fmset G as" + then have ya: "fmset G ys \# fmset G as" by (rule divides_fmsubset) fact+ assume "y divides b" - then have yb: "fmset G ys \# fmset G bs" + then have yb: "fmset G ys \# fmset G bs" by (rule divides_fmsubset) fact+ - from ya yb csmset have "fmset G ys \# fmset G cs" + from ya yb csmset have "fmset G ys \# 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 \# fmset G cs" + from csmset have "fmset G as \# 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 \# fmset G cs" + from csmset have "fmset G bs \# 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 \# fmset G ys" + then have ya: "fmset G as \# fmset G ys" by (rule divides_fmsubset) fact+ assume "b divides y" - then have yb: "fmset G bs \# fmset G ys" + then have yb: "fmset G bs \# fmset G ys" by (rule divides_fmsubset) fact+ - from ya yb csmset have "fmset G cs \# fmset G ys" + from ya yb csmset have "fmset G cs \# 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 diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Library/DAList_Multiset.thy --- 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 \ m1 \# m2 \ m2 \# m1" +lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \ m1 \# m2 \ m2 \# m1" by (metis equal_multiset_def subset_mset.eq_iff) text \By default the code for \<\ is @{prop"xs < ys \ xs \ ys \ \ xs = ys"}. With equality implemented by \\\, this leads to three calls of \\\. Here is a more efficient version:\ -lemma mset_less[code]: "xs <# (ys :: 'a multiset) \ xs \# ys \ \ ys \# xs" +lemma mset_less[code]: "xs \# (ys :: 'a multiset) \ xs \# ys \ \ ys \# xs" by (rule subset_mset.less_le_not_le) lemma mset_less_eq_Bag0: - "Bag xs \# A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" + "Bag xs \# A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" (is "?lhs \ ?rhs") proof assume ?lhs @@ -255,7 +255,7 @@ qed lemma mset_less_eq_Bag [code]: - "Bag xs \# (A :: 'a multiset) \ (\(x, n) \ set (DAList.impl_of xs). n \ count A x)" + "Bag xs \# (A :: 'a multiset) \ (\(x, n) \ set (DAList.impl_of xs). n \ count A x)" proof - { fix x n diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Library/Multiset.thy --- 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) \ \FIXME: avoid junk stemming from type class interpretation\ -interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \#" "op <#" +interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \#" "op \#" by standard \ \FIXME: avoid junk stemming from type class interpretation\ @@ -547,7 +547,7 @@ apply (auto intro: multiset_eq_iff [THEN iffD2]) done -interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \#" "op <#" "op -" +interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \#" "op \#" "op -" by standard (simp, fact mset_subset_eq_exists_conv) \ \FIXME: avoid junk stemming from type class interpretation\ @@ -628,8 +628,8 @@ lemma mset_subset_of_empty[simp]: "A \# {#} \ 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]: "{#} \# add_mset x M" + by (auto intro: subset_mset.gr_zeroI) lemma empty_le: "{#} \# A" by (fact subset_mset.zero_le) diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Library/Multiset_Order.thy --- 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 \ - (\X Y. X \ {#} \ X \# N \ M = (N - X) + Y \ (\k. k \# Y \ (\a. a \# X \ k < a)))" + (\X Y. X \ {#} \ X \# N \ M = (N - X) + Y \ (\k. k \# Y \ (\a. a \# X \ k < a)))" text \The Huet--Oppen ordering:\ @@ -123,11 +123,11 @@ proof - assume "less_multiset\<^sub>D\<^sub>M M N" then obtain X Y where - "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ k < a)" + "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ k < a)" unfolding less_multiset\<^sub>D\<^sub>M_def by blast then have "(N - X + Y, N - X + X) \ mult {(x, y). x < y}" by (intro one_step_implies_mult) (auto simp: Bex_def trans_def) - with \M = N - X + Y\ \X \# N\ show "(M, N) \ mult {(x, y). x < y}" + with \M = N - X + Y\ \X \# N\ show "(M, N) \ 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 \ {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq) - from z show "X \# N" unfolding X_def by auto + from z show "X \# 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 "\k. k \# Y \ (\a. a \# X \ 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 \# N \ M \ N" + shows "M \# N \ M \ 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]: "\ M < {#}" using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast -lemma union_le_diff_plus: "P \# M \ N < P \ M - P + N < M" +lemma union_le_diff_plus: "P \# M \ N < P \ 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 diff -r 1d25ca718790 -r 8355a6e2df79 src/HOL/Library/Permutation.thy --- 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 \# mset ys \ (\zs. xs @ zs <~~> ys)" +proposition mset_le_perm_append: "mset xs \# mset ys \ (\zs. xs @ zs <~~> ys)" apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv) apply (insert surj_mset) apply (drule surjD)