--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon May 02 11:03:27 2005 +0200
@@ -180,7 +180,7 @@
\S\ref{sec:InductionHeuristics}
\begin{exercise}
- We strengthen the definition of a @{term normal} If-expression as follows:
+ We strengthen the definition of a @{const normal} If-expression as follows:
the first argument of all @{term IF}s must be a variable. Adapt the above
development to this changed requirement. (Hint: you may need to formulate
some of the goals as implications (@{text"\<longrightarrow>"}) rather than
--- a/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 11:03:27 2005 +0200
@@ -119,7 +119,7 @@
those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just
-proved: the more complex notion (@{term itrev}) is on the left-hand
+proved: the more complex notion (@{const itrev}) is on the left-hand
side, the simpler one (@{term rev}) on the right-hand side. This constitutes
another, albeit weak heuristic that is not restricted to induction:
\begin{quote}
--- a/doc-src/TutorialI/Misc/Option2.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Mon May 02 11:03:27 2005 +0200
@@ -14,7 +14,7 @@
text{*\noindent
Frequently one needs to add a distinguished element to some existing type.
For example, type @{text"t option"} can model the result of a computation that
-may either terminate with an error (represented by @{term None}) or return
+may either terminate with an error (represented by @{const None}) or return
some value @{term v} (represented by @{term"Some v"}).
Similarly, @{typ nat} extended with $\infty$ can be modeled by type
@{typ"nat option"}. In both cases one could define a new datatype with
--- a/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 11:03:27 2005 +0200
@@ -21,7 +21,7 @@
subsubsection{*Rule Induction*}
-text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
+text{* Rule induction for set @{const even}, @{thm[source]even.induct}:
@{thm[display] even.induct[no_vars]}*}
(*<*)thm even.induct[no_vars](*>*)
--- a/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Mon May 02 11:03:27 2005 +0200
@@ -29,7 +29,7 @@
"sep1(a, xs) = xs";
text{*
-This is what the rules for @{term sep1} are turned into:
+This is what the rules for @{const sep1} are turned into:
@{thm[display,indent=5] sep1.simps[no_vars]}
*}
(*<*)
--- a/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 11:03:27 2005 +0200
@@ -26,11 +26,11 @@
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle
(while processing the declaration of @{text term}). Why does the
-recursive call of @{term trev} lead to this
+recursive call of @{const trev} lead to this
condition? Because \isacommand{recdef} knows that @{term map}
-will apply @{term trev} only to elements of @{term ts}. Thus the
+will apply @{const trev} only to elements of @{term ts}. Thus the
condition expresses that the size of the argument @{prop"t : set ts"} of any
-recursive call of @{term trev} is strictly less than @{term"size(App f ts)"},
+recursive call of @{const trev} is strictly less than @{term"size(App f ts)"},
which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} knows about @{term map}.
--- a/doc-src/TutorialI/Recdef/examples.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Mon May 02 11:03:27 2005 +0200
@@ -63,7 +63,7 @@
one does not match, Isabelle internally replaces the second equation
by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
@{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and
-@{term sep1} are identical.
+@{const sep1} are identical.
\begin{warn}
\isacommand{recdef} only takes the first argument of a (curried)
--- a/doc-src/TutorialI/Trie/Trie.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Mon May 02 11:03:27 2005 +0200
@@ -49,7 +49,7 @@
text{*
As a first simple property we prove that looking up a string in the empty
-trie @{term"Trie None []"} always returns @{term None}. The proof merely
+trie @{term"Trie None []"} always returns @{const None}. The proof merely
distinguishes the two cases whether the search string is empty or not:
*};
@@ -76,10 +76,10 @@
@{term tt} associated with the first letter @{term a} is extracted,
recursively updated, and then placed in front of the association list.
The old subtrie associated with @{term a} is still in the association list
-but no longer accessible via @{term assoc}. Clearly, there is room here for
+but no longer accessible via @{const assoc}. Clearly, there is room here for
optimizations!
-Before we start on any proofs about @{term update} we tell the simplifier to
+Before we start on any proofs about @{const update} we tell the simplifier to
expand all @{text let}s and to split all @{text case}-constructs over
options:
*};
@@ -88,11 +88,11 @@
text{*\noindent
The reason becomes clear when looking (probably after a failed proof
-attempt) at the body of @{term update}: it contains both
+attempt) at the body of @{const update}: it contains both
@{text let} and a case distinction over type @{text option}.
-Our main goal is to prove the correct interaction of @{term update} and
-@{term lookup}:
+Our main goal is to prove the correct interaction of @{const update} and
+@{const lookup}:
*};
theorem "\<forall>t v bs. lookup (update t as v) bs =
@@ -102,8 +102,8 @@
Our plan is to induct on @{term as}; hence the remaining variables are
quantified. From the definitions it is clear that induction on either
@{term as} or @{term bs} is required. The choice of @{term as} is
-guided by the intuition that simplification of @{term lookup} might be easier
-if @{term update} has already been simplified, which can only happen if
+guided by the intuition that simplification of @{const lookup} might be easier
+if @{const update} has already been simplified, which can only happen if
@{term as} is instantiated.
The start of the proof is conventional:
*};
@@ -138,7 +138,7 @@
sense and solves the proof.
\begin{exercise}
- Modify @{term update} (and its type) such that it allows both insertion and
+ Modify @{const update} (and its type) such that it allows both insertion and
deletion of entries with a single function. Prove the corresponding version
of the main theorem above.
Optimize your function such that it shrinks tries after
@@ -146,10 +146,10 @@
\end{exercise}
\begin{exercise}
- Write an improved version of @{term update} that does not suffer from the
+ Write an improved version of @{const update} that does not suffer from the
space leak (pointed out above) caused by not deleting overwritten entries
from the association list. Prove the main theorem for your improved
- @{term update}.
+ @{const update}.
\end{exercise}
\begin{exercise}
--- a/doc-src/TutorialI/Types/Pairs.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Types/Pairs.thy Mon May 02 11:03:27 2005 +0200
@@ -138,7 +138,7 @@
lemma "swap(swap p) = p"
txt{*\noindent
-simplification will do nothing, because the defining equation for @{term swap}
+simplification will do nothing, because the defining equation for @{const swap}
expects a pair. Again, we need to turn @{term p} into a pair first, but this
time there is no @{term split} in sight. In this case the only thing we can do
is to split the term by hand:
--- a/doc-src/TutorialI/Types/Records.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Types/Records.thy Mon May 02 11:03:27 2005 +0200
@@ -45,8 +45,8 @@
Ycoord :: int
text {*
- Records of type @{typ point} have two fields named @{text Xcoord}
- and @{text Ycoord}, both of type~@{typ int}. We now define a
+ Records of type @{typ point} have two fields named @{const Xcoord}
+ and @{const Ycoord}, both of type~@{typ int}. We now define a
constant of type @{typ point}:
*}
@@ -78,8 +78,8 @@
text {*
The \emph{update}\index{update!record} operation is functional. For
- example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord}
- value is zero and whose @{text Ycoord} value is copied from~@{text
+ example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{const Xcoord}
+ value is zero and whose @{const Ycoord} value is copied from~@{text
p}. Updates of explicit records are also simplified automatically:
*}
@@ -111,7 +111,7 @@
col :: colour
text {*
- The fields of this new type are @{text Xcoord}, @{text Ycoord} and
+ The fields of this new type are @{const Xcoord}, @{text Ycoord} and
@{text col}, in that order.
*}
@@ -137,7 +137,7 @@
text {*
This lemma applies to any record whose first two fields are @{text
- Xcoord} and~@{text Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord
+ Xcoord} and~@{const Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord
= b, \<dots> = ()\<rparr>"} is exactly the same as @{text "\<lparr>Xcoord = a, Ycoord
= b\<rparr>"}. Selectors and updates are always polymorphic wrt.\ the
@{text more} part of a record scheme, its value is just ignored (for
@@ -169,7 +169,7 @@
\medskip
Type @{typ point} is for fixed records having exactly the two fields
- @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
+ @{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
"'a point_scheme"} comprises all possible extensions to those two
fields. Note that @{typ "unit point_scheme"} coincides with @{typ
point}, and @{typ "\<lparr>col :: colour\<rparr> point_scheme"} with @{typ
@@ -188,7 +188,7 @@
text {*
Here is a generic method that modifies a point, incrementing its
- @{text Xcoord} field. The @{text Ycoord} and @{text more} fields
+ @{const Xcoord} field. The @{text Ycoord} and @{text more} fields
are copied across. It works for any record type scheme derived from
@{typ point} (including @{typ cpoint} etc.):
*}
@@ -200,7 +200,7 @@
text {*
Generic theorems can be proved about generic methods. This trivial
- lemma relates @{text incX} to @{text getX} and @{text setX}:
+ lemma relates @{const incX} to @{text getX} and @{text setX}:
*}
lemma "incX r = setX r (getX r + 1)"
@@ -272,7 +272,7 @@
text {*
Here the simplifier can do nothing, since general record equality is
not eliminated automatically. One way to proceed is by an explicit
- forward step that applies the selector @{text Xcoord} to both sides
+ forward step that applies the selector @{const Xcoord} to both sides
of the assumed record equality:
*}
@@ -376,7 +376,7 @@
"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
text {*
- The coloured points @{text cpt1} and @{text cpt2} are equal. The
+ The coloured points @{const cpt1} and @{text cpt2} are equal. The
proof is trivial, by unfolding all the definitions. We deliberately
omit the definition of~@{text pt1} in order to reveal the underlying
comparison on type @{typ point}.