--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/Even.thy Tue Oct 24 10:46:04 2000 +0200
@@ -0,0 +1,130 @@
+theory Even = Main:
+
+text{*We begin with a simple example: the set of even numbers. Obviously this
+concept can be expressed already using the divides relation (dvd). We shall
+prove below that the two formulations coincide.
+
+First, we declare the constant \isa{even} to be a set of natural numbers.
+Then, an inductive declaration gives it the desired properties.
+*}
+
+
+consts even :: "nat set"
+inductive even
+intros
+zero[intro!]: "0 \<in> even"
+step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
+
+text{*An inductive definition consists of introduction rules. The first one
+above states that 0 is even; the second states that if $n$ is even, so is
+$n+2$. Given this declaration, Isabelle generates a fixed point definition
+for \isa{even} and proves many theorems about it. These theorems include the
+introduction rules specified in the declaration, an elimination rule for case
+analysis and an induction rule. We can refer to these theorems by
+automatically-generated names:
+
+@{thm[display] even.step}
+\rulename{even.step}
+
+@{thm[display] even.induct}
+\rulename{even.induct}
+
+Attributes can be given to the introduction rules. Here both rules are
+specified as \isa{intro!}, which will cause them to be applied aggressively.
+Obviously, regarding 0 as even is always safe. The second rule is also safe
+because $n+2$ is even if and only if $n$ is even. We prove this equivalence
+later.*}
+
+text{*Our first lemma states that numbers of the form $2\times k$ are even.
+Introduction rules are used to show that given values belong to the inductive
+set. Often, as here, the proof involves some other sort of induction.*}
+lemma two_times_even[intro!]: "#2*k \<in> even"
+apply (induct "k")
+ apply auto
+done
+
+text{* The first step is induction on the natural number \isa{k}, which leaves
+two subgoals:
+
+pr(latex xsymbols symbols);
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline
+{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even
+
+Here \isa{auto} simplifies both subgoals so that they match the introduction
+rules, which then are applied automatically. *}
+
+text{*Our goal is to prove the equivalence between the traditional definition
+of even (using the divides relation) and our inductive definition. Half of
+this equivalence is trivial using the lemma just proved, whose \isa{intro!}
+attribute ensures it will be applied automatically. *}
+
+lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
+apply (auto simp add: dvd_def)
+done
+
+text{*our first rule induction!*}
+lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
+apply (erule even.induct)
+ apply simp
+apply (simp add: dvd_def)
+apply clarify
+apply (rule_tac x = "Suc k" in exI)
+apply simp
+done
+text{*
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
+n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
+\ {\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}
+
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
+n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
+\ {\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
+*}
+
+
+text{*no iff-attribute because we don't always want to use it*}
+theorem even_iff_dvd: "(n \<in> even) = (#2 dvd n)"
+apply (blast intro: dvd_imp_even even_imp_dvd)
+done
+
+text{*this result ISN'T inductive...*}
+lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
+apply (erule even.induct)
+oops
+text{*
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline
+Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\isanewline
+\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even
+*}
+
+
+text{*...so we need an inductive lemma...*}
+lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n-#2 \<in> even"
+apply (erule even.induct)
+apply auto
+done
+
+text{*...and prove it in a separate step*}
+lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
+apply (drule even_imp_even_minus_2)
+apply simp
+done
+
+lemma Suc_Suc_even_iff [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
+apply (blast dest: Suc_Suc_even_imp_even)
+done
+
+end
+