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 ***
     1 (* ID:         $Id$ *)
     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 
    27 @{thm[display] even.step[no_vars]}
    28 \rulename{even.step}
    29 
    30 @{thm[display] even.induct[no_vars]}
    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 
    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 
    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 
   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 
   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 
   142 lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
   143 apply (blast dest: Suc_Suc_even_imp_even)
   144 done
   145 
   146 end
   147