summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 10 Nov 2014 15:09:58 +0100 | |

changeset 58962 | e3491acee50f |

parent 58961 | 7c507e664047 |

child 58964 | a93d114eaa5d |

even -> evn because even is now in Main

--- a/src/Doc/Prog_Prove/Logic.thy Mon Nov 10 10:29:19 2014 +0100 +++ b/src/Doc/Prog_Prove/Logic.thy Mon Nov 10 15:09:58 2014 +0100 @@ -537,23 +537,23 @@ example, let us prove that the inductive definition of even numbers agrees with the following recursive one:*} -fun even :: "nat \<Rightarrow> bool" where -"even 0 = True" | -"even (Suc 0) = False" | -"even (Suc(Suc n)) = even n" +fun evn :: "nat \<Rightarrow> bool" where +"evn 0 = True" | +"evn (Suc 0) = False" | +"evn (Suc(Suc n)) = evn n" -text{* We prove @{prop"ev m \<Longrightarrow> even m"}. That is, we +text{* We prove @{prop"ev m \<Longrightarrow> evn m"}. That is, we assume @{prop"ev m"} and by induction on the form of its derivation -prove @{prop"even m"}. There are two cases corresponding to the two rules +prove @{prop"evn m"}. There are two cases corresponding to the two rules for @{const ev}: \begin{description} \item[Case @{thm[source]ev0}:] @{prop"ev m"} was derived by rule @{prop "ev 0"}: \\ - @{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "even m = even 0 = True"} + @{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "evn m = evn 0 = True"} \item[Case @{thm[source]evSS}:] @{prop"ev m"} was derived by rule @{prop "ev n \<Longrightarrow> ev(n+2)"}: \\ -@{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"even n"}\\ -@{text"\<Longrightarrow>"} @{text"even m = even(n + 2) = even n = True"} +@{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"evn n"}\\ +@{text"\<Longrightarrow>"} @{text"evn m = evn(n + 2) = evn n = True"} \end{description} What we have just seen is a special case of \concept{rule induction}. @@ -627,7 +627,7 @@ Rule induction is applied by giving the induction rule explicitly via the @{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}*} -lemma "ev m \<Longrightarrow> even m" +lemma "ev m \<Longrightarrow> evn m" apply(induction rule: ev.induct) by(simp_all) @@ -636,17 +636,17 @@ one. As a bonus, we also prove the remaining direction of the equivalence of -@{const ev} and @{const even}: +@{const ev} and @{const evn}: *} -lemma "even n \<Longrightarrow> ev n" -apply(induction n rule: even.induct) +lemma "evn n \<Longrightarrow> ev n" +apply(induction n rule: evn.induct) txt{* This is a proof by computation induction on @{text n} (see \autoref{sec:recursive-funs}) that sets up three subgoals corresponding to -the three equations for @{const even}: +the three equations for @{const evn}: @{subgoals[display,indent=0]} -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}: +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}: *} by (simp_all add: ev0 evSS) @@ -674,8 +674,8 @@ information, for example, that @{text 1} is not even, has to be proved from it (by induction or rule inversion). On the other hand, rule induction is tailor-made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you -to prove the positive cases. In the proof of @{prop"even n \<Longrightarrow> P n"} by -computation induction via @{thm[source]even.induct}, we are also presented +to prove the positive cases. In the proof of @{prop"evn n \<Longrightarrow> P n"} by +computation induction via @{thm[source]evn.induct}, we are also presented with the trivial negative cases. If you want the convenience of both rewriting and rule induction, you can make two definitions and show their equivalence (as above) or make one definition and prove additional properties