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 (*>*)