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.7 -section {* (Finite) multisets *}
1.8 +section \<open>(Finite) multisets\<close>
1.10  theory Multiset
1.11  imports Main
1.12  begin
1.14 -subsection {* The type of multisets *}
1.15 +subsection \<open>The type of multisets\<close>
1.17  definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
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.23 -text {*
1.24 +text \<open>
1.25   \medskip Preservation of the representing set @{term multiset}.
1.26 -*}
1.27 +\<close>
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.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.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.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.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.59 -subsubsection {* Difference *}
1.60 +subsubsection \<open>Difference\<close>
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.68 -subsubsection {* Equality of multisets *}
1.69 +subsubsection \<open>Equality of multisets\<close>
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.102 -subsubsection {* Pointwise ordering induced by count *}
1.103 +subsubsection \<open>Pointwise ordering induced by count\<close>
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.111 -subsubsection {* Intersection *}
1.112 +subsubsection \<open>Intersection\<close>
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.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.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.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.133 -subsubsection {* Filter (with comprehension syntax) *}
1.135 -text {* Multiset comprehension *}
1.136 +subsubsection \<open>Filter (with comprehension syntax)\<close>
1.138 +text \<open>Multiset comprehension\<close>
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.146 -subsubsection {* Set of elements *}
1.147 +subsubsection \<open>Set of elements\<close>
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.155 -subsubsection {* Size *}
1.156 +subsubsection \<open>Size\<close>
1.158  definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
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.164 -subsection {* Induction and case splits *}
1.165 +subsection \<open>Induction and case splits\<close>
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.182 -subsubsection {* Strong induction and subset induction for multisets *}
1.184 -text {* Well-foundedness of strict subset relation *}
1.185 +subsubsection \<open>Strong induction and subset induction for multisets\<close>
1.187 +text \<open>Well-foundedness of strict subset relation\<close>
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.204 -subsection {* The fold combinator *}
1.205 +subsection \<open>The fold combinator\<close>
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.211  end
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.225 -subsection {* Image *}
1.226 +\<close>
1.229 +subsection \<open>Image\<close>
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.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.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.252 -subsection {* Further conversions *}
1.253 +subsection \<open>Further conversions\<close>
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.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.276 -subsection {* Big operators *}
1.277 +subsection \<open>Big operators\<close>
1.279  no_notation times (infixl "*" 70)
1.280  no_notation Groups.one ("1")
1.281 @@ -1354,7 +1354,7 @@
1.282  qed
1.285 -subsection {* Replicate operation *}
1.286 +subsection \<open>Replicate operation\<close>
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.294 -subsection {* Alternative representations *}
1.296 -subsubsection {* Lists *}
1.297 +subsection \<open>Alternative representations\<close>
1.299 +subsubsection \<open>Lists\<close>
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.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.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.329 -text {* A stable parametrized quicksort *}
1.330 +text \<open>A stable parametrized quicksort\<close>
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.338 -subsection {* The multiset order *}
1.340 -subsubsection {* Well-foundedness *}
1.341 +subsection \<open>The multiset order\<close>
1.343 +subsubsection \<open>Well-foundedness\<close>
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.365 @@ -1688,9 +1688,9 @@
1.366  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
1.369 -subsubsection {* Closure-free presentation *}
1.371 -text {* One direction. *}
1.372 +subsubsection \<open>Closure-free presentation\<close>
1.374 +text \<open>One direction.\<close>
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.391 -subsubsection {* Partial-order properties *}
1.392 +subsubsection \<open>Partial-order properties\<close>
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.400 -subsubsection {* Monotonicity of multiset union *}
1.401 +subsubsection \<open>Monotonicity of multiset union\<close>
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.409 -subsubsection {* Termination proofs with multiset orders *}
1.410 +subsubsection \<open>Termination proofs with multiset orders\<close>
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.418 -setup {*
1.419 +setup \<open>
1.420  let
1.421    fun msetT T = Type (@{type_name multiset}, [T]);
1.423 @@ -1984,10 +1984,10 @@
1.424      reduction_pair= @{thm ms_reduction_pair}
1.425    })
1.426  end
1.427 -*}
1.430 -subsection {* Legacy theorem bindings *}
1.431 +\<close>
1.434 +subsection \<open>Legacy theorem bindings\<close>
1.436  lemmas multi_count_eq = multiset_eq_iff [symmetric]
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.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.453 -declaration {*
1.454 +\<close>
1.456 +declaration \<open>
1.457  Nitpick_Model.register_term_postprocessor @{typ "'a multiset"}
1.458      multiset_postproc
1.459 -*}
1.462 -subsection {* Naive implementation using lists *}
1.463 +\<close>
1.466 +subsection \<open>Naive implementation using lists\<close>
1.468  code_datatype multiset_of
1.470 @@ -2140,7 +2140,7 @@
1.472  declare sorted_list_of_multiset_multiset_of [code]
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.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.489 -text {* Quickcheck generators *}
1.490 +\<close>
1.492 +text \<open>Quickcheck generators\<close>
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.500 -subsection {* BNF setup *}
1.501 +subsection \<open>BNF setup\<close>
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.509 -subsection {* Size setup *}
1.510 +subsection \<open>Size setup\<close>
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.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.524  hide_const (open) wcount