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