src/HOL/Library/Multiset.thy
changeset 60500 903bb1495239
parent 60400 a8a31b9ebff5
child 60502 aa58872267ee
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -6,13 +6,13 @@
     1.4      Author:     Mathias Fleury, MPII
     1.5  *)
     1.6  
     1.7 -section {* (Finite) multisets *}
     1.8 +section \<open>(Finite) multisets\<close>
     1.9  
    1.10  theory Multiset
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -subsection {* The type of multisets *}
    1.15 +subsection \<open>The type of multisets\<close>
    1.16  
    1.17  definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
    1.18  
    1.19 @@ -39,9 +39,9 @@
    1.20    "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
    1.21    using multiset_eq_iff by auto
    1.22  
    1.23 -text {*
    1.24 +text \<open>
    1.25   \medskip Preservation of the representing set @{term multiset}.
    1.26 -*}
    1.27 +\<close>
    1.28  
    1.29  lemma const0_in_multiset:
    1.30    "(\<lambda>a. 0) \<in> multiset"
    1.31 @@ -79,9 +79,9 @@
    1.32    union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
    1.33  
    1.34  
    1.35 -subsection {* Representing multisets *}
    1.36 -
    1.37 -text {* Multiset enumeration *}
    1.38 +subsection \<open>Representing multisets\<close>
    1.39 +
    1.40 +text \<open>Multiset enumeration\<close>
    1.41  
    1.42  instantiation multiset :: (type) cancel_comm_monoid_add
    1.43  begin
    1.44 @@ -119,15 +119,15 @@
    1.45    by (simp add: single.rep_eq)
    1.46  
    1.47  
    1.48 -subsection {* Basic operations *}
    1.49 -
    1.50 -subsubsection {* Union *}
    1.51 +subsection \<open>Basic operations\<close>
    1.52 +
    1.53 +subsubsection \<open>Union\<close>
    1.54  
    1.55  lemma count_union [simp]: "count (M + N) a = count M a + count N a"
    1.56    by (simp add: plus_multiset.rep_eq)
    1.57  
    1.58  
    1.59 -subsubsection {* Difference *}
    1.60 +subsubsection \<open>Difference\<close>
    1.61  
    1.62  instantiation multiset :: (type) comm_monoid_diff
    1.63  begin
    1.64 @@ -177,7 +177,7 @@
    1.65    by (simp add: multiset_eq_iff)
    1.66  
    1.67  
    1.68 -subsubsection {* Equality of multisets *}
    1.69 +subsubsection \<open>Equality of multisets\<close>
    1.70  
    1.71  lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
    1.72    by (simp add: multiset_eq_iff)
    1.73 @@ -234,12 +234,12 @@
    1.74    assume ?lhs
    1.75    show ?rhs
    1.76    proof (cases "a = b")
    1.77 -    case True with `?lhs` show ?thesis by simp
    1.78 +    case True with \<open>?lhs\<close> show ?thesis by simp
    1.79    next
    1.80      case False
    1.81 -    from `?lhs` have "a \<in># N + {#b#}" by (rule union_single_eq_member)
    1.82 +    from \<open>?lhs\<close> have "a \<in># N + {#b#}" by (rule union_single_eq_member)
    1.83      with False have "a \<in># N" by auto
    1.84 -    moreover from `?lhs` have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
    1.85 +    moreover from \<open>?lhs\<close> have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
    1.86      moreover note False
    1.87      ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap)
    1.88    qed
    1.89 @@ -269,7 +269,7 @@
    1.90    assumes "c \<in># B" and "b \<noteq> c"
    1.91    shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
    1.92  proof -
    1.93 -  from `c \<in># B` obtain A where B: "B = A + {#c#}"
    1.94 +  from \<open>c \<in># B\<close> obtain A where B: "B = A + {#c#}"
    1.95      by (blast dest: multi_member_split)
    1.96    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
    1.97    then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
    1.98 @@ -278,7 +278,7 @@
    1.99  qed
   1.100  
   1.101  
   1.102 -subsubsection {* Pointwise ordering induced by count *}
   1.103 +subsubsection \<open>Pointwise ordering induced by count\<close>
   1.104  
   1.105  definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
   1.106  "subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
   1.107 @@ -396,7 +396,7 @@
   1.108    by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
   1.109  
   1.110  
   1.111 -subsubsection {* Intersection *}
   1.112 +subsubsection \<open>Intersection\<close>
   1.113  
   1.114  definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
   1.115    multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
   1.116 @@ -454,7 +454,7 @@
   1.117    by (simp add: multiset_eq_iff)
   1.118  
   1.119  
   1.120 -subsubsection {* Bounded union *}
   1.121 +subsubsection \<open>Bounded union\<close>
   1.122  definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)  where
   1.123    "sup_subset_mset A B = A + (B - A)"
   1.124  
   1.125 @@ -493,12 +493,12 @@
   1.126    "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
   1.127    by (simp add: multiset_eq_iff)
   1.128  
   1.129 -subsubsection {*Subset is an order*}
   1.130 +subsubsection \<open>Subset is an order\<close>
   1.131  interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
   1.132  
   1.133 -subsubsection {* Filter (with comprehension syntax) *}
   1.134 -
   1.135 -text {* Multiset comprehension *}
   1.136 +subsubsection \<open>Filter (with comprehension syntax)\<close>
   1.137 +
   1.138 +text \<open>Multiset comprehension\<close>
   1.139  
   1.140  lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
   1.141  is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
   1.142 @@ -547,7 +547,7 @@
   1.143    "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
   1.144  
   1.145  
   1.146 -subsubsection {* Set of elements *}
   1.147 +subsubsection \<open>Set of elements\<close>
   1.148  
   1.149  definition set_of :: "'a multiset => 'a set" where
   1.150    "set_of M = {x. x :# M}"
   1.151 @@ -583,7 +583,7 @@
   1.152    by auto
   1.153  
   1.154  
   1.155 -subsubsection {* Size *}
   1.156 +subsubsection \<open>Size\<close>
   1.157  
   1.158  definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
   1.159  
   1.160 @@ -673,7 +673,7 @@
   1.161    "M \<le># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
   1.162  by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
   1.163  
   1.164 -subsection {* Induction and case splits *}
   1.165 +subsection \<open>Induction and case splits\<close>
   1.166  
   1.167  theorem multiset_induct [case_names empty add, induct type: multiset]:
   1.168    assumes empty: "P {#}"
   1.169 @@ -684,7 +684,7 @@
   1.170  next
   1.171    case (Suc k)
   1.172    obtain N x where "M = N + {#x#}"
   1.173 -    using `Suc k = size M` [symmetric]
   1.174 +    using \<open>Suc k = size M\<close> [symmetric]
   1.175      using size_eq_Suc_imp_eq_union by fast
   1.176    with Suc add show "P M" by simp
   1.177  qed
   1.178 @@ -729,9 +729,9 @@
   1.179  lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
   1.180  by (cases M) auto
   1.181  
   1.182 -subsubsection {* Strong induction and subset induction for multisets *}
   1.183 -
   1.184 -text {* Well-foundedness of strict subset relation *}
   1.185 +subsubsection \<open>Strong induction and subset induction for multisets\<close>
   1.186 +
   1.187 +text \<open>Well-foundedness of strict subset relation\<close>
   1.188  
   1.189  lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}"
   1.190  apply (rule wf_measure [THEN wf_subset, where f1=size])
   1.191 @@ -751,7 +751,7 @@
   1.192    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
   1.193  shows "P F"
   1.194  proof -
   1.195 -  from `F \<le># A`
   1.196 +  from \<open>F \<le># A\<close>
   1.197    show ?thesis
   1.198    proof (induct F)
   1.199      show "P {#}" by fact
   1.200 @@ -768,7 +768,7 @@
   1.201  qed
   1.202  
   1.203  
   1.204 -subsection {* The fold combinator *}
   1.205 +subsection \<open>The fold combinator\<close>
   1.206  
   1.207  definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
   1.208  where
   1.209 @@ -840,7 +840,7 @@
   1.210  
   1.211  end
   1.212  
   1.213 -text {*
   1.214 +text \<open>
   1.215    A note on code generation: When defining some function containing a
   1.216    subterm @{term "fold_mset F"}, code generation is not automatic. When
   1.217    interpreting locale @{text left_commutative} with @{text F}, the
   1.218 @@ -849,10 +849,10 @@
   1.219    contains defined symbols, i.e.\ is not a code thm. Hence a separate
   1.220    constant with its own code thms needs to be introduced for @{text
   1.221    F}. See the image operator below.
   1.222 -*}
   1.223 -
   1.224 -
   1.225 -subsection {* Image *}
   1.226 +\<close>
   1.227 +
   1.228 +
   1.229 +subsection \<open>Image\<close>
   1.230  
   1.231  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   1.232    "image_mset f = fold_mset (plus o single o f) {#}"
   1.233 @@ -920,12 +920,12 @@
   1.234  translations
   1.235    "{#e | x\<in>#M. P#}" => "{#e. x \<in># {# x\<in>#M. P#}#}"
   1.236  
   1.237 -text {*
   1.238 +text \<open>
   1.239    This allows to write not just filters like @{term "{#x:#M. x<c#}"}
   1.240    but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
   1.241    "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
   1.242    @{term "{#x+x|x:#M. x<c#}"}.
   1.243 -*}
   1.244 +\<close>
   1.245  
   1.246  lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
   1.247    by (metis mem_set_of_iff set_of_image_mset)
   1.248 @@ -961,7 +961,7 @@
   1.249    by (metis image_mset_cong split_cong)
   1.250  
   1.251  
   1.252 -subsection {* Further conversions *}
   1.253 +subsection \<open>Further conversions\<close>
   1.254  
   1.255  primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
   1.256    "multiset_of [] = {#}" |
   1.257 @@ -1121,12 +1121,12 @@
   1.258      proof (cases "finite A")
   1.259        case False then show ?thesis by simp
   1.260      next
   1.261 -      case True from True `x \<notin> A` show ?thesis by (induct A) auto
   1.262 +      case True from True \<open>x \<notin> A\<close> show ?thesis by (induct A) auto
   1.263      qed
   1.264    } note * = this
   1.265    then show "PROP ?P" "PROP ?Q" "PROP ?R"
   1.266    by (auto elim!: Set.set_insert)
   1.267 -qed -- {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *}
   1.268 +qed -- \<open>TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset}\<close>
   1.269  
   1.270  lemma elem_multiset_of_set[simp, intro]: "finite A \<Longrightarrow> x \<in># multiset_of_set A \<longleftrightarrow> x \<in> A"
   1.271    by (induct A rule: finite_induct) simp_all
   1.272 @@ -1185,7 +1185,7 @@
   1.273    by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
   1.274  
   1.275  
   1.276 -subsection {* Big operators *}
   1.277 +subsection \<open>Big operators\<close>
   1.278  
   1.279  no_notation times (infixl "*" 70)
   1.280  no_notation Groups.one ("1")
   1.281 @@ -1354,7 +1354,7 @@
   1.282  qed
   1.283  
   1.284  
   1.285 -subsection {* Replicate operation *}
   1.286 +subsection \<open>Replicate operation\<close>
   1.287  
   1.288  definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
   1.289    "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
   1.290 @@ -1385,9 +1385,9 @@
   1.291    by (induct D) simp_all
   1.292  
   1.293  
   1.294 -subsection {* Alternative representations *}
   1.295 -
   1.296 -subsubsection {* Lists *}
   1.297 +subsection \<open>Alternative representations\<close>
   1.298 +
   1.299 +subsubsection \<open>Lists\<close>
   1.300  
   1.301  context linorder
   1.302  begin
   1.303 @@ -1400,10 +1400,10 @@
   1.304    "multiset_of (sort_key k xs) = multiset_of xs"
   1.305    by (induct xs) (simp_all add: ac_simps)
   1.306  
   1.307 -text {*
   1.308 +text \<open>
   1.309    This lemma shows which properties suffice to show that a function
   1.310    @{text "f"} with @{text "f xs = ys"} behaves like sort.
   1.311 -*}
   1.312 +\<close>
   1.313  
   1.314  lemma properties_for_sort_key:
   1.315    assumes "multiset_of ys = multiset_of xs"
   1.316 @@ -1431,7 +1431,7 @@
   1.317    shows "sort xs = ys"
   1.318  proof (rule properties_for_sort_key)
   1.319    from multiset show "multiset_of ys = multiset_of xs" .
   1.320 -  from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp
   1.321 +  from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   1.322    from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
   1.323      by (rule multiset_of_eq_length_filter)
   1.324    then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
   1.325 @@ -1485,7 +1485,7 @@
   1.326      @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
   1.327    using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
   1.328  
   1.329 -text {* A stable parametrized quicksort *}
   1.330 +text \<open>A stable parametrized quicksort\<close>
   1.331  
   1.332  definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
   1.333    "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
   1.334 @@ -1561,9 +1561,9 @@
   1.335    by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
   1.336  
   1.337  
   1.338 -subsection {* The multiset order *}
   1.339 -
   1.340 -subsubsection {* Well-foundedness *}
   1.341 +subsection \<open>The multiset order\<close>
   1.342 +
   1.343 +subsubsection \<open>Well-foundedness\<close>
   1.344  
   1.345  definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   1.346    "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   1.347 @@ -1632,7 +1632,7 @@
   1.348        proof (elim exE disjE conjE)
   1.349          fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
   1.350          from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
   1.351 -        from this and `(M, M0) \<in> ?R` have "M + {#a#} \<in> ?W" ..
   1.352 +        from this and \<open>(M, M0) \<in> ?R\<close> have "M + {#a#} \<in> ?W" ..
   1.353          then show "N \<in> ?W" by (simp only: N)
   1.354        next
   1.355          fix K
   1.356 @@ -1677,7 +1677,7 @@
   1.357            by (rule acc_induct) (rule tedious_reasoning [OF _ r])
   1.358        qed
   1.359      qed
   1.360 -    from this and `M \<in> ?W` show "M + {#a#} \<in> ?W" ..
   1.361 +    from this and \<open>M \<in> ?W\<close> show "M + {#a#} \<in> ?W" ..
   1.362    qed
   1.363  qed
   1.364  
   1.365 @@ -1688,9 +1688,9 @@
   1.366  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
   1.367  
   1.368  
   1.369 -subsubsection {* Closure-free presentation *}
   1.370 -
   1.371 -text {* One direction. *}
   1.372 +subsubsection \<open>Closure-free presentation\<close>
   1.373 +
   1.374 +text \<open>One direction.\<close>
   1.375  
   1.376  lemma mult_implies_one_step:
   1.377    "trans r ==> (M, N) \<in> mult r ==>
   1.378 @@ -1736,7 +1736,7 @@
   1.379   apply (simp add: mult_def)
   1.380   apply (rule r_into_trancl)
   1.381   apply (simp add: mult1_def set_of_def, blast)
   1.382 -txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   1.383 +txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close>
   1.384  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   1.385  apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
   1.386  apply (erule ssubst)
   1.387 @@ -1761,7 +1761,7 @@
   1.388  using one_step_implies_mult_aux by blast
   1.389  
   1.390  
   1.391 -subsubsection {* Partial-order properties *}
   1.392 +subsubsection \<open>Partial-order properties\<close>
   1.393  
   1.394  definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
   1.395    "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
   1.396 @@ -1804,7 +1804,7 @@
   1.397    by simp
   1.398  
   1.399  
   1.400 -subsubsection {* Monotonicity of multiset union *}
   1.401 +subsubsection \<open>Monotonicity of multiset union\<close>
   1.402  
   1.403  lemma mult1_union: "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
   1.404  apply (unfold mult1_def)
   1.405 @@ -1836,7 +1836,7 @@
   1.406  qed (auto simp add: le_multiset_def intro: union_less_mono2)
   1.407  
   1.408  
   1.409 -subsubsection {* Termination proofs with multiset orders *}
   1.410 +subsubsection \<open>Termination proofs with multiset orders\<close>
   1.411  
   1.412  lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
   1.413    and multi_member_this: "x \<in># {# x #} + XS"
   1.414 @@ -1944,7 +1944,7 @@
   1.415  and nonempty_single: "{# x #} \<noteq> {#}"
   1.416  by auto
   1.417  
   1.418 -setup {*
   1.419 +setup \<open>
   1.420  let
   1.421    fun msetT T = Type (@{type_name multiset}, [T]);
   1.422  
   1.423 @@ -1984,10 +1984,10 @@
   1.424      reduction_pair= @{thm ms_reduction_pair}
   1.425    })
   1.426  end
   1.427 -*}
   1.428 -
   1.429 -
   1.430 -subsection {* Legacy theorem bindings *}
   1.431 +\<close>
   1.432 +
   1.433 +
   1.434 +subsection \<open>Legacy theorem bindings\<close>
   1.435  
   1.436  lemmas multi_count_eq = multiset_eq_iff [symmetric]
   1.437  
   1.438 @@ -2044,7 +2044,7 @@
   1.439    "M #\<subset># N ==> (\<not> P ==> N #\<subset># (M::'a::order multiset)) ==> P"
   1.440    by (fact multiset_order.less_asym)
   1.441  
   1.442 -ML {*
   1.443 +ML \<open>
   1.444  fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
   1.445                        (Const _ $ t') =
   1.446      let
   1.447 @@ -2067,15 +2067,15 @@
   1.448                                                  elem_T --> T))) ts)
   1.449      end
   1.450    | multiset_postproc _ _ _ _ t = t
   1.451 -*}
   1.452 -
   1.453 -declaration {*
   1.454 +\<close>
   1.455 +
   1.456 +declaration \<open>
   1.457  Nitpick_Model.register_term_postprocessor @{typ "'a multiset"}
   1.458      multiset_postproc
   1.459 -*}
   1.460 -
   1.461 -
   1.462 -subsection {* Naive implementation using lists *}
   1.463 +\<close>
   1.464 +
   1.465 +
   1.466 +subsection \<open>Naive implementation using lists\<close>
   1.467  
   1.468  code_datatype multiset_of
   1.469  
   1.470 @@ -2140,7 +2140,7 @@
   1.471  
   1.472  declare sorted_list_of_multiset_multiset_of [code]
   1.473  
   1.474 -lemma [code]: -- {* not very efficient, but representation-ignorant! *}
   1.475 +lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
   1.476    "multiset_of_set A = multiset_of (sorted_list_of_set A)"
   1.477    apply (cases "finite A")
   1.478    apply simp_all
   1.479 @@ -2225,12 +2225,12 @@
   1.480    then show ?thesis by simp
   1.481  qed
   1.482  
   1.483 -text {*
   1.484 +text \<open>
   1.485    Exercise for the casual reader: add implementations for @{const le_multiset}
   1.486    and @{const less_multiset} (multiset order).
   1.487 -*}
   1.488 -
   1.489 -text {* Quickcheck generators *}
   1.490 +\<close>
   1.491 +
   1.492 +text \<open>Quickcheck generators\<close>
   1.493  
   1.494  definition (in term_syntax)
   1.495    msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
   1.496 @@ -2267,7 +2267,7 @@
   1.497  hide_const (open) msetify
   1.498  
   1.499  
   1.500 -subsection {* BNF setup *}
   1.501 +subsection \<open>BNF setup\<close>
   1.502  
   1.503  definition rel_mset where
   1.504    "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. multiset_of xs = X \<and> multiset_of ys = Y \<and> list_all2 R xs ys)"
   1.505 @@ -2580,17 +2580,17 @@
   1.506           rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]
   1.507  
   1.508  
   1.509 -subsection {* Size setup *}
   1.510 +subsection \<open>Size setup\<close>
   1.511  
   1.512  lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
   1.513    unfolding o_apply by (rule ext) (induct_tac, auto)
   1.514  
   1.515 -setup {*
   1.516 +setup \<open>
   1.517  BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
   1.518    @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
   1.519      size_union}
   1.520    @{thms multiset_size_o_map}
   1.521 -*}
   1.522 +\<close>
   1.523  
   1.524  hide_const (open) wcount
   1.525