210
+ − 1
theory Ind_General_Scheme
346
+ − 2
imports Ind_Intro 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
565
+ − 39
section \<open>The Code in a Nutshell\label{sec:nutshell}\<close>
210
+ − 40
+ − 41
565
+ − 42
text \<open>
212
+ − 43
The inductive package will generate the reasoning infrastructure for
565
+ − 44
mutually recursive predicates, say \<open>pred\<^sub>1\<dots>pred\<^sub>n\<close>. 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]
565
+ − 48
"\<^sup>*"}. The shorthand for the predicates will therefore be \<open>preds\<close> or \<open>pred\<^sup>*\<close>. In the case of the predicates there must
212
+ − 49
be, of course, at least a single one in order to obtain a meaningful
+ − 50
definition.
210
+ − 51
565
+ − 52
The input for the inductive package will be some \<open>preds\<close> with possible
210
+ − 53
typing and syntax annotations, and also some introduction rules. We call below the
565
+ − 54
introduction rules short as \<open>rules\<close>. Borrowing some idealised Isabelle
+ − 55
notation, one such \<open>rule\<close> is assumed to be of the form
210
+ − 56
+ − 57
\begin{isabelle}
565
+ − 58
\<open>rule ::=
+ − 59
\<And>xs. \<^latex>\<open>$\underbrace{\mbox{\<close>As\<^latex>\<open>}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$\<close> \<Longrightarrow>
+ − 60
\<^latex>\<open>$\underbrace{\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\text{\rm recursive premises}}$>\<close>
+ − 61
\<Longrightarrow> pred ts\<close>
210
+ − 62
\end{isabelle}
+ − 63
565
+ − 64
For the purposes here, we will assume the \<open>rules\<close> have this format and
278
+ − 65
omit any code that actually tests this. Therefore ``things'' can go horribly
565
+ − 66
wrong, if the \<open>rules\<close> are not of this form. The \<open>As\<close> and
+ − 67
\<open>Bs\<close> in a \<open>rule\<close> stand for formulae not involving the
+ − 68
inductive predicates \<open>preds\<close>; the instances \<open>pred ss\<close> and
+ − 69
\<open>pred ts\<close> can stand for different predicates, like \<open>pred\<^sub>1 ss\<close> and \<open>pred\<^sub>2 ts\<close>, in case mutual recursive
+ − 70
predicates are defined; the terms \<open>ss\<close> and \<open>ts\<close> are the
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred
565
+ − 72
ts"} is a premise of the rule. The outermost quantified variables \<open>xs\<close> are usually omitted in the user's input. The quantification for the
+ − 73
variables \<open>ys\<close> is local with respect to one recursive premise and
+ − 74
must be given. Some examples of \<open>rule\<close>s are
278
+ − 75
210
+ − 76
+ − 77
@{thm [display] fresh_var[no_vars]}
+ − 78
+ − 79
which has only a single non-recursive premise, whereas
+ − 80
+ − 81
@{thm [display] evenS[no_vars]}
+ − 82
+ − 83
has a single recursive premise; the rule
+ − 84
+ − 85
@{thm [display] accpartI[no_vars]}
+ − 86
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 87
has a single recursive premise that has a precondition. As is custom all
565
+ − 88
rules are stated without the leading meta-quantification \<open>\<And>xs\<close>.
210
+ − 89
215
+ − 90
The output of the inductive package will be definitions for the predicates,
+ − 91
induction principles and introduction rules. For the definitions we need to have the
565
+ − 92
\<open>rules\<close> in a form where the meta-quantifiers and meta-implications are
+ − 93
replaced by their object logic equivalents. Therefore an \<open>orule\<close> is
215
+ − 94
of the form
210
+ − 95
551
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 96
@{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^sup>* \<longrightarrow> pred ts"}
210
+ − 97
565
+ − 98
A definition for the predicate \<open>pred\<close> has then the form
210
+ − 99
+ − 100
@{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+ − 101
565
+ − 102
The induction principles for every predicate \<open>pred\<close> are of the
210
+ − 103
form
+ − 104
+ − 105
@{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
+ − 106
565
+ − 107
where in the \<open>rules\<close>-part every \<open>pred\<close> is replaced by a fresh
+ − 108
schematic variable \<open>?P\<close>.
210
+ − 109
565
+ − 110
In order to derive an induction principle for the predicate \<open>pred\<close>,
+ − 111
we first transform \<open>ind\<close> into the object logic and fix the schematic variables.
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
+ − 112
Hence we have to prove a formula of the form
210
+ − 113
+ − 114
@{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
+ − 115
565
+ − 116
If we assume \<open>pred zs\<close> and unfold its definition, then we have an
212
+ − 117
assumption
210
+ − 118
+ − 119
@{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"}
+ − 120
212
+ − 121
and must prove the goal
210
+ − 122
+ − 123
@{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
+ − 124
565
+ − 125
This can be done by instantiating the \<open>\<forall>preds\<close>-quantification
+ − 126
with the \<open>Ps\<close>. Then we are done since we are left with a simple
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
+ − 127
identity.
210
+ − 128
565
+ − 129
Although the user declares the introduction rules \<open>rules\<close>, they must
+ − 130
also be derived from the \<open>defs\<close>. 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
+ − 131
Assuming we want to prove the introduction rule
210
+ − 132
551
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 133
@{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
210
+ − 134
215
+ − 135
then we have assumptions of the form
210
+ − 136
+ − 137
\begin{isabelle}
565
+ − 138
(i)~~\<open>As\<close>\\
+ − 139
(ii)~\<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<close>
210
+ − 140
\end{isabelle}
+ − 141
212
+ − 142
and must show the goal
210
+ − 143
+ − 144
@{text [display] "pred ts"}
+ − 145
565
+ − 146
If we now unfold the definitions for the \<open>preds\<close>, we have assumptions
210
+ − 147
+ − 148
\begin{isabelle}
565
+ − 149
(i)~~~\<open>As\<close>\\
+ − 150
(ii)~~\<open>(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*\<close>\\
+ − 151
(iii)~\<open>orules\<close>
210
+ − 152
\end{isabelle}
+ − 153
+ − 154
and need to show
+ − 155
+ − 156
@{text [display] "pred ts"}
+ − 157
565
+ − 158
In the last step we removed some quantifiers and moved the precondition \<open>orules\<close>
+ − 159
into the assumption. The \<open>orules\<close> stand for all introduction rules that are given
+ − 160
by the user. We apply the \<open>orule\<close> that corresponds to introduction rule we are
278
+ − 161
proving. After transforming the object connectives into meta-connectives, this introduction
+ − 162
rule must necessarily be of the form
210
+ − 163
551
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 164
@{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
210
+ − 165
+ − 166
When we apply this rule we end up in the goal state where we have to prove
212
+ − 167
goals of the form
210
+ − 168
+ − 169
\begin{isabelle}
565
+ − 170
(a)~\<open>As\<close>\\
+ − 171
(b)~\<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<close>
210
+ − 172
\end{isabelle}
+ − 173
565
+ − 174
We can immediately discharge the goals \<open>As\<close> using the assumptions in
+ − 175
\<open>(i)\<close>. The goals in \<open>(b)\<close> can be discharged as follows: we
+ − 176
assume the \<open>Bs\<close> and prove \<open>pred ss\<close>. For this we resolve the
+ − 177
\<open>Bs\<close> with the assumptions in \<open>(ii)\<close>. This gives us the
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
assumptions
210
+ − 179
551
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 180
@{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}
210
+ − 181
+ − 182
Instantiating the universal quantifiers and then resolving with the assumptions
565
+ − 183
in \<open>(iii)\<close> gives us \<open>pred ss\<close>, 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
+ − 184
This completes the proof for introduction rules.
210
+ − 185
215
+ − 186
What remains is to implement in Isabelle the reasoning outlined in this section.
+ − 187
We will describe the code in the next section. For building testcases, we use the shorthands for
565
+ − 188
\<open>even/odd\<close>, @{term "fresh"} and @{term "accpart"}
215
+ − 189
defined in Figure~\ref{fig:shorthands}.
565
+ − 190
\<close>
210
+ − 191
+ − 192
565
+ − 193
text_raw\<open>
210
+ − 194
\begin{figure}[p]
+ − 195
\begin{minipage}{\textwidth}
565
+ − 196
\begin{isabelle}\<close>
+ − 197
ML %grayML\<open>(* even-odd example *)
210
+ − 198
val eo_defs = [@{thm even_def}, @{thm odd_def}]
+ − 199
+ − 200
val eo_rules =
+ − 201
[@{prop "even 0"},
+ − 202
@{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
+ − 203
@{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
+ − 204
+ − 205
val eo_orules =
+ − 206
[@{prop "even 0"},
+ − 207
@{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
+ − 208
@{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
+ − 209
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
val eo_preds = [@{term "even::nat \<Rightarrow> bool"}, @{term "odd::nat \<Rightarrow> bool"}]
210
+ − 211
val eo_prednames = [@{binding "even"}, @{binding "odd"}]
237
+ − 212
val eo_mxs = [NoSyn, NoSyn]
210
+ − 213
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
+ − 214
val e_pred = @{term "even::nat \<Rightarrow> bool"}
210
+ − 215
val e_arg_tys = [@{typ "nat"}]
+ − 216
+ − 217
+ − 218
+ − 219
(* freshness example *)
+ − 220
val fresh_rules =
+ − 221
[@{prop "\<And>a b. a \<noteq> b \<Longrightarrow> fresh a (Var b)"},
+ − 222
@{prop "\<And>a s t. fresh a t \<Longrightarrow> fresh a s \<Longrightarrow> fresh a (App t s)"},
+ − 223
@{prop "\<And>a t. fresh a (Lam a t)"},
+ − 224
@{prop "\<And>a b t. a \<noteq> b \<Longrightarrow> fresh a t \<Longrightarrow> fresh a (Lam b t)"}]
+ − 225
+ − 226
val fresh_orules =
+ − 227
[@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"},
+ − 228
@{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"},
+ − 229
@{prop "\<forall>a t. fresh a (Lam a t)"},
+ − 230
@{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}]
+ − 231
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 232
val fresh_pred = @{term "fresh::string \<Rightarrow> trm \<Rightarrow> bool"}
210
+ − 233
val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}]
+ − 234
+ − 235
+ − 236
+ − 237
(* accessible-part example *)
+ − 238
val acc_rules =
+ − 239
[@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
565
+ − 240
val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}\<close>
+ − 241
text_raw\<open>
210
+ − 242
\end{isabelle}
+ − 243
\end{minipage}
565
+ − 244
\caption{Shorthands for the inductive predicates \<open>even\<close>/\<open>odd\<close>,
+ − 245
\<open>fresh\<close> and \<open>accpart\<close>. The names of these shorthands follow
+ − 246
the convention \<open>rules\<close>, \<open>orules\<close>, \<open>preds\<close> and so on.
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
+ − 247
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
+ − 248
in Section~\ref{sec:code}.\label{fig:shorthands}}
210
+ − 249
\end{figure}
565
+ − 250
\<close>
210
+ − 251
+ − 252
+ − 253
32
+ − 254
end