src/Doc/Tutorial/Misc/AdvancedInd.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48994 c84278efa9d5
child 63178 b9e1d53124f5
permissions -rw-r--r--
eliminated spurious semicolons;
nipkow@9645
     1
(*<*)
wenzelm@58860
     2
theory AdvancedInd imports Main begin
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
paulson@11494
     7
finer points of induction.  We consider two questions: 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}).
wenzelm@58860
    12
*}
nipkow@9645
    13
wenzelm@58860
    14
subsection{*Massaging the Proposition*}
nipkow@9645
    15
nipkow@10217
    16
text{*\label{sec:ind-var-in-prems}
paulson@11494
    17
Often we have assumed that the theorem to be proved is already in a form
paulson@10885
    18
that is amenable to induction, but sometimes it isn't.
paulson@10885
    19
Here is an example.
paulson@10885
    20
Since @{term"hd"} and @{term"last"} return the first and last element of a
paulson@10885
    21
non-empty list, this lemma looks easy to prove:
wenzelm@58860
    22
*}
nipkow@9645
    23
paulson@10885
    24
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
paulson@10885
    25
apply(induct_tac xs)
nipkow@9645
    26
nipkow@9645
    27
txt{*\noindent
paulson@10885
    28
But induction produces the warning
nipkow@9645
    29
\begin{quote}\tt
nipkow@9645
    30
Induction variable occurs also among premises!
nipkow@9645
    31
\end{quote}
nipkow@9645
    32
and leads to the base case
nipkow@10363
    33
@{subgoals[display,indent=0,goals_limit=1]}
paulson@11494
    34
Simplification reduces the base case to this:
nipkow@9723
    35
\begin{isabelle}
nipkow@9645
    36
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
nipkow@9723
    37
\end{isabelle}
nipkow@10242
    38
We cannot prove this equality because we do not know what @{term hd} and
nipkow@10242
    39
@{term last} return when applied to @{term"[]"}.
nipkow@9645
    40
paulson@10885
    41
We should not have ignored the warning. Because the induction
paulson@10885
    42
formula is only the conclusion, induction does not affect the occurrence of @{term xs} in the premises.  
paulson@10885
    43
Thus the case that should have been trivial
paulson@11494
    44
becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
nipkow@10242
    45
heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
nipkow@9645
    46
\begin{quote}
nipkow@9645
    47
\emph{Pull all occurrences of the induction variable into the conclusion
nipkow@9792
    48
using @{text"\<longrightarrow>"}.}
nipkow@9645
    49
\end{quote}
paulson@10885
    50
Thus we should state the lemma as an ordinary 
paulson@10885
    51
implication~(@{text"\<longrightarrow>"}), letting
paulson@11494
    52
\attrdx{rule_format} (\S\ref{sec:forward}) convert the
paulson@10885
    53
result to the usual @{text"\<Longrightarrow>"} form:
wenzelm@58860
    54
*}
wenzelm@58860
    55
(*<*)oops(*>*)
wenzelm@58860
    56
lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"
nipkow@9645
    57
(*<*)
wenzelm@58860
    58
apply(induct_tac xs)
nipkow@9645
    59
(*>*)
nipkow@9645
    60
nipkow@10420
    61
txt{*\noindent
paulson@10885
    62
This time, induction leaves us with a trivial base case:
nipkow@10420
    63
@{subgoals[display,indent=0,goals_limit=1]}
paulson@10885
    64
And @{text"auto"} completes the proof.
nipkow@9645
    65
paulson@10885
    66
If there are multiple premises $A@1$, \dots, $A@n$ containing the
nipkow@9645
    67
induction variable, you should turn the conclusion $C$ into
paulson@11494
    68
\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
nipkow@9645
    69
Additionally, you may also have to universally quantify some other variables,
nipkow@11196
    70
which can yield a fairly complex conclusion.  However, @{text rule_format} 
paulson@10885
    71
can remove any number of occurrences of @{text"\<forall>"} and
paulson@10885
    72
@{text"\<longrightarrow>"}.
nipkow@9645
    73
paulson@11494
    74
\index{induction!on a term}%
nipkow@9645
    75
A second reason why your proposition may not be amenable to induction is that
paulson@11494
    76
you want to induct on a complex term, rather than a variable. In
paulson@11494
    77
general, induction on a term~$t$ requires rephrasing the conclusion~$C$
nipkow@10217
    78
as
nipkow@11277
    79
\begin{equation}\label{eqn:ind-over-term}
paulson@11494
    80
\forall y@1 \dots y@n.~ x = t \longrightarrow C.
nipkow@11277
    81
\end{equation}
paulson@11494
    82
where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
wenzelm@12815
    83
Now you can perform induction on~$x$. An example appears in
nipkow@10217
    84
\S\ref{sec:complete-ind} below.
nipkow@10217
    85
nipkow@10217
    86
The very same problem may occur in connection with rule induction. Remember
nipkow@10217
    87
that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
nipkow@10217
    88
some inductively defined set and the $x@i$ are variables.  If instead we have
nipkow@10217
    89
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
nipkow@10217
    90
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
paulson@11494
    91
\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
nipkow@10217
    92
For an example see \S\ref{sec:CTL-revisited} below.
nipkow@10281
    93
nipkow@10281
    94
Of course, all premises that share free variables with $t$ need to be pulled into
nipkow@10281
    95
the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
nipkow@11277
    96
nipkow@11277
    97
Readers who are puzzled by the form of statement
nipkow@11277
    98
(\ref{eqn:ind-over-term}) above should remember that the
nipkow@11277
    99
transformation is only performed to permit induction. Once induction
nipkow@11277
   100
has been applied, the statement can be transformed back into something quite
nipkow@11277
   101
intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
nipkow@11277
   102
$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
nipkow@11277
   103
little leads to the goal
nipkow@11278
   104
\[ \bigwedge\overline{y}.\ 
nipkow@11278
   105
   \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
nipkow@11278
   106
    \ \Longrightarrow\ C\,\overline{y} \]
nipkow@11278
   107
where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
nipkow@11278
   108
$C$ on the free variables of $t$ has been made explicit.
nipkow@11278
   109
Unfortunately, this induction schema cannot be expressed as a
nipkow@11278
   110
single theorem because it depends on the number of free variables in $t$ ---
nipkow@11278
   111
the notation $\overline{y}$ is merely an informal device.
nipkow@11277
   112
*}
nipkow@12492
   113
(*<*)by auto(*>*)
nipkow@9645
   114
wenzelm@58860
   115
subsection{*Beyond Structural and Recursion Induction*}
nipkow@9645
   116
nipkow@10217
   117
text{*\label{sec:complete-ind}
paulson@10885
   118
So far, inductive proofs were by structural induction for
nipkow@9645
   119
primitive recursive functions and recursion induction for total recursive
nipkow@9645
   120
functions. But sometimes structural induction is awkward and there is no
paulson@10885
   121
recursive function that could furnish a more appropriate
paulson@10885
   122
induction schema. In such cases a general-purpose induction schema can
nipkow@9645
   123
be helpful. We show how to apply such induction schemas by an example.
nipkow@9645
   124
nipkow@9792
   125
Structural induction on @{typ"nat"} is
paulson@11494
   126
usually known as mathematical induction. There is also \textbf{complete}
paulson@11494
   127
\index{induction!complete}%
paulson@11494
   128
induction, where you prove $P(n)$ under the assumption that $P(m)$
paulson@11494
   129
holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
nipkow@9933
   130
@{thm[display]"nat_less_induct"[no_vars]}
paulson@11494
   131
As an application, we prove a property of the following
nipkow@11278
   132
function:
wenzelm@58860
   133
*}
nipkow@9645
   134
wenzelm@48994
   135
axiomatization f :: "nat \<Rightarrow> nat"
wenzelm@48994
   136
  where f_ax: "f(f(n)) < f(Suc(n))"
nipkow@9645
   137
nipkow@11256
   138
text{*
nipkow@11256
   139
\begin{warn}
nipkow@11256
   140
We discourage the use of axioms because of the danger of
nipkow@11256
   141
inconsistencies.  Axiom @{text f_ax} does
nipkow@11256
   142
not introduce an inconsistency because, for example, the identity function
nipkow@11256
   143
satisfies it.  Axioms can be useful in exploratory developments, say when 
nipkow@11256
   144
you assume some well-known theorems so that you can quickly demonstrate some
nipkow@11256
   145
point about methodology.  If your example turns into a substantial proof
nipkow@11256
   146
development, you should replace axioms by theorems.
nipkow@11256
   147
\end{warn}\noindent
paulson@10885
   148
The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
nipkow@11196
   149
be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
nipkow@9645
   150
above, we have to phrase the proposition as follows to allow induction:
wenzelm@58860
   151
*}
nipkow@9645
   152
wenzelm@58860
   153
lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
nipkow@9645
   154
nipkow@9645
   155
txt{*\noindent
nipkow@10363
   156
To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
nipkow@10363
   157
the same general induction method as for recursion induction (see
nipkow@25258
   158
\S\ref{sec:fun-induction}):
wenzelm@58860
   159
*}
nipkow@9645
   160
wenzelm@58860
   161
apply(induct_tac k rule: nat_less_induct)
nipkow@10363
   162
nipkow@10363
   163
txt{*\noindent
paulson@11494
   164
We get the following proof state:
nipkow@10363
   165
@{subgoals[display,indent=0,margin=65]}
nipkow@10363
   166
After stripping the @{text"\<forall>i"}, the proof continues with a case
nipkow@12699
   167
distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on
nipkow@10363
   168
the other case:
nipkow@10363
   169
*}
nipkow@10363
   170
nipkow@11196
   171
apply(rule allI)
nipkow@11196
   172
apply(case_tac i)
nipkow@11196
   173
 apply(simp)
nipkow@10363
   174
txt{*
nipkow@10363
   175
@{subgoals[display,indent=0]}
nipkow@11196
   176
*}
nipkow@11196
   177
by(blast intro!: f_ax Suc_leI intro: le_less_trans)
nipkow@9645
   178
nipkow@9645
   179
text{*\noindent
nipkow@11196
   180
If you find the last step puzzling, here are the two lemmas it employs:
paulson@10885
   181
\begin{isabelle}
paulson@10885
   182
@{thm Suc_leI[no_vars]}
paulson@10885
   183
\rulename{Suc_leI}\isanewline
paulson@10885
   184
@{thm le_less_trans[no_vars]}
paulson@10885
   185
\rulename{le_less_trans}
paulson@10885
   186
\end{isabelle}
paulson@10885
   187
%
nipkow@9792
   188
The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
nipkow@9792
   189
Since @{prop"i = Suc j"} it suffices to show
paulson@10885
   190
\hbox{@{prop"j < f(Suc j)"}},
paulson@10885
   191
by @{thm[source]Suc_leI}\@.  This is
nipkow@9792
   192
proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
paulson@10885
   193
(1) which implies @{prop"f j <= f (f j)"} by the induction hypothesis.
paulson@10885
   194
Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by the transitivity
paulson@10885
   195
rule @{thm[source]le_less_trans}.
nipkow@9792
   196
Using the induction hypothesis once more we obtain @{prop"j <= f j"}
nipkow@9792
   197
which, together with (2) yields @{prop"j < f (Suc j)"} (again by
nipkow@9792
   198
@{thm[source]le_less_trans}).
nipkow@9645
   199
paulson@11494
   200
This last step shows both the power and the danger of automatic proofs.  They
paulson@11494
   201
will usually not tell you how the proof goes, because it can be hard to
paulson@11494
   202
translate the internal proof into a human-readable format.  Automatic
paulson@11494
   203
proofs are easy to write but hard to read and understand.
nipkow@9645
   204
paulson@11494
   205
The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
wenzelm@58860
   206
*}
nipkow@9645
   207
wenzelm@58860
   208
lemmas f_incr = f_incr_lem[rule_format, OF refl]
nipkow@9645
   209
nipkow@9689
   210
text{*\noindent
paulson@10885
   211
The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. 
paulson@10885
   212
We could have included this derivation in the original statement of the lemma:
wenzelm@58860
   213
*}
nipkow@9645
   214
wenzelm@58860
   215
lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
wenzelm@58860
   216
(*<*)oops(*>*)
nipkow@9645
   217
nipkow@9645
   218
text{*
nipkow@11256
   219
\begin{exercise}
nipkow@11256
   220
From the axiom and lemma for @{term"f"}, show that @{term"f"} is the
nipkow@11256
   221
identity function.
nipkow@11256
   222
\end{exercise}
nipkow@9645
   223
paulson@11428
   224
Method \methdx{induct_tac} can be applied with any rule $r$
nipkow@9792
   225
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
nipkow@9645
   226
format is
nipkow@9792
   227
\begin{quote}
nipkow@9792
   228
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
paulson@11428
   229
\end{quote}
wenzelm@27320
   230
where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
paulson@10885
   231
nipkow@11256
   232
A further useful induction rule is @{thm[source]length_induct},
nipkow@11256
   233
induction on the length of a list\indexbold{*length_induct}
nipkow@11256
   234
@{thm[display]length_induct[no_vars]}
nipkow@11256
   235
which is a special case of @{thm[source]measure_induct}
nipkow@11256
   236
@{thm[display]measure_induct[no_vars]}
nipkow@11256
   237
where @{term f} may be any function into type @{typ nat}.
nipkow@11256
   238
*}
nipkow@9645
   239
wenzelm@58860
   240
subsection{*Derivation of New Induction Schemas*}
nipkow@9689
   241
nipkow@9689
   242
text{*\label{sec:derive-ind}
paulson@11494
   243
\index{induction!deriving new schemas}%
nipkow@9689
   244
Induction schemas are ordinary theorems and you can derive new ones
paulson@11494
   245
whenever you wish.  This section shows you how, using the example
nipkow@9933
   246
of @{thm[source]nat_less_induct}. Assume we only have structural induction
paulson@11494
   247
available for @{typ"nat"} and want to derive complete induction.  We
paulson@11494
   248
must generalize the statement as shown:
wenzelm@58860
   249
*}
nipkow@9689
   250
wenzelm@58860
   251
lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m"
wenzelm@58860
   252
apply(induct_tac n)
nipkow@9689
   253
nipkow@9689
   254
txt{*\noindent
nipkow@11196
   255
The base case is vacuously true. For the induction step (@{prop"m <
nipkow@9933
   256
Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
nipkow@9933
   257
hypothesis and case @{prop"m = n"} follows from the assumption, again using
nipkow@9689
   258
the induction hypothesis:
wenzelm@58860
   259
*}
wenzelm@58860
   260
 apply(blast)
wenzelm@12815
   261
by(blast elim: less_SucE)
nipkow@9689
   262
nipkow@9689
   263
text{*\noindent
nipkow@11196
   264
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
nipkow@9689
   265
@{thm[display]"less_SucE"[no_vars]}
nipkow@9689
   266
nipkow@9689
   267
Now it is straightforward to derive the original version of
nipkow@11256
   268
@{thm[source]nat_less_induct} by manipulating the conclusion of the above
nipkow@11256
   269
lemma: instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"}
nipkow@11256
   270
and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
nipkow@9689
   271
happens automatically when we add the lemma as a new premise to the
nipkow@9689
   272
desired goal:
wenzelm@58860
   273
*}
nipkow@9689
   274
wenzelm@58860
   275
theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"
wenzelm@58860
   276
by(insert induct_lem, blast)
nipkow@9689
   277
nipkow@9933
   278
text{*
paulson@11494
   279
HOL already provides the mother of
nipkow@10396
   280
all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
paulson@10885
   281
example theorem @{thm[source]nat_less_induct} is
nipkow@10396
   282
a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
paulson@10885
   283
@{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}.
nipkow@10654
   284
*}
nipkow@10654
   285
(*<*)end(*>*)