doc-src/TutorialI/Misc/AdvancedInd.thy
author nipkow
Tue Aug 29 16:05:13 2000 +0200 (2000-08-29)
changeset 9723 a977245dfc8a
parent 9689 751fde5307e4
child 9792 bbefb6ce5cb2
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@9689
    12
subsection{*Massaging the proposition\label{sec:ind-var-in-prems}*};
nipkow@9645
    13
nipkow@9645
    14
text{*
nipkow@9645
    15
\noindent
nipkow@9645
    16
So far we have assumed that the theorem we want to prove is already in a form
nipkow@9645
    17
that is amenable to induction, but this is not always the case:
nipkow@9689
    18
*};
nipkow@9645
    19
nipkow@9645
    20
lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) = last xs";
nipkow@9645
    21
apply(induct_tac xs);
nipkow@9645
    22
nipkow@9645
    23
txt{*\noindent
nipkow@9645
    24
(where \isa{hd} and \isa{last} return the first and last element of a
nipkow@9645
    25
non-empty list)
nipkow@9645
    26
produces the warning
nipkow@9645
    27
\begin{quote}\tt
nipkow@9645
    28
Induction variable occurs also among premises!
nipkow@9645
    29
\end{quote}
nipkow@9645
    30
and leads to the base case
nipkow@9723
    31
\begin{isabelle}
nipkow@9645
    32
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
nipkow@9723
    33
\end{isabelle}
nipkow@9645
    34
which, after simplification, becomes
nipkow@9723
    35
\begin{isabelle}
nipkow@9645
    36
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
nipkow@9723
    37
\end{isabelle}
nipkow@9645
    38
We cannot prove this equality because we do not know what \isa{hd} and
nipkow@9645
    39
\isa{last} return when applied to \isa{[]}.
nipkow@9645
    40
nipkow@9645
    41
The point is that we have violated the above warning. Because the induction
nipkow@9645
    42
formula is only the conclusion, the occurrence of \isa{xs} in the premises is
nipkow@9645
    43
not modified by induction. Thus the case that should have been trivial
nipkow@9645
    44
becomes unprovable. Fortunately, the solution is easy:
nipkow@9645
    45
\begin{quote}
nipkow@9645
    46
\emph{Pull all occurrences of the induction variable into the conclusion
nipkow@9645
    47
using \isa{\isasymlongrightarrow}.}
nipkow@9645
    48
\end{quote}
nipkow@9645
    49
This means we should prove
nipkow@9689
    50
*};
nipkow@9689
    51
(*<*)oops;(*>*)
nipkow@9645
    52
lemma hd_rev: "xs \\<noteq> [] \\<longrightarrow> hd(rev xs) = last xs";
nipkow@9645
    53
(*<*)
nipkow@9689
    54
by(induct_tac xs, auto);
nipkow@9645
    55
(*>*)
nipkow@9645
    56
nipkow@9645
    57
text{*\noindent
nipkow@9645
    58
This time, induction leaves us with the following base case
nipkow@9723
    59
\begin{isabelle}
nipkow@9645
    60
\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
nipkow@9723
    61
\end{isabelle}
nipkow@9645
    62
which is trivial, and \isa{auto} finishes the whole proof.
nipkow@9645
    63
nipkow@9689
    64
If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
nipkow@9645
    65
really need the \isa{\isasymLongrightarrow}-version of \isa{hd\_rev}, for
nipkow@9645
    66
example because you want to apply it as an introduction rule, you need to
nipkow@9645
    67
derive it separately, by combining it with 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@9645
    81
Here is a simple example (which is proved by \isa{blast}):
nipkow@9689
    82
*};
nipkow@9645
    83
nipkow@9689
    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@9645
    89
application of modus ponens and \isa{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@9645
    95
or the wholesale stripping of \isa{\isasymforall} and
nipkow@9645
    96
\isa{\isasymlongrightarrow} in the conclusion via \isa{rulify} 
nipkow@9689
    97
*};
nipkow@9645
    98
nipkow@9689
    99
lemmas myrule = simple[rulify];
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
nipkow@9689
   107
lemma myrule[rulify]:  "\\<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@9645
   117
general, when inducting on some term $t$ you must rephrase the conclusion as
nipkow@9645
   118
\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$
nipkow@9645
   119
are the free variables in $t$ and $x$ is new, and perform induction on $x$
nipkow@9645
   120
afterwards. An example appears below.
nipkow@9689
   121
*};
nipkow@9645
   122
nipkow@9689
   123
subsection{*Beyond structural and recursion induction*};
nipkow@9645
   124
nipkow@9645
   125
text{*
nipkow@9645
   126
So far, inductive proofs where by structural induction for
nipkow@9645
   127
primitive recursive functions and recursion induction for total recursive
nipkow@9645
   128
functions. But sometimes structural induction is awkward and there is no
nipkow@9645
   129
recursive function in sight either that could furnish a more appropriate
nipkow@9645
   130
induction schema. In such cases some existing standard induction schema can
nipkow@9645
   131
be helpful. We show how to apply such induction schemas by an example.
nipkow@9645
   132
nipkow@9645
   133
Structural induction on \isa{nat} is
nipkow@9645
   134
usually known as ``mathematical induction''. There is also ``complete
nipkow@9645
   135
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
nipkow@9645
   136
holds for all $m<n$. In Isabelle, this is the theorem \isa{less\_induct}:
nipkow@9645
   137
\begin{quote}
nipkow@9689
   138
@{thm[display]"less_induct"[no_vars]}
nipkow@9645
   139
\end{quote}
nipkow@9645
   140
Here is an example of its application.
nipkow@9689
   141
*};
nipkow@9645
   142
nipkow@9689
   143
consts f :: "nat => nat";
nipkow@9689
   144
axioms f_ax: "f(f(n)) < f(Suc(n))";
nipkow@9645
   145
nipkow@9645
   146
text{*\noindent
nipkow@9645
   147
From the above axiom\footnote{In general, the use of axioms is strongly
nipkow@9645
   148
discouraged, because of the danger of inconsistencies. The above axiom does
nipkow@9645
   149
not introduce an inconsistency because, for example, the identity function
nipkow@9645
   150
satisfies it.}
nipkow@9645
   151
for \isa{f} it follows that @{term"n <= f n"}, which can
nipkow@9645
   152
be proved by induction on @{term"f n"}. Following the recipy outlined
nipkow@9645
   153
above, we have to phrase the proposition as follows to allow induction:
nipkow@9689
   154
*};
nipkow@9645
   155
nipkow@9689
   156
lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
nipkow@9645
   157
nipkow@9645
   158
txt{*\noindent
nipkow@9645
   159
To perform induction on \isa{k} using \isa{less\_induct}, we use the same
nipkow@9645
   160
general induction method as for recursion induction (see
nipkow@9645
   161
\S\ref{sec:recdef-induction}):
nipkow@9689
   162
*};
nipkow@9645
   163
nipkow@9689
   164
apply(induct_tac k rule:less_induct);
nipkow@9645
   165
(*<*)
nipkow@9689
   166
apply(rule allI);
nipkow@9645
   167
apply(case_tac i);
nipkow@9645
   168
 apply(simp);
nipkow@9645
   169
(*>*)
nipkow@9645
   170
txt{*\noindent
nipkow@9645
   171
which leaves us with the following proof state:
nipkow@9723
   172
\begin{isabelle}
nipkow@9645
   173
\ 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
   174
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
nipkow@9723
   175
\end{isabelle}
nipkow@9645
   176
After stripping the \isa{\isasymforall i}, the proof continues with a case
nipkow@9645
   177
distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
nipkow@9645
   178
other case:
nipkow@9723
   179
\begin{isabelle}
nipkow@9645
   180
\ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
nipkow@9645
   181
\ \ \ \ \ \ \ {\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
   182
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
nipkow@9723
   183
\end{isabelle}
nipkow@9689
   184
*};
nipkow@9645
   185
nipkow@9645
   186
by(blast intro!: f_ax Suc_leI intro:le_less_trans);
nipkow@9645
   187
nipkow@9645
   188
text{*\noindent
nipkow@9645
   189
It is not surprising if you find the last step puzzling.
nipkow@9645
   190
The proof goes like this (writing \isa{j} instead of \isa{nat}).
nipkow@9645
   191
Since @{term"i = Suc j"} it suffices to show
nipkow@9689
   192
@{term"j < f(Suc j)"} (by \isa{Suc\_leI}: @{thm"Suc_leI"[no_vars]}). This is
nipkow@9645
   193
proved as follows. From \isa{f\_ax} we have @{term"f (f j) < f (Suc j)"}
nipkow@9645
   194
(1) which implies @{term"f j <= f (f j)"} (by the induction hypothesis).
nipkow@9645
   195
Using (1) once more we obtain @{term"f j < f(Suc j)"} (2) by transitivity
nipkow@9689
   196
(\isa{le_less_trans}: @{thm"le_less_trans"[no_vars]}).
nipkow@9645
   197
Using the induction hypothesis once more we obtain @{term"j <= f j"}
nipkow@9645
   198
which, together with (2) yields @{term"j < f (Suc j)"} (again by
nipkow@9645
   199
\isa{le_less_trans}).
nipkow@9645
   200
nipkow@9645
   201
This last step shows both the power and the danger of automatic proofs: they
nipkow@9645
   202
will usually not tell you how the proof goes, because it can be very hard to
nipkow@9645
   203
translate the internal proof into a human-readable format. Therefore
nipkow@9645
   204
\S\ref{sec:part2?} introduces a language for writing readable yet concise
nipkow@9645
   205
proofs.
nipkow@9645
   206
nipkow@9645
   207
We can now derive the desired @{term"i <= f i"} from \isa{f\_incr}:
nipkow@9689
   208
*};
nipkow@9645
   209
nipkow@9645
   210
lemmas f_incr = f_incr_lem[rulify, OF refl];
nipkow@9645
   211
nipkow@9689
   212
text{*\noindent
nipkow@9645
   213
The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could
nipkow@9645
   214
have included this derivation in the original statement of the lemma:
nipkow@9689
   215
*};
nipkow@9645
   216
nipkow@9689
   217
lemma f_incr[rulify, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
nipkow@9689
   218
(*<*)oops;(*>*)
nipkow@9645
   219
nipkow@9645
   220
text{*
nipkow@9645
   221
\begin{exercise}
nipkow@9645
   222
From the above axiom and lemma for \isa{f} show that \isa{f} is the identity.
nipkow@9645
   223
\end{exercise}
nipkow@9645
   224
nipkow@9645
   225
In general, \isa{induct\_tac} can be applied with any rule \isa{r}
nipkow@9645
   226
whose conclusion is of the form \isa{?P ?x1 \dots ?xn}, in which case the
nipkow@9645
   227
format is
nipkow@9645
   228
\begin{ttbox}
nipkow@9645
   229
apply(induct_tac y1 ... yn rule: r)
nipkow@9645
   230
\end{ttbox}\index{*induct_tac}%
nipkow@9645
   231
where \isa{y1}, \dots, \isa{yn} are variables in the first subgoal.
nipkow@9645
   232
In fact, \isa{induct\_tac} even allows the conclusion of
nipkow@9645
   233
\isa{r} to be an (iterated) conjunction of formulae of the above form, in
nipkow@9645
   234
which case the application is
nipkow@9645
   235
\begin{ttbox}
nipkow@9645
   236
apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)
nipkow@9645
   237
\end{ttbox}
nipkow@9689
   238
*};
nipkow@9645
   239
nipkow@9689
   240
subsection{*Derivation of new induction schemas*};
nipkow@9689
   241
nipkow@9689
   242
text{*\label{sec:derive-ind}
nipkow@9689
   243
Induction schemas are ordinary theorems and you can derive new ones
nipkow@9689
   244
whenever you wish.  This section shows you how to, using the example
nipkow@9689
   245
of \isa{less\_induct}. Assume we only have structural induction
nipkow@9689
   246
available for @{typ"nat"} and want to derive complete induction. This
nipkow@9689
   247
requires us to generalize the statement first:
nipkow@9689
   248
*};
nipkow@9689
   249
nipkow@9689
   250
lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> \\<forall>m<n. P m";
nipkow@9689
   251
apply(induct_tac n);
nipkow@9689
   252
nipkow@9689
   253
txt{*\noindent
nipkow@9689
   254
The base case is trivially true. For the induction step (@{term"m <
nipkow@9689
   255
Suc n"}) we distinguish two cases: @{term"m < n"} is true by induction
nipkow@9689
   256
hypothesis and @{term"m = n"} follow from the assumption again using
nipkow@9689
   257
the induction hypothesis:
nipkow@9689
   258
*};
nipkow@9689
   259
nipkow@9689
   260
apply(blast);
nipkow@9689
   261
(* apply(blast elim:less_SucE); *)
nipkow@9689
   262
ML"set quick_and_dirty"
nipkow@9689
   263
sorry;
nipkow@9689
   264
ML"reset quick_and_dirty"
nipkow@9689
   265
nipkow@9689
   266
text{*\noindent
nipkow@9689
   267
The elimination rule \isa{less_SucE} expresses the case distinction:
nipkow@9689
   268
\begin{quote}
nipkow@9689
   269
@{thm[display]"less_SucE"[no_vars]}
nipkow@9689
   270
\end{quote}
nipkow@9689
   271
nipkow@9689
   272
Now it is straightforward to derive the original version of
nipkow@9689
   273
\isa{less\_induct} by manipulting the conclusion of the above lemma:
nipkow@9689
   274
instantiate \isa{n} by @{term"Suc n"} and \isa{m} by \isa{n} and
nipkow@9689
   275
remove the trivial condition @{term"n < Sc n"}. Fortunately, this
nipkow@9689
   276
happens automatically when we add the lemma as a new premise to the
nipkow@9689
   277
desired goal:
nipkow@9689
   278
*};
nipkow@9689
   279
nipkow@9689
   280
theorem less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> P n";
nipkow@9689
   281
by(insert induct_lem, blast);
nipkow@9689
   282
nipkow@9689
   283
text{*\noindent
nipkow@9645
   284
Finally we should mention that HOL already provides the mother of all
nipkow@9645
   285
inductions, \emph{wellfounded induction} (\isa{wf\_induct}):
nipkow@9645
   286
\begin{quote}
nipkow@9689
   287
@{thm[display]"wf_induct"[no_vars]}
nipkow@9645
   288
\end{quote}
nipkow@9689
   289
where @{term"wf r"} means that the relation \isa{r} is wellfounded.
nipkow@9689
   290
For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on @{typ"nat"}.
nipkow@9645
   291
For details see the library.
nipkow@9689
   292
*};
nipkow@9645
   293
nipkow@9645
   294
(*<*)
nipkow@9645
   295
end
nipkow@9645
   296
(*>*)