127
+ − 1
theory Ind_Prelims
219
+ − 2
imports Main LaTeXsugar "../Base"
32
+ − 3
begin
+ − 4
127
+ − 5
section{* Preliminaries *}
+ − 6
32
+ − 7
text {*
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 8
The user will just give a specification of inductive predicate(s) and
129
+ − 9
expects from the package to produce a convenient reasoning
+ − 10
infrastructure. This infrastructure needs to be derived from the definition
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
that correspond to the specified predicate(s). Before we start with
219
+ − 12
explaining all parts of the package, let us first give some examples
+ − 13
showing how to define inductive predicates and then also how
+ − 14
to generate a reasoning infrastructure for them. From the examples
+ − 15
we will figure out a general method for
+ − 16
defining inductive predicates. The aim in this section is \emph{not} to
+ − 17
write proofs that are as beautiful as possible, but as close as possible to
+ − 18
the ML-code we will develop in later sections.
129
+ − 19
219
+ − 20
+ − 21
+ − 22
We first consider the transitive closure of a relation @{text R}. The
+ − 23
``pencil-and-paper'' specification for the transitive closure is:
+ − 24
127
+ − 25
\begin{center}\small
116
+ − 26
@{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
+ − 27
@{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
88
+ − 28
\end{center}
+ − 29
224
+ − 30
The package has to make an appropriate definition for @{term "trcl"}.
+ − 31
Since an inductively
127
+ − 32
defined predicate is the least predicate closed under a collection of
+ − 33
introduction rules, the predicate @{text "trcl R x y"} can be defined so
+ − 34
that it holds if and only if @{text "P x y"} holds for every predicate
+ − 35
@{text P} closed under the rules above. This gives rise to the definition
32
+ − 36
*}
+ − 37
127
+ − 38
definition "trcl \<equiv>
+ − 39
\<lambda>R x y. \<forall>P. (\<forall>x. P x x)
+ − 40
\<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
32
+ − 41
+ − 42
text {*
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
We have to use the object implication @{text "\<longrightarrow>"} and object quantification
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
@{text "\<forall>"} for stating this definition (there is no other way for
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
definitions in HOL). However, the introduction rules and induction
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46
principles associated with the transitive closure should use the meta-connectives,
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
since they simplify the reasoning for the user.
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
32
+ − 49
127
+ − 50
With this definition, the proof of the induction principle for @{term trcl}
129
+ − 51
is almost immediate. It suffices to convert all the meta-level
116
+ − 52
connectives in the lemma to object-level connectives using the
219
+ − 53
proof method @{text atomize} (Line 4 below), expand the definition of @{term trcl}
127
+ − 54
(Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
and then solve the goal by @{text assumption} (Line 8).
113
+ − 56
32
+ − 57
*}
+ − 58
114
+ − 59
lemma %linenos trcl_induct:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
assumes "trcl R x y"
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
113
+ − 62
apply(atomize (full))
165
+ − 63
apply(cut_tac prems)
113
+ − 64
apply(unfold trcl_def)
+ − 65
apply(drule spec[where x=P])
+ − 66
apply(assumption)
+ − 67
done
88
+ − 68
113
+ − 69
text {*
127
+ − 70
The proofs for the introduction rules are slightly more complicated.
+ − 71
For the first one, we need to prove the following lemma:
+ − 72
*}
+ − 73
+ − 74
lemma %linenos trcl_base:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 75
shows "trcl R x x"
127
+ − 76
apply(unfold trcl_def)
+ − 77
apply(rule allI impI)+
+ − 78
apply(drule spec)
+ − 79
apply(assumption)
+ − 80
done
+ − 81
+ − 82
text {*
+ − 83
We again unfold first the definition and apply introduction rules
+ − 84
for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).
116
+ − 85
We then end up in the goal state:
113
+ − 86
*}
88
+ − 87
113
+ − 88
(*<*)lemma "trcl R x x"
115
+ − 89
apply (unfold trcl_def)
+ − 90
apply (rule allI impI)+(*>*)
113
+ − 91
txt {* @{subgoals [display]} *}
32
+ − 92
(*<*)oops(*>*)
88
+ − 93
113
+ − 94
text {*
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
The two assumptions come from the definition of @{term trcl} and correspond
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
to the introduction rules. Thus, all we have to do is to eliminate the
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
universal quantifier in front of the first assumption (Line 5), and then
219
+ − 98
solve the goal by @{text assumption} (Line 6).
113
+ − 99
*}
+ − 100
+ − 101
text {*
127
+ − 102
Next we have to show that the second introduction rule also follows from the
+ − 103
definition. Since this rule has premises, the proof is a bit more
+ − 104
involved. After unfolding the definitions and applying the introduction
+ − 105
rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
113
+ − 106
*}
+ − 107
127
+ − 108
lemma trcl_step:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 109
shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
115
+ − 110
apply (unfold trcl_def)
127
+ − 111
apply (rule allI impI)+
113
+ − 112
127
+ − 113
txt {*
+ − 114
we obtain the goal state
+ − 115
+ − 116
@{subgoals [display]}
+ − 117
+ − 118
To see better where we are, let us explicitly name the assumptions
+ − 119
by starting a subproof.
115
+ − 120
*}
+ − 121
+ − 122
proof -
+ − 123
case (goal1 P)
127
+ − 124
have p1: "R x y" by fact
+ − 125
have p2: "\<forall>P. (\<forall>x. P x x)
+ − 126
\<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
+ − 127
have r1: "\<forall>x. P x x" by fact
+ − 128
have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+ − 129
show "P x z"
+ − 130
+ − 131
txt {*
+ − 132
The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}
219
+ − 134
come from the definition of @{term trcl}. We apply @{text "r2"} to the goal
+ − 135
@{term "P x z"}. In order for this assumption to be applicable as a rule, we
127
+ − 136
have to eliminate the universal quantifier and turn the object-level
+ − 137
implications into meta-level ones. This can be accomplished using the @{text
+ − 138
rule_format} attribute. So we continue the proof with:
115
+ − 139
32
+ − 140
*}
113
+ − 141
127
+ − 142
apply (rule r2[rule_format])
88
+ − 143
127
+ − 144
txt {*
+ − 145
This gives us two new subgoals
+ − 146
+ − 147
@{subgoals [display]}
+ − 148
+ − 149
which can be solved using assumptions @{text p1} and @{text p2}. The latter
+ − 150
involves a quantifier and implications that have to be eliminated before it
+ − 151
can be applied. To avoid potential problems with higher-order unification,
+ − 152
we explicitly instantiate the quantifier to @{text "P"} and also match
+ − 153
explicitly the implications with @{text "r1"} and @{text "r2"}. This gives
+ − 154
the proof:
+ − 155
*}
+ − 156
+ − 157
apply(rule p1)
+ − 158
apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
115
+ − 159
done
+ − 160
qed
32
+ − 161
+ − 162
text {*
127
+ − 163
Now we are done. It might be surprising that we are not using the automatic
+ − 164
tactics available in Isabelle for proving this lemmas. After all @{text
+ − 165
"blast"} would easily dispense of it.
115
+ − 166
*}
88
+ − 167
127
+ − 168
lemma trcl_step_blast:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 169
shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
115
+ − 170
apply(unfold trcl_def)
+ − 171
apply(blast)
+ − 172
done
+ − 173
+ − 174
text {*
116
+ − 175
Experience has shown that it is generally a bad idea to rely heavily on
+ − 176
@{text blast}, @{text auto} and the like in automated proofs. The reason is
+ − 177
that you do not have precise control over them (the user can, for example,
+ − 178
declare new intro- or simplification rules that can throw automatic tactics
+ − 179
off course) and also it is very hard to debug proofs involving automatic
+ − 180
tactics whenever something goes wrong. Therefore if possible, automatic
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
tactics should be avoided or be constrained sufficiently.
115
+ − 182
116
+ − 183
The method of defining inductive predicates by impredicative quantification
+ − 184
also generalises to mutually inductive predicates. The next example defines
219
+ − 185
the predicates @{text even} and @{text odd} given by
32
+ − 186
219
+ − 187
\begin{center}\small
+ − 188
@{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
+ − 189
@{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
+ − 190
@{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
+ − 191
\end{center}
32
+ − 192
127
+ − 193
Since the predicates @{term even} and @{term odd} are mutually inductive, each
+ − 194
corresponding definition must quantify over both predicates (we name them
+ − 195
below @{text "P"} and @{text "Q"}).
+ − 196
*}
+ − 197
219
+ − 198
definition "even \<equiv>
127
+ − 199
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
+ − 200
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
+ − 201
219
+ − 202
definition "odd \<equiv>
127
+ − 203
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
+ − 204
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
32
+ − 205
+ − 206
text {*
116
+ − 207
For proving the induction principles, we use exactly the same technique
+ − 208
as in the transitive closure example, namely:
32
+ − 209
*}
+ − 210
+ − 211
lemma even_induct:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 212
assumes "even n"
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 213
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
115
+ − 214
apply(atomize (full))
165
+ − 215
apply(cut_tac prems)
115
+ − 216
apply(unfold even_def)
+ − 217
apply(drule spec[where x=P])
+ − 218
apply(drule spec[where x=Q])
+ − 219
apply(assumption)
+ − 220
done
32
+ − 221
+ − 222
text {*
127
+ − 223
The only difference with the proof @{text "trcl_induct"} is that we have to
+ − 224
instantiate here two universal quantifiers. We omit the other induction
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
principle that has @{prop "even n"} as premise and @{term "Q n"} as conclusion.
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
The proofs of the introduction rules are also very similar to the ones in
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 227
the @{text "trcl"}-example. We only show the proof of the second introduction
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 228
rule.
32
+ − 229
*}
+ − 230
127
+ − 231
lemma %linenos evenS:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 232
shows "odd m \<Longrightarrow> even (Suc m)"
115
+ − 233
apply (unfold odd_def even_def)
+ − 234
apply (rule allI impI)+
+ − 235
proof -
165
+ − 236
case (goal1 P Q)
127
+ − 237
have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
115
+ − 238
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
127
+ − 239
have r1: "P 0" by fact
+ − 240
have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
+ − 241
have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
115
+ − 242
show "P (Suc m)"
127
+ − 243
apply(rule r2[rule_format])
+ − 244
apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q],
+ − 245
THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
115
+ − 246
done
+ − 247
qed
88
+ − 248
32
+ − 249
text {*
219
+ − 250
The interesting lines are 7 to 15. The assumptions fall into two categories:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
@{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
to @{text "r3"} come from the definition of @{text "even"}.
127
+ − 253
In Line 13, we apply the assumption @{text "r2"} (since we prove the second
+ − 254
introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
+ − 255
the second introduction rule had more premises we have to do that for all
+ − 256
of them). In order for this assumption to be applicable, the quantifiers
+ − 257
need to be instantiated and then also the implications need to be resolved
+ − 258
with the other rules.
+ − 259
219
+ − 260
Next we define the accessible part of a relation @{text R} given by
+ − 261
the single rule:
+ − 262
+ − 263
\begin{center}\small
+ − 264
\mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+ − 265
\end{center}
+ − 266
+ − 267
The definition of @{text "accpart"} is:
32
+ − 268
*}
+ − 269
127
+ − 270
definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
32
+ − 271
+ − 272
text {*
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
The proof of the induction principle is again straightforward and omitted.
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 274
Proving the introduction rule is a little more complicated, because the
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275
quantifier and the implication in the premise. The proof is as follows.
115
+ − 276
*}
+ − 277
127
+ − 278
lemma %linenos accpartI:
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
115
+ − 280
apply (unfold accpart_def)
+ − 281
apply (rule allI impI)+
+ − 282
proof -
+ − 283
case (goal1 P)
127
+ − 284
have p1: "\<And>y. R y x \<Longrightarrow>
115
+ − 285
(\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
127
+ − 286
have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
115
+ − 287
show "P x"
127
+ − 288
apply(rule r1[rule_format])
115
+ − 289
proof -
+ − 290
case (goal1 y)
127
+ − 291
have r1_prem: "R y x" by fact
115
+ − 292
show "P y"
127
+ − 293
apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
115
+ − 294
done
+ − 295
qed
+ − 296
qed
+ − 297
+ − 298
text {*
219
+ − 299
As you can see, there are now two subproofs. The assumptions fall again into
+ − 300
two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
+ − 301
"r1"} generates a goal state with the new local assumption @{term "R y x"},
+ − 302
named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is
+ − 303
used to solve the goal @{term "P y"} with the help of assumption @{text
+ − 304
"p1"}.
+ − 305
124
+ − 306
219
+ − 307
\begin{exercise}
+ − 308
Give the definition for the freshness predicate for lambda-terms. The rules
+ − 309
for this predicate are:
+ − 310
+ − 311
\begin{center}\small
+ − 312
@{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm}
+ − 313
@{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm]
+ − 314
@{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm}
+ − 315
@{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
+ − 316
\end{center}
+ − 317
+ − 318
From the definition derive the induction principle and the introduction
+ − 319
rules.
+ − 320
\end{exercise}
+ − 321
+ − 322
The point of all these examples is to get a feeling what the automatic
+ − 323
proofs should do in order to solve all inductive definitions we throw at
+ − 324
them. This is usually the first step in writing a package. We next explain
129
+ − 325
the parsing and typing part of the package.
127
+ − 326
115
+ − 327
*}
129
+ − 328
(*<*)end(*>*)