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