author paulson Wed, 25 Oct 2000 17:44:48 +0200 changeset 10326 d4fe5ce8a5d5 parent 10325 76f318befccb child 10327 19214ac381cf
minor tinkering
```--- a/doc-src/TutorialI/Inductive/Even.thy	Wed Oct 25 17:43:34 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Wed Oct 25 17:44:48 2000 +0200
@@ -23,10 +23,10 @@
analysis and an induction rule.  We can refer to these theorems by
automatically-generated names:

-@{thm[display] even.step}
+@{thm[display] even.step[no_vars]}
\rulename{even.step}

-@{thm[display] even.induct}
+@{thm[display] even.induct[no_vars]}
\rulename{even.induct}

Attributes can be given to the introduction rules.  Here both rules are
@@ -83,6 +83,12 @@

+\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
@@ -116,13 +122,23 @@
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"
apply (drule even_imp_even_minus_2)
apply simp
done

-lemma Suc_Suc_even_iff [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
+lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)"
apply (blast dest: Suc_Suc_even_imp_even)
done
```