haftmann@28213: theory Program
haftmann@28419: imports Introduction
haftmann@28213: begin
haftmann@28213: 
haftmann@28419: section {* Turning Theories into Programs \label{sec:program} *}
haftmann@28213: 
haftmann@28213: subsection {* The @{text "Isabelle/HOL"} default setup *}
haftmann@28213: 
haftmann@28447: text {*
haftmann@28447:   We have already seen how by default equations stemming from
paulson@34155:   @{command definition}, @{command primrec} and @{command fun}
haftmann@28447:   statements are used for code generation.  This default behaviour
paulson@34155:   can be changed, e.g.\ by providing different code equations.
paulson@34155:   The customisations shown in this section are \emph{safe}
paulson@34155:   as regards correctness: all programs that can be generated are partially
haftmann@28447:   correct.
haftmann@28447: *}
haftmann@28447: 
haftmann@28213: subsection {* Selecting code equations *}
haftmann@28213: 
haftmann@28419: text {*
haftmann@28447:   Coming back to our introductory example, we
haftmann@29560:   could provide an alternative code equations for @{const dequeue}
haftmann@28447:   explicitly:
haftmann@28419: *}
haftmann@28213: 
haftmann@28564: lemma %quote [code]:
haftmann@29735:   "dequeue (AQueue xs []) =
haftmann@29735:      (if xs = [] then (None, AQueue [] [])
haftmann@29735:        else dequeue (AQueue [] (rev xs)))"
haftmann@29735:   "dequeue (AQueue xs (y # ys)) =
haftmann@29735:      (Some y, AQueue xs ys)"
haftmann@28419:   by (cases xs, simp_all) (cases "rev xs", simp_all)
haftmann@28213: 
haftmann@28419: text {*
haftmann@28562:   \noindent The annotation @{text "[code]"} is an @{text Isar}
haftmann@28419:   @{text attribute} which states that the given theorems should be
haftmann@29560:   considered as code equations for a @{text fun} statement --
haftmann@28419:   the corresponding constant is determined syntactically.  The resulting code:
haftmann@28419: *}
haftmann@28213: 
haftmann@28564: text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   \noindent You may note that the equality test @{term "xs = []"} has been
haftmann@28419:   replaced by the predicate @{term "null xs"}.  This is due to the default
haftmann@28419:   setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
haftmann@28419: 
haftmann@28419:   Changing the default constructor set of datatypes is also
haftmann@29731:   possible.  See \secref{sec:datatypes} for an example.
haftmann@28419: 
haftmann@28419:   As told in \secref{sec:concept}, code generation is based
haftmann@28419:   on a structured collection of code theorems.
paulson@34155:   This collection
haftmann@28419:   may be inspected using the @{command code_thms} command:
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: code_thms %quote dequeue
haftmann@28419: 
haftmann@28419: text {*
haftmann@29560:   \noindent prints a table with \emph{all} code equations
haftmann@28419:   for @{const dequeue}, including
haftmann@29560:   \emph{all} code equations those equations depend
haftmann@28419:   on recursively.
haftmann@28419:   
haftmann@28419:   Similarly, the @{command code_deps} command shows a graph
haftmann@29560:   visualising dependencies between code equations.
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: subsection {* @{text class} and @{text instantiation} *}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28447:   Concerning type classes and code generation, let us examine an example
haftmann@28419:   from abstract algebra:
haftmann@28419: *}
haftmann@28419: 
haftmann@29731: class %quote semigroup =
haftmann@28419:   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
haftmann@28419:   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
haftmann@28419: 
haftmann@28564: class %quote monoid = semigroup +
haftmann@28419:   fixes neutral :: 'a ("\<one>")
haftmann@28419:   assumes neutl: "\<one> \<otimes> x = x"
haftmann@28419:     and neutr: "x \<otimes> \<one> = x"
haftmann@28419: 
haftmann@28564: instantiation %quote nat :: monoid
haftmann@28419: begin
haftmann@28419: 
haftmann@28564: primrec %quote mult_nat where
haftmann@28419:     "0 \<otimes> n = (0\<Colon>nat)"
haftmann@28419:   | "Suc m \<otimes> n = n + m \<otimes> n"
haftmann@28419: 
haftmann@28564: definition %quote neutral_nat where
haftmann@28419:   "\<one> = Suc 0"
haftmann@28419: 
haftmann@28564: lemma %quote add_mult_distrib:
haftmann@28419:   fixes n m q :: nat
haftmann@28419:   shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
haftmann@28419:   by (induct n) simp_all
haftmann@28419: 
haftmann@28564: instance %quote proof
haftmann@28419:   fix m n q :: nat
haftmann@28419:   show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
haftmann@28419:     by (induct m) (simp_all add: add_mult_distrib)
haftmann@28419:   show "\<one> \<otimes> n = n"
haftmann@28419:     by (simp add: neutral_nat_def)
haftmann@28419:   show "m \<otimes> \<one> = m"
haftmann@28419:     by (induct m) (simp_all add: neutral_nat_def)
haftmann@28419: qed
haftmann@28419: 
haftmann@28564: end %quote
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   \noindent We define the natural operation of the natural numbers
haftmann@28419:   on monoids:
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@28419:     "pow 0 a = \<one>"
haftmann@28419:   | "pow (Suc n) a = a \<otimes> pow n a"
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   \noindent This we use to define the discrete exponentiation function:
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: definition %quote bexp :: "nat \<Rightarrow> nat" where
haftmann@28419:   "bexp n = pow n (Suc (Suc 0))"
haftmann@28419: 
haftmann@28419: text {*
paulson@34155:   \noindent The corresponding code in Haskell uses that language's native classes:
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: text %quote {*@{code_stmts bexp (Haskell)}*}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28447:   \noindent This is a convenient place to show how explicit dictionary construction
haftmann@28419:   manifests in generated code (here, the same example in @{text SML}):
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: text %quote {*@{code_stmts bexp (SML)}*}
haftmann@28419: 
haftmann@28447: text {*
paulson@34155:   \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
haftmann@28447:     which are the dictionary parameters.
haftmann@28447: *}
haftmann@28419: 
haftmann@28419: subsection {* The preprocessor \label{sec:preproc} *}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   Before selected function theorems are turned into abstract
haftmann@28419:   code, a chain of definitional transformation steps is carried
haftmann@28419:   out: \emph{preprocessing}.  In essence, the preprocessor
haftmann@28419:   consists of two components: a \emph{simpset} and \emph{function transformers}.
haftmann@28419: 
paulson@34155:   The \emph{simpset} can apply the full generality of the
haftmann@32000:   Isabelle simplifier.  Due to the interpretation of theorems as code
haftmann@32000:   equations, rewrites are applied to the right hand side and the
haftmann@32000:   arguments of the left hand side of an equation, but never to the
haftmann@32000:   constant heading the left hand side.  An important special case are
paulson@34155:   \emph{unfold theorems},  which may be declared and removed using
haftmann@32000:   the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
paulson@34155:   attribute, respectively.
haftmann@28419: 
haftmann@28419:   Some common applications:
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: text_raw {*
haftmann@28419:   \begin{itemize}
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:      \item replacing non-executable constructs by executable ones:
haftmann@28419: *}     
haftmann@28419: 
haftmann@37209: lemma %quote [code_unfold]:
haftmann@37209:   "x \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:      \item eliminating superfluous constants:
haftmann@28419: *}
haftmann@28419: 
haftmann@37209: lemma %quote [code_unfold]:
haftmann@37209:   "1 = Suc 0" by (fact One_nat_def)
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:      \item replacing executable but inconvenient constructs:
haftmann@28419: *}
haftmann@28419: 
haftmann@37209: lemma %quote [code_unfold]:
haftmann@37209:   "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
haftmann@28419: 
haftmann@28419: text_raw {*
haftmann@28419:   \end{itemize}
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28447:   \noindent \emph{Function transformers} provide a very general interface,
haftmann@28419:   transforming a list of function theorems to another
haftmann@28419:   list of function theorems, provided that neither the heading
haftmann@28419:   constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
haftmann@28419:   pattern elimination implemented in
haftmann@28419:   theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
haftmann@28419:   interface.
haftmann@28419: 
haftmann@28419:   \noindent The current setup of the preprocessor may be inspected using
haftmann@31248:   the @{command print_codeproc} command.
haftmann@28419:   @{command code_thms} provides a convenient
haftmann@28419:   mechanism to inspect the impact of a preprocessor setup
haftmann@29560:   on code equations.
haftmann@28419: 
haftmann@28419:   \begin{warn}
haftmann@32000: 
haftmann@32000:     Attribute @{attribute code_unfold} also applies to the
haftmann@32000:     preprocessor of the ancient @{text "SML code generator"}; in case
haftmann@32000:     this is not what you intend, use @{attribute code_inline} instead.
haftmann@28419:   \end{warn}
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: subsection {* Datatypes \label{sec:datatypes} *}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   Conceptually, any datatype is spanned by a set of
haftmann@29731:   \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
haftmann@29731:   "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
haftmann@29731:   @{text "\<tau>"}.  The HOL datatype package by default registers any new
haftmann@29731:   datatype in the table of datatypes, which may be inspected using the
haftmann@29731:   @{command print_codesetup} command.
haftmann@28419: 
haftmann@29731:   In some cases, it is appropriate to alter or extend this table.  As
haftmann@29731:   an example, we will develop an alternative representation of the
haftmann@29731:   queue example given in \secref{sec:intro}.  The amortised
haftmann@29731:   representation is convenient for generating code but exposes its
haftmann@29731:   \qt{implementation} details, which may be cumbersome when proving
paulson@34155:   theorems about it.  Therefore, here is a simple, straightforward
haftmann@29731:   representation of queues:
haftmann@28419: *}
haftmann@28419: 
haftmann@29731: datatype %quote 'a queue = Queue "'a list"
haftmann@28419: 
haftmann@29731: definition %quote empty :: "'a queue" where
haftmann@29731:   "empty = Queue []"
haftmann@29731: 
haftmann@29731: primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
haftmann@29731:   "enqueue x (Queue xs) = Queue (xs @ [x])"
haftmann@29731: 
haftmann@29731: fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
haftmann@29731:     "dequeue (Queue []) = (None, Queue [])"
haftmann@29731:   | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
haftmann@28419: 
haftmann@28419: text {*
haftmann@29731:   \noindent This we can use directly for proving;  for executing,
haftmann@29731:   we provide an alternative characterisation:
haftmann@28419: *}
haftmann@28419: 
haftmann@29731: definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
haftmann@29731:   "AQueue xs ys = Queue (ys @ rev xs)"
haftmann@29731: 
haftmann@29731: code_datatype %quote AQueue
haftmann@29731: 
haftmann@29735: text {*
haftmann@29735:   \noindent Here we define a \qt{constructor} @{const "AQueue"} which
haftmann@29735:   is defined in terms of @{text "Queue"} and interprets its arguments
haftmann@29735:   according to what the \emph{content} of an amortised queue is supposed
haftmann@29735:   to be.  Equipped with this, we are able to prove the following equations
haftmann@29735:   for our primitive queue operations which \qt{implement} the simple
haftmann@29735:   queues in an amortised fashion:
haftmann@29735: *}
haftmann@29731: 
haftmann@29731: lemma %quote empty_AQueue [code]:
haftmann@29731:   "empty = AQueue [] []"
haftmann@29731:   unfolding AQueue_def empty_def by simp
haftmann@29731: 
haftmann@29731: lemma %quote enqueue_AQueue [code]:
haftmann@29731:   "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
haftmann@29731:   unfolding AQueue_def by simp
haftmann@29731: 
haftmann@29731: lemma %quote dequeue_AQueue [code]:
haftmann@29731:   "dequeue (AQueue xs []) =
haftmann@29735:     (if xs = [] then (None, AQueue [] [])
haftmann@29735:     else dequeue (AQueue [] (rev xs)))"
haftmann@29731:   "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
haftmann@29731:   unfolding AQueue_def by simp_all
haftmann@29731: 
haftmann@29735: text {*
haftmann@29735:   \noindent For completeness, we provide a substitute for the
haftmann@29735:   @{text case} combinator on queues:
haftmann@29735: *}
haftmann@29731: 
haftmann@30210: lemma %quote queue_case_AQueue [code]:
haftmann@30210:   "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
haftmann@30210:   unfolding AQueue_def by simp
haftmann@29731: 
haftmann@29735: text {*
haftmann@29735:   \noindent The resulting code looks as expected:
haftmann@29735: *}
haftmann@29731: 
haftmann@29731: text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
haftmann@28419: 
haftmann@28419: text {*
haftmann@29731:   \noindent From this example, it can be glimpsed that using own
haftmann@29731:   constructor sets is a little delicate since it changes the set of
haftmann@29731:   valid patterns for values of that type.  Without going into much
haftmann@29731:   detail, here some practical hints:
haftmann@28419: 
haftmann@28419:   \begin{itemize}
haftmann@29731: 
haftmann@29731:     \item When changing the constructor set for datatypes, take care
haftmann@30210:       to provide alternative equations for the @{text case} combinator.
haftmann@29731: 
haftmann@29731:     \item Values in the target language need not to be normalised --
haftmann@29731:       different values in the target language may represent the same
haftmann@29731:       value in the logic.
haftmann@29731: 
haftmann@29731:     \item Usually, a good methodology to deal with the subtleties of
haftmann@29731:       pattern matching is to see the type as an abstract type: provide
haftmann@29731:       a set of operations which operate on the concrete representation
haftmann@29731:       of the type, and derive further operations by combinations of
haftmann@29731:       these primitive ones, without relying on a particular
haftmann@29731:       representation.
haftmann@29731: 
haftmann@28419:   \end{itemize}
haftmann@28419: *}
haftmann@28419: 
haftmann@28213: 
haftmann@30938: subsection {* Equality *}
haftmann@28213: 
haftmann@28419: text {*
haftmann@28419:   Surely you have already noticed how equality is treated
haftmann@28419:   by the code generator:
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@28447:   "collect_duplicates xs ys [] = xs"
haftmann@28419:   | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
haftmann@28419:       then if z \<in> set ys
haftmann@28419:         then collect_duplicates xs ys zs
haftmann@28419:         else collect_duplicates xs (z#ys) zs
haftmann@28419:       else collect_duplicates (z#xs) (z#ys) zs)"
haftmann@28419: 
haftmann@28419: text {*
haftmann@28428:   \noindent The membership test during preprocessing is rewritten,
haftmann@28419:   resulting in @{const List.member}, which itself
haftmann@28419:   performs an explicit equality check.
haftmann@28419: *}
haftmann@28419: 
haftmann@28564: text %quote {*@{code_stmts collect_duplicates (SML)}*}
haftmann@28419: 
haftmann@28419: text {*
haftmann@28419:   \noindent Obviously, polymorphic equality is implemented the Haskell
haftmann@28419:   way using a type class.  How is this achieved?  HOL introduces
haftmann@28419:   an explicit class @{class eq} with a corresponding operation
haftmann@28419:   @{const eq_class.eq} such that @{thm eq [no_vars]}.
haftmann@28447:   The preprocessing framework does the rest by propagating the
haftmann@29560:   @{class eq} constraints through all dependent code equations.
haftmann@28419:   For datatypes, instances of @{class eq} are implicitly derived
haftmann@28419:   when possible.  For other types, you may instantiate @{text eq}
haftmann@28419:   manually like any other type class.
haftmann@28419: *}
haftmann@28419: 
haftmann@28419: 
haftmann@28462: subsection {* Explicit partiality *}
haftmann@28213: 
haftmann@28462: text {*
haftmann@28462:   Partiality usually enters the game by partial patterns, as
haftmann@28462:   in the following example, again for amortised queues:
haftmann@28462: *}
haftmann@28462: 
haftmann@29735: definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
haftmann@29735:   "strict_dequeue q = (case dequeue q
haftmann@29735:     of (Some x, q') \<Rightarrow> (x, q'))"
haftmann@29735: 
haftmann@29735: lemma %quote strict_dequeue_AQueue [code]:
haftmann@29735:   "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
haftmann@29735:   "strict_dequeue (AQueue xs []) =
haftmann@29735:     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
haftmann@29735:   by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
haftmann@28462: 
haftmann@28462: text {*
haftmann@28462:   \noindent In the corresponding code, there is no equation
haftmann@29735:   for the pattern @{term "AQueue [] []"}:
haftmann@28462: *}
haftmann@28462: 
haftmann@28564: text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
haftmann@28462: 
haftmann@28462: text {*
haftmann@28462:   \noindent In some cases it is desirable to have this
haftmann@28462:   pseudo-\qt{partiality} more explicitly, e.g.~as follows:
haftmann@28462: *}
haftmann@28462: 
haftmann@28564: axiomatization %quote empty_queue :: 'a
haftmann@28462: 
haftmann@29735: definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
haftmann@29735:   "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
haftmann@28462: 
haftmann@29735: lemma %quote strict_dequeue'_AQueue [code]:
haftmann@29735:   "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
haftmann@29735:      else strict_dequeue' (AQueue [] (rev xs)))"
haftmann@29735:   "strict_dequeue' (AQueue xs (y # ys)) =
haftmann@29735:      (y, AQueue xs ys)"
haftmann@29735:   by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
haftmann@28462: 
haftmann@28462: text {*
haftmann@29735:   Observe that on the right hand side of the definition of @{const
paulson@34155:   "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
haftmann@28462: 
haftmann@29735:   Normally, if constants without any code equations occur in a
haftmann@29735:   program, the code generator complains (since in most cases this is
paulson@34155:   indeed an error).  But such constants can also be thought
paulson@34155:   of as function definitions which always fail,
haftmann@29735:   since there is never a successful pattern match on the left hand
haftmann@29735:   side.  In order to categorise a constant into that category
haftmann@29735:   explicitly, use @{command "code_abort"}:
haftmann@28462: *}
haftmann@28462: 
haftmann@28564: code_abort %quote empty_queue
haftmann@28462: 
haftmann@28462: text {*
haftmann@28462:   \noindent Then the code generator will just insert an error or
haftmann@28462:   exception at the appropriate position:
haftmann@28462: *}
haftmann@28462: 
haftmann@28564: text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
haftmann@28462: 
haftmann@28462: text {*
haftmann@28462:   \noindent This feature however is rarely needed in practice.
haftmann@28462:   Note also that the @{text HOL} default setup already declares
haftmann@28462:   @{const undefined} as @{command "code_abort"}, which is most
haftmann@28462:   likely to be used in such situations.
haftmann@28462: *}
haftmann@28213: 
bulwahn@33942: subsection {* Inductive Predicates *}
bulwahn@33942: (*<*)
wenzelm@36176: hide_const append
bulwahn@33942: 
bulwahn@33942: inductive append
bulwahn@33942: where
bulwahn@33942:   "append [] ys ys"
bulwahn@33942: | "append xs ys zs ==> append (x # xs) ys (x # zs)"
bulwahn@33942: (*>*)
bulwahn@33942: text {*
bulwahn@33942: To execute inductive predicates, a special preprocessor, the predicate
bulwahn@33942:  compiler, generates code equations from the introduction rules of the predicates.
bulwahn@33942: The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
bulwahn@33942: Consider the simple predicate @{const append} given by these two
bulwahn@33942: introduction rules:
bulwahn@33942: *}
bulwahn@33942: text %quote {*
bulwahn@33942: @{thm append.intros(1)[of ys]}\\
bulwahn@33942: \noindent@{thm append.intros(2)[of xs ys zs x]}
bulwahn@33942: *}
bulwahn@33942: text {*
bulwahn@33942: \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
bulwahn@33942: *}
bulwahn@33942: code_pred %quote append .
bulwahn@33942: text {*
bulwahn@33942: \noindent The @{command "code_pred"} command takes the name
bulwahn@33942: of the inductive predicate and then you put a period to discharge
bulwahn@33942: a trivial correctness proof. 
bulwahn@33942: The compiler infers possible modes 
bulwahn@33942: for the predicate and produces the derived code equations.
bulwahn@33942: Modes annotate which (parts of the) arguments are to be taken as input,
bulwahn@33942: and which output. Modes are similar to types, but use the notation @{text "i"}
bulwahn@33942: for input and @{text "o"} for output.
bulwahn@33942:  
bulwahn@33942: For @{term "append"}, the compiler can infer the following modes:
bulwahn@33942: \begin{itemize}
bulwahn@33942: \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
bulwahn@33942: \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
bulwahn@33942: \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
bulwahn@33942: \end{itemize}
bulwahn@33942: You can compute sets of predicates using @{command_def "values"}:
bulwahn@33942: *}
bulwahn@33942: values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
bulwahn@33942: text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
bulwahn@33942: values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
bulwahn@33942: text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
bulwahn@33942: text {*
bulwahn@33942: \noindent If you are only interested in the first elements of the set
bulwahn@33942: comprehension (with respect to a depth-first search on the introduction rules), you can
bulwahn@33942: pass an argument to
bulwahn@33942: @{command "values"} to specify the number of elements you want:
bulwahn@33942: *}
bulwahn@33942: 
bulwahn@33942: values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
bulwahn@33942: values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
bulwahn@33942: 
bulwahn@33942: text {*
bulwahn@33942: \noindent The @{command "values"} command can only compute set
bulwahn@33942:  comprehensions for which a mode has been inferred.
bulwahn@33942: 
bulwahn@33942: The code equations for a predicate are made available as theorems with
bulwahn@33942:  the suffix @{text "equation"}, and can be inspected with:
bulwahn@33942: *}
bulwahn@33942: thm %quote append.equation
bulwahn@33942: text {*
bulwahn@33942: \noindent More advanced options are described in the following subsections.
bulwahn@33942: *}
bulwahn@33942: subsubsection {* Alternative names for functions *}
bulwahn@33942: text {* 
bulwahn@33942: By default, the functions generated from a predicate are named after the predicate with the
bulwahn@33942: mode mangled into the name (e.g., @{text "append_i_i_o"}).
bulwahn@33942: You can specify your own names as follows:
bulwahn@33942: *}
bulwahn@33942: code_pred %quote (modes: i => i => o => bool as concat,
bulwahn@33942:   o => o => i => bool as split,
bulwahn@33942:   i => o => i => bool as suffix) append .
bulwahn@33942: 
bulwahn@33942: subsubsection {* Alternative introduction rules *}
bulwahn@33942: text {*
bulwahn@33942: Sometimes the introduction rules of an predicate are not executable because they contain
bulwahn@33942: non-executable constants or specific modes could not be inferred.
bulwahn@33942: It is also possible that the introduction rules yield a function that loops forever
bulwahn@33942: due to the execution in a depth-first search manner.
bulwahn@33942: Therefore, you can declare alternative introduction rules for predicates with the attribute
bulwahn@33942: @{attribute "code_pred_intro"}.
bulwahn@33942: For example, the transitive closure is defined by: 
bulwahn@33942: *}
bulwahn@33942: text %quote {*
bulwahn@33942: @{thm tranclp.intros(1)[of r a b]}\\
bulwahn@33942: \noindent @{thm tranclp.intros(2)[of r a b c]}
bulwahn@33942: *}
bulwahn@33942: text {*
bulwahn@33942: \noindent These rules do not suit well for executing the transitive closure 
bulwahn@33942: with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
bulwahn@33942: cause an infinite loop in the recursive call.
bulwahn@33942: This can be avoided using the following alternative rules which are
bulwahn@33942: declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
bulwahn@33942: *}
bulwahn@33942: lemma %quote [code_pred_intro]:
bulwahn@33942:   "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
bulwahn@33942:   "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
bulwahn@33942: by auto
bulwahn@33942: text {*
bulwahn@33942: \noindent After declaring all alternative rules for the transitive closure,
bulwahn@33942: you invoke @{command "code_pred"} as usual.
bulwahn@33942: As you have declared alternative rules for the predicate, you are urged to prove that these
bulwahn@33942: introduction rules are complete, i.e., that you can derive an elimination rule for the
bulwahn@33942: alternative rules:
bulwahn@33942: *}
bulwahn@33942: code_pred %quote tranclp
bulwahn@33942: proof -
bulwahn@33942:   case tranclp
bulwahn@33942:   from this converse_tranclpE[OF this(1)] show thesis by metis
bulwahn@33942: qed
bulwahn@33942: text {*
bulwahn@33942: \noindent Alternative rules can also be used for constants that have not
bulwahn@33942: been defined inductively. For example, the lexicographic order which
bulwahn@33942: is defined as: *}
bulwahn@33942: text %quote {*
bulwahn@33942: @{thm [display] lexord_def[of "r"]}
bulwahn@33942: *}
bulwahn@33942: text {*
bulwahn@33942: \noindent To make it executable, you can derive the following two rules and prove the
bulwahn@33942: elimination rule:
bulwahn@33942: *}
bulwahn@33942: (*<*)
bulwahn@33942: lemma append: "append xs ys zs = (xs @ ys = zs)"
bulwahn@33942: by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
bulwahn@33942: (*>*)
bulwahn@33942: lemma %quote [code_pred_intro]:
bulwahn@33942:   "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
bulwahn@33942: (*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
bulwahn@33942: 
bulwahn@33942: lemma %quote [code_pred_intro]:
bulwahn@33942:   "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
bulwahn@33942:   \<Longrightarrow> lexord r (xs, ys)"
bulwahn@33942: (*<*)unfolding lexord_def Collect_def append mem_def apply simp
bulwahn@33942: apply (rule disjI2) by auto
bulwahn@33942: (*>*)
bulwahn@33942: 
bulwahn@33942: code_pred %quote lexord
bulwahn@33942: (*<*)
bulwahn@33942: proof -
bulwahn@36259:   fix r xs ys
bulwahn@36259:   assume lexord: "lexord r (xs, ys)"
bulwahn@36259:   assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
bulwahn@36259:   assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
bulwahn@33942:   {
bulwahn@33942:     assume "\<exists>a v. ys = xs @ a # v"
bulwahn@36259:     from this 1 have thesis
bulwahn@33942:         by (fastsimp simp add: append)
bulwahn@33942:   } moreover
bulwahn@33942:   {
bulwahn@33942:     assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
bulwahn@36259:     from this 2 have thesis by (fastsimp simp add: append mem_def)
bulwahn@33942:   } moreover
bulwahn@36259:   note lexord
bulwahn@33942:   ultimately show thesis
bulwahn@33942:     unfolding lexord_def
bulwahn@33942:     by (fastsimp simp add: Collect_def)
bulwahn@33942: qed
bulwahn@33942: (*>*)
bulwahn@33942: subsubsection {* Options for values *}
bulwahn@33942: text {*
bulwahn@33942: In the presence of higher-order predicates, multiple modes for some predicate could be inferred
bulwahn@33942: that are not disambiguated by the pattern of the set comprehension.
bulwahn@33942: To disambiguate the modes for the arguments of a predicate, you can state
bulwahn@33942: the modes explicitly in the @{command "values"} command. 
bulwahn@33942: Consider the simple predicate @{term "succ"}:
bulwahn@33942: *}
bulwahn@33942: inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
bulwahn@33942: where
bulwahn@33942:   "succ 0 (Suc 0)"
bulwahn@33942: | "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
bulwahn@33942: 
bulwahn@33942: code_pred succ .
bulwahn@33942: 
bulwahn@33942: text {*
bulwahn@33942: \noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
bulwahn@33942:   @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
bulwahn@33942: The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
bulwahn@33942: modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
bulwahn@33942: is chosen. To choose another mode for the argument, you can declare the mode for the argument between
bulwahn@33942: the @{command "values"} and the number of elements.
bulwahn@33942: *}
bulwahn@33942: values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
bulwahn@33942: values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
bulwahn@33942: 
bulwahn@33942: subsubsection {* Embedding into functional code within Isabelle/HOL *}
bulwahn@33942: text {*
bulwahn@33942: To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
bulwahn@33942: you have a number of options:
bulwahn@33942: \begin{itemize}
bulwahn@33942: \item You want to use the first-order predicate with the mode
bulwahn@33942:   where all arguments are input. Then you can use the predicate directly, e.g.
bulwahn@33942: \begin{quote}
bulwahn@33942:   @{text "valid_suffix ys zs = "}\\
bulwahn@33942:   @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
bulwahn@33942: \end{quote}
bulwahn@33942: \item If you know that the execution returns only one value (it is deterministic), then you can
bulwahn@33942:   use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
bulwahn@33942:   is defined with
bulwahn@33942: \begin{quote}
bulwahn@33942:   @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
bulwahn@33942: \end{quote}
bulwahn@33942:   Note that if the evaluation does not return a unique value, it raises a run-time error
bulwahn@33942:   @{term "not_unique"}.
bulwahn@33942: \end{itemize}
bulwahn@33942: *}
bulwahn@33942: subsubsection {* Further Examples *}
bulwahn@33942: text {* Further examples for compiling inductive predicates can be found in
bulwahn@33942: the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
bulwahn@33942: There are also some examples in the Archive of Formal Proofs, notably
bulwahn@33942: in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
bulwahn@33942: *}
haftmann@28213: end