18 (*>*) |
18 (*>*) |
19 |
19 |
20 section {* The Code in a Nutshell\label{sec:nutshell} *} |
20 section {* The Code in a Nutshell\label{sec:nutshell} *} |
21 |
21 |
22 text {* |
22 text {* |
23 (FIXME: perhaps move somewhere else) |
23 The inductive package will generate the reasoning infrastructure for |
24 |
24 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
25 The point of these examples is to get a feeling what the automatic proofs |
25 follows we will have the convention that various, possibly empty collections |
26 should do in order to solve all inductive definitions we throw at them. For this |
26 of ``things'' (lists, nested implications and so on) are indicated either by |
27 it is instructive to look at the general construction principle |
27 adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] |
28 of inductive definitions, which we shall do in the next section. |
28 "\<^isup>*"}. The shorthand for the predicates will therefore be @{text |
29 *} |
29 "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must |
30 |
30 be, of course, at least a single one in order to obtain a meaningful |
31 text {* |
31 definition. |
32 The inductive package will generate the reasoning infrastructure |
|
33 for mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
|
34 follows we will have the convention that various, possibly empty collections of |
|
35 ``things'' are indicated either by adding an @{text "s"} or by adding |
|
36 a superscript @{text [quotes] "\<^isup>*"}. The shorthand for the predicates |
|
37 will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In the case of the |
|
38 predicates there must be, of course, at least a single one in order to obtain a |
|
39 meaningful definition. |
|
40 |
32 |
41 The input for the inductive package will be some @{text "preds"} with possible |
33 The input for the inductive package will be some @{text "preds"} with possible |
42 typing and syntax annotations, and also some introduction rules. We call below the |
34 typing and syntax annotations, and also some introduction rules. We call below the |
43 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle |
35 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle |
44 notation, one such @{text "rule"} is assumed to be of the form |
36 notation, one such @{text "rule"} is assumed to be of the form |
52 |
44 |
53 For the purposes here, we will assume the @{text rules} have |
45 For the purposes here, we will assume the @{text rules} have |
54 this format and omit any code that actually tests this. Therefore ``things'' |
46 this format and omit any code that actually tests this. Therefore ``things'' |
55 can go horribly wrong, if the @{text "rules"} are not of this |
47 can go horribly wrong, if the @{text "rules"} are not of this |
56 form.\footnote{FIXME: Exercise to test this format.} The @{text As} and |
48 form.\footnote{FIXME: Exercise to test this format.} The @{text As} and |
57 @{text Bs} in a @{text "rule"} are formulae not involving the inductive |
49 @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive |
58 predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred |
50 predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred |
59 ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and |
51 ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and |
60 @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the |
52 @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the |
61 arguments of the predicates. Every formula left of @{text [quotes] |
53 arguments of these predicates. Every formula left of @{text [quotes] |
62 "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified |
54 "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified |
63 variables @{text "xs"} are usually omitted in the user's input. The |
55 variables @{text "xs"} are usually omitted in the user's input. The |
64 quantification for the variables @{text "ys"} is local with respect to |
56 quantification for the variables @{text "ys"} is local with respect to |
65 one recursive premise and must be given. Some examples of @{text "rule"}s |
57 one recursive premise and must be given. Some examples of @{text "rule"}s |
66 are |
58 are |
73 |
65 |
74 has a single recursive premise; the rule |
66 has a single recursive premise; the rule |
75 |
67 |
76 @{thm [display] accpartI[no_vars]} |
68 @{thm [display] accpartI[no_vars]} |
77 |
69 |
78 has a recursive premise that has a precondition. As usual all |
70 has a single recursive premise that has a precondition. As usual all |
79 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
71 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
80 |
72 |
81 The code of the inductive package falls roughly in tree parts: the first |
73 The code of the inductive package falls roughly in tree parts: the first |
82 deals with the definitions, the second with the induction principles and |
74 deals with the definitions, the second with the induction principles and |
83 the third with the introduction rules. |
75 the third with the introduction rules. |
104 we first transform @{text ind} into the object logic and fix the meta-variables. |
96 we first transform @{text ind} into the object logic and fix the meta-variables. |
105 Hence we have to prove a formula of the form |
97 Hence we have to prove a formula of the form |
106 |
98 |
107 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"} |
99 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"} |
108 |
100 |
109 If we assume @{text "pred zs"} and unfold its definition, then we have |
101 If we assume @{text "pred zs"} and unfold its definition, then we have an |
|
102 assumption |
110 |
103 |
111 @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} |
104 @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} |
112 |
105 |
113 and must prove |
106 and must prove the goal |
114 |
107 |
115 @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"} |
108 @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"} |
116 |
109 |
117 This can be done by instantiating the @{text "\<forall>preds"}-quantification |
110 This can be done by instantiating the @{text "\<forall>preds"}-quantification |
118 with the @{text "Ps"}. Then we are done since we are left with a simple |
111 with the @{text "Ps"}. Then we are done since we are left with a simple |
119 identity. |
112 identity. |
120 |
113 |
121 Although the user declares introduction rules @{text rules}, they must |
114 Although the user declares introduction rules @{text rules}, they must |
122 be derived from the @{text defs}. These derivations are a bit involved. |
115 also be derived from the @{text defs}. These derivations are a bit involved. |
123 Assuming we want to prove the introduction rule |
116 Assuming we want to prove the introduction rule |
124 |
117 |
125 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
118 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
126 |
119 |
127 then we can assume |
120 then we can have assumptions of the form |
128 |
121 |
129 \begin{isabelle} |
122 \begin{isabelle} |
130 (i)~~@{text "As"}\\ |
123 (i)~~@{text "As"}\\ |
131 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
124 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
132 \end{isabelle} |
125 \end{isabelle} |
133 |
126 |
134 and must show |
127 and must show the goal |
135 |
128 |
136 @{text [display] "pred ts"} |
129 @{text [display] "pred ts"} |
137 |
130 |
138 If we now unfold the definitions for the @{text preds}, we have |
131 If we now unfold the definitions for the @{text preds}, we have assumptions |
139 |
132 |
140 \begin{isabelle} |
133 \begin{isabelle} |
141 (i)~~~@{text "As"}\\ |
134 (i)~~~@{text "As"}\\ |
142 (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\ |
135 (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\ |
143 (iii)~@{text "orules"} |
136 (iii)~@{text "orules"} |
153 proving. This introduction rule must necessarily be of the form |
146 proving. This introduction rule must necessarily be of the form |
154 |
147 |
155 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
148 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
156 |
149 |
157 When we apply this rule we end up in the goal state where we have to prove |
150 When we apply this rule we end up in the goal state where we have to prove |
|
151 goals of the form |
158 |
152 |
159 \begin{isabelle} |
153 \begin{isabelle} |
160 (a)~@{text "As"}\\ |
154 (a)~@{text "As"}\\ |
161 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
155 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
162 \end{isabelle} |
156 \end{isabelle} |
163 |
157 |
164 We can immediately discharge the goals @{text "As"} using the assumption in |
158 We can immediately discharge the goals @{text "As"} using the assumptions in |
165 @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we |
159 @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we |
166 assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the |
160 assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the |
167 @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the |
161 @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the |
168 assumptions |
162 assumptions |
169 |
163 |
171 |
165 |
172 Instantiating the universal quantifiers and then resolving with the assumptions |
166 Instantiating the universal quantifiers and then resolving with the assumptions |
173 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
167 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
174 This completes the proof for introduction rules. |
168 This completes the proof for introduction rules. |
175 |
169 |
176 What remains is to implement the reasoning outlined above. We do this in |
170 What remains is to implement the reasoning outlined in this section. We do this |
177 the next section. For building testcases, we use the shorthands for |
171 next. For building testcases, we use the shorthands for |
178 @{text "even/odd"}, @{term "fresh"} and @{term "accpart"} |
172 @{text "even/odd"}, @{term "fresh"} and @{term "accpart"} |
179 given in Figure~\ref{fig:shorthands}. |
173 given in Figure~\ref{fig:shorthands}. |
180 *} |
174 *} |
181 |
175 |
182 |
176 |