14 |
14 |
15 lemmas lexordp_def = |
15 lemmas lexordp_def = |
16 lexordp_def [unfolded lexord_def mem_Collect_eq split] |
16 lexordp_def [unfolded lexord_def mem_Collect_eq split] |
17 (*>*) |
17 (*>*) |
18 |
18 |
19 section {* Inductive Predicates \label{sec:inductive} *} |
19 section \<open>Inductive Predicates \label{sec:inductive}\<close> |
20 |
20 |
21 text {* |
21 text \<open> |
22 The @{text "predicate compiler"} is an extension of the code generator |
22 The @{text "predicate compiler"} is an extension of the code generator |
23 which turns inductive specifications into equational ones, from |
23 which turns inductive specifications into equational ones, from |
24 which in turn executable code can be generated. The mechanisms of |
24 which in turn executable code can be generated. The mechanisms of |
25 this compiler are described in detail in |
25 this compiler are described in detail in |
26 @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}. |
26 @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}. |
27 |
27 |
28 Consider the simple predicate @{const append} given by these two |
28 Consider the simple predicate @{const append} given by these two |
29 introduction rules: |
29 introduction rules: |
30 *} |
30 \<close> |
31 |
31 |
32 text %quote {* |
32 text %quote \<open> |
33 @{thm append.intros(1)[of ys]} \\ |
33 @{thm append.intros(1)[of ys]} \\ |
34 @{thm append.intros(2)[of xs ys zs x]} |
34 @{thm append.intros(2)[of xs ys zs x]} |
35 *} |
35 \<close> |
36 |
36 |
37 text {* |
37 text \<open> |
38 \noindent To invoke the compiler, simply use @{command_def "code_pred"}: |
38 \noindent To invoke the compiler, simply use @{command_def "code_pred"}: |
39 *} |
39 \<close> |
40 |
40 |
41 code_pred %quote append . |
41 code_pred %quote append . |
42 |
42 |
43 text {* |
43 text \<open> |
44 \noindent The @{command "code_pred"} command takes the name of the |
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 |
45 inductive predicate and then you put a period to discharge a trivial |
46 correctness proof. The compiler infers possible modes for the |
46 correctness proof. The compiler infers possible modes for the |
47 predicate and produces the derived code equations. Modes annotate |
47 predicate and produces the derived code equations. Modes annotate |
48 which (parts of the) arguments are to be taken as input, and which |
48 which (parts of the) arguments are to be taken as input, and which |
54 \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"} |
54 \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"} |
55 \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"} |
55 \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"} |
56 \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"} |
56 \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"} |
57 \end{itemize} |
57 \end{itemize} |
58 You can compute sets of predicates using @{command_def "values"}: |
58 You can compute sets of predicates using @{command_def "values"}: |
59 *} |
59 \<close> |
60 |
60 |
61 values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" |
61 values %quote "{zs. append [(1::nat),2,3] [4,5] zs}" |
62 |
62 |
63 text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *} |
63 text \<open>\noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and\<close> |
64 |
64 |
65 values %quote "{(xs, ys). append xs ys [(2::nat),3]}" |
65 values %quote "{(xs, ys). append xs ys [(2::nat),3]}" |
66 |
66 |
67 text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *} |
67 text \<open>\noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}.\<close> |
68 |
68 |
69 text {* |
69 text \<open> |
70 \noindent If you are only interested in the first elements of the |
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 |
71 set comprehension (with respect to a depth-first search on the |
72 introduction rules), you can pass an argument to @{command "values"} |
72 introduction rules), you can pass an argument to @{command "values"} |
73 to specify the number of elements you want: |
73 to specify the number of elements you want: |
74 *} |
74 \<close> |
75 |
75 |
76 values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}" |
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]}" |
77 values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}" |
78 |
78 |
79 text {* |
79 text \<open> |
80 \noindent The @{command "values"} command can only compute set |
80 \noindent The @{command "values"} command can only compute set |
81 comprehensions for which a mode has been inferred. |
81 comprehensions for which a mode has been inferred. |
82 |
82 |
83 The code equations for a predicate are made available as theorems with |
83 The code equations for a predicate are made available as theorems with |
84 the suffix @{text "equation"}, and can be inspected with: |
84 the suffix @{text "equation"}, and can be inspected with: |
85 *} |
85 \<close> |
86 |
86 |
87 thm %quote append.equation |
87 thm %quote append.equation |
88 |
88 |
89 text {* |
89 text \<open> |
90 \noindent More advanced options are described in the following subsections. |
90 \noindent More advanced options are described in the following subsections. |
91 *} |
91 \<close> |
92 |
92 |
93 subsection {* Alternative names for functions *} |
93 subsection \<open>Alternative names for functions\<close> |
94 |
94 |
95 text {* |
95 text \<open> |
96 By default, the functions generated from a predicate are named after |
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 |
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: |
98 "append_i_i_o"}). You can specify your own names as follows: |
99 *} |
99 \<close> |
100 |
100 |
101 code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat, |
101 code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat, |
102 o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split, |
102 o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split, |
103 i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append . |
103 i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append . |
104 |
104 |
105 subsection {* Alternative introduction rules *} |
105 subsection \<open>Alternative introduction rules\<close> |
106 |
106 |
107 text {* |
107 text \<open> |
108 Sometimes the introduction rules of an predicate are not executable |
108 Sometimes the introduction rules of an predicate are not executable |
109 because they contain non-executable constants or specific modes |
109 because they contain non-executable constants or specific modes |
110 could not be inferred. It is also possible that the introduction |
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 |
111 rules yield a function that loops forever due to the execution in a |
112 depth-first search manner. Therefore, you can declare alternative |
112 depth-first search manner. Therefore, you can declare alternative |
113 introduction rules for predicates with the attribute @{attribute |
113 introduction rules for predicates with the attribute @{attribute |
114 "code_pred_intro"}. For example, the transitive closure is defined |
114 "code_pred_intro"}. For example, the transitive closure is defined |
115 by: |
115 by: |
116 *} |
116 \<close> |
117 |
117 |
118 text %quote {* |
118 text %quote \<open> |
119 @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\ |
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))} |
120 @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))} |
121 *} |
121 \<close> |
122 |
122 |
123 text {* |
123 text \<open> |
124 \noindent These rules do not suit well for executing the transitive |
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 |
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. |
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 |
127 This can be avoided using the following alternative rules which are |
128 declared to the predicate compiler by the attribute @{attribute |
128 declared to the predicate compiler by the attribute @{attribute |
129 "code_pred_intro"}: |
129 "code_pred_intro"}: |
130 *} |
130 \<close> |
131 |
131 |
132 lemma %quote [code_pred_intro]: |
132 lemma %quote [code_pred_intro]: |
133 "r a b \<Longrightarrow> tranclp r a b" |
133 "r a b \<Longrightarrow> tranclp r a b" |
134 "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
134 "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
135 by auto |
135 by auto |
136 |
136 |
137 text {* |
137 text \<open> |
138 \noindent After declaring all alternative rules for the transitive |
138 \noindent After declaring all alternative rules for the transitive |
139 closure, you invoke @{command "code_pred"} as usual. As you have |
139 closure, you invoke @{command "code_pred"} as usual. As you have |
140 declared alternative rules for the predicate, you are urged to prove |
140 declared alternative rules for the predicate, you are urged to prove |
141 that these introduction rules are complete, i.e., that you can |
141 that these introduction rules are complete, i.e., that you can |
142 derive an elimination rule for the alternative rules: |
142 derive an elimination rule for the alternative rules: |
143 *} |
143 \<close> |
144 |
144 |
145 code_pred %quote tranclp |
145 code_pred %quote tranclp |
146 proof - |
146 proof - |
147 case tranclp |
147 case tranclp |
148 from this converse_tranclpE [OF tranclp.prems] show thesis by metis |
148 from this converse_tranclpE [OF tranclp.prems] show thesis by metis |
149 qed |
149 qed |
150 |
150 |
151 text {* |
151 text \<open> |
152 \noindent Alternative rules can also be used for constants that have |
152 \noindent Alternative rules can also be used for constants that have |
153 not been defined inductively. For example, the lexicographic order |
153 not been defined inductively. For example, the lexicographic order |
154 which is defined as: |
154 which is defined as: |
155 *} |
155 \<close> |
156 |
156 |
157 text %quote {* |
157 text %quote \<open> |
158 @{thm [display] lexordp_def [of r]} |
158 @{thm [display] lexordp_def [of r]} |
159 *} |
159 \<close> |
160 |
160 |
161 text {* |
161 text \<open> |
162 \noindent To make it executable, you can derive the following two |
162 \noindent To make it executable, you can derive the following two |
163 rules and prove the elimination rule: |
163 rules and prove the elimination rule: |
164 *} |
164 \<close> |
165 |
165 |
166 lemma %quote [code_pred_intro]: |
166 lemma %quote [code_pred_intro]: |
167 "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys" |
167 "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys" |
168 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*) |
168 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*) |
169 |
169 |
195 unfolding lexordp_def |
195 unfolding lexordp_def |
196 by fastforce |
196 by fastforce |
197 qed(*>*) |
197 qed(*>*) |
198 |
198 |
199 |
199 |
200 subsection {* Options for values *} |
200 subsection \<open>Options for values\<close> |
201 |
201 |
202 text {* |
202 text \<open> |
203 In the presence of higher-order predicates, multiple modes for some |
203 In the presence of higher-order predicates, multiple modes for some |
204 predicate could be inferred that are not disambiguated by the |
204 predicate could be inferred that are not disambiguated by the |
205 pattern of the set comprehension. To disambiguate the modes for 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 |
206 arguments of a predicate, you can state the modes explicitly in the |
207 @{command "values"} command. Consider the simple predicate @{term |
207 @{command "values"} command. Consider the simple predicate @{term |
208 "succ"}: |
208 "succ"}: |
209 *} |
209 \<close> |
210 |
210 |
211 inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
211 inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
212 "succ 0 (Suc 0)" |
212 "succ 0 (Suc 0)" |
213 | "succ x y \<Longrightarrow> succ (Suc x) (Suc y)" |
213 | "succ x y \<Longrightarrow> succ (Suc x) (Suc y)" |
214 |
214 |
215 code_pred %quote succ . |
215 code_pred %quote succ . |
216 |
216 |
217 text {* |
217 text \<open> |
218 \noindent For this, the predicate compiler can infer modes @{text "o |
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 |
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"} |
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 |
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 |
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, |
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 |
224 you can declare the mode for the argument between the @{command |
225 "values"} and the number of elements. |
225 "values"} and the number of elements. |
226 *} |
226 \<close> |
227 |
227 |
228 values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*) |
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}" |
229 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}" |
230 |
230 |
231 |
231 |
232 subsection {* Embedding into functional code within Isabelle/HOL *} |
232 subsection \<open>Embedding into functional code within Isabelle/HOL\<close> |
233 |
233 |
234 text {* |
234 text \<open> |
235 To embed the computation of an inductive predicate into functions |
235 To embed the computation of an inductive predicate into functions |
236 that are defined in Isabelle/HOL, you have a number of options: |
236 that are defined in Isabelle/HOL, you have a number of options: |
237 |
237 |
238 \begin{itemize} |
238 \begin{itemize} |
239 |
239 |