1.1 --- a/doc-src/Codegen/Thy/Program.thy	Sun Nov 29 20:23:03 2009 +0100
     1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Mon Nov 30 08:44:08 2009 +0100
     1.3 @@ -430,5 +430,220 @@
     1.4    likely to be used in such situations.
     1.5  *}
     1.6  
     1.7 +subsection {* Inductive Predicates *}
     1.8 +(*<*)
     1.9 +hide const append
    1.10 +
    1.11 +inductive append
    1.12 +where
    1.13 +  "append [] ys ys"
    1.14 +| "append xs ys zs ==> append (x # xs) ys (x # zs)"
    1.15 +(*>*)
    1.16 +text {*
    1.17 +To execute inductive predicates, a special preprocessor, the predicate
    1.18 + compiler, generates code equations from the introduction rules of the predicates.
    1.19 +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
    1.20 +Consider the simple predicate @{const append} given by these two
    1.21 +introduction rules:
    1.22 +*}
    1.23 +text %quote {*
    1.24 +@{thm append.intros(1)[of ys]}\\
    1.25 +\noindent@{thm append.intros(2)[of xs ys zs x]}
    1.26 +*}
    1.27 +text {*
    1.28 +\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
    1.29 +*}
    1.30 +code_pred %quote append .
    1.31 +text {*
    1.32 +\noindent The @{command "code_pred"} command takes the name
    1.33 +of the inductive predicate and then you put a period to discharge
    1.34 +a trivial correctness proof. 
    1.35 +The compiler infers possible modes 
    1.36 +for the predicate and produces the derived code equations.
    1.37 +Modes annotate which (parts of the) arguments are to be taken as input,
    1.38 +and which output. Modes are similar to types, but use the notation @{text "i"}
    1.39 +for input and @{text "o"} for output.
    1.40 + 
    1.41 +For @{term "append"}, the compiler can infer the following modes:
    1.42 +\begin{itemize}
    1.43 +\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
    1.44 +\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
    1.45 +\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
    1.46 +\end{itemize}
    1.47 +You can compute sets of predicates using @{command_def "values"}:
    1.48 +*}
    1.49 +values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
    1.50 +text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
    1.51 +values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
    1.52 +text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
    1.53 +text {*
    1.54 +\noindent If you are only interested in the first elements of the set
    1.55 +comprehension (with respect to a depth-first search on the introduction rules), you can
    1.56 +pass an argument to
    1.57 +@{command "values"} to specify the number of elements you want:
    1.58 +*}
    1.59 +
    1.60 +values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
    1.61 +values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
    1.62 +
    1.63 +text {*
    1.64 +\noindent The @{command "values"} command can only compute set
    1.65 + comprehensions for which a mode has been inferred.
    1.66 +
    1.67 +The code equations for a predicate are made available as theorems with
    1.68 + the suffix @{text "equation"}, and can be inspected with:
    1.69 +*}
    1.70 +thm %quote append.equation
    1.71 +text {*
    1.72 +\noindent More advanced options are described in the following subsections.
    1.73 +*}
    1.74 +subsubsection {* Alternative names for functions *}
    1.75 +text {* 
    1.76 +By default, the functions generated from a predicate are named after the predicate with the
    1.77 +mode mangled into the name (e.g., @{text "append_i_i_o"}).
    1.78 +You can specify your own names as follows:
    1.79 +*}
    1.80 +code_pred %quote (modes: i => i => o => bool as concat,
    1.81 +  o => o => i => bool as split,
    1.82 +  i => o => i => bool as suffix) append .
    1.83 +
    1.84 +subsubsection {* Alternative introduction rules *}
    1.85 +text {*
    1.86 +Sometimes the introduction rules of an predicate are not executable because they contain
    1.87 +non-executable constants or specific modes could not be inferred.
    1.88 +It is also possible that the introduction rules yield a function that loops forever
    1.89 +due to the execution in a depth-first search manner.
    1.90 +Therefore, you can declare alternative introduction rules for predicates with the attribute
    1.91 +@{attribute "code_pred_intro"}.
    1.92 +For example, the transitive closure is defined by: 
    1.93 +*}
    1.94 +text %quote {*
    1.95 +@{thm tranclp.intros(1)[of r a b]}\\
    1.96 +\noindent @{thm tranclp.intros(2)[of r a b c]}
    1.97 +*}
    1.98 +text {*
    1.99 +\noindent These rules do not suit well for executing the transitive closure 
   1.100 +with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
   1.101 +cause an infinite loop in the recursive call.
   1.102 +This can be avoided using the following alternative rules which are
   1.103 +declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
   1.104 +*}
   1.105 +lemma %quote [code_pred_intro]:
   1.106 +  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
   1.107 +  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
   1.108 +by auto
   1.109 +text {*
   1.110 +\noindent After declaring all alternative rules for the transitive closure,
   1.111 +you invoke @{command "code_pred"} as usual.
   1.112 +As you have declared alternative rules for the predicate, you are urged to prove that these
   1.113 +introduction rules are complete, i.e., that you can derive an elimination rule for the
   1.114 +alternative rules:
   1.115 +*}
   1.116 +code_pred %quote tranclp
   1.117 +proof -
   1.118 +  case tranclp
   1.119 +  from this converse_tranclpE[OF this(1)] show thesis by metis
   1.120 +qed
   1.121 +text {*
   1.122 +\noindent Alternative rules can also be used for constants that have not
   1.123 +been defined inductively. For example, the lexicographic order which
   1.124 +is defined as: *}
   1.125 +text %quote {*
   1.126 +@{thm [display] lexord_def[of "r"]}
   1.127 +*}
   1.128 +text {*
   1.129 +\noindent To make it executable, you can derive the following two rules and prove the
   1.130 +elimination rule:
   1.131 +*}
   1.132 +(*<*)
   1.133 +lemma append: "append xs ys zs = (xs @ ys = zs)"
   1.134 +by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
   1.135 +(*>*)
   1.136 +lemma %quote [code_pred_intro]:
   1.137 +  "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
   1.138 +(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
   1.139 +
   1.140 +lemma %quote [code_pred_intro]:
   1.141 +  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
   1.142 +  \<Longrightarrow> lexord r (xs, ys)"
   1.143 +(*<*)unfolding lexord_def Collect_def append mem_def apply simp
   1.144 +apply (rule disjI2) by auto
   1.145 +(*>*)
   1.146 +
   1.147 +code_pred %quote lexord
   1.148 +(*<*)
   1.149 +proof -
   1.150 +  fix r a1
   1.151 +  assume lexord: "lexord r a1"
   1.152 +  assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
   1.153 +  assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis"
   1.154 +  obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
   1.155 +  {
   1.156 +    assume "\<exists>a v. ys = xs @ a # v"
   1.157 +    from this 1 a1 have thesis
   1.158 +        by (fastsimp simp add: append)
   1.159 +  } moreover
   1.160 +  {
   1.161 +    assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
   1.162 +    from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
   1.163 +  } moreover
   1.164 +  note lexord[simplified a1]
   1.165 +  ultimately show thesis
   1.166 +    unfolding lexord_def
   1.167 +    by (fastsimp simp add: Collect_def)
   1.168 +qed
   1.169 +(*>*)
   1.170 +subsubsection {* Options for values *}
   1.171 +text {*
   1.172 +In the presence of higher-order predicates, multiple modes for some predicate could be inferred
   1.173 +that are not disambiguated by the pattern of the set comprehension.
   1.174 +To disambiguate the modes for the arguments of a predicate, you can state
   1.175 +the modes explicitly in the @{command "values"} command. 
   1.176 +Consider the simple predicate @{term "succ"}:
   1.177 +*}
   1.178 +inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.179 +where
   1.180 +  "succ 0 (Suc 0)"
   1.181 +| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
   1.182 +
   1.183 +code_pred succ .
   1.184 +
   1.185 +text {*
   1.186 +\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
   1.187 +  @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
   1.188 +The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
   1.189 +modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
   1.190 +is chosen. To choose another mode for the argument, you can declare the mode for the argument between
   1.191 +the @{command "values"} and the number of elements.
   1.192 +*}
   1.193 +values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   1.194 +values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   1.195 +
   1.196 +subsubsection {* Embedding into functional code within Isabelle/HOL *}
   1.197 +text {*
   1.198 +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
   1.199 +you have a number of options:
   1.200 +\begin{itemize}
   1.201 +\item You want to use the first-order predicate with the mode
   1.202 +  where all arguments are input. Then you can use the predicate directly, e.g.
   1.203 +\begin{quote}
   1.204 +  @{text "valid_suffix ys zs = "}\\
   1.205 +  @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
   1.206 +\end{quote}
   1.207 +\item If you know that the execution returns only one value (it is deterministic), then you can
   1.208 +  use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
   1.209 +  is defined with
   1.210 +\begin{quote}
   1.211 +  @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
   1.212 +\end{quote}
   1.213 +  Note that if the evaluation does not return a unique value, it raises a run-time error
   1.214 +  @{term "not_unique"}.
   1.215 +\end{itemize}
   1.216 +*}
   1.217 +subsubsection {* Further Examples *}
   1.218 +text {* Further examples for compiling inductive predicates can be found in
   1.219 +the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
   1.220 +There are also some examples in the Archive of Formal Proofs, notably
   1.221 +in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
   1.222 +*}
   1.223  end
   1.224 - 
   1.225 \ No newline at end of file

     2.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Sun Nov 29 20:23:03 2009 +0100
     2.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Mon Nov 30 08:44:08 2009 +0100
     2.3 @@ -968,6 +968,458 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 +\isamarkupsubsection{Inductive Predicates%
     2.8 +}
     2.9 +\isamarkuptrue%
    2.10 +%
    2.11 +\begin{isamarkuptext}%
    2.12 +To execute inductive predicates, a special preprocessor, the predicate
    2.13 + compiler, generates code equations from the introduction rules of the predicates.
    2.14 +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
    2.15 +Consider the simple predicate \isa{append} given by these two
    2.16 +introduction rules:%
    2.17 +\end{isamarkuptext}%
    2.18 +\isamarkuptrue%
    2.19 +%
    2.20 +\isadelimquote
    2.21 +%
    2.22 +\endisadelimquote
    2.23 +%
    2.24 +\isatagquote
    2.25 +%
    2.26 +\begin{isamarkuptext}%
    2.27 +\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
    2.28 +\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
    2.29 +\end{isamarkuptext}%
    2.30 +\isamarkuptrue%
    2.31 +%
    2.32 +\endisatagquote
    2.33 +{\isafoldquote}%
    2.34 +%
    2.35 +\isadelimquote
    2.36 +%
    2.37 +\endisadelimquote
    2.38 +%
    2.39 +\begin{isamarkuptext}%
    2.40 +\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:%
    2.41 +\end{isamarkuptext}%
    2.42 +\isamarkuptrue%
    2.43 +%
    2.44 +\isadelimquote
    2.45 +%
    2.46 +\endisadelimquote
    2.47 +%
    2.48 +\isatagquote
    2.49 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
    2.50 +\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
    2.51 +%
    2.52 +\endisatagquote
    2.53 +{\isafoldquote}%
    2.54 +%
    2.55 +\isadelimquote
    2.56 +%
    2.57 +\endisadelimquote
    2.58 +%
    2.59 +\begin{isamarkuptext}%
    2.60 +\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
    2.61 +of the inductive predicate and then you put a period to discharge
    2.62 +a trivial correctness proof. 
    2.63 +The compiler infers possible modes 
    2.64 +for the predicate and produces the derived code equations.
    2.65 +Modes annotate which (parts of the) arguments are to be taken as input,
    2.66 +and which output. Modes are similar to types, but use the notation \isa{i}
    2.67 +for input and \isa{o} for output.
    2.68 + 
    2.69 +For \isa{append}, the compiler can infer the following modes:
    2.70 +\begin{itemize}
    2.71 +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
    2.72 +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
    2.73 +\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
    2.74 +\end{itemize}
    2.75 +You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
    2.76 +\end{isamarkuptext}%
    2.77 +\isamarkuptrue%
    2.78 +%
    2.79 +\isadelimquote
    2.80 +%
    2.81 +\endisadelimquote
    2.82 +%
    2.83 +\isatagquote
    2.84 +\isacommand{values}\isamarkupfalse%
    2.85 +\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}%
    2.86 +\endisatagquote
    2.87 +{\isafoldquote}%
    2.88 +%
    2.89 +\isadelimquote
    2.90 +%
    2.91 +\endisadelimquote
    2.92 +%
    2.93 +\begin{isamarkuptext}%
    2.94 +\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and%
    2.95 +\end{isamarkuptext}%
    2.96 +\isamarkuptrue%
    2.97 +%
    2.98 +\isadelimquote
    2.99 +%
   2.100 +\endisadelimquote
   2.101 +%
   2.102 +\isatagquote
   2.103 +\isacommand{values}\isamarkupfalse%
   2.104 +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
   2.105 +\endisatagquote
   2.106 +{\isafoldquote}%
   2.107 +%
   2.108 +\isadelimquote
   2.109 +%
   2.110 +\endisadelimquote
   2.111 +%
   2.112 +\begin{isamarkuptext}%
   2.113 +\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.%
   2.114 +\end{isamarkuptext}%
   2.115 +\isamarkuptrue%
   2.116 +%
   2.117 +\begin{isamarkuptext}%
   2.118 +\noindent If you are only interested in the first elements of the set
   2.119 +comprehension (with respect to a depth-first search on the introduction rules), you can
   2.120 +pass an argument to
   2.121 +\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
   2.122 +\end{isamarkuptext}%
   2.123 +\isamarkuptrue%
   2.124 +%
   2.125 +\isadelimquote
   2.126 +%
   2.127 +\endisadelimquote
   2.128 +%
   2.129 +\isatagquote
   2.130 +\isacommand{values}\isamarkupfalse%
   2.131 +\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
   2.132 +\isacommand{values}\isamarkupfalse%
   2.133 +\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
   2.134 +\endisatagquote
   2.135 +{\isafoldquote}%
   2.136 +%
   2.137 +\isadelimquote
   2.138 +%
   2.139 +\endisadelimquote
   2.140 +%
   2.141 +\begin{isamarkuptext}%
   2.142 +\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
   2.143 + comprehensions for which a mode has been inferred.
   2.144 +
   2.145 +The code equations for a predicate are made available as theorems with
   2.146 + the suffix \isa{equation}, and can be inspected with:%
   2.147 +\end{isamarkuptext}%
   2.148 +\isamarkuptrue%
   2.149 +%
   2.150 +\isadelimquote
   2.151 +%
   2.152 +\endisadelimquote
   2.153 +%
   2.154 +\isatagquote
   2.155 +\isacommand{thm}\isamarkupfalse%
   2.156 +\ append{\isachardot}equation%
   2.157 +\endisatagquote
   2.158 +{\isafoldquote}%
   2.159 +%
   2.160 +\isadelimquote
   2.161 +%
   2.162 +\endisadelimquote
   2.163 +%
   2.164 +\begin{isamarkuptext}%
   2.165 +\noindent More advanced options are described in the following subsections.%
   2.166 +\end{isamarkuptext}%
   2.167 +\isamarkuptrue%
   2.168 +%
   2.169 +\isamarkupsubsubsection{Alternative names for functions%
   2.170 +}
   2.171 +\isamarkuptrue%
   2.172 +%
   2.173 +\begin{isamarkuptext}%
   2.174 +By default, the functions generated from a predicate are named after the predicate with the
   2.175 +mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
   2.176 +You can specify your own names as follows:%
   2.177 +\end{isamarkuptext}%
   2.178 +\isamarkuptrue%
   2.179 +%
   2.180 +\isadelimquote
   2.181 +%
   2.182 +\endisadelimquote
   2.183 +%
   2.184 +\isatagquote
   2.185 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
   2.186 +\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
   2.187 +\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
   2.188 +\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
   2.189 +%
   2.190 +\endisatagquote
   2.191 +{\isafoldquote}%
   2.192 +%
   2.193 +\isadelimquote
   2.194 +%
   2.195 +\endisadelimquote
   2.196 +%
   2.197 +\isamarkupsubsubsection{Alternative introduction rules%
   2.198 +}
   2.199 +\isamarkuptrue%
   2.200 +%
   2.201 +\begin{isamarkuptext}%
   2.202 +Sometimes the introduction rules of an predicate are not executable because they contain
   2.203 +non-executable constants or specific modes could not be inferred.
   2.204 +It is also possible that the introduction rules yield a function that loops forever
   2.205 +due to the execution in a depth-first search manner.
   2.206 +Therefore, you can declare alternative introduction rules for predicates with the attribute
   2.207 +\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
   2.208 +For example, the transitive closure is defined by:%
   2.209 +\end{isamarkuptext}%
   2.210 +\isamarkuptrue%
   2.211 +%
   2.212 +\isadelimquote
   2.213 +%
   2.214 +\endisadelimquote
   2.215 +%
   2.216 +\isatagquote
   2.217 +%
   2.218 +\begin{isamarkuptext}%
   2.219 +\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
   2.220 +\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
   2.221 +\end{isamarkuptext}%
   2.222 +\isamarkuptrue%
   2.223 +%
   2.224 +\endisatagquote
   2.225 +{\isafoldquote}%
   2.226 +%
   2.227 +\isadelimquote
   2.228 +%
   2.229 +\endisadelimquote
   2.230 +%
   2.231 +\begin{isamarkuptext}%
   2.232 +\noindent These rules do not suit well for executing the transitive closure 
   2.233 +with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
   2.234 +cause an infinite loop in the recursive call.
   2.235 +This can be avoided using the following alternative rules which are
   2.236 +declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
   2.237 +\end{isamarkuptext}%
   2.238 +\isamarkuptrue%
   2.239 +%
   2.240 +\isadelimquote
   2.241 +%
   2.242 +\endisadelimquote
   2.243 +%
   2.244 +\isatagquote
   2.245 +\isacommand{lemma}\isamarkupfalse%
   2.246 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
   2.247 +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
   2.248 +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
   2.249 +\isacommand{by}\isamarkupfalse%
   2.250 +\ auto%
   2.251 +\endisatagquote
   2.252 +{\isafoldquote}%
   2.253 +%
   2.254 +\isadelimquote
   2.255 +%
   2.256 +\endisadelimquote
   2.257 +%
   2.258 +\begin{isamarkuptext}%
   2.259 +\noindent After declaring all alternative rules for the transitive closure,
   2.260 +you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
   2.261 +As you have declared alternative rules for the predicate, you are urged to prove that these
   2.262 +introduction rules are complete, i.e., that you can derive an elimination rule for the
   2.263 +alternative rules:%
   2.264 +\end{isamarkuptext}%
   2.265 +\isamarkuptrue%
   2.266 +%
   2.267 +\isadelimquote
   2.268 +%
   2.269 +\endisadelimquote
   2.270 +%
   2.271 +\isatagquote
   2.272 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
   2.273 +\ tranclp\isanewline
   2.274 +\isacommand{proof}\isamarkupfalse%
   2.275 +\ {\isacharminus}\isanewline
   2.276 +\ \ \isacommand{case}\isamarkupfalse%
   2.277 +\ tranclp\isanewline
   2.278 +\ \ \isacommand{from}\isamarkupfalse%
   2.279 +\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
   2.280 +\ thesis\ \isacommand{by}\isamarkupfalse%
   2.281 +\ metis\isanewline
   2.282 +\isacommand{qed}\isamarkupfalse%
   2.283 +%
   2.284 +\endisatagquote
   2.285 +{\isafoldquote}%
   2.286 +%
   2.287 +\isadelimquote
   2.288 +%
   2.289 +\endisadelimquote
   2.290 +%
   2.291 +\begin{isamarkuptext}%
   2.292 +\noindent Alternative rules can also be used for constants that have not
   2.293 +been defined inductively. For example, the lexicographic order which
   2.294 +is defined as:%
   2.295 +\end{isamarkuptext}%
   2.296 +\isamarkuptrue%
   2.297 +%
   2.298 +\isadelimquote
   2.299 +%
   2.300 +\endisadelimquote
   2.301 +%
   2.302 +\isatagquote
   2.303 +%
   2.304 +\begin{isamarkuptext}%
   2.305 +\begin{isabelle}%
   2.306 +lexord\ r\ {\isasymequiv}\isanewline
   2.307 +{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
   2.308 +\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
   2.309 +\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%
   2.310 +\end{isabelle}%
   2.311 +\end{isamarkuptext}%
   2.312 +\isamarkuptrue%
   2.313 +%
   2.314 +\endisatagquote
   2.315 +{\isafoldquote}%
   2.316 +%
   2.317 +\isadelimquote
   2.318 +%
   2.319 +\endisadelimquote
   2.320 +%
   2.321 +\begin{isamarkuptext}%
   2.322 +\noindent To make it executable, you can derive the following two rules and prove the
   2.323 +elimination rule:%
   2.324 +\end{isamarkuptext}%
   2.325 +\isamarkuptrue%
   2.326 +%
   2.327 +\isadelimproof
   2.328 +%
   2.329 +\endisadelimproof
   2.330 +%
   2.331 +\isatagproof
   2.332 +%
   2.333 +\endisatagproof
   2.334 +{\isafoldproof}%
   2.335 +%
   2.336 +\isadelimproof
   2.337 +%
   2.338 +\endisadelimproof
   2.339 +%
   2.340 +\isadelimquote
   2.341 +%
   2.342 +\endisadelimquote
   2.343 +%
   2.344 +\isatagquote
   2.345 +\isacommand{lemma}\isamarkupfalse%
   2.346 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
   2.347 +\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.348 +\isacommand{lemma}\isamarkupfalse%
   2.349 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
   2.350 +\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
   2.351 +\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.352 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
   2.353 +\ lexord%
   2.354 +\endisatagquote
   2.355 +{\isafoldquote}%
   2.356 +%
   2.357 +\isadelimquote
   2.358 +%
   2.359 +\endisadelimquote
   2.360 +%
   2.361 +\isamarkupsubsubsection{Options for values%
   2.362 +}
   2.363 +\isamarkuptrue%
   2.364 +%
   2.365 +\begin{isamarkuptext}%
   2.366 +In the presence of higher-order predicates, multiple modes for some predicate could be inferred
   2.367 +that are not disambiguated by the pattern of the set comprehension.
   2.368 +To disambiguate the modes for the arguments of a predicate, you can state
   2.369 +the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. 
   2.370 +Consider the simple predicate \isa{succ}:%
   2.371 +\end{isamarkuptext}%
   2.372 +\isamarkuptrue%
   2.373 +\isacommand{inductive}\isamarkupfalse%
   2.374 +\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.375 +\isakeyword{where}\isanewline
   2.376 +\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.377 +{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.378 +\isanewline
   2.379 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
   2.380 +\ succ%
   2.381 +\isadelimproof
   2.382 +\ %
   2.383 +\endisadelimproof
   2.384 +%
   2.385 +\isatagproof
   2.386 +\isacommand{{\isachardot}}\isamarkupfalse%
   2.387 +%
   2.388 +\endisatagproof
   2.389 +{\isafoldproof}%
   2.390 +%
   2.391 +\isadelimproof
   2.392 +%
   2.393 +\endisadelimproof
   2.394 +%
   2.395 +\begin{isamarkuptext}%
   2.396 +\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
   2.397 +  \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
   2.398 +The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple
   2.399 +modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
   2.400 +is chosen. To choose another mode for the argument, you can declare the mode for the argument between
   2.401 +the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
   2.402 +\end{isamarkuptext}%
   2.403 +\isamarkuptrue%
   2.404 +%
   2.405 +\isadelimquote
   2.406 +%
   2.407 +\endisadelimquote
   2.408 +%
   2.409 +\isatagquote
   2.410 +\isacommand{values}\isamarkupfalse%
   2.411 +\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
   2.412 +\isacommand{values}\isamarkupfalse%
   2.413 +\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
   2.414 +\endisatagquote
   2.415 +{\isafoldquote}%
   2.416 +%
   2.417 +\isadelimquote
   2.418 +%
   2.419 +\endisadelimquote
   2.420 +%
   2.421 +\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
   2.422 +}
   2.423 +\isamarkuptrue%
   2.424 +%
   2.425 +\begin{isamarkuptext}%
   2.426 +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
   2.427 +you have a number of options:
   2.428 +\begin{itemize}
   2.429 +\item You want to use the first-order predicate with the mode
   2.430 +  where all arguments are input. Then you can use the predicate directly, e.g.
   2.431 +\begin{quote}
   2.432 +  \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
   2.433 +  \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
   2.434 +\end{quote}
   2.435 +\item If you know that the execution returns only one value (it is deterministic), then you can
   2.436 +  use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
   2.437 +  is defined with
   2.438 +\begin{quote}
   2.439 +  \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
   2.440 +\end{quote}
   2.441 +  Note that if the evaluation does not return a unique value, it raises a run-time error
   2.442 +  \isa{not{\isacharunderscore}unique}.
   2.443 +\end{itemize}%
   2.444 +\end{isamarkuptext}%
   2.445 +\isamarkuptrue%
   2.446 +%
   2.447 +\isamarkupsubsubsection{Further Examples%
   2.448 +}
   2.449 +\isamarkuptrue%
   2.450 +%
   2.451 +\begin{isamarkuptext}%
   2.452 +Further examples for compiling inductive predicates can be found in
   2.453 +the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
   2.454 +There are also some examples in the Archive of Formal Proofs, notably
   2.455 +in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
   2.456 +\end{isamarkuptext}%
   2.457 +\isamarkuptrue%
   2.458 +%
   2.459  \isadelimtheory
   2.460  %
   2.461  \endisadelimtheory
   2.462 @@ -982,7 +1434,7 @@
   2.463  %
   2.464  \endisadelimtheory
   2.465  \isanewline
   2.466 -\ \end{isabellebody}%
   2.467 +\end{isabellebody}%
   2.468  %%% Local Variables:
   2.469  %%% mode: latex
   2.470  %%% TeX-master: "root"

     3.1 --- a/doc-src/Codegen/codegen.tex	Sun Nov 29 20:23:03 2009 +0100
     3.2 +++ b/doc-src/Codegen/codegen.tex	Mon Nov 30 08:44:08 2009 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  \title{\includegraphics[scale=0.5]{isabelle_isar}
     3.6    \\[4ex] Code generation from Isabelle/HOL theories}
     3.7 -\author{\emph{Florian Haftmann}}
     3.8 +\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
     3.9  
    3.10  \begin{document}
    3.11  

     4.1 --- a/doc-src/manual.bib	Sun Nov 29 20:23:03 2009 +0100
     4.2 +++ b/doc-src/manual.bib	Mon Nov 30 08:44:08 2009 +0100
     4.3 @@ -172,6 +172,14 @@
     4.4    title =        {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
     4.5    crossref =     {tphols2001}}
     4.6  
     4.7 +@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
     4.8 +    author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
     4.9 +    booktitle = {Theorem Proving in Higher Order Logics},
    4.10 +    pages = {131--146},
    4.11 +    title = {Turning Inductive into Equational Specifications},
    4.12 +    year = {2009}
    4.13 +}
    4.14 +
    4.15  @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
    4.16    crossref        = "tphols2000",
    4.17    title           = "Proof terms for simply typed higher order logic",