--- a/NEWS Wed Jun 17 17:52:04 2015 +0200
+++ b/NEWS Wed Jun 17 17:54:09 2015 +0200
@@ -115,6 +115,9 @@
are now available through the "subset_mset" interpretation
(e.g. add_mono ~> subset_mset.add_mono).
INCOMPATIBILITY.
+ - Renamed conversions:
+ set_of ~> set_mset
+ INCOMPATIBILITY
- Renamed lemmas:
mset_le_def ~> subseteq_mset_def
mset_less_def ~> subset_mset_def
--- a/src/HOL/Algebra/Divisibility.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Wed Jun 17 17:54:09 2015 +0200
@@ -2025,7 +2025,7 @@
subsubsection {* Interpreting multisets as factorizations *}
lemma (in monoid) mset_fmsetEx:
- assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
+ assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
proof -
have "\<exists>Cs'. Cs = multiset_of Cs'"
@@ -2062,7 +2062,7 @@
qed
lemma (in monoid) mset_wfactorsEx:
- assumes elems: "\<And>X. X \<in> set_of Cs
+ assumes elems: "\<And>X. X \<in> set_mset Cs
\<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
proof -
@@ -2171,7 +2171,7 @@
fix X
assume "count (fmset G as) X < count (fmset G bs) X"
hence "0 < count (fmset G bs) X" by simp
- hence "X \<in> set_of (fmset G bs)" by simp
+ hence "X \<in> set_mset (fmset G bs)" by simp
hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
from this obtain x
@@ -2595,8 +2595,8 @@
fmset G cs = fmset G as #\<inter> fmset G bs"
proof (intro mset_wfactorsEx)
fix X
- assume "X \<in> set_of (fmset G as #\<inter> fmset G bs)"
- hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)
+ assume "X \<in> set_mset (fmset G as #\<inter> fmset G bs)"
+ hence "X \<in> set_mset (fmset G as)" by (simp add: multiset_inter_def)
hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
from this obtain x
@@ -2673,12 +2673,12 @@
fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
proof (intro mset_wfactorsEx)
fix X
- assume "X \<in> set_of ((fmset G as - fmset G bs) + fmset G bs)"
- hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"
+ assume "X \<in> set_mset ((fmset G as - fmset G bs) + fmset G bs)"
+ hence "X \<in> set_mset (fmset G as) \<or> X \<in> set_mset (fmset G bs)"
by (cases "X :# fmset G bs", simp, simp)
moreover
{
- assume "X \<in> set_of (fmset G as)"
+ assume "X \<in> set_mset (fmset G as)"
hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
from this obtain x
@@ -2693,7 +2693,7 @@
}
moreover
{
- assume "X \<in> set_of (fmset G bs)"
+ assume "X \<in> set_mset (fmset G bs)"
hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
from this obtain x
--- a/src/HOL/Groups_Big.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Groups_Big.thy Wed Jun 17 17:54:09 2015 +0200
@@ -490,11 +490,11 @@
written @{text"\<Sum>x\<in>A. e"}. *}
syntax
- "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10)
+ "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
- "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
+ "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
syntax (HTML output)
- "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
+ "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
translations -- {* Beware of argument permutation! *}
"SUM i:A. b" == "CONST setsum (%i. b) A"
@@ -506,9 +506,9 @@
syntax
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
- "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+ "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
syntax (HTML output)
- "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+ "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
translations
"SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
@@ -1054,11 +1054,11 @@
end
syntax
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10)
+ "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
+ "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
syntax (HTML output)
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
+ "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
translations -- {* Beware of argument permutation! *}
"PROD i:A. b" == "CONST setprod (%i. b) A"
@@ -1068,11 +1068,11 @@
@{text"\<Prod>x|P. e"}. *}
syntax
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
+ "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
+ "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
syntax (HTML output)
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
+ "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
translations
"PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Wed Jun 17 17:54:09 2015 +0200
@@ -538,7 +538,7 @@
unfolding Array.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
- by (simp, subst set_of_multiset_of[symmetric], simp)
+ by (simp, subst set_mset_multiset_of[symmetric], simp)
(* -- These steps are the analogous for the right sublist \<dots> *)
from quicksort_outer_remains [OF qs1] length_remains
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
@@ -549,7 +549,7 @@
unfolding Array.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
- by (simp, subst set_of_multiset_of[symmetric], simp)
+ by (simp, subst set_mset_multiset_of[symmetric], simp)
(* -- Thirdly and finally, we show that the array is sorted
following from the facts above. *)
from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
--- a/src/HOL/Library/DAList_Multiset.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Wed Jun 17 17:54:09 2015 +0200
@@ -34,7 +34,7 @@
lemma [code, code del]: "msetprod = msetprod" ..
-lemma [code, code del]: "set_of = set_of" ..
+lemma [code, code del]: "set_mset = set_mset" ..
lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
@@ -403,15 +403,15 @@
qed
-lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
+lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
proof -
interpret comp_fun_commute ?f by default auto
show ?thesis by (induct A) auto
qed
-lemma set_of_Bag[code]:
- "set_of (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
- unfolding set_of_fold
+lemma set_mset_Bag[code]:
+ "set_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
+ unfolding set_mset_fold
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
fix a n x
show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
--- a/src/HOL/Library/Multiset.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 17 17:54:09 2015 +0200
@@ -549,37 +549,37 @@
subsubsection \<open>Set of elements\<close>
-definition set_of :: "'a multiset => 'a set" where
- "set_of M = {x. x :# M}"
-
-lemma set_of_empty [simp]: "set_of {#} = {}"
-by (simp add: set_of_def)
-
-lemma set_of_single [simp]: "set_of {#b#} = {b}"
-by (simp add: set_of_def)
-
-lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
-by (auto simp add: set_of_def)
-
-lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-by (auto simp add: set_of_def multiset_eq_iff)
-
-lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
-by (auto simp add: set_of_def)
-
-lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
-by (auto simp add: set_of_def)
-
-lemma finite_set_of [iff]: "finite (set_of M)"
- using count [of M] by (simp add: multiset_def set_of_def)
+definition set_mset :: "'a multiset => 'a set" where
+ "set_mset M = {x. x :# M}"
+
+lemma set_mset_empty [simp]: "set_mset {#} = {}"
+by (simp add: set_mset_def)
+
+lemma set_mset_single [simp]: "set_mset {#b#} = {b}"
+by (simp add: set_mset_def)
+
+lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N"
+by (auto simp add: set_mset_def)
+
+lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
+by (auto simp add: set_mset_def multiset_eq_iff)
+
+lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x :# M)"
+by (auto simp add: set_mset_def)
+
+lemma set_mset_filter [simp]: "set_mset {# x:#M. P x #} = set_mset M \<inter> {x. P x}"
+by (auto simp add: set_mset_def)
+
+lemma finite_set_mset [iff]: "finite (set_mset M)"
+ using count [of M] by (simp add: multiset_def set_mset_def)
lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
- unfolding set_of_def[symmetric] by simp
-
-lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
- by (metis mset_leD subsetI mem_set_of_iff)
-
-lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
+ unfolding set_mset_def[symmetric] by simp
+
+lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
+ by (metis mset_leD subsetI mem_set_mset_iff)
+
+lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
by auto
@@ -591,7 +591,7 @@
by (auto simp: wcount_def add_mult_distrib)
definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
- "size_multiset f M = setsum (wcount f M) (set_of M)"
+ "size_multiset f M = setsum (wcount f M) (set_mset M)"
lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
@@ -617,10 +617,10 @@
by (simp add: size_multiset_overloaded_def)
lemma setsum_wcount_Int:
- "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
+ "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
apply (induct rule: finite_induct)
apply simp
-apply (simp add: Int_insert_left set_of_def wcount_def)
+apply (simp add: Int_insert_left set_mset_def wcount_def)
done
lemma size_multiset_union [simp]:
@@ -772,7 +772,7 @@
definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
where
- "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
+ "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
lemma fold_mset_empty [simp]:
"fold_mset f s {#} = s"
@@ -789,18 +789,18 @@
interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
by (fact comp_fun_commute_funpow)
show ?thesis
- proof (cases "x \<in> set_of M")
+ proof (cases "x \<in> set_mset M")
case False
then have *: "count (M + {#x#}) x = 1" by simp
- from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
- Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
+ from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
+ Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
with False * show ?thesis
by (simp add: fold_mset_def del: count_union)
next
case True
- def N \<equiv> "set_of M - {x}"
- from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
+ def N \<equiv> "set_mset M - {x}"
+ from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
@@ -884,8 +884,8 @@
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
by simp
-lemma set_of_image_mset [simp]:
- "set_of (image_mset f M) = image f (set_of M)"
+lemma set_mset_image_mset [simp]:
+ "set_mset (image_mset f M) = image f (set_mset M)"
by (induct M) simp_all
lemma size_image_mset [simp]:
@@ -927,8 +927,8 @@
@{term "{#x+x|x:#M. x<c#}"}.
\<close>
-lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
- by (metis mem_set_of_iff set_of_image_mset)
+lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
+ by (metis mem_set_mset_iff set_mset_image_mset)
functor image_mset: image_mset
proof -
@@ -981,7 +981,7 @@
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
by (induct x) auto
-lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
+lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
by (induct x) auto
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
@@ -1019,7 +1019,7 @@
apply (induct x, simp, rule iffI, simp_all)
apply (rename_tac a b)
apply (rule conjI)
-apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
+apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
apply (erule_tac x = a in allE, simp, clarify)
apply (erule_tac x = aa in allE, simp)
done
@@ -1046,10 +1046,6 @@
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
by (induct xs) (auto simp: ac_simps)
-lemma count_multiset_of_length_filter:
- "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
- by (induct xs) auto
-
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
apply (induct ls arbitrary: i)
apply simp
@@ -1166,18 +1162,18 @@
"sorted_list_of_multiset (multiset_of xs) = sort xs"
by (induct xs) simp_all
-lemma finite_set_of_multiset_of_set:
+lemma finite_set_mset_multiset_of_set:
assumes "finite A"
- shows "set_of (multiset_of_set A) = A"
+ shows "set_mset (multiset_of_set A) = A"
using assms by (induct A) simp_all
-lemma infinite_set_of_multiset_of_set:
+lemma infinite_set_mset_multiset_of_set:
assumes "\<not> finite A"
- shows "set_of (multiset_of_set A) = {}"
+ shows "set_mset (multiset_of_set A) = {}"
using assms by simp
lemma set_sorted_list_of_multiset [simp]:
- "set (sorted_list_of_multiset M) = set_of M"
+ "set (sorted_list_of_multiset M) = set_mset M"
by (induct M) (simp_all add: set_insort)
lemma sorted_list_of_multiset_of_set [simp]:
@@ -1261,8 +1257,8 @@
case empty then show ?case by simp
next
case (add M x) then show ?case
- by (cases "x \<in> set_of M")
- (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
+ by (cases "x \<in> set_mset M")
+ (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
qed
@@ -1271,7 +1267,7 @@
notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
-lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
+lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
by (induct MM) auto
lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
@@ -1324,7 +1320,7 @@
by (cases "finite A") (induct A rule: finite_induct, simp_all)
lemma msetprod_multiplicity:
- "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
+ "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
end
@@ -1371,7 +1367,7 @@
lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
unfolding replicate_mset_def by (induct n) simp_all
-lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
+lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
by (auto split: if_splits)
lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
@@ -1695,8 +1691,8 @@
lemma mult_implies_one_step:
"trans r ==> (M, N) \<in> mult r ==>
\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
- (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
-apply (unfold mult_def mult1_def set_of_def)
+ (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
+apply (unfold mult_def mult1_def set_mset_def)
apply (erule converse_trancl_induct, clarify)
apply (rule_tac x = M0 in exI, simp, clarify)
apply (case_tac "a :# K")
@@ -1726,7 +1722,7 @@
lemma one_step_implies_mult_aux:
"trans r ==>
- \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
+ \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r))
--> (I + K, I + J) \<in> mult r"
apply (induct_tac n, auto)
apply (frule size_eq_Suc_imp_eq_union, clarify)
@@ -1735,10 +1731,10 @@
apply (case_tac "J' = {#}")
apply (simp add: mult_def)
apply (rule r_into_trancl)
- apply (simp add: mult1_def set_of_def, blast)
+ apply (simp add: mult1_def set_mset_def, blast)
txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close>
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
apply (erule ssubst)
apply (simp add: Ball_def, auto)
apply (subgoal_tac
@@ -1749,14 +1745,14 @@
apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
apply (erule trancl_trans)
apply (rule r_into_trancl)
-apply (simp add: mult1_def set_of_def)
+apply (simp add: mult1_def set_mset_def)
apply (rule_tac x = a in exI)
apply (rule_tac x = "I + J'" in exI)
apply (simp add: ac_simps)
done
lemma one_step_implies_mult:
- "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
+ "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
==> (I + K, I + J) \<in> mult r"
using one_step_implies_mult_aux by blast
@@ -1783,14 +1779,14 @@
by (rule transI) simp
moreover note MM
ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
- \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+ \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
by (rule mult_implies_one_step)
then obtain I J K where "M = I + J" and "M = I + K"
- and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
- then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
- have "finite (set_of K)" by simp
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+ then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+ have "finite (set_mset K)" by simp
moreover note aux2
- ultimately have "set_of K = {}"
+ ultimately have "set_mset K = {}"
by (induct rule: finite_induct) (auto intro: order_less_trans)
with aux1 show False by simp
qed
@@ -1851,12 +1847,12 @@
by (auto intro: wf_mult1 wf_trancl simp: mult_def)
lemma smsI:
- "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
+ "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
unfolding ms_strict_def
by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
lemma wmsI:
- "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
+ "(set_mset A, set_mset B) \<in> max_strict \<or> A = {#} \<and> B = {#}
\<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
unfolding ms_weak_def ms_strict_def
by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
@@ -1872,7 +1868,7 @@
lemma pw_leq_split:
assumes "pw_leq X Y"
- shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+ shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
using assms
proof (induct)
case pw_leq_empty thus ?case by auto
@@ -1880,7 +1876,7 @@
case (pw_leq_step x y X Y)
then obtain A B Z where
[simp]: "X = A + Z" "Y = B + Z"
- and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
+ and 1[simp]: "(set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
by auto
from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
unfolding pair_leq_def by auto
@@ -1890,7 +1886,7 @@
have
"{#x#} + X = A + ({#y#}+Z)
\<and> {#y#} + Y = B + ({#y#}+Z)
- \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+ \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
by (auto simp: ac_simps)
thus ?case by (intro exI)
next
@@ -1900,7 +1896,7 @@
"{#y#} + Y = ?B' + Z"
by (auto simp add: ac_simps)
moreover have
- "(set_of ?A', set_of ?B') \<in> max_strict"
+ "(set_mset ?A', set_mset ?B') \<in> max_strict"
using 1 A unfolding max_strict_def
by (auto elim!: max_ext.cases)
ultimately show ?thesis by blast
@@ -1909,22 +1905,22 @@
lemma
assumes pwleq: "pw_leq Z Z'"
- shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
- and ms_weakI1: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
+ shows ms_strictI: "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
+ and ms_weakI1: "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
and ms_weakI2: "(Z + {#}, Z' + {#}) \<in> ms_weak"
proof -
from pw_leq_split[OF pwleq]
obtain A' B' Z''
where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
- and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
+ and mx_or_empty: "(set_mset A', set_mset B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
by blast
{
- assume max: "(set_of A, set_of B) \<in> max_strict"
+ assume max: "(set_mset A, set_mset B) \<in> max_strict"
from mx_or_empty
have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
proof
- assume max': "(set_of A', set_of B') \<in> max_strict"
- with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
+ assume max': "(set_mset A', set_mset B') \<in> max_strict"
+ with max have "(set_mset (A + A'), set_mset (B + B')) \<in> max_strict"
by (auto simp: max_strict_def intro: max_ext_additive)
thus ?thesis by (rule smsI)
next
@@ -1972,14 +1968,14 @@
ORELSE (rtac @{thm pw_leq_lstep} i)
ORELSE (rtac @{thm pw_leq_empty} i)
- val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
+ val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
@{thm Un_insert_left}, @{thm Un_empty_left}]
in
ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
{
msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
- mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
+ mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
reduction_pair= @{thm ms_reduction_pair}
})
@@ -2136,7 +2132,7 @@
then show ?thesis by simp
qed
-declare set_of_multiset_of [code]
+declare set_mset_multiset_of [code]
declare sorted_list_of_multiset_multiset_of [code]
@@ -2170,7 +2166,7 @@
hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
{
assume "multiset_of (x # xs) \<le># multiset_of ys"
- from set_of_mono[OF this] x have False by simp
+ from set_mset_mono[OF this] x have False by simp
} note nle = this
moreover
{
@@ -2367,7 +2363,7 @@
bnf "'a multiset"
map: image_mset
- sets: set_of
+ sets: set_mset
bd: natLeq
wits: "{#}"
rel: rel_mset
@@ -2379,11 +2375,11 @@
unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
next
fix X :: "'a multiset"
- show "\<And>f g. (\<And>z. z \<in> set_of X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
+ show "\<And>f g. (\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
by (induct X, (simp (no_asm))+,
- metis One_nat_def Un_iff count_single mem_set_of_iff set_of_union zero_less_Suc)
+ metis One_nat_def Un_iff count_single mem_set_mset_iff set_mset_union zero_less_Suc)
next
- show "\<And>f. set_of \<circ> image_mset f = op ` f \<circ> set_of"
+ show "\<And>f. set_mset \<circ> image_mset f = op ` f \<circ> set_mset"
by auto
next
show "card_order natLeq"
@@ -2392,7 +2388,7 @@
show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
by (rule natLeq_cinfinite)
next
- show "\<And>X. ordLeq3 (card_of (set_of X)) natLeq"
+ show "\<And>X. ordLeq3 (card_of (set_mset X)) natLeq"
by transfer
(auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
next
@@ -2404,8 +2400,8 @@
by (auto intro: list_all2_trans)
next
show "\<And>R. rel_mset R =
- (BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset snd)"
+ (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
+ BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)"
unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
apply (rule ext)+
apply auto
@@ -2424,7 +2420,7 @@
apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
done
next
- show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
+ show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
by auto
qed
@@ -2444,10 +2440,10 @@
assumes ab: "R a b" and MN: "rel_mset R M N"
shows "rel_mset R (M + {#a#}) (N + {#b#})"
proof-
- {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
+ {fix y assume "R a b" and "set_mset y \<subseteq> {(x, y). R x y}"
hence "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
image_mset snd y + {#b#} = image_mset snd ya \<and>
- set_of ya \<subseteq> {(x, y). R x y}"
+ set_mset ya \<subseteq> {(x, y). R x y}"
apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
}
thus ?thesis
@@ -2510,7 +2506,7 @@
proof-
obtain a where a: "a \<in># M" and fa: "f a = b"
using multiset.set_map[of f M] unfolding assms
- by (metis image_iff mem_set_of_iff union_single_eq_member)
+ by (metis image_iff mem_set_mset_iff union_single_eq_member)
then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
thus ?thesis using M fa by blast
@@ -2521,7 +2517,7 @@
shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
proof-
obtain K where KM: "image_mset fst K = M + {#a#}"
- and KN: "image_mset snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+ and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
using assms
unfolding multiset.rel_compp_Grp Grp_def by auto
obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
@@ -2539,7 +2535,7 @@
shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
proof-
obtain K where KN: "image_mset snd K = N + {#b#}"
- and KM: "image_mset fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+ and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
using assms
unfolding multiset.rel_compp_Grp Grp_def by auto
obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
--- a/src/HOL/Library/Multiset_Order.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Wed Jun 17 17:54:09 2015 +0200
@@ -47,14 +47,14 @@
moreover
assume "(M, M) \<in> mult {(x, y). x < y}"
ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
- \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+ \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
by (rule mult_implies_one_step)
then obtain I J K where "M = I + J" and "M = I + K"
- and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
- then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
- have "finite (set_of K)" by simp
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+ then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+ have "finite (set_mset K)" by simp
moreover note aux2
- ultimately have "set_of K = {}"
+ ultimately have "set_mset K = {}"
by (induct rule: finite_induct)
(simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
with aux1 show False by simp
--- a/src/HOL/Library/Permutation.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Jun 17 17:54:09 2015 +0200
@@ -136,7 +136,7 @@
apply (erule perm.trans)
apply (rule perm_sym)
apply (erule perm_remove)
- apply (drule_tac f=set_of in arg_cong)
+ apply (drule_tac f=set_mset in arg_cong)
apply simp
done
--- a/src/HOL/Library/Tree_Multiset.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy Wed Jun 17 17:54:09 2015 +0200
@@ -14,7 +14,7 @@
"mset_tree Leaf = {#}" |
"mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
-lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
+lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
by(induction t) auto
lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Jun 17 17:54:09 2015 +0200
@@ -37,67 +37,67 @@
subsection {* unique factorization: multiset version *}
lemma multiset_prime_factorization_exists [rule_format]: "n > 0 -->
- (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
+ (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
proof (rule nat_less_induct, clarify)
fix n :: nat
- assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m =
+ assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_mset M. prime p) & m =
(PROD i :# M. i))"
assume "(n::nat) > 0"
then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
by arith
moreover {
assume "n = 1"
- then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" by auto
+ then have "(ALL p : set_mset {#}. prime p) & n = (PROD i :# {#}. i)" by auto
} moreover {
assume "n > 1" and "prime n"
- then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
+ then have "(ALL p : set_mset {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
by auto
} moreover {
assume "n > 1" and "~ prime n"
with not_prime_eq_prod_nat
obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
by blast
- with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
- and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
+ with ih obtain Q R where "(ALL p : set_mset Q. prime p) & m = (PROD i:#Q. i)"
+ and "(ALL p: set_mset R. prime p) & k = (PROD i:#R. i)"
by blast
- then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+ then have "(ALL p: set_mset (Q + R). prime p) & n = (PROD i :# Q + R. i)"
by (auto simp add: n msetprod_Un)
- then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
+ then have "EX M. (ALL p : set_mset M. prime p) & n = (PROD i :# M. i)"..
}
- ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
+ ultimately show "EX M. (ALL p : set_mset M. prime p) & n = (PROD i::nat:#M. i)"
by blast
qed
lemma multiset_prime_factorization_unique_aux:
fixes a :: nat
- assumes "(ALL p : set_of M. prime p)" and
- "(ALL p : set_of N. prime p)" and
+ assumes "(ALL p : set_mset M. prime p)" and
+ "(ALL p : set_mset N. prime p)" and
"(PROD i :# M. i) dvd (PROD i:# N. i)"
shows
"count M a <= count N a"
proof cases
- assume M: "a : set_of M"
+ assume M: "a : set_mset M"
with assms have a: "prime a" by auto
with M have "a ^ count M a dvd (PROD i :# M. i)"
by (auto simp add: msetprod_multiplicity)
also have "... dvd (PROD i :# N. i)" by (rule assms)
- also have "... = (PROD i : (set_of N). i ^ (count N i))"
+ also have "... = (PROD i : (set_mset N). i ^ (count N i))"
by (simp add: msetprod_multiplicity)
- also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
+ also have "... = a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))"
proof (cases)
- assume "a : set_of N"
- then have b: "set_of N = {a} Un (set_of N - {a})"
+ assume "a : set_mset N"
+ then have b: "set_mset N = {a} Un (set_mset N - {a})"
by auto
then show ?thesis
by (subst (1) b, subst setprod.union_disjoint, auto)
next
- assume "a ~: set_of N"
+ assume "a ~: set_mset N"
then show ?thesis by auto
qed
finally have "a ^ count M a dvd
- a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
+ a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))".
moreover
- have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
+ have "coprime (a ^ count M a) (PROD i : (set_mset N - {a}). i ^ (count N i))"
apply (subst gcd_commute_nat)
apply (rule setprod_coprime_nat)
apply (rule primes_imp_powers_coprime_nat)
@@ -111,13 +111,13 @@
apply auto
done
next
- assume "a ~: set_of M"
+ assume "a ~: set_mset M"
then show ?thesis by auto
qed
lemma multiset_prime_factorization_unique:
- assumes "(ALL (p::nat) : set_of M. prime p)" and
- "(ALL p : set_of N. prime p)" and
+ assumes "(ALL (p::nat) : set_mset M. prime p)" and
+ "(ALL p : set_mset N. prime p)" and
"(PROD i :# M. i) = (PROD i:# N. i)"
shows
"M = N"
@@ -137,12 +137,12 @@
definition multiset_prime_factorization :: "nat => nat multiset"
where
"multiset_prime_factorization n ==
- if n > 0 then (THE M. ((ALL p : set_of M. prime p) &
+ if n > 0 then (THE M. ((ALL p : set_mset M. prime p) &
n = (PROD i :# M. i)))
else {#}"
lemma multiset_prime_factorization: "n > 0 ==>
- (ALL p : set_of (multiset_prime_factorization n). prime p) &
+ (ALL p : set_mset (multiset_prime_factorization n). prime p) &
n = (PROD i :# (multiset_prime_factorization n). i)"
apply (unfold multiset_prime_factorization_def)
apply clarsimp
@@ -169,7 +169,7 @@
where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
definition prime_factors_nat :: "nat \<Rightarrow> nat set"
- where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+ where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
instance ..
@@ -306,12 +306,12 @@
apply force
apply force
using assms
- apply (simp add: set_of_def msetprod_multiplicity)
+ apply (simp add: set_mset_def msetprod_multiplicity)
done
with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
by simp
with S_eq show ?thesis
- by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
+ by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
qed
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
@@ -435,7 +435,7 @@
apply (cases "n = 0")
apply auto
apply (frule multiset_prime_factorization)
- apply (auto simp add: set_of_def multiplicity_nat_def)
+ apply (auto simp add: set_mset_def multiplicity_nat_def)
done
lemma multiplicity_not_factor_nat [simp]:
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 17 17:54:09 2015 +0200
@@ -1413,7 +1413,7 @@
lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
by transfer rule
-lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M"
+lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M"
by (auto simp: set_pmf_iff)
end
--- a/src/HOL/Wellfounded.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/Wellfounded.thy Wed Jun 17 17:54:09 2015 +0200
@@ -318,7 +318,6 @@
2. There is no such step.
Pick an S-min element of A. In this case it must be an R-min
element of A as well.
-
*)
lemma wf_Un:
"[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
@@ -382,30 +381,59 @@
subsection {* Well-Foundedness of Composition *}
-text{* Provided by Tjark Weber: *}
+text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
-lemma wf_relcomp_compatible:
+lemma qc_wf_relto_iff:
+ assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
+ shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
+proof
+ assume "wf ?S"
+ moreover have "R \<subseteq> ?S" by auto
+ ultimately show "wf R" using wf_subset by auto
+next
+ assume "wf R"
+ show "wf ?S"
+ proof (rule wfI_pf)
+ fix A assume A: "A \<subseteq> ?S `` A"
+ let ?X = "(R \<union> S)\<^sup>* `` A"
+ have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
+ proof -
+ { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
+ then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
+ proof (induct y z)
+ case rtrancl_refl then show ?case by auto
+ next
+ case (rtrancl_into_rtrancl a b c)
+ then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
+ then show ?case by simp
+ qed }
+ then show ?thesis by auto
+ qed
+ then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
+ then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
+ also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
+ finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" by (simp add: O_assoc[symmetric] relcomp_mono)
+ also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
+ finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
+ then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
+ moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
+ ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
+ then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
+ moreover have "A \<subseteq> ?X" by auto
+ ultimately show "A = {}" by simp
+ qed
+qed
+
+corollary wf_relcomp_compatible:
assumes "wf R" and "R O S \<subseteq> S O R"
shows "wf (S O R)"
-proof (rule wfI_pf)
- fix A assume A: "A \<subseteq> (S O R) `` A"
- {
- fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
- proof (induction n)
- case 0 show ?case using A by (simp add: relcomp_Image)
- next
- case (Suc n)
- then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n) `` A"
- by (simp add: Image_mono)
- also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2)
- by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono)
- finally show ?case by (simp add: relcomp_Image)
- qed
- }
- then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S ^^ n) `` A)" by blast
- then have "(\<Union>n. (S ^^ n) `` A) = {}"
- using assms(1) by (simp only: wfE_pf)
- then show "A = {}" using relpow.simps(1) by blast
+proof -
+ have "R O S \<subseteq> (R \<union> S)\<^sup>* O R"
+ using assms by blast
+ then have "wf (S\<^sup>* O R O S\<^sup>*)"
+ by (simp add: assms qc_wf_relto_iff)
+ then show ?thesis
+ by (rule Wellfounded.wf_subset) blast
qed
@@ -486,7 +514,7 @@
by (simp add: less_than_def less_eq)
lemma wf_less: "wf {(x, y::nat). x < y}"
- using wf_less_than by (simp add: less_than_def less_eq [symmetric])
+ by (rule Wellfounded.wellorder_class.wf)
subsection {* Accessible Part *}
--- a/src/HOL/ZF/LProd.thy Wed Jun 17 17:52:04 2015 +0200
+++ b/src/HOL/ZF/LProd.thy Wed Jun 17 17:54:09 2015 +0200
@@ -50,10 +50,10 @@
from lprod_list have "(?ma, ?mb) \<in> mult R"
by auto
with mult_implies_one_step[OF transR] have
- "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+ "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)"
by blast
then obtain I J K where
- decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+ decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)"
by blast
show ?case
proof (cases "a = b")