(continued)
authorhaftmann
Mon Nov 06 16:28:29 2006 +0100 (2006-11-06)
changeset 211895435ccdb4ea1
parent 21188 2aa15b663cd4
child 21190 08ec81dfc7fb
(continued)
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 06 12:04:44 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 06 16:28:29 2006 +0100
     1.3 @@ -47,6 +47,10 @@
     1.4    of code generation into a small set of orthogonal principles
     1.5    while achieving a big coverage of application areas
     1.6    with maximum flexibility.
     1.7 +
     1.8 +  For readers, some familiarity and experience
     1.9 +  with the the ingredients
    1.10 +  of the HOL \emph{Main} theory is assumed.
    1.11  *}
    1.12  
    1.13  
    1.14 @@ -80,6 +84,13 @@
    1.15  subsection {* Code generation process *}
    1.16  
    1.17  text {*
    1.18 +  \begin{figure}[h]
    1.19 +  \centering
    1.20 +  \includegraphics[width=0.7\textwidth]{codegen_process}
    1.21 +  \caption{code generator -- processing overview}
    1.22 +  \label{fig:process}
    1.23 +  \end{figure}
    1.24 +
    1.25    The code generator employs a notion of executability
    1.26    for three foundational executable ingredients known
    1.27    from functional programming:
    1.28 @@ -114,13 +125,6 @@
    1.29  
    1.30    \end{itemize}
    1.31  
    1.32 -  \begin{figure}[h]
    1.33 -  \centering
    1.34 -  \includegraphics[width=0.3\textwidth]{codegen_process}
    1.35 -  \caption{code generator -- processing overview}
    1.36 -  \label{fig:process}
    1.37 -  \end{figure}
    1.38 -
    1.39    From these steps, only the two last are carried out
    1.40    outside the logic; by keeping this layer as
    1.41    thin as possible, the amount of code to trust is
    1.42 @@ -440,12 +444,12 @@
    1.43  
    1.44      \item[ExecutableSet] allows to generate code
    1.45         for finite sets using lists.
    1.46 -    \item[ExecutableRat] implements rational
    1.47 +    \item[ExecutableRat] \label{exec_rat} implements rational
    1.48         numbers as triples @{text "(sign, enumerator, denominator)"}.
    1.49 -    \item[EfficientNat] implements natural numbers by integers,
    1.50 +    \item[EfficientNat] \label{eff_nat} implements natural numbers by integers,
    1.51         which in general will result in higher efficency; pattern
    1.52         matching with @{const "0\<Colon>nat"} / @{const "Suc"}
    1.53 -       is eliminated. \label{eff_nat}
    1.54 +       is eliminated.
    1.55      \item[MLString] provides an additional datatype @{text "mlstring"};
    1.56         in the HOL default setup, strings in HOL are mapped to list
    1.57         of chars in SML; values of type @{text "mlstring"} are
    1.58 @@ -837,7 +841,7 @@
    1.59    Another subtlety
    1.60    enters the stage when definitions of overloaded constants
    1.61    are dependent on operational equality.  For example, let
    1.62 -  us define a lexicographic ordering on tuples: \\
    1.63 +  us define a lexicographic ordering on tuples:
    1.64  *}
    1.65  
    1.66  (*<*)
    1.67 @@ -940,7 +944,7 @@
    1.68  
    1.69  text {*
    1.70    Imagine the following quick-and-dirty setup for implementing
    1.71 -  some sets as lists:
    1.72 +  some kind of sets as lists in SML:
    1.73  *}
    1.74  
    1.75  code_type set
    1.76 @@ -950,42 +954,219 @@
    1.77    (SML "![]" and infixl 7 "::")
    1.78  
    1.79  definition
    1.80 -  dummy_set :: "nat set"
    1.81 -  "dummy_set = {1, 2, 3}"
    1.82 +  dummy_set :: "(nat \<Rightarrow> nat) set"
    1.83 +  "dummy_set = {Suc}"
    1.84 +
    1.85 +text {*
    1.86 +  Then code generation for @{const dummy_set} will fail.
    1.87 +  Why? A glimpse at the function equations will offer:
    1.88 +*}
    1.89 +
    1.90 +print_codethms (insert)
    1.91 +
    1.92 +text {*
    1.93 +  This reveals the function equation @{thm insert_def}
    1.94 +  for @{const insert}, which is operationally meaningsless
    1.95 +  but forces an equality constraint on the set members
    1.96 +  (which is not fullfiable if the set members are functions).
    1.97 +  Even when using set of natural numbers (which are an instance
    1.98 +  of \emph{eq}), we run into a problem:
    1.99 +*}
   1.100 +
   1.101 +definition
   1.102 +  foobar_set :: "nat set"
   1.103 +  "foobar_set = {0, 1, 2}"
   1.104 +
   1.105 +text {*
   1.106 +  In this case the serializer would complain that @{const insert}
   1.107 +  expects dictionaries (namely an \emph{eq} dictionary) but
   1.108 +  has also been given a customary serialization.
   1.109 +
   1.110 +  The solution to this dilemma:
   1.111 +*}
   1.112 +
   1.113 +lemma [code func]:
   1.114 +  "insert = insert" ..
   1.115 +
   1.116 +code_gen dummy_set foobar_set (SML "examples/dirty_set.ML")
   1.117 +
   1.118 +text {*
   1.119 +  \lstsml{Thy/examples/dirty_set.ML}
   1.120  
   1.121 -(*print_codethms (dummy_set)
   1.122 -code_gen dummy_set (SML -)*)
   1.123 +  Reflexive function equations by convention are dropped.
   1.124 +  But their presence prevents primitive definitions to be
   1.125 +  used as function equations:
   1.126 +*}
   1.127 +
   1.128 +print_codethms (insert)
   1.129 +
   1.130 +text {*
   1.131 +  will show \emph{no} function equations for insert.
   1.132  
   1.133 +  Note that the sort constraints of reflexive equations
   1.134 +  are considered; so
   1.135 +*}
   1.136 +
   1.137 +lemma [code func]:
   1.138 +  "(insert \<Colon> 'a\<Colon>eq \<Rightarrow> 'a set \<Rightarrow> 'a set) = insert" ..
   1.139 +
   1.140 +text {*
   1.141 +  would mean nothing else than to introduce the evil
   1.142 +  sort constraint by hand.
   1.143 +*}
   1.144 +
   1.145 +subsection {* Cyclic module dependencies *}
   1.146  
   1.147 -(* shadowing by user-defined serializations, understanding the type game,
   1.148 -reflexive equations, dangerous equations *)
   1.149 +text {*
   1.150 +  Sometimes the awkward situation occurs that dependencies
   1.151 +  between definitions introduce cyclic dependencies
   1.152 +  between modules, which in the Haskell world leaves
   1.153 +  you to the mercy of the Haskell implementation you are using,
   1.154 +  while for SML code generation is not possible.
   1.155  
   1.156 +  A solution is to declare module names explicitly.
   1.157 +  Let use assume the three cyclically dependent
   1.158 +  modules are named \emph{A}, \emph{B} and \emph{C}.
   1.159 +  Then, by stating
   1.160 +*}
   1.161 +
   1.162 +code_modulename SML
   1.163 +  A ABC
   1.164 +  B ABC
   1.165 +  C ABC
   1.166 +
   1.167 +text {*
   1.168 +  we explicitly map all those modules on \emph{ABC},
   1.169 +  resulting in an ad-hoc merge of this three modules
   1.170 +  at serialization time.
   1.171 +*}
   1.172  
   1.173  subsection {* Axiomatic extensions *}
   1.174  
   1.175  text {*
   1.176    \begin{warn}
   1.177      The extensions introduced in this section, though working
   1.178 -    in practice, are not the cream of the crop.  They will
   1.179 +    in practice, are not the cream of the crop, as you
   1.180 +    will notice during reading.  They will
   1.181      eventually be replaced by more mature approaches.
   1.182    \end{warn}
   1.183 +
   1.184 +  Sometimes equalities are taken for granted which are
   1.185 +  not derivable inside the HOL logic but are silently assumed
   1.186 +  to hold for executable code.  For example, we may want
   1.187 +  to identify the famous HOL constant @{const arbitrary}
   1.188 +  of type @{typ "'a option"} with @{const None}.
   1.189 +  By brute force:
   1.190 +*}
   1.191 +
   1.192 +axioms
   1.193 +  arbitrary_option: "arbitrary = None"
   1.194 +
   1.195 +text {*
   1.196 +  However this has to be considered harmful since this axiom,
   1.197 +  though probably justifiable for generated code, could
   1.198 +  introduce serious inconsistencies into the logic.
   1.199 +
   1.200 +  So, there is a distinguished construct for stating axiomatic
   1.201 +  equalities of constants which apply only for code generation.
   1.202 +  Before introducing this, here is a convenient place to describe
   1.203 +  shortly how to deal with some restrictions the type discipline
   1.204 +  imposes.
   1.205 +
   1.206 +  By itself, the constant @{const arbitrary} is a non-overloaded
   1.207 +  polymorphic constant.  So, there is no way to distinguish
   1.208 +  different versions of @{const arbitrary} for different types
   1.209 +  inside the code generator framework.  However, inlining
   1.210 +  theorems together with auxiliary constants provide a solution:
   1.211  *}
   1.212  
   1.213 -(* code_modulename *)
   1.214 -(* existing libraries, code inline code_constsubst, code_abstype*)
   1.215 +definition
   1.216 +  arbitrary_option :: "'a option"
   1.217 +  [symmetric, code inline]: "arbitrary_option = arbitrary"
   1.218 +
   1.219 +text {*
   1.220 +  By that, we replace any @{const arbitrary} with option type
   1.221 +  by @{const arbitrary_option} in function equations.
   1.222 +
   1.223 +  For technical reasons, we further have to provide a
   1.224 +  synonym for @{const None} which in code generator view
   1.225 +  is a function rather than a datatype constructor
   1.226 +*}
   1.227 +
   1.228 +definition
   1.229 +  "None' = None"
   1.230 +
   1.231 +text {*
   1.232 +  Then finally we are enabled to use \isasymCODEAXIOMS:
   1.233 +*}
   1.234 +
   1.235 +code_axioms
   1.236 +  arbitrary_option \<equiv> None'
   1.237 +
   1.238 +text {*
   1.239 +  A dummy example:
   1.240 +*}
   1.241 +
   1.242 +fun
   1.243 +  dummy_option :: "'a list \<Rightarrow> 'a option" where
   1.244 +  "dummy_option (x#xs) = Some x"
   1.245 +  "dummy_option [] = arbitrary"
   1.246 +termination by (auto_term "{}")
   1.247 +(*<*)
   1.248 +declare dummy_option.simps [code func]
   1.249 +(*>*)
   1.250 +
   1.251 +code_gen dummy_option (SML "examples/arbitrary.ML")
   1.252 +
   1.253 +text {*
   1.254 +  \lstsml{Thy/examples/arbitrary.ML}
   1.255 +
   1.256 +  Another axiomatic extension is code generation
   1.257 +  for abstracted types.  For this, the  
   1.258 +  \emph{ExecutableRat} (see \secref{exec_rat})
   1.259 +  forms a good example.
   1.260 +*}
   1.261 +
   1.262  
   1.263  section {* ML interfaces \label{sec:ml} *}
   1.264  
   1.265 +text {*
   1.266 +  Since the code generator framework not only aims to provide
   1.267 +  a nice Isar interface but also to form a base for
   1.268 +  code-generation-based applications, here a short
   1.269 +  description of the most important ML interfaces.
   1.270 +*}
   1.271 +
   1.272  subsection {* Constants with type discipline: codegen\_consts.ML *}
   1.273  
   1.274 +text {*
   1.275 +  This Pure module manages identification of (probably overloaded)
   1.276 +  constants by unique identifiers.
   1.277 +*}
   1.278 +
   1.279  text %mlref {*
   1.280    \begin{mldecls}
   1.281    @{index_ML_type CodegenConsts.const} \\
   1.282 -  @{index_ML CodegenConsts.inst_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
   1.283 +  @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
   1.284    @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\
   1.285 -  @{index_ML CodegenConsts.norm: "theory -> CodegenConsts.const -> CodegenConsts.const"} \\
   1.286 -  @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"}
   1.287 -  \end{mldecls}
   1.288 + \end{mldecls}
   1.289 +
   1.290 +  \begin{description}
   1.291 +
   1.292 +  \item @{ML_type CodegenConsts.const} is the identifier type:
   1.293 +     the product of a \emph{string} with a list of \emph{typs}.
   1.294 +     The \emph{string} is the constant name as represented inside Isabelle;
   1.295 +     the \emph{typs} are a type instantion in the sense of System F,
   1.296 +     with canonical names for type variables.
   1.297 +
   1.298 +  \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"}
   1.299 +     maps a constant expression @{text "(constname, typ)"} to its canonical identifier.
   1.300 +
   1.301 +  \item @{ML CodegenConsts.typ_of_inst}~@{text thy}~@{text const}
   1.302 +     maps a canonical identifier @{text const} to a constant
   1.303 +     expression with appropriate type.
   1.304 +
   1.305 +  \end{description}
   1.306  *}
   1.307  
   1.308  subsection {* Executable theory content: codegen\_data.ML *}
   1.309 @@ -1002,33 +1183,109 @@
   1.310    @{index_ML_type CodegenData.lthms} \\
   1.311    @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
   1.312    \end{mldecls}
   1.313 +
   1.314 +  \begin{description}
   1.315 +
   1.316 +  \item @{ML_type CodegenData.lthms} is an abstract view
   1.317 +     on suspended theorems.  Suspensions are evaluated on demand.
   1.318 +
   1.319 +  \item @{ML CodegenData.lazy}~@{text f} turns an abstract
   1.320 +     theorem computation @{text f} into suspended theorems.
   1.321 +
   1.322 +  \end{description}
   1.323  *}
   1.324  
   1.325  subsubsection {* Executable content *}
   1.326  
   1.327  text %mlref {*
   1.328    \begin{mldecls}
   1.329 +  @{index_ML_type CodegenData.lthms} \\
   1.330    @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
   1.331    @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   1.332    @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
   1.333 -  @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory"} \\
   1.334 -  @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
   1.335    @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   1.336    @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
   1.337 -  @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list) -> theory -> theory"} \\
   1.338 -  @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list) -> theory -> theory"} \\
   1.339 -  @{index_ML CodegenData.these_funcs: "theory -> CodegenConsts.const -> thm list"} \\
   1.340 -  @{index_ML CodegenData.get_datatype: "theory -> string -> ((string * sort) list * (string * typ list) list) option"} \\
   1.341 +  @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list)
   1.342 +    -> theory -> theory"} \\
   1.343 +  @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list)
   1.344 +    -> theory -> theory"} \\
   1.345 +  @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
   1.346 +    * CodegenData.lthms) -> theory -> theory"} \\
   1.347 +  @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
   1.348 +  @{index_ML CodegenData.get_datatype: "theory -> string
   1.349 +    -> ((string * sort) list * (string * typ list) list) option"} \\
   1.350    @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
   1.351    \end{mldecls}
   1.352  
   1.353    \begin{description}
   1.354  
   1.355 -  \item @{ML CodegenData.add_func}~@{text "thm"}
   1.356 +  \item @{ML CodegenData.add_func}~@{text "thm"}~@{text "thy"} adds function
   1.357 +     theorem @{text "thm"} to executable content.
   1.358 +
   1.359 +  \item @{ML CodegenData.del_func}~@{text "thm"}~@{text "thy"} removes function
   1.360 +     theorem @{text "thm"} from executable content, if present.
   1.361 +
   1.362 +  \item @{ML CodegenData.add_funcl}~@{text "(const, lthms)"}~@{text "thy"} adds
   1.363 +     suspended function equations @{text lthms} for constant
   1.364 +     @{text const} to executable content.
   1.365 +
   1.366 +  \item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
   1.367 +     inlineing theorem @{text thm} to executable content.
   1.368 +
   1.369 +  \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
   1.370 +     inlining theorem @{text thm} from executable content, if present.
   1.371 +
   1.372 +  \item @{ML CodegenData.add_inline_proc}~@{text "f"}~@{text "thy"} adds
   1.373 +     inline procedure @{text f} to executable content;
   1.374 +     @{text f} is a computation of rewrite rules dependent on
   1.375 +     the current theory context and the list of all arguments
   1.376 +     and right hand sides of the function equations belonging
   1.377 +     to a certain function definition.
   1.378 +
   1.379 +  \item @{ML CodegenData.add_preproc}~@{text "f"}~@{text "thy"} adds
   1.380 +     generic preprocessor @{text f} to executable content;
   1.381 +     @{text f} is a transformation of the function equations belonging
   1.382 +     to a certain function definition, depending on the
   1.383 +     current theory context.
   1.384 +
   1.385 +  \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
   1.386 +     a datatype to executable content, with type constructor
   1.387 +     @{text name} and specification @{text spec}; @{text spec} is
   1.388 +     a pair consisting of a list of type variable with sort
   1.389 +     contraints and a list of constructors with name
   1.390 +     and types of arguments.  The addition as datatype
   1.391 +     has to be justified giving a certificate of suspended
   1.392 +     theorems as wittnesses for injectiveness and distincness.
   1.393 +
   1.394 +  \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
   1.395 +     remove a datatype from executable content, if present.
   1.396 +
   1.397 +  \item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
   1.398 +     returns type constructor corresponding to
   1.399 +     constructor @{text const}; returns @{text NONE}
   1.400 +     if @{text const} is no constructor.
   1.401  
   1.402    \end{description}
   1.403  *}
   1.404  
   1.405 +subsection {* Function equation systems: codegen\_funcgr.ML *}
   1.406 +
   1.407 +text {*
   1.408 +  
   1.409 +*}
   1.410 +
   1.411 +text %mlref {*
   1.412 +  \begin{mldecls}
   1.413 +  @{index_ML_type CodegenFuncgr.T} \\
   1.414 +  @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
   1.415 +  @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
   1.416 +  @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
   1.417 +  @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
   1.418 +    -> CodegenConsts.const list -> CodegenConsts.const list list"} \\
   1.419 +  @{index_ML CodegenFuncgr.all: "CodegenFuncgr.T -> CodegenConsts.const list"}
   1.420 +  \end{mldecls}
   1.421 +*}
   1.422 +
   1.423  subsection {* Further auxiliary *}
   1.424  
   1.425  text %mlref {*
   1.426 @@ -1038,6 +1295,7 @@
   1.427    @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
   1.428    @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
   1.429    @{index_ML_structure CodegenConsts.Consttab} \\
   1.430 +  @{index_ML_structure CodegenFuncgr.Constgraph} \\
   1.431    @{index_ML CodegenData.typ_func: "theory -> thm -> typ"} \\
   1.432    @{index_ML CodegenData.rewrite_func: "thm list -> thm -> thm"} \\
   1.433    \end{mldecls}
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 12:04:44 2006 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 16:28:29 2006 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  module Codegen where
     2.5 -import qualified IntDef
     2.6 +import qualified Nat
     2.7  
     2.8  class Null a where
     2.9    null :: a
    2.10 @@ -14,5 +14,5 @@
    2.11  instance Codegen.Null (Maybe b) where
    2.12    null = Codegen.null_option
    2.13  
    2.14 -dummy :: Maybe IntDef.Nat
    2.15 -dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]
    2.16 +dummy :: Maybe Nat.Nat
    2.17 +dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML	Mon Nov 06 12:04:44 2006 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML	Mon Nov 06 16:28:29 2006 +0100
     3.3 @@ -16,24 +16,24 @@
     3.4  
     3.5  end; (*struct HOL*)
     3.6  
     3.7 -structure IntDef = 
     3.8 +structure Nat = 
     3.9  struct
    3.10  
    3.11 -datatype nat = Zero_nat | Succ_nat of nat;
    3.12 +datatype nat = Zero_nat | Suc of nat;
    3.13  
    3.14 -fun less_nat Zero_nat (Succ_nat n) = HOL.True
    3.15 +fun less_nat Zero_nat (Suc n) = HOL.True
    3.16    | less_nat n Zero_nat = HOL.False
    3.17 -  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
    3.18 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    3.19  
    3.20  fun less_eq_nat m n = HOL.nota (less_nat n m);
    3.21  
    3.22 -end; (*struct IntDef*)
    3.23 +end; (*struct Nat*)
    3.24  
    3.25  structure Codegen = 
    3.26  struct
    3.27  
    3.28  fun in_interval (k, l) n =
    3.29 -  HOL.op_conj (IntDef.less_eq_nat k n) (IntDef.less_eq_nat n l);
    3.30 +  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    3.31  
    3.32  end; (*struct Codegen*)
    3.33  
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML	Mon Nov 06 12:04:44 2006 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML	Mon Nov 06 16:28:29 2006 +0100
     4.3 @@ -9,24 +9,24 @@
     4.4  
     4.5  end; (*struct HOL*)
     4.6  
     4.7 -structure IntDef = 
     4.8 +structure Nat = 
     4.9  struct
    4.10  
    4.11 -datatype nat = Zero_nat | Succ_nat of nat;
    4.12 +datatype nat = Zero_nat | Suc of nat;
    4.13  
    4.14 -fun less_nat Zero_nat (Succ_nat n) = true
    4.15 +fun less_nat Zero_nat (Suc n) = true
    4.16    | less_nat n Zero_nat = false
    4.17 -  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
    4.18 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    4.19  
    4.20  fun less_eq_nat m n = HOL.nota (less_nat n m);
    4.21  
    4.22 -end; (*struct IntDef*)
    4.23 +end; (*struct Nat*)
    4.24  
    4.25  structure Codegen = 
    4.26  struct
    4.27  
    4.28  fun in_interval (k, l) n =
    4.29 -  (IntDef.less_eq_nat k n) andalso (IntDef.less_eq_nat n l);
    4.30 +  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    4.31  
    4.32  end; (*struct Codegen*)
    4.33