--- a/doc-src/TutorialI/CTL/Base.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy Fri Jan 26 15:50:28 2001 +0100
@@ -60,7 +60,7 @@
text{*\noindent
Command \isacommand{typedecl} merely declares a new type but without
-defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because @{typ state} really is an implicit parameter of our model. Of
course it would have been more generic to make @{typ state} a type
--- a/doc-src/TutorialI/CTL/CTL.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Fri Jan 26 15:50:28 2001 +0100
@@ -17,8 +17,9 @@
| AF formula;
text{*\noindent
-which stands for "always in the future":
-on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+which stands for ``\emph{A}lways in the \emph{F}uture'':
+on all infinite paths, at some point the formula holds.
+Formalizing the notion of an infinite path is easy
in HOL: it is simply a function from @{typ nat} to @{typ state}.
*};
@@ -67,7 +68,7 @@
text{*\noindent
Because @{term af} is monotone in its second argument (and also its first, but
-that is irrelevant) @{term"af A"} has a least fixed point:
+that is irrelevant), @{term"af A"} has a least fixed point:
*};
lemma mono_af: "mono(af A)";
@@ -150,8 +151,8 @@
infinite @{term A}-avoiding path starting from @{term s}. The reason is
that by unfolding @{term lfp} we find that if @{term s} is not in
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
-direct successor of @{term s} that is again not in @{term"lfp(af
-A)"}. Iterating this argument yields the promised infinite
+direct successor of @{term s} that is again not in \mbox{@{term"lfp(af
+A)"}}. Iterating this argument yields the promised infinite
@{term A}-avoiding path. Let us formalize this sketch.
The one-step argument in the sketch above
@@ -159,7 +160,7 @@
*};
lemma not_in_lfp_afD:
- "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
+ "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
apply(erule contrapos_np);
apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
apply(simp add:af_def);
@@ -196,8 +197,8 @@
\<exists>p\<in>Paths s. \<forall>i. Q(p i)";
txt{*\noindent
-First we rephrase the conclusion slightly because we need to prove both the path property
-and the fact that @{term Q} holds simultaneously:
+First we rephrase the conclusion slightly because we need to prove simultaneously
+both the path property and the fact that @{term Q} holds:
*};
apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))");
@@ -216,7 +217,7 @@
apply(clarsimp);
txt{*\noindent
-After simplification and clarification the subgoal has the following compact form
+After simplification and clarification, the subgoal has the following form
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
and invites a proof by induction on @{term i}:
*};
@@ -225,7 +226,7 @@
apply(simp);
txt{*\noindent
-After simplification the base case boils down to
+After simplification, the base case boils down to
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
holds. However, we first have to show that such a @{term t} actually exists! This reasoning
@@ -345,8 +346,8 @@
text{*
The language defined above is not quite CTL\@. The latter also includes an
-until-operator @{term"EU f g"} with semantics ``there exists a path
-where @{term f} is true until @{term g} becomes true''. With the help
+until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path
+where @{term f} is true \emph{U}ntil @{term g} becomes true''. With the help
of an auxiliary function
*}
@@ -360,7 +361,7 @@
text{*\noindent
the semantics of @{term EU} is straightforward:
-@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
+@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}
Note that @{term EU} is not definable in terms of the other operators!
Model checking @{term EU} is again a least fixed point construction:
@@ -457,10 +458,10 @@
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only @{term lfp} requires a little thought.
Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator_Example}.}
+\footnote{See theory \isa{While_Combinator}.}
provides a theorem stating that
in the case of finite sets and a monotone function~@{term F},
-the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} until
+the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.
*}
--- a/doc-src/TutorialI/CTL/PDL.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy Fri Jan 26 15:50:28 2001 +0100
@@ -42,8 +42,8 @@
text{*\noindent
The first three equations should be self-explanatory. The temporal formula
-@{term"AX f"} means that @{term f} is true in all next states whereas
-@{term"EF f"} means that there exists some future state in which @{term f} is
+@{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas
+@{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is
true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
@@ -68,7 +68,7 @@
fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
@{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
find it hard to see that @{term"mc(EF f)"} contains exactly those states from
-which there is a path to a state where @{term f} is true, do not worry --- that
+which there is a path to a state where @{term f} is true, do not worry --- this
will be proved in a moment.
First we prove monotonicity of the function inside @{term lfp}
@@ -180,7 +180,7 @@
text{*
\begin{exercise}
@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
-as that is the ASCII equivalent of @{text"\<exists>"}}
+as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
(``there exists a next state such that'') with the intended semantics
@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
--- a/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:50:28 2001 +0100
@@ -63,7 +63,7 @@
\begin{isamarkuptext}%
\noindent
Command \isacommand{typedecl} merely declares a new type but without
-defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because \isa{state} really is an implicit parameter of our model. Of
course it would have been more generic to make \isa{state} a type
--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 26 15:50:28 2001 +0100
@@ -15,8 +15,9 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
\begin{isamarkuptext}%
\noindent
-which stands for "always in the future":
-on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+which stands for ``\emph{A}lways in the \emph{F}uture'':
+on all infinite paths, at some point the formula holds.
+Formalizing the notion of an infinite path is easy
in HOL: it is simply a function from \isa{nat} to \isa{state}.%
\end{isamarkuptext}%
\isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
@@ -45,7 +46,7 @@
\begin{isamarkuptext}%
\noindent
Because \isa{af} is monotone in its second argument (and also its first, but
-that is irrelevant) \isa{af\ A} has a least fixed point:%
+that is irrelevant), \isa{af\ A} has a least fixed point:%
\end{isamarkuptext}%
\isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -111,14 +112,14 @@
infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
that by unfolding \isa{lfp} we find that if \isa{s} is not in
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
-direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
+direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
\isa{A}-avoiding path. Let us formalize this sketch.
The one-step argument in the sketch above
is proved by a variant of contraposition:%
\end{isamarkuptext}%
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
-\ {\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
+\ {\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
\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -153,8 +154,8 @@
\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-First we rephrase the conclusion slightly because we need to prove both the path property
-and the fact that \isa{Q} holds simultaneously:%
+First we rephrase the conclusion slightly because we need to prove simultaneously
+both the path property and the fact that \isa{Q} holds:%
\end{isamarkuptxt}%
\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}%
\begin{isamarkuptxt}%
@@ -170,7 +171,7 @@
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-After simplification and clarification the subgoal has the following compact form
+After simplification and clarification, the subgoal has the following form
\begin{isabelle}%
\ {\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
\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
@@ -182,7 +183,7 @@
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-After simplification the base case boils down to
+After simplification, the base case boils down to
\begin{isabelle}%
\ {\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
\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
@@ -281,8 +282,8 @@
\isacommand{done}%
\begin{isamarkuptext}%
The language defined above is not quite CTL\@. The latter also includes an
-until-operator \isa{EU\ f\ g} with semantics ``there exists a path
-where \isa{f} is true until \isa{g} becomes true''. With the help
+until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
+where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help
of an auxiliary function%
\end{isamarkuptext}%
\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
@@ -293,7 +294,7 @@
\noindent
the semantics of \isa{EU} is straightforward:
\begin{isabelle}%
-\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}%
+\ \ \ \ \ 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}%
\end{isabelle}
Note that \isa{EU} is not definable in terms of the other operators!
@@ -320,10 +321,10 @@
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only \isa{lfp} requires a little thought.
Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator_Example}.}
+\footnote{See theory \isa{While_Combinator}.}
provides a theorem stating that
in the case of finite sets and a monotone function~\isa{F},
-the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
+the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 26 15:50:28 2001 +0100
@@ -43,8 +43,8 @@
\begin{isamarkuptext}%
\noindent
The first three equations should be self-explanatory. The temporal formula
-\isa{AX\ f} means that \isa{f} is true in all next states whereas
-\isa{EF\ f} means that there exists some future state in which \isa{f} is
+\isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas
+\isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is
true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
@@ -68,7 +68,7 @@
fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
-which there is a path to a state where \isa{f} is true, do not worry --- that
+which there is a path to a state where \isa{f} is true, do not worry --- this
will be proved in a moment.
First we prove monotonicity of the function inside \isa{lfp}
@@ -177,7 +177,7 @@
\begin{isamarkuptext}%
\begin{exercise}
\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
-as that is the ASCII equivalent of \isa{{\isasymexists}}}
+as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}}
(``there exists a next state such that'') with the intended semantics
\begin{isabelle}%
\ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:50:28 2001 +0100
@@ -166,7 +166,7 @@
Of course we can also unfold definitions in the middle of a proof.
You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
+rule because this defeats the whole purpose.
\begin{warn}
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
--- a/doc-src/TutorialI/Misc/simp.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Jan 26 15:50:28 2001 +0100
@@ -162,7 +162,7 @@
Of course we can also unfold definitions in the middle of a proof.
You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
+rule because this defeats the whole purpose.
\begin{warn}
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
--- a/doc-src/TutorialI/Rules/rules.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Fri Jan 26 15:50:28 2001 +0100
@@ -966,7 +966,7 @@
\subsection{Definite Descriptions}
-In ASCII, we write \isa{SOME} for $\varepsilon$.
+In \textsc{ascii}, we write \isa{SOME} for $\varepsilon$.
\REMARK{the internal constant is \isa{Eps}}
The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
description}: when \isa{P} is satisfied by a unique value,~\isa{a}.
--- a/doc-src/TutorialI/Sets/Functions.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/Functions.thy Fri Jan 26 15:50:28 2001 +0100
@@ -79,7 +79,7 @@
*}
lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
- apply (simp add: expand_fun_eq inj_on_def o_def)
+ apply (simp add: expand_fun_eq inj_on_def)
apply (auto)
done
--- a/doc-src/TutorialI/Sets/sets.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Fri Jan 26 15:50:28 2001 +0100
@@ -96,7 +96,7 @@
\isacommand{by}\ blast
\end{isabelle}
%
-This is the same example using ASCII syntax, illustrating a pitfall:
+This is the same example using \textsc{ascii} syntax, illustrating a pitfall:
\begin{isabelle}
\isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)"
\end{isabelle}
@@ -287,8 +287,8 @@
\end{isabelle}
Unions can be formed over the values of a given set. The syntax is
-\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN
-x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
+\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
+x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
\begin{isabelle}
(b\ \isasymin\
(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
@@ -320,12 +320,12 @@
over a \emph{type}:
\begin{isabelle}
\ \ \ \ \
-({\isasymUnion}x.\ B\ x)\ {==}\
+({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
\end{isabelle}
Abbreviations work as you might expect. The term on the left-hand side of
the
-\isa{==} symbol is automatically translated to the right-hand side when the
+\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
term is parsed, the reverse translation being done when the term is
displayed.
@@ -523,7 +523,7 @@
Theorems involving these concepts can be hard to prove. The following
example is easy, but it cannot be proved automatically. To begin
-with, we need a law that relates the quality of functions to
+with, we need a law that relates the equality of functions to
equality over all arguments:
\begin{isabelle}
(f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
@@ -535,7 +535,7 @@
side of function composition:
\begin{isabelle}
\isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
-\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline
+\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline
\isacommand{apply}\ auto\isanewline
\isacommand{done}
\end{isabelle}
@@ -593,7 +593,7 @@
abbreviates an application of image to {\isa{UNIV}}:
\begin{isabelle}
\ \ \ \ \ range\ f\
-{==}\ f`UNIV
+{\isasymrightleftharpoons}\ f`UNIV
\end{isabelle}
%
Few theorems are proved specifically
@@ -845,7 +845,7 @@
Induction comes in many forms, including traditional mathematical
induction, structural induction on lists and induction on size.
More general than these is induction over a well-founded relation.
-Such A relation expresses the notion of a terminating process.
+Such a relation expresses the notion of a terminating process.
Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
infinite descending chains
\[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
@@ -944,9 +944,9 @@
\section{Fixed Point Operators}
-Fixed point operators define sets recursively. Most users invoke
-them by making an inductive definition, as discussed in
-Chap.\ts\ref{chap:inductive} below. However, they can be used directly.
+Fixed point operators define sets recursively. They are invoked
+implicitly when making an inductive definition, as discussed in
+Chap.\ts\ref{chap:inductive} below. However, they can be used directly, too.
The
\relax{least} or \relax{strongest} fixed point yields an inductive
definition; the \relax{greatest} or \relax{weakest} fixed point yields a
@@ -954,7 +954,7 @@
existence of these fixed points is guaranteed by the Knaster-Tarski
theorem.
-The theory works applies only to monotonic functions. Isabelle's
+The theory applies only to monotonic functions. Isabelle's
definition of monotone is overloaded over all orderings:
\begin{isabelle}
mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
--- a/doc-src/TutorialI/Types/Typedef.thy Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy Fri Jan 26 15:50:28 2001 +0100
@@ -96,8 +96,10 @@
@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
\end{tabular}
\end{center}
-Constant @{term three} is just an abbreviation (@{thm[source]three_def}):
-@{thm[display]three_def}
+Constant @{term three} is explicitly defined as the representing set:
+\begin{center}
+@{thm three_def}\hfill(@{thm[source]three_def})
+\end{center}
The situation is best summarized with the help of the following diagram,
where squares are types and circles are sets:
\begin{center}
@@ -118,10 +120,10 @@
surjective on the subset @{term three} and @{term Abs_three} and @{term
Rep_three} are inverses of each other:
\begin{center}
-\begin{tabular}{rl}
-@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\
-@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\
-@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse})
+\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
+@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
+@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
\end{tabular}
\end{center}
%
--- a/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 26 15:50:28 2001 +0100
@@ -102,10 +102,10 @@
\isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
\end{tabular}
\end{center}
-Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}):
-\begin{isabelle}%
-three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
-\end{isabelle}
+Constant \isa{three} is explicitly defined as the representing set:
+\begin{center}
+\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
+\end{center}
The situation is best summarized with the help of the following diagram,
where squares are types and circles are sets:
\begin{center}
@@ -125,10 +125,10 @@
Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
\begin{center}
-\begin{tabular}{rl}
-\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} &~~ (\isa{Rep{\isacharunderscore}three}) \\
-\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} &~~ (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
-\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
+\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
+\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
+\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
\end{tabular}
\end{center}
%
--- a/doc-src/TutorialI/Types/numerics.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Fri Jan 26 15:50:28 2001 +0100
@@ -270,7 +270,7 @@
\begin{warn}
The absolute value bars shown above cannot be typed on a keyboard. They
-can be entered using the X-symbol package. In ASCII, type \isa{abs x} to
+can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
get \isa{\isasymbar x\isasymbar}.
\end{warn}
--- a/doc-src/TutorialI/appendix.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex Fri Jan 26 15:50:28 2001 +0100
@@ -98,9 +98,9 @@
\hline
\end{tabular}
\end{center}
-\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
+\caption{Mathematical symbols, their \textsc{ascii}-equivalents and X-symbol codes}
\label{tab:ascii}
-\end{table}\indexbold{ASCII symbols}
+\end{table}\indexbold{ASCII@\textsc{ascii} symbols}
\input{Misc/document/appendix.tex}
--- a/doc-src/TutorialI/basics.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Fri Jan 26 15:50:28 2001 +0100
@@ -8,12 +8,14 @@
HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
following the equation
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We assume that the reader is familiar with the basic concepts of both fields.
-For excellent introductions to functional programming consult the textbooks
-by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although
-this tutorial initially concentrates on functional programming, do not be
-misled: HOL can express most mathematical concepts, and functional
-programming is just one particularly simple and ubiquitous instance.
+We do not assume that the reader is familiar with mathematical logic but that
+(s)he is used to logical and set theoretic notation. In contrast, we do assume
+that the reader is familiar with the basic concepts of functional programming.
+For excellent introductions consult the textbooks by Bird and
+Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this
+tutorial initially concentrates on functional programming, do not be
+misled: HOL can express most mathematical concepts, and functional programming
+is just one particularly simple and ubiquitous instance.
Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
This has influenced some of HOL's concrete syntax but is otherwise
@@ -233,7 +235,7 @@
\end{itemize}
For the sake of readability the usual mathematical symbols are used throughout
-the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
+the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
the appendix.
@@ -278,7 +280,7 @@
General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
Some interfaces (including the shell level) offer special fonts with
-mathematical symbols. For those that do not, remember that ASCII-equivalents
+mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
are shown in table~\ref{tab:ascii} in the appendix.
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
@@ -295,7 +297,7 @@
starts the default logic, which usually is already \texttt{HOL}. This is
controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
System Manual} for more details.} This presents you with Isabelle's most
-basic ASCII interface. In addition you need to open an editor window to
+basic \textsc{ascii} interface. In addition you need to open an editor window to
create theory files. While you are developing a theory, we recommend to
type each command into the file first and then enter it into Isabelle by
copy-and-paste, thus ensuring that you have a complete record of your theory.
--- a/doc-src/TutorialI/fp.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Jan 26 15:50:28 2001 +0100
@@ -1,16 +1,18 @@
\chapter{Functional Programming in HOL}
Although on the surface this chapter is mainly concerned with how to write
-functional programs in HOL and how to verify them, most of the
-constructs and proof procedures introduced are general purpose and recur in
-any specification or verification task.
+functional programs in HOL and how to verify them, most of the constructs and
+proof procedures introduced are general purpose and recur in any specification
+or verification task. In fact, it we should really speak of functional
+\emph{modelling} rather than \emph{programming} because our aim is not
+primarily to write programs but to design abstract models of systems. HOL is
+a specification language that goes well beyond what can be expressed as a
+program. However, for the time being we concentrate on the computable.
The dedicated functional programmer should be warned: HOL offers only
-\emph{total functional programming} --- all functions in HOL must be total;
-lazy data structures are not directly available. On the positive side,
-functions in HOL need not be computable: HOL is a specification language that
-goes well beyond what can be expressed as a program. However, for the time
-being we concentrate on the computable.
+\emph{total functional programming} --- all functions in HOL must be total,
+i.e.\ they must terminate for all inputs; lazy data structures are not
+directly available.
\section{An Introductory Theory}
\label{sec:intro-theory}
--- a/doc-src/TutorialI/todo.tobias Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Fri Jan 26 15:50:28 2001 +0100
@@ -35,15 +35,12 @@
Minor fixes in the tutorial
===========================
-adjust type of ^ in tab:overloading
-
-explanation of term "contrapositive"/contraposition in Rules?
-Index the notion and maybe the rules contrapos_xy
+Adjust FP textbook refs: new Bird, Hudak
+Discrete math textbook: Rosen?
-get rid of use_thy in tutorial?
+say something about "abbreviations" when defs are introduced.
-Orderings on numbers (with hint that it is overloaded):
-bounded quantifers ALL x<y, <=.
+adjust type of ^ in tab:overloading
an example of induction: !y. A --> B --> C ??
@@ -74,16 +71,6 @@
unfold?
-Tacticals: , ? +
-Note: + is used in typedef section!
-
-A list of further useful commands (rules? tricks?)
-prefer, defer, print_simpset (-> print_simps?)
-
-demonstrate x : set xs in Sets. Or Tricks chapter?
-
-Appendix with HOL and Isar keywords.
-
Possible exercises
==================