doc-src/TutorialI/Inductive/Even.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10341 6eb91805a012 child 10883 2b9f87bf9113 permissions -rw-r--r--
*** empty log message ***
 paulson@10341 1 (* ID: $Id$ *) paulson@10314 2 theory Even = Main: paulson@10314 3 paulson@10314 4 text{*We begin with a simple example: the set of even numbers. Obviously this paulson@10314 5 concept can be expressed already using the divides relation (dvd). We shall paulson@10314 6 prove below that the two formulations coincide. paulson@10314 7 paulson@10314 8 First, we declare the constant \isa{even} to be a set of natural numbers. paulson@10314 9 Then, an inductive declaration gives it the desired properties. paulson@10314 10 *} paulson@10314 11 paulson@10314 12 paulson@10314 13 consts even :: "nat set" paulson@10314 14 inductive even paulson@10314 15 intros paulson@10314 16 zero[intro!]: "0 \ even" paulson@10314 17 step[intro!]: "n \ even \ (Suc (Suc n)) \ even" paulson@10314 18 paulson@10314 19 text{*An inductive definition consists of introduction rules. The first one paulson@10314 20 above states that 0 is even; the second states that if $n$ is even, so is paulson@10314 21 $n+2$. Given this declaration, Isabelle generates a fixed point definition paulson@10314 22 for \isa{even} and proves many theorems about it. These theorems include the paulson@10314 23 introduction rules specified in the declaration, an elimination rule for case paulson@10314 24 analysis and an induction rule. We can refer to these theorems by paulson@10314 25 automatically-generated names: paulson@10314 26 paulson@10326 27 @{thm[display] even.step[no_vars]} paulson@10314 28 \rulename{even.step} paulson@10314 29 paulson@10326 30 @{thm[display] even.induct[no_vars]} paulson@10314 31 \rulename{even.induct} paulson@10314 32 paulson@10314 33 Attributes can be given to the introduction rules. Here both rules are paulson@10314 34 specified as \isa{intro!}, which will cause them to be applied aggressively. paulson@10314 35 Obviously, regarding 0 as even is always safe. The second rule is also safe paulson@10314 36 because $n+2$ is even if and only if $n$ is even. We prove this equivalence paulson@10314 37 later.*} paulson@10314 38 paulson@10314 39 text{*Our first lemma states that numbers of the form $2\times k$ are even. paulson@10314 40 Introduction rules are used to show that given values belong to the inductive paulson@10314 41 set. Often, as here, the proof involves some other sort of induction.*} paulson@10314 42 lemma two_times_even[intro!]: "#2*k \ even" paulson@10314 43 apply (induct "k") paulson@10314 44 apply auto paulson@10314 45 done paulson@10314 46 paulson@10314 47 text{* The first step is induction on the natural number \isa{k}, which leaves paulson@10314 48 two subgoals: paulson@10314 49 paulson@10314 50 pr(latex xsymbols symbols); paulson@10314 51 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline paulson@10314 52 \isanewline paulson@10314 53 goal\ {\isacharparenleft}lemma\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline paulson@10314 54 {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\isanewline paulson@10314 55 \ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline paulson@10314 56 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even paulson@10314 57 paulson@10314 58 Here \isa{auto} simplifies both subgoals so that they match the introduction paulson@10314 59 rules, which then are applied automatically. *} paulson@10314 60 paulson@10314 61 text{*Our goal is to prove the equivalence between the traditional definition paulson@10314 62 of even (using the divides relation) and our inductive definition. Half of paulson@10314 63 this equivalence is trivial using the lemma just proved, whose \isa{intro!} paulson@10314 64 attribute ensures it will be applied automatically. *} paulson@10314 65 paulson@10314 66 lemma dvd_imp_even: "#2 dvd n \ n \ even" paulson@10314 67 apply (auto simp add: dvd_def) paulson@10314 68 done paulson@10314 69 paulson@10314 70 text{*our first rule induction!*} paulson@10314 71 lemma even_imp_dvd: "n \ even \ #2 dvd n" paulson@10314 72 apply (erule even.induct) paulson@10314 73 apply simp paulson@10314 74 apply (simp add: dvd_def) paulson@10314 75 apply clarify paulson@10314 76 apply (rule_tac x = "Suc k" in exI) paulson@10314 77 apply simp paulson@10314 78 done paulson@10314 79 text{* paulson@10314 80 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline paulson@10314 81 \isanewline paulson@10314 82 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline paulson@10314 83 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline paulson@10314 84 \ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline paulson@10314 85 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright} paulson@10314 86 paulson@10326 87 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline paulson@10326 88 \isanewline paulson@10326 89 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline paulson@10326 90 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline paulson@10326 91 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k paulson@10326 92 paulson@10314 93 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline paulson@10314 94 \isanewline paulson@10314 95 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline paulson@10314 96 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline paulson@10314 97 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ ka paulson@10314 98 *} paulson@10314 99 paulson@10314 100 paulson@10314 101 text{*no iff-attribute because we don't always want to use it*} paulson@10314 102 theorem even_iff_dvd: "(n \ even) = (#2 dvd n)" paulson@10314 103 apply (blast intro: dvd_imp_even even_imp_dvd) paulson@10314 104 done paulson@10314 105 paulson@10314 106 text{*this result ISN'T inductive...*} paulson@10314 107 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \ even \ n \ even" paulson@10314 108 apply (erule even.induct) paulson@10314 109 oops paulson@10314 110 text{* paulson@10314 111 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline paulson@10314 112 \isanewline paulson@10314 113 goal\ {\isacharparenleft}lemma\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline paulson@10314 114 Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\isanewline paulson@10314 115 \ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline paulson@10314 116 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even paulson@10314 117 *} paulson@10314 118 paulson@10314 119 paulson@10314 120 text{*...so we need an inductive lemma...*} paulson@10314 121 lemma even_imp_even_minus_2: "n \ even \ n-#2 \ even" paulson@10314 122 apply (erule even.induct) paulson@10314 123 apply auto paulson@10314 124 done paulson@10314 125 paulson@10326 126 text{* paulson@10326 127 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline paulson@10326 128 \isanewline paulson@10326 129 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharparenright}{\isacharcolon}\isanewline paulson@10326 130 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline paulson@10326 131 \ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline paulson@10326 132 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even paulson@10326 133 *} paulson@10326 134 paulson@10326 135 paulson@10314 136 text{*...and prove it in a separate step*} paulson@10314 137 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \ even \ n \ even" paulson@10314 138 apply (drule even_imp_even_minus_2) paulson@10314 139 apply simp paulson@10314 140 done paulson@10314 141 paulson@10326 142 lemma [iff]: "((Suc (Suc n)) \ even) = (n \ even)" paulson@10314 143 apply (blast dest: Suc_Suc_even_imp_even) paulson@10314 144 done paulson@10314 145 paulson@10314 146 end paulson@10314 147