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 \<in> even"
paulson@10314
    17
step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> 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 \<in> 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 \<Longrightarrow> n \<in> 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 \<in> even \<Longrightarrow> #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 \<in> 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) \<in> even \<Longrightarrow> n \<in> 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 \<in> even \<Longrightarrow> n-#2 \<in> 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) \<in> even \<Longrightarrow> n \<in> 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)) \<in> even) = (n \<in> 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