*** empty log message ***
authornipkow
Fri Jan 26 15:50:28 2001 +0100 (2001-01-26)
changeset 1098359961d32b1ae
parent 10982 55c0f9a8df78
child 10984 8f49dcbec859
*** empty log message ***
doc-src/TutorialI/CTL/Base.thy
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/document/Base.tex
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/Functions.thy
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/Types/Typedef.thy
doc-src/TutorialI/Types/document/Typedef.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/todo.tobias
     1.1 --- a/doc-src/TutorialI/CTL/Base.thy	Fri Jan 26 15:02:04 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/Base.thy	Fri Jan 26 15:50:28 2001 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  text{*\noindent
     1.6  Command \isacommand{typedecl} merely declares a new type but without
     1.7 -defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
     1.8 +defining it (see \S\ref{sec:typedecl}). Thus we know nothing
     1.9  about the type other than its existence. That is exactly what we need
    1.10  because @{typ state} really is an implicit parameter of our model.  Of
    1.11  course it would have been more generic to make @{typ state} a type
     2.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 26 15:02:04 2001 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 26 15:50:28 2001 +0100
     2.3 @@ -17,8 +17,9 @@
     2.4                    | AF formula;
     2.5  
     2.6  text{*\noindent
     2.7 -which stands for "always in the future":
     2.8 -on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
     2.9 +which stands for ``\emph{A}lways in the \emph{F}uture'':
    2.10 +on all infinite paths, at some point the formula holds.
    2.11 +Formalizing the notion of an infinite path is easy
    2.12  in HOL: it is simply a function from @{typ nat} to @{typ state}.
    2.13  *};
    2.14  
    2.15 @@ -67,7 +68,7 @@
    2.16  
    2.17  text{*\noindent
    2.18  Because @{term af} is monotone in its second argument (and also its first, but
    2.19 -that is irrelevant) @{term"af A"} has a least fixed point:
    2.20 +that is irrelevant), @{term"af A"} has a least fixed point:
    2.21  *};
    2.22  
    2.23  lemma mono_af: "mono(af A)";
    2.24 @@ -150,8 +151,8 @@
    2.25  infinite @{term A}-avoiding path starting from @{term s}. The reason is
    2.26  that by unfolding @{term lfp} we find that if @{term s} is not in
    2.27  @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
    2.28 -direct successor of @{term s} that is again not in @{term"lfp(af
    2.29 -A)"}. Iterating this argument yields the promised infinite
    2.30 +direct successor of @{term s} that is again not in \mbox{@{term"lfp(af
    2.31 +A)"}}. Iterating this argument yields the promised infinite
    2.32  @{term A}-avoiding path. Let us formalize this sketch.
    2.33  
    2.34  The one-step argument in the sketch above
    2.35 @@ -159,7 +160,7 @@
    2.36  *};
    2.37  
    2.38  lemma not_in_lfp_afD:
    2.39 - "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
    2.40 + "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
    2.41  apply(erule contrapos_np);
    2.42  apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
    2.43  apply(simp add:af_def);
    2.44 @@ -196,8 +197,8 @@
    2.45     \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
    2.46  
    2.47  txt{*\noindent
    2.48 -First we rephrase the conclusion slightly because we need to prove both the path property
    2.49 -and the fact that @{term Q} holds simultaneously:
    2.50 +First we rephrase the conclusion slightly because we need to prove simultaneously
    2.51 +both the path property and the fact that @{term Q} holds:
    2.52  *};
    2.53  
    2.54  apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))");
    2.55 @@ -216,7 +217,7 @@
    2.56  apply(clarsimp);
    2.57  
    2.58  txt{*\noindent
    2.59 -After simplification and clarification the subgoal has the following compact form
    2.60 +After simplification and clarification, the subgoal has the following form
    2.61  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
    2.62  and invites a proof by induction on @{term i}:
    2.63  *};
    2.64 @@ -225,7 +226,7 @@
    2.65   apply(simp);
    2.66  
    2.67  txt{*\noindent
    2.68 -After simplification the base case boils down to
    2.69 +After simplification, the base case boils down to
    2.70  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
    2.71  The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
    2.72  holds. However, we first have to show that such a @{term t} actually exists! This reasoning
    2.73 @@ -345,8 +346,8 @@
    2.74  text{*
    2.75  
    2.76  The language defined above is not quite CTL\@. The latter also includes an
    2.77 -until-operator @{term"EU f g"} with semantics ``there exists a path
    2.78 -where @{term f} is true until @{term g} becomes true''. With the help
    2.79 +until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path
    2.80 +where @{term f} is true \emph{U}ntil @{term g} becomes true''. With the help
    2.81  of an auxiliary function
    2.82  *}
    2.83  
    2.84 @@ -360,7 +361,7 @@
    2.85  
    2.86  text{*\noindent
    2.87  the semantics of @{term EU} is straightforward:
    2.88 -@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
    2.89 +@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}
    2.90  Note that @{term EU} is not definable in terms of the other operators!
    2.91  
    2.92  Model checking @{term EU} is again a least fixed point construction:
    2.93 @@ -457,10 +458,10 @@
    2.94  It is clear that if all sets are finite, they can be represented as lists and the usual
    2.95  set operations are easily implemented. Only @{term lfp} requires a little thought.
    2.96  Fortunately, the HOL Library%
    2.97 -\footnote{See theory \isa{While_Combinator_Example}.}
    2.98 +\footnote{See theory \isa{While_Combinator}.}
    2.99  provides a theorem stating that 
   2.100  in the case of finite sets and a monotone function~@{term F},
   2.101 -the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} until
   2.102 +the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
   2.103  a fixed point is reached. It is actually possible to generate executable functional programs
   2.104  from HOL definitions, but that is beyond the scope of the tutorial.
   2.105  *}
     3.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:02:04 2001 +0100
     3.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:50:28 2001 +0100
     3.3 @@ -42,8 +42,8 @@
     3.4  
     3.5  text{*\noindent
     3.6  The first three equations should be self-explanatory. The temporal formula
     3.7 -@{term"AX f"} means that @{term f} is true in all next states whereas
     3.8 -@{term"EF f"} means that there exists some future state in which @{term f} is
     3.9 +@{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas
    3.10 +@{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is
    3.11  true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
    3.12  closure. Because of reflexivity, the future includes the present.
    3.13  
    3.14 @@ -68,7 +68,7 @@
    3.15  fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
    3.16  @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
    3.17  find it hard to see that @{term"mc(EF f)"} contains exactly those states from
    3.18 -which there is a path to a state where @{term f} is true, do not worry --- that
    3.19 +which there is a path to a state where @{term f} is true, do not worry --- this
    3.20  will be proved in a moment.
    3.21  
    3.22  First we prove monotonicity of the function inside @{term lfp}
    3.23 @@ -180,7 +180,7 @@
    3.24  text{*
    3.25  \begin{exercise}
    3.26  @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
    3.27 -as that is the ASCII equivalent of @{text"\<exists>"}}
    3.28 +as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
    3.29  (``there exists a next state such that'') with the intended semantics
    3.30  @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
    3.31  Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
     4.1 --- a/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 26 15:02:04 2001 +0100
     4.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 26 15:50:28 2001 +0100
     4.3 @@ -63,7 +63,7 @@
     4.4  \begin{isamarkuptext}%
     4.5  \noindent
     4.6  Command \isacommand{typedecl} merely declares a new type but without
     4.7 -defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
     4.8 +defining it (see \S\ref{sec:typedecl}). Thus we know nothing
     4.9  about the type other than its existence. That is exactly what we need
    4.10  because \isa{state} really is an implicit parameter of our model.  Of
    4.11  course it would have been more generic to make \isa{state} a type
     5.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 26 15:02:04 2001 +0100
     5.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 26 15:50:28 2001 +0100
     5.3 @@ -15,8 +15,9 @@
     5.4  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
     5.5  \begin{isamarkuptext}%
     5.6  \noindent
     5.7 -which stands for "always in the future":
     5.8 -on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
     5.9 +which stands for ``\emph{A}lways in the \emph{F}uture'':
    5.10 +on all infinite paths, at some point the formula holds.
    5.11 +Formalizing the notion of an infinite path is easy
    5.12  in HOL: it is simply a function from \isa{nat} to \isa{state}.%
    5.13  \end{isamarkuptext}%
    5.14  \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
    5.15 @@ -45,7 +46,7 @@
    5.16  \begin{isamarkuptext}%
    5.17  \noindent
    5.18  Because \isa{af} is monotone in its second argument (and also its first, but
    5.19 -that is irrelevant) \isa{af\ A} has a least fixed point:%
    5.20 +that is irrelevant), \isa{af\ A} has a least fixed point:%
    5.21  \end{isamarkuptext}%
    5.22  \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
    5.23  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    5.24 @@ -111,14 +112,14 @@
    5.25  infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
    5.26  that by unfolding \isa{lfp} we find that if \isa{s} is not in
    5.27  \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
    5.28 -direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
    5.29 +direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
    5.30  \isa{A}-avoiding path. Let us formalize this sketch.
    5.31  
    5.32  The one-step argument in the sketch above
    5.33  is proved by a variant of contraposition:%
    5.34  \end{isamarkuptext}%
    5.35  \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
    5.36 -\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    5.37 +\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    5.38  \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
    5.39  \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
    5.40  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
    5.41 @@ -153,8 +154,8 @@
    5.42  \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
    5.43  \begin{isamarkuptxt}%
    5.44  \noindent
    5.45 -First we rephrase the conclusion slightly because we need to prove both the path property
    5.46 -and the fact that \isa{Q} holds simultaneously:%
    5.47 +First we rephrase the conclusion slightly because we need to prove simultaneously
    5.48 +both the path property and the fact that \isa{Q} holds:%
    5.49  \end{isamarkuptxt}%
    5.50  \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
    5.51  \begin{isamarkuptxt}%
    5.52 @@ -170,7 +171,7 @@
    5.53  \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    5.54  \begin{isamarkuptxt}%
    5.55  \noindent
    5.56 -After simplification and clarification the subgoal has the following compact form
    5.57 +After simplification and clarification, the subgoal has the following form
    5.58  \begin{isabelle}%
    5.59  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
    5.60  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
    5.61 @@ -182,7 +183,7 @@
    5.62  \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
    5.63  \begin{isamarkuptxt}%
    5.64  \noindent
    5.65 -After simplification the base case boils down to
    5.66 +After simplification, the base case boils down to
    5.67  \begin{isabelle}%
    5.68  \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
    5.69  \isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
    5.70 @@ -281,8 +282,8 @@
    5.71  \isacommand{done}%
    5.72  \begin{isamarkuptext}%
    5.73  The language defined above is not quite CTL\@. The latter also includes an
    5.74 -until-operator \isa{EU\ f\ g} with semantics ``there exists a path
    5.75 -where \isa{f} is true until \isa{g} becomes true''. With the help
    5.76 +until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
    5.77 +where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help
    5.78  of an auxiliary function%
    5.79  \end{isamarkuptext}%
    5.80  \isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    5.81 @@ -293,7 +294,7 @@
    5.82  \noindent
    5.83  the semantics of \isa{EU} is straightforward:
    5.84  \begin{isabelle}%
    5.85 -\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}%
    5.86 +\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
    5.87  \end{isabelle}
    5.88  Note that \isa{EU} is not definable in terms of the other operators!
    5.89  
    5.90 @@ -320,10 +321,10 @@
    5.91  It is clear that if all sets are finite, they can be represented as lists and the usual
    5.92  set operations are easily implemented. Only \isa{lfp} requires a little thought.
    5.93  Fortunately, the HOL Library%
    5.94 -\footnote{See theory \isa{While_Combinator_Example}.}
    5.95 +\footnote{See theory \isa{While_Combinator}.}
    5.96  provides a theorem stating that 
    5.97  in the case of finite sets and a monotone function~\isa{F},
    5.98 -the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
    5.99 +the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
   5.100  a fixed point is reached. It is actually possible to generate executable functional programs
   5.101  from HOL definitions, but that is beyond the scope of the tutorial.%
   5.102  \end{isamarkuptext}%
     6.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 26 15:02:04 2001 +0100
     6.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 26 15:50:28 2001 +0100
     6.3 @@ -43,8 +43,8 @@
     6.4  \begin{isamarkuptext}%
     6.5  \noindent
     6.6  The first three equations should be self-explanatory. The temporal formula
     6.7 -\isa{AX\ f} means that \isa{f} is true in all next states whereas
     6.8 -\isa{EF\ f} means that there exists some future state in which \isa{f} is
     6.9 +\isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas
    6.10 +\isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is
    6.11  true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive
    6.12  closure. Because of reflexivity, the future includes the present.
    6.13  
    6.14 @@ -68,7 +68,7 @@
    6.15  fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
    6.16  \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
    6.17  find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
    6.18 -which there is a path to a state where \isa{f} is true, do not worry --- that
    6.19 +which there is a path to a state where \isa{f} is true, do not worry --- this
    6.20  will be proved in a moment.
    6.21  
    6.22  First we prove monotonicity of the function inside \isa{lfp}
    6.23 @@ -177,7 +177,7 @@
    6.24  \begin{isamarkuptext}%
    6.25  \begin{exercise}
    6.26  \isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
    6.27 -as that is the ASCII equivalent of \isa{{\isasymexists}}}
    6.28 +as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}}
    6.29  (``there exists a next state such that'') with the intended semantics
    6.30  \begin{isabelle}%
    6.31  \ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
     7.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 26 15:02:04 2001 +0100
     7.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 26 15:50:28 2001 +0100
     7.3 @@ -166,7 +166,7 @@
     7.4  Of course we can also unfold definitions in the middle of a proof.
     7.5  
     7.6  You should normally not turn a definition permanently into a simplification
     7.7 -rule because this defeats the whole purpose of an abbreviation.
     7.8 +rule because this defeats the whole purpose.
     7.9  
    7.10  \begin{warn}
    7.11    If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
     8.1 --- a/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:02:04 2001 +0100
     8.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:50:28 2001 +0100
     8.3 @@ -162,7 +162,7 @@
     8.4  Of course we can also unfold definitions in the middle of a proof.
     8.5  
     8.6  You should normally not turn a definition permanently into a simplification
     8.7 -rule because this defeats the whole purpose of an abbreviation.
     8.8 +rule because this defeats the whole purpose.
     8.9  
    8.10  \begin{warn}
    8.11    If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
     9.1 --- a/doc-src/TutorialI/Rules/rules.tex	Fri Jan 26 15:02:04 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jan 26 15:50:28 2001 +0100
     9.3 @@ -966,7 +966,7 @@
     9.4  
     9.5  \subsection{Definite Descriptions}
     9.6  
     9.7 -In ASCII, we write \isa{SOME} for $\varepsilon$.
     9.8 +In \textsc{ascii}, we write \isa{SOME} for $\varepsilon$.
     9.9  \REMARK{the internal constant is \isa{Eps}}
    9.10  The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
    9.11  description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
    10.1 --- a/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:02:04 2001 +0100
    10.2 +++ b/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:50:28 2001 +0100
    10.3 @@ -79,7 +79,7 @@
    10.4  *}
    10.5  
    10.6  lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
    10.7 -  apply (simp add: expand_fun_eq inj_on_def o_def)
    10.8 +  apply (simp add: expand_fun_eq inj_on_def)
    10.9    apply (auto)
   10.10    done
   10.11  
    11.1 --- a/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:02:04 2001 +0100
    11.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:50:28 2001 +0100
    11.3 @@ -96,7 +96,7 @@
    11.4  \isacommand{by}\ blast
    11.5  \end{isabelle}
    11.6  %
    11.7 -This is the same example using ASCII syntax, illustrating a pitfall: 
    11.8 +This is the same example using \textsc{ascii} syntax, illustrating a pitfall: 
    11.9  \begin{isabelle}
   11.10  \isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)"
   11.11  \end{isabelle}
   11.12 @@ -287,8 +287,8 @@
   11.13  \end{isabelle}
   11.14  
   11.15  Unions can be formed over the values of a given  set.  The syntax is
   11.16 -\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN
   11.17 -x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
   11.18 +\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
   11.19 +x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
   11.20  \begin{isabelle}
   11.21  (b\ \isasymin\
   11.22  (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
   11.23 @@ -320,12 +320,12 @@
   11.24  over a \emph{type}:
   11.25  \begin{isabelle}
   11.26  \ \ \ \ \
   11.27 -({\isasymUnion}x.\ B\ x)\ {==}\
   11.28 +({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
   11.29  ({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
   11.30  \end{isabelle}
   11.31  Abbreviations work as you might expect.  The term on the left-hand side of
   11.32  the
   11.33 -\isa{==} symbol is automatically translated to the right-hand side when the
   11.34 +\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
   11.35  term is parsed, the reverse translation being done when the term is
   11.36  displayed.
   11.37  
   11.38 @@ -523,7 +523,7 @@
   11.39  
   11.40  Theorems involving these concepts can be hard to prove. The following 
   11.41  example is easy, but it cannot be proved automatically. To begin 
   11.42 -with, we need a law that relates the quality of functions to 
   11.43 +with, we need a law that relates the equality of functions to 
   11.44  equality over all arguments: 
   11.45  \begin{isabelle}
   11.46  (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
   11.47 @@ -535,7 +535,7 @@
   11.48  side of function composition: 
   11.49  \begin{isabelle}
   11.50  \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
   11.51 -\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline
   11.52 +\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline
   11.53  \isacommand{apply}\ auto\isanewline
   11.54  \isacommand{done}
   11.55  \end{isabelle}
   11.56 @@ -593,7 +593,7 @@
   11.57  abbreviates an application of image to {\isa{UNIV}}: 
   11.58  \begin{isabelle}
   11.59  \ \ \ \ \ range\ f\
   11.60 -{==}\ f`UNIV
   11.61 +{\isasymrightleftharpoons}\ f`UNIV
   11.62  \end{isabelle}
   11.63  %
   11.64  Few theorems are proved specifically 
   11.65 @@ -845,7 +845,7 @@
   11.66  Induction comes in many forms, including traditional mathematical 
   11.67  induction, structural induction on lists and induction on size. 
   11.68  More general than these is induction over a well-founded relation. 
   11.69 -Such A relation expresses the notion of a terminating process. 
   11.70 +Such a relation expresses the notion of a terminating process. 
   11.71  Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
   11.72  infinite  descending chains
   11.73  \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
   11.74 @@ -944,9 +944,9 @@
   11.75  
   11.76  \section{Fixed Point Operators}
   11.77  
   11.78 -Fixed point operators define sets recursively.  Most users invoke 
   11.79 -them by making an inductive definition, as discussed in
   11.80 -Chap.\ts\ref{chap:inductive} below.  However, they can be used directly.
   11.81 +Fixed point operators define sets recursively.  They are invoked
   11.82 +implicitly when making an inductive definition, as discussed in
   11.83 +Chap.\ts\ref{chap:inductive} below.  However, they can be used directly, too.
   11.84  The
   11.85  \relax{least}  or \relax{strongest} fixed point yields an inductive
   11.86  definition;  the \relax{greatest} or \relax{weakest} fixed point yields a
   11.87 @@ -954,7 +954,7 @@
   11.88  existence  of these fixed points is guaranteed by the Knaster-Tarski
   11.89  theorem. 
   11.90  
   11.91 -The theory works applies only to monotonic functions. Isabelle's 
   11.92 +The theory applies only to monotonic functions. Isabelle's 
   11.93  definition of monotone is overloaded over all orderings:
   11.94  \begin{isabelle}
   11.95  mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
    12.1 --- a/doc-src/TutorialI/Types/Typedef.thy	Fri Jan 26 15:02:04 2001 +0100
    12.2 +++ b/doc-src/TutorialI/Types/Typedef.thy	Fri Jan 26 15:50:28 2001 +0100
    12.3 @@ -96,8 +96,10 @@
    12.4  @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
    12.5  \end{tabular}
    12.6  \end{center}
    12.7 -Constant @{term three} is just an abbreviation (@{thm[source]three_def}):
    12.8 -@{thm[display]three_def}
    12.9 +Constant @{term three} is explicitly defined as the representing set:
   12.10 +\begin{center}
   12.11 +@{thm three_def}\hfill(@{thm[source]three_def})
   12.12 +\end{center}
   12.13  The situation is best summarized with the help of the following diagram,
   12.14  where squares are types and circles are sets:
   12.15  \begin{center}
   12.16 @@ -118,10 +120,10 @@
   12.17  surjective on the subset @{term three} and @{term Abs_three} and @{term
   12.18  Rep_three} are inverses of each other:
   12.19  \begin{center}
   12.20 -\begin{tabular}{rl}
   12.21 -@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\
   12.22 -@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\
   12.23 -@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse})
   12.24 +\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
   12.25 +@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
   12.26 +@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
   12.27 +@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
   12.28  \end{tabular}
   12.29  \end{center}
   12.30  %
    13.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex	Fri Jan 26 15:02:04 2001 +0100
    13.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex	Fri Jan 26 15:50:28 2001 +0100
    13.3 @@ -102,10 +102,10 @@
    13.4  \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
    13.5  \end{tabular}
    13.6  \end{center}
    13.7 -Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}):
    13.8 -\begin{isabelle}%
    13.9 -three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
   13.10 -\end{isabelle}
   13.11 +Constant \isa{three} is explicitly defined as the representing set:
   13.12 +\begin{center}
   13.13 +\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
   13.14 +\end{center}
   13.15  The situation is best summarized with the help of the following diagram,
   13.16  where squares are types and circles are sets:
   13.17  \begin{center}
   13.18 @@ -125,10 +125,10 @@
   13.19  Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
   13.20  surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
   13.21  \begin{center}
   13.22 -\begin{tabular}{rl}
   13.23 -\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} &~~ (\isa{Rep{\isacharunderscore}three}) \\
   13.24 -\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} &~~ (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
   13.25 -\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
   13.26 +\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
   13.27 +\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
   13.28 +\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
   13.29 +\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
   13.30  \end{tabular}
   13.31  \end{center}
   13.32  %
    14.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jan 26 15:02:04 2001 +0100
    14.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jan 26 15:50:28 2001 +0100
    14.3 @@ -270,7 +270,7 @@
    14.4  
    14.5  \begin{warn}
    14.6  The absolute value bars shown above cannot be typed on a keyboard.  They
    14.7 -can be entered using the X-symbol package.  In ASCII, type \isa{abs x} to
    14.8 +can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
    14.9  get \isa{\isasymbar x\isasymbar}.
   14.10  \end{warn}
   14.11  
    15.1 --- a/doc-src/TutorialI/appendix.tex	Fri Jan 26 15:02:04 2001 +0100
    15.2 +++ b/doc-src/TutorialI/appendix.tex	Fri Jan 26 15:50:28 2001 +0100
    15.3 @@ -98,9 +98,9 @@
    15.4  \hline
    15.5  \end{tabular}
    15.6  \end{center}
    15.7 -\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
    15.8 +\caption{Mathematical symbols, their \textsc{ascii}-equivalents and X-symbol codes}
    15.9  \label{tab:ascii}
   15.10 -\end{table}\indexbold{ASCII symbols}
   15.11 +\end{table}\indexbold{ASCII@\textsc{ascii} symbols}
   15.12  
   15.13  \input{Misc/document/appendix.tex}
   15.14  
    16.1 --- a/doc-src/TutorialI/basics.tex	Fri Jan 26 15:02:04 2001 +0100
    16.2 +++ b/doc-src/TutorialI/basics.tex	Fri Jan 26 15:50:28 2001 +0100
    16.3 @@ -8,12 +8,14 @@
    16.4  HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
    16.5  following the equation
    16.6  \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
    16.7 -We assume that the reader is familiar with the basic concepts of both fields.
    16.8 -For excellent introductions to functional programming consult the textbooks
    16.9 -by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
   16.10 -this tutorial initially concentrates on functional programming, do not be
   16.11 -misled: HOL can express most mathematical concepts, and functional
   16.12 -programming is just one particularly simple and ubiquitous instance.
   16.13 +We do not assume that the reader is familiar with mathematical logic but that
   16.14 +(s)he is used to logical and set theoretic notation.  In contrast, we do assume
   16.15 +that the reader is familiar with the basic concepts of functional programming.
   16.16 +For excellent introductions consult the textbooks by Bird and
   16.17 +Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although this
   16.18 +tutorial initially concentrates on functional programming, do not be
   16.19 +misled: HOL can express most mathematical concepts, and functional programming
   16.20 +is just one particularly simple and ubiquitous instance.
   16.21  
   16.22  Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
   16.23  This has influenced some of HOL's concrete syntax but is otherwise
   16.24 @@ -233,7 +235,7 @@
   16.25  \end{itemize}
   16.26  
   16.27  For the sake of readability the usual mathematical symbols are used throughout
   16.28 -the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
   16.29 +the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
   16.30  the appendix.
   16.31  
   16.32  
   16.33 @@ -278,7 +280,7 @@
   16.34    General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
   16.35  
   16.36  Some interfaces (including the shell level) offer special fonts with
   16.37 -mathematical symbols. For those that do not, remember that ASCII-equivalents
   16.38 +mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
   16.39  are shown in table~\ref{tab:ascii} in the appendix.
   16.40  
   16.41  Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
   16.42 @@ -295,7 +297,7 @@
   16.43    starts the default logic, which usually is already \texttt{HOL}.  This is
   16.44    controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
   16.45      System Manual} for more details.} This presents you with Isabelle's most
   16.46 -basic ASCII interface.  In addition you need to open an editor window to
   16.47 +basic \textsc{ascii} interface.  In addition you need to open an editor window to
   16.48  create theory files.  While you are developing a theory, we recommend to
   16.49  type each command into the file first and then enter it into Isabelle by
   16.50  copy-and-paste, thus ensuring that you have a complete record of your theory.
    17.1 --- a/doc-src/TutorialI/fp.tex	Fri Jan 26 15:02:04 2001 +0100
    17.2 +++ b/doc-src/TutorialI/fp.tex	Fri Jan 26 15:50:28 2001 +0100
    17.3 @@ -1,16 +1,18 @@
    17.4  \chapter{Functional Programming in HOL}
    17.5  
    17.6  Although on the surface this chapter is mainly concerned with how to write
    17.7 -functional programs in HOL and how to verify them, most of the
    17.8 -constructs and proof procedures introduced are general purpose and recur in
    17.9 -any specification or verification task.
   17.10 +functional programs in HOL and how to verify them, most of the constructs and
   17.11 +proof procedures introduced are general purpose and recur in any specification
   17.12 +or verification task. In fact, it we should really speak of functional
   17.13 +\emph{modelling} rather than \emph{programming} because our aim is not
   17.14 +primarily to write programs but to design abstract models of systems.  HOL is
   17.15 +a specification language that goes well beyond what can be expressed as a
   17.16 +program. However, for the time being we concentrate on the computable.
   17.17  
   17.18  The dedicated functional programmer should be warned: HOL offers only
   17.19 -\emph{total functional programming} --- all functions in HOL must be total;
   17.20 -lazy data structures are not directly available. On the positive side,
   17.21 -functions in HOL need not be computable: HOL is a specification language that
   17.22 -goes well beyond what can be expressed as a program. However, for the time
   17.23 -being we concentrate on the computable.
   17.24 +\emph{total functional programming} --- all functions in HOL must be total,
   17.25 +i.e.\ they must terminate for all inputs; lazy data structures are not
   17.26 +directly available.
   17.27  
   17.28  \section{An Introductory Theory}
   17.29  \label{sec:intro-theory}
    18.1 --- a/doc-src/TutorialI/todo.tobias	Fri Jan 26 15:02:04 2001 +0100
    18.2 +++ b/doc-src/TutorialI/todo.tobias	Fri Jan 26 15:50:28 2001 +0100
    18.3 @@ -35,15 +35,12 @@
    18.4  Minor fixes in the tutorial
    18.5  ===========================
    18.6  
    18.7 -adjust type of ^ in tab:overloading
    18.8 -
    18.9 -explanation of term "contrapositive"/contraposition in Rules?
   18.10 -Index the notion and maybe the rules contrapos_xy
   18.11 +Adjust FP textbook refs: new Bird, Hudak
   18.12 +Discrete math textbook: Rosen?
   18.13  
   18.14 -get rid of use_thy in tutorial?
   18.15 +say something about "abbreviations" when defs are introduced.
   18.16  
   18.17 -Orderings on numbers (with hint that it is overloaded):
   18.18 -bounded quantifers ALL x<y, <=.
   18.19 +adjust type of ^ in tab:overloading
   18.20  
   18.21  an example of induction: !y. A --> B --> C ??
   18.22  
   18.23 @@ -74,16 +71,6 @@
   18.24  
   18.25  unfold?
   18.26  
   18.27 -Tacticals: , ? +
   18.28 -Note: + is used in typedef section!
   18.29 -
   18.30 -A list of further useful commands (rules? tricks?)
   18.31 -prefer, defer, print_simpset (-> print_simps?)
   18.32 -
   18.33 -demonstrate x : set xs in Sets. Or Tricks chapter?
   18.34 -
   18.35 -Appendix with HOL and Isar keywords.
   18.36 -
   18.37  
   18.38  Possible exercises
   18.39  ==================