1.1 --- a/doc-src/TutorialI/Inductive/Mutual.thy	Sun Apr 09 18:51:23 2006 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/Mutual.thy	Sun Apr 09 19:29:44 2006 +0200
     1.3 @@ -8,28 +8,28 @@
     1.4  natural numbers:
     1.5  *}
     1.6  
     1.7 -consts even :: "nat set"
     1.8 -       odd  :: "nat set"
     1.9 +consts Even :: "nat set"
    1.10 +       Odd  :: "nat set"
    1.11  
    1.12 -inductive even odd
    1.13 +inductive Even Odd
    1.14  intros
    1.15 -zero:  "0 \<in> even"
    1.16 -evenI: "n \<in> odd \<Longrightarrow> Suc n \<in> even"
    1.17 -oddI:  "n \<in> even \<Longrightarrow> Suc n \<in> odd"
    1.18 +zero:  "0 \<in> Even"
    1.19 +EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
    1.20 +OddI:  "n \<in> Even \<Longrightarrow> Suc n \<in> Odd"
    1.21  
    1.22  text{*\noindent
    1.23  The mutually inductive definition of multiple sets is no different from
    1.24  that of a single set, except for induction: just as for mutually recursive
    1.25  datatypes, induction needs to involve all the simultaneously defined sets. In
    1.26 -the above case, the induction rule is called @{thm[source]even_odd.induct}
    1.27 +the above case, the induction rule is called @{thm[source]Even_Odd.induct}
    1.28  (simply concatenate the names of the sets involved) and has the conclusion
    1.29 -@{text[display]"(?x \<in> even \<longrightarrow> ?P ?x) \<and> (?y \<in> odd \<longrightarrow> ?Q ?y)"}
    1.30 +@{text[display]"(?x \<in> Even \<longrightarrow> ?P ?x) \<and> (?y \<in> Odd \<longrightarrow> ?Q ?y)"}
    1.31  
    1.32  If we want to prove that all even numbers are divisible by two, we have to
    1.33  generalize the statement as follows:
    1.34  *}
    1.35  
    1.36 -lemma "(m \<in> even \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
    1.37 +lemma "(m \<in> Even \<longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<longrightarrow> 2 dvd (Suc n))"
    1.38  
    1.39  txt{*\noindent
    1.40  The proof is by rule induction. Because of the form of the induction theorem,
    1.41 @@ -37,7 +37,7 @@
    1.42  inductive definitions:
    1.43  *}
    1.44  
    1.45 -apply(rule even_odd.induct)
    1.46 +apply(rule Even_Odd.induct)
    1.47  
    1.48  txt{*
    1.49  @{subgoals[display,indent=0]}

     2.1 --- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Sun Apr 09 18:51:23 2006 +0200
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Sun Apr 09 19:29:44 2006 +0200
     2.3 @@ -26,24 +26,24 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  \isacommand{consts}\isamarkupfalse%
     2.7 -\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
     2.8 -\ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
     2.9 +\ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
    2.10 +\ \ \ \ \ \ \ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
    2.11  \isanewline
    2.12  \isacommand{inductive}\isamarkupfalse%
    2.13 -\ even\ odd\isanewline
    2.14 +\ Even\ Odd\isanewline
    2.15  \isakeyword{intros}\isanewline
    2.16 -zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
    2.17 -evenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
    2.18 -oddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequoteclose}%
    2.19 +zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
    2.20 +EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline
    2.21 +OddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ Even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Odd{\isachardoublequoteclose}%
    2.22  \begin{isamarkuptext}%
    2.23  \noindent
    2.24  The mutually inductive definition of multiple sets is no different from
    2.25  that of a single set, except for induction: just as for mutually recursive
    2.26  datatypes, induction needs to involve all the simultaneously defined sets. In
    2.27 -the above case, the induction rule is called \isa{even{\isacharunderscore}odd{\isachardot}induct}
    2.28 +the above case, the induction rule is called \isa{Even{\isacharunderscore}Odd{\isachardot}induct}
    2.29  (simply concatenate the names of the sets involved) and has the conclusion
    2.30  \begin{isabelle}%
    2.31 -\ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
    2.32 +\ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ Even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ Odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
    2.33  \end{isabelle}
    2.34  
    2.35  If we want to prove that all even numbers are divisible by two, we have to
    2.36 @@ -51,7 +51,7 @@
    2.37  \end{isamarkuptext}%
    2.38  \isamarkuptrue%
    2.39  \isacommand{lemma}\isamarkupfalse%
    2.40 -\ {\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}%
    2.41 +\ {\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}%
    2.42  \isadelimproof
    2.43  %
    2.44  \endisadelimproof
    2.45 @@ -66,12 +66,12 @@
    2.46  \end{isamarkuptxt}%
    2.47  \isamarkuptrue%
    2.48  \isacommand{apply}\isamarkupfalse%
    2.49 -{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
    2.50 +{\isacharparenleft}rule\ Even{\isacharunderscore}Odd{\isachardot}induct{\isacharparenright}%
    2.51  \begin{isamarkuptxt}%
    2.52  \begin{isabelle}%
    2.53  \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
    2.54 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline
    2.55 -\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Mutual{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    2.56 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline
    2.57 +\ {\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}%
    2.58  \end{isabelle}
    2.59  The first two subgoals are proved by simplification and the final one can be
    2.60  proved in the same manner as in \S\ref{sec:rule-induction}