--- a/doc-src/TutorialI/Advanced/Partial.thy Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Mon May 02 10:56:13 2005 +0200
@@ -49,7 +49,7 @@
\index{recursion!guarded}%
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
prefix an equation with a condition in the way ordinary definitions do
-(see @{term minus} above). Instead we have to move the condition over
+(see @{const minus} above). Instead we have to move the condition over
to the right-hand side of the equation. Given a partial function $f$
that should satisfy the recursion equation $f(x) = t$ over its domain
$dom(f)$, we turn this into the \isacommand{recdef}
@@ -117,7 +117,7 @@
well-foundedness of the relation given to \isacommand{recdef} is immediate.
Furthermore, each recursive call descends along that relation: the first
argument stays unchanged and the second one descends along @{term"step1
-f"}. The proof requires unfolding the definition of @{term step1},
+f"}. The proof requires unfolding the definition of @{const step1},
as specified in the \isacommand{hints} above.
Normally you will then derive the following conditional variant from
@@ -157,7 +157,7 @@
x := s; while b(x) do x := c(x); return x
\end{verbatim}
In general, @{term s} will be a tuple or record. As an example
-consider the following definition of function @{term find}:
+consider the following definition of function @{const find}:
*}
constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -181,7 +181,7 @@
(premise~3). And each loop iteration must descend along a well-founded
relation @{term r} (premises 4 and~5).
-Let us now prove that @{term find2} does indeed find a fixed point. Instead
+Let us now prove that @{const find2} does indeed find a fixed point. Instead
of induction we apply the above while rule, suitably instantiated.
Only the final premise of @{thm[source]while_rule} is left unproved
by @{text auto} but falls to @{text simp}:
--- a/doc-src/TutorialI/Advanced/simp.thy Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Mon May 02 10:56:13 2005 +0200
@@ -140,7 +140,7 @@
The simplifier will still try to apply the rule provided it
matches directly: without much $\lambda$-calculus hocus
pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
-@{term"g a \<in> range g"} to @{term True}, but will fail to match
+@{term"g a \<in> range g"} to @{const True}, but will fail to match
@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
eliminate the offending subterms --- those that are not patterns ---
by adding new variables and conditions.
--- a/doc-src/TutorialI/CTL/CTL.thy Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Mon May 02 10:56:13 2005 +0200
@@ -28,7 +28,7 @@
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
text{*\noindent
-This definition allows a succinct statement of the semantics of @{term AF}:
+This definition allows a succinct statement of the semantics of @{const AF}:
\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
@@ -47,7 +47,7 @@
"s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
text{*\noindent
-Model checking @{term AF} involves a function which
+Model checking @{const AF} involves a function which
is just complicated enough to warrant a separate definition:
*};
@@ -69,7 +69,7 @@
"mc(AF f) = lfp(af(mc f))";
text{*\noindent
-Because @{term af} is monotone in its second argument (and also its first, but
+Because @{const af} is monotone in its second argument (and also its first, but
that is irrelevant), @{term"af A"} has a least fixed point:
*};
@@ -101,7 +101,7 @@
(*>*)
text{*
All we need to prove now is @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
-that @{term mc} and @{text"\<Turnstile>"} agree for @{term AF}\@.
+that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
This time we prove the two inclusions separately, starting
with the easy one:
*};
@@ -110,7 +110,7 @@
"lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}";
txt{*\noindent
-In contrast to the analogous proof for @{term EF}, and just
+In contrast to the analogous proof for @{const EF}, and just
for a change, we do not use fixed point induction. Park-induction,
named after David Park, is weaker but sufficient for this proof:
\begin{center}
@@ -139,7 +139,7 @@
The opposite inclusion is proved by contradiction: if some state
@{term s} is not in @{term"lfp(af A)"}, then we can construct an
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
+that by unfolding @{const 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 \mbox{@{term"lfp(af
A)"}}. Iterating this argument yields the promised infinite
@@ -158,8 +158,8 @@
text{*\noindent
We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
-Unfolding @{term lfp} once and
-simplifying with the definition of @{term af} finishes the proof.
+Unfolding @{const lfp} once and
+simplifying with the definition of @{const af} finishes the proof.
Now we iterate this process. The following construction of the desired
path is parameterized by a predicate @{term Q} that should hold along the path:
@@ -175,7 +175,7 @@
@{term t} of element @{term n} such that @{term"Q t"} holds. Remember that @{text"SOME t. R t"}
is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
course, such a @{term t} need not exist, but that is of no
-concern to us since we will only use @{term path} when a
+concern to us since we will only use @{const path} when a
suitable @{term t} does exist.
Let us show that if each state @{term s} that satisfies @{term Q}
@@ -244,7 +244,7 @@
automatically. This is what happens in the step case.
The induction step is similar, but more involved, because now we face nested
-occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
+occurrences of @{const SOME}. As a result, @{text fast} is no longer able to
solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely
show the proof commands but do not describe the details:
*};
@@ -258,7 +258,7 @@
done;
text{*
-Function @{term path} has fulfilled its purpose now and can be forgotten.
+Function @{const path} has fulfilled its purpose now and can be forgotten.
It was merely defined to provide the witness in the proof of the
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
that we could have given the witness without having to define a new function:
@@ -446,7 +446,7 @@
text{* Let us close this section with a few words about the executability of
our model checkers. 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, theory
+implemented. Only @{const lfp} requires a little thought. Fortunately, theory
@{text While_Combinator} in the Library~\cite{HOL-Library} provides a
theorem stating that in the case of finite sets and a monotone
function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
--- a/doc-src/TutorialI/CTL/CTLind.thy Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy Mon May 02 10:56:13 2005 +0200
@@ -32,7 +32,7 @@
text{*
It is easy to see that for any infinite @{term A}-avoiding path @{term f}
with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
-starting with @{term s} because (by definition of @{term Avoid}) there is a
+starting with @{term s} because (by definition of @{const Avoid}) there is a
finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}.
The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,
this requires the following
@@ -98,7 +98,7 @@
subgoal once, we have to prove that @{term t} is in @{term A} or all successors
of @{term t} are in @{term"lfp (af A)"}. But if @{term t} is not in @{term A},
the second
-@{term Avoid}-rule implies that all successors of @{term t} are in
+@{const Avoid}-rule implies that all successors of @{term t} are in
@{term"Avoid s A"}, because we also assume @{prop"t \<in> Avoid s A"}.
Hence, by the induction hypothesis, all successors of @{term t} are indeed in
@{term"lfp(af A)"}. Mechanically:
@@ -136,7 +136,7 @@
@{thm[display]Avoid_in_lfp[no_vars]}
The main theorem is simply the corollary where @{prop"t = s"},
when the assumption @{prop"t \<in> Avoid s A"} is trivially true
-by the first @{term Avoid}-rule. Isabelle confirms this:%
+by the first @{const Avoid}-rule. Isabelle confirms this:%
\index{CTL|)}*}
theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
--- a/doc-src/TutorialI/CTL/document/CTL.tex Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon May 02 10:56:13 2005 +0200
@@ -69,6 +69,11 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
@@ -84,9 +89,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
+\isanewline
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -208,6 +211,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -289,6 +293,12 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
@@ -301,10 +311,8 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
+\isanewline
+\isanewline
\isamarkupfalse%
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Mon May 02 10:56:13 2005 +0200
@@ -112,7 +112,6 @@
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isanewline
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon May 02 10:56:13 2005 +0200
@@ -158,14 +158,17 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
--- a/doc-src/TutorialI/Datatype/Nested.thy Mon May 02 08:17:16 2005 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Mon May 02 10:56:13 2005 +0200
@@ -94,7 +94,7 @@
\end{exercise}
The experienced functional programmer may feel that our definition of
-@{term subst} is too complicated in that @{term substs} is
+@{term subst} is too complicated in that @{const substs} is
unnecessary. The @{term App}-case can be defined directly as
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
where @{term"map"} is the standard list function such that
@@ -143,7 +143,7 @@
declare subst_App [simp del]
text{*\noindent
-The advantage is that now we have replaced @{term substs} by
+The advantage is that now we have replaced @{const substs} by
@{term map}, we can profit from the large number of pre-proved lemmas
about @{term map}. Unfortunately inductive proofs about type
@{text term} are still awkward because they expect a conjunction. One