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.109          apply (simp add: set_n_lists)
   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