10341
|
1 |
(* ID: $Id$ *)
|
10314
|
2 |
theory Even = Main:
|
|
3 |
|
|
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.
|
|
7 |
|
|
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.
|
|
10 |
*}
|
|
11 |
|
|
12 |
|
|
13 |
consts even :: "nat set"
|
|
14 |
inductive even
|
|
15 |
intros
|
|
16 |
zero[intro!]: "0 \<in> even"
|
|
17 |
step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
|
|
18 |
|
|
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:
|
|
26 |
|
10326
|
27 |
@{thm[display] even.step[no_vars]}
|
10314
|
28 |
\rulename{even.step}
|
|
29 |
|
10326
|
30 |
@{thm[display] even.induct[no_vars]}
|
10314
|
31 |
\rulename{even.induct}
|
|
32 |
|
|
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
|
|
37 |
later.*}
|
|
38 |
|
|
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"
|
|
43 |
apply (induct "k")
|
|
44 |
apply auto
|
|
45 |
done
|
|
46 |
|
|
47 |
text{* The first step is induction on the natural number \isa{k}, which leaves
|
|
48 |
two subgoals:
|
|
49 |
|
|
50 |
pr(latex xsymbols symbols);
|
|
51 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
|
|
52 |
\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
|
|
57 |
|
|
58 |
Here \isa{auto} simplifies both subgoals so that they match the introduction
|
|
59 |
rules, which then are applied automatically. *}
|
|
60 |
|
|
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. *}
|
|
65 |
|
|
66 |
lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
|
|
67 |
apply (auto simp add: dvd_def)
|
|
68 |
done
|
|
69 |
|
|
70 |
text{*our first rule induction!*}
|
|
71 |
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
|
|
72 |
apply (erule even.induct)
|
|
73 |
apply simp
|
|
74 |
apply (simp add: dvd_def)
|
|
75 |
apply clarify
|
|
76 |
apply (rule_tac x = "Suc k" in exI)
|
|
77 |
apply simp
|
|
78 |
done
|
|
79 |
text{*
|
|
80 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
|
|
81 |
\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}
|
|
86 |
|
10326
|
87 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline
|
|
88 |
\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
|
|
92 |
|
10314
|
93 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline
|
|
94 |
\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
|
|
98 |
*}
|
|
99 |
|
|
100 |
|
|
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)
|
|
104 |
done
|
|
105 |
|
|
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)
|
|
109 |
oops
|
|
110 |
text{*
|
|
111 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
|
|
112 |
\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
|
|
117 |
*}
|
|
118 |
|
|
119 |
|
|
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)
|
|
123 |
apply auto
|
|
124 |
done
|
|
125 |
|
10326
|
126 |
text{*
|
|
127 |
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
|
|
128 |
\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
|
|
133 |
*}
|
|
134 |
|
|
135 |
|
10314
|
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)
|
|
139 |
apply simp
|
|
140 |
done
|
|
141 |
|
10326
|
142 |
lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
|
10314
|
143 |
apply (blast dest: Suc_Suc_even_imp_even)
|
|
144 |
done
|
|
145 |
|
|
146 |
end
|
|
147 |
|