210
|
1 |
theory Ind_General_Scheme
|
244
|
2 |
imports "../Base" Simple_Inductive_Package
|
32
|
3 |
begin
|
|
4 |
|
244
|
5 |
(*<*)
|
|
6 |
simple_inductive
|
|
7 |
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
8 |
where
|
|
9 |
base: "trcl R x x"
|
|
10 |
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
|
|
11 |
|
|
12 |
simple_inductive
|
|
13 |
even and odd
|
|
14 |
where
|
|
15 |
even0: "even 0"
|
|
16 |
| evenS: "odd n \<Longrightarrow> even (Suc n)"
|
|
17 |
| oddS: "even n \<Longrightarrow> odd (Suc n)"
|
|
18 |
|
|
19 |
simple_inductive
|
|
20 |
accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
|
|
21 |
where
|
|
22 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
|
|
23 |
|
|
24 |
datatype trm =
|
|
25 |
Var "string"
|
|
26 |
| App "trm" "trm"
|
|
27 |
| Lam "string" "trm"
|
|
28 |
|
|
29 |
simple_inductive
|
|
30 |
fresh :: "string \<Rightarrow> trm \<Rightarrow> bool"
|
|
31 |
where
|
|
32 |
fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
|
|
33 |
| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
|
|
34 |
| fresh_lam1: "fresh a (Lam a t)"
|
|
35 |
| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
|
|
36 |
(*>*)
|
|
37 |
|
|
38 |
|
219
|
39 |
section {* The Code in a Nutshell\label{sec:nutshell} *}
|
210
|
40 |
|
|
41 |
|
32
|
42 |
text {*
|
212
|
43 |
The inductive package will generate the reasoning infrastructure for
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
|
212
|
45 |
follows we will have the convention that various, possibly empty collections
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
of ``things'' (lists, terms, nested implications and so on) are indicated either by
|
212
|
47 |
adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
|
|
48 |
"\<^isup>*"}. The shorthand for the predicates will therefore be @{text
|
|
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
|
|
51 |
definition.
|
210
|
52 |
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
The input for the inductive package will be some @{text "preds"} with possible
|
210
|
54 |
typing and syntax annotations, and also some introduction rules. We call below the
|
|
55 |
introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
notation, one such @{text "rule"} is assumed to be of the form
|
210
|
57 |
|
|
58 |
\begin{isabelle}
|
|
59 |
@{text "rule ::=
|
|
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}}$>
|
|
62 |
\<Longrightarrow> pred ts"}
|
|
63 |
\end{isabelle}
|
|
64 |
|
278
|
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
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
wrong, if the @{text "rules"} are not of this form. The @{text As} and
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
@{text Bs} in a @{text "rule"} stand for formulae not involving the
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
inductive predicates @{text "preds"}; the instances @{text "pred ss"} and
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
@{text "pred ts"} can stand for different predicates, like @{text
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
"pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}, in case mutual recursive
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
predicates are defined; the terms @{text ss} and @{text ts} are the
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
ts"} is a premise of the rule. The outermost quantified variables @{text
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
"xs"} are usually omitted in the user's input. The quantification for the
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
variables @{text "ys"} is local with respect to one recursive premise and
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
must be given. Some examples of @{text "rule"}s are
|
278
|
78 |
|
210
|
79 |
|
|
80 |
@{thm [display] fresh_var[no_vars]}
|
|
81 |
|
|
82 |
which has only a single non-recursive premise, whereas
|
|
83 |
|
|
84 |
@{thm [display] evenS[no_vars]}
|
|
85 |
|
|
86 |
has a single recursive premise; the rule
|
|
87 |
|
|
88 |
@{thm [display] accpartI[no_vars]}
|
|
89 |
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
has a single recursive premise that has a precondition. As is custom all
|
210
|
91 |
rules are stated without the leading meta-quantification @{text "\<And>xs"}.
|
|
92 |
|
215
|
93 |
The output of the inductive package will be definitions for the predicates,
|
|
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
|
|
96 |
replaced by their object logic equivalents. Therefore an @{text "orule"} is
|
|
97 |
of the form
|
210
|
98 |
|
|
99 |
@{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
|
|
100 |
|
|
101 |
A definition for the predicate @{text "pred"} has then the form
|
|
102 |
|
|
103 |
@{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
|
|
104 |
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
The induction principles for every predicate @{text "pred"} are of the
|
210
|
106 |
form
|
|
107 |
|
|
108 |
@{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
|
|
109 |
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
meta-variable @{text "?P"}.
|
210
|
112 |
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
In order to derive an induction principle for the predicate @{text "pred"},
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
we first transform @{text ind} into the object logic and fix the meta-variables.
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
Hence we have to prove a formula of the form
|
210
|
116 |
|
|
117 |
@{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
|
|
118 |
|
212
|
119 |
If we assume @{text "pred zs"} and unfold its definition, then we have an
|
|
120 |
assumption
|
210
|
121 |
|
|
122 |
@{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"}
|
|
123 |
|
212
|
124 |
and must prove the goal
|
210
|
125 |
|
|
126 |
@{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
|
|
127 |
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
This can be done by instantiating the @{text "\<forall>preds"}-quantification
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
with the @{text "Ps"}. Then we are done since we are left with a simple
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
identity.
|
210
|
131 |
|
215
|
132 |
Although the user declares the introduction rules @{text rules}, they must
|
212
|
133 |
also be derived from the @{text defs}. These derivations are a bit involved.
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
Assuming we want to prove the introduction rule
|
210
|
135 |
|
|
136 |
@{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
|
|
137 |
|
215
|
138 |
then we have assumptions of the form
|
210
|
139 |
|
|
140 |
\begin{isabelle}
|
|
141 |
(i)~~@{text "As"}\\
|
|
142 |
(ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
|
|
143 |
\end{isabelle}
|
|
144 |
|
212
|
145 |
and must show the goal
|
210
|
146 |
|
|
147 |
@{text [display] "pred ts"}
|
|
148 |
|
212
|
149 |
If we now unfold the definitions for the @{text preds}, we have assumptions
|
210
|
150 |
|
|
151 |
\begin{isabelle}
|
|
152 |
(i)~~~@{text "As"}\\
|
|
153 |
(ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\
|
|
154 |
(iii)~@{text "orules"}
|
|
155 |
\end{isabelle}
|
|
156 |
|
|
157 |
and need to show
|
|
158 |
|
|
159 |
@{text [display] "pred ts"}
|
|
160 |
|
|
161 |
In the last step we removed some quantifiers and moved the precondition @{text "orules"}
|
278
|
162 |
into the assumption. The @{text "orules"} stand for all introduction rules that are given
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
by the user. We apply the @{text orule} that corresponds to introduction rule we are
|
278
|
164 |
proving. After transforming the object connectives into meta-connectives, this introduction
|
|
165 |
rule must necessarily be of the form
|
210
|
166 |
|
|
167 |
@{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
|
|
168 |
|
|
169 |
When we apply this rule we end up in the goal state where we have to prove
|
212
|
170 |
goals of the form
|
210
|
171 |
|
|
172 |
\begin{isabelle}
|
|
173 |
(a)~@{text "As"}\\
|
|
174 |
(b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
|
|
175 |
\end{isabelle}
|
|
176 |
|
212
|
177 |
We can immediately discharge the goals @{text "As"} using the assumptions in
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
@{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
179 |
assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
@{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
assumptions
|
210
|
182 |
|
|
183 |
@{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
|
|
184 |
|
|
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.
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
This completes the proof for introduction rules.
|
210
|
188 |
|
215
|
189 |
What remains is to implement in Isabelle the reasoning outlined in this section.
|
|
190 |
We will describe the code in the next section. For building testcases, we use the shorthands for
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
@{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
|
215
|
192 |
defined in Figure~\ref{fig:shorthands}.
|
210
|
193 |
*}
|
|
194 |
|
|
195 |
|
|
196 |
text_raw{*
|
|
197 |
\begin{figure}[p]
|
|
198 |
\begin{minipage}{\textwidth}
|
|
199 |
\begin{isabelle}*}
|
|
200 |
ML{*(* even-odd example *)
|
|
201 |
val eo_defs = [@{thm even_def}, @{thm odd_def}]
|
|
202 |
|
|
203 |
val eo_rules =
|
|
204 |
[@{prop "even 0"},
|
|
205 |
@{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
|
|
206 |
@{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
|
|
207 |
|
|
208 |
val eo_orules =
|
|
209 |
[@{prop "even 0"},
|
|
210 |
@{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
|
|
211 |
@{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
|
|
212 |
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
val eo_preds = [@{term "even::nat \<Rightarrow> bool"}, @{term "odd::nat \<Rightarrow> bool"}]
|
210
|
214 |
val eo_prednames = [@{binding "even"}, @{binding "odd"}]
|
237
|
215 |
val eo_mxs = [NoSyn, NoSyn]
|
210
|
216 |
val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
val e_pred = @{term "even::nat \<Rightarrow> bool"}
|
210
|
218 |
val e_arg_tys = [@{typ "nat"}]
|
|
219 |
|
|
220 |
|
|
221 |
|
|
222 |
(* freshness example *)
|
|
223 |
val fresh_rules =
|
|
224 |
[@{prop "\<And>a b. a \<noteq> b \<Longrightarrow> fresh a (Var b)"},
|
|
225 |
@{prop "\<And>a s t. fresh a t \<Longrightarrow> fresh a s \<Longrightarrow> fresh a (App t s)"},
|
|
226 |
@{prop "\<And>a t. fresh a (Lam a t)"},
|
|
227 |
@{prop "\<And>a b t. a \<noteq> b \<Longrightarrow> fresh a t \<Longrightarrow> fresh a (Lam b t)"}]
|
|
228 |
|
|
229 |
val fresh_orules =
|
|
230 |
[@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"},
|
|
231 |
@{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"},
|
|
232 |
@{prop "\<forall>a t. fresh a (Lam a t)"},
|
|
233 |
@{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}]
|
|
234 |
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
235 |
val fresh_pred = @{term "fresh::string \<Rightarrow> trm \<Rightarrow> bool"}
|
210
|
236 |
val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}]
|
|
237 |
|
|
238 |
|
|
239 |
|
|
240 |
(* accessible-part example *)
|
|
241 |
val acc_rules =
|
|
242 |
[@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
243 |
val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}*}
|
210
|
244 |
text_raw{*
|
|
245 |
\end{isabelle}
|
|
246 |
\end{minipage}
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
\caption{Shorthands for the inductive predicates @{text "even"}/@{text "odd"},
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
248 |
@{text "fresh"} and @{text "accpart"}. The names of these shorthands follow
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
249 |
the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on.
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
250 |
The purpose of these shorthands is to simplify the construction of testcases
|
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
251 |
in Section~\ref{sec:code}.\label{fig:shorthands}}
|
210
|
252 |
\end{figure}
|
|
253 |
*}
|
|
254 |
|
|
255 |
|
|
256 |
|
32
|
257 |
end
|