src/HOL/Enum.thy
 changeset 60758 d8d85a8172b5 parent 60429 d3d1e185cd63 child 61076 bdc1e2f0a86a
```     1.1 --- a/src/HOL/Enum.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Enum.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -1,12 +1,12 @@
1.4  (* Author: Florian Haftmann, TU Muenchen *)
1.5
1.6 -section {* Finite types as explicit enumerations *}
1.7 +section \<open>Finite types as explicit enumerations\<close>
1.8
1.9  theory Enum
1.10  imports Map Groups_List
1.11  begin
1.12
1.13 -subsection {* Class @{text enum} *}
1.14 +subsection \<open>Class @{text enum}\<close>
1.15
1.16  class enum =
1.17    fixes enum :: "'a list"
1.18 @@ -16,7 +16,7 @@
1.19      and enum_distinct: "distinct enum"
1.20    assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
1.21    assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P"
1.22 -   -- {* tailored towards simple instantiation *}
1.23 +   -- \<open>tailored towards simple instantiation\<close>
1.24  begin
1.25
1.26  subclass finite proof
1.27 @@ -52,9 +52,9 @@
1.28  end
1.29
1.30
1.31 -subsection {* Implementations using @{class enum} *}
1.32 +subsection \<open>Implementations using @{class enum}\<close>
1.33
1.34 -subsubsection {* Unbounded operations and quantifiers *}
1.35 +subsubsection \<open>Unbounded operations and quantifiers\<close>
1.36
1.37  lemma Collect_code [code]:
1.38    "Collect P = set (filter P enum)"
1.39 @@ -82,7 +82,7 @@
1.40    by (auto simp add: list_ex1_iff enum_UNIV)
1.41
1.42
1.43 -subsubsection {* An executable choice operator *}
1.44 +subsubsection \<open>An executable choice operator\<close>
1.45
1.46  definition
1.47    [code del]: "enum_the = The"
1.48 @@ -106,7 +106,7 @@
1.49            and "\<forall> x \<in> set vs. \<not> P x"
1.50            and "P a"
1.51            by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
1.52 -        with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
1.53 +        with \<open>P x\<close> in_enum[of x, unfolded enum_eq] \<open>x \<noteq> a\<close> show "False" by auto
1.54        qed
1.55      next
1.56        from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
1.57 @@ -122,7 +122,7 @@
1.58    constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"
1.59
1.60
1.61 -subsubsection {* Equality and order on functions *}
1.62 +subsubsection \<open>Equality and order on functions\<close>
1.63
1.64  instantiation "fun" :: (enum, equal) equal
1.65  begin
1.66 @@ -150,7 +150,7 @@
1.67    by (simp_all add: fun_eq_iff le_fun_def order_less_le)
1.68
1.69
1.70 -subsubsection {* Operations on relations *}
1.71 +subsubsection \<open>Operations on relations\<close>
1.72
1.73  lemma [code]:
1.74    "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
1.75 @@ -177,7 +177,7 @@
1.76    by (auto simp add: mlex_prod_def)
1.77
1.78
1.79 -subsubsection {* Bounded accessible part *}
1.80 +subsubsection \<open>Bounded accessible part\<close>
1.81
1.82  primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set"
1.83  where
1.84 @@ -219,7 +219,7 @@
1.85        fix y assume y: "(y, x) : r"
1.86        with n have "y : bacc r (n y)" by auto
1.87        moreover have "n y <= Max ((%(y, x). n y) ` r)"
1.88 -        using y `finite r` by (auto intro!: Max_ge)
1.89 +        using y \<open>finite r\<close> by (auto intro!: Max_ge)
1.90        note bacc_mono[OF this, of r]
1.91        ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
1.92      qed
1.93 @@ -241,7 +241,7 @@
1.94    by (simp add: card_UNIV_def acc_bacc_eq)
1.95
1.96
1.97 -subsection {* Default instances for @{class enum} *}
1.98 +subsection \<open>Default instances for @{class enum}\<close>
1.99
1.100  lemma map_of_zip_enum_is_Some:
1.101    assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
1.102 @@ -329,7 +329,7 @@
1.103        fix f :: "'a \<Rightarrow> 'b"
1.104        have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.105          by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
1.106 -      from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))"
1.107 +      from \<open>enum_all P\<close> have "P (the \<circ> map_of (zip enum (map f enum)))"
1.108          unfolding enum_all_fun_def all_n_lists_def
1.110          apply (erule_tac x="map f enum" in allE)
1.111 @@ -354,7 +354,7 @@
1.112      from this obtain f where "P f" ..
1.113      have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.114        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
1.115 -    from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
1.116 +    from \<open>P f\<close> this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
1.117        by auto
1.118      from  this show "enum_ex P"
1.119        unfolding enum_ex_fun_def ex_n_lists_def
1.120 @@ -489,9 +489,9 @@
1.121  end
1.122
1.123
1.124 -subsection {* Small finite types *}
1.125 +subsection \<open>Small finite types\<close>
1.126
1.127 -text {* We define small finite types for use in Quickcheck *}
1.128 +text \<open>We define small finite types for use in Quickcheck\<close>
1.129
1.130  datatype (plugins only: code "quickcheck" extraction) finite_1 =
1.131    a\<^sub>1
1.132 @@ -562,12 +562,12 @@
1.133  lemma finite_1_eq: "x = a\<^sub>1"
1.134  by(cases x) simp
1.135
1.136 -simproc_setup finite_1_eq ("x::finite_1") = {*
1.137 +simproc_setup finite_1_eq ("x::finite_1") = \<open>
1.138    fn _ => fn _ => fn ct =>
1.139      (case Thm.term_of ct of
1.140        Const (@{const_name a\<^sub>1}, _) => NONE
1.141      | _ => SOME (mk_meta_eq @{thm finite_1_eq}))
1.142 -*}
1.143 +\<close>
1.144
1.145  instantiation finite_1 :: complete_boolean_algebra
1.146  begin
1.147 @@ -864,8 +864,8 @@
1.148
1.149  instantiation finite_4 :: complete_lattice begin
1.150
1.151 -text {* @{term a\<^sub>1} \$<\$ @{term a\<^sub>2},@{term a\<^sub>3} \$<\$ @{term a\<^sub>4},
1.152 -  but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable. *}
1.153 +text \<open>@{term a\<^sub>1} \$<\$ @{term a\<^sub>2},@{term a\<^sub>3} \$<\$ @{term a\<^sub>4},
1.154 +  but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable.\<close>
1.155
1.156  definition
1.157    "x < y \<longleftrightarrow> (case (x, y) of
1.158 @@ -968,7 +968,7 @@
1.159  instantiation finite_5 :: complete_lattice
1.160  begin
1.161
1.162 -text {* The non-distributive pentagon lattice \$N_5\$ *}
1.163 +text \<open>The non-distributive pentagon lattice \$N_5\$\<close>
1.164
1.165  definition
1.166    "x < y \<longleftrightarrow> (case (x, y) of
1.167 @@ -1034,7 +1034,7 @@
1.168  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5
1.169
1.170
1.171 -subsection {* Closing up *}
1.172 +subsection \<open>Closing up\<close>
1.173
1.174  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
1.175  hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
```