doc-src/IsarRef/Thy/HOL_Specific.thy

 
   \end{description}
 *}
 
 
-subsection {* The old code generator (S. Berghofer) *}
-
-text {* This framework generates code from both functional and
-  relational programs to SML, as explained below.
-
-  \begin{matharray}{rcl}
-    @{command_def "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{attribute_def code} & : & @{text attribute} \\
-  \end{matharray}
-
-  @{rail "
-  ( @@{command code_module} | @@{command code_library} ) modespec? @{syntax name}? \\
-    ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\
-    @'contains' ( ( @{syntax name} '=' @{syntax term} ) + | @{syntax term} + )
-  ;
-
-  modespec: '(' ( @{syntax name} * ) ')'
-  ;
-
-  @@{command (HOL) consts_code} (codespec +)
-  ;
-
-  codespec: const template attachment ?
-  ;
-
-  @@{command (HOL) types_code} (tycodespec +)
-  ;
-
-  tycodespec: @{syntax name} template attachment ?
-  ;
-
-  const: @{syntax term}
-  ;
-
-  template: '(' @{syntax string} ')'
-  ;
-
-  attachment: 'attach' modespec? '{' @{syntax text} '}'
-  ;
-
-  @@{attribute code} name?
-  "}
-*}
-
-
-subsubsection {* Invoking the code generator *}
-
-text {* The code generator is invoked via the @{command code_module}
-  and @{command code_library} commands, which correspond to
-  \emph{incremental} and \emph{modular} code generation, respectively.
-
-  \begin{description}
-
-  \item [Modular] For each theory, an ML structure is generated,
-  containing the code generated from the constants defined in this
-  theory.
-
-  \item [Incremental] All the generated code is emitted into the same
-  structure.  This structure may import code from previously generated
-  structures, which can be specified via @{keyword "imports"}.
-  Moreover, the generated structure may also be referred to in later
-  invocations of the code generator.
-
-  \end{description}
-
-  After the @{command code_module} and @{command code_library}
-  keywords, the user may specify an optional list of ``modes'' in
-  parentheses. These can be used to instruct the code generator to
-  emit additional code for special purposes, e.g.\ functions for
-  converting elements of generated datatypes to Isabelle terms, or
-  test data generators. The list of modes is followed by a module
-  name.  The module name is optional for modular code generation, but
-  must be specified for incremental code generation.
-
-  The code can either be written to a file, in which case a file name
-  has to be specified after the @{keyword "file"} keyword, or be loaded
-  directly into Isabelle's ML environment. In the latter case, the
-  @{command ML} theory command can be used to inspect the results
-  interactively, for example.
-
-  The terms from which to generate code can be specified after the
-  @{keyword "contains"} keyword, either as a list of bindings, or just
-  as a list of terms. In the latter case, the code generator just
-  produces code for all constants and types occuring in the term, but
-  does not bind the compiled terms to ML identifiers.
-
-  Here is an example:
-*}
-
-code_module Test
-contains test = "foldl op + (0 :: int) [1, 2, 3, 4, 5]"
-
-text {* \noindent This binds the result of compiling the given term to
-  the ML identifier @{ML Test.test}.  *}
-
-ML {* @{assert} (Test.test = 15) *}
-
-
-subsubsection {* Configuring the code generator *}
-
-text {* When generating code for a complex term, the code generator
-  recursively calls itself for all subterms.  When it arrives at a
-  constant, the default strategy of the code generator is to look up
-  its definition and try to generate code for it.  Constants which
-  have no definitions that are immediately executable, may be
-  associated with a piece of ML code manually using the @{command_ref
-  consts_code} command.  It takes a list whose elements consist of a
-  constant (given in usual term syntax -- an explicit type constraint
-  accounts for overloading), and a mixfix template describing the ML
-  code. The latter is very much the same as the mixfix templates used
-  when declaring new constants.  The most notable difference is that
-  terms may be included in the ML template using antiquotation
-  brackets @{verbatim "{"}@{verbatim "*"}~@{text "..."}~@{verbatim
-  "*"}@{verbatim "}"}.
-
-  A similar mechanism is available for types: @{command_ref
-  types_code} associates type constructors with specific ML code.
-
-  For example, the following declarations copied from @{file
-  "~~/src/HOL/Product_Type.thy"} describe how the product type of
-  Isabelle/HOL should be compiled to ML.  *}
-
-typedecl ('a, 'b) prod
-consts Pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) prod"
-
-types_code prod  ("(_ */ _)")
-consts_code Pair  ("(_,/ _)")
-
-text {* Sometimes, the code associated with a constant or type may
-  need to refer to auxiliary functions, which have to be emitted when
-  the constant is used. Code for such auxiliary functions can be
-  declared using @{keyword "attach"}. For example, the @{const wfrec}
-  function can be implemented as follows:
-*}
-
-consts_code wfrec  ("\<module>wfrec?")  (* FIXME !? *)
-attach {* fun wfrec f x = f (wfrec f) x *}
-
-text {* If the code containing a call to @{const wfrec} resides in an
-  ML structure different from the one containing the function
-  definition attached to @{const wfrec}, the name of the ML structure
-  (followed by a ``@{text "."}'')  is inserted in place of ``@{text
-  "\<module>"}'' in the above template.  The ``@{text "?"}''  means that
-  the code generator should ignore the first argument of @{const
-  wfrec}, i.e.\ the termination relation, which is usually not
-  executable.
-
-  \medskip Another possibility of configuring the code generator is to
-  register theorems to be used for code generation. Theorems can be
-  registered via the @{attribute code} attribute. It takes an optional
-  name as an argument, which indicates the format of the
-  theorem. Currently supported formats are equations (this is the
-  default when no name is specified) and horn clauses (this is
-  indicated by the name \texttt{ind}). The left-hand sides of
-  equations may only contain constructors and distinct variables,
-  whereas horn clauses must have the same format as introduction rules
-  of inductive definitions.
-
-  The following example specifies three equations from which to
-  generate code for @{term "op <"} on natural numbers (see also
-  @{"file" "~~/src/HOL/Nat.thy"}).  *}
-
-lemma [code]: "(Suc m < Suc n) = (m < n)"
-  and [code]: "((n::nat) < 0) = False"
-  and [code]: "(0 < Suc n) = True" by simp_all
-
-
-subsubsection {* Specific HOL code generators *}
-
-text {* The basic code generator framework offered by Isabelle/Pure
-  has already been extended with additional code generators for
-  specific HOL constructs. These include datatypes, recursive
-  functions and inductive relations. The code generator for inductive
-  relations can handle expressions of the form @{text "(t\<^sub>1, \<dots>, t\<^sub>n) \<in>
-  r"}, where @{text "r"} is an inductively defined relation. If at
-  least one of the @{text "t\<^sub>i"} is a dummy pattern ``@{text "_"}'',
-  the above expression evaluates to a sequence of possible answers. If
-  all of the @{text "t\<^sub>i"} are proper terms, the expression evaluates
-  to a boolean value.
-
-  The following example demonstrates this for beta-reduction on lambda
-  terms (see also @{"file" "~~/src/HOL/Proofs/Lambda/Lambda.thy"}).
-*}
-
-datatype dB =
-    Var nat
-  | App dB dB  (infixl "\<degree>" 200)
-  | Abs dB
-
-primrec lift :: "dB \<Rightarrow> nat \<Rightarrow> dB"
-where
-    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
-  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
-  | "lift (Abs s) k = Abs (lift s (k + 1))"
-
-primrec subst :: "dB \<Rightarrow> dB \<Rightarrow> nat \<Rightarrow> dB"  ("_[_'/_]" [300, 0, 0] 300)
-where
-    "(Var i)[s/k] =
-      (if k < i then Var (i - 1) else if i = k then s else Var i)"
-  | "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
-  | "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
-
-inductive beta :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
-where
-    beta: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
-  | appL: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
-  | appR: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
-  | abs: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
-
-code_module Test
-contains
-  test1 = "Abs (Var 0) \<degree> Var 0 \<rightarrow>\<^sub>\<beta> Var 0"
-  test2 = "Abs (Abs (Var 0 \<degree> Var 0) \<degree> (Abs (Var 0) \<degree> Var 0)) \<rightarrow>\<^sub>\<beta> _"
-
-text {*
-  In the above example, @{ML Test.test1} evaluates to a boolean,
-  whereas @{ML Test.test2} is a lazy sequence whose elements can be
-  inspected separately.
-*}
-
-ML {* @{assert} Test.test1 *}
-ML {* val results = DSeq.list_of Test.test2 *}
-ML {* @{assert} (length results = 2) *}
-
-text {*
-  \medskip The theory underlying the HOL code generator is described
-  more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
-  illustrate the usage of the code generator can be found e.g.\ in
-  @{"file" "~~/src/HOL/MicroJava/J/JListExample.thy"} and @{"file"
-  "~~/src/HOL/MicroJava/JVM/JVMListExample.thy"}.
-*}
-
-
 section {* Definition by specification \label{sec:hol-specification} *}
 
 text {*
   \begin{matharray}{rcl}
     @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\