author paulson Fri, 12 Jan 2001 16:19:44 +0100 changeset 10883 2b9f87bf9113 parent 10882 ca41ba5fb8e2 child 10884 2995639c6a09
updated for new version of even-examples.tex
--- a/doc-src/TutorialI/Inductive/Even.thy	Fri Jan 12 16:16:09 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy	Fri Jan 12 16:19:44 2001 +0100
@@ -1,14 +1,6 @@
(* ID:         $Id$ *)
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
@@ -16,13 +8,7 @@
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:
+text{*An inductive definition consists of introduction rules.

@{thm[display] even.step[no_vars]}
\rulename{even.step}
@@ -31,117 +17,74 @@
\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.*}
+specified as \isa{intro!}

-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.*}
+Our first lemma states that numbers of the form $2\times k$ are even. *}
lemma two_times_even[intro!]: "#2*k \<in> even"
apply (induct "k")
+txt{*
+The first step is induction on the natural number \isa{k}, which leaves
+two subgoals:
+@{subgoals[display,indent=0,margin=65]}
+Here \isa{auto} simplifies both subgoals so that they match the introduction
+rules, which then are applied automatically.*};
apply auto
done

-text{* The first step is induction on the natural number \isa{k}, which leaves
-two subgoals:
-
-pr(latex xsymbols symbols);
-\isanewline
-goal\ {\isacharparenleft}lemma\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline
-
-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"
-done

text{*our first rule induction!*}
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
apply (erule even.induct)
- apply simp
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
apply clarify
-apply (rule_tac x = "Suc k" in exI)
-apply simp
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply (rule_tac x = "Suc k" in exI, simp)
done
-text{*
-\isanewline
-goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
-n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\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{\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
-
-\isanewline
-goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline
-n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline
-*}

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
+by (blast intro: dvd_imp_even even_imp_dvd)

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)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
oops
-text{*
-\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{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)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
apply auto
done

-text{*
-\isanewline
-n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline
-\ {\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
-*}
+text{*...and prove it in a separate step*}
+lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"
+by (drule even_imp_even_minus_2, simp)

-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 [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
-apply (blast dest: Suc_Suc_even_imp_even)
-done
+by (blast dest: Suc_Suc_even_imp_even)

end