doc-src/TutorialI/Inductive/Even.thy

 (* 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
 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:
+text{*An inductive definition consists of introduction rules. 
 
 @{thm[display] even.step[no_vars]}
 \rulename{even.step}
 
 @{thm[display] even.induct[no_vars]}
 \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);
-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
+by (auto simp add: dvd_def)
 
 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)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply (simp_all add: dvd_def)
+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{*
-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{3}}\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
-
-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
+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{*
-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)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
 apply auto
 done
 
-text{*
-proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
-\isanewline
-goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharparenright}{\isacharcolon}\isanewline
-n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline
-\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\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