--- a/doc-src/Codegen/IsaMakefile Mon Aug 16 10:54:08 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile Mon Aug 16 11:18:28 2010 +0200
@@ -24,7 +24,7 @@
Thy: $(THY)
$(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
- @$(USEDIR) HOL Thy
+ @$(USEDIR) -m no_brackets -m iff HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 10:54:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 11:18:28 2010 +0200
@@ -2,135 +2,164 @@
imports Setup
begin
-section {* Inductive Predicates \label{sec:inductive} *}
(*<*)
-hide_const append
+hide_const %invisible append
-inductive append
-where
+inductive %invisible append where
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+
+lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
+ by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
(*>*)
-text {*
-To execute inductive predicates, a special preprocessor, the predicate
- compiler, generates code equations from the introduction rules of the predicates.
-The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-Consider the simple predicate @{const append} given by these two
-introduction rules:
-*}
-text %quote {*
-@{thm append.intros(1)[of ys]}\\
-\noindent@{thm append.intros(2)[of xs ys zs x]}
-*}
-text {*
-\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
-*}
-code_pred %quote append .
+
+section {* Inductive Predicates \label{sec:inductive} *}
+
text {*
-\noindent The @{command "code_pred"} command takes the name
-of the inductive predicate and then you put a period to discharge
-a trivial correctness proof.
-The compiler infers possible modes
-for the predicate and produces the derived code equations.
-Modes annotate which (parts of the) arguments are to be taken as input,
-and which output. Modes are similar to types, but use the notation @{text "i"}
-for input and @{text "o"} for output.
-
-For @{term "append"}, the compiler can infer the following modes:
-\begin{itemize}
-\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
-\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
-\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
-\end{itemize}
-You can compute sets of predicates using @{command_def "values"}:
+ The @{text predicate_compiler} is an extension of the code generator
+ which turns inductive specifications into equational ones, from
+ which in turn executable code can be generated. The mechanisms of
+ this compiler are described in detail in
+ \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+
+ Consider the simple predicate @{const append} given by these two
+ introduction rules:
*}
-values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
-text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
-values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
-text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+
+text %quote {*
+ @{thm append.intros(1)[of ys]} \\
+ @{thm append.intros(2)[of xs ys zs x]}
+*}
+
text {*
-\noindent If you are only interested in the first elements of the set
-comprehension (with respect to a depth-first search on the introduction rules), you can
-pass an argument to
-@{command "values"} to specify the number of elements you want:
+ \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
*}
-values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
-values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+code_pred %quote append .
+
+text {*
+ \noindent The @{command "code_pred"} command takes the name of the
+ inductive predicate and then you put a period to discharge a trivial
+ correctness proof. The compiler infers possible modes for the
+ predicate and produces the derived code equations. Modes annotate
+ which (parts of the) arguments are to be taken as input, and which
+ output. Modes are similar to types, but use the notation @{text "i"}
+ for input and @{text "o"} for output.
+
+ For @{term "append"}, the compiler can infer the following modes:
+ \begin{itemize}
+ \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
+ \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
+ \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
+ \end{itemize}
+ You can compute sets of predicates using @{command_def "values"}:
+*}
+
+values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
+
+text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+
+values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
+
+text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
text {*
-\noindent The @{command "values"} command can only compute set
- comprehensions for which a mode has been inferred.
+ \noindent If you are only interested in the first elements of the
+ set comprehension (with respect to a depth-first search on the
+ introduction rules), you can pass an argument to @{command "values"}
+ to specify the number of elements you want:
+*}
-The code equations for a predicate are made available as theorems with
- the suffix @{text "equation"}, and can be inspected with:
-*}
-thm %quote append.equation
+values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
+values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
+
text {*
-\noindent More advanced options are described in the following subsections.
+ \noindent The @{command "values"} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+ The code equations for a predicate are made available as theorems with
+ the suffix @{text "equation"}, and can be inspected with:
*}
-subsubsection {* Alternative names for functions *}
+
+thm %quote append.equation
+
+text {*
+ \noindent More advanced options are described in the following subsections.
+*}
+
+subsection {* Alternative names for functions *}
+
text {*
-By default, the functions generated from a predicate are named after the predicate with the
-mode mangled into the name (e.g., @{text "append_i_i_o"}).
-You can specify your own names as follows:
+ By default, the functions generated from a predicate are named after
+ the predicate with the mode mangled into the name (e.g., @{text
+ "append_i_i_o"}). You can specify your own names as follows:
*}
+
code_pred %quote (modes: i => i => o => bool as concat,
o => o => i => bool as split,
i => o => i => bool as suffix) append .
-subsubsection {* Alternative introduction rules *}
+subsection {* Alternative introduction rules *}
+
text {*
-Sometimes the introduction rules of an predicate are not executable because they contain
-non-executable constants or specific modes could not be inferred.
-It is also possible that the introduction rules yield a function that loops forever
-due to the execution in a depth-first search manner.
-Therefore, you can declare alternative introduction rules for predicates with the attribute
-@{attribute "code_pred_intro"}.
-For example, the transitive closure is defined by:
+ Sometimes the introduction rules of an predicate are not executable
+ because they contain non-executable constants or specific modes
+ could not be inferred. It is also possible that the introduction
+ rules yield a function that loops forever due to the execution in a
+ depth-first search manner. Therefore, you can declare alternative
+ introduction rules for predicates with the attribute @{attribute
+ "code_pred_intro"}. For example, the transitive closure is defined
+ by:
*}
+
text %quote {*
-@{thm tranclp.intros(1)[of r a b]}\\
-\noindent @{thm tranclp.intros(2)[of r a b c]}
+ @{thm tranclp.intros(1)[of r a b]} \\
+ @{thm tranclp.intros(2)[of r a b c]}
*}
+
text {*
-\noindent These rules do not suit well for executing the transitive closure
-with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
-cause an infinite loop in the recursive call.
-This can be avoided using the following alternative rules which are
-declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
+ \noindent These rules do not suit well for executing the transitive
+ closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
+ the second rule will cause an infinite loop in the recursive call.
+ This can be avoided using the following alternative rules which are
+ declared to the predicate compiler by the attribute @{attribute
+ "code_pred_intro"}:
*}
+
lemma %quote [code_pred_intro]:
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
by auto
+
text {*
-\noindent After declaring all alternative rules for the transitive closure,
-you invoke @{command "code_pred"} as usual.
-As you have declared alternative rules for the predicate, you are urged to prove that these
-introduction rules are complete, i.e., that you can derive an elimination rule for the
-alternative rules:
+ \noindent After declaring all alternative rules for the transitive
+ closure, you invoke @{command "code_pred"} as usual. As you have
+ declared alternative rules for the predicate, you are urged to prove
+ that these introduction rules are complete, i.e., that you can
+ derive an elimination rule for the alternative rules:
*}
+
code_pred %quote tranclp
proof -
case tranclp
- from this converse_tranclpE[OF this(1)] show thesis by metis
+ from this converse_tranclpE [OF this(1)] show thesis by metis
qed
+
text {*
-\noindent Alternative rules can also be used for constants that have not
-been defined inductively. For example, the lexicographic order which
-is defined as: *}
-text %quote {*
-@{thm [display] lexord_def[of "r"]}
+ \noindent Alternative rules can also be used for constants that have
+ not been defined inductively. For example, the lexicographic order
+ which is defined as:
*}
-text {*
-\noindent To make it executable, you can derive the following two rules and prove the
-elimination rule:
+
+text %quote {*
+ @{thm [display] lexord_def[of "r"]}
*}
-(*<*)
-lemma append: "append xs ys zs = (xs @ ys = zs)"
-by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
-(*>*)
+
+text {*
+ \noindent To make it executable, you can derive the following two
+ rules and prove the elimination rule:
+*}
+
lemma %quote [code_pred_intro]:
"append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
@@ -139,12 +168,10 @@
"append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
\<Longrightarrow> lexord r (xs, ys)"
(*<*)unfolding lexord_def Collect_def append mem_def apply simp
-apply (rule disjI2) by auto
-(*>*)
+apply (rule disjI2) by auto(*>*)
code_pred %quote lexord
-(*<*)
-proof -
+(*<*)proof -
fix r xs ys
assume lexord: "lexord r (xs, ys)"
assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
@@ -162,59 +189,81 @@
ultimately show thesis
unfolding lexord_def
by (fastsimp simp add: Collect_def)
-qed
-(*>*)
-subsubsection {* Options for values *}
+qed(*>*)
+
+
+subsection {* Options for values *}
+
text {*
-In the presence of higher-order predicates, multiple modes for some predicate could be inferred
-that are not disambiguated by the pattern of the set comprehension.
-To disambiguate the modes for the arguments of a predicate, you can state
-the modes explicitly in the @{command "values"} command.
-Consider the simple predicate @{term "succ"}:
+ In the presence of higher-order predicates, multiple modes for some
+ predicate could be inferred that are not disambiguated by the
+ pattern of the set comprehension. To disambiguate the modes for the
+ arguments of a predicate, you can state the modes explicitly in the
+ @{command "values"} command. Consider the simple predicate @{term
+ "succ"}:
*}
-inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-where
+
+inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 (Suc 0)"
| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
-code_pred succ .
+code_pred %quote succ .
text {*
-\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
- @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
-The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
-modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
-is chosen. To choose another mode for the argument, you can declare the mode for the argument between
-the @{command "values"} and the number of elements.
+ \noindent For this, the predicate compiler can infer modes @{text "o
+ \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
+ @{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}
+ @{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the
+ predicate @{text "succ"} are possible and here the first mode @{text
+ "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
+ you can declare the mode for the argument between the @{command
+ "values"} and the number of elements.
*}
+
values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
-subsubsection {* Embedding into functional code within Isabelle/HOL *}
+
+subsection {* Embedding into functional code within Isabelle/HOL *}
+
text {*
-To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
-you have a number of options:
-\begin{itemize}
-\item You want to use the first-order predicate with the mode
- where all arguments are input. Then you can use the predicate directly, e.g.
-\begin{quote}
- @{text "valid_suffix ys zs = "}\\
- @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
-\end{quote}
-\item If you know that the execution returns only one value (it is deterministic), then you can
- use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
- is defined with
-\begin{quote}
- @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
-\end{quote}
- Note that if the evaluation does not return a unique value, it raises a run-time error
- @{term "not_unique"}.
-\end{itemize}
+ To embed the computation of an inductive predicate into functions
+ that are defined in Isabelle/HOL, you have a number of options:
+
+ \begin{itemize}
+
+ \item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+
+ \begin{quote}
+ @{text "valid_suffix ys zs = "} \\
+ @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
+ \end{quote}
+
+ \item If you know that the execution returns only one value (it is
+ deterministic), then you can use the combinator @{term
+ "Predicate.the"}, e.g., a functional concatenation of lists is
+ defined with
+
+ \begin{quote}
+ @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
+ \end{quote}
+
+ Note that if the evaluation does not return a unique value, it
+ raises a run-time error @{term "not_unique"}.
+
+ \end{itemize}
*}
-subsubsection {* Further Examples *}
-text {* Further examples for compiling inductive predicates can be found in
-the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
-There are also some examples in the Archive of Formal Proofs, notably
-in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
+
+
+subsection {* Further Examples *}
+
+text {*
+ Further examples for compiling inductive predicates can be found in
+ the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file. There are
+ also some examples in the Archive of Formal Proofs, notably in the
+ @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
+ sessions.
*}
+
end
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 10:54:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 11:18:28 2010 +0200
@@ -10,7 +10,8 @@
\isacommand{theory}\isamarkupfalse%
\ Inductive{\isacharunderscore}Predicate\isanewline
\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
+\isakeyword{begin}\isanewline
+%
\endisatagtheory
{\isafoldtheory}%
%
@@ -18,16 +19,32 @@
%
\endisadelimtheory
%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
\isamarkupsection{Inductive Predicates \label{sec:inductive}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To execute inductive predicates, a special preprocessor, the predicate
- compiler, generates code equations from the introduction rules of the predicates.
-The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-Consider the simple predicate \isa{append} given by these two
-introduction rules:%
+The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
+ which turns inductive specifications into equational ones, from
+ which in turn executable code can be generated. The mechanisms of
+ this compiler are described in detail in
+ \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+
+ Consider the simple predicate \isa{append} given by these two
+ introduction rules:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -38,8 +55,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
-\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
+\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys} \\
+ \isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -71,22 +88,21 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
-of the inductive predicate and then you put a period to discharge
-a trivial correctness proof.
-The compiler infers possible modes
-for the predicate and produces the derived code equations.
-Modes annotate which (parts of the) arguments are to be taken as input,
-and which output. Modes are similar to types, but use the notation \isa{i}
-for input and \isa{o} for output.
+\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name of the
+ inductive predicate and then you put a period to discharge a trivial
+ correctness proof. The compiler infers possible modes for the
+ predicate and produces the derived code equations. Modes annotate
+ which (parts of the) arguments are to be taken as input, and which
+ output. Modes are similar to types, but use the notation \isa{i}
+ for input and \isa{o} for output.
-For \isa{append}, the compiler can infer the following modes:
-\begin{itemize}
-\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
-\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
-\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
-\end{itemize}
-You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
+ For \isa{append}, the compiler can infer the following modes:
+ \begin{itemize}
+ \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+ \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+ \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+ \end{itemize}
+ You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -129,10 +145,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\noindent If you are only interested in the first elements of the set
-comprehension (with respect to a depth-first search on the introduction rules), you can
-pass an argument to
-\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
+\noindent If you are only interested in the first elements of the
+ set comprehension (with respect to a depth-first search on the
+ introduction rules), you can pass an argument to \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
+ to specify the number of elements you want:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -142,9 +158,9 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\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
+\ {\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
\isacommand{values}\isamarkupfalse%
-\ {\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}%
+\ {\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}%
\endisatagquote
{\isafoldquote}%
%
@@ -154,10 +170,10 @@
%
\begin{isamarkuptext}%
\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
- comprehensions for which a mode has been inferred.
+ comprehensions for which a mode has been inferred.
-The code equations for a predicate are made available as theorems with
- the suffix \isa{equation}, and can be inspected with:%
+ The code equations for a predicate are made available as theorems with
+ the suffix \isa{equation}, and can be inspected with:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -180,14 +196,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Alternative names for functions%
+\isamarkupsubsection{Alternative names for functions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-By default, the functions generated from a predicate are named after 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:%
+By default, the functions generated from a predicate are named after
+ 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:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -208,18 +223,18 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Alternative introduction rules%
+\isamarkupsubsection{Alternative introduction rules%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Sometimes the introduction rules of an predicate are not executable because they contain
-non-executable constants or specific modes could not be inferred.
-It is also possible that the introduction rules yield a function that loops forever
-due to the execution in a depth-first search manner.
-Therefore, you can declare alternative 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 by:%
+Sometimes the introduction rules of an predicate are not executable
+ because they contain non-executable constants or specific modes
+ could not be inferred. It is also possible that the introduction
+ rules yield a function that loops forever due to the execution in a
+ depth-first search manner. Therefore, you can declare alternative
+ 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
+ by:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -230,8 +245,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
-\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\
+ \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -243,11 +258,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent These rules do not suit well for executing the transitive closure
-with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
-cause an infinite loop in the recursive call.
-This can be avoided using the following alternative rules which are
-declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
+\noindent These rules do not suit well for executing the transitive
+ closure with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as
+ the second rule will cause an infinite loop in the recursive call.
+ This can be avoided using the following alternative rules which are
+ declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -270,11 +285,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent After declaring all alternative rules for the transitive closure,
-you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
-As you have declared alternative rules for the predicate, you are urged to prove that these
-introduction rules are complete, i.e., that you can derive an elimination rule for the
-alternative rules:%
+\noindent After declaring all alternative rules for the transitive
+ closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. As you have
+ declared alternative rules for the predicate, you are urged to prove
+ that these introduction rules are complete, i.e., that you can
+ derive an elimination rule for the alternative rules:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -290,7 +305,7 @@
\ \ \isacommand{case}\isamarkupfalse%
\ tranclp\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
\ thesis\ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isacommand{qed}\isamarkupfalse%
@@ -303,9 +318,9 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Alternative rules can also be used for constants that have not
-been defined inductively. For example, the lexicographic order which
-is defined as:%
+\noindent Alternative rules can also be used for constants that have
+ not been defined inductively. For example, the lexicographic order
+ which is defined as:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -333,24 +348,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent To make it executable, you can derive the following two rules and prove the
-elimination rule:%
+\noindent To make it executable, you can derive the following two
+ rules and prove the elimination rule:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
\isadelimquote
%
\endisadelimquote
@@ -372,47 +374,45 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Options for values%
+\isamarkupsubsection{Options for values%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In the presence of higher-order predicates, multiple modes for some predicate could be inferred
-that are not disambiguated by the pattern of the set comprehension.
-To disambiguate the modes for the arguments of a predicate, you can state
-the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.
-Consider the simple predicate \isa{succ}:%
+In the presence of higher-order predicates, multiple modes for some
+ predicate could be inferred that are not disambiguated by the
+ pattern of the set comprehension. To disambiguate the modes for the
+ arguments of a predicate, you can state the modes explicitly in the
+ \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. Consider the simple predicate \isa{succ}:%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
\isacommand{inductive}\isamarkupfalse%
-\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
+\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ succ%
-\isadelimproof
-\ %
-\endisadelimproof
+\ succ\ \isacommand{{\isachardot}}\isamarkupfalse%
%
-\isatagproof
-\isacommand{{\isachardot}}\isamarkupfalse%
+\endisatagquote
+{\isafoldquote}%
%
-\endisatagproof
-{\isafoldproof}%
+\isadelimquote
%
-\isadelimproof
-%
-\endisadelimproof
+\endisadelimquote
%
\begin{isamarkuptext}%
-\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 \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
-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
-modes for the 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, you can declare the mode for the argument between
-the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
+\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
+ \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. 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 modes for the
+ 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,
+ you can declare the mode for the argument between the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -432,41 +432,49 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
+\isamarkupsubsection{Embedding into functional code within Isabelle/HOL%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
-you have a number of options:
-\begin{itemize}
-\item You want to use the first-order predicate with the mode
- where all arguments are input. Then you can use the predicate directly, e.g.
-\begin{quote}
- \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
- \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
-\end{quote}
-\item If you know that the execution returns only one value (it is deterministic), then you can
- use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
- is defined with
-\begin{quote}
- \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
-\end{quote}
- Note that if the evaluation does not return a unique value, it raises a run-time error
- \isa{not{\isacharunderscore}unique}.
-\end{itemize}%
+To embed the computation of an inductive predicate into functions
+ that are defined in Isabelle/HOL, you have a number of options:
+
+ \begin{itemize}
+
+ \item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+
+ \begin{quote}
+ \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}} \\
+ \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
+ \end{quote}
+
+ \item If you know that the execution returns only one value (it is
+ deterministic), then you can use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists is
+ defined with
+
+ \begin{quote}
+ \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
+ \end{quote}
+
+ Note that if the evaluation does not return a unique value, it
+ raises a run-time error \isa{not{\isacharunderscore}unique}.
+
+ \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Further Examples%
+\isamarkupsubsection{Further Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Further examples for compiling inductive predicates can be found in
-the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
-There are also some examples in the Archive of Formal Proofs, notably
-in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
+ the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file. There are
+ also some examples in the Archive of Formal Proofs, notably in the
+ \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
+ sessions.%
\end{isamarkuptext}%
\isamarkuptrue%
%