1.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Mar 15 10:58:29 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Mar 15 10:58:49 2004 +0100
     1.3 @@ -40,7 +40,8 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
     1.8 +\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline
     1.9 +\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P%
    1.10  \end{isabelle}
    1.11  \rulename{even.cases}
    1.12  
    1.13 @@ -57,7 +58,7 @@
    1.14  %
    1.15  \begin{isamarkuptext}%
    1.16  \begin{isabelle}%
    1.17 -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
    1.18 +\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
    1.19  \end{isabelle}
    1.20  \rulename{Suc_Suc_cases}
    1.21  

     2.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Mar 15 10:58:29 2004 +0100
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Mar 15 10:58:49 2004 +0100
     2.3 @@ -17,12 +17,13 @@
     2.4  An inductive definition consists of introduction rules. 
     2.5  
     2.6  \begin{isabelle}%
     2.7 -\ \ \ \ \ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even%
     2.8 +\ \ \ \ \ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even%
     2.9  \end{isabelle}
    2.10  \rulename{even.step}
    2.11  
    2.12  \begin{isabelle}%
    2.13 -\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ xa%
    2.14 +\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline
    2.15 +\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ xa%
    2.16  \end{isabelle}
    2.17  \rulename{even.induct}
    2.18  
    2.19 @@ -40,8 +41,8 @@
    2.20  The first step is induction on the natural number \isa{k}, which leaves
    2.21  two subgoals:
    2.22  \begin{isabelle}%
    2.23 -\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline
    2.24 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even%
    2.25 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ Even{\isachardot}even\isanewline
    2.26 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ Even{\isachardot}even%
    2.27  \end{isabelle}
    2.28  Here \isa{auto} simplifies both subgoals so that they match the introduction
    2.29  rules, which then are applied automatically.%
    2.30 @@ -73,7 +74,7 @@
    2.31  \begin{isamarkuptxt}%
    2.32  \begin{isabelle}%
    2.33  \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
    2.34 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    2.35 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    2.36  \end{isabelle}%
    2.37  \end{isamarkuptxt}%
    2.38  \isamarkuptrue%
    2.39 @@ -81,7 +82,7 @@
    2.40  %
    2.41  \begin{isamarkuptxt}%
    2.42  \begin{isabelle}%
    2.43 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k%
    2.44 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k%
    2.45  \end{isabelle}%
    2.46  \end{isamarkuptxt}%
    2.47  \isamarkuptrue%
    2.48 @@ -89,7 +90,7 @@
    2.49  %
    2.50  \begin{isamarkuptxt}%
    2.51  \begin{isabelle}%
    2.52 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka%
    2.53 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka%
    2.54  \end{isabelle}%
    2.55  \end{isamarkuptxt}%
    2.56  \isamarkuptrue%
    2.57 @@ -115,8 +116,8 @@
    2.58  %
    2.59  \begin{isamarkuptxt}%
    2.60  \begin{isabelle}%
    2.61 -\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline
    2.62 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even%
    2.63 +\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ Even{\isachardot}even\isanewline
    2.64 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ Even{\isachardot}even%
    2.65  \end{isabelle}%
    2.66  \end{isamarkuptxt}%
    2.67  \isamarkuptrue%
    2.68 @@ -132,8 +133,9 @@
    2.69  %
    2.70  \begin{isamarkuptxt}%
    2.71  \begin{isabelle}%
    2.72 -\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline
    2.73 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even%
    2.74 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even\isanewline
    2.75 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\isanewline
    2.76 +\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even%
    2.77  \end{isabelle}%
    2.78  \end{isamarkuptxt}%
    2.79  \isamarkuptrue%

     3.1 --- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Mon Mar 15 10:58:29 2004 +0100
     3.2 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Mon Mar 15 10:58:49 2004 +0100
     3.3 @@ -53,7 +53,7 @@
     3.4  \begin{isabelle}%
     3.5  \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
     3.6  \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline
     3.7 -\ {\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}%
     3.8 +\ {\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}%
     3.9  \end{isabelle}
    3.10  The first two subgoals are proved by simplification and the final one can be
    3.11  proved in the same manner as in \S\ref{sec:rule-induction}