39 section {* The Code in a Nutshell\label{sec:nutshell} *} |
39 section {* The Code in a Nutshell\label{sec:nutshell} *} |
40 |
40 |
41 |
41 |
42 text {* |
42 text {* |
43 The inductive package will generate the reasoning infrastructure for |
43 The inductive package will generate the reasoning infrastructure for |
44 mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
44 mutually recursive predicates, say @{text "pred\<^sub>1\<dots>pred\<^sub>n"}. In what |
45 follows we will have the convention that various, possibly empty collections |
45 follows we will have the convention that various, possibly empty collections |
46 of ``things'' (lists, terms, nested implications and so on) are indicated either by |
46 of ``things'' (lists, terms, nested implications and so on) are indicated either by |
47 adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] |
47 adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes] |
48 "\<^isup>*"}. The shorthand for the predicates will therefore be @{text |
48 "\<^sup>*"}. The shorthand for the predicates will therefore be @{text |
49 "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must |
49 "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must |
50 be, of course, at least a single one in order to obtain a meaningful |
50 be, of course, at least a single one in order to obtain a meaningful |
51 definition. |
51 definition. |
52 |
52 |
53 The input for the inductive package will be some @{text "preds"} with possible |
53 The input for the inductive package will be some @{text "preds"} with possible |
56 notation, one such @{text "rule"} is assumed to be of the form |
56 notation, one such @{text "rule"} is assumed to be of the form |
57 |
57 |
58 \begin{isabelle} |
58 \begin{isabelle} |
59 @{text "rule ::= |
59 @{text "rule ::= |
60 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
60 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
61 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
61 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
62 \<Longrightarrow> pred ts"} |
62 \<Longrightarrow> pred ts"} |
63 \end{isabelle} |
63 \end{isabelle} |
64 |
64 |
65 For the purposes here, we will assume the @{text rules} have this format and |
65 For the purposes here, we will assume the @{text rules} have this format and |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
67 wrong, if the @{text "rules"} are not of this form. The @{text As} and |
67 wrong, if the @{text "rules"} are not of this form. The @{text As} and |
68 @{text Bs} in a @{text "rule"} stand for formulae not involving the |
68 @{text Bs} in a @{text "rule"} stand for formulae not involving the |
69 inductive predicates @{text "preds"}; the instances @{text "pred ss"} and |
69 inductive predicates @{text "preds"}; the instances @{text "pred ss"} and |
70 @{text "pred ts"} can stand for different predicates, like @{text |
70 @{text "pred ts"} can stand for different predicates, like @{text |
71 "pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}, in case mutual recursive |
71 "pred\<^sub>1 ss"} and @{text "pred\<^sub>2 ts"}, in case mutual recursive |
72 predicates are defined; the terms @{text ss} and @{text ts} are the |
72 predicates are defined; the terms @{text ss} and @{text ts} are the |
73 arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred |
73 arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred |
74 ts"} is a premise of the rule. The outermost quantified variables @{text |
74 ts"} is a premise of the rule. The outermost quantified variables @{text |
75 "xs"} are usually omitted in the user's input. The quantification for the |
75 "xs"} are usually omitted in the user's input. The quantification for the |
76 variables @{text "ys"} is local with respect to one recursive premise and |
76 variables @{text "ys"} is local with respect to one recursive premise and |
94 induction principles and introduction rules. For the definitions we need to have the |
94 induction principles and introduction rules. For the definitions we need to have the |
95 @{text rules} in a form where the meta-quantifiers and meta-implications are |
95 @{text rules} in a form where the meta-quantifiers and meta-implications are |
96 replaced by their object logic equivalents. Therefore an @{text "orule"} is |
96 replaced by their object logic equivalents. Therefore an @{text "orule"} is |
97 of the form |
97 of the form |
98 |
98 |
99 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
99 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^sup>* \<longrightarrow> pred ts"} |
100 |
100 |
101 A definition for the predicate @{text "pred"} has then the form |
101 A definition for the predicate @{text "pred"} has then the form |
102 |
102 |
103 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
103 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
104 |
104 |
131 |
131 |
132 Although the user declares the introduction rules @{text rules}, they must |
132 Although the user declares the introduction rules @{text rules}, they must |
133 also be derived from the @{text defs}. These derivations are a bit involved. |
133 also be derived from the @{text defs}. These derivations are a bit involved. |
134 Assuming we want to prove the introduction rule |
134 Assuming we want to prove the introduction rule |
135 |
135 |
136 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
136 @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"} |
137 |
137 |
138 then we have assumptions of the form |
138 then we have assumptions of the form |
139 |
139 |
140 \begin{isabelle} |
140 \begin{isabelle} |
141 (i)~~@{text "As"}\\ |
141 (i)~~@{text "As"}\\ |
142 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
142 (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"} |
143 \end{isabelle} |
143 \end{isabelle} |
144 |
144 |
145 and must show the goal |
145 and must show the goal |
146 |
146 |
147 @{text [display] "pred ts"} |
147 @{text [display] "pred ts"} |
148 |
148 |
149 If we now unfold the definitions for the @{text preds}, we have assumptions |
149 If we now unfold the definitions for the @{text preds}, we have assumptions |
150 |
150 |
151 \begin{isabelle} |
151 \begin{isabelle} |
152 (i)~~~@{text "As"}\\ |
152 (i)~~~@{text "As"}\\ |
153 (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\ |
153 (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}\\ |
154 (iii)~@{text "orules"} |
154 (iii)~@{text "orules"} |
155 \end{isabelle} |
155 \end{isabelle} |
156 |
156 |
157 and need to show |
157 and need to show |
158 |
158 |
162 into the assumption. The @{text "orules"} stand for all introduction rules that are given |
162 into the assumption. The @{text "orules"} stand for all introduction rules that are given |
163 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
163 by the user. We apply the @{text orule} that corresponds to introduction rule we are |
164 proving. After transforming the object connectives into meta-connectives, this introduction |
164 proving. After transforming the object connectives into meta-connectives, this introduction |
165 rule must necessarily be of the form |
165 rule must necessarily be of the form |
166 |
166 |
167 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
167 @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"} |
168 |
168 |
169 When we apply this rule we end up in the goal state where we have to prove |
169 When we apply this rule we end up in the goal state where we have to prove |
170 goals of the form |
170 goals of the form |
171 |
171 |
172 \begin{isabelle} |
172 \begin{isabelle} |
173 (a)~@{text "As"}\\ |
173 (a)~@{text "As"}\\ |
174 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"} |
174 (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"} |
175 \end{isabelle} |
175 \end{isabelle} |
176 |
176 |
177 We can immediately discharge the goals @{text "As"} using the assumptions in |
177 We can immediately discharge the goals @{text "As"} using the assumptions in |
178 @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we |
178 @{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we |
179 assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the |
179 assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the |
180 @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the |
180 @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the |
181 assumptions |
181 assumptions |
182 |
182 |
183 @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"} |
183 @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"} |
184 |
184 |
185 Instantiating the universal quantifiers and then resolving with the assumptions |
185 Instantiating the universal quantifiers and then resolving with the assumptions |
186 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
186 in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after. |
187 This completes the proof for introduction rules. |
187 This completes the proof for introduction rules. |
188 |
188 |