--- a/src/Doc/Codegen/Inductive_Predicate.thy Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Thu Jan 15 13:39:41 2015 +0100
@@ -16,9 +16,9 @@
lexordp_def [unfolded lexord_def mem_Collect_eq split]
(*>*)
-section {* Inductive Predicates \label{sec:inductive} *}
+section \<open>Inductive Predicates \label{sec:inductive}\<close>
-text {*
+text \<open>
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
@@ -27,20 +27,20 @@
Consider the simple predicate @{const append} given by these two
introduction rules:
-*}
+\<close>
-text %quote {*
+text %quote \<open>
@{thm append.intros(1)[of ys]} \\
@{thm append.intros(2)[of xs ys zs x]}
-*}
+\<close>
-text {*
+text \<open>
\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
-*}
+\<close>
code_pred %quote append .
-text {*
+text \<open>
\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
@@ -56,55 +56,55 @@
\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
\end{itemize}
You can compute sets of predicates using @{command_def "values"}:
-*}
+\<close>
values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
-text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+text \<open>\noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and\<close>
values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
-text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+text \<open>\noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}.\<close>
-text {*
+text \<open>
\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:
-*}
+\<close>
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 {*
+text \<open>
\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:
-*}
+\<close>
thm %quote append.equation
-text {*
+text \<open>
\noindent More advanced options are described in the following subsections.
-*}
+\<close>
-subsection {* Alternative names for functions *}
+subsection \<open>Alternative names for functions\<close>
-text {*
+text \<open>
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:
-*}
+\<close>
code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
-subsection {* Alternative introduction rules *}
+subsection \<open>Alternative introduction rules\<close>
-text {*
+text \<open>
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
@@ -113,34 +113,34 @@
introduction rules for predicates with the attribute @{attribute
"code_pred_intro"}. For example, the transitive closure is defined
by:
-*}
+\<close>
-text %quote {*
+text %quote \<open>
@{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
@{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
-*}
+\<close>
-text {*
+text \<open>
\noindent These rules do not suit well for executing the transitive
closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
the second rule will cause an infinite loop in the recursive call.
This can be avoided using the following alternative rules which are
declared to the predicate compiler by the attribute @{attribute
"code_pred_intro"}:
-*}
+\<close>
lemma %quote [code_pred_intro]:
"r a b \<Longrightarrow> tranclp r a b"
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
by auto
-text {*
+text \<open>
\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:
-*}
+\<close>
code_pred %quote tranclp
proof -
@@ -148,20 +148,20 @@
from this converse_tranclpE [OF tranclp.prems] show thesis by metis
qed
-text {*
+text \<open>
\noindent Alternative rules can also be used for constants that have
not been defined inductively. For example, the lexicographic order
which is defined as:
-*}
+\<close>
-text %quote {*
+text %quote \<open>
@{thm [display] lexordp_def [of r]}
-*}
+\<close>
-text {*
+text \<open>
\noindent To make it executable, you can derive the following two
rules and prove the elimination rule:
-*}
+\<close>
lemma %quote [code_pred_intro]:
"append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
@@ -197,16 +197,16 @@
qed(*>*)
-subsection {* Options for values *}
+subsection \<open>Options for values\<close>
-text {*
+text \<open>
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"}:
-*}
+\<close>
inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 (Suc 0)"
@@ -214,7 +214,7 @@
code_pred %quote succ .
-text {*
+text \<open>
\noindent For this, the predicate compiler can infer modes @{text "o
\<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
@{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}
@@ -223,15 +223,15 @@
"o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
you can declare the mode for the argument between the @{command
"values"} and the number of elements.
-*}
+\<close>
values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
-subsection {* Embedding into functional code within Isabelle/HOL *}
+subsection \<open>Embedding into functional code within Isabelle/HOL\<close>
-text {*
+text \<open>
To embed the computation of an inductive predicate into functions
that are defined in Isabelle/HOL, you have a number of options:
@@ -258,18 +258,18 @@
raises a run-time error @{term "not_unique"}.
\end{itemize}
-*}
+\<close>
-subsection {* Further Examples *}
+subsection \<open>Further Examples\<close>
-text {*
+text \<open>
Further examples for compiling inductive predicates can be found in
@{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.
-*}
+\<close>
end