updated;
authorwenzelm
Wed Dec 06 21:10:40 2000 +0100 (2000-12-06)
changeset 10617adc0ed64a120
parent 10616 ad39ca9477d5
child 10618 5b96bc5fbec3
updated;
doc-src/AxClass/generated/isabellesym.sty
doc-src/TutorialI/Advanced/document/simp.tex
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Inductive/document/Even.tex
doc-src/TutorialI/Inductive/document/Star.tex
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Types/document/Axioms.tex
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Typedef.tex
doc-src/TutorialI/isabellesym.sty
     1.1 --- a/doc-src/AxClass/generated/isabellesym.sty	Wed Dec 06 20:45:36 2000 +0100
     1.2 +++ b/doc-src/AxClass/generated/isabellesym.sty	Wed Dec 06 21:10:40 2000 +0100
     1.3 @@ -43,6 +43,32 @@
     1.4  \newcommand{\isasymX}{\isamath{\mathcal{X}}}
     1.5  \newcommand{\isasymY}{\isamath{\mathcal{Y}}}
     1.6  \newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
     1.7 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
     1.8 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
     1.9 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
    1.10 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
    1.11 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
    1.12 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
    1.13 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
    1.14 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
    1.15 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
    1.16 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
    1.17 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
    1.18 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
    1.19 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
    1.20 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
    1.21 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
    1.22 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
    1.23 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
    1.24 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
    1.25 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
    1.26 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
    1.27 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
    1.28 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
    1.29 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
    1.30 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
    1.31 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
    1.32 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
    1.33  \newcommand{\isasymalpha}{\isamath{\alpha}}
    1.34  \newcommand{\isasymbeta}{\isamath{\beta}}
    1.35  \newcommand{\isasymgamma}{\isamath{\gamma}}
     2.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex	Wed Dec 06 20:45:36 2000 +0100
     2.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex	Wed Dec 06 21:10:40 2000 +0100
     2.3 @@ -28,7 +28,7 @@
     2.4  controlled by so-called \bfindex{congruence rules}. This is the one for
     2.5  \isa{{\isasymlongrightarrow}}:
     2.6  \begin{isabelle}%
     2.7 -\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}%
     2.8 +\ \ \ \ \ P\ {\isacharequal}\ P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharparenleft}P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}%
     2.9  \end{isabelle}
    2.10  It should be read as follows:
    2.11  In order to simplify \isa{P\ {\isasymlongrightarrow}\ Q} to \isa{P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}},
    2.12 @@ -38,14 +38,15 @@
    2.13  Here are some more examples.  The congruence rules for bounded
    2.14  quantifiers supply contextual information about the bound variable:
    2.15  \begin{isabelle}%
    2.16 -\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
    2.17 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
    2.18 +\ \ \ \ \ A\ {\isacharequal}\ B\ {\isasymLongrightarrow}\isanewline
    2.19 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
    2.20  \end{isabelle}
    2.21  The congruence rule for conditional expressions supply contextual
    2.22  information for simplifying the arms:
    2.23  \begin{isabelle}%
    2.24 -\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
    2.25 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
    2.26 +\ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\isanewline
    2.27 +\ \ \ \ \ {\isacharparenleft}c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    2.28 +\ \ \ \ \ {\isacharparenleft}{\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
    2.29  \end{isabelle}
    2.30  A congruence rule can also \emph{prevent} simplification of some arguments.
    2.31  Here is an alternative congruence rule for conditional expressions:
    2.32 @@ -72,7 +73,7 @@
    2.33  \begin{warn}
    2.34  The congruence rule \isa{conj{\isacharunderscore}cong}
    2.35  \begin{isabelle}%
    2.36 -\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}%
    2.37 +\ \ \ \ \ P\ {\isacharequal}\ P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharparenleft}P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}%
    2.38  \end{isabelle}
    2.39  is occasionally useful but not a default rule; you have to use it explicitly.
    2.40  \end{warn}%
     3.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Dec 06 20:45:36 2000 +0100
     3.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Dec 06 21:10:40 2000 +0100
     3.3 @@ -73,12 +73,11 @@
     3.4  \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
     3.5  \begin{isamarkuptxt}%
     3.6  \begin{isabelle}%
     3.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
     3.8 -\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
     3.9 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    3.10 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
    3.11 -\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    3.12 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    3.13 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
    3.14 +\ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    3.15 +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    3.16 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    3.17 +\ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    3.18  \end{isabelle}
    3.19  Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
    3.20  \end{isamarkuptxt}%
    3.21 @@ -92,10 +91,10 @@
    3.22  \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    3.23  \begin{isamarkuptxt}%
    3.24  \begin{isabelle}%
    3.25 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
    3.26 -\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    3.27 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    3.28 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    3.29 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\isanewline
    3.30 +\ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    3.31 +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    3.32 +\ \ \ \ \ \ \ \ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    3.33  \end{isabelle}
    3.34  It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its
    3.35  first element. The rest is practically automatic:%
    3.36 @@ -171,9 +170,10 @@
    3.37  \noindent
    3.38  After simplification and clarification the subgoal has the following compact form
    3.39  \begin{isabelle}%
    3.40 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
    3.41 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
    3.42 -\ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}%
    3.43 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline
    3.44 +\ \ \ \ \ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    3.45 +\ \ \ \ \ \ \ \ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
    3.46 +\ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}%
    3.47  \end{isabelle}
    3.48  and invites a proof by induction on \isa{i}:%
    3.49  \end{isamarkuptxt}%
    3.50 @@ -183,14 +183,15 @@
    3.51  \noindent
    3.52  After simplification the base case boils down to
    3.53  \begin{isabelle}%
    3.54 -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
    3.55 -\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M%
    3.56 +\ {\isadigit{1}}{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline
    3.57 +\ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    3.58 +\ \ \ \ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M%
    3.59  \end{isabelle}
    3.60  The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
    3.61  holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
    3.62  is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
    3.63  \begin{isabelle}%
    3.64 -\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
    3.65 +\ \ \ \ \ {\isasymexists}a{\isachardot}\ {\isacharquery}P\ a\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
    3.66  \end{isabelle}
    3.67  When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
    3.68  \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
     4.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Dec 06 20:45:36 2000 +0100
     4.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Dec 06 21:10:40 2000 +0100
     4.3 @@ -121,7 +121,7 @@
     4.4  into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
     4.5  \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
     4.6  \begin{isabelle}%
     4.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
     4.8 +\ \ \ \ \ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
     4.9  \end{isabelle}
    4.10  The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
    4.11  in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
     5.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Dec 06 20:45:36 2000 +0100
     5.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Dec 06 21:10:40 2000 +0100
     5.3 @@ -127,7 +127,7 @@
     5.4  \noindent
     5.5  After simplification and clarification we are left with
     5.6  \begin{isabelle}%
     5.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}%
     5.8 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}%
     5.9  \end{isabelle}
    5.10  This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
    5.11  checker works backwards (from \isa{t} to \isa{s}), we cannot use the
    5.12 @@ -135,9 +135,9 @@
    5.13  forward direction. Fortunately the converse induction theorem
    5.14  \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
    5.15  \begin{isabelle}%
    5.16 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
    5.17 -\ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
    5.18 -\ \ \ \ \ {\isasymLongrightarrow}\ P\ a%
    5.19 +\ \ \ \ \ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
    5.20 +\ \ \ \ \ P\ b\ {\isasymLongrightarrow}\isanewline
    5.21 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}y\ z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ P\ z\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
    5.22  \end{isabelle}
    5.23  It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
    5.24  \isa{P\ a} provided each step backwards from a predecessor \isa{z} of
     6.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 20:45:36 2000 +0100
     6.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 21:10:40 2000 +0100
     6.3 @@ -96,8 +96,8 @@
     6.4  1 on our way from 0 to 2. Formally, we appeal to the following discrete
     6.5  intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
     6.6  \begin{isabelle}%
     6.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
     6.8 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
     6.9 +\ \ \ \ \ {\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}\ {\isasymLongrightarrow}\isanewline
    6.10 +\ \ \ \ \ f\ {\isadigit{0}}\ {\isasymle}\ k\ {\isasymLongrightarrow}\ k\ {\isasymle}\ f\ n\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
    6.11  \end{isabelle}
    6.12  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
    6.13  \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
     7.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Wed Dec 06 20:45:36 2000 +0100
     7.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Wed Dec 06 21:10:40 2000 +0100
     7.3 @@ -36,7 +36,7 @@
     7.4  We completely forgot about "rule inversion". 
     7.5  
     7.6  \begin{isabelle}%
     7.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%
     7.8 +\ \ \ \ \ a\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
     7.9  \end{isabelle}
    7.10  \rulename{even.cases}
    7.11  
    7.12 @@ -50,7 +50,7 @@
    7.13  \isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases%
    7.14  \begin{isamarkuptext}%
    7.15  \begin{isabelle}%
    7.16 -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
    7.17 +\ \ \ \ \ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
    7.18  \end{isabelle}
    7.19  \rulename{Suc_Suc_cases}
    7.20  
    7.21 @@ -65,7 +65,7 @@
    7.22  this is what we get:
    7.23  
    7.24  \begin{isabelle}%
    7.25 -\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
    7.26 +\ \ \ \ \ Apply\ f\ args\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ f\ {\isasymin}\ F\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
    7.27  \end{isabelle}
    7.28  \rulename{gterm_Apply_elim}%
    7.29  \end{isamarkuptext}%
     8.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 06 20:45:36 2000 +0100
     8.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 06 21:10:40 2000 +0100
     8.3 @@ -31,7 +31,7 @@
     8.4  \rulename{even.step}
     8.5  
     8.6  \begin{isabelle}%
     8.7 -\ \ \ \ \ {\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%
     8.8 +\ \ \ \ \ xa\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xa%
     8.9  \end{isabelle}
    8.10  \rulename{even.induct}
    8.11  
     9.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Dec 06 20:45:36 2000 +0100
     9.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Dec 06 21:10:40 2000 +0100
     9.3 @@ -51,9 +51,9 @@
     9.4  To prove transitivity, we need rule induction, i.e.\ theorem
     9.5  \isa{rtc{\isachardot}induct}:
     9.6  \begin{isabelle}%
     9.7 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
     9.8 -\ \ \ \ \ \ \ \ {\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
     9.9 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
    9.10 +\ \ \ \ \ {\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
    9.11 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    9.12 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ y\ z\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
    9.13  \end{isabelle}
    9.14  It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
    9.15  i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the
    9.16 @@ -110,8 +110,9 @@
    9.17  \begin{isabelle}%
    9.18  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
    9.19  \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
    9.20 -\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
    9.21 -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
    9.22 +\ \ \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\isanewline
    9.23 +\ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
    9.24 +\ \ \ \ \ \ \ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
    9.25  \end{isabelle}%
    9.26  \end{isamarkuptxt}%
    9.27  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
    9.28 @@ -156,7 +157,7 @@
    9.29  \begin{exercise}\label{ex:converse-rtc-step}
    9.30  Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
    9.31  \begin{isabelle}%
    9.32 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
    9.33 +\ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
    9.34  \end{isabelle}
    9.35  \end{exercise}
    9.36  \begin{exercise}
    10.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Dec 06 20:45:36 2000 +0100
    10.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Dec 06 21:10:40 2000 +0100
    10.3 @@ -95,7 +95,7 @@
    10.4  \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
    10.5  \begin{isamarkuptext}%
    10.6  \noindent
    10.7 -yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
    10.8 +yielding \isa{A\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
    10.9  You can go one step further and include these derivations already in the
   10.10  statement of your original lemma, thus avoiding the intermediate step:%
   10.11  \end{isamarkuptext}%
   10.12 @@ -182,8 +182,7 @@
   10.13  \begin{isamarkuptxt}%
   10.14  \begin{isabelle}%
   10.15  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
   10.16 -\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\isanewline
   10.17 -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   10.18 +\ \ \ \ \ \ \ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\ i\ {\isacharequal}\ Suc\ nat\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   10.19  \end{isabelle}%
   10.20  \end{isamarkuptxt}%
   10.21  \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
   10.22 @@ -196,7 +195,7 @@
   10.23  proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
   10.24  (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).
   10.25  Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity
   10.26 -(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
   10.27 +(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ j\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
   10.28  Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
   10.29  which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
   10.30  \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
   10.31 @@ -268,7 +267,7 @@
   10.32  \noindent
   10.33  The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
   10.34  \begin{isabelle}%
   10.35 -\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
   10.36 +\ \ \ \ \ m\ {\isacharless}\ Suc\ n\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
   10.37  \end{isabelle}
   10.38  
   10.39  Now it is straightforward to derive the original version of
    11.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Dec 06 20:45:36 2000 +0100
    11.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Dec 06 21:10:40 2000 +0100
    11.3 @@ -299,8 +299,8 @@
    11.4  In contrast to splitting the conclusion, this actually creates two
    11.5  separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
    11.6  \begin{isabelle}%
    11.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
    11.8 -\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
    11.9 +\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
   11.10 +\ {\isadigit{2}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
   11.11  \end{isabelle}
   11.12  If you need to split both in the assumptions and the conclusion,
   11.13  use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
    12.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 06 20:45:36 2000 +0100
    12.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 06 21:10:40 2000 +0100
    12.3 @@ -61,8 +61,9 @@
    12.4  \isacommand{recdef} has been supplied with the congruence theorem
    12.5  \isa{map{\isacharunderscore}cong}:
    12.6  \begin{isabelle}%
    12.7 -\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
    12.8 -\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
    12.9 +\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline
   12.10 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
   12.11 +\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
   12.12  \end{isabelle}
   12.13  Its second premise expresses (indirectly) that the second argument of
   12.14  \isa{map} is only applied to elements of its third argument. Congruence
    13.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex	Wed Dec 06 20:45:36 2000 +0100
    13.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Dec 06 21:10:40 2000 +0100
    13.3 @@ -68,8 +68,8 @@
    13.4  specialized to type \isa{bool}, as subgoals:
    13.5  \begin{isabelle}%
    13.6  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
    13.7 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
    13.8 -\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
    13.9 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
   13.10 +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
   13.11  \ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
   13.12  \end{isabelle}
   13.13  Fortunately, the proof is easy for blast, once we have unfolded the definitions
    14.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Wed Dec 06 20:45:36 2000 +0100
    14.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Wed Dec 06 21:10:40 2000 +0100
    14.3 @@ -75,12 +75,12 @@
    14.4  %
    14.5  \begin{isamarkuptext}%
    14.6  \begin{isabelle}%
    14.7 -\ \ \ \ \ {\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
    14.8 +\ \ \ \ \ i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ k\ {\isasymle}\ l\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
    14.9  \end{isabelle}
   14.10  \rulename{mult_le_mono}
   14.11  
   14.12  \begin{isabelle}%
   14.13 -\ \ \ \ \ {\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k%
   14.14 +\ \ \ \ \ i\ {\isacharless}\ j\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k%
   14.15  \end{isabelle}
   14.16  \rulename{mult_less_mono1}
   14.17  
   14.18 @@ -160,12 +160,12 @@
   14.19  \rulename{DIVISION_BY_ZERO_MOD}
   14.20  
   14.21  \begin{isabelle}%
   14.22 -\ \ \ \ \ {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
   14.23 +\ \ \ \ \ m\ dvd\ n\ {\isasymLongrightarrow}\ n\ dvd\ m\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
   14.24  \end{isabelle}
   14.25  \rulename{dvd_anti_sym}
   14.26  
   14.27  \begin{isabelle}%
   14.28 -\ \ \ \ \ {\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}%
   14.29 +\ \ \ \ \ k\ dvd\ m\ {\isasymLongrightarrow}\ k\ dvd\ n\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}%
   14.30  \end{isabelle}
   14.31  \rulename{dvd_add}
   14.32  
    15.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex	Wed Dec 06 20:45:36 2000 +0100
    15.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex	Wed Dec 06 21:10:40 2000 +0100
    15.3 @@ -204,7 +204,7 @@
    15.4  Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
    15.5  elimination with \isa{le{\isacharunderscore}SucE}
    15.6  \begin{isabelle}%
    15.7 -\ \ \ \ \ {\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
    15.8 +\ \ \ \ \ {\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R%
    15.9  \end{isabelle}
   15.10  reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and
   15.11  \isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
   15.12 @@ -231,10 +231,10 @@
   15.13  \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}%
   15.14  \begin{isamarkuptxt}%
   15.15  \begin{isabelle}%
   15.16 -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
   15.17 -\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
   15.18 -\ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
   15.19 -\ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
   15.20 +\ {\isadigit{1}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
   15.21 +\ {\isadigit{2}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
   15.22 +\ {\isadigit{3}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
   15.23 +\ {\isadigit{4}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
   15.24  \end{isabelle}
   15.25  The resulting subgoals are easily solved by simplification:%
   15.26  \end{isamarkuptxt}%
    16.1 --- a/doc-src/TutorialI/isabellesym.sty	Wed Dec 06 20:45:36 2000 +0100
    16.2 +++ b/doc-src/TutorialI/isabellesym.sty	Wed Dec 06 21:10:40 2000 +0100
    16.3 @@ -43,6 +43,32 @@
    16.4  \newcommand{\isasymX}{\isamath{\mathcal{X}}}
    16.5  \newcommand{\isasymY}{\isamath{\mathcal{Y}}}
    16.6  \newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
    16.7 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
    16.8 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
    16.9 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
   16.10 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
   16.11 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
   16.12 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
   16.13 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
   16.14 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
   16.15 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
   16.16 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
   16.17 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
   16.18 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
   16.19 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
   16.20 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
   16.21 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
   16.22 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
   16.23 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
   16.24 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
   16.25 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
   16.26 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
   16.27 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
   16.28 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
   16.29 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
   16.30 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
   16.31 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
   16.32 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
   16.33  \newcommand{\isasymalpha}{\isamath{\alpha}}
   16.34  \newcommand{\isasymbeta}{\isamath{\beta}}
   16.35  \newcommand{\isasymgamma}{\isamath{\gamma}}