doc-src/TutorialI/Misc/AdvancedInd.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9933 9feb1e0c4cb3
child 10186 499637e8f2c6
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     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 @{term"hd"} and @{term"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 @{term"hd"} and
    39 @{term"last"} return when applied to @{term"[]"}.
    40 
    41 The point is that we have violated the above warning. Because the induction
    42 formula is only the conclusion, the occurrence of @{term"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 @{text"\<longrightarrow>"}.}
    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 @{text"auto"} finishes the whole proof.
    63 
    64 If @{thm[source]hd_rev} is meant to be a simplification rule, you are
    65 done. But if you really need the @{text"\<Longrightarrow>"}-version of
    66 @{thm[source]hd_rev}, for example because you want to apply it as an
    67 introduction rule, you need to derive it separately, by combining it with
    68 modus ponens:
    69 *};
    70 
    71 lemmas hd_revI = hd_rev[THEN mp];
    72  
    73 text{*\noindent
    74 which yields the lemma we originally set out to prove.
    75 
    76 In case there are multiple premises $A@1$, \dots, $A@n$ containing the
    77 induction variable, you should turn the conclusion $C$ into
    78 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
    79 (see the remark?? in \S\ref{??}).
    80 Additionally, you may also have to universally quantify some other variables,
    81 which can yield a fairly complex conclusion.
    82 Here is a simple example (which is proved by @{text"blast"}):
    83 *};
    84 
    85 lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
    86 (*<*)by blast;(*>*)
    87 
    88 text{*\noindent
    89 You can get the desired lemma by explicit
    90 application of modus ponens and @{thm[source]spec}:
    91 *};
    92 
    93 lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
    94 
    95 text{*\noindent
    96 or the wholesale stripping of @{text"\<forall>"} and
    97 @{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"} 
    98 *};
    99 
   100 lemmas myrule = simple[rule_format];
   101 
   102 text{*\noindent
   103 yielding @{thm"myrule"[no_vars]}.
   104 You can go one step further and include these derivations already in the
   105 statement of your original lemma, thus avoiding the intermediate step:
   106 *};
   107 
   108 lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
   109 (*<*)
   110 by blast;
   111 (*>*)
   112 
   113 text{*
   114 \bigskip
   115 
   116 A second reason why your proposition may not be amenable to induction is that
   117 you want to induct on a whole term, rather than an individual variable. In
   118 general, when inducting on some term $t$ you must rephrase the conclusion as
   119 \[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$
   120 are the free variables in $t$ and $x$ is new, and perform induction on $x$
   121 afterwards. An example appears below.
   122 *};
   123 
   124 subsection{*Beyond structural and recursion induction*};
   125 
   126 text{*
   127 So far, inductive proofs where by structural induction for
   128 primitive recursive functions and recursion induction for total recursive
   129 functions. But sometimes structural induction is awkward and there is no
   130 recursive function in sight either that could furnish a more appropriate
   131 induction schema. In such cases some existing standard induction schema can
   132 be helpful. We show how to apply such induction schemas by an example.
   133 
   134 Structural induction on @{typ"nat"} is
   135 usually known as ``mathematical induction''. There is also ``complete
   136 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
   137 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
   138 @{thm[display]"nat_less_induct"[no_vars]}
   139 Here is an example of its application.
   140 *};
   141 
   142 consts f :: "nat => nat";
   143 axioms f_ax: "f(f(n)) < f(Suc(n))";
   144 
   145 text{*\noindent
   146 From the above axiom\footnote{In general, the use of axioms is strongly
   147 discouraged, because of the danger of inconsistencies. The above axiom does
   148 not introduce an inconsistency because, for example, the identity function
   149 satisfies it.}
   150 for @{term"f"} it follows that @{prop"n <= f n"}, which can
   151 be proved by induction on @{term"f n"}. Following the recipy outlined
   152 above, we have to phrase the proposition as follows to allow induction:
   153 *};
   154 
   155 lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
   156 
   157 txt{*\noindent
   158 To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same
   159 general induction method as for recursion induction (see
   160 \S\ref{sec:recdef-induction}):
   161 *};
   162 
   163 apply(induct_tac k rule: nat_less_induct);
   164 (*<*)
   165 apply(rule allI);
   166 apply(case_tac i);
   167  apply(simp);
   168 (*>*)
   169 txt{*\noindent
   170 which leaves us with the following proof state:
   171 \begin{isabelle}
   172 \ 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
   173 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
   174 \end{isabelle}
   175 After stripping the @{text"\<forall>i"}, the proof continues with a case
   176 distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on
   177 the other case:
   178 \begin{isabelle}
   179 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
   180 \ \ \ \ \ \ \ {\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
   181 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
   182 \end{isabelle}
   183 *};
   184 
   185 by(blast intro!: f_ax Suc_leI intro: le_less_trans);
   186 
   187 text{*\noindent
   188 It is not surprising if you find the last step puzzling.
   189 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
   190 Since @{prop"i = Suc j"} it suffices to show
   191 @{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is
   192 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
   193 (1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).
   194 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity
   195 (@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).
   196 Using the induction hypothesis once more we obtain @{prop"j <= f j"}
   197 which, together with (2) yields @{prop"j < f (Suc j)"} (again by
   198 @{thm[source]le_less_trans}).
   199 
   200 This last step shows both the power and the danger of automatic proofs: they
   201 will usually not tell you how the proof goes, because it can be very hard to
   202 translate the internal proof into a human-readable format. Therefore
   203 \S\ref{sec:part2?} introduces a language for writing readable yet concise
   204 proofs.
   205 
   206 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
   207 *};
   208 
   209 lemmas f_incr = f_incr_lem[rule_format, OF refl];
   210 
   211 text{*\noindent
   212 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
   213 we could have included this derivation in the original statement of the lemma:
   214 *};
   215 
   216 lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
   217 (*<*)oops;(*>*)
   218 
   219 text{*
   220 \begin{exercise}
   221 From the above axiom and lemma for @{term"f"} show that @{term"f"} is the
   222 identity.
   223 \end{exercise}
   224 
   225 In general, @{text"induct_tac"} can be applied with any rule $r$
   226 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
   227 format is
   228 \begin{quote}
   229 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
   230 \end{quote}\index{*induct_tac}%
   231 where $y@1, \dots, y@n$ are variables in the first subgoal.
   232 In fact, @{text"induct_tac"} even allows the conclusion of
   233 $r$ to be an (iterated) conjunction of formulae of the above form, in
   234 which case the application is
   235 \begin{quote}
   236 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}
   237 \end{quote}
   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 @{thm[source]nat_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) \<Longrightarrow> \<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 (@{prop"m <
   255 Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
   256 hypothesis and case @{prop"m = n"} follows from the assumption, again using
   257 the induction hypothesis:
   258 *};
   259 apply(blast);
   260 by(blast elim:less_SucE)
   261 
   262 text{*\noindent
   263 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
   264 @{thm[display]"less_SucE"[no_vars]}
   265 
   266 Now it is straightforward to derive the original version of
   267 @{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
   268 instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
   269 remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
   270 happens automatically when we add the lemma as a new premise to the
   271 desired goal:
   272 *};
   273 
   274 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
   275 by(insert induct_lem, blast);
   276 
   277 text{*
   278 Finally we should mention that HOL already provides the mother of all
   279 inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
   280 @{thm[display]"wf_induct"[no_vars]}
   281 where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
   282 For example, theorem @{thm[source]nat_less_induct} can be viewed (and
   283 derived) as a special case of @{thm[source]wf_induct} where 
   284 @{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.
   285 *};
   286 
   287 (*<*)
   288 end
   289 (*>*)