doc-src/TutorialI/Misc/AdvancedInd.thy
author nipkow
Tue Oct 17 13:28:57 2000 +0200 (2000-10-17)
changeset 10236 7626cb4e1407
parent 10217 e61e7e1eacaf
child 10241 e0428c2778f1
permissions -rw-r--r--
*** empty log message ***
nipkow@9645
     1
(*<*)
nipkow@9645
     2
theory AdvancedInd = Main:;
nipkow@9645
     3
(*>*)
nipkow@9645
     4
nipkow@9645
     5
text{*\noindent
nipkow@9645
     6
Now that we have learned about rules and logic, we take another look at the
nipkow@9645
     7
finer points of induction. The two questions we answer are: what to do if the
nipkow@9645
     8
proposition to be proved is not directly amenable to induction, and how to
nipkow@9645
     9
utilize and even derive new induction schemas.
nipkow@9689
    10
*};
nipkow@9645
    11
nipkow@10217
    12
subsection{*Massaging the proposition*};
nipkow@9645
    13
nipkow@10217
    14
text{*\label{sec:ind-var-in-prems}
nipkow@9645
    15
So far we have assumed that the theorem we want to prove is already in a form
nipkow@9645
    16
that is amenable to induction, but this is not always the case:
nipkow@9689
    17
*};
nipkow@9645
    18
nipkow@9933
    19
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";
nipkow@9645
    20
apply(induct_tac xs);
nipkow@9645
    21
nipkow@9645
    22
txt{*\noindent
nipkow@9792
    23
(where @{term"hd"} and @{term"last"} return the first and last element of a
nipkow@9645
    24
non-empty list)
nipkow@9645
    25
produces the warning
nipkow@9645
    26
\begin{quote}\tt
nipkow@9645
    27
Induction variable occurs also among premises!
nipkow@9645
    28
\end{quote}
nipkow@9645
    29
and leads to the base case
nipkow@9723
    30
\begin{isabelle}
nipkow@9645
    31
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
nipkow@9723
    32
\end{isabelle}
nipkow@9645
    33
which, after simplification, becomes
nipkow@9723
    34
\begin{isabelle}
nipkow@9645
    35
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
nipkow@9723
    36
\end{isabelle}
nipkow@9792
    37
We cannot prove this equality because we do not know what @{term"hd"} and
nipkow@9792
    38
@{term"last"} return when applied to @{term"[]"}.
nipkow@9645
    39
nipkow@9645
    40
The point is that we have violated the above warning. Because the induction
nipkow@9792
    41
formula is only the conclusion, the occurrence of @{term"xs"} in the premises is
nipkow@9645
    42
not modified by induction. Thus the case that should have been trivial
nipkow@9645
    43
becomes unprovable. Fortunately, the solution is easy:
nipkow@9645
    44
\begin{quote}
nipkow@9645
    45
\emph{Pull all occurrences of the induction variable into the conclusion
nipkow@9792
    46
using @{text"\<longrightarrow>"}.}
nipkow@9645
    47
\end{quote}
nipkow@9645
    48
This means we should prove
nipkow@9689
    49
*};
nipkow@9689
    50
(*<*)oops;(*>*)
nipkow@9933
    51
lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
nipkow@9645
    52
(*<*)
nipkow@9689
    53
by(induct_tac xs, auto);
nipkow@9645
    54
(*>*)
nipkow@9645
    55
nipkow@9645
    56
text{*\noindent
nipkow@9645
    57
This time, induction leaves us with the following base case
nipkow@9723
    58
\begin{isabelle}
nipkow@9645
    59
\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
nipkow@9723
    60
\end{isabelle}
nipkow@9792
    61
which is trivial, and @{text"auto"} finishes the whole proof.
nipkow@9645
    62
nipkow@9792
    63
If @{thm[source]hd_rev} is meant to be a simplification rule, you are
nipkow@9792
    64
done. But if you really need the @{text"\<Longrightarrow>"}-version of
nipkow@9792
    65
@{thm[source]hd_rev}, for example because you want to apply it as an
nipkow@9792
    66
introduction rule, you need to derive it separately, by combining it with
nipkow@9792
    67
modus ponens:
nipkow@9689
    68
*};
nipkow@9645
    69
nipkow@9689
    70
lemmas hd_revI = hd_rev[THEN mp];
nipkow@9645
    71
 
nipkow@9645
    72
text{*\noindent
nipkow@9645
    73
which yields the lemma we originally set out to prove.
nipkow@9645
    74
nipkow@9645
    75
In case there are multiple premises $A@1$, \dots, $A@n$ containing the
nipkow@9645
    76
induction variable, you should turn the conclusion $C$ into
nipkow@9645
    77
\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
nipkow@9645
    78
(see the remark?? in \S\ref{??}).
nipkow@9645
    79
Additionally, you may also have to universally quantify some other variables,
nipkow@9645
    80
which can yield a fairly complex conclusion.
nipkow@9792
    81
Here is a simple example (which is proved by @{text"blast"}):
nipkow@9689
    82
*};
nipkow@9645
    83
nipkow@9933
    84
lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
nipkow@9689
    85
(*<*)by blast;(*>*)
nipkow@9645
    86
nipkow@9645
    87
text{*\noindent
nipkow@9645
    88
You can get the desired lemma by explicit
nipkow@9792
    89
application of modus ponens and @{thm[source]spec}:
nipkow@9689
    90
*};
nipkow@9645
    91
nipkow@9689
    92
lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
nipkow@9645
    93
nipkow@9645
    94
text{*\noindent
nipkow@9792
    95
or the wholesale stripping of @{text"\<forall>"} and
wenzelm@9941
    96
@{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"} 
nipkow@9689
    97
*};
nipkow@9645
    98
wenzelm@9941
    99
lemmas myrule = simple[rule_format];
nipkow@9645
   100
nipkow@9645
   101
text{*\noindent
nipkow@9689
   102
yielding @{thm"myrule"[no_vars]}.
nipkow@9645
   103
You can go one step further and include these derivations already in the
nipkow@9645
   104
statement of your original lemma, thus avoiding the intermediate step:
nipkow@9689
   105
*};
nipkow@9645
   106
wenzelm@9941
   107
lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
nipkow@9645
   108
(*<*)
nipkow@9689
   109
by blast;
nipkow@9645
   110
(*>*)
nipkow@9645
   111
nipkow@9645
   112
text{*
nipkow@9645
   113
\bigskip
nipkow@9645
   114
nipkow@9645
   115
A second reason why your proposition may not be amenable to induction is that
nipkow@9645
   116
you want to induct on a whole term, rather than an individual variable. In
nipkow@10217
   117
general, when inducting on some term $t$ you must rephrase the conclusion $C$
nipkow@10217
   118
as
nipkow@10217
   119
\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \]
nipkow@10217
   120
where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
nipkow@10217
   121
perform induction on $x$ afterwards. An example appears in
nipkow@10217
   122
\S\ref{sec:complete-ind} below.
nipkow@10217
   123
nipkow@10217
   124
The very same problem may occur in connection with rule induction. Remember
nipkow@10217
   125
that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
nipkow@10217
   126
some inductively defined set and the $x@i$ are variables.  If instead we have
nipkow@10217
   127
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
nipkow@10217
   128
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
nipkow@10217
   129
\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
nipkow@10217
   130
For an example see \S\ref{sec:CTL-revisited} below.
nipkow@9689
   131
*};
nipkow@9645
   132
nipkow@9689
   133
subsection{*Beyond structural and recursion induction*};
nipkow@9645
   134
nipkow@10217
   135
text{*\label{sec:complete-ind}
nipkow@9645
   136
So far, inductive proofs where by structural induction for
nipkow@9645
   137
primitive recursive functions and recursion induction for total recursive
nipkow@9645
   138
functions. But sometimes structural induction is awkward and there is no
nipkow@9645
   139
recursive function in sight either that could furnish a more appropriate
nipkow@9645
   140
induction schema. In such cases some existing standard induction schema can
nipkow@9645
   141
be helpful. We show how to apply such induction schemas by an example.
nipkow@9645
   142
nipkow@9792
   143
Structural induction on @{typ"nat"} is
nipkow@9645
   144
usually known as ``mathematical induction''. There is also ``complete
nipkow@9645
   145
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
nipkow@9933
   146
holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
nipkow@9933
   147
@{thm[display]"nat_less_induct"[no_vars]}
nipkow@9645
   148
Here is an example of its application.
nipkow@9689
   149
*};
nipkow@9645
   150
nipkow@9689
   151
consts f :: "nat => nat";
nipkow@9689
   152
axioms f_ax: "f(f(n)) < f(Suc(n))";
nipkow@9645
   153
nipkow@9645
   154
text{*\noindent
nipkow@9645
   155
From the above axiom\footnote{In general, the use of axioms is strongly
nipkow@9645
   156
discouraged, because of the danger of inconsistencies. The above axiom does
nipkow@9645
   157
not introduce an inconsistency because, for example, the identity function
nipkow@9645
   158
satisfies it.}
nipkow@9792
   159
for @{term"f"} it follows that @{prop"n <= f n"}, which can
nipkow@9645
   160
be proved by induction on @{term"f n"}. Following the recipy outlined
nipkow@9645
   161
above, we have to phrase the proposition as follows to allow induction:
nipkow@9689
   162
*};
nipkow@9645
   163
nipkow@9933
   164
lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
nipkow@9645
   165
nipkow@9645
   166
txt{*\noindent
nipkow@9933
   167
To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same
nipkow@9645
   168
general induction method as for recursion induction (see
nipkow@9645
   169
\S\ref{sec:recdef-induction}):
nipkow@9689
   170
*};
nipkow@9645
   171
wenzelm@9923
   172
apply(induct_tac k rule: nat_less_induct);
nipkow@9645
   173
(*<*)
nipkow@9689
   174
apply(rule allI);
nipkow@9645
   175
apply(case_tac i);
nipkow@9645
   176
 apply(simp);
nipkow@9645
   177
(*>*)
nipkow@9645
   178
txt{*\noindent
nipkow@9645
   179
which leaves us with the following proof state:
nipkow@9723
   180
\begin{isabelle}
nipkow@9645
   181
\ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
nipkow@9645
   182
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
nipkow@9723
   183
\end{isabelle}
nipkow@9792
   184
After stripping the @{text"\<forall>i"}, the proof continues with a case
nipkow@9792
   185
distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on
nipkow@9792
   186
the other case:
nipkow@9723
   187
\begin{isabelle}
nipkow@9645
   188
\ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
nipkow@9645
   189
\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
nipkow@9645
   190
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
nipkow@9723
   191
\end{isabelle}
nipkow@9689
   192
*};
nipkow@9645
   193
wenzelm@9923
   194
by(blast intro!: f_ax Suc_leI intro: le_less_trans);
nipkow@9645
   195
nipkow@9645
   196
text{*\noindent
nipkow@9645
   197
It is not surprising if you find the last step puzzling.
nipkow@9792
   198
The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
nipkow@9792
   199
Since @{prop"i = Suc j"} it suffices to show
nipkow@9792
   200
@{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is
nipkow@9792
   201
proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
nipkow@9792
   202
(1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).
nipkow@9792
   203
Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity
nipkow@9792
   204
(@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).
nipkow@9792
   205
Using the induction hypothesis once more we obtain @{prop"j <= f j"}
nipkow@9792
   206
which, together with (2) yields @{prop"j < f (Suc j)"} (again by
nipkow@9792
   207
@{thm[source]le_less_trans}).
nipkow@9645
   208
nipkow@9645
   209
This last step shows both the power and the danger of automatic proofs: they
nipkow@9645
   210
will usually not tell you how the proof goes, because it can be very hard to
nipkow@9645
   211
translate the internal proof into a human-readable format. Therefore
nipkow@9645
   212
\S\ref{sec:part2?} introduces a language for writing readable yet concise
nipkow@9645
   213
proofs.
nipkow@9645
   214
nipkow@9792
   215
We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
nipkow@9689
   216
*};
nipkow@9645
   217
wenzelm@9941
   218
lemmas f_incr = f_incr_lem[rule_format, OF refl];
nipkow@9645
   219
nipkow@9689
   220
text{*\noindent
nipkow@9792
   221
The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
nipkow@9792
   222
we could have included this derivation in the original statement of the lemma:
nipkow@9689
   223
*};
nipkow@9645
   224
wenzelm@9941
   225
lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
nipkow@9689
   226
(*<*)oops;(*>*)
nipkow@9645
   227
nipkow@9645
   228
text{*
nipkow@9645
   229
\begin{exercise}
nipkow@9792
   230
From the above axiom and lemma for @{term"f"} show that @{term"f"} is the
nipkow@9792
   231
identity.
nipkow@9645
   232
\end{exercise}
nipkow@9645
   233
nipkow@10236
   234
In general, @{text induct_tac} can be applied with any rule $r$
nipkow@9792
   235
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
nipkow@9645
   236
format is
nipkow@9792
   237
\begin{quote}
nipkow@9792
   238
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
nipkow@9792
   239
\end{quote}\index{*induct_tac}%
nipkow@9792
   240
where $y@1, \dots, y@n$ are variables in the first subgoal.
nipkow@10236
   241
A further example of a useful induction rule is @{thm[source]length_induct},
nipkow@10236
   242
induction on the length of a list:\indexbold{*length_induct}
nipkow@10236
   243
@{thm[display]length_induct[no_vars]}
nipkow@10236
   244
nipkow@9792
   245
In fact, @{text"induct_tac"} even allows the conclusion of
nipkow@9792
   246
$r$ to be an (iterated) conjunction of formulae of the above form, in
nipkow@9645
   247
which case the application is
nipkow@9792
   248
\begin{quote}
nipkow@9792
   249
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}
nipkow@9792
   250
\end{quote}
nipkow@9689
   251
*};
nipkow@9645
   252
nipkow@9689
   253
subsection{*Derivation of new induction schemas*};
nipkow@9689
   254
nipkow@9689
   255
text{*\label{sec:derive-ind}
nipkow@9689
   256
Induction schemas are ordinary theorems and you can derive new ones
nipkow@9689
   257
whenever you wish.  This section shows you how to, using the example
nipkow@9933
   258
of @{thm[source]nat_less_induct}. Assume we only have structural induction
nipkow@9689
   259
available for @{typ"nat"} and want to derive complete induction. This
nipkow@9689
   260
requires us to generalize the statement first:
nipkow@9689
   261
*};
nipkow@9689
   262
nipkow@9933
   263
lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
nipkow@9689
   264
apply(induct_tac n);
nipkow@9689
   265
nipkow@9689
   266
txt{*\noindent
nipkow@9792
   267
The base case is trivially true. For the induction step (@{prop"m <
nipkow@9933
   268
Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
nipkow@9933
   269
hypothesis and case @{prop"m = n"} follows from the assumption, again using
nipkow@9689
   270
the induction hypothesis:
nipkow@9689
   271
*};
nipkow@9689
   272
apply(blast);
nipkow@9933
   273
by(blast elim:less_SucE)
nipkow@9689
   274
nipkow@9689
   275
text{*\noindent
nipkow@9792
   276
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
nipkow@9689
   277
@{thm[display]"less_SucE"[no_vars]}
nipkow@9689
   278
nipkow@9689
   279
Now it is straightforward to derive the original version of
nipkow@9933
   280
@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
nipkow@9792
   281
instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
nipkow@9792
   282
remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
nipkow@9689
   283
happens automatically when we add the lemma as a new premise to the
nipkow@9689
   284
desired goal:
nipkow@9689
   285
*};
nipkow@9689
   286
nipkow@9933
   287
theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
nipkow@9689
   288
by(insert induct_lem, blast);
nipkow@9689
   289
nipkow@9933
   290
text{*
nipkow@10186
   291
nipkow@9645
   292
Finally we should mention that HOL already provides the mother of all
nipkow@10186
   293
inductions, \textbf{wellfounded
nipkow@10186
   294
induction}\indexbold{induction!wellfounded}\index{wellfounded
nipkow@10186
   295
induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
nipkow@10186
   296
@{thm[display]wf_induct[no_vars]}
nipkow@10186
   297
where @{term"wf r"} means that the relation @{term r} is wellfounded
nipkow@10186
   298
(see \S\ref{sec:wellfounded}).
nipkow@9933
   299
For example, theorem @{thm[source]nat_less_induct} can be viewed (and
nipkow@9933
   300
derived) as a special case of @{thm[source]wf_induct} where 
nipkow@10186
   301
@{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.
nipkow@10186
   302
For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.
nipkow@9689
   303
*};
nipkow@9645
   304
nipkow@9645
   305
(*<*)
nipkow@9645
   306
end
nipkow@9645
   307
(*>*)