4 text{*We begin with a simple example: the set of even numbers. Obviously this
5 concept can be expressed already using the divides relation (dvd). We shall
6 prove below that the two formulations coincide.
8 First, we declare the constant \isa{even} to be a set of natural numbers.
9 Then, an inductive declaration gives it the desired properties.
13 consts even :: "nat set"
16 zero[intro!]: "0 \<in> even"
17 step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
19 text{*An inductive definition consists of introduction rules. The first one
20 above states that 0 is even; the second states that if $n$ is even, so is
21 $n+2$. Given this declaration, Isabelle generates a fixed point definition
22 for \isa{even} and proves many theorems about it. These theorems include the
23 introduction rules specified in the declaration, an elimination rule for case
24 analysis and an induction rule. We can refer to these theorems by
25 automatically-generated names:
27 @{thm[display] even.step[no_vars]}
30 @{thm[display] even.induct[no_vars]}
31 \rulename{even.induct}
33 Attributes can be given to the introduction rules. Here both rules are
34 specified as \isa{intro!}, which will cause them to be applied aggressively.
35 Obviously, regarding 0 as even is always safe. The second rule is also safe
36 because $n+2$ is even if and only if $n$ is even. We prove this equivalence
39 text{*Our first lemma states that numbers of the form $2\times k$ are even.
40 Introduction rules are used to show that given values belong to the inductive
41 set. Often, as here, the proof involves some other sort of induction.*}
42 lemma two_times_even[intro!]: "#2*k \<in> even"
47 text{* The first step is induction on the natural number \isa{k}, which leaves
50 pr(latex xsymbols symbols);
51 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
53 goal\ {\isacharparenleft}lemma\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline
54 {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\isanewline
55 \ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline
56 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even
58 Here \isa{auto} simplifies both subgoals so that they match the introduction
59 rules, which then are applied automatically. *}
61 text{*Our goal is to prove the equivalence between the traditional definition
62 of even (using the divides relation) and our inductive definition. Half of
63 this equivalence is trivial using the lemma just proved, whose \isa{intro!}
64 attribute ensures it will be applied automatically. *}
66 lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
67 apply (auto simp add: dvd_def)
70 text{*our first rule induction!*}
71 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
72 apply (erule even.induct)
74 apply (simp add: dvd_def)
76 apply (rule_tac x = "Suc k" in exI)
80 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
82 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
83 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
84 \ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
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}
87 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline
89 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
90 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
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
93 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline
95 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
96 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
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
101 text{*no iff-attribute because we don't always want to use it*}
102 theorem even_iff_dvd: "(n \<in> even) = (#2 dvd n)"
103 apply (blast intro: dvd_imp_even even_imp_dvd)
106 text{*this result ISN'T inductive...*}
107 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
108 apply (erule even.induct)
111 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
113 goal\ {\isacharparenleft}lemma\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline
114 Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\isanewline
115 \ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline
116 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even
120 text{*...so we need an inductive lemma...*}
121 lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n-#2 \<in> even"
122 apply (erule even.induct)
127 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
129 goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharparenright}{\isacharcolon}\isanewline
130 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline
131 \ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline
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
136 text{*...and prove it in a separate step*}
137 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
138 apply (drule even_imp_even_minus_2)
142 lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
143 apply (blast dest: Suc_Suc_even_imp_even)