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