1.1 --- a/doc-src/Codegen/IsaMakefile Mon Aug 16 10:54:08 2010 +0200
1.2 +++ b/doc-src/Codegen/IsaMakefile Mon Aug 16 11:18:28 2010 +0200
1.3 @@ -24,7 +24,7 @@
1.4 Thy: $(THY)
1.5
1.6 $(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
1.7 - @$(USEDIR) HOL Thy
1.8 + @$(USEDIR) -m no_brackets -m iff HOL Thy
1.9 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
1.10 Thy/document/pdfsetup.sty Thy/document/session.tex
1.11
2.1 --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 10:54:08 2010 +0200
2.2 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 11:18:28 2010 +0200
2.3 @@ -2,135 +2,164 @@
2.4 imports Setup
2.5 begin
2.6
2.7 -section {* Inductive Predicates \label{sec:inductive} *}
2.8 (*<*)
2.9 -hide_const append
2.10 +hide_const %invisible append
2.11
2.12 -inductive append
2.13 -where
2.14 +inductive %invisible append where
2.15 "append [] ys ys"
2.16 | "append xs ys zs ==> append (x # xs) ys (x # zs)"
2.17 +
2.18 +lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
2.19 + by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
2.20 (*>*)
2.21 +
2.22 +section {* Inductive Predicates \label{sec:inductive} *}
2.23 +
2.24 text {*
2.25 -To execute inductive predicates, a special preprocessor, the predicate
2.26 - compiler, generates code equations from the introduction rules of the predicates.
2.27 -The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
2.28 -Consider the simple predicate @{const append} given by these two
2.29 -introduction rules:
2.30 -*}
2.31 -text %quote {*
2.32 -@{thm append.intros(1)[of ys]}\\
2.33 -\noindent@{thm append.intros(2)[of xs ys zs x]}
2.34 -*}
2.35 -text {*
2.36 -\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
2.37 -*}
2.38 -code_pred %quote append .
2.39 -text {*
2.40 -\noindent The @{command "code_pred"} command takes the name
2.41 -of the inductive predicate and then you put a period to discharge
2.42 -a trivial correctness proof.
2.43 -The compiler infers possible modes
2.44 -for the predicate and produces the derived code equations.
2.45 -Modes annotate which (parts of the) arguments are to be taken as input,
2.46 -and which output. Modes are similar to types, but use the notation @{text "i"}
2.47 -for input and @{text "o"} for output.
2.48 -
2.49 -For @{term "append"}, the compiler can infer the following modes:
2.50 -\begin{itemize}
2.51 -\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
2.52 -\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
2.53 -\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
2.54 -\end{itemize}
2.55 -You can compute sets of predicates using @{command_def "values"}:
2.56 -*}
2.57 -values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
2.58 -text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
2.59 -values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
2.60 -text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
2.61 -text {*
2.62 -\noindent If you are only interested in the first elements of the set
2.63 -comprehension (with respect to a depth-first search on the introduction rules), you can
2.64 -pass an argument to
2.65 -@{command "values"} to specify the number of elements you want:
2.66 + The @{text predicate_compiler} is an extension of the code generator
2.67 + which turns inductive specifications into equational ones, from
2.68 + which in turn executable code can be generated. The mechanisms of
2.69 + this compiler are described in detail in
2.70 + \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
2.71 +
2.72 + Consider the simple predicate @{const append} given by these two
2.73 + introduction rules:
2.74 *}
2.75
2.76 -values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
2.77 -values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
2.78 +text %quote {*
2.79 + @{thm append.intros(1)[of ys]} \\
2.80 + @{thm append.intros(2)[of xs ys zs x]}
2.81 +*}
2.82
2.83 text {*
2.84 -\noindent The @{command "values"} command can only compute set
2.85 - comprehensions for which a mode has been inferred.
2.86 + \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
2.87 +*}
2.88
2.89 -The code equations for a predicate are made available as theorems with
2.90 - the suffix @{text "equation"}, and can be inspected with:
2.91 +code_pred %quote append .
2.92 +
2.93 +text {*
2.94 + \noindent The @{command "code_pred"} command takes the name of the
2.95 + inductive predicate and then you put a period to discharge a trivial
2.96 + correctness proof. The compiler infers possible modes for the
2.97 + predicate and produces the derived code equations. Modes annotate
2.98 + which (parts of the) arguments are to be taken as input, and which
2.99 + output. Modes are similar to types, but use the notation @{text "i"}
2.100 + for input and @{text "o"} for output.
2.101 +
2.102 + For @{term "append"}, the compiler can infer the following modes:
2.103 + \begin{itemize}
2.104 + \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
2.105 + \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
2.106 + \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
2.107 + \end{itemize}
2.108 + You can compute sets of predicates using @{command_def "values"}:
2.109 *}
2.110 +
2.111 +values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
2.112 +
2.113 +text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
2.114 +
2.115 +values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
2.116 +
2.117 +text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
2.118 +
2.119 +text {*
2.120 + \noindent If you are only interested in the first elements of the
2.121 + set comprehension (with respect to a depth-first search on the
2.122 + introduction rules), you can pass an argument to @{command "values"}
2.123 + to specify the number of elements you want:
2.124 +*}
2.125 +
2.126 +values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
2.127 +values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
2.128 +
2.129 +text {*
2.130 + \noindent The @{command "values"} command can only compute set
2.131 + comprehensions for which a mode has been inferred.
2.132 +
2.133 + The code equations for a predicate are made available as theorems with
2.134 + the suffix @{text "equation"}, and can be inspected with:
2.135 +*}
2.136 +
2.137 thm %quote append.equation
2.138 +
2.139 text {*
2.140 -\noindent More advanced options are described in the following subsections.
2.141 + \noindent More advanced options are described in the following subsections.
2.142 *}
2.143 -subsubsection {* Alternative names for functions *}
2.144 +
2.145 +subsection {* Alternative names for functions *}
2.146 +
2.147 text {*
2.148 -By default, the functions generated from a predicate are named after the predicate with the
2.149 -mode mangled into the name (e.g., @{text "append_i_i_o"}).
2.150 -You can specify your own names as follows:
2.151 + By default, the functions generated from a predicate are named after
2.152 + the predicate with the mode mangled into the name (e.g., @{text
2.153 + "append_i_i_o"}). You can specify your own names as follows:
2.154 *}
2.155 +
2.156 code_pred %quote (modes: i => i => o => bool as concat,
2.157 o => o => i => bool as split,
2.158 i => o => i => bool as suffix) append .
2.159
2.160 -subsubsection {* Alternative introduction rules *}
2.161 +subsection {* Alternative introduction rules *}
2.162 +
2.163 text {*
2.164 -Sometimes the introduction rules of an predicate are not executable because they contain
2.165 -non-executable constants or specific modes could not be inferred.
2.166 -It is also possible that the introduction rules yield a function that loops forever
2.167 -due to the execution in a depth-first search manner.
2.168 -Therefore, you can declare alternative introduction rules for predicates with the attribute
2.169 -@{attribute "code_pred_intro"}.
2.170 -For example, the transitive closure is defined by:
2.171 + Sometimes the introduction rules of an predicate are not executable
2.172 + because they contain non-executable constants or specific modes
2.173 + could not be inferred. It is also possible that the introduction
2.174 + rules yield a function that loops forever due to the execution in a
2.175 + depth-first search manner. Therefore, you can declare alternative
2.176 + introduction rules for predicates with the attribute @{attribute
2.177 + "code_pred_intro"}. For example, the transitive closure is defined
2.178 + by:
2.179 *}
2.180 +
2.181 text %quote {*
2.182 -@{thm tranclp.intros(1)[of r a b]}\\
2.183 -\noindent @{thm tranclp.intros(2)[of r a b c]}
2.184 + @{thm tranclp.intros(1)[of r a b]} \\
2.185 + @{thm tranclp.intros(2)[of r a b c]}
2.186 *}
2.187 +
2.188 text {*
2.189 -\noindent These rules do not suit well for executing the transitive closure
2.190 -with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
2.191 -cause an infinite loop in the recursive call.
2.192 -This can be avoided using the following alternative rules which are
2.193 -declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
2.194 + \noindent These rules do not suit well for executing the transitive
2.195 + closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
2.196 + the second rule will cause an infinite loop in the recursive call.
2.197 + This can be avoided using the following alternative rules which are
2.198 + declared to the predicate compiler by the attribute @{attribute
2.199 + "code_pred_intro"}:
2.200 *}
2.201 +
2.202 lemma %quote [code_pred_intro]:
2.203 "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
2.204 "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
2.205 by auto
2.206 +
2.207 text {*
2.208 -\noindent After declaring all alternative rules for the transitive closure,
2.209 -you invoke @{command "code_pred"} as usual.
2.210 -As you have declared alternative rules for the predicate, you are urged to prove that these
2.211 -introduction rules are complete, i.e., that you can derive an elimination rule for the
2.212 -alternative rules:
2.213 + \noindent After declaring all alternative rules for the transitive
2.214 + closure, you invoke @{command "code_pred"} as usual. As you have
2.215 + declared alternative rules for the predicate, you are urged to prove
2.216 + that these introduction rules are complete, i.e., that you can
2.217 + derive an elimination rule for the alternative rules:
2.218 *}
2.219 +
2.220 code_pred %quote tranclp
2.221 proof -
2.222 case tranclp
2.223 - from this converse_tranclpE[OF this(1)] show thesis by metis
2.224 + from this converse_tranclpE [OF this(1)] show thesis by metis
2.225 qed
2.226 +
2.227 text {*
2.228 -\noindent Alternative rules can also be used for constants that have not
2.229 -been defined inductively. For example, the lexicographic order which
2.230 -is defined as: *}
2.231 + \noindent Alternative rules can also be used for constants that have
2.232 + not been defined inductively. For example, the lexicographic order
2.233 + which is defined as:
2.234 +*}
2.235 +
2.236 text %quote {*
2.237 -@{thm [display] lexord_def[of "r"]}
2.238 + @{thm [display] lexord_def[of "r"]}
2.239 *}
2.240 +
2.241 text {*
2.242 -\noindent To make it executable, you can derive the following two rules and prove the
2.243 -elimination rule:
2.244 + \noindent To make it executable, you can derive the following two
2.245 + rules and prove the elimination rule:
2.246 *}
2.247 -(*<*)
2.248 -lemma append: "append xs ys zs = (xs @ ys = zs)"
2.249 -by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
2.250 -(*>*)
2.251 +
2.252 lemma %quote [code_pred_intro]:
2.253 "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
2.254 (*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
2.255 @@ -139,12 +168,10 @@
2.256 "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
2.257 \<Longrightarrow> lexord r (xs, ys)"
2.258 (*<*)unfolding lexord_def Collect_def append mem_def apply simp
2.259 -apply (rule disjI2) by auto
2.260 -(*>*)
2.261 +apply (rule disjI2) by auto(*>*)
2.262
2.263 code_pred %quote lexord
2.264 -(*<*)
2.265 -proof -
2.266 +(*<*)proof -
2.267 fix r xs ys
2.268 assume lexord: "lexord r (xs, ys)"
2.269 assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
2.270 @@ -162,59 +189,81 @@
2.271 ultimately show thesis
2.272 unfolding lexord_def
2.273 by (fastsimp simp add: Collect_def)
2.274 -qed
2.275 -(*>*)
2.276 -subsubsection {* Options for values *}
2.277 +qed(*>*)
2.278 +
2.279 +
2.280 +subsection {* Options for values *}
2.281 +
2.282 text {*
2.283 -In the presence of higher-order predicates, multiple modes for some predicate could be inferred
2.284 -that are not disambiguated by the pattern of the set comprehension.
2.285 -To disambiguate the modes for the arguments of a predicate, you can state
2.286 -the modes explicitly in the @{command "values"} command.
2.287 -Consider the simple predicate @{term "succ"}:
2.288 + In the presence of higher-order predicates, multiple modes for some
2.289 + predicate could be inferred that are not disambiguated by the
2.290 + pattern of the set comprehension. To disambiguate the modes for the
2.291 + arguments of a predicate, you can state the modes explicitly in the
2.292 + @{command "values"} command. Consider the simple predicate @{term
2.293 + "succ"}:
2.294 *}
2.295 -inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2.296 -where
2.297 +
2.298 +inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
2.299 "succ 0 (Suc 0)"
2.300 | "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
2.301
2.302 -code_pred succ .
2.303 +code_pred %quote succ .
2.304
2.305 text {*
2.306 -\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
2.307 - @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
2.308 -The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
2.309 -modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
2.310 -is chosen. To choose another mode for the argument, you can declare the mode for the argument between
2.311 -the @{command "values"} and the number of elements.
2.312 + \noindent For this, the predicate compiler can infer modes @{text "o
2.313 + \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
2.314 + @{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}
2.315 + @{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the
2.316 + predicate @{text "succ"} are possible and here the first mode @{text
2.317 + "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
2.318 + you can declare the mode for the argument between the @{command
2.319 + "values"} and the number of elements.
2.320 *}
2.321 +
2.322 values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
2.323 values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
2.324
2.325 -subsubsection {* Embedding into functional code within Isabelle/HOL *}
2.326 +
2.327 +subsection {* Embedding into functional code within Isabelle/HOL *}
2.328 +
2.329 text {*
2.330 -To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
2.331 -you have a number of options:
2.332 -\begin{itemize}
2.333 -\item You want to use the first-order predicate with the mode
2.334 - where all arguments are input. Then you can use the predicate directly, e.g.
2.335 -\begin{quote}
2.336 - @{text "valid_suffix ys zs = "}\\
2.337 - @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
2.338 -\end{quote}
2.339 -\item If you know that the execution returns only one value (it is deterministic), then you can
2.340 - use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
2.341 - is defined with
2.342 -\begin{quote}
2.343 - @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
2.344 -\end{quote}
2.345 - Note that if the evaluation does not return a unique value, it raises a run-time error
2.346 - @{term "not_unique"}.
2.347 -\end{itemize}
2.348 + To embed the computation of an inductive predicate into functions
2.349 + that are defined in Isabelle/HOL, you have a number of options:
2.350 +
2.351 + \begin{itemize}
2.352 +
2.353 + \item You want to use the first-order predicate with the mode
2.354 + where all arguments are input. Then you can use the predicate directly, e.g.
2.355 +
2.356 + \begin{quote}
2.357 + @{text "valid_suffix ys zs = "} \\
2.358 + @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
2.359 + \end{quote}
2.360 +
2.361 + \item If you know that the execution returns only one value (it is
2.362 + deterministic), then you can use the combinator @{term
2.363 + "Predicate.the"}, e.g., a functional concatenation of lists is
2.364 + defined with
2.365 +
2.366 + \begin{quote}
2.367 + @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
2.368 + \end{quote}
2.369 +
2.370 + Note that if the evaluation does not return a unique value, it
2.371 + raises a run-time error @{term "not_unique"}.
2.372 +
2.373 + \end{itemize}
2.374 *}
2.375 -subsubsection {* Further Examples *}
2.376 -text {* Further examples for compiling inductive predicates can be found in
2.377 -the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
2.378 -There are also some examples in the Archive of Formal Proofs, notably
2.379 -in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
2.380 +
2.381 +
2.382 +subsection {* Further Examples *}
2.383 +
2.384 +text {*
2.385 + Further examples for compiling inductive predicates can be found in
2.386 + the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file. There are
2.387 + also some examples in the Archive of Formal Proofs, notably in the
2.388 + @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
2.389 + sessions.
2.390 *}
2.391 +
2.392 end
3.1 --- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 10:54:08 2010 +0200
3.2 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 11:18:28 2010 +0200
3.3 @@ -10,7 +10,8 @@
3.4 \isacommand{theory}\isamarkupfalse%
3.5 \ Inductive{\isacharunderscore}Predicate\isanewline
3.6 \isakeyword{imports}\ Setup\isanewline
3.7 -\isakeyword{begin}%
3.8 +\isakeyword{begin}\isanewline
3.9 +%
3.10 \endisatagtheory
3.11 {\isafoldtheory}%
3.12 %
3.13 @@ -18,16 +19,32 @@
3.14 %
3.15 \endisadelimtheory
3.16 %
3.17 +\isadeliminvisible
3.18 +%
3.19 +\endisadeliminvisible
3.20 +%
3.21 +\isataginvisible
3.22 +%
3.23 +\endisataginvisible
3.24 +{\isafoldinvisible}%
3.25 +%
3.26 +\isadeliminvisible
3.27 +%
3.28 +\endisadeliminvisible
3.29 +%
3.30 \isamarkupsection{Inductive Predicates \label{sec:inductive}%
3.31 }
3.32 \isamarkuptrue%
3.33 %
3.34 \begin{isamarkuptext}%
3.35 -To execute inductive predicates, a special preprocessor, the predicate
3.36 - compiler, generates code equations from the introduction rules of the predicates.
3.37 -The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
3.38 -Consider the simple predicate \isa{append} given by these two
3.39 -introduction rules:%
3.40 +The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
3.41 + which turns inductive specifications into equational ones, from
3.42 + which in turn executable code can be generated. The mechanisms of
3.43 + this compiler are described in detail in
3.44 + \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
3.45 +
3.46 + Consider the simple predicate \isa{append} given by these two
3.47 + introduction rules:%
3.48 \end{isamarkuptext}%
3.49 \isamarkuptrue%
3.50 %
3.51 @@ -38,8 +55,8 @@
3.52 \isatagquote
3.53 %
3.54 \begin{isamarkuptext}%
3.55 -\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
3.56 -\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
3.57 +\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys} \\
3.58 + \isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
3.59 \end{isamarkuptext}%
3.60 \isamarkuptrue%
3.61 %
3.62 @@ -71,22 +88,21 @@
3.63 \endisadelimquote
3.64 %
3.65 \begin{isamarkuptext}%
3.66 -\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
3.67 -of the inductive predicate and then you put a period to discharge
3.68 -a trivial correctness proof.
3.69 -The compiler infers possible modes
3.70 -for the predicate and produces the derived code equations.
3.71 -Modes annotate which (parts of the) arguments are to be taken as input,
3.72 -and which output. Modes are similar to types, but use the notation \isa{i}
3.73 -for input and \isa{o} for output.
3.74 +\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name of the
3.75 + inductive predicate and then you put a period to discharge a trivial
3.76 + correctness proof. The compiler infers possible modes for the
3.77 + predicate and produces the derived code equations. Modes annotate
3.78 + which (parts of the) arguments are to be taken as input, and which
3.79 + output. Modes are similar to types, but use the notation \isa{i}
3.80 + for input and \isa{o} for output.
3.81
3.82 -For \isa{append}, the compiler can infer the following modes:
3.83 -\begin{itemize}
3.84 -\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
3.85 -\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
3.86 -\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
3.87 -\end{itemize}
3.88 -You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
3.89 + For \isa{append}, the compiler can infer the following modes:
3.90 + \begin{itemize}
3.91 + \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
3.92 + \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
3.93 + \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
3.94 + \end{itemize}
3.95 + You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
3.96 \end{isamarkuptext}%
3.97 \isamarkuptrue%
3.98 %
3.99 @@ -129,10 +145,10 @@
3.100 \isamarkuptrue%
3.101 %
3.102 \begin{isamarkuptext}%
3.103 -\noindent If you are only interested in the first elements of the set
3.104 -comprehension (with respect to a depth-first search on the introduction rules), you can
3.105 -pass an argument to
3.106 -\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
3.107 +\noindent If you are only interested in the first elements of the
3.108 + set comprehension (with respect to a depth-first search on the
3.109 + introduction rules), you can pass an argument to \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
3.110 + to specify the number of elements you want:%
3.111 \end{isamarkuptext}%
3.112 \isamarkuptrue%
3.113 %
3.114 @@ -142,9 +158,9 @@
3.115 %
3.116 \isatagquote
3.117 \isacommand{values}\isamarkupfalse%
3.118 -\ {\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
3.119 +\ {\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
3.120 \isacommand{values}\isamarkupfalse%
3.121 -\ {\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}%
3.122 +\ {\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}%
3.123 \endisatagquote
3.124 {\isafoldquote}%
3.125 %
3.126 @@ -154,10 +170,10 @@
3.127 %
3.128 \begin{isamarkuptext}%
3.129 \noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
3.130 - comprehensions for which a mode has been inferred.
3.131 + comprehensions for which a mode has been inferred.
3.132
3.133 -The code equations for a predicate are made available as theorems with
3.134 - the suffix \isa{equation}, and can be inspected with:%
3.135 + The code equations for a predicate are made available as theorems with
3.136 + the suffix \isa{equation}, and can be inspected with:%
3.137 \end{isamarkuptext}%
3.138 \isamarkuptrue%
3.139 %
3.140 @@ -180,14 +196,13 @@
3.141 \end{isamarkuptext}%
3.142 \isamarkuptrue%
3.143 %
3.144 -\isamarkupsubsubsection{Alternative names for functions%
3.145 +\isamarkupsubsection{Alternative names for functions%
3.146 }
3.147 \isamarkuptrue%
3.148 %
3.149 \begin{isamarkuptext}%
3.150 -By default, the functions generated from a predicate are named after the predicate with the
3.151 -mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
3.152 -You can specify your own names as follows:%
3.153 +By default, the functions generated from a predicate are named after
3.154 + the predicate with the mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). You can specify your own names as follows:%
3.155 \end{isamarkuptext}%
3.156 \isamarkuptrue%
3.157 %
3.158 @@ -208,18 +223,18 @@
3.159 %
3.160 \endisadelimquote
3.161 %
3.162 -\isamarkupsubsubsection{Alternative introduction rules%
3.163 +\isamarkupsubsection{Alternative introduction rules%
3.164 }
3.165 \isamarkuptrue%
3.166 %
3.167 \begin{isamarkuptext}%
3.168 -Sometimes the introduction rules of an predicate are not executable because they contain
3.169 -non-executable constants or specific modes could not be inferred.
3.170 -It is also possible that the introduction rules yield a function that loops forever
3.171 -due to the execution in a depth-first search manner.
3.172 -Therefore, you can declare alternative introduction rules for predicates with the attribute
3.173 -\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
3.174 -For example, the transitive closure is defined by:%
3.175 +Sometimes the introduction rules of an predicate are not executable
3.176 + because they contain non-executable constants or specific modes
3.177 + could not be inferred. It is also possible that the introduction
3.178 + rules yield a function that loops forever due to the execution in a
3.179 + depth-first search manner. Therefore, you can declare alternative
3.180 + introduction rules for predicates with the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. For example, the transitive closure is defined
3.181 + by:%
3.182 \end{isamarkuptext}%
3.183 \isamarkuptrue%
3.184 %
3.185 @@ -230,8 +245,8 @@
3.186 \isatagquote
3.187 %
3.188 \begin{isamarkuptext}%
3.189 -\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
3.190 -\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
3.191 +\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\
3.192 + \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
3.193 \end{isamarkuptext}%
3.194 \isamarkuptrue%
3.195 %
3.196 @@ -243,11 +258,11 @@
3.197 \endisadelimquote
3.198 %
3.199 \begin{isamarkuptext}%
3.200 -\noindent These rules do not suit well for executing the transitive closure
3.201 -with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
3.202 -cause an infinite loop in the recursive call.
3.203 -This can be avoided using the following alternative rules which are
3.204 -declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
3.205 +\noindent These rules do not suit well for executing the transitive
3.206 + closure with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as
3.207 + the second rule will cause an infinite loop in the recursive call.
3.208 + This can be avoided using the following alternative rules which are
3.209 + declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
3.210 \end{isamarkuptext}%
3.211 \isamarkuptrue%
3.212 %
3.213 @@ -270,11 +285,11 @@
3.214 \endisadelimquote
3.215 %
3.216 \begin{isamarkuptext}%
3.217 -\noindent After declaring all alternative rules for the transitive closure,
3.218 -you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
3.219 -As you have declared alternative rules for the predicate, you are urged to prove that these
3.220 -introduction rules are complete, i.e., that you can derive an elimination rule for the
3.221 -alternative rules:%
3.222 +\noindent After declaring all alternative rules for the transitive
3.223 + closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. As you have
3.224 + declared alternative rules for the predicate, you are urged to prove
3.225 + that these introduction rules are complete, i.e., that you can
3.226 + derive an elimination rule for the alternative rules:%
3.227 \end{isamarkuptext}%
3.228 \isamarkuptrue%
3.229 %
3.230 @@ -290,7 +305,7 @@
3.231 \ \ \isacommand{case}\isamarkupfalse%
3.232 \ tranclp\isanewline
3.233 \ \ \isacommand{from}\isamarkupfalse%
3.234 -\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
3.235 +\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
3.236 \ thesis\ \isacommand{by}\isamarkupfalse%
3.237 \ metis\isanewline
3.238 \isacommand{qed}\isamarkupfalse%
3.239 @@ -303,9 +318,9 @@
3.240 \endisadelimquote
3.241 %
3.242 \begin{isamarkuptext}%
3.243 -\noindent Alternative rules can also be used for constants that have not
3.244 -been defined inductively. For example, the lexicographic order which
3.245 -is defined as:%
3.246 +\noindent Alternative rules can also be used for constants that have
3.247 + not been defined inductively. For example, the lexicographic order
3.248 + which is defined as:%
3.249 \end{isamarkuptext}%
3.250 \isamarkuptrue%
3.251 %
3.252 @@ -333,24 +348,11 @@
3.253 \endisadelimquote
3.254 %
3.255 \begin{isamarkuptext}%
3.256 -\noindent To make it executable, you can derive the following two rules and prove the
3.257 -elimination rule:%
3.258 +\noindent To make it executable, you can derive the following two
3.259 + rules and prove the elimination rule:%
3.260 \end{isamarkuptext}%
3.261 \isamarkuptrue%
3.262 %
3.263 -\isadelimproof
3.264 -%
3.265 -\endisadelimproof
3.266 -%
3.267 -\isatagproof
3.268 -%
3.269 -\endisatagproof
3.270 -{\isafoldproof}%
3.271 -%
3.272 -\isadelimproof
3.273 -%
3.274 -\endisadelimproof
3.275 -%
3.276 \isadelimquote
3.277 %
3.278 \endisadelimquote
3.279 @@ -372,47 +374,45 @@
3.280 %
3.281 \endisadelimquote
3.282 %
3.283 -\isamarkupsubsubsection{Options for values%
3.284 +\isamarkupsubsection{Options for values%
3.285 }
3.286 \isamarkuptrue%
3.287 %
3.288 \begin{isamarkuptext}%
3.289 -In the presence of higher-order predicates, multiple modes for some predicate could be inferred
3.290 -that are not disambiguated by the pattern of the set comprehension.
3.291 -To disambiguate the modes for the arguments of a predicate, you can state
3.292 -the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.
3.293 -Consider the simple predicate \isa{succ}:%
3.294 +In the presence of higher-order predicates, multiple modes for some
3.295 + predicate could be inferred that are not disambiguated by the
3.296 + pattern of the set comprehension. To disambiguate the modes for the
3.297 + arguments of a predicate, you can state the modes explicitly in the
3.298 + \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. Consider the simple predicate \isa{succ}:%
3.299 \end{isamarkuptext}%
3.300 \isamarkuptrue%
3.301 +%
3.302 +\isadelimquote
3.303 +%
3.304 +\endisadelimquote
3.305 +%
3.306 +\isatagquote
3.307 \isacommand{inductive}\isamarkupfalse%
3.308 -\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
3.309 -\isakeyword{where}\isanewline
3.310 +\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.311 \ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.312 {\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.313 \isanewline
3.314 \isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
3.315 -\ succ%
3.316 -\isadelimproof
3.317 -\ %
3.318 -\endisadelimproof
3.319 +\ succ\ \isacommand{{\isachardot}}\isamarkupfalse%
3.320 %
3.321 -\isatagproof
3.322 -\isacommand{{\isachardot}}\isamarkupfalse%
3.323 +\endisatagquote
3.324 +{\isafoldquote}%
3.325 %
3.326 -\endisatagproof
3.327 -{\isafoldproof}%
3.328 +\isadelimquote
3.329 %
3.330 -\isadelimproof
3.331 -%
3.332 -\endisadelimproof
3.333 +\endisadelimquote
3.334 %
3.335 \begin{isamarkuptext}%
3.336 -\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
3.337 - \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
3.338 -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
3.339 -modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
3.340 -is chosen. To choose another mode for the argument, you can declare the mode for the argument between
3.341 -the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
3.342 +\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and
3.343 + \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
3.344 + \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple modes for the
3.345 + predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} is chosen. To choose another mode for the argument,
3.346 + you can declare the mode for the argument between the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
3.347 \end{isamarkuptext}%
3.348 \isamarkuptrue%
3.349 %
3.350 @@ -432,41 +432,49 @@
3.351 %
3.352 \endisadelimquote
3.353 %
3.354 -\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
3.355 +\isamarkupsubsection{Embedding into functional code within Isabelle/HOL%
3.356 }
3.357 \isamarkuptrue%
3.358 %
3.359 \begin{isamarkuptext}%
3.360 -To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
3.361 -you have a number of options:
3.362 -\begin{itemize}
3.363 -\item You want to use the first-order predicate with the mode
3.364 - where all arguments are input. Then you can use the predicate directly, e.g.
3.365 -\begin{quote}
3.366 - \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
3.367 - \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
3.368 -\end{quote}
3.369 -\item If you know that the execution returns only one value (it is deterministic), then you can
3.370 - use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
3.371 - is defined with
3.372 -\begin{quote}
3.373 - \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
3.374 -\end{quote}
3.375 - Note that if the evaluation does not return a unique value, it raises a run-time error
3.376 - \isa{not{\isacharunderscore}unique}.
3.377 -\end{itemize}%
3.378 +To embed the computation of an inductive predicate into functions
3.379 + that are defined in Isabelle/HOL, you have a number of options:
3.380 +
3.381 + \begin{itemize}
3.382 +
3.383 + \item You want to use the first-order predicate with the mode
3.384 + where all arguments are input. Then you can use the predicate directly, e.g.
3.385 +
3.386 + \begin{quote}
3.387 + \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}} \\
3.388 + \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
3.389 + \end{quote}
3.390 +
3.391 + \item If you know that the execution returns only one value (it is
3.392 + deterministic), then you can use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists is
3.393 + defined with
3.394 +
3.395 + \begin{quote}
3.396 + \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
3.397 + \end{quote}
3.398 +
3.399 + Note that if the evaluation does not return a unique value, it
3.400 + raises a run-time error \isa{not{\isacharunderscore}unique}.
3.401 +
3.402 + \end{itemize}%
3.403 \end{isamarkuptext}%
3.404 \isamarkuptrue%
3.405 %
3.406 -\isamarkupsubsubsection{Further Examples%
3.407 +\isamarkupsubsection{Further Examples%
3.408 }
3.409 \isamarkuptrue%
3.410 %
3.411 \begin{isamarkuptext}%
3.412 Further examples for compiling inductive predicates can be found in
3.413 -the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
3.414 -There are also some examples in the Archive of Formal Proofs, notably
3.415 -in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
3.416 + the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file. There are
3.417 + also some examples in the Archive of Formal Proofs, notably in the
3.418 + \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
3.419 + sessions.%
3.420 \end{isamarkuptext}%
3.421 \isamarkuptrue%
3.422 %