# HG changeset patch # User Mathias Fleury # Date 1433935456 -7200 # Node ID f8a513fedb310feefbd1f0283b804a3b745af31e # Parent b640770117fd727155d73f3b41b9a9bf546594a6 Renaming multiset operators < ~> <#,... diff -r b640770117fd -r f8a513fedb31 NEWS --- a/NEWS Mon Jun 08 22:04:19 2015 +0200 +++ b/NEWS Wed Jun 10 13:24:16 2015 +0200 @@ -47,6 +47,24 @@ separate constants, and infix syntax is usually not available during instantiation. +* Library/Multiset: + - Renamed multiset inclusion operators: + < ~> <# + \ ~> \# + <= ~> <=# + \ ~> \# + \ ~> \# + INCOMPATIBILITY. + - "'a multiset" is no longer an instance of the "order", + "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff", + "semilattice_inf", and "semilattice_sup" type classes. The theorems + previously provided by these type classes (directly or indirectly) + are now available through the "subset_mset" interpretation + (e.g. add_mono ~> subset_mset.add_mono). + INCOMPATIBILITY. + - Removing mset_le_def: + mset_le_def ~> subseteq_mset_def + mset_less_def ~> subset_mset_def New in Isabelle2015 (May 2015) ------------------------------ diff -r b640770117fd -r f8a513fedb31 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Wed Jun 10 13:24:16 2015 +0200 @@ -2137,7 +2137,7 @@ assumes ab: "a divides b" 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 @@ -2157,7 +2157,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" and bcarr: "b \ carrier G" and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" @@ -2193,7 +2193,7 @@ from csmset msubset have "fmset G bs = fmset G as + fmset G cs" - by (simp add: multiset_eq_iff mset_le_def) + by (simp add: multiset_eq_iff subseteq_mset_def) hence basc: "b \ a \ c" by (rule fmset_wfactors_mult) fact+ @@ -2210,7 +2210,7 @@ assumes "wfactors G as a" and "wfactors G bs b" and "a \ carrier G" 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) @@ -2218,7 +2218,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" and "a \ carrier G" and "b \ carrier G" @@ -2228,10 +2228,10 @@ apply (rule fmsubset_divides[of as bs], fact+) proof assume "b divides a" - hence "fmset G bs \ fmset G as" + hence "fmset G bs \# fmset G as" by (rule divides_fmsubset) fact+ with asubb - have "fmset G as = fmset G bs" by (rule order_antisym) + have "fmset G as = fmset G bs" by (rule subset_mset.antisym) with anb show "False" .. qed @@ -2241,7 +2241,7 @@ and "wfactors G as a" and "wfactors G bs b" and "a \ carrier G" 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 @@ -2619,13 +2619,13 @@ have "c gcdof a b" proof (simp add: isgcd_def, safe) from csmset - have "fmset G cs \ fmset G as" - by (simp add: multiset_inter_def mset_le_def) + have "fmset G cs \# fmset G as" + by (simp add: multiset_inter_def subset_mset_def) thus "c divides a" by (rule fmsubset_divides) fact+ next from csmset - have "fmset G cs \ fmset G bs" - by (simp add: multiset_inter_def mset_le_def, force) + have "fmset G cs \# fmset G bs" + by (simp add: multiset_inter_def subseteq_mset_def, force) thus "c divides b" by (rule fmsubset_divides) fact+ next fix y @@ -2637,13 +2637,13 @@ by auto assume "y divides a" - hence ya: "fmset G ys \ fmset G as" by (rule divides_fmsubset) fact+ + hence ya: "fmset G ys \# fmset G as" by (rule divides_fmsubset) fact+ assume "y divides b" - hence yb: "fmset G ys \ fmset G bs" by (rule divides_fmsubset) fact+ + hence yb: "fmset G ys \# fmset G bs" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G ys \ fmset G cs" by (simp add: mset_le_def) + have "fmset G ys \# fmset G cs" by (simp add: subset_mset_def) thus "y divides c" by (rule fmsubset_divides) fact+ qed @@ -2718,10 +2718,10 @@ have "c lcmof a b" proof (simp add: islcm_def, safe) - from csmset have "fmset G as \ fmset G cs" by (simp add: mset_le_def, force) + from csmset have "fmset G as \# fmset G cs" by (simp add: subseteq_mset_def, force) thus "a divides c" by (rule fmsubset_divides) fact+ next - from csmset have "fmset G bs \ fmset G cs" by (simp add: mset_le_def) + from csmset have "fmset G bs \# fmset G cs" by (simp add: subset_mset_def) thus "b divides c" by (rule fmsubset_divides) fact+ next fix y @@ -2733,14 +2733,14 @@ by auto assume "a divides y" - hence ya: "fmset G as \ fmset G ys" by (rule divides_fmsubset) fact+ + hence ya: "fmset G as \# fmset G ys" by (rule divides_fmsubset) fact+ assume "b divides y" - hence yb: "fmset G bs \ fmset G ys" by (rule divides_fmsubset) fact+ + hence yb: "fmset G bs \# fmset G ys" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G cs \ fmset G ys" - apply (simp add: mset_le_def, clarify) + 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 apply simp diff -r b640770117fd -r f8a513fedb31 src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/Library/DAList_Multiset.thy Wed Jun 10 13:24:16 2015 +0200 @@ -18,9 +18,9 @@ lemma [code, code del]: "minus = (minus :: 'a multiset \ _)" .. -lemma [code, code del]: "inf = (inf :: 'a multiset \ _)" .. +lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \ _)" .. -lemma [code, code del]: "sup = (sup :: 'a multiset \ _)" .. +lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \ _)" .. lemma [code, code del]: "image_mset = image_mset" .. @@ -38,9 +38,9 @@ lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" .. -lemma [code, code del]: "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset" .. +lemma [code, code del]: "subset_mset = subset_mset" .. -lemma [code, code del]: "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset" .. +lemma [code, code del]: "subseteq_mset = subseteq_mset" .. lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" .. @@ -203,21 +203,21 @@ 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" - by (metis equal_multiset_def eq_iff) +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 @{text "<"} is @{prop"xs < ys \ xs \ ys \ \ xs = ys"}. With equality implemented by @{text"\"}, this leads to three calls of @{text"\"}. Here is a more efficient version:\ -lemma mset_less[code]: "xs < (ys :: 'a multiset) \ xs \ ys \ \ ys \ xs" - by (rule less_le_not_le) +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 - then show ?rhs by (auto simp add: mset_le_def) + then show ?rhs by (auto simp add: subseteq_mset_def) next assume ?rhs show ?lhs @@ -225,12 +225,12 @@ fix x from \?rhs\ have "count_of (DAList.impl_of xs) x \ count A x" by (cases "x \ fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty) - then show "count (Bag xs) x \ count A x" by (simp add: mset_le_def) + then show "count (Bag xs) x \ count A x" by (simp add: subset_mset_def) qed 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 @@ -266,7 +266,7 @@ qed declare multiset_inter_def [code] -declare sup_multiset_def [code] +declare sup_subset_mset_def [code] declare multiset_of.simps [code] diff -r b640770117fd -r f8a513fedb31 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/Library/Multiset.thy Wed Jun 10 13:24:16 2015 +0200 @@ -280,157 +280,137 @@ subsubsection {* Pointwise ordering induced by count *} -instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le -begin - -lift_definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" is "\ A B. (\a. A a \ B a)" . - -lemmas mset_le_def = less_eq_multiset_def - -definition less_multiset :: "'a multiset \ 'a multiset \ bool" where - mset_less_def: "(A::'a multiset) < B \ A \ B \ A \ B" - -instance - by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym) - -end - -abbreviation less_mset :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where - "A <# B \ A < B" -abbreviation (xsymbols) subset_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where - "A \# B \ A < B" - -abbreviation less_eq_mset :: "'a multiset \ 'a multiset \ bool" (infix "<=#" 50) where - "A <=# B \ A \ B" -abbreviation (xsymbols) leq_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where - "A \# B \ A \ B" -abbreviation (xsymbols) subseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where - "A \# B \ A \ B" +definition subseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix "<=#" 50) where +"subseteq_mset A B \ (\a. count A a \ count B a)" + +definition subset_mset :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where +"subset_mset A B \ (A <=# B \ A \ B)" + +notation subseteq_mset (infix "\#" 50) +notation (xsymbols) subseteq_mset (infix "\#" 50) + +notation (xsymbols) subset_mset (infix "\#" 50) + +interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op <=#" "op <#" + by default (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) lemma mset_less_eqI: - "(\x. count A x \ count B x) \ A \ B" - by (simp add: mset_le_def) + "(\x. count A x \ count B x) \ A \# B" + by (simp add: subseteq_mset_def) lemma mset_le_exists_conv: - "(A::'a multiset) \ B \ (\C. B = A + C)" -apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI) + "(A::'a multiset) \# B \ (\C. B = A + C)" +apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI) apply (auto intro: multiset_eq_iff [THEN iffD2]) done -instance multiset :: (type) ordered_cancel_comm_monoid_diff +interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" "op -" 0 "op \#" "op <#" by default (simp, fact mset_le_exists_conv) lemma mset_le_mono_add_right_cancel [simp]: - "(A::'a multiset) + C \ B + C \ A \ B" - by (fact add_le_cancel_right) + "(A::'a multiset) + C \# B + C \ A \# B" + by (fact subset_mset.add_le_cancel_right) lemma mset_le_mono_add_left_cancel [simp]: - "C + (A::'a multiset) \ C + B \ A \ B" - by (fact add_le_cancel_left) + "C + (A::'a multiset) \# C + B \ A \# B" + by (fact subset_mset.add_le_cancel_left) lemma mset_le_mono_add: - "(A::'a multiset) \ B \ C \ D \ A + C \ B + D" - by (fact add_mono) + "(A::'a multiset) \# B \ C \# D \ A + C \# B + D" + by (fact subset_mset.add_mono) lemma mset_le_add_left [simp]: - "(A::'a multiset) \ A + B" - unfolding mset_le_def by auto + "(A::'a multiset) \# A + B" + unfolding subseteq_mset_def by auto lemma mset_le_add_right [simp]: - "B \ (A::'a multiset) + B" - unfolding mset_le_def by auto + "B \# (A::'a multiset) + B" + unfolding subseteq_mset_def by auto lemma mset_le_single: - "a :# B \ {#a#} \ B" - by (simp add: mset_le_def) + "a :# B \ {#a#} \# B" + by (simp add: subseteq_mset_def) lemma multiset_diff_union_assoc: - "C \ B \ (A::'a multiset) + B - C = A + (B - C)" - by (simp add: multiset_eq_iff mset_le_def) + "C \# B \ (A::'a multiset) + B - C = A + (B - C)" + by (simp add: subset_mset.diff_add_assoc) lemma mset_le_multiset_union_diff_commute: - "B \ A \ (A::'a multiset) - B + C = A + C - B" -by (simp add: multiset_eq_iff mset_le_def) - -lemma diff_le_self[simp]: "(M::'a multiset) - N \ M" -by(simp add: mset_le_def) - -lemma mset_lessD: "A < B \ x \# A \ x \# B" -apply (clarsimp simp: mset_le_def mset_less_def) + "B \# A \ (A::'a multiset) - B + C = A + C - B" +by (simp add: subset_mset.add_diff_assoc2) + +lemma diff_le_self[simp]: "(M::'a multiset) - N \# M" +by(simp add: subseteq_mset_def) + +lemma mset_lessD: "A <# B \ x \# A \ x \# B" +apply (clarsimp simp: subset_mset_def subseteq_mset_def) apply (erule_tac x=x in allE) apply auto done -lemma mset_leD: "A \ B \ x \# A \ x \# B" -apply (clarsimp simp: mset_le_def mset_less_def) +lemma mset_leD: "A \# B \ x \# A \ x \# B" +apply (clarsimp simp: subset_mset_def subseteq_mset_def) apply (erule_tac x = x in allE) apply auto done -lemma mset_less_insertD: "(A + {#x#} < B) \ (x \# B \ A < B)" +lemma mset_less_insertD: "(A + {#x#} <# B) \ (x \# B \ A <# B)" apply (rule conjI) apply (simp add: mset_lessD) -apply (clarsimp simp: mset_le_def mset_less_def) +apply (clarsimp simp: subset_mset_def subseteq_mset_def) apply safe apply (erule_tac x = a in allE) apply (auto split: split_if_asm) done -lemma mset_le_insertD: "(A + {#x#} \ B) \ (x \# B \ A \ B)" +lemma mset_le_insertD: "(A + {#x#} \# B) \ (x \# B \ A \# B)" apply (rule conjI) apply (simp add: mset_leD) -apply (force simp: mset_le_def mset_less_def split: split_if_asm) +apply (force simp: subset_mset_def subseteq_mset_def split: split_if_asm) done -lemma mset_less_of_empty[simp]: "A < {#} \ False" - by (auto simp add: mset_less_def mset_le_def multiset_eq_iff) - -lemma empty_le[simp]: "{#} \ A" +lemma mset_less_of_empty[simp]: "A <# {#} \ False" + by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff) + +lemma empty_le[simp]: "{#} \# A" unfolding mset_le_exists_conv by auto -lemma le_empty[simp]: "(M \ {#}) = (M = {#})" +lemma le_empty[simp]: "(M \# {#}) = (M = {#})" unfolding mset_le_exists_conv by auto -lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" - by (auto simp: mset_le_def mset_less_def) - -lemma multi_psub_self[simp]: "(A::'a multiset) < A = False" +lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}" + by (auto simp: subset_mset_def subseteq_mset_def) + +lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False" by simp -lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \ N < M" - by (fact add_less_imp_less_right) +lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \ N <# M" + by (fact subset_mset.add_less_imp_less_right) lemma mset_less_empty_nonempty: - "{#} < S \ S \ {#}" - by (auto simp: mset_le_def mset_less_def) + "{#} <# S \ S \ {#}" + by (auto simp: subset_mset_def subseteq_mset_def) lemma mset_less_diff_self: - "c \# B \ B - {#c#} < B" - by (auto simp: mset_le_def mset_less_def multiset_eq_iff) + "c \# B \ B - {#c#} <# B" + by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff) subsubsection {* Intersection *} -instantiation multiset :: (type) semilattice_inf -begin - -definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where - multiset_inter_def: "inf_multiset A B = A - (A - B)" - -instance +definition inf_subset_mset :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where + multiset_inter_def: "inf_subset_mset A B = A - (A - B)" + +interpretation subset_mset: semilattice_inf inf_subset_mset "op \#" "op <#" proof - - have aux: "\m n q :: nat. m \ n \ m \ q \ m \ n - (n - q)" by arith - show "OFCLASS('a multiset, semilattice_inf_class)" - by default (auto simp add: multiset_inter_def mset_le_def aux) + have aux: "\m n q :: nat. m \ n \ m \ q \ m \ n - (n - q)" by arith + show "class.semilattice_inf op #\ op \# op <#" + by default (auto simp add: multiset_inter_def subseteq_mset_def aux) qed -end - -abbreviation multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where - "multiset_inter \ inf" lemma multiset_inter_count [simp]: - "count (A #\ B) x = min (count A x) (count B x)" + "count ((A::'a multiset) #\ B) x = min (count A x) (count B x)" by (simp add: multiset_inter_def) lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" @@ -475,28 +455,19 @@ subsubsection {* Bounded union *} - -instantiation multiset :: (type) semilattice_sup -begin - -definition sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where - "sup_multiset A B = A + (B - A)" - -instance +definition sup_subset_mset :: "'a multiset \ 'a multiset \ 'a multiset"(infixl "#\" 70) where + "sup_subset_mset A B = A + (B - A)" + +interpretation subset_mset: semilattice_sup sup_subset_mset "op \#" "op <#" proof - have aux: "\m n q :: nat. m \ n \ q \ n \ m + (q - m) \ n" by arith - show "OFCLASS('a multiset, semilattice_sup_class)" - by default (auto simp add: sup_multiset_def mset_le_def aux) + show "class.semilattice_sup op #\ op \# op <#" + by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux) qed -end - -abbreviation sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where - "sup_multiset \ sup" - -lemma sup_multiset_count [simp]: +lemma sup_subset_mset_count [simp]: "count (A #\ B) x = max (count A x) (count B x)" - by (simp add: sup_multiset_def) + by (simp add: sup_subset_mset_def) lemma empty_sup [simp]: "{#} #\ M = M" @@ -522,6 +493,8 @@ "x \# N \ N #\ (M + {#x#}) = ((N - {#x#}) #\ M) + {#x#}" by (simp add: multiset_eq_iff) +subsubsection {*Subset is an order*} +interpretation subset_mset: order "op \#" "op <#" by unfold_locales auto subsubsection {* Filter (with comprehension syntax) *} @@ -555,11 +528,11 @@ "filter_mset P (M #\ N) = filter_mset P M #\ filter_mset P N" by (rule multiset_eqI) simp -lemma multiset_filter_subset[simp]: "filter_mset f M \ M" - unfolding less_eq_multiset.rep_eq by auto - -lemma multiset_filter_mono: assumes "A \ B" - shows "filter_mset f A \ filter_mset f B" +lemma multiset_filter_subset[simp]: "filter_mset f M \# M" + by (simp add: mset_less_eqI) + +lemma multiset_filter_mono: assumes "A \# B" + shows "filter_mset f A \# filter_mset f B" proof - from assms[unfolded mset_le_exists_conv] obtain C where B: "B = A + C" by auto @@ -603,7 +576,7 @@ lemma finite_Collect_mem [iff]: "finite {x. x :# M}" unfolding set_of_def[symmetric] by simp -lemma set_of_mono: "A \ B \ set_of A \ set_of B" +lemma set_of_mono: "A \# B \ set_of A \ set_of B" by (metis mset_leD subsetI mem_set_of_iff) lemma ball_set_of_iff: "(\x \ set_of M. P x) \ (\x. x \# M \ P x)" @@ -685,7 +658,7 @@ then show ?thesis by blast qed -lemma size_mset_mono: assumes "A \ B" +lemma size_mset_mono: assumes "A \# B" shows "size A \ size(B::_ multiset)" proof - from assms[unfolded mset_le_exists_conv] @@ -697,7 +670,7 @@ by (rule size_mset_mono[OF multiset_filter_subset]) lemma size_Diff_submset: - "M \ M' \ size (M' - M) = size M' - size(M::'a multiset)" + "M \# M' \ size (M' - M) = size M' - size(M::'a multiset)" by (metis add_diff_cancel_left' size_union mset_le_exists_conv) subsection {* Induction and case splits *} @@ -732,7 +705,7 @@ apply auto done -lemma mset_less_size: "(A::'a multiset) < B \ size A < size B" +lemma mset_less_size: "(A::'a multiset) <# B \ size A < size B" proof (induct A arbitrary: B) case (empty M) then have "M \ {#}" by (simp add: mset_less_empty_nonempty) @@ -741,12 +714,12 @@ then show ?case by simp next case (add S x T) - have IH: "\B. S < B \ size S < size B" by fact - have SxsubT: "S + {#x#} < T" by fact - then have "x \# T" and "S < T" by (auto dest: mset_less_insertD) + have IH: "\B. S <# B \ size S < size B" by fact + have SxsubT: "S + {#x#} <# T" by fact + then have "x \# T" and "S <# T" by (auto dest: mset_less_insertD) then obtain T' where T: "T = T' + {#x#}" by (blast dest: multi_member_split) - then have "S < T'" using SxsubT + then have "S <# T'" using SxsubT by (blast intro: mset_less_add_bothsides) then have "size S < size T'" using IH by simp then show ?case using T by simp @@ -760,35 +733,35 @@ text {* Well-foundedness of strict subset relation *} -lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}" +lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}" apply (rule wf_measure [THEN wf_subset, where f1=size]) apply (clarsimp simp: measure_def inv_image_def mset_less_size) done lemma full_multiset_induct [case_names less]: -assumes ih: "\B. \(A::'a multiset). A < B \ P A \ P B" +assumes ih: "\B. \(A::'a multiset). A <# B \ P A \ P B" shows "P B" apply (rule wf_less_mset_rel [THEN wf_induct]) apply (rule ih, auto) done lemma multi_subset_induct [consumes 2, case_names empty add]: -assumes "F \ A" +assumes "F \# A" and empty: "P {#}" and insert: "\a F. a \# A \ P F \ P (F + {#a#})" shows "P F" proof - - from `F \ A` + from `F \# A` show ?thesis proof (induct F) show "P {#}" by fact next fix x F - assume P: "F \ A \ P F" and i: "F + {#x#} \ A" + assume P: "F \# A \ P F" and i: "F + {#x#} \# A" show "P (F + {#x#})" proof (rule insert) from i show "x \# A" by (auto dest: mset_le_insertD) - from i have "F \ A" by (auto dest: mset_le_insertD) + from i have "F \# A" by (auto dest: mset_le_insertD) with P show "P F" . qed qed @@ -1280,8 +1253,8 @@ lemma msetsum_diff: fixes M N :: "('a \ ordered_cancel_comm_monoid_diff) multiset" - shows "N \ M \ msetsum (M - N) = msetsum M - msetsum N" - by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse) + shows "N \# M \ msetsum (M - N) = msetsum M - msetsum N" + by (metis add_diff_cancel_right' msetsum.union subset_mset.diff_add) lemma size_eq_msetsum: "size M = msetsum (image_mset (\_. 1) M)" proof (induct M) @@ -1404,8 +1377,9 @@ lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n" by (induct n, simp_all) -lemma count_le_replicate_mset_le: "n \ count M x \ replicate_mset n x \ M" - by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq) +lemma count_le_replicate_mset_le: "n \ count M x \ replicate_mset n x \# M" + by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def) + lemma filter_eq_replicate_mset: "{#y \# D. y = x#} = replicate_mset (count D x) x" by (induct D) simp_all @@ -1555,8 +1529,8 @@ hide_const (open) part -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \ multiset_of xs" - by (induct xs) (auto intro: order_trans) +lemma multiset_of_remdups_le: "multiset_of (remdups xs) \# multiset_of xs" + by (induct xs) (auto intro: subset_mset.order_trans) lemma multiset_of_update: "i < length ls \ multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}" @@ -2037,17 +2011,17 @@ lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \ X = Y" by (fact add_left_imp_eq) -lemma mset_less_trans: "(M::'a multiset) < K \ K < N \ M < N" - by (fact order_less_trans) +lemma mset_less_trans: "(M::'a multiset) <# K \ K <# N \ M <# N" + by (fact subset_mset.less_trans) lemma multiset_inter_commute: "A #\ B = B #\ A" - by (fact inf.commute) + by (fact subset_mset.inf.commute) lemma multiset_inter_assoc: "A #\ (B #\ C) = A #\ B #\ C" - by (fact inf.assoc [symmetric]) + by (fact subset_mset.inf.assoc [symmetric]) lemma multiset_inter_left_commute: "A #\ (B #\ C) = B #\ (A #\ C)" - by (fact inf.left_commute) + by (fact subset_mset.inf.left_commute) lemmas multiset_inter_ac = multiset_inter_commute @@ -2182,8 +2156,8 @@ None \ None | Some (ys1,_,ys2) \ ms_lesseq_impl xs (ys1 @ ys2))" -lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \ \ multiset_of xs \ multiset_of ys) \ - (ms_lesseq_impl xs ys = Some True \ multiset_of xs < multiset_of ys) \ +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \ \ multiset_of xs \# multiset_of ys) \ + (ms_lesseq_impl xs ys = Some True \ multiset_of xs <# multiset_of ys) \ (ms_lesseq_impl xs ys = Some False \ multiset_of xs = multiset_of ys)" proof (induct xs arbitrary: ys) case (Nil ys) @@ -2195,13 +2169,13 @@ case None hence x: "x \ set ys" by (simp add: extract_None_iff) { - assume "multiset_of (x # xs) \ multiset_of ys" + assume "multiset_of (x # xs) \# multiset_of ys" from set_of_mono[OF this] x have False by simp } note nle = this moreover { - assume "multiset_of (x # xs) < multiset_of ys" - hence "multiset_of (x # xs) \ multiset_of ys" by auto + assume "multiset_of (x # xs) <# multiset_of ys" + hence "multiset_of (x # xs) \# multiset_of ys" by auto from nle[OF this] have False . } ultimately show ?thesis using None by auto @@ -2216,14 +2190,14 @@ unfolding Some option.simps split unfolding id using Cons[of "ys1 @ ys2"] - unfolding mset_le_def mset_less_def by auto + unfolding subset_mset_def subseteq_mset_def by auto qed qed -lemma [code]: "multiset_of xs \ multiset_of ys \ ms_lesseq_impl xs ys \ None" +lemma [code]: "multiset_of xs \# multiset_of ys \ ms_lesseq_impl xs ys \ None" using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto) -lemma [code]: "multiset_of xs < multiset_of ys \ ms_lesseq_impl xs ys = Some True" +lemma [code]: "multiset_of xs <# multiset_of ys \ ms_lesseq_impl xs ys = Some True" using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto) instantiation multiset :: (equal) equal diff -r b640770117fd -r f8a513fedb31 src/HOL/Library/Multiset_Order.thy --- a/src/HOL/Library/Multiset_Order.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/Library/Multiset_Order.thy Wed Jun 10 13:24:16 2015 +0200 @@ -69,7 +69,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: *} @@ -134,12 +134,12 @@ 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}" - by (metis ordered_cancel_comm_monoid_diff_class.diff_add) + with `M = N - X + Y` `X \# N` show "(M, N) \ mult {(x, y). x < y}" + by (metis subset_mset.diff_add) qed lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \ less_multiset\<^sub>D\<^sub>M M N" @@ -151,7 +151,7 @@ def X \ "N - M" def 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) @@ -239,9 +239,9 @@ lemma less_eq_imp_le_multiset: fixes M N :: "('a \ linorder) multiset" - shows "M \ N \ M #\# N" + shows "M \# N \ M #\# N" unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O - by (auto dest: leD simp add: less_eq_multiset.rep_eq) + by (simp add: less_le_not_le subseteq_mset_def) lemma less_multiset_right_total: fixes M :: "('a \ linorder) multiset" @@ -302,7 +302,7 @@ 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 \ M \ N #\# P \ M - P + N #\# M" - by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2) +lemma union_less_diff_plus: "P \# M \ N #\# P \ M - P + N #\# M" + by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2) end diff -r b640770117fd -r f8a513fedb31 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/Library/Permutation.thy Wed Jun 10 13:24:16 2015 +0200 @@ -140,7 +140,7 @@ apply simp done -lemma multiset_of_le_perm_append: "multiset_of xs \ multiset_of ys \ (\zs. xs @ zs <~~> ys)" +lemma multiset_of_le_perm_append: "multiset_of xs \# multiset_of ys \ (\zs. xs @ zs <~~> ys)" apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) apply (insert surj_multiset_of) apply (drule surjD) diff -r b640770117fd -r f8a513fedb31 src/HOL/UNITY/Comp/AllocBase.thy --- a/src/HOL/UNITY/Comp/AllocBase.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Jun 10 13:24:16 2015 +0200 @@ -5,7 +5,7 @@ section{*Common Declarations for Chandy and Charpentier's Allocator*} -theory AllocBase imports "../UNITY_Main" begin +theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin consts Nclients :: nat (*Number of clients*) @@ -41,12 +41,19 @@ lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" by (induct l) (simp_all add: ac_simps) +lemma subseteq_le_multiset: "A #<=# A + B" +unfolding le_multiset_def apply (cases B; simp) +apply (rule HOL.disjI1) +apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified]) +apply (simp add: less_multiset\<^sub>H\<^sub>O) +done + lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" apply (rule monoI) apply (unfold prefix_def) -apply (erule genPrefix.induct, auto) +apply (erule genPrefix.induct, simp_all add: add_right_mono) apply (erule order_trans) -apply simp +apply (simp add: less_eq_multiset_def subseteq_le_multiset) done (** setsum **) diff -r b640770117fd -r f8a513fedb31 src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Mon Jun 08 22:04:19 2015 +0200 +++ b/src/HOL/UNITY/Follows.thy Wed Jun 10 13:24:16 2015 +0200 @@ -168,6 +168,19 @@ subsection{*Multiset union properties (with the multiset ordering)*} +(*TODO: remove when multiset is of sort ord again*) +instantiation multiset :: (order) ordered_ab_semigroup_add +begin + +definition less_multiset :: "'a\order multiset \ 'a multiset \ bool" where + "M' < M \ M' #<# M" + +definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" where + "(M'::'a multiset) \ M \ M' #<=# M" + +instance + by default (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono) +end lemma increasing_union: "[| F \ increasing f; F \ increasing g |]