--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Sep 01 19:09:44 2000 +0200
@@ -16,16 +16,16 @@
text{*\noindent
The two constants are represented by @{term"Const True"} and
@{term"Const False"}. Variables are represented by terms of the form
-@{term"Var n"}, where @{term"n"} is a natural number (type \isa{nat}).
+@{term"Var n"}, where @{term"n"} is a natural number (type @{typ"nat"}).
For example, the formula $P@0 \land \neg P@1$ is represented by the term
@{term"And (Var 0) (Neg(Var 1))"}.
\subsubsection{What is the value of a boolean expression?}
The value of a boolean expression depends on the value of its variables.
-Hence the function \isa{value} takes an additional parameter, an {\em
- environment} of type @{typ"nat => bool"}, which maps variables to
-their values:
+Hence the function @{text"value"} takes an additional parameter, an
+\emph{environment} of type @{typ"nat => bool"}, which maps variables to their
+values:
*}
consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
@@ -40,14 +40,14 @@
An alternative and often more efficient (because in a certain sense
canonical) representation are so-called \emph{If-expressions} built up
-from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
-(\isa{IF}):
+from constants (@{term"CIF"}), variables (@{term"VIF"}) and conditionals
+(@{term"IF"}):
*}
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
text{*\noindent
-The evaluation if If-expressions proceeds as for \isa{boolex}:
+The evaluation if If-expressions proceeds as for @{typ"boolex"}:
*}
consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
@@ -60,9 +60,9 @@
text{*
\subsubsection{Transformation into and of If-expressions}
-The type \isa{boolex} is close to the customary representation of logical
-formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
-translate from \isa{boolex} into \isa{ifex}:
+The type @{typ"boolex"} is close to the customary representation of logical
+formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
+translate from @{typ"boolex"} into @{typ"ifex"}:
*}
consts bool2if :: "boolex \\<Rightarrow> ifex";
@@ -73,7 +73,7 @@
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
text{*\noindent
-At last, we have something we can verify: that \isa{bool2if} preserves the
+At last, we have something we can verify: that @{term"bool2if"} preserves the
value of its argument:
*}
@@ -91,7 +91,7 @@
not show them below.
More interesting is the transformation of If-expressions into a normal form
-where the first argument of \isa{IF} cannot be another \isa{IF} but
+where the first argument of @{term"IF"} cannot be another @{term"IF"} but
must be a constant or variable. Such a normal form can be computed by
repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by
@{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following
@@ -120,7 +120,7 @@
text{*\noindent
The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what \isa{normif} does):
+lemma (which also helps to understand what @{term"normif"} does):
*}
lemma [simp]:
@@ -135,9 +135,9 @@
(*>*)
text{*\noindent
Note that the lemma does not have a name, but is implicitly used in the proof
-of the theorem shown above because of the \isa{[simp]} attribute.
+of the theorem shown above because of the @{text"[simp]"} attribute.
-But how can we be sure that \isa{norm} really produces a normal form in
+But how can we be sure that @{term"norm"} really produces a normal form in
the above sense? We define a function that tests If-expressions for normality
*}
@@ -149,8 +149,8 @@
(case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
text{*\noindent
-and prove \isa{normal(norm b)}. Of course, this requires a lemma about
-normality of \isa{normif}:
+and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
+normality of @{term"normif"}:
*}
lemma[simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";