--- 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]}