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