doc-src/IsarAdvanced/Codegen/Thy/Program.thy

 
 text {*
   We have already seen how by default equations stemming from
   @{command definition}/@{command primrec}/@{command fun}
   statements are used for code generation.  This default behaviour
-  can be changed, e.g. by providing different defining equations.
+  can be changed, e.g. by providing different code equations.
   All kinds of customisation shown in this section is \emph{safe}
   in the sense that the user does not have to worry about
   correctness -- all programs generatable that way are partially
   correct.
 *}
 
 subsection {* Selecting code equations *}
 
 text {*
   Coming back to our introductory example, we
-  could provide an alternative defining equations for @{const dequeue}
+  could provide an alternative code equations for @{const dequeue}
   explicitly:
 *}
 
 lemma %quote [code]:
   "dequeue (Queue xs []) =

   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
 text {*
   \noindent The annotation @{text "[code]"} is an @{text Isar}
   @{text attribute} which states that the given theorems should be
-  considered as defining equations for a @{text fun} statement --
+  considered as code equations for a @{text fun} statement --
   the corresponding constant is determined syntactically.  The resulting code:
 *}
 
 text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
 

 *}
 
 code_thms %quote dequeue
 
 text {*
-  \noindent prints a table with \emph{all} defining equations
+  \noindent prints a table with \emph{all} code equations
   for @{const dequeue}, including
-  \emph{all} defining equations those equations depend
+  \emph{all} code equations those equations depend
   on recursively.
   
   Similarly, the @{command code_deps} command shows a graph
-  visualising dependencies between defining equations.
+  visualising dependencies between code equations.
 *}
 
 subsection {* @{text class} and @{text instantiation} *}
 
 text {*

   out: \emph{preprocessing}.  In essence, the preprocessor
   consists of two components: a \emph{simpset} and \emph{function transformers}.
 
   The \emph{simpset} allows to employ the full generality of the Isabelle
   simplifier.  Due to the interpretation of theorems
-  as defining equations, rewrites are applied to the right
+  as code equations, rewrites are applied to the right
   hand side and the arguments of the left hand side of an
   equation, but never to the constant heading the left hand side.
   An important special case are \emph{inline theorems} which may be
   declared and undeclared using the
   \emph{code inline} or \emph{code inline del} attribute respectively.

 
   \noindent The current setup of the preprocessor may be inspected using
   the @{command print_codesetup} command.
   @{command code_thms} provides a convenient
   mechanism to inspect the impact of a preprocessor setup
-  on defining equations.
+  on code equations.
 
   \begin{warn}
     The attribute \emph{code unfold}
     associated with the @{text "SML code generator"} also applies to
     the @{text "generic code generator"}:

   \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces
   an explicit class @{class eq} with a corresponding operation
   @{const eq_class.eq} such that @{thm eq [no_vars]}.
   The preprocessing framework does the rest by propagating the
-  @{class eq} constraints through all dependent defining equations.
+  @{class eq} constraints through all dependent code equations.
   For datatypes, instances of @{class eq} are implicitly derived
   when possible.  For other types, you may instantiate @{text eq}
   manually like any other type class.
 
   Though this @{text eq} class is designed to get rarely in

 *}
 
 text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
 
 text {*
-  In some cases, the automatically derived defining equations
+  In some cases, the automatically derived code equations
   for equality on a particular type may not be appropriate.
   As example, watch the following datatype representing
   monomorphic parametric types (where type constructors
   are referred to by natural numbers):
 *}

   @{const strict_dequeue'} is more involved since it requires
   a manual termination proof.  Apart from that observe that
   on the right hand side of its first equation the constant
   @{const empty_queue} occurs which is unspecified.
 
-  Normally, if constants without any defining equations occur in
+  Normally, if constants without any code equations occur in
   a program, the code generator complains (since in most cases
   this is not what the user expects).  But such constants can also
   be thought of as function definitions with no equations which
   always fail, since there is never a successful pattern match
   on the left hand side.  In order to categorise a constant into