modernized cartouches
authorhaftmann
Thu Jan 15 13:39:41 2015 +0100 (2015-01-15)
changeset 59377056945909f60
parent 59376 ead400fd6484
child 59378 065f349852e6
modernized cartouches
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Foundations.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Inductive_Predicate.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Refinement.thy
src/Doc/Codegen/Setup.thy
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.3 @@ -2,14 +2,14 @@
     1.4  imports Setup
     1.5  begin
     1.6  
     1.7 -setup %invisible {* Code_Target.add_derived_target ("\<SML>", [("SML", I)])
     1.8 -  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)]) *}
     1.9 +setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
    1.10 +  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)])\<close>
    1.11  
    1.12 -section {* Adaptation to target languages \label{sec:adaptation} *}
    1.13 +section \<open>Adaptation to target languages \label{sec:adaptation}\<close>
    1.14  
    1.15 -subsection {* Adapting code generation *}
    1.16 +subsection \<open>Adapting code generation\<close>
    1.17  
    1.18 -text {*
    1.19 +text \<open>
    1.20    The aspects of code generation introduced so far have two aspects
    1.21    in common:
    1.22  
    1.23 @@ -61,12 +61,12 @@
    1.24    setup by importing particular library theories.  In order to
    1.25    understand these, we provide some clues here; these however are not
    1.26    supposed to replace a careful study of the sources.
    1.27 -*}
    1.28 +\<close>
    1.29  
    1.30  
    1.31 -subsection {* The adaptation principle *}
    1.32 +subsection \<open>The adaptation principle\<close>
    1.33  
    1.34 -text {*
    1.35 +text \<open>
    1.36    Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
    1.37    conceptually supposed to be:
    1.38  
    1.39 @@ -146,11 +146,11 @@
    1.40    \noindent As figure \ref{fig:adaptation} illustrates, all these
    1.41    adaptation mechanisms have to act consistently; it is at the
    1.42    discretion of the user to take care for this.
    1.43 -*}
    1.44 +\<close>
    1.45  
    1.46 -subsection {* Common adaptation patterns *}
    1.47 +subsection \<open>Common adaptation patterns\<close>
    1.48  
    1.49 -text {*
    1.50 +text \<open>
    1.51    The @{theory HOL} @{theory Main} theory already provides a code
    1.52    generator setup which should be suitable for most applications.
    1.53    Common extensions and modifications are available by certain
    1.54 @@ -200,14 +200,14 @@
    1.55         arrays \emph{in SML only}.
    1.56  
    1.57    \end{description}
    1.58 -*}
    1.59 +\<close>
    1.60  
    1.61  
    1.62 -subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
    1.63 +subsection \<open>Parametrising serialisation \label{sec:adaptation_mechanisms}\<close>
    1.64  
    1.65 -text {*
    1.66 +text \<open>
    1.67    Consider the following function and its corresponding SML code:
    1.68 -*}
    1.69 +\<close>
    1.70  
    1.71  primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.72    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
    1.73 @@ -219,11 +219,11 @@
    1.74  | constant HOL.conj \<rightharpoonup> (SML)
    1.75  | constant Not \<rightharpoonup> (SML)
    1.76  (*>*)
    1.77 -text %quotetypewriter {*
    1.78 +text %quotetypewriter \<open>
    1.79    @{code_stmts in_interval (SML)}
    1.80 -*}
    1.81 +\<close>
    1.82  
    1.83 -text {*
    1.84 +text \<open>
    1.85    \noindent Though this is correct code, it is a little bit
    1.86    unsatisfactory: boolean values and operators are materialised as
    1.87    distinguished entities with have nothing to do with the SML-built-in
    1.88 @@ -232,7 +232,7 @@
    1.89    which would perfectly terminate when the existing SML @{verbatim
    1.90    "bool"} would be used.  To map the HOL @{typ bool} on SML @{verbatim
    1.91    "bool"}, we may use \qn{custom serialisations}:
    1.92 -*}
    1.93 +\<close>
    1.94  
    1.95  code_printing %quotett
    1.96    type_constructor bool \<rightharpoonup> (SML) "bool"
    1.97 @@ -240,7 +240,7 @@
    1.98  | constant False \<rightharpoonup> (SML) "false"
    1.99  | constant HOL.conj \<rightharpoonup> (SML) "_ andalso _"
   1.100  
   1.101 -text {*
   1.102 +text \<open>
   1.103    \noindent The @{command_def code_printing} command takes a series
   1.104    of symbols (contants, type constructor, \ldots)
   1.105    together with target-specific custom serialisations.  Each
   1.106 @@ -249,28 +249,28 @@
   1.107    inserted whenever the type constructor would occur.  Each
   1.108    ``@{verbatim "_"}'' in a serialisation expression is treated as a
   1.109    placeholder for the constant's or the type constructor's arguments.
   1.110 -*}
   1.111 +\<close>
   1.112  
   1.113 -text %quotetypewriter {*
   1.114 +text %quotetypewriter \<open>
   1.115    @{code_stmts in_interval (SML)}
   1.116 -*}
   1.117 +\<close>
   1.118  
   1.119 -text {*
   1.120 +text \<open>
   1.121    \noindent This still is not perfect: the parentheses around the
   1.122    \qt{andalso} expression are superfluous.  Though the serialiser by
   1.123    no means attempts to imitate the rich Isabelle syntax framework, it
   1.124    provides some common idioms, notably associative infixes with
   1.125    precedences which may be used here:
   1.126 -*}
   1.127 +\<close>
   1.128  
   1.129  code_printing %quotett
   1.130    constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
   1.131  
   1.132 -text %quotetypewriter {*
   1.133 +text %quotetypewriter \<open>
   1.134    @{code_stmts in_interval (SML)}
   1.135 -*}
   1.136 +\<close>
   1.137  
   1.138 -text {*
   1.139 +text \<open>
   1.140    \noindent The attentive reader may ask how we assert that no
   1.141    generated code will accidentally overwrite.  For this reason the
   1.142    serialiser has an internal table of identifiers which have to be
   1.143 @@ -278,14 +278,14 @@
   1.144    typically contains the keywords of the target language.  It can be
   1.145    extended manually, thus avoiding accidental overwrites, using the
   1.146    @{command_def "code_reserved"} command:
   1.147 -*}
   1.148 +\<close>
   1.149  
   1.150  code_reserved %quote "\<SMLdummy>" bool true false andalso
   1.151  
   1.152 -text {*
   1.153 +text \<open>
   1.154    \noindent Next, we try to map HOL pairs to SML pairs, using the
   1.155    infix ``@{verbatim "*"}'' type constructor and parentheses:
   1.156 -*}
   1.157 +\<close>
   1.158  (*<*)
   1.159  code_printing %invisible
   1.160    type_constructor prod \<rightharpoonup> (SML)
   1.161 @@ -295,7 +295,7 @@
   1.162    type_constructor prod \<rightharpoonup> (SML) infix 2 "*"
   1.163  | constant Pair \<rightharpoonup> (SML) "!((_),/ (_))"
   1.164  
   1.165 -text {*
   1.166 +text \<open>
   1.167    \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
   1.168    never to put parentheses around the whole expression (they are
   1.169    already present), while the parentheses around argument place
   1.170 @@ -314,28 +314,28 @@
   1.171    in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
   1.172    proper underscore while the second ``@{verbatim "_"}'' is a
   1.173    placeholder.
   1.174 -*}
   1.175 +\<close>
   1.176  
   1.177  
   1.178 -subsection {* @{text Haskell} serialisation *}
   1.179 +subsection \<open>@{text Haskell} serialisation\<close>
   1.180  
   1.181 -text {*
   1.182 +text \<open>
   1.183    For convenience, the default @{text HOL} setup for @{text Haskell}
   1.184    maps the @{class equal} class to its counterpart in @{text Haskell},
   1.185    giving custom serialisations for the class @{class equal}
   1.186    and its operation @{const [source] HOL.equal}.
   1.187 -*}
   1.188 +\<close>
   1.189  
   1.190  code_printing %quotett
   1.191    type_class equal \<rightharpoonup> (Haskell) "Eq"
   1.192  | constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "=="
   1.193  
   1.194 -text {*
   1.195 +text \<open>
   1.196    \noindent A problem now occurs whenever a type which is an instance
   1.197    of @{class equal} in @{text HOL} is mapped on a @{text
   1.198    Haskell}-built-in type which is also an instance of @{text Haskell}
   1.199    @{text Eq}:
   1.200 -*}
   1.201 +\<close>
   1.202  
   1.203  typedecl %quote bar
   1.204  
   1.205 @@ -351,35 +351,35 @@
   1.206  (*>*) code_printing %quotett
   1.207    type_constructor bar \<rightharpoonup> (Haskell) "Integer"
   1.208  
   1.209 -text {*
   1.210 +text \<open>
   1.211    \noindent The code generator would produce an additional instance,
   1.212    which of course is rejected by the @{text Haskell} compiler.  To
   1.213    suppress this additional instance:
   1.214 -*}
   1.215 +\<close>
   1.216  
   1.217  code_printing %quotett
   1.218    class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -
   1.219  
   1.220  
   1.221 -subsection {* Enhancing the target language context \label{sec:include} *}
   1.222 +subsection \<open>Enhancing the target language context \label{sec:include}\<close>
   1.223  
   1.224 -text {*
   1.225 +text \<open>
   1.226    In rare cases it is necessary to \emph{enrich} the context of a
   1.227    target language; this can also be accomplished using the @{command
   1.228    "code_printing"} command:
   1.229 -*}
   1.230 +\<close>
   1.231  
   1.232  code_printing %quotett
   1.233 -  code_module "Errno" \<rightharpoonup> (Haskell) {*errno i = error ("Error number: " ++ show i)*}
   1.234 +  code_module "Errno" \<rightharpoonup> (Haskell) \<open>errno i = error ("Error number: " ++ show i)\<close>
   1.235  
   1.236  code_reserved %quotett Haskell Errno
   1.237  
   1.238 -text {*
   1.239 +text \<open>
   1.240    \noindent Such named modules are then prepended to every
   1.241    generated code.  Inspect such code in order to find out how
   1.242    this behaves with respect to a particular
   1.243    target language.
   1.244 -*}
   1.245 +\<close>
   1.246  
   1.247  end
   1.248  
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     2.3 @@ -2,9 +2,9 @@
     2.4  imports Setup
     2.5  begin
     2.6  
     2.7 -section {* Evaluation \label{sec:evaluation} *}
     2.8 +section \<open>Evaluation \label{sec:evaluation}\<close>
     2.9  
    2.10 -text {*
    2.11 +text \<open>
    2.12    Recalling \secref{sec:principle}, code generation turns a system of
    2.13    equations into a program with the \emph{same} equational semantics.
    2.14    As a consequence, this program can be used as a \emph{rewrite
    2.15 @@ -12,12 +12,12 @@
    2.16    term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
    2.17    application of code generation in the following is referred to as
    2.18    \emph{evaluation}.
    2.19 -*}
    2.20 +\<close>
    2.21  
    2.22  
    2.23 -subsection {* Evaluation techniques *}
    2.24 +subsection \<open>Evaluation techniques\<close>
    2.25  
    2.26 -text {*
    2.27 +text \<open>
    2.28    The existing infrastructure provides a rich palette of evaluation
    2.29    techniques, each comprising different aspects:
    2.30  
    2.31 @@ -35,34 +35,34 @@
    2.32        trustable.
    2.33  
    2.34    \end{description}
    2.35 -*}
    2.36 +\<close>
    2.37  
    2.38  
    2.39 -subsubsection {* The simplifier (@{text simp}) *}
    2.40 +subsubsection \<open>The simplifier (@{text simp})\<close>
    2.41  
    2.42 -text {*
    2.43 +text \<open>
    2.44    The simplest way for evaluation is just using the simplifier with
    2.45    the original code equations of the underlying program.  This gives
    2.46    fully symbolic evaluation and highest trustablity, with the usual
    2.47    performance of the simplifier.  Note that for operations on abstract
    2.48    datatypes (cf.~\secref{sec:invariant}), the original theorems as
    2.49    given by the users are used, not the modified ones.
    2.50 -*}
    2.51 +\<close>
    2.52  
    2.53  
    2.54 -subsubsection {* Normalization by evaluation (@{text nbe}) *}
    2.55 +subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>
    2.56  
    2.57 -text {*
    2.58 +text \<open>
    2.59    Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
    2.60    provides a comparably fast partially symbolic evaluation which
    2.61    permits also normalization of functions and uninterpreted symbols;
    2.62    the stack of code to be trusted is considerable.
    2.63 -*}
    2.64 +\<close>
    2.65  
    2.66  
    2.67 -subsubsection {* Evaluation in ML (@{text code}) *}
    2.68 +subsubsection \<open>Evaluation in ML (@{text code})\<close>
    2.69  
    2.70 -text {*
    2.71 +text \<open>
    2.72    Highest performance can be achieved by evaluation in ML, at the cost
    2.73    of being restricted to ground results and a layered stack of code to
    2.74    be trusted, including code generator configurations by the user.
    2.75 @@ -73,32 +73,32 @@
    2.76    out there depends crucially on the correctness of the code
    2.77    generator setup; this is one of the reasons why you should not use
    2.78    adaptation (see \secref{sec:adaptation}) frivolously.
    2.79 -*}
    2.80 +\<close>
    2.81  
    2.82  
    2.83 -subsection {* Aspects of evaluation *}
    2.84 +subsection \<open>Aspects of evaluation\<close>
    2.85  
    2.86 -text {*
    2.87 +text \<open>
    2.88    Each of the techniques can be combined with different aspects.  The
    2.89    most important distinction is between dynamic and static evaluation.
    2.90    Dynamic evaluation takes the code generator configuration \qt{as it
    2.91    is} at the point where evaluation is issued.  Best example is the
    2.92    @{command_def value} command which allows ad-hoc evaluation of
    2.93    terms:
    2.94 -*}
    2.95 +\<close>
    2.96  
    2.97  value %quote "42 / (12 :: rat)"
    2.98  
    2.99 -text {*
   2.100 +text \<open>
   2.101    \noindent @{command value} tries first to evaluate using ML, falling
   2.102    back to normalization by evaluation if this fails.
   2.103  
   2.104    A particular technique may be specified in square brackets, e.g.
   2.105 -*}
   2.106 +\<close>
   2.107  
   2.108  value %quote [nbe] "42 / (12 :: rat)"
   2.109  
   2.110 -text {*
   2.111 +text \<open>
   2.112    To employ dynamic evaluation in the document generation, there is also
   2.113    a @{text value} antiquotation with the same evaluation techniques 
   2.114    as @{command value}.
   2.115 @@ -162,12 +162,12 @@
   2.116    For property conversion (which coincides with conversion except for
   2.117    evaluation in ML), methods are provided which solve a given goal by
   2.118    evaluation.
   2.119 -*}
   2.120 +\<close>
   2.121  
   2.122  
   2.123 -subsection {* Schematic overview *}
   2.124 +subsection \<open>Schematic overview\<close>
   2.125  
   2.126 -text {*
   2.127 +text \<open>
   2.128    \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   2.129    \fontsize{9pt}{12pt}\selectfont
   2.130    \begin{tabular}{ll||c|c|c}
   2.131 @@ -189,12 +189,12 @@
   2.132        & \ttsize@{ML "Nbe.static_conv"}
   2.133        & \ttsize@{ML "Code_Evaluation.static_conv"}
   2.134    \end{tabular}
   2.135 -*}
   2.136 +\<close>
   2.137  
   2.138  
   2.139 -subsection {* Preprocessing HOL terms into evaluable shape *}
   2.140 +subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   2.141  
   2.142 -text {*
   2.143 +text \<open>
   2.144    When integration decision procedures developed inside HOL into HOL itself,
   2.145    it is necessary to somehow get from the Isabelle/ML representation to
   2.146    the representation used by the decision procedure itself (``reification'').
   2.147 @@ -203,7 +203,7 @@
   2.148    @{ML "Reification.conv"} and @{ML "Reification.tac"}
   2.149  
   2.150    An simplistic example:
   2.151 -*}
   2.152 +\<close>
   2.153  
   2.154  datatype %quote form_ord = T | F | Less nat nat
   2.155    | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   2.156 @@ -217,21 +217,21 @@
   2.157  | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   2.158  | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   2.159  
   2.160 -text {*
   2.161 +text \<open>
   2.162    The datatype @{type form_ord} represents formulae whose semantics is given by
   2.163    @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   2.164    whose concrete values are given in list @{term vs}.
   2.165 -*}
   2.166 +\<close>
   2.167  
   2.168 -ML (*<*) {* *}
   2.169 +ML (*<*) \<open>\<close>
   2.170  schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
   2.171  ML_prf 
   2.172 -(*>*) {* val thm =
   2.173 -  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
   2.174 -by (tactic {* ALLGOALS (rtac thm) *})
   2.175 +(*>*) \<open>val thm =
   2.176 +  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   2.177 +by (tactic \<open>ALLGOALS (rtac thm)\<close>)
   2.178  (*>*) 
   2.179  
   2.180 -text {*
   2.181 +text \<open>
   2.182    By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   2.183    which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   2.184    to @{const interp} does not contain any free variables and can thus be evaluated
   2.185 @@ -239,38 +239,38 @@
   2.186  
   2.187    A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   2.188    theory @{text Regexp_Method}.
   2.189 -*}
   2.190 +\<close>
   2.191  
   2.192  
   2.193 -subsection {* Intimate connection between logic and system runtime *}
   2.194 +subsection \<open>Intimate connection between logic and system runtime\<close>
   2.195  
   2.196 -text {*
   2.197 +text \<open>
   2.198    The toolbox of static evaluation conversions forms a reasonable base
   2.199    to interweave generated code and system tools.  However in some
   2.200    situations more direct interaction is desirable.
   2.201 -*}
   2.202 +\<close>
   2.203  
   2.204  
   2.205 -subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
   2.206 +subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
   2.207  
   2.208 -text {*
   2.209 +text \<open>
   2.210    The @{text code} antiquotation allows to include constants from
   2.211    generated code directly into ML system code, as in the following toy
   2.212    example:
   2.213 -*}
   2.214 +\<close>
   2.215  
   2.216  datatype %quote form = T | F | And form form | Or form form (*<*)
   2.217  
   2.218 -(*>*) ML %quotett {*
   2.219 +(*>*) ML %quotett \<open>
   2.220    fun eval_form @{code T} = true
   2.221      | eval_form @{code F} = false
   2.222      | eval_form (@{code And} (p, q)) =
   2.223          eval_form p andalso eval_form q
   2.224      | eval_form (@{code Or} (p, q)) =
   2.225          eval_form p orelse eval_form q;
   2.226 -*}
   2.227 +\<close>
   2.228  
   2.229 -text {*
   2.230 +text \<open>
   2.231    \noindent @{text code} takes as argument the name of a constant;
   2.232    after the whole ML is read, the necessary code is generated
   2.233    transparently and the corresponding constant names are inserted.
   2.234 @@ -281,24 +281,24 @@
   2.235  
   2.236    For a less simplistic example, theory @{text Approximation} in
   2.237    the @{text Decision_Procs} session is a good reference.
   2.238 -*}
   2.239 +\<close>
   2.240  
   2.241  
   2.242 -subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
   2.243 +subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
   2.244  
   2.245 -text {*
   2.246 +text \<open>
   2.247    The @{text code} antiquoation is lightweight, but the generated code
   2.248    is only accessible while the ML section is processed.  Sometimes this
   2.249    is not appropriate, especially if the generated code contains datatype
   2.250    declarations which are shared with other parts of the system.  In these
   2.251    cases, @{command_def code_reflect} can be used:
   2.252 -*}
   2.253 +\<close>
   2.254  
   2.255  code_reflect %quote Sum_Type
   2.256    datatypes sum = Inl | Inr
   2.257    functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
   2.258  
   2.259 -text {*
   2.260 +text \<open>
   2.261    \noindent @{command_def code_reflect} takes a structure name and
   2.262    references to datatypes and functions; for these code is compiled
   2.263    into the named ML structure and the \emph{Eval} target is modified
   2.264 @@ -309,17 +309,17 @@
   2.265  
   2.266    A typical example for @{command code_reflect} can be found in the
   2.267    @{theory Predicate} theory.
   2.268 -*}
   2.269 +\<close>
   2.270  
   2.271  
   2.272 -subsubsection {* Separate compilation -- @{text code_reflect} *}
   2.273 +subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
   2.274  
   2.275 -text {*
   2.276 +text \<open>
   2.277    For technical reasons it is sometimes necessary to separate
   2.278    generation and compilation of code which is supposed to be used in
   2.279    the system runtime.  For this @{command code_reflect} with an
   2.280    optional @{text "file"} argument can be used:
   2.281 -*}
   2.282 +\<close>
   2.283  
   2.284  code_reflect %quote Rat
   2.285    datatypes rat = Frct
   2.286 @@ -328,10 +328,10 @@
   2.287      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   2.288    file "$ISABELLE_TMP/examples/rat.ML"
   2.289  
   2.290 -text {*
   2.291 +text \<open>
   2.292    \noindent This merely generates the referenced code to the given
   2.293    file which can be included into the system runtime later on.
   2.294 -*}
   2.295 +\<close>
   2.296  
   2.297  end
   2.298  
     3.1 --- a/src/Doc/Codegen/Foundations.thy	Thu Jan 15 13:39:41 2015 +0100
     3.2 +++ b/src/Doc/Codegen/Foundations.thy	Thu Jan 15 13:39:41 2015 +0100
     3.3 @@ -2,11 +2,11 @@
     3.4  imports Introduction
     3.5  begin
     3.6  
     3.7 -section {* Code generation foundations \label{sec:foundations} *}
     3.8 +section \<open>Code generation foundations \label{sec:foundations}\<close>
     3.9  
    3.10 -subsection {* Code generator architecture \label{sec:architecture} *}
    3.11 +subsection \<open>Code generator architecture \label{sec:architecture}\<close>
    3.12  
    3.13 -text {*
    3.14 +text \<open>
    3.15    The code generator is actually a framework consisting of different
    3.16    components which can be customised individually.
    3.17  
    3.18 @@ -90,12 +90,12 @@
    3.19    \noindent From these steps, only the last two are carried out
    3.20    outside the logic; by keeping this layer as thin as possible, the
    3.21    amount of code to trust is kept to a minimum.
    3.22 -*}
    3.23 +\<close>
    3.24  
    3.25  
    3.26 -subsection {* The pre- and postprocessor \label{sec:preproc} *}
    3.27 +subsection \<open>The pre- and postprocessor \label{sec:preproc}\<close>
    3.28  
    3.29 -text {*
    3.30 +text \<open>
    3.31    Before selected function theorems are turned into abstract code, a
    3.32    chain of definitional transformation steps is carried out:
    3.33    \emph{preprocessing}.  The preprocessor consists of two
    3.34 @@ -122,13 +122,13 @@
    3.35    is is just expressed as @{term "x \<in> set xs"}.  But for execution
    3.36    the intermediate set is not desirable.  Hence the following
    3.37    specification:
    3.38 -*}
    3.39 +\<close>
    3.40  
    3.41  definition %quote member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
    3.42  where
    3.43    [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
    3.44  
    3.45 -text {*
    3.46 +text \<open>
    3.47    \noindent The \emph{@{attribute code_abbrev} attribute} declares
    3.48    its theorem a rewrite rule for the postprocessor and the symmetric
    3.49    of its theorem as rewrite rule for the preprocessor.  Together,
    3.50 @@ -153,12 +153,12 @@
    3.51    code_thms} (see \secref{sec:equations}) provides a convenient
    3.52    mechanism to inspect the impact of a preprocessor setup on code
    3.53    equations.
    3.54 -*}
    3.55 +\<close>
    3.56  
    3.57  
    3.58 -subsection {* Understanding code equations \label{sec:equations} *}
    3.59 +subsection \<open>Understanding code equations \label{sec:equations}\<close>
    3.60  
    3.61 -text {*
    3.62 +text \<open>
    3.63    As told in \secref{sec:principle}, the notion of code equations is
    3.64    vital to code generation.  Indeed most problems which occur in
    3.65    practice can be resolved by an inspection of the underlying code
    3.66 @@ -166,7 +166,7 @@
    3.67  
    3.68    It is possible to exchange the default code equations for constants
    3.69    by explicitly proving alternative ones:
    3.70 -*}
    3.71 +\<close>
    3.72  
    3.73  lemma %quote [code]:
    3.74    "dequeue (AQueue xs []) =
    3.75 @@ -176,18 +176,18 @@
    3.76       (Some y, AQueue xs ys)"
    3.77    by (cases xs, simp_all) (cases "rev xs", simp_all)
    3.78  
    3.79 -text {*
    3.80 +text \<open>
    3.81    \noindent The annotation @{text "[code]"} is an @{text attribute}
    3.82    which states that the given theorems should be considered as code
    3.83    equations for a @{text fun} statement -- the corresponding constant
    3.84    is determined syntactically.  The resulting code:
    3.85 -*}
    3.86 +\<close>
    3.87  
    3.88 -text %quotetypewriter {*
    3.89 +text %quotetypewriter \<open>
    3.90    @{code_stmts dequeue (consts) dequeue (Haskell)}
    3.91 -*}
    3.92 +\<close>
    3.93  
    3.94 -text {*
    3.95 +text \<open>
    3.96    \noindent You may note that the equality test @{term "xs = []"} has
    3.97    been replaced by the predicate @{term "List.null xs"}.  This is due
    3.98    to the default setup of the \qn{preprocessor}.
    3.99 @@ -206,24 +206,24 @@
   3.100    The code equations after preprocessing are already are blueprint of
   3.101    the generated program and can be inspected using the @{command
   3.102    code_thms} command:
   3.103 -*}
   3.104 +\<close>
   3.105  
   3.106  code_thms %quote dequeue
   3.107  
   3.108 -text {*
   3.109 +text \<open>
   3.110    \noindent This prints a table with the code equations for @{const
   3.111    dequeue}, including \emph{all} code equations those equations depend
   3.112    on recursively.  These dependencies themselves can be visualized using
   3.113    the @{command_def code_deps} command.
   3.114 -*}
   3.115 +\<close>
   3.116  
   3.117  
   3.118 -subsection {* Equality *}
   3.119 +subsection \<open>Equality\<close>
   3.120  
   3.121 -text {*
   3.122 +text \<open>
   3.123    Implementation of equality deserves some attention.  Here an example
   3.124    function involving polymorphic equality:
   3.125 -*}
   3.126 +\<close>
   3.127  
   3.128  primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   3.129    "collect_duplicates xs ys [] = xs"
   3.130 @@ -233,17 +233,17 @@
   3.131        else collect_duplicates xs (z#ys) zs
   3.132      else collect_duplicates (z#xs) (z#ys) zs)"
   3.133  
   3.134 -text {*
   3.135 +text \<open>
   3.136    \noindent During preprocessing, the membership test is rewritten,
   3.137    resulting in @{const List.member}, which itself performs an explicit
   3.138    equality check, as can be seen in the corresponding @{text SML} code:
   3.139 -*}
   3.140 +\<close>
   3.141  
   3.142 -text %quotetypewriter {*
   3.143 +text %quotetypewriter \<open>
   3.144    @{code_stmts collect_duplicates (SML)}
   3.145 -*}
   3.146 +\<close>
   3.147  
   3.148 -text {*
   3.149 +text \<open>
   3.150    \noindent Obviously, polymorphic equality is implemented the Haskell
   3.151    way using a type class.  How is this achieved?  HOL introduces an
   3.152    explicit class @{class equal} with a corresponding operation @{const
   3.153 @@ -252,15 +252,15 @@
   3.154    through all dependent code equations.  For datatypes, instances of
   3.155    @{class equal} are implicitly derived when possible.  For other types,
   3.156    you may instantiate @{text equal} manually like any other type class.
   3.157 -*}
   3.158 +\<close>
   3.159  
   3.160  
   3.161 -subsection {* Explicit partiality \label{sec:partiality} *}
   3.162 +subsection \<open>Explicit partiality \label{sec:partiality}\<close>
   3.163  
   3.164 -text {*
   3.165 +text \<open>
   3.166    Partiality usually enters the game by partial patterns, as
   3.167    in the following example, again for amortised queues:
   3.168 -*}
   3.169 +\<close>
   3.170  
   3.171  definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   3.172    "strict_dequeue q = (case dequeue q
   3.173 @@ -272,19 +272,19 @@
   3.174      (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
   3.175    by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
   3.176  
   3.177 -text {*
   3.178 +text \<open>
   3.179    \noindent In the corresponding code, there is no equation
   3.180    for the pattern @{term "AQueue [] []"}:
   3.181 -*}
   3.182 +\<close>
   3.183  
   3.184 -text %quotetypewriter {*
   3.185 +text %quotetypewriter \<open>
   3.186    @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
   3.187 -*}
   3.188 +\<close>
   3.189  
   3.190 -text {*
   3.191 +text \<open>
   3.192    \noindent In some cases it is desirable to have this
   3.193    pseudo-\qt{partiality} more explicitly, e.g.~as follows:
   3.194 -*}
   3.195 +\<close>
   3.196  
   3.197  axiomatization %quote empty_queue :: 'a
   3.198  
   3.199 @@ -298,7 +298,7 @@
   3.200       (y, AQueue xs ys)"
   3.201    by (simp_all add: strict_dequeue'_def split: list.splits)
   3.202  
   3.203 -text {*
   3.204 +text \<open>
   3.205    Observe that on the right hand side of the definition of @{const
   3.206    "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
   3.207  
   3.208 @@ -310,30 +310,30 @@
   3.209    side.  In order to categorise a constant into that category
   3.210    explicitly, use the @{attribute code} attribute with
   3.211    @{text abort}:
   3.212 -*}
   3.213 +\<close>
   3.214  
   3.215  declare %quote [[code abort: empty_queue]]
   3.216  
   3.217 -text {*
   3.218 +text \<open>
   3.219    \noindent Then the code generator will just insert an error or
   3.220    exception at the appropriate position:
   3.221 -*}
   3.222 +\<close>
   3.223  
   3.224 -text %quotetypewriter {*
   3.225 +text %quotetypewriter \<open>
   3.226    @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
   3.227 -*}
   3.228 +\<close>
   3.229  
   3.230 -text {*
   3.231 +text \<open>
   3.232    \noindent This feature however is rarely needed in practice.  Note
   3.233    also that the HOL default setup already declares @{const undefined},
   3.234    which is most likely to be used in such situations, as
   3.235    @{text "code abort"}.
   3.236 -*}
   3.237 +\<close>
   3.238  
   3.239  
   3.240 -subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}
   3.241 +subsection \<open>If something goes utterly wrong \label{sec:utterly_wrong}\<close>
   3.242  
   3.243 -text {*
   3.244 +text \<open>
   3.245    Under certain circumstances, the code generator fails to produce
   3.246    code entirely.  To debug these, the following hints may prove
   3.247    helpful:
   3.248 @@ -371,6 +371,6 @@
   3.249        class signatures (\qt{wellsortedness error}).
   3.250  
   3.251    \end{description}
   3.252 -*}
   3.253 +\<close>
   3.254  
   3.255  end
     4.1 --- a/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     4.2 +++ b/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     4.3 @@ -2,11 +2,11 @@
     4.4  imports Setup "~~/src/Tools/Permanent_Interpretation"
     4.5  begin
     4.6  
     4.7 -section {* Further issues \label{sec:further} *}
     4.8 +section \<open>Further issues \label{sec:further}\<close>
     4.9  
    4.10 -subsection {* Specialities of the @{text Scala} target language \label{sec:scala} *}
    4.11 +subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
    4.12  
    4.13 -text {*
    4.14 +text \<open>
    4.15    @{text Scala} deviates from languages of the ML family in a couple
    4.16    of aspects; those which affect code generation mainly have to do with
    4.17    @{text Scala}'s type system:
    4.18 @@ -43,7 +43,7 @@
    4.19    Isabelle's type classes are mapped onto @{text Scala} implicits; in
    4.20    cases with diamonds in the subclass hierarchy this can lead to
    4.21    ambiguities in the generated code:
    4.22 -*}
    4.23 +\<close>
    4.24  
    4.25  class %quote class1 =
    4.26    fixes foo :: "'a \<Rightarrow> 'a"
    4.27 @@ -52,62 +52,62 @@
    4.28  
    4.29  class %quote class3 = class1
    4.30  
    4.31 -text {*
    4.32 +text \<open>
    4.33    \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
    4.34    forming the upper part of a diamond.
    4.35 -*}
    4.36 +\<close>
    4.37  
    4.38  definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
    4.39    "bar = foo"
    4.40  
    4.41 -text {*
    4.42 +text \<open>
    4.43    \noindent This yields the following code:
    4.44 -*}
    4.45 +\<close>
    4.46  
    4.47 -text %quotetypewriter {*
    4.48 +text %quotetypewriter \<open>
    4.49    @{code_stmts bar (Scala)}
    4.50 -*}
    4.51 +\<close>
    4.52  
    4.53 -text {*
    4.54 +text \<open>
    4.55    \noindent This code is rejected by the @{text Scala} compiler: in
    4.56    the definition of @{text bar}, it is not clear from where to derive
    4.57    the implicit argument for @{text foo}.
    4.58  
    4.59    The solution to the problem is to close the diamond by a further
    4.60    class with inherits from both @{class class2} and @{class class3}:
    4.61 -*}
    4.62 +\<close>
    4.63  
    4.64  class %quote class4 = class2 + class3
    4.65  
    4.66 -text {*
    4.67 +text \<open>
    4.68    \noindent Then the offending code equation can be restricted to
    4.69    @{class class4}:
    4.70 -*}
    4.71 +\<close>
    4.72  
    4.73  lemma %quote [code]:
    4.74    "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
    4.75    by (simp only: bar_def)
    4.76  
    4.77 -text {*
    4.78 +text \<open>
    4.79    \noindent with the following code:
    4.80 -*}
    4.81 +\<close>
    4.82  
    4.83 -text %quotetypewriter {*
    4.84 +text %quotetypewriter \<open>
    4.85    @{code_stmts bar (Scala)}
    4.86 -*}
    4.87 +\<close>
    4.88  
    4.89 -text {*
    4.90 +text \<open>
    4.91    \noindent which exposes no ambiguity.
    4.92  
    4.93    Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
    4.94    constraints through a system of code equations, it is usually not
    4.95    very difficult to identify the set of code equations which actually
    4.96    needs more restricted sort constraints.
    4.97 -*}
    4.98 +\<close>
    4.99  
   4.100 -subsection {* Modules namespace *}
   4.101 +subsection \<open>Modules namespace\<close>
   4.102  
   4.103 -text {*
   4.104 +text \<open>
   4.105    When invoking the @{command export_code} command it is possible to
   4.106    leave out the @{keyword "module_name"} part; then code is
   4.107    distributed over different modules, where the module name space
   4.108 @@ -122,38 +122,38 @@
   4.109    A solution is to declare module names explicitly.  Let use assume
   4.110    the three cyclically dependent modules are named \emph{A}, \emph{B}
   4.111    and \emph{C}.  Then, by stating
   4.112 -*}
   4.113 +\<close>
   4.114  
   4.115  code_identifier %quote
   4.116    code_module A \<rightharpoonup> (SML) ABC
   4.117  | code_module B \<rightharpoonup> (SML) ABC
   4.118  | code_module C \<rightharpoonup> (SML) ABC
   4.119  
   4.120 -text {*
   4.121 +text \<open>
   4.122    \noindent we explicitly map all those modules on \emph{ABC},
   4.123    resulting in an ad-hoc merge of this three modules at serialisation
   4.124    time.
   4.125 -*}
   4.126 +\<close>
   4.127  
   4.128 -subsection {* Locales and interpretation *}
   4.129 +subsection \<open>Locales and interpretation\<close>
   4.130  
   4.131 -text {*
   4.132 +text \<open>
   4.133    A technical issue comes to surface when generating code from
   4.134    specifications stemming from locale interpretation.
   4.135  
   4.136    Let us assume a locale specifying a power operation on arbitrary
   4.137    types:
   4.138 -*}
   4.139 +\<close>
   4.140  
   4.141  locale %quote power =
   4.142    fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   4.143    assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
   4.144  begin
   4.145  
   4.146 -text {*
   4.147 +text \<open>
   4.148    \noindent Inside that locale we can lift @{text power} to exponent
   4.149    lists by means of specification relative to that locale:
   4.150 -*}
   4.151 +\<close>
   4.152  
   4.153  primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   4.154    "powers [] = id"
   4.155 @@ -175,7 +175,7 @@
   4.156  
   4.157  end %quote
   4.158  
   4.159 -text {*
   4.160 +text \<open>
   4.161    After an interpretation of this locale (say, @{command_def
   4.162    interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
   4.163    :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
   4.164 @@ -189,43 +189,43 @@
   4.165    achieved.  First, a dedicated definition of the constant on which
   4.166    the local @{text "powers"} after interpretation is supposed to be
   4.167    mapped on:
   4.168 -*}
   4.169 +\<close>
   4.170  
   4.171  definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   4.172    [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
   4.173  
   4.174 -text {*
   4.175 +text \<open>
   4.176    \noindent In general, the pattern is @{text "c = t"} where @{text c}
   4.177    is the name of the future constant and @{text t} the foundational
   4.178    term corresponding to the local constant after interpretation.
   4.179  
   4.180    The interpretation itself is enriched with an equation @{text "t = c"}:
   4.181 -*}
   4.182 +\<close>
   4.183  
   4.184  interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
   4.185    "power.powers (\<lambda>n f. f ^^ n) = funpows"
   4.186    by unfold_locales
   4.187      (simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
   4.188  
   4.189 -text {*
   4.190 +text \<open>
   4.191    \noindent This additional equation is trivially proved by the
   4.192    definition itself.
   4.193  
   4.194    After this setup procedure, code generation can continue as usual:
   4.195 -*}
   4.196 +\<close>
   4.197  
   4.198 -text %quotetypewriter {*
   4.199 +text %quotetypewriter \<open>
   4.200    @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
   4.201 -*} (*<*)
   4.202 +\<close> (*<*)
   4.203  
   4.204 -(*>*) text {*
   4.205 +(*>*) text \<open>
   4.206    Fortunately, an even more succint approach is available using command
   4.207    @{command permanent_interpretation}.  This is available
   4.208    by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
   4.209    Then the pattern above collapses to
   4.210 -*} (*<*)
   4.211 +\<close> (*<*)
   4.212  
   4.213 -setup {* Sign.add_path "funpows" *}
   4.214 +setup \<open>Sign.add_path "funpows"\<close>
   4.215  hide_const (open) funpows
   4.216  
   4.217  (*>*)
   4.218 @@ -234,43 +234,43 @@
   4.219    by unfold_locales
   4.220      (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
   4.221  
   4.222 -setup {* Sign.parent_path *}
   4.223 +setup \<open>Sign.parent_path\<close>
   4.224  
   4.225  (*>*)
   4.226  
   4.227  
   4.228 -subsection {* Parallel computation *}
   4.229 +subsection \<open>Parallel computation\<close>
   4.230  
   4.231 -text {*
   4.232 +text \<open>
   4.233    Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
   4.234    operations to exploit parallelism inside the Isabelle/ML
   4.235    runtime engine.
   4.236 -*}
   4.237 +\<close>
   4.238  
   4.239 -subsection {* Imperative data structures *}
   4.240 +subsection \<open>Imperative data structures\<close>
   4.241  
   4.242 -text {*
   4.243 +text \<open>
   4.244    If you consider imperative data structures as inevitable for a
   4.245    specific application, you should consider \emph{Imperative
   4.246    Functional Programming with Isabelle/HOL}
   4.247    @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
   4.248    is available in session @{text Imperative_HOL}, together with a
   4.249    short primer document.
   4.250 -*}
   4.251 +\<close>
   4.252  
   4.253  
   4.254 -subsection {* ML system interfaces \label{sec:ml} *}
   4.255 +subsection \<open>ML system interfaces \label{sec:ml}\<close>
   4.256  
   4.257 -text {*
   4.258 +text \<open>
   4.259    Since the code generator framework not only aims to provide a nice
   4.260    Isar interface but also to form a base for code-generation-based
   4.261    applications, here a short description of the most fundamental ML
   4.262    interfaces.
   4.263 -*}
   4.264 +\<close>
   4.265  
   4.266 -subsubsection {* Managing executable content *}
   4.267 +subsubsection \<open>Managing executable content\<close>
   4.268  
   4.269 -text %mlref {*
   4.270 +text %mlref \<open>
   4.271    \begin{mldecls}
   4.272    @{index_ML Code.read_const: "theory -> string -> string"} \\
   4.273    @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
   4.274 @@ -322,12 +322,12 @@
   4.275       if @{text const} is no constructor.
   4.276  
   4.277    \end{description}
   4.278 -*}
   4.279 +\<close>
   4.280  
   4.281  
   4.282 -subsubsection {* Data depending on the theory's executable content *}
   4.283 +subsubsection \<open>Data depending on the theory's executable content\<close>
   4.284  
   4.285 -text {*
   4.286 +text \<open>
   4.287    Implementing code generator applications on top of the framework set
   4.288    out so far usually not only involves using those primitive
   4.289    interfaces but also storing code-dependent data and various other
   4.290 @@ -373,7 +373,7 @@
   4.291    \item @{text change_yield} update with side result.
   4.292  
   4.293    \end{description}
   4.294 -*}
   4.295 +\<close>
   4.296  
   4.297  end
   4.298  
     5.1 --- a/src/Doc/Codegen/Inductive_Predicate.thy	Thu Jan 15 13:39:41 2015 +0100
     5.2 +++ b/src/Doc/Codegen/Inductive_Predicate.thy	Thu Jan 15 13:39:41 2015 +0100
     5.3 @@ -16,9 +16,9 @@
     5.4    lexordp_def [unfolded lexord_def mem_Collect_eq split]
     5.5  (*>*)
     5.6  
     5.7 -section {* Inductive Predicates \label{sec:inductive} *}
     5.8 +section \<open>Inductive Predicates \label{sec:inductive}\<close>
     5.9  
    5.10 -text {*
    5.11 +text \<open>
    5.12    The @{text "predicate compiler"} is an extension of the code generator
    5.13    which turns inductive specifications into equational ones, from
    5.14    which in turn executable code can be generated.  The mechanisms of
    5.15 @@ -27,20 +27,20 @@
    5.16  
    5.17    Consider the simple predicate @{const append} given by these two
    5.18    introduction rules:
    5.19 -*}
    5.20 +\<close>
    5.21  
    5.22 -text %quote {*
    5.23 +text %quote \<open>
    5.24    @{thm append.intros(1)[of ys]} \\
    5.25    @{thm append.intros(2)[of xs ys zs x]}
    5.26 -*}
    5.27 +\<close>
    5.28  
    5.29 -text {*
    5.30 +text \<open>
    5.31    \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
    5.32 -*}
    5.33 +\<close>
    5.34  
    5.35  code_pred %quote append .
    5.36  
    5.37 -text {*
    5.38 +text \<open>
    5.39    \noindent The @{command "code_pred"} command takes the name of the
    5.40    inductive predicate and then you put a period to discharge a trivial
    5.41    correctness proof.  The compiler infers possible modes for the
    5.42 @@ -56,55 +56,55 @@
    5.43      \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
    5.44    \end{itemize}
    5.45    You can compute sets of predicates using @{command_def "values"}:
    5.46 -*}
    5.47 +\<close>
    5.48  
    5.49  values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
    5.50  
    5.51 -text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
    5.52 +text \<open>\noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and\<close>
    5.53  
    5.54  values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
    5.55  
    5.56 -text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
    5.57 +text \<open>\noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}.\<close>
    5.58  
    5.59 -text {*
    5.60 +text \<open>
    5.61    \noindent If you are only interested in the first elements of the
    5.62    set comprehension (with respect to a depth-first search on the
    5.63    introduction rules), you can pass an argument to @{command "values"}
    5.64    to specify the number of elements you want:
    5.65 -*}
    5.66 +\<close>
    5.67  
    5.68  values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
    5.69  values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
    5.70  
    5.71 -text {*
    5.72 +text \<open>
    5.73    \noindent The @{command "values"} command can only compute set
    5.74    comprehensions for which a mode has been inferred.
    5.75  
    5.76    The code equations for a predicate are made available as theorems with
    5.77    the suffix @{text "equation"}, and can be inspected with:
    5.78 -*}
    5.79 +\<close>
    5.80  
    5.81  thm %quote append.equation
    5.82  
    5.83 -text {*
    5.84 +text \<open>
    5.85    \noindent More advanced options are described in the following subsections.
    5.86 -*}
    5.87 +\<close>
    5.88  
    5.89 -subsection {* Alternative names for functions *}
    5.90 +subsection \<open>Alternative names for functions\<close>
    5.91  
    5.92 -text {* 
    5.93 +text \<open>
    5.94    By default, the functions generated from a predicate are named after
    5.95    the predicate with the mode mangled into the name (e.g., @{text
    5.96    "append_i_i_o"}).  You can specify your own names as follows:
    5.97 -*}
    5.98 +\<close>
    5.99  
   5.100  code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
   5.101    o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
   5.102    i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
   5.103  
   5.104 -subsection {* Alternative introduction rules *}
   5.105 +subsection \<open>Alternative introduction rules\<close>
   5.106  
   5.107 -text {*
   5.108 +text \<open>
   5.109    Sometimes the introduction rules of an predicate are not executable
   5.110    because they contain non-executable constants or specific modes
   5.111    could not be inferred.  It is also possible that the introduction
   5.112 @@ -113,34 +113,34 @@
   5.113    introduction rules for predicates with the attribute @{attribute
   5.114    "code_pred_intro"}.  For example, the transitive closure is defined
   5.115    by:
   5.116 -*}
   5.117 +\<close>
   5.118  
   5.119 -text %quote {*
   5.120 +text %quote \<open>
   5.121    @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
   5.122    @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
   5.123 -*}
   5.124 +\<close>
   5.125  
   5.126 -text {*
   5.127 +text \<open>
   5.128    \noindent These rules do not suit well for executing the transitive
   5.129    closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
   5.130    the second rule will cause an infinite loop in the recursive call.
   5.131    This can be avoided using the following alternative rules which are
   5.132    declared to the predicate compiler by the attribute @{attribute
   5.133    "code_pred_intro"}:
   5.134 -*}
   5.135 +\<close>
   5.136  
   5.137  lemma %quote [code_pred_intro]:
   5.138    "r a b \<Longrightarrow> tranclp r a b"
   5.139    "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   5.140  by auto
   5.141  
   5.142 -text {*
   5.143 +text \<open>
   5.144    \noindent After declaring all alternative rules for the transitive
   5.145    closure, you invoke @{command "code_pred"} as usual.  As you have
   5.146    declared alternative rules for the predicate, you are urged to prove
   5.147    that these introduction rules are complete, i.e., that you can
   5.148    derive an elimination rule for the alternative rules:
   5.149 -*}
   5.150 +\<close>
   5.151  
   5.152  code_pred %quote tranclp
   5.153  proof -
   5.154 @@ -148,20 +148,20 @@
   5.155    from this converse_tranclpE [OF tranclp.prems] show thesis by metis
   5.156  qed
   5.157  
   5.158 -text {*
   5.159 +text \<open>
   5.160    \noindent Alternative rules can also be used for constants that have
   5.161    not been defined inductively. For example, the lexicographic order
   5.162    which is defined as:
   5.163 -*}
   5.164 +\<close>
   5.165  
   5.166 -text %quote {*
   5.167 +text %quote \<open>
   5.168    @{thm [display] lexordp_def [of r]}
   5.169 -*}
   5.170 +\<close>
   5.171  
   5.172 -text {*
   5.173 +text \<open>
   5.174    \noindent To make it executable, you can derive the following two
   5.175    rules and prove the elimination rule:
   5.176 -*}
   5.177 +\<close>
   5.178  
   5.179  lemma %quote [code_pred_intro]:
   5.180    "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
   5.181 @@ -197,16 +197,16 @@
   5.182  qed(*>*)
   5.183  
   5.184  
   5.185 -subsection {* Options for values *}
   5.186 +subsection \<open>Options for values\<close>
   5.187  
   5.188 -text {*
   5.189 +text \<open>
   5.190    In the presence of higher-order predicates, multiple modes for some
   5.191    predicate could be inferred that are not disambiguated by the
   5.192    pattern of the set comprehension.  To disambiguate the modes for the
   5.193    arguments of a predicate, you can state the modes explicitly in the
   5.194    @{command "values"} command.  Consider the simple predicate @{term
   5.195    "succ"}:
   5.196 -*}
   5.197 +\<close>
   5.198  
   5.199  inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   5.200    "succ 0 (Suc 0)"
   5.201 @@ -214,7 +214,7 @@
   5.202  
   5.203  code_pred %quote succ .
   5.204  
   5.205 -text {*
   5.206 +text \<open>
   5.207    \noindent For this, the predicate compiler can infer modes @{text "o
   5.208    \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
   5.209    @{text "i \<Rightarrow> i \<Rightarrow> bool"}.  The invocation of @{command "values"}
   5.210 @@ -223,15 +223,15 @@
   5.211    "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
   5.212    you can declare the mode for the argument between the @{command
   5.213    "values"} and the number of elements.
   5.214 -*}
   5.215 +\<close>
   5.216  
   5.217  values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
   5.218  values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
   5.219  
   5.220  
   5.221 -subsection {* Embedding into functional code within Isabelle/HOL *}
   5.222 +subsection \<open>Embedding into functional code within Isabelle/HOL\<close>
   5.223  
   5.224 -text {*
   5.225 +text \<open>
   5.226    To embed the computation of an inductive predicate into functions
   5.227    that are defined in Isabelle/HOL, you have a number of options:
   5.228  
   5.229 @@ -258,18 +258,18 @@
   5.230        raises a run-time error @{term "not_unique"}.
   5.231  
   5.232    \end{itemize}
   5.233 -*}
   5.234 +\<close>
   5.235  
   5.236  
   5.237 -subsection {* Further Examples *}
   5.238 +subsection \<open>Further Examples\<close>
   5.239  
   5.240 -text {*
   5.241 +text \<open>
   5.242    Further examples for compiling inductive predicates can be found in
   5.243    @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}.  There are
   5.244    also some examples in the Archive of Formal Proofs, notably in the
   5.245    @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   5.246    sessions.
   5.247 -*}
   5.248 +\<close>
   5.249  
   5.250  end
   5.251  
     6.1 --- a/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
     6.2 +++ b/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
     6.3 @@ -2,9 +2,9 @@
     6.4  imports Setup
     6.5  begin
     6.6  
     6.7 -section {* Introduction *}
     6.8 +section \<open>Introduction\<close>
     6.9  
    6.10 -text {*
    6.11 +text \<open>
    6.12    This tutorial introduces the code generator facilities of @{text
    6.13    "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
    6.14    specifications into corresponding executable code in the programming
    6.15 @@ -14,12 +14,12 @@
    6.16  
    6.17    To profit from this tutorial, some familiarity and experience with
    6.18    @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
    6.19 -*}
    6.20 +\<close>
    6.21  
    6.22  
    6.23 -subsection {* Code generation principle: shallow embedding \label{sec:principle} *}
    6.24 +subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close>
    6.25  
    6.26 -text {*
    6.27 +text \<open>
    6.28    The key concept for understanding Isabelle's code generation is
    6.29    \emph{shallow embedding}: logical entities like constants, types and
    6.30    classes are identified with corresponding entities in the target
    6.31 @@ -29,12 +29,12 @@
    6.32    system, then every rewrite step performed by the program can be
    6.33    simulated in the logic, which guarantees partial correctness
    6.34    @{cite "Haftmann-Nipkow:2010:code"}.
    6.35 -*}
    6.36 +\<close>
    6.37  
    6.38  
    6.39 -subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
    6.40 +subsection \<open>A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}\<close>
    6.41  
    6.42 -text {*
    6.43 +text \<open>
    6.44    In a HOL theory, the @{command_def datatype} and @{command_def
    6.45    definition}/@{command_def primrec}/@{command_def fun} declarations
    6.46    form the core of a functional programming language.  By default
    6.47 @@ -43,7 +43,7 @@
    6.48    ado.
    6.49  
    6.50    For example, here a simple \qt{implementation} of amortised queues:
    6.51 -*}
    6.52 +\<close>
    6.53  
    6.54  datatype %quote 'a queue = AQueue "'a list" "'a list"
    6.55  
    6.56 @@ -63,18 +63,18 @@
    6.57    "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
    6.58    by (cases xs) (simp_all split: list.splits) (*>*)
    6.59  
    6.60 -text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
    6.61 +text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
    6.62  
    6.63  export_code %quote empty dequeue enqueue in SML
    6.64    module_name Example file "$ISABELLE_TMP/examples/example.ML"
    6.65  
    6.66 -text {* \noindent resulting in the following code: *}
    6.67 +text \<open>\noindent resulting in the following code:\<close>
    6.68  
    6.69 -text %quotetypewriter {*
    6.70 +text %quotetypewriter \<open>
    6.71    @{code_stmts empty enqueue dequeue (SML)}
    6.72 -*}
    6.73 +\<close>
    6.74  
    6.75 -text {*
    6.76 +text \<open>
    6.77    \noindent The @{command_def export_code} command takes a
    6.78    space-separated list of constants for which code shall be generated;
    6.79    anything else needed for those is added implicitly.  Then follows a
    6.80 @@ -84,31 +84,31 @@
    6.81    @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
    6.82    for @{text Haskell} it denotes a \emph{directory} where a file named as the
    6.83    module name (with extension @{text ".hs"}) is written:
    6.84 -*}
    6.85 +\<close>
    6.86  
    6.87  export_code %quote empty dequeue enqueue in Haskell
    6.88    module_name Example file "$ISABELLE_TMP/examples/"
    6.89  
    6.90 -text {*
    6.91 +text \<open>
    6.92    \noindent This is the corresponding code:
    6.93 -*}
    6.94 +\<close>
    6.95  
    6.96 -text %quotetypewriter {*
    6.97 +text %quotetypewriter \<open>
    6.98    @{code_stmts empty enqueue dequeue (Haskell)}
    6.99 -*}
   6.100 +\<close>
   6.101  
   6.102 -text {*
   6.103 +text \<open>
   6.104    \noindent For more details about @{command export_code} see
   6.105    \secref{sec:further}.
   6.106 -*}
   6.107 +\<close>
   6.108  
   6.109  
   6.110 -subsection {* Type classes *}
   6.111 +subsection \<open>Type classes\<close>
   6.112  
   6.113 -text {*
   6.114 +text \<open>
   6.115    Code can also be generated from type classes in a Haskell-like
   6.116    manner.  For illustration here an example from abstract algebra:
   6.117 -*}
   6.118 +\<close>
   6.119  
   6.120  class %quote semigroup =
   6.121    fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
   6.122 @@ -146,51 +146,51 @@
   6.123  
   6.124  end %quote
   6.125  
   6.126 -text {*
   6.127 +text \<open>
   6.128    \noindent We define the natural operation of the natural numbers
   6.129    on monoids:
   6.130 -*}
   6.131 +\<close>
   6.132  
   6.133  primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   6.134      "pow 0 a = \<one>"
   6.135    | "pow (Suc n) a = a \<otimes> pow n a"
   6.136  
   6.137 -text {*
   6.138 +text \<open>
   6.139    \noindent This we use to define the discrete exponentiation
   6.140    function:
   6.141 -*}
   6.142 +\<close>
   6.143  
   6.144  definition %quote bexp :: "nat \<Rightarrow> nat" where
   6.145    "bexp n = pow n (Suc (Suc 0))"
   6.146  
   6.147 -text {*
   6.148 +text \<open>
   6.149    \noindent The corresponding code in Haskell uses that language's
   6.150    native classes:
   6.151 -*}
   6.152 +\<close>
   6.153  
   6.154 -text %quotetypewriter {*
   6.155 +text %quotetypewriter \<open>
   6.156    @{code_stmts bexp (Haskell)}
   6.157 -*}
   6.158 +\<close>
   6.159  
   6.160 -text {*
   6.161 +text \<open>
   6.162    \noindent This is a convenient place to show how explicit dictionary
   6.163    construction manifests in generated code -- the same example in
   6.164    @{text SML}:
   6.165 -*}
   6.166 +\<close>
   6.167  
   6.168 -text %quotetypewriter {*
   6.169 +text %quotetypewriter \<open>
   6.170    @{code_stmts bexp (SML)}
   6.171 -*}
   6.172 +\<close>
   6.173  
   6.174 -text {*
   6.175 +text \<open>
   6.176    \noindent Note the parameters with trailing underscore (@{verbatim
   6.177    "A_"}), which are the dictionary parameters.
   6.178 -*}
   6.179 +\<close>
   6.180  
   6.181  
   6.182 -subsection {* How to continue from here *}
   6.183 +subsection \<open>How to continue from here\<close>
   6.184  
   6.185 -text {*
   6.186 +text \<open>
   6.187    What you have seen so far should be already enough in a lot of
   6.188    cases.  If you are content with this, you can quit reading here.
   6.189  
   6.190 @@ -236,7 +236,7 @@
   6.191      \begin{center}\textit{Happy proving, happy hacking!}\end{center}
   6.192  
   6.193    \end{minipage}}}\end{center}
   6.194 -*}
   6.195 +\<close>
   6.196  
   6.197  end
   6.198  
     7.1 --- a/src/Doc/Codegen/Refinement.thy	Thu Jan 15 13:39:41 2015 +0100
     7.2 +++ b/src/Doc/Codegen/Refinement.thy	Thu Jan 15 13:39:41 2015 +0100
     7.3 @@ -2,81 +2,81 @@
     7.4  imports Setup
     7.5  begin
     7.6  
     7.7 -section {* Program and datatype refinement \label{sec:refinement} *}
     7.8 +section \<open>Program and datatype refinement \label{sec:refinement}\<close>
     7.9  
    7.10 -text {*
    7.11 +text \<open>
    7.12    Code generation by shallow embedding (cf.~\secref{sec:principle})
    7.13    allows to choose code equations and datatype constructors freely,
    7.14    given that some very basic syntactic properties are met; this
    7.15    flexibility opens up mechanisms for refinement which allow to extend
    7.16    the scope and quality of generated code dramatically.
    7.17 -*}
    7.18 +\<close>
    7.19  
    7.20  
    7.21 -subsection {* Program refinement *}
    7.22 +subsection \<open>Program refinement\<close>
    7.23  
    7.24 -text {*
    7.25 +text \<open>
    7.26    Program refinement works by choosing appropriate code equations
    7.27    explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
    7.28    numbers:
    7.29 -*}
    7.30 +\<close>
    7.31  
    7.32  fun %quote fib :: "nat \<Rightarrow> nat" where
    7.33      "fib 0 = 0"
    7.34    | "fib (Suc 0) = Suc 0"
    7.35    | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    7.36  
    7.37 -text {*
    7.38 +text \<open>
    7.39    \noindent The runtime of the corresponding code grows exponential due
    7.40    to two recursive calls:
    7.41 -*}
    7.42 +\<close>
    7.43  
    7.44 -text %quotetypewriter {*
    7.45 +text %quotetypewriter \<open>
    7.46    @{code_stmts fib (consts) fib (Haskell)}
    7.47 -*}
    7.48 +\<close>
    7.49  
    7.50 -text {*
    7.51 +text \<open>
    7.52    \noindent A more efficient implementation would use dynamic
    7.53    programming, e.g.~sharing of common intermediate results between
    7.54    recursive calls.  This idea is expressed by an auxiliary operation
    7.55    which computes a Fibonacci number and its successor simultaneously:
    7.56 -*}
    7.57 +\<close>
    7.58  
    7.59  definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
    7.60    "fib_step n = (fib (Suc n), fib n)"
    7.61  
    7.62 -text {*
    7.63 +text \<open>
    7.64    \noindent This operation can be implemented by recursion using
    7.65    dynamic programming:
    7.66 -*}
    7.67 +\<close>
    7.68  
    7.69  lemma %quote [code]:
    7.70    "fib_step 0 = (Suc 0, 0)"
    7.71    "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
    7.72    by (simp_all add: fib_step_def)
    7.73  
    7.74 -text {*
    7.75 +text \<open>
    7.76    \noindent What remains is to implement @{const fib} by @{const
    7.77    fib_step} as follows:
    7.78 -*}
    7.79 +\<close>
    7.80  
    7.81  lemma %quote [code]:
    7.82    "fib 0 = 0"
    7.83    "fib (Suc n) = fst (fib_step n)"
    7.84    by (simp_all add: fib_step_def)
    7.85  
    7.86 -text {*
    7.87 +text \<open>
    7.88    \noindent The resulting code shows only linear growth of runtime:
    7.89 -*}
    7.90 +\<close>
    7.91  
    7.92 -text %quotetypewriter {*
    7.93 +text %quotetypewriter \<open>
    7.94    @{code_stmts fib (consts) fib fib_step (Haskell)}
    7.95 -*}
    7.96 +\<close>
    7.97  
    7.98  
    7.99 -subsection {* Datatype refinement *}
   7.100 +subsection \<open>Datatype refinement\<close>
   7.101  
   7.102 -text {*
   7.103 +text \<open>
   7.104    Selecting specific code equations \emph{and} datatype constructors
   7.105    leads to datatype refinement.  As an example, we will develop an
   7.106    alternative representation of the queue example given in
   7.107 @@ -85,7 +85,7 @@
   7.108    details, which may be cumbersome when proving theorems about it.
   7.109    Therefore, here is a simple, straightforward representation of
   7.110    queues:
   7.111 -*}
   7.112 +\<close>
   7.113  
   7.114  datatype %quote 'a queue = Queue "'a list"
   7.115  
   7.116 @@ -99,17 +99,17 @@
   7.117      "dequeue (Queue []) = (None, Queue [])"
   7.118    | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
   7.119  
   7.120 -text {*
   7.121 +text \<open>
   7.122    \noindent This we can use directly for proving;  for executing,
   7.123    we provide an alternative characterisation:
   7.124 -*}
   7.125 +\<close>
   7.126  
   7.127  definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
   7.128    "AQueue xs ys = Queue (ys @ rev xs)"
   7.129  
   7.130  code_datatype %quote AQueue
   7.131  
   7.132 -text {*
   7.133 +text \<open>
   7.134    \noindent Here we define a \qt{constructor} @{const "AQueue"} which
   7.135    is defined in terms of @{text "Queue"} and interprets its arguments
   7.136    according to what the \emph{content} of an amortised queue is supposed
   7.137 @@ -127,7 +127,7 @@
   7.138    Equipped with this, we are able to prove the following equations
   7.139    for our primitive queue operations which \qt{implement} the simple
   7.140    queues in an amortised fashion:
   7.141 -*}
   7.142 +\<close>
   7.143  
   7.144  lemma %quote empty_AQueue [code]:
   7.145    "empty = AQueue [] []"
   7.146 @@ -144,12 +144,12 @@
   7.147    "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
   7.148    by (simp_all add: AQueue_def)
   7.149  
   7.150 -text {*
   7.151 +text \<open>
   7.152    \noindent It is good style, although no absolute requirement, to
   7.153    provide code equations for the original artefacts of the implemented
   7.154    type, if possible; in our case, these are the datatype constructor
   7.155    @{const Queue} and the case combinator @{const case_queue}:
   7.156 -*}
   7.157 +\<close>
   7.158  
   7.159  lemma %quote Queue_AQueue [code]:
   7.160    "Queue = AQueue []"
   7.161 @@ -159,15 +159,15 @@
   7.162    "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
   7.163    by (simp add: AQueue_def)
   7.164  
   7.165 -text {*
   7.166 +text \<open>
   7.167    \noindent The resulting code looks as expected:
   7.168 -*}
   7.169 +\<close>
   7.170  
   7.171 -text %quotetypewriter {*
   7.172 +text %quotetypewriter \<open>
   7.173    @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
   7.174 -*}
   7.175 +\<close>
   7.176  
   7.177 -text {*
   7.178 +text \<open>
   7.179    The same techniques can also be applied to types which are not
   7.180    specified as datatypes, e.g.~type @{typ int} is originally specified
   7.181    as quotient type by means of @{command_def typedef}, but for code
   7.182 @@ -176,12 +176,12 @@
   7.183  
   7.184    This approach however fails if the representation of a type demands
   7.185    invariants; this issue is discussed in the next section.
   7.186 -*}
   7.187 +\<close>
   7.188  
   7.189  
   7.190 -subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
   7.191 +subsection \<open>Datatype refinement involving invariants \label{sec:invariant}\<close>
   7.192  
   7.193 -text {*
   7.194 +text \<open>
   7.195    Datatype representation involving invariants require a dedicated
   7.196    setup for the type and its primitive operations.  As a running
   7.197    example, we implement a type @{text "'a dlist"} of list consisting
   7.198 @@ -191,31 +191,31 @@
   7.199    type (in our example @{text "'a dlist"}) should be implemented.
   7.200    Here we choose @{text "'a list"}.  Then a conversion from the concrete
   7.201    type to the abstract type must be specified, here:
   7.202 -*}
   7.203 +\<close>
   7.204  
   7.205 -text %quote {*
   7.206 +text %quote \<open>
   7.207    @{term_type Dlist}
   7.208 -*}
   7.209 +\<close>
   7.210  
   7.211 -text {*
   7.212 +text \<open>
   7.213    \noindent Next follows the specification of a suitable \emph{projection},
   7.214    i.e.~a conversion from abstract to concrete type:
   7.215 -*}
   7.216 +\<close>
   7.217  
   7.218 -text %quote {*
   7.219 +text %quote \<open>
   7.220    @{term_type list_of_dlist}
   7.221 -*}
   7.222 +\<close>
   7.223  
   7.224 -text {*
   7.225 +text \<open>
   7.226    \noindent This projection must be specified such that the following
   7.227    \emph{abstract datatype certificate} can be proven:
   7.228 -*}
   7.229 +\<close>
   7.230  
   7.231  lemma %quote [code abstype]:
   7.232    "Dlist (list_of_dlist dxs) = dxs"
   7.233    by (fact Dlist_list_of_dlist)
   7.234  
   7.235 -text {*
   7.236 +text \<open>
   7.237    \noindent Note that so far the invariant on representations
   7.238    (@{term_type distinct}) has never been mentioned explicitly:
   7.239    the invariant is only referred to implicitly: all values in
   7.240 @@ -226,26 +226,26 @@
   7.241    indirectly using the projection @{const list_of_dlist}.  For
   7.242    the empty @{text "dlist"}, @{const Dlist.empty}, we finally want
   7.243    the code equation
   7.244 -*}
   7.245 +\<close>
   7.246  
   7.247 -text %quote {*
   7.248 +text %quote \<open>
   7.249    @{term "Dlist.empty = Dlist []"}
   7.250 -*}
   7.251 +\<close>
   7.252  
   7.253 -text {*
   7.254 +text \<open>
   7.255    \noindent This we have to prove indirectly as follows:
   7.256 -*}
   7.257 +\<close>
   7.258  
   7.259  lemma %quote [code]:
   7.260    "list_of_dlist Dlist.empty = []"
   7.261    by (fact list_of_dlist_empty)
   7.262  
   7.263 -text {*
   7.264 +text \<open>
   7.265    \noindent This equation logically encodes both the desired code
   7.266    equation and that the expression @{const Dlist} is applied to obeys
   7.267    the implicit invariant.  Equations for insertion and removal are
   7.268    similar:
   7.269 -*}
   7.270 +\<close>
   7.271  
   7.272  lemma %quote [code]:
   7.273    "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
   7.274 @@ -255,15 +255,15 @@
   7.275    "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
   7.276    by (fact list_of_dlist_remove)
   7.277  
   7.278 -text {*
   7.279 +text \<open>
   7.280    \noindent Then the corresponding code is as follows:
   7.281 -*}
   7.282 +\<close>
   7.283  
   7.284 -text %quotetypewriter {*
   7.285 +text %quotetypewriter \<open>
   7.286    @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
   7.287 -*}
   7.288 +\<close>
   7.289  
   7.290 -text {*
   7.291 +text \<open>
   7.292    See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
   7.293    for the meta theory of datatype refinement involving invariants.
   7.294  
   7.295 @@ -271,6 +271,6 @@
   7.296    invariants are available in the library, theory @{theory Mapping}
   7.297    specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
   7.298    these can be implemented by red-black-trees (theory @{theory RBT}).
   7.299 -*}
   7.300 +\<close>
   7.301  
   7.302  end
     8.1 --- a/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
     8.2 +++ b/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4  ML_file "../antiquote_setup.ML"
     8.5  ML_file "../more_antiquote.ML"
     8.6  
     8.7 -setup {*
     8.8 +setup \<open>
     8.9  let
    8.10    val typ = Simple_Syntax.read_typ;
    8.11  in
    8.12 @@ -25,7 +25,7 @@
    8.13     [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    8.14      ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    8.15  end
    8.16 -*}
    8.17 +\<close>
    8.18  
    8.19  declare [[default_code_width = 74]]
    8.20