author wenzelm Sun, 09 Apr 2006 19:29:44 +0200 changeset 19389 0d57259fea82 parent 19388 5cfa11eeddfe child 19390 6c7383f80ad1
Even/Odd: avoid clash with even/odd of Main HOL;
--- a/doc-src/TutorialI/Inductive/Mutual.thy	Sun Apr 09 18:51:23 2006 +0200
+++ b/doc-src/TutorialI/Inductive/Mutual.thy	Sun Apr 09 19:29:44 2006 +0200
@@ -8,28 +8,28 @@
natural numbers:
*}

-consts even :: "nat set"
-       odd  :: "nat set"
+consts Even :: "nat set"
+       Odd  :: "nat set"

-inductive even odd
+inductive Even Odd
intros
-zero:  "0 \<in> even"
-evenI: "n \<in> odd \<Longrightarrow> Suc n \<in> even"
-oddI:  "n \<in> even \<Longrightarrow> Suc n \<in> odd"
+zero:  "0 \<in> Even"
+EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
+OddI:  "n \<in> Even \<Longrightarrow> Suc n \<in> Odd"

text{*\noindent
The mutually inductive definition of multiple sets is no different from
that of a single set, except for induction: just as for mutually recursive
datatypes, induction needs to involve all the simultaneously defined sets. In
-the above case, the induction rule is called @{thm[source]even_odd.induct}
+the above case, the induction rule is called @{thm[source]Even_Odd.induct}
(simply concatenate the names of the sets involved) and has the conclusion
-@{text[display]"(?x \<in> even \<longrightarrow> ?P ?x) \<and> (?y \<in> odd \<longrightarrow> ?Q ?y)"}
+@{text[display]"(?x \<in> Even \<longrightarrow> ?P ?x) \<and> (?y \<in> Odd \<longrightarrow> ?Q ?y)"}

If we want to prove that all even numbers are divisible by two, we have to
generalize the statement as follows:
*}

-lemma "(m \<in> even \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
+lemma "(m \<in> Even \<longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<longrightarrow> 2 dvd (Suc n))"

txt{*\noindent
The proof is by rule induction. Because of the form of the induction theorem,
@@ -37,7 +37,7 @@
inductive definitions:
*}

-apply(rule even_odd.induct)
+apply(rule Even_Odd.induct)

txt{*
@{subgoals[display,indent=0]}
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Sun Apr 09 18:51:23 2006 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Sun Apr 09 19:29:44 2006 +0200
@@ -26,24 +26,24 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{inductive}\isamarkupfalse%
-\ even\ odd\isanewline
+\ Even\ Odd\isanewline
\isakeyword{intros}\isanewline
-evenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
-oddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequoteclose}%
+EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
+OddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ Even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Odd{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The mutually inductive definition of multiple sets is no different from
that of a single set, except for induction: just as for mutually recursive
datatypes, induction needs to involve all the simultaneously defined sets. In
-the above case, the induction rule is called \isa{even{\isacharunderscore}odd{\isachardot}induct}
+the above case, the induction rule is called \isa{Even{\isacharunderscore}Odd{\isachardot}induct}
(simply concatenate the names of the sets involved) and has the conclusion
\begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
+\ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ Even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ Odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
\end{isabelle}

If we want to prove that all even numbers are divisible by two, we have to
@@ -51,7 +51,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymin}\ Even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ Odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
%
@@ -66,12 +66,12 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
+{\isacharparenleft}rule\ Even{\isacharunderscore}Odd{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\begin{isabelle}%
proved in the same manner as in \S\ref{sec:rule-induction}