535 |
535 |
536 Showing that all even numbers have some property is more complicated. For |
536 Showing that all even numbers have some property is more complicated. For |
537 example, let us prove that the inductive definition of even numbers agrees |
537 example, let us prove that the inductive definition of even numbers agrees |
538 with the following recursive one:*} |
538 with the following recursive one:*} |
539 |
539 |
540 fun even :: "nat \<Rightarrow> bool" where |
540 fun evn :: "nat \<Rightarrow> bool" where |
541 "even 0 = True" | |
541 "evn 0 = True" | |
542 "even (Suc 0) = False" | |
542 "evn (Suc 0) = False" | |
543 "even (Suc(Suc n)) = even n" |
543 "evn (Suc(Suc n)) = evn n" |
544 |
544 |
545 text{* We prove @{prop"ev m \<Longrightarrow> even m"}. That is, we |
545 text{* We prove @{prop"ev m \<Longrightarrow> evn m"}. That is, we |
546 assume @{prop"ev m"} and by induction on the form of its derivation |
546 assume @{prop"ev m"} and by induction on the form of its derivation |
547 prove @{prop"even m"}. There are two cases corresponding to the two rules |
547 prove @{prop"evn m"}. There are two cases corresponding to the two rules |
548 for @{const ev}: |
548 for @{const ev}: |
549 \begin{description} |
549 \begin{description} |
550 \item[Case @{thm[source]ev0}:] |
550 \item[Case @{thm[source]ev0}:] |
551 @{prop"ev m"} was derived by rule @{prop "ev 0"}: \\ |
551 @{prop"ev m"} was derived by rule @{prop "ev 0"}: \\ |
552 @{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "even m = even 0 = True"} |
552 @{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "evn m = evn 0 = True"} |
553 \item[Case @{thm[source]evSS}:] |
553 \item[Case @{thm[source]evSS}:] |
554 @{prop"ev m"} was derived by rule @{prop "ev n \<Longrightarrow> ev(n+2)"}: \\ |
554 @{prop"ev m"} was derived by rule @{prop "ev n \<Longrightarrow> ev(n+2)"}: \\ |
555 @{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"even n"}\\ |
555 @{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"evn n"}\\ |
556 @{text"\<Longrightarrow>"} @{text"even m = even(n + 2) = even n = True"} |
556 @{text"\<Longrightarrow>"} @{text"evn m = evn(n + 2) = evn n = True"} |
557 \end{description} |
557 \end{description} |
558 |
558 |
559 What we have just seen is a special case of \concept{rule induction}. |
559 What we have just seen is a special case of \concept{rule induction}. |
560 Rule induction applies to propositions of this form |
560 Rule induction applies to propositions of this form |
561 \begin{quote} |
561 \begin{quote} |
625 |
625 |
626 text{* \indent |
626 text{* \indent |
627 Rule induction is applied by giving the induction rule explicitly via the |
627 Rule induction is applied by giving the induction rule explicitly via the |
628 @{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}*} |
628 @{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}*} |
629 |
629 |
630 lemma "ev m \<Longrightarrow> even m" |
630 lemma "ev m \<Longrightarrow> evn m" |
631 apply(induction rule: ev.induct) |
631 apply(induction rule: ev.induct) |
632 by(simp_all) |
632 by(simp_all) |
633 |
633 |
634 text{* Both cases are automatic. Note that if there are multiple assumptions |
634 text{* Both cases are automatic. Note that if there are multiple assumptions |
635 of the form @{prop"ev t"}, method @{text induction} will induct on the leftmost |
635 of the form @{prop"ev t"}, method @{text induction} will induct on the leftmost |
636 one. |
636 one. |
637 |
637 |
638 As a bonus, we also prove the remaining direction of the equivalence of |
638 As a bonus, we also prove the remaining direction of the equivalence of |
639 @{const ev} and @{const even}: |
639 @{const ev} and @{const evn}: |
640 *} |
640 *} |
641 |
641 |
642 lemma "even n \<Longrightarrow> ev n" |
642 lemma "evn n \<Longrightarrow> ev n" |
643 apply(induction n rule: even.induct) |
643 apply(induction n rule: evn.induct) |
644 |
644 |
645 txt{* This is a proof by computation induction on @{text n} (see |
645 txt{* This is a proof by computation induction on @{text n} (see |
646 \autoref{sec:recursive-funs}) that sets up three subgoals corresponding to |
646 \autoref{sec:recursive-funs}) that sets up three subgoals corresponding to |
647 the three equations for @{const even}: |
647 the three equations for @{const evn}: |
648 @{subgoals[display,indent=0]} |
648 @{subgoals[display,indent=0]} |
649 The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because @{prop"even(Suc 0)"} is @{const False}: |
649 The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because @{prop"evn(Suc 0)"} is @{const False}: |
650 *} |
650 *} |
651 |
651 |
652 by (simp_all add: ev0 evSS) |
652 by (simp_all add: ev0 evSS) |
653 |
653 |
654 text{* The rules for @{const ev} make perfect simplification and introduction |
654 text{* The rules for @{const ev} make perfect simplification and introduction |
672 negative information (which numbers are not even) directly. An inductive |
672 negative information (which numbers are not even) directly. An inductive |
673 definition only expresses the positive information directly. The negative |
673 definition only expresses the positive information directly. The negative |
674 information, for example, that @{text 1} is not even, has to be proved from |
674 information, for example, that @{text 1} is not even, has to be proved from |
675 it (by induction or rule inversion). On the other hand, rule induction is |
675 it (by induction or rule inversion). On the other hand, rule induction is |
676 tailor-made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you |
676 tailor-made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you |
677 to prove the positive cases. In the proof of @{prop"even n \<Longrightarrow> P n"} by |
677 to prove the positive cases. In the proof of @{prop"evn n \<Longrightarrow> P n"} by |
678 computation induction via @{thm[source]even.induct}, we are also presented |
678 computation induction via @{thm[source]evn.induct}, we are also presented |
679 with the trivial negative cases. If you want the convenience of both |
679 with the trivial negative cases. If you want the convenience of both |
680 rewriting and rule induction, you can make two definitions and show their |
680 rewriting and rule induction, you can make two definitions and show their |
681 equivalence (as above) or make one definition and prove additional properties |
681 equivalence (as above) or make one definition and prove additional properties |
682 from it, for example rule induction from computation induction. |
682 from it, for example rule induction from computation induction. |
683 |
683 |