src/HOL/Library/Multiset.thy
changeset 60495 d7ff0a1df90a
parent 60400 a8a31b9ebff5
child 60498 c8141ac6f03f
child 60502 aa58872267ee
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Jun 16 20:50:00 2015 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 17:21:11 2015 +0200
     1.3 @@ -549,37 +549,37 @@
     1.4  
     1.5  subsubsection {* Set of elements *}
     1.6  
     1.7 -definition set_of :: "'a multiset => 'a set" where
     1.8 -  "set_of M = {x. x :# M}"
     1.9 -
    1.10 -lemma set_of_empty [simp]: "set_of {#} = {}"
    1.11 -by (simp add: set_of_def)
    1.12 -
    1.13 -lemma set_of_single [simp]: "set_of {#b#} = {b}"
    1.14 -by (simp add: set_of_def)
    1.15 -
    1.16 -lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
    1.17 -by (auto simp add: set_of_def)
    1.18 -
    1.19 -lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
    1.20 -by (auto simp add: set_of_def multiset_eq_iff)
    1.21 -
    1.22 -lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
    1.23 -by (auto simp add: set_of_def)
    1.24 -
    1.25 -lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
    1.26 -by (auto simp add: set_of_def)
    1.27 -
    1.28 -lemma finite_set_of [iff]: "finite (set_of M)"
    1.29 -  using count [of M] by (simp add: multiset_def set_of_def)
    1.30 +definition set_mset :: "'a multiset => 'a set" where
    1.31 +  "set_mset M = {x. x :# M}"
    1.32 +
    1.33 +lemma set_mset_empty [simp]: "set_mset {#} = {}"
    1.34 +by (simp add: set_mset_def)
    1.35 +
    1.36 +lemma set_mset_single [simp]: "set_mset {#b#} = {b}"
    1.37 +by (simp add: set_mset_def)
    1.38 +
    1.39 +lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N"
    1.40 +by (auto simp add: set_mset_def)
    1.41 +
    1.42 +lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
    1.43 +by (auto simp add: set_mset_def multiset_eq_iff)
    1.44 +
    1.45 +lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x :# M)"
    1.46 +by (auto simp add: set_mset_def)
    1.47 +
    1.48 +lemma set_mset_filter [simp]: "set_mset {# x:#M. P x #} = set_mset M \<inter> {x. P x}"
    1.49 +by (auto simp add: set_mset_def)
    1.50 +
    1.51 +lemma finite_set_mset [iff]: "finite (set_mset M)"
    1.52 +  using count [of M] by (simp add: multiset_def set_mset_def)
    1.53  
    1.54  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    1.55 -  unfolding set_of_def[symmetric] by simp
    1.56 -
    1.57 -lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
    1.58 -  by (metis mset_leD subsetI mem_set_of_iff)
    1.59 -
    1.60 -lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
    1.61 +  unfolding set_mset_def[symmetric] by simp
    1.62 +
    1.63 +lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
    1.64 +  by (metis mset_leD subsetI mem_set_mset_iff)
    1.65 +
    1.66 +lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
    1.67    by auto
    1.68  
    1.69  
    1.70 @@ -591,7 +591,7 @@
    1.71    by (auto simp: wcount_def add_mult_distrib)
    1.72  
    1.73  definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
    1.74 -  "size_multiset f M = setsum (wcount f M) (set_of M)"
    1.75 +  "size_multiset f M = setsum (wcount f M) (set_mset M)"
    1.76  
    1.77  lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
    1.78  
    1.79 @@ -617,10 +617,10 @@
    1.80  by (simp add: size_multiset_overloaded_def)
    1.81  
    1.82  lemma setsum_wcount_Int:
    1.83 -  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
    1.84 +  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
    1.85  apply (induct rule: finite_induct)
    1.86   apply simp
    1.87 -apply (simp add: Int_insert_left set_of_def wcount_def)
    1.88 +apply (simp add: Int_insert_left set_mset_def wcount_def)
    1.89  done
    1.90  
    1.91  lemma size_multiset_union [simp]:
    1.92 @@ -772,7 +772,7 @@
    1.93  
    1.94  definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    1.95  where
    1.96 -  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    1.97 +  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
    1.98  
    1.99  lemma fold_mset_empty [simp]:
   1.100    "fold_mset f s {#} = s"
   1.101 @@ -789,18 +789,18 @@
   1.102    interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
   1.103      by (fact comp_fun_commute_funpow)
   1.104    show ?thesis
   1.105 -  proof (cases "x \<in> set_of M")
   1.106 +  proof (cases "x \<in> set_mset M")
   1.107      case False
   1.108      then have *: "count (M + {#x#}) x = 1" by simp
   1.109 -    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
   1.110 -      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
   1.111 +    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
   1.112 +      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
   1.113        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   1.114      with False * show ?thesis
   1.115        by (simp add: fold_mset_def del: count_union)
   1.116    next
   1.117      case True
   1.118 -    def N \<equiv> "set_of M - {x}"
   1.119 -    from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
   1.120 +    def N \<equiv> "set_mset M - {x}"
   1.121 +    from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
   1.122      then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
   1.123        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
   1.124        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   1.125 @@ -884,8 +884,8 @@
   1.126    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   1.127    by simp
   1.128  
   1.129 -lemma set_of_image_mset [simp]:
   1.130 -  "set_of (image_mset f M) = image f (set_of M)"
   1.131 +lemma set_mset_image_mset [simp]:
   1.132 +  "set_mset (image_mset f M) = image f (set_mset M)"
   1.133    by (induct M) simp_all
   1.134  
   1.135  lemma size_image_mset [simp]:
   1.136 @@ -927,8 +927,8 @@
   1.137    @{term "{#x+x|x:#M. x<c#}"}.
   1.138  *}
   1.139  
   1.140 -lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
   1.141 -  by (metis mem_set_of_iff set_of_image_mset)
   1.142 +lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
   1.143 +  by (metis mem_set_mset_iff set_mset_image_mset)
   1.144  
   1.145  functor image_mset: image_mset
   1.146  proof -
   1.147 @@ -981,7 +981,7 @@
   1.148  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   1.149  by (induct x) auto
   1.150  
   1.151 -lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
   1.152 +lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
   1.153  by (induct x) auto
   1.154  
   1.155  lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   1.156 @@ -1019,7 +1019,7 @@
   1.157  apply (induct x, simp, rule iffI, simp_all)
   1.158  apply (rename_tac a b)
   1.159  apply (rule conjI)
   1.160 -apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
   1.161 +apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
   1.162  apply (erule_tac x = a in allE, simp, clarify)
   1.163  apply (erule_tac x = aa in allE, simp)
   1.164  done
   1.165 @@ -1046,10 +1046,6 @@
   1.166    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   1.167    by (induct xs) (auto simp: ac_simps)
   1.168  
   1.169 -lemma count_multiset_of_length_filter:
   1.170 -  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
   1.171 -  by (induct xs) auto
   1.172 -
   1.173  lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
   1.174  apply (induct ls arbitrary: i)
   1.175   apply simp
   1.176 @@ -1166,18 +1162,18 @@
   1.177    "sorted_list_of_multiset (multiset_of xs) = sort xs"
   1.178    by (induct xs) simp_all
   1.179  
   1.180 -lemma finite_set_of_multiset_of_set:
   1.181 +lemma finite_set_mset_multiset_of_set:
   1.182    assumes "finite A"
   1.183 -  shows "set_of (multiset_of_set A) = A"
   1.184 +  shows "set_mset (multiset_of_set A) = A"
   1.185    using assms by (induct A) simp_all
   1.186  
   1.187 -lemma infinite_set_of_multiset_of_set:
   1.188 +lemma infinite_set_mset_multiset_of_set:
   1.189    assumes "\<not> finite A"
   1.190 -  shows "set_of (multiset_of_set A) = {}"
   1.191 +  shows "set_mset (multiset_of_set A) = {}"
   1.192    using assms by simp
   1.193  
   1.194  lemma set_sorted_list_of_multiset [simp]:
   1.195 -  "set (sorted_list_of_multiset M) = set_of M"
   1.196 +  "set (sorted_list_of_multiset M) = set_mset M"
   1.197    by (induct M) (simp_all add: set_insort)
   1.198  
   1.199  lemma sorted_list_of_multiset_of_set [simp]:
   1.200 @@ -1261,8 +1257,8 @@
   1.201    case empty then show ?case by simp
   1.202  next
   1.203    case (add M x) then show ?case
   1.204 -    by (cases "x \<in> set_of M")
   1.205 -      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
   1.206 +    by (cases "x \<in> set_mset M")
   1.207 +      (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
   1.208  qed
   1.209  
   1.210  
   1.211 @@ -1271,7 +1267,7 @@
   1.212  
   1.213  notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
   1.214  
   1.215 -lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
   1.216 +lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   1.217    by (induct MM) auto
   1.218  
   1.219  lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
   1.220 @@ -1324,7 +1320,7 @@
   1.221    by (cases "finite A") (induct A rule: finite_induct, simp_all)
   1.222  
   1.223  lemma msetprod_multiplicity:
   1.224 -  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
   1.225 +  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   1.226    by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   1.227  
   1.228  end
   1.229 @@ -1371,7 +1367,7 @@
   1.230  lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
   1.231    unfolding replicate_mset_def by (induct n) simp_all
   1.232  
   1.233 -lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
   1.234 +lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
   1.235    by (auto split: if_splits)
   1.236  
   1.237  lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   1.238 @@ -1695,8 +1691,8 @@
   1.239  lemma mult_implies_one_step:
   1.240    "trans r ==> (M, N) \<in> mult r ==>
   1.241      \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
   1.242 -    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   1.243 -apply (unfold mult_def mult1_def set_of_def)
   1.244 +    (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
   1.245 +apply (unfold mult_def mult1_def set_mset_def)
   1.246  apply (erule converse_trancl_induct, clarify)
   1.247   apply (rule_tac x = M0 in exI, simp, clarify)
   1.248  apply (case_tac "a :# K")
   1.249 @@ -1726,7 +1722,7 @@
   1.250  
   1.251  lemma one_step_implies_mult_aux:
   1.252    "trans r ==>
   1.253 -    \<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))
   1.254 +    \<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))
   1.255        --> (I + K, I + J) \<in> mult r"
   1.256  apply (induct_tac n, auto)
   1.257  apply (frule size_eq_Suc_imp_eq_union, clarify)
   1.258 @@ -1735,10 +1731,10 @@
   1.259  apply (case_tac "J' = {#}")
   1.260   apply (simp add: mult_def)
   1.261   apply (rule r_into_trancl)
   1.262 - apply (simp add: mult1_def set_of_def, blast)
   1.263 + apply (simp add: mult1_def set_mset_def, blast)
   1.264  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   1.265  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   1.266 -apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
   1.267 +apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
   1.268  apply (erule ssubst)
   1.269  apply (simp add: Ball_def, auto)
   1.270  apply (subgoal_tac
   1.271 @@ -1749,14 +1745,14 @@
   1.272  apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
   1.273  apply (erule trancl_trans)
   1.274  apply (rule r_into_trancl)
   1.275 -apply (simp add: mult1_def set_of_def)
   1.276 +apply (simp add: mult1_def set_mset_def)
   1.277  apply (rule_tac x = a in exI)
   1.278  apply (rule_tac x = "I + J'" in exI)
   1.279  apply (simp add: ac_simps)
   1.280  done
   1.281  
   1.282  lemma one_step_implies_mult:
   1.283 -  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
   1.284 +  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
   1.285      ==> (I + K, I + J) \<in> mult r"
   1.286  using one_step_implies_mult_aux by blast
   1.287  
   1.288 @@ -1783,14 +1779,14 @@
   1.289        by (rule transI) simp
   1.290      moreover note MM
   1.291      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
   1.292 -      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
   1.293 +      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
   1.294        by (rule mult_implies_one_step)
   1.295      then obtain I J K where "M = I + J" and "M = I + K"
   1.296 -      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
   1.297 -    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
   1.298 -    have "finite (set_of K)" by simp
   1.299 +      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
   1.300 +    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
   1.301 +    have "finite (set_mset K)" by simp
   1.302      moreover note aux2
   1.303 -    ultimately have "set_of K = {}"
   1.304 +    ultimately have "set_mset K = {}"
   1.305        by (induct rule: finite_induct) (auto intro: order_less_trans)
   1.306      with aux1 show False by simp
   1.307    qed
   1.308 @@ -1851,12 +1847,12 @@
   1.309  by (auto intro: wf_mult1 wf_trancl simp: mult_def)
   1.310  
   1.311  lemma smsI:
   1.312 -  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
   1.313 +  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
   1.314    unfolding ms_strict_def
   1.315  by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
   1.316  
   1.317  lemma wmsI:
   1.318 -  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
   1.319 +  "(set_mset A, set_mset B) \<in> max_strict \<or> A = {#} \<and> B = {#}
   1.320    \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
   1.321  unfolding ms_weak_def ms_strict_def
   1.322  by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
   1.323 @@ -1872,7 +1868,7 @@
   1.324  
   1.325  lemma pw_leq_split:
   1.326    assumes "pw_leq X Y"
   1.327 -  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 = {#}))"
   1.328 +  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 = {#}))"
   1.329    using assms
   1.330  proof (induct)
   1.331    case pw_leq_empty thus ?case by auto
   1.332 @@ -1880,7 +1876,7 @@
   1.333    case (pw_leq_step x y X Y)
   1.334    then obtain A B Z where
   1.335      [simp]: "X = A + Z" "Y = B + Z"
   1.336 -      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
   1.337 +      and 1[simp]: "(set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
   1.338      by auto
   1.339    from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
   1.340      unfolding pair_leq_def by auto
   1.341 @@ -1890,7 +1886,7 @@
   1.342      have
   1.343        "{#x#} + X = A + ({#y#}+Z)
   1.344        \<and> {#y#} + Y = B + ({#y#}+Z)
   1.345 -      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   1.346 +      \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   1.347        by (auto simp: ac_simps)
   1.348      thus ?case by (intro exI)
   1.349    next
   1.350 @@ -1900,7 +1896,7 @@
   1.351        "{#y#} + Y = ?B' + Z"
   1.352        by (auto simp add: ac_simps)
   1.353      moreover have
   1.354 -      "(set_of ?A', set_of ?B') \<in> max_strict"
   1.355 +      "(set_mset ?A', set_mset ?B') \<in> max_strict"
   1.356        using 1 A unfolding max_strict_def
   1.357        by (auto elim!: max_ext.cases)
   1.358      ultimately show ?thesis by blast
   1.359 @@ -1909,22 +1905,22 @@
   1.360  
   1.361  lemma
   1.362    assumes pwleq: "pw_leq Z Z'"
   1.363 -  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
   1.364 -  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   1.365 +  shows ms_strictI: "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
   1.366 +  and   ms_weakI1:  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   1.367    and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
   1.368  proof -
   1.369    from pw_leq_split[OF pwleq]
   1.370    obtain A' B' Z''
   1.371      where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
   1.372 -    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
   1.373 +    and mx_or_empty: "(set_mset A', set_mset B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
   1.374      by blast
   1.375    {
   1.376 -    assume max: "(set_of A, set_of B) \<in> max_strict"
   1.377 +    assume max: "(set_mset A, set_mset B) \<in> max_strict"
   1.378      from mx_or_empty
   1.379      have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
   1.380      proof
   1.381 -      assume max': "(set_of A', set_of B') \<in> max_strict"
   1.382 -      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
   1.383 +      assume max': "(set_mset A', set_mset B') \<in> max_strict"
   1.384 +      with max have "(set_mset (A + A'), set_mset (B + B')) \<in> max_strict"
   1.385          by (auto simp: max_strict_def intro: max_ext_additive)
   1.386        thus ?thesis by (rule smsI)
   1.387      next
   1.388 @@ -1972,14 +1968,14 @@
   1.389        ORELSE (rtac @{thm pw_leq_lstep} i)
   1.390        ORELSE (rtac @{thm pw_leq_empty} i)
   1.391  
   1.392 -  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
   1.393 +  val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
   1.394                        @{thm Un_insert_left}, @{thm Un_empty_left}]
   1.395  in
   1.396    ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
   1.397    {
   1.398      msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
   1.399      mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
   1.400 -    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
   1.401 +    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
   1.402      smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
   1.403      reduction_pair= @{thm ms_reduction_pair}
   1.404    })
   1.405 @@ -2136,7 +2132,7 @@
   1.406    then show ?thesis by simp
   1.407  qed
   1.408  
   1.409 -declare set_of_multiset_of [code]
   1.410 +declare set_mset_multiset_of [code]
   1.411  
   1.412  declare sorted_list_of_multiset_multiset_of [code]
   1.413  
   1.414 @@ -2170,7 +2166,7 @@
   1.415      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   1.416      {
   1.417        assume "multiset_of (x # xs) \<le># multiset_of ys"
   1.418 -      from set_of_mono[OF this] x have False by simp
   1.419 +      from set_mset_mono[OF this] x have False by simp
   1.420      } note nle = this
   1.421      moreover
   1.422      {
   1.423 @@ -2367,7 +2363,7 @@
   1.424  
   1.425  bnf "'a multiset"
   1.426    map: image_mset
   1.427 -  sets: set_of
   1.428 +  sets: set_mset
   1.429    bd: natLeq
   1.430    wits: "{#}"
   1.431    rel: rel_mset
   1.432 @@ -2379,11 +2375,11 @@
   1.433      unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
   1.434  next
   1.435    fix X :: "'a multiset"
   1.436 -  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"
   1.437 +  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"
   1.438      by (induct X, (simp (no_asm))+,
   1.439 -      metis One_nat_def Un_iff count_single mem_set_of_iff set_of_union zero_less_Suc)
   1.440 +      metis One_nat_def Un_iff count_single mem_set_mset_iff set_mset_union zero_less_Suc)
   1.441  next
   1.442 -  show "\<And>f. set_of \<circ> image_mset f = op ` f \<circ> set_of"
   1.443 +  show "\<And>f. set_mset \<circ> image_mset f = op ` f \<circ> set_mset"
   1.444      by auto
   1.445  next
   1.446    show "card_order natLeq"
   1.447 @@ -2392,7 +2388,7 @@
   1.448    show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
   1.449      by (rule natLeq_cinfinite)
   1.450  next
   1.451 -  show "\<And>X. ordLeq3 (card_of (set_of X)) natLeq"
   1.452 +  show "\<And>X. ordLeq3 (card_of (set_mset X)) natLeq"
   1.453      by transfer
   1.454        (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
   1.455  next
   1.456 @@ -2404,8 +2400,8 @@
   1.457      by (auto intro: list_all2_trans)
   1.458  next
   1.459    show "\<And>R. rel_mset R =
   1.460 -    (BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
   1.461 -    BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset snd)"
   1.462 +    (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
   1.463 +    BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)"
   1.464      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
   1.465      apply (rule ext)+
   1.466      apply auto
   1.467 @@ -2424,7 +2420,7 @@
   1.468      apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
   1.469      done
   1.470  next
   1.471 -  show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
   1.472 +  show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
   1.473      by auto
   1.474  qed
   1.475  
   1.476 @@ -2444,10 +2440,10 @@
   1.477  assumes ab: "R a b" and MN: "rel_mset R M N"
   1.478  shows "rel_mset R (M + {#a#}) (N + {#b#})"
   1.479  proof-
   1.480 -  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
   1.481 +  {fix y assume "R a b" and "set_mset y \<subseteq> {(x, y). R x y}"
   1.482     hence "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
   1.483                 image_mset snd y + {#b#} = image_mset snd ya \<and>
   1.484 -               set_of ya \<subseteq> {(x, y). R x y}"
   1.485 +               set_mset ya \<subseteq> {(x, y). R x y}"
   1.486     apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
   1.487    }
   1.488    thus ?thesis
   1.489 @@ -2510,7 +2506,7 @@
   1.490  proof-
   1.491    obtain a where a: "a \<in># M" and fa: "f a = b"
   1.492    using multiset.set_map[of f M] unfolding assms
   1.493 -  by (metis image_iff mem_set_of_iff union_single_eq_member)
   1.494 +  by (metis image_iff mem_set_mset_iff union_single_eq_member)
   1.495    then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
   1.496    have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
   1.497    thus ?thesis using M fa by blast
   1.498 @@ -2521,7 +2517,7 @@
   1.499  shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
   1.500  proof-
   1.501    obtain K where KM: "image_mset fst K = M + {#a#}"
   1.502 -  and KN: "image_mset snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   1.503 +  and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   1.504    using assms
   1.505    unfolding multiset.rel_compp_Grp Grp_def by auto
   1.506    obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   1.507 @@ -2539,7 +2535,7 @@
   1.508  shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
   1.509  proof-
   1.510    obtain K where KN: "image_mset snd K = N + {#b#}"
   1.511 -  and KM: "image_mset fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   1.512 +  and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   1.513    using assms
   1.514    unfolding multiset.rel_compp_Grp Grp_def by auto
   1.515    obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"