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