1 theory Ind_General_Scheme |
1 theory Ind_General_Scheme |
2 imports Main |
2 imports Simple_Inductive_Package Ind_Prelims |
3 begin |
3 begin |
4 |
4 |
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
5 (*<*) |
|
6 datatype trm = |
|
7 Var "string" |
|
8 | App "trm" "trm" |
|
9 | Lam "string" "trm" |
|
10 |
|
11 simple_inductive |
|
12 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" |
|
13 where |
|
14 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
|
15 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
|
16 | fresh_lam1: "fresh a (Lam a t)" |
|
17 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
|
18 (*>*) |
|
19 |
|
20 section {* The Code in a Nutshell *} |
6 |
21 |
7 text {* |
22 text {* |
8 |
23 (FIXME: perhaps move somewhere else) |
|
24 |
9 The point of these examples is to get a feeling what the automatic proofs |
25 The point of these examples is to get a feeling what the automatic proofs |
10 should do in order to solve all inductive definitions we throw at them. For this |
26 should do in order to solve all inductive definitions we throw at them. For this |
11 it is instructive to look at the general construction principle |
27 it is instructive to look at the general construction principle |
12 of inductive definitions, which we shall do in the next section. |
28 of inductive definitions, which we shall do in the next section. |
13 |
|
14 Before we start with the implementation, it is useful to describe the general |
|
15 form of inductive definitions that our package should accept. |
|
16 Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
|
17 some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |
|
18 the form |
|
19 |
|
20 \[ |
|
21 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
|
22 R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i |
|
23 \qquad \mbox{for\ } i=1,\ldots,r |
|
24 \] |
|
25 |
|
26 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. |
|
27 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure |
|
28 that all occurrences of the predicates in the premises of the introduction rules are |
|
29 \emph{strictly positive}. This condition guarantees the existence of predicates |
|
30 that are closed under the introduction rules shown above. Then the definitions of the |
|
31 inductive predicates $R_1,\ldots,R_n$ is: |
|
32 |
|
33 \[ |
|
34 \begin{array}{l@ {\qquad}l} |
|
35 R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i & |
|
36 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
|
37 \mbox{where} \\ |
|
38 K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow |
|
39 P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i & |
|
40 \mbox{for\ } i=1,\ldots,r |
|
41 \end{array} |
|
42 \] |
|
43 |
|
44 The induction principles for the inductive predicates $R_1,\ldots,R_n$ are |
|
45 |
|
46 \[ |
|
47 \begin{array}{l@ {\qquad}l} |
|
48 R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i & |
|
49 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
|
50 \mbox{where} \\ |
|
51 I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
|
52 P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i & |
|
53 \mbox{for\ } i=1,\ldots,r |
|
54 \end{array} |
|
55 \] |
|
56 |
|
57 Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level |
|
58 connectives, it is clear that the proof of the induction theorem is straightforward. We will |
|
59 therefore focus on the proof of the introduction rules. When proving the introduction rule |
|
60 shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields |
|
61 |
|
62 \[ |
|
63 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
|
64 \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i |
|
65 \] |
|
66 |
|
67 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for |
|
68 $\forall$ and $\longrightarrow$ yields a goal state in which we have to prove $P_{l_i}~\vec{t}_i$ |
|
69 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to the meta-logic format) |
|
70 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, |
|
71 as well as subgoals of the form |
|
72 |
|
73 \[ |
|
74 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i |
|
75 \] |
|
76 |
|
77 that can be solved using the assumptions |
|
78 |
|
79 \[ |
|
80 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
|
81 \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K} |
|
82 \] |
|
83 |
|
84 What remains is to implement these proofs generically. |
|
85 *} |
29 *} |
86 |
30 |
|
31 text {* |
|
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 this case of the |
|
38 predicates there must be at least a single one in order to obtain a meaningful |
|
39 definition. |
|
40 |
|
41 The input for the inductive predicate will be some @{text "preds"} with possible |
|
42 typing and syntax annotations, and also some introduction rules. We call below the |
|
43 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle |
|
44 notation, one such @{text "rule"} is of the form |
|
45 |
|
46 \begin{isabelle} |
|
47 @{text "rule ::= |
|
48 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
|
49 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
|
50 \<Longrightarrow> pred ts"} |
|
51 \end{isabelle} |
|
52 |
|
53 We actually assume the user will always state rules of this form and we omit |
|
54 any code that test this format. So things can go horribly wrong if the |
|
55 @{text "rules"} are not of this form.\footnote{FIXME: Exercise to test this |
|
56 format.} The @{text As} and @{text Bs} in a @{text "rule"} are formulae not |
|
57 involving the inductive predicates @{text "preds"}; the instances @{text |
|
58 "pred ss"} and @{text "pred ts"} can stand for different predicates. |
|
59 Everything left of @{text [quotes] "\<Longrightarrow> pred ts"} are called the premises of |
|
60 the rule. The variables @{text "xs"} are usually omitted in the user's |
|
61 input. The variables @{text "ys"} are local with respect to on recursive |
|
62 premise. Some examples of @{text "rule"}s the user might write are: |
|
63 |
|
64 |
|
65 @{thm [display] fresh_var[no_vars]} |
|
66 |
|
67 which has only a single non-recursive premise, whereas |
|
68 |
|
69 @{thm [display] evenS[no_vars]} |
|
70 |
|
71 has a single recursive premise; the rule |
|
72 |
|
73 @{thm [display] accpartI[no_vars]} |
|
74 |
|
75 has a recursive premise which has a precondition. In the examples, all |
|
76 rules are stated without the leading meta-quantification @{text "\<And>xs"}. |
|
77 |
|
78 The code of the inductive package falls roughly in tree parts involving |
|
79 the definitions, the induction principles and the introduction rules, |
|
80 respectively. For the definitions we need to have the @{text rules} |
|
81 in a form where the meta-quantifiers and meta-implications are replaced |
|
82 by their object logic equivalent. Therefore an @{text "orule"} is of the |
|
83 form |
|
84 |
|
85 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
|
86 |
|
87 A definition for the predicate @{text "pred"} has then the form |
|
88 |
|
89 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
|
90 |
|
91 The induction principles for the predicate @{text "pred"} are of the |
|
92 form |
|
93 |
|
94 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"} |
|
95 |
|
96 where in the @{text "rules"} every @{text pred} is replaced by a new |
|
97 (meta)variable @{text "?P"}. |
|
98 |
|
99 In order to derive an induction principle for the predicate @{text "pred"} |
|
100 we first transform it into the object logic and fix the meta-variables. Hence |
|
101 we have to prove a formula of the form |
|
102 |
|
103 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"} |
|
104 |
|
105 If we assume @{text "pred zs"} and unfold its definition, then we have |
|
106 |
|
107 @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} |
|
108 |
|
109 and must prove |
|
110 |
|
111 @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"} |
|
112 |
|
113 This can be done by instantiating the @{text "\<forall>preds"} with the @{text "Ps"}. |
|
114 Then we are done since we are left with a simple identity. |
|
115 |
|
116 The proofs for the introduction rules are more involved. Assuming we want to |
|
117 prove the introduction rule |
|
118 |
|
119 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
|
120 |
|
121 then we can assume |
|
122 |
|
123 \begin{isabelle} |
|
124 (i)~~@{text "As"}\\ |
|
125 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
|
126 \end{isabelle} |
|
127 |
|
128 and must show |
|
129 |
|
130 @{text [display] "pred ts"} |
|
131 |
|
132 If we now unfold the definitions for the @{text preds}, we have |
|
133 |
|
134 \begin{isabelle} |
|
135 (i)~~~@{text "As"}\\ |
|
136 (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\ |
|
137 (iii)~@{text "orules"} |
|
138 \end{isabelle} |
|
139 |
|
140 and need to show |
|
141 |
|
142 @{text [display] "pred ts"} |
|
143 |
|
144 In the last step we removed some quantifiers and moved the precondition @{text "orules"} |
|
145 into the assumtion. The @{text "orules"} stand for all introduction rules that are given |
|
146 by the user. We apply the one which corresponds to introduction rule we are proving. |
|
147 This introduction rule must be of the form |
|
148 |
|
149 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
|
150 |
|
151 When we apply this rule we end up in the goal state where we have to prove |
|
152 |
|
153 \begin{isabelle} |
|
154 (a)~@{text "As"}\\ |
|
155 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
|
156 \end{isabelle} |
|
157 |
|
158 The goals @{text "As"} we can immediately discharge with the assumption in @{text "(i)"}. |
|
159 The goals in @{text "(b)"} we discharge as follows: we assume the @{text "(iv)"} |
|
160 @{text "Bs"} and prove @{text "(c)"} @{text "pred ss"}. We then resolve the |
|
161 @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us |
|
162 |
|
163 @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"} |
|
164 |
|
165 Instantiating the universal quantifiers and then resolving with the assumptions |
|
166 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
|
167 |
|
168 |
|
169 What remains is to implement the reasoning outlined above. |
|
170 For building testcases, we use some shorthands for the definitions |
|
171 of @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}. |
|
172 *} |
|
173 |
|
174 |
|
175 text_raw{* |
|
176 \begin{figure}[p] |
|
177 \begin{minipage}{\textwidth} |
|
178 \begin{isabelle}*} |
|
179 ML{*(* even-odd example *) |
|
180 val eo_defs = [@{thm even_def}, @{thm odd_def}] |
|
181 |
|
182 val eo_rules = |
|
183 [@{prop "even 0"}, |
|
184 @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"}, |
|
185 @{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}] |
|
186 |
|
187 val eo_orules = |
|
188 [@{prop "even 0"}, |
|
189 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
|
190 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
|
191 |
|
192 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
|
193 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
|
194 val eo_syns = [NoSyn, NoSyn] |
|
195 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
|
196 val e_pred = @{term "even::nat\<Rightarrow>bool"} |
|
197 val e_arg_tys = [@{typ "nat"}] |
|
198 |
|
199 |
|
200 |
|
201 (* freshness example *) |
|
202 val fresh_rules = |
|
203 [@{prop "\<And>a b. a \<noteq> b \<Longrightarrow> fresh a (Var b)"}, |
|
204 @{prop "\<And>a s t. fresh a t \<Longrightarrow> fresh a s \<Longrightarrow> fresh a (App t s)"}, |
|
205 @{prop "\<And>a t. fresh a (Lam a t)"}, |
|
206 @{prop "\<And>a b t. a \<noteq> b \<Longrightarrow> fresh a t \<Longrightarrow> fresh a (Lam b t)"}] |
|
207 |
|
208 val fresh_orules = |
|
209 [@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}, |
|
210 @{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}, |
|
211 @{prop "\<forall>a t. fresh a (Lam a t)"}, |
|
212 @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}] |
|
213 |
|
214 val fresh_pred = @{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"} |
|
215 val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}] |
|
216 |
|
217 |
|
218 |
|
219 (* accessible-part example *) |
|
220 val acc_rules = |
|
221 [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}] |
|
222 val acc_pred = @{term "accpart:: ('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*} |
|
223 text_raw{* |
|
224 \end{isabelle} |
|
225 \end{minipage} |
|
226 \caption{Shorthands for the inductive predicates of @{text "even"}-@{text "odd"}, |
|
227 @{text "fresh"} and @{text "accpart"}. The follow the convention @{text "rules"}, |
|
228 @{text "orules"}, @{text "preds"} and so on as used in Section ???. The purpose |
|
229 of these shorthands is to simplify the construction of testcases.} |
|
230 \end{figure} |
|
231 *} |
|
232 |
|
233 |
|
234 |
87 end |
235 end |