doc-src/TutorialI/Ifexpr/Ifexpr.thy

                 | And boolex boolex;
 
 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";
 primrec
 "value (Const b) env = b"

 text{*\noindent
 \subsubsection{If-expressions}
 
 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";
 primrec
 "valif (CIF b)    env = b"

                                         else valif e env)";
 
 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";
 primrec
 "bool2if (Const b) = CIF b"
 "bool2if (Var x)   = VIF x"
 "bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)"
 "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:
 *}
 
 lemma "valif (bool2if b) env = value b env";
 

 text{*\noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
 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
 primitive recursive functions perform this task:
 *}

 
 theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
 
 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]:
   "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
 (*<*)

 apply(induct_tac b);
 by(auto);
 (*>*)
 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
 *}
 
 consts normal :: "ifex \\<Rightarrow> bool";
 primrec

 "normal(VIF x) = True"
 "normal(IF b t e) = (normal t \\<and> normal e \\<and>
      (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)";
 (*<*)
 apply(induct_tac b);