author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
child 72172 | 6f20a44c3cb1 |
permissions | -rw-r--r-- |
37613 | 1 |
theory Inductive_Predicate |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
66453
diff
changeset
|
2 |
imports Setup |
37613 | 3 |
begin |
4 |
||
5 |
(*<*) |
|
38441 | 6 |
hide_const %invisible append |
37613 | 7 |
|
38441 | 8 |
inductive %invisible append where |
37613 | 9 |
"append [] ys ys" |
38811 | 10 |
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" |
38441 | 11 |
|
12 |
lemma %invisible append: "append xs ys zs = (xs @ ys = zs)" |
|
13 |
by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros) |
|
46515 | 14 |
|
15 |
lemmas lexordp_def = |
|
16 |
lexordp_def [unfolded lexord_def mem_Collect_eq split] |
|
37613 | 17 |
(*>*) |
38441 | 18 |
|
59377 | 19 |
section \<open>Inductive Predicates \label{sec:inductive}\<close> |
38441 | 20 |
|
59377 | 21 |
text \<open> |
69505 | 22 |
The \<open>predicate compiler\<close> is an extension of the code generator |
38441 | 23 |
which turns inductive specifications into equational ones, from |
24 |
which in turn executable code can be generated. The mechanisms of |
|
25 |
this compiler are described in detail in |
|
58620 | 26 |
@{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}. |
38441 | 27 |
|
69597 | 28 |
Consider the simple predicate \<^const>\<open>append\<close> given by these two |
38441 | 29 |
introduction rules: |
59377 | 30 |
\<close> |
38441 | 31 |
|
59377 | 32 |
text %quote \<open> |
38441 | 33 |
@{thm append.intros(1)[of ys]} \\ |
34 |
@{thm append.intros(2)[of xs ys zs x]} |
|
59377 | 35 |
\<close> |
38441 | 36 |
|
59377 | 37 |
text \<open> |
38441 | 38 |
\noindent To invoke the compiler, simply use @{command_def "code_pred"}: |
59377 | 39 |
\<close> |
37613 | 40 |
|
38441 | 41 |
code_pred %quote append . |
42 |
||
59377 | 43 |
text \<open> |
38441 | 44 |
\noindent The @{command "code_pred"} command takes the name of the |
45 |
inductive predicate and then you put a period to discharge a trivial |
|
46 |
correctness proof. The compiler infers possible modes for the |
|
47 |
predicate and produces the derived code equations. Modes annotate |
|
48 |
which (parts of the) arguments are to be taken as input, and which |
|
69505 | 49 |
output. Modes are similar to types, but use the notation \<open>i\<close> |
50 |
for input and \<open>o\<close> for output. |
|
38441 | 51 |
|
69597 | 52 |
For \<^term>\<open>append\<close>, the compiler can infer the following modes: |
38441 | 53 |
\begin{itemize} |
69505 | 54 |
\item \<open>i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool\<close> |
55 |
\item \<open>i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool\<close> |
|
56 |
\item \<open>o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool\<close> |
|
38441 | 57 |
\end{itemize} |
58 |
You can compute sets of predicates using @{command_def "values"}: |
|
59377 | 59 |
\<close> |
38441 | 60 |
|
61 |
values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" |
|
62 |
||
69505 | 63 |
text \<open>\noindent outputs \<open>{[1, 2, 3, 4, 5]}\<close>, and\<close> |
38441 | 64 |
|
65 |
values %quote "{(xs, ys). append xs ys [(2::nat),3]}" |
|
66 |
||
69505 | 67 |
text \<open>\noindent outputs \<open>{([], [2, 3]), ([2], [3]), ([2, 3], [])}\<close>.\<close> |
37613 | 68 |
|
59377 | 69 |
text \<open> |
38441 | 70 |
\noindent If you are only interested in the first elements of the |
71 |
set comprehension (with respect to a depth-first search on the |
|
72 |
introduction rules), you can pass an argument to @{command "values"} |
|
73 |
to specify the number of elements you want: |
|
59377 | 74 |
\<close> |
37613 | 75 |
|
38441 | 76 |
values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}" |
77 |
values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}" |
|
78 |
||
59377 | 79 |
text \<open> |
38441 | 80 |
\noindent The @{command "values"} command can only compute set |
81 |
comprehensions for which a mode has been inferred. |
|
82 |
||
83 |
The code equations for a predicate are made available as theorems with |
|
69505 | 84 |
the suffix \<open>equation\<close>, and can be inspected with: |
59377 | 85 |
\<close> |
38441 | 86 |
|
87 |
thm %quote append.equation |
|
88 |
||
59377 | 89 |
text \<open> |
38441 | 90 |
\noindent More advanced options are described in the following subsections. |
59377 | 91 |
\<close> |
38441 | 92 |
|
59377 | 93 |
subsection \<open>Alternative names for functions\<close> |
38441 | 94 |
|
59377 | 95 |
text \<open> |
38441 | 96 |
By default, the functions generated from a predicate are named after |
69505 | 97 |
the predicate with the mode mangled into the name (e.g., \<open>append_i_i_o\<close>). You can specify your own names as follows: |
59377 | 98 |
\<close> |
38441 | 99 |
|
38811 | 100 |
code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat, |
101 |
o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split, |
|
102 |
i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append . |
|
37613 | 103 |
|
59377 | 104 |
subsection \<open>Alternative introduction rules\<close> |
38441 | 105 |
|
59377 | 106 |
text \<open> |
38441 | 107 |
Sometimes the introduction rules of an predicate are not executable |
108 |
because they contain non-executable constants or specific modes |
|
109 |
could not be inferred. It is also possible that the introduction |
|
110 |
rules yield a function that loops forever due to the execution in a |
|
111 |
depth-first search manner. Therefore, you can declare alternative |
|
112 |
introduction rules for predicates with the attribute @{attribute |
|
113 |
"code_pred_intro"}. For example, the transitive closure is defined |
|
114 |
by: |
|
59377 | 115 |
\<close> |
38441 | 116 |
|
59377 | 117 |
text %quote \<open> |
39682
066e2d4d0de8
avoid fragile tranclp syntax; corrected resolution; corrected typo
haftmann
parents:
39065
diff
changeset
|
118 |
@{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\ |
066e2d4d0de8
avoid fragile tranclp syntax; corrected resolution; corrected typo
haftmann
parents:
39065
diff
changeset
|
119 |
@{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))} |
59377 | 120 |
\<close> |
38441 | 121 |
|
59377 | 122 |
text \<open> |
38441 | 123 |
\noindent These rules do not suit well for executing the transitive |
69505 | 124 |
closure with the mode \<open>(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool\<close>, as |
38441 | 125 |
the second rule will cause an infinite loop in the recursive call. |
126 |
This can be avoided using the following alternative rules which are |
|
127 |
declared to the predicate compiler by the attribute @{attribute |
|
128 |
"code_pred_intro"}: |
|
59377 | 129 |
\<close> |
38441 | 130 |
|
37613 | 131 |
lemma %quote [code_pred_intro]: |
39682
066e2d4d0de8
avoid fragile tranclp syntax; corrected resolution; corrected typo
haftmann
parents:
39065
diff
changeset
|
132 |
"r a b \<Longrightarrow> tranclp r a b" |
066e2d4d0de8
avoid fragile tranclp syntax; corrected resolution; corrected typo
haftmann
parents:
39065
diff
changeset
|
133 |
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
37613 | 134 |
by auto |
38441 | 135 |
|
59377 | 136 |
text \<open> |
38441 | 137 |
\noindent After declaring all alternative rules for the transitive |
138 |
closure, you invoke @{command "code_pred"} as usual. As you have |
|
139 |
declared alternative rules for the predicate, you are urged to prove |
|
140 |
that these introduction rules are complete, i.e., that you can |
|
141 |
derive an elimination rule for the alternative rules: |
|
59377 | 142 |
\<close> |
38441 | 143 |
|
37613 | 144 |
code_pred %quote tranclp |
145 |
proof - |
|
146 |
case tranclp |
|
39682
066e2d4d0de8
avoid fragile tranclp syntax; corrected resolution; corrected typo
haftmann
parents:
39065
diff
changeset
|
147 |
from this converse_tranclpE [OF tranclp.prems] show thesis by metis |
37613 | 148 |
qed |
38441 | 149 |
|
59377 | 150 |
text \<open> |
38441 | 151 |
\noindent Alternative rules can also be used for constants that have |
152 |
not been defined inductively. For example, the lexicographic order |
|
153 |
which is defined as: |
|
59377 | 154 |
\<close> |
38441 | 155 |
|
59377 | 156 |
text %quote \<open> |
46515 | 157 |
@{thm [display] lexordp_def [of r]} |
59377 | 158 |
\<close> |
38441 | 159 |
|
59377 | 160 |
text \<open> |
38441 | 161 |
\noindent To make it executable, you can derive the following two |
162 |
rules and prove the elimination rule: |
|
59377 | 163 |
\<close> |
38441 | 164 |
|
37613 | 165 |
lemma %quote [code_pred_intro]: |
46515 | 166 |
"append xs (a # v) ys \<Longrightarrow> lexordp r xs ys" |
167 |
(*<*)unfolding lexordp_def by (auto simp add: append)(*>*) |
|
37613 | 168 |
|
169 |
lemma %quote [code_pred_intro]: |
|
46515 | 170 |
"append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b |
171 |
\<Longrightarrow> lexordp r xs ys" |
|
172 |
(*<*)unfolding lexordp_def append apply simp |
|
38441 | 173 |
apply (rule disjI2) by auto(*>*) |
37613 | 174 |
|
46515 | 175 |
code_pred %quote lexordp |
38441 | 176 |
(*<*)proof - |
37613 | 177 |
fix r xs ys |
46515 | 178 |
assume lexord: "lexordp r xs ys" |
179 |
assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
|
180 |
\<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis" |
|
181 |
assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys' |
|
182 |
\<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis" |
|
37613 | 183 |
{ |
184 |
assume "\<exists>a v. ys = xs @ a # v" |
|
185 |
from this 1 have thesis |
|
46515 | 186 |
by (fastforce simp add: append) |
37613 | 187 |
} moreover |
188 |
{ |
|
46515 | 189 |
assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w" |
190 |
from this 2 have thesis by (fastforce simp add: append) |
|
37613 | 191 |
} moreover |
192 |
note lexord |
|
193 |
ultimately show thesis |
|
46515 | 194 |
unfolding lexordp_def |
195 |
by fastforce |
|
38441 | 196 |
qed(*>*) |
197 |
||
198 |
||
59377 | 199 |
subsection \<open>Options for values\<close> |
38441 | 200 |
|
59377 | 201 |
text \<open> |
38441 | 202 |
In the presence of higher-order predicates, multiple modes for some |
203 |
predicate could be inferred that are not disambiguated by the |
|
204 |
pattern of the set comprehension. To disambiguate the modes for the |
|
205 |
arguments of a predicate, you can state the modes explicitly in the |
|
69597 | 206 |
@{command "values"} command. Consider the simple predicate \<^term>\<open>succ\<close>: |
59377 | 207 |
\<close> |
38441 | 208 |
|
209 |
inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
37613 | 210 |
"succ 0 (Suc 0)" |
211 |
| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)" |
|
212 |
||
38441 | 213 |
code_pred %quote succ . |
37613 | 214 |
|
59377 | 215 |
text \<open> |
69505 | 216 |
\noindent For this, the predicate compiler can infer modes \<open>o |
217 |
\<Rightarrow> o \<Rightarrow> bool\<close>, \<open>i \<Rightarrow> o \<Rightarrow> bool\<close>, \<open>o \<Rightarrow> i \<Rightarrow> bool\<close> and |
|
218 |
\<open>i \<Rightarrow> i \<Rightarrow> bool\<close>. The invocation of @{command "values"} |
|
219 |
\<open>{n. tranclp succ 10 n}\<close> loops, as multiple modes for the |
|
220 |
predicate \<open>succ\<close> are possible and here the first mode \<open>o \<Rightarrow> o \<Rightarrow> bool\<close> is chosen. To choose another mode for the argument, |
|
38441 | 221 |
you can declare the mode for the argument between the @{command |
222 |
"values"} and the number of elements. |
|
59377 | 223 |
\<close> |
38441 | 224 |
|
61498 | 225 |
values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIXME does not terminate for n\<ge>1*) |
39065 | 226 |
values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}" |
37613 | 227 |
|
38441 | 228 |
|
59377 | 229 |
subsection \<open>Embedding into functional code within Isabelle/HOL\<close> |
38441 | 230 |
|
59377 | 231 |
text \<open> |
38441 | 232 |
To embed the computation of an inductive predicate into functions |
233 |
that are defined in Isabelle/HOL, you have a number of options: |
|
234 |
||
235 |
\begin{itemize} |
|
236 |
||
61498 | 237 |
\item You want to use the first-order predicate with the mode |
238 |
where all arguments are input. Then you can use the predicate directly, e.g. |
|
38441 | 239 |
|
61498 | 240 |
@{text [display] |
241 |
\<open>valid_suffix ys zs = |
|
242 |
(if append [Suc 0, 2] ys zs then Some ys else None)\<close>} |
|
38441 | 243 |
|
61498 | 244 |
\item If you know that the execution returns only one value (it is |
69597 | 245 |
deterministic), then you can use the combinator \<^term>\<open>Predicate.the\<close>, e.g., a functional concatenation of lists is |
61498 | 246 |
defined with |
38441 | 247 |
|
61498 | 248 |
@{term [display] "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"} |
38441 | 249 |
|
61498 | 250 |
Note that if the evaluation does not return a unique value, it |
69597 | 251 |
raises a run-time error \<^term>\<open>not_unique\<close>. |
38441 | 252 |
|
253 |
\end{itemize} |
|
59377 | 254 |
\<close> |
38441 | 255 |
|
256 |
||
59377 | 257 |
subsection \<open>Further Examples\<close> |
38441 | 258 |
|
59377 | 259 |
text \<open> |
38441 | 260 |
Further examples for compiling inductive predicates can be found in |
63680 | 261 |
\<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>. There are |
38441 | 262 |
also some examples in the Archive of Formal Proofs, notably in the |
69505 | 263 |
\<open>POPLmark-deBruijn\<close> and the \<open>FeatherweightJava\<close> |
38441 | 264 |
sessions. |
59377 | 265 |
\<close> |
38441 | 266 |
|
37613 | 267 |
end |
46515 | 268 |