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