1 theory Ind_Prelims |
1 theory Ind_Prelims |
2 imports Main LaTeXsugar"../Base" Simple_Inductive_Package |
2 imports Main LaTeXsugar "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section{* Preliminaries *} |
5 section{* Preliminaries *} |
6 |
6 |
7 text {* |
7 text {* |
8 The user will just give a specification of inductive predicate(s) and |
8 The user will just give a specification of inductive predicate(s) and |
9 expects from the package to produce a convenient reasoning |
9 expects from the package to produce a convenient reasoning |
10 infrastructure. This infrastructure needs to be derived from the definition |
10 infrastructure. This infrastructure needs to be derived from the definition |
11 that correspond to the specified predicate(s). Before we start with |
11 that correspond to the specified predicate(s). Before we start with |
12 explaining all parts of the package, let us first give four examples showing |
12 explaining all parts of the package, let us first give some examples |
13 how to define inductive predicates by hand and then also how to prove by |
13 showing how to define inductive predicates and then also how |
14 hand properties about them. See Figure \ref{fig:paperpreds} for their usual |
14 to generate a reasoning infrastructure for them. From the examples |
15 ``pencil-and-paper'' definitions. From these examples, we will |
15 we will figure out a general method for |
16 figure out a general method for defining inductive predicates. The aim in |
16 defining inductive predicates. The aim in this section is \emph{not} to |
17 this section is \emph{not} to write proofs that are as beautiful as |
17 write proofs that are as beautiful as possible, but as close as possible to |
18 possible, but as close as possible to the ML-code we will develop in later |
18 the ML-code we will develop in later sections. |
19 sections. |
19 |
20 |
20 |
21 \begin{figure}[t] |
21 |
22 \begin{boxedminipage}{\textwidth} |
22 We first consider the transitive closure of a relation @{text R}. The |
|
23 ``pencil-and-paper'' specification for the transitive closure is: |
|
24 |
23 \begin{center}\small |
25 \begin{center}\small |
24 @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} |
26 @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} |
25 @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
27 @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
26 \end{center} |
28 \end{center} |
27 \begin{center}\small |
29 |
28 @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
30 The package has to make an appropriate definition. Since an inductively |
29 @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm} |
|
30 @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"} |
|
31 \end{center} |
|
32 \begin{center}\small |
|
33 \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}} |
|
34 \end{center} |
|
35 \begin{center}\small |
|
36 @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm} |
|
37 @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm] |
|
38 @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm} |
|
39 @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"} |
|
40 \end{center} |
|
41 \end{boxedminipage} |
|
42 \caption{Examples of four ``Pencil-and-paper'' definitions of inductively defined |
|
43 predicates. In formal reasoning with Isabelle, the user just wants to give such |
|
44 definitions and expects that the reasoning structure is derived automatically. |
|
45 For this definitional packages need to be implemented.\label{fig:paperpreds}} |
|
46 \end{figure} |
|
47 |
|
48 We first consider the transitive closure of a relation @{text R}. The user will |
|
49 state for @{term trcl\<iota>} the specification: |
|
50 *} |
|
51 |
|
52 simple_inductive |
|
53 trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
54 where |
|
55 base: "trcl\<iota> R x x" |
|
56 | step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z" |
|
57 |
|
58 text {* |
|
59 The package has to make an appropriate definition and provide |
|
60 lemmas to reason about the predicate @{term trcl\<iota>}. Since an inductively |
|
61 defined predicate is the least predicate closed under a collection of |
31 defined predicate is the least predicate closed under a collection of |
62 introduction rules, the predicate @{text "trcl R x y"} can be defined so |
32 introduction rules, the predicate @{text "trcl R x y"} can be defined so |
63 that it holds if and only if @{text "P x y"} holds for every predicate |
33 that it holds if and only if @{text "P x y"} holds for every predicate |
64 @{text P} closed under the rules above. This gives rise to the definition |
34 @{text P} closed under the rules above. This gives rise to the definition |
65 *} |
35 *} |
77 |
47 |
78 |
48 |
79 With this definition, the proof of the induction principle for @{term trcl} |
49 With this definition, the proof of the induction principle for @{term trcl} |
80 is almost immediate. It suffices to convert all the meta-level |
50 is almost immediate. It suffices to convert all the meta-level |
81 connectives in the lemma to object-level connectives using the |
51 connectives in the lemma to object-level connectives using the |
82 proof method @{text atomize} (Line 4), expand the definition of @{term trcl} |
52 proof method @{text atomize} (Line 4 below), expand the definition of @{term trcl} |
83 (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7), |
53 (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7), |
84 and then solve the goal by @{text assumption} (Line 8). |
54 and then solve the goal by @{text assumption} (Line 8). |
85 |
55 |
86 *} |
56 *} |
87 |
57 |
122 |
92 |
123 text {* |
93 text {* |
124 The two assumptions come from the definition of @{term trcl} and correspond |
94 The two assumptions come from the definition of @{term trcl} and correspond |
125 to the introduction rules. Thus, all we have to do is to eliminate the |
95 to the introduction rules. Thus, all we have to do is to eliminate the |
126 universal quantifier in front of the first assumption (Line 5), and then |
96 universal quantifier in front of the first assumption (Line 5), and then |
127 solve the goal by assumption (Line 6). |
97 solve the goal by @{text assumption} (Line 6). |
128 *} |
98 *} |
129 |
99 |
130 text {* |
100 text {* |
131 Next we have to show that the second introduction rule also follows from the |
101 Next we have to show that the second introduction rule also follows from the |
132 definition. Since this rule has premises, the proof is a bit more |
102 definition. Since this rule has premises, the proof is a bit more |
158 show "P x z" |
128 show "P x z" |
159 |
129 |
160 txt {* |
130 txt {* |
161 The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of |
131 The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of |
162 the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"} |
132 the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"} |
163 come from the definition of @{term trcl} . We apply @{text "r2"} to the goal |
133 come from the definition of @{term trcl}. We apply @{text "r2"} to the goal |
164 @{term "P x z"}. In order for the assumption to be applicable as a rule, we |
134 @{term "P x z"}. In order for this assumption to be applicable as a rule, we |
165 have to eliminate the universal quantifier and turn the object-level |
135 have to eliminate the universal quantifier and turn the object-level |
166 implications into meta-level ones. This can be accomplished using the @{text |
136 implications into meta-level ones. This can be accomplished using the @{text |
167 rule_format} attribute. So we continue the proof with: |
137 rule_format} attribute. So we continue the proof with: |
168 |
138 |
169 *} |
139 *} |
209 tactics whenever something goes wrong. Therefore if possible, automatic |
179 tactics whenever something goes wrong. Therefore if possible, automatic |
210 tactics should be avoided or be constrained sufficiently. |
180 tactics should be avoided or be constrained sufficiently. |
211 |
181 |
212 The method of defining inductive predicates by impredicative quantification |
182 The method of defining inductive predicates by impredicative quantification |
213 also generalises to mutually inductive predicates. The next example defines |
183 also generalises to mutually inductive predicates. The next example defines |
214 the predicates @{text even} and @{text odd}. The user will state for this |
184 the predicates @{text even} and @{text odd} given by |
215 inductive definition the specification: |
185 |
216 *} |
186 \begin{center}\small |
217 |
187 @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
218 simple_inductive |
188 @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm} |
219 even and odd |
189 @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"} |
220 where |
190 \end{center} |
221 even0: "even 0" |
191 |
222 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
|
223 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
|
224 |
|
225 text {* |
|
226 Since the predicates @{term even} and @{term odd} are mutually inductive, each |
192 Since the predicates @{term even} and @{term odd} are mutually inductive, each |
227 corresponding definition must quantify over both predicates (we name them |
193 corresponding definition must quantify over both predicates (we name them |
228 below @{text "P"} and @{text "Q"}). |
194 below @{text "P"} and @{text "Q"}). |
229 *} |
195 *} |
230 |
196 |
231 definition "even\<iota> \<equiv> |
197 definition "even \<equiv> |
232 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
198 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
233 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
199 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
234 |
200 |
235 definition "odd\<iota> \<equiv> |
201 definition "odd \<equiv> |
236 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
202 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
237 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
203 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
238 |
204 |
239 text {* |
205 text {* |
240 For proving the induction principles, we use exactly the same technique |
206 For proving the induction principles, we use exactly the same technique |
278 THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3]) |
244 THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3]) |
279 done |
245 done |
280 qed |
246 qed |
281 |
247 |
282 text {* |
248 text {* |
283 The interesting lines are 7 to 15. The assumptions fall into to categories: |
249 The interesting lines are 7 to 15. The assumptions fall into two categories: |
284 @{text p1} corresponds to the premise of the introduction rule; @{text "r1"} |
250 @{text p1} corresponds to the premise of the introduction rule; @{text "r1"} |
285 to @{text "r3"} come from the definition of @{text "even"}. |
251 to @{text "r3"} come from the definition of @{text "even"}. |
286 In Line 13, we apply the assumption @{text "r2"} (since we prove the second |
252 In Line 13, we apply the assumption @{text "r2"} (since we prove the second |
287 introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if |
253 introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if |
288 the second introduction rule had more premises we have to do that for all |
254 the second introduction rule had more premises we have to do that for all |
289 of them). In order for this assumption to be applicable, the quantifiers |
255 of them). In order for this assumption to be applicable, the quantifiers |
290 need to be instantiated and then also the implications need to be resolved |
256 need to be instantiated and then also the implications need to be resolved |
291 with the other rules. |
257 with the other rules. |
292 |
258 |
293 As a final example, we define the accessible part of a relation @{text R} |
259 Next we define the accessible part of a relation @{text R} given by |
294 (see Figure~\ref{fig:paperpreds}). There the premsise of the introduction |
260 the single rule: |
295 rule involves a universal quantifier and an implication. The |
261 |
296 definition of @{text accpart} is: |
262 \begin{center}\small |
|
263 \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}} |
|
264 \end{center} |
|
265 |
|
266 The definition of @{text "accpart"} is: |
297 *} |
267 *} |
298 |
268 |
299 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
269 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
300 |
270 |
301 text {* |
271 text {* |
323 done |
293 done |
324 qed |
294 qed |
325 qed |
295 qed |
326 |
296 |
327 text {* |
297 text {* |
328 There are now two subproofs. The assumptions fall again into two categories (Lines |
298 As you can see, there are now two subproofs. The assumptions fall again into |
329 7 to 9). In Line 11, applying the assumption @{text "r1"} generates a goal state |
299 two categories (Lines 7 to 9). In Line 11, applying the assumption @{text |
330 with the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the |
300 "r1"} generates a goal state with the new local assumption @{term "R y x"}, |
331 proof (Line 14). This local assumption is used to solve |
301 named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is |
332 the goal @{term "P y"} with the help of assumption @{text "p1"}. |
302 used to solve the goal @{term "P y"} with the help of assumption @{text |
333 |
303 "p1"}. |
334 The point of these examples is to get a feeling what the automatic proofs |
304 |
335 should do in order to solve all inductive definitions we throw at them. |
305 |
336 This is usually the first step in writing a package. We next explain |
306 \begin{exercise} |
|
307 Give the definition for the freshness predicate for lambda-terms. The rules |
|
308 for this predicate are: |
|
309 |
|
310 \begin{center}\small |
|
311 @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm} |
|
312 @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm] |
|
313 @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm} |
|
314 @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"} |
|
315 \end{center} |
|
316 |
|
317 From the definition derive the induction principle and the introduction |
|
318 rules. |
|
319 \end{exercise} |
|
320 |
|
321 The point of all these examples is to get a feeling what the automatic |
|
322 proofs should do in order to solve all inductive definitions we throw at |
|
323 them. This is usually the first step in writing a package. We next explain |
337 the parsing and typing part of the package. |
324 the parsing and typing part of the package. |
338 |
325 |
339 *} |
326 *} |
340 (*<*)end(*>*) |
327 (*<*)end(*>*) |