# HG changeset patch # User haftmann # Date 1277803530 -7200 # Node ID 1e99d8fc3d0716a4b4d29890027d429ea3fc4e4c # Parent ebc157ab01b09b3580650597a93672c2c2d5ed34# Parent d804c8b9c2dcc9723540f34b28a0b0d338b63952 merged diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Classes/Thy/document/Classes.tex Tue Jun 29 11:25:30 2010 +0200 @@ -1166,14 +1166,14 @@ \hspace*{0pt} ~inverse ::~a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ -\hspace*{0pt}inverse{\char95}int i = negate i;\\ +\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ +\hspace*{0pt}mult{\char95}int i j = i + j;\\ \hspace*{0pt}\\ \hspace*{0pt}neutral{\char95}int ::~Integer;\\ \hspace*{0pt}neutral{\char95}int = 0;\\ \hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ -\hspace*{0pt}mult{\char95}int i j = i + j;\\ +\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ +\hspace*{0pt}inverse{\char95}int i = negate i;\\ \hspace*{0pt}\\ \hspace*{0pt}instance Semigroup Integer where {\char123}\\ \hspace*{0pt} ~mult = mult{\char95}int;\\ @@ -1241,9 +1241,9 @@ \hspace*{0pt} ~type 'a group\\ \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\ \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\ -\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ +\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ -\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ +\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ \hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ @@ -1275,11 +1275,11 @@ \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\ \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ +\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ \hspace*{0pt}\\ \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ \hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ +\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ \hspace*{0pt}\\ \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ \hspace*{0pt}\\ diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/Inductive_Predicate.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Tue Jun 29 11:25:30 2010 +0200 @@ -0,0 +1,220 @@ +theory Inductive_Predicate +imports Setup +begin + +subsection {* Inductive Predicates *} +(*<*) +hide_const append + +inductive append +where + "append [] ys ys" +| "append xs ys zs ==> append (x # xs) ys (x # zs)" +(*>*) +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 . +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 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: +*} + +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 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: +*} +thm %quote append.equation +text {* +\noindent More advanced options are described in the following subsections. +*} +subsubsection {* 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: +*} +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 *} +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: +*} +text %quote {* +@{thm tranclp.intros(1)[of r a b]}\\ +\noindent @{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"}: +*} +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: +*} +code_pred %quote tranclp +proof - + case tranclp + 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"]} +*} +text {* +\noindent To make it executable, you can derive the following two rules and prove the +elimination rule: +*} +(*<*) +lemma append: "append xs ys zs = (xs @ ys = zs)" +by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) +(*>*) +lemma %quote [code_pred_intro]: + "append xs (a # v) ys \ lexord r (xs, ys)" +(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) + +lemma %quote [code_pred_intro]: + "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 +(*>*) + +code_pred %quote lexord +(*<*) +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" + assume 2: "\ r' xs' ys' u a v b w. r = r' \ (xs, ys) = (xs', ys') \ append u (a # v) xs' \ append u (b # w) ys' \ r' (a, b) \ thesis" + { + assume "\a v. ys = xs @ a # v" + from this 1 have thesis + by (fastsimp simp add: append) + } moreover + { + assume "\u a b v w. (a, b) \ r \ xs = u @ a # v \ ys = u @ b # w" + from this 2 have thesis by (fastsimp simp add: append mem_def) + } moreover + note lexord + ultimately show thesis + unfolding lexord_def + by (fastsimp simp add: Collect_def) +qed +(*>*) +subsubsection {* 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"}: +*} +inductive succ :: "nat \ nat \ bool" +where + "succ 0 (Suc 0)" +| "succ x y \ succ (Suc x) (Suc y)" + +code_pred 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. +*} +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 *} +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} +*} +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. +*} +end diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/ML.thy Tue Jun 29 11:25:30 2010 +0200 @@ -31,7 +31,7 @@ @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ @{index_ML Code.get_type: "theory -> string - -> (string * sort) list * (string * typ list) list"} \\ + -> (string * sort) list * ((string * string list) * typ list) list"} \\ @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} \end{mldecls} diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/Program.thy --- a/doc-src/Codegen/Thy/Program.thy Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/Program.thy Tue Jun 29 11:25:30 2010 +0200 @@ -174,7 +174,7 @@ *} lemma %quote [code_unfold]: - "x \ set xs \ member xs x" by (fact in_set_code) + "x \ set xs \ List.member xs x" by (fact in_set_member) text {* \item eliminating superfluous constants: @@ -188,7 +188,7 @@ *} lemma %quote [code_unfold]: - "xs = [] \ List.null xs" by (fact empty_null) + "xs = [] \ List.null xs" by (fact eq_Nil_null) text_raw {* \end{itemize} @@ -339,7 +339,7 @@ else collect_duplicates (z#xs) (z#ys) zs)" text {* - \noindent The membership test during preprocessing is rewritten, + \noindent During preprocessing, the membership test is rewritten, resulting in @{const List.member}, which itself performs an explicit equality check. *} @@ -429,219 +429,4 @@ likely to be used in such situations. *} -subsection {* Inductive Predicates *} -(*<*) -hide_const append - -inductive append -where - "append [] ys ys" -| "append xs ys zs ==> append (x # xs) ys (x # zs)" -(*>*) -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 . -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 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: -*} - -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 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: -*} -thm %quote append.equation -text {* -\noindent More advanced options are described in the following subsections. -*} -subsubsection {* 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: -*} -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 *} -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: -*} -text %quote {* -@{thm tranclp.intros(1)[of r a b]}\\ -\noindent @{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"}: -*} -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: -*} -code_pred %quote tranclp -proof - - case tranclp - 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"]} -*} -text {* -\noindent To make it executable, you can derive the following two rules and prove the -elimination rule: -*} -(*<*) -lemma append: "append xs ys zs = (xs @ ys = zs)" -by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) -(*>*) -lemma %quote [code_pred_intro]: - "append xs (a # v) ys \ lexord r (xs, ys)" -(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*) - -lemma %quote [code_pred_intro]: - "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 -(*>*) - -code_pred %quote lexord -(*<*) -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" - assume 2: "\ r' xs' ys' u a v b w. r = r' \ (xs, ys) = (xs', ys') \ append u (a # v) xs' \ append u (b # w) ys' \ r' (a, b) \ thesis" - { - assume "\a v. ys = xs @ a # v" - from this 1 have thesis - by (fastsimp simp add: append) - } moreover - { - assume "\u a b v w. (a, b) \ r \ xs = u @ a # v \ ys = u @ b # w" - from this 2 have thesis by (fastsimp simp add: append mem_def) - } moreover - note lexord - ultimately show thesis - unfolding lexord_def - by (fastsimp simp add: Collect_def) -qed -(*>*) -subsubsection {* 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"}: -*} -inductive succ :: "nat \ nat \ bool" -where - "succ 0 (Suc 0)" -| "succ x y \ succ (Suc x) (Suc y)" - -code_pred 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. -*} -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 *} -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} -*} -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. -*} end diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/ROOT.ML --- a/doc-src/Codegen/Thy/ROOT.ML Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/ROOT.ML Tue Jun 29 11:25:30 2010 +0200 @@ -4,6 +4,7 @@ use_thy "Introduction"; use_thy "Program"; +use_thy "Inductive_Predicate"; use_thy "Adaptation"; use_thy "Further"; use_thy "ML"; diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Tue Jun 29 11:25:30 2010 +0200 @@ -0,0 +1,491 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Inductive{\isacharunderscore}Predicate}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Inductive{\isacharunderscore}Predicate\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsubsection{Inductive Predicates% +} +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\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}}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ append\ \isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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. + +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% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% +\end{isamarkuptext}% +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\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 +\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}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{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 \isa{equation}, and can be inspected with:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{thm}\isamarkupfalse% +\ append{\isachardot}equation% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent More advanced options are described in the following subsections.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline +\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline +\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline +\isacommand{by}\isamarkupfalse% +\ auto% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ tranclp\isanewline +\isacommand{proof}\isamarkupfalse% +\ {\isacharminus}\isanewline +\ \ \isacommand{case}\isamarkupfalse% +\ tranclp\isanewline +\ \ \isacommand{from}\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% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\begin{isabelle}% +lexord\ r\ {\isacharequal}\isanewline +{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline +\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline +\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}% +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\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 +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline +\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% +\ lexord% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{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}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive}\isamarkupfalse% +\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\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 +% +\isatagproof +\isacommand{{\isachardot}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{values}\isamarkupfalse% +\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\isacommand{values}\isamarkupfalse% +\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsubsection{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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 29 11:25:30 2010 +0200 @@ -149,7 +149,6 @@ \hspace*{0pt}structure Example :~sig\\ \hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ \hspace*{0pt} ~val rev :~'a list -> 'a list\\ -\hspace*{0pt} ~val list{\char95}case :~'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a\\ \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ \hspace*{0pt} ~val empty :~'a queue\\ \hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ @@ -161,9 +160,6 @@ \hspace*{0pt}\\ \hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\ -\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ \hspace*{0pt}\\ \hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ @@ -234,10 +230,6 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\ -\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ -\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ \hspace*{0pt}data Queue a = AQueue [a] [a];\\ \hspace*{0pt}\\ \hspace*{0pt}empty ::~forall a.~Queue a;\\ @@ -248,7 +240,7 @@ \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ \hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ +\hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ \hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ \hspace*{0pt}\\ \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/document/ML.tex Tue Jun 29 11:25:30 2010 +0200 @@ -61,7 +61,7 @@ \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% -\verb| -> (string * sort) list * (string * typ list) list| \\ +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| \end{mldecls} diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jun 29 11:25:30 2010 +0200 @@ -89,8 +89,8 @@ \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ \hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));% +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -292,13 +292,13 @@ \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ \hspace*{0pt}instance Semigroup Nat where {\char123}\\ \hspace*{0pt} ~mult = mult{\char95}nat;\\ \hspace*{0pt}{\char125};\\ @@ -346,8 +346,8 @@ \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ \hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ \hspace*{0pt} ~val bexp :~nat -> nat\\ @@ -368,11 +368,11 @@ \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ \hspace*{0pt}\\ \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ @@ -434,8 +434,8 @@ \isatagquote \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}% +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% \endisatagquote {\isafoldquote}% % @@ -477,7 +477,7 @@ \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}% +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% \endisatagquote {\isafoldquote}% % @@ -763,8 +763,8 @@ \endisadelimquote % \begin{isamarkuptext}% -\noindent The membership test during preprocessing is rewritten, - resulting in \isa{member}, which itself +\noindent During preprocessing, the membership test is rewritten, + resulting in \isa{List{\isachardot}member}, which itself performs an explicit equality check.% \end{isamarkuptext}% \isamarkuptrue% @@ -878,7 +878,7 @@ \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ \hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = rev xs;\\ +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% \end{isamarkuptext}% @@ -972,7 +972,8 @@ \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));% +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -991,458 +992,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Inductive Predicates% -} -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\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}}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ append\ \isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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. - -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% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.% -\end{isamarkuptext}% -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\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 -\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}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{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 \isa{equation}, and can be inspected with:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{thm}\isamarkupfalse% -\ append{\isachardot}equation% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent More advanced options are described in the following subsections.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline -\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline -\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\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}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline -\isacommand{by}\isamarkupfalse% -\ auto% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ tranclp\isanewline -\isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ tranclp\isanewline -\ \ \isacommand{from}\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% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\begin{isabelle}% -lexord\ r\ {\isacharequal}\isanewline -{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline -\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline -\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}% -\end{isabelle}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\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 -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline -\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{code{\isacharunderscore}pred}\isamarkupfalse% -\ lexord% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{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}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{inductive}\isamarkupfalse% -\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline -\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 -% -\isatagproof -\isacommand{{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\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.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline -\isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\isamarkupsubsubsection{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}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{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.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isadelimtheory % \endisadelimtheory diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 29 11:25:30 2010 +0200 @@ -2,10 +2,6 @@ module Example where { -list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a; -list_case f1 f2 (a : list) = f2 a list; -list_case f1 f2 [] = f1; - data Queue a = AQueue [a] [a]; empty :: forall a. Queue a; @@ -16,7 +12,7 @@ dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys); dequeue (AQueue (v : va) []) = let { - (y : ys) = rev (v : va); + (y : ys) = reverse (v : va); } in (Just y, AQueue [] ys); enqueue :: forall a. a -> Queue a -> Queue a; diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/Thy/examples/example.ML --- a/doc-src/Codegen/Thy/examples/example.ML Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/Thy/examples/example.ML Tue Jun 29 11:25:30 2010 +0200 @@ -1,7 +1,6 @@ structure Example : sig val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a val rev : 'a list -> 'a list - val list_case : 'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a datatype 'a queue = AQueue of 'a list * 'a list val empty : 'a queue val dequeue : 'a queue -> 'a option * 'a queue @@ -13,9 +12,6 @@ fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs; -fun list_case f1 f2 (a :: lista) = f2 a lista - | list_case f1 f2 [] = f1; - datatype 'a queue = AQueue of 'a list * 'a list; val empty : 'a queue = AQueue ([], []); diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/Codegen/codegen.tex --- a/doc-src/Codegen/codegen.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/Codegen/codegen.tex Tue Jun 29 11:25:30 2010 +0200 @@ -32,6 +32,7 @@ \input{Thy/document/Introduction.tex} \input{Thy/document/Program.tex} +\input{Thy/document/Inductive_Predicate.tex} \input{Thy/document/Adaptation.tex} \input{Thy/document/Further.tex} \input{Thy/document/ML.tex} diff -r ebc157ab01b0 -r 1e99d8fc3d07 doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 29 09:37:23 2010 +0100 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 29 11:25:30 2010 +0200 @@ -60,7 +60,7 @@ Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as \begin{center} -\isa{split\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}} +\isa{prod{\isacharunderscore}case\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}} \hfill(\isa{split{\isacharunderscore}def}) \end{center} Pattern matching in @@ -74,7 +74,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The most obvious approach is the brute force expansion of \isa{split}:% +The most obvious approach is the brute force expansion of \isa{prod{\isacharunderscore}case}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -105,10 +105,10 @@ If we consider why this lemma presents a problem, we realize that we need to replace variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the equation would simplify to \isa{a} by the simplification rules -\isa{split\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. +\isa{prod{\isacharunderscore}case\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. To reason about tuple patterns requires some way of converting a variable of product type into a pair. -In case of a subterm of the form \isa{split\ f\ p} this is easy: the split +In case of a subterm of the form \isa{prod{\isacharunderscore}case\ f\ p} this is easy: the split rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% \index{*split (method)}% \end{isamarkuptext}% @@ -169,7 +169,7 @@ {\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p% +\ {\isadigit{1}}{\isachardot}\ case\ p\ of\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymRightarrow}\ fst\ p\ {\isacharequal}\ x% \end{isabelle} A paired \isa{let} reduces to a paired $\lambda$-abstraction, which can be split as above. The same is true for paired set comprehension:% @@ -194,7 +194,7 @@ \ simp% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% +\ {\isadigit{1}}{\isachardot}\ prod{\isacharunderscore}case\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% \end{isabelle} Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} as above. If you are worried about the strange form of the premise: @@ -220,9 +220,9 @@ \begin{isamarkuptxt}% \noindent except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because -\isa{split} occurs in the assumptions. +\isa{prod{\isacharunderscore}case} occurs in the assumptions. -However, splitting \isa{split} is not always a solution, as no \isa{split} +However, splitting \isa{prod{\isacharunderscore}case} is not always a solution, as no \isa{prod{\isacharunderscore}case} may be present in the goal. Consider the following function:% \end{isamarkuptxt}% \isamarkuptrue% @@ -253,7 +253,7 @@ \noindent simplification will do nothing, because the defining equation for \isa{swap} expects a pair. Again, we need to turn \isa{p} -into a pair first, but this time there is no \isa{split} in sight. +into a pair first, but this time there is no \isa{prod{\isacharunderscore}case} in sight. The only thing we can do is to split the term by hand:% \end{isamarkuptxt}% \isamarkuptrue%