# HG changeset patch # User haftmann # Date 1281950308 -7200 # Node ID 2fffd5ac487fc134f9e44539d9e6484b84ec0521 # Parent 6c0d02f416ba0863c09dd138119cdfcbbc7e705c tuned section on predicate compiler diff -r 6c0d02f416ba -r 2fffd5ac487f doc-src/Codegen/IsaMakefile --- 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 diff -r 6c0d02f416ba -r 2fffd5ac487f doc-src/Codegen/Thy/Inductive_Predicate.thy --- 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 \ i \ i \ bool"} -\item @{text "i \ i \ o \ bool"} -\item @{text "o \ o \ i \ 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 \ i \ i \ bool"} + \item @{text "i \ i \ o \ bool"} + \item @{text "o \ o \ i \ 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 \ o \ bool) \ i \ o \ 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 \ o \ bool) \ i \ o \ 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 \ r\<^sup>+\<^sup>+ a b" "r a b \ r\<^sup>+\<^sup>+ b c \ 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 \ lexord r (xs, ys)" (*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) @@ -139,12 +168,10 @@ "append u (a # v) xs \ append u (b # w) ys \ r (a, b) \ 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: "\ r' xs' ys' a v. r = r' \ (xs, ys) = (xs', ys') \ append xs' (a # v) ys' \ 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 \ nat \ bool" -where + +inductive %quote succ :: "nat \ nat \ bool" where "succ 0 (Suc 0)" | "succ x y \ succ (Suc x) (Suc y)" -code_pred succ . +code_pred %quote succ . text {* -\noindent For this, the predicate compiler can infer modes @{text "o \ o \ bool"}, @{text "i \ o \ bool"}, - @{text "o \ i \ bool"} and @{text "i \ i \ 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 \ o \ 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 + \ o \ bool"}, @{text "i \ o \ bool"}, @{text "o \ i \ bool"} and + @{text "i \ i \ 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 \ o \ 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 diff -r 6c0d02f416ba -r 2fffd5ac487f doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- 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% %