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