--- a/doc-src/TutorialI/Inductive/Even.tex Tue Jan 02 11:03:37 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Even.tex Tue Jan 02 12:04:33 2001 +0100
@@ -80,6 +80,7 @@
\end{isabelle}
\subsection{Rule induction}
+\label{sec:rule-induction}
From the definition of the set
\isa{even}, Isabelle has
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/Mutual.thy Tue Jan 02 12:04:33 2001 +0100
@@ -0,0 +1,59 @@
+(*<*)theory Mutual = Main:(*>*)
+
+subsection{*Mutual inductive definitions*}
+
+text{*
+Just as there are datatypes defined by mutual recursion, there are sets defined
+by mutual induction. As a trivial example we consider the even and odd natural numbers:
+*}
+
+consts even :: "nat set"
+ odd :: "nat set"
+
+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"
+
+text{*\noindent
+The simultaneous 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} (simply concenate 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)"}
+
+If we want to prove that all even numbers are divisible by 2, 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))"
+
+txt{*\noindent
+The proof is by rule induction. Because of the form of the induction theorem, it is
+applied by @{text rule} rather than @{text erule} as for ordinary inductive definitions:
+*}
+
+apply(rule even_odd.induct)
+
+txt{*
+@{subgoals[display,indent=0]}
+The first two subgoals are proved by simplification and the final one can be
+proved in the same manner as in \S\ref{sec:rule-induction}
+where the same subgoal was encountered before.
+We do not show the proof script.
+*}
+(*<*)
+ apply simp
+ apply simp
+apply(simp add:dvd_def)
+apply(clarify)
+apply(rule_tac x = "Suc k" in exI)
+apply simp
+done
+(*>*)
+(*
+Exercise: 1 : odd
+*)
+(*<*)end(*>*)
\ No newline at end of file
--- a/doc-src/TutorialI/Inductive/ROOT.ML Tue Jan 02 11:03:37 2001 +0100
+++ b/doc-src/TutorialI/Inductive/ROOT.ML Tue Jan 02 12:04:33 2001 +0100
@@ -1,5 +1,6 @@
use "../settings.ML";
use_thy "Even";
+use_thy "Mutual";
use_thy "Star";
use_thy "AB";
use_thy "Advanced";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Tue Jan 02 12:04:33 2001 +0100
@@ -0,0 +1,56 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Mutual}%
+%
+\isamarkupsubsection{Mutual inductive definitions%
+}
+%
+\begin{isamarkuptext}%
+Just as there are datatypes defined by mutual recursion, there are sets defined
+by mutual induction. As a trivial example we consider the even and odd natural numbers:%
+\end{isamarkuptext}%
+\isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
+\isanewline
+\isacommand{inductive}\ even\ odd\isanewline
+\isakeyword{intros}\isanewline
+zero{\isacharcolon}\ \ {\isachardoublequote}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequote}\isanewline
+evenI{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline
+oddI{\isacharcolon}\ \ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+The simultaneous 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} (simply concenate 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}%
+\end{isabelle}
+
+If we want to prove that all even numbers are divisible by 2, we have to generalize
+the statement as follows:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+The proof is by rule induction. Because of the form of the induction theorem, it is
+applied by \isa{rule} rather than \isa{erule} as for ordinary inductive definitions:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
+\end{isabelle}
+The first two subgoals are proved by simplification and the final one can be
+proved in the same manner as in \S\ref{sec:rule-induction}
+where the same subgoal was encountered before.
+We do not show the proof script.%
+\end{isamarkuptxt}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/TutorialI/Inductive/inductive.tex Tue Jan 02 11:03:37 2001 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex Tue Jan 02 12:04:33 2001 +0100
@@ -14,6 +14,7 @@
of advanced forms of inductive definitions.
\input{Inductive/Even}
+\input{Inductive/document/Mutual}
\input{Inductive/document/Star}
\section{Advanced inductive definitions}
--- a/doc-src/TutorialI/IsaMakefile Tue Jan 02 11:03:37 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile Tue Jan 02 12:04:33 2001 +0100
@@ -138,7 +138,8 @@
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
- Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Advanced.thy
+ Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
+ Inductive/Advanced.thy
$(USEDIR) Inductive
@rm -f tutorial.dvi