# HG changeset patch # User nipkow # Date 978433473 -3600 # Node ID cd1a2bee55492d443742c18f681d5ecdf29fe8a8 # Parent 0d36ace55e5aedde4d0417f5faa64388b842cc08 *** empty log message *** diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/Inductive/Even.tex --- 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 diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/Inductive/Mutual.thy --- /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 \ even" +evenI: "n \ odd \ Suc n \ even" +oddI: "n \ even \ Suc n \ 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 \ even \ ?P ?x) \ (?y \ odd \ ?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 \ even \ 2 dvd m) \ (n \ odd \ 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 diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/Inductive/ROOT.ML --- 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"; diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/Inductive/document/Mutual.tex --- /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: diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/Inductive/inductive.tex --- 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} diff -r 0d36ace55e5a -r cd1a2bee5549 doc-src/TutorialI/IsaMakefile --- 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