doc-src/TutorialI/Datatype/ABexpr.thy
changeset 10971 6852682eaf16
parent 10171 59d6633835fa
child 11309 d666f11ca2d4
     1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -28,13 +28,13 @@
     1.4  text{*\noindent
     1.5  Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
     1.6  except that we have fixed the values to be of type @{typ"nat"} and that we
     1.7 -have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean
     1.8 +have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
     1.9  expressions can be arithmetic comparisons, conjunctions and negations.
    1.10  The semantics is fixed via two evaluation functions
    1.11  *}
    1.12  
    1.13 -consts  evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
    1.14 -        evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
    1.15 +consts  evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
    1.16 +        evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
    1.17  
    1.18  text{*\noindent
    1.19  that take an expression and an environment (a mapping from variables @{typ"'a"} to values
    1.20 @@ -53,15 +53,15 @@
    1.21    "evala (Num n) env = n"
    1.22  
    1.23    "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
    1.24 -  "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
    1.25 -  "evalb (Neg b) env = (\\<not> evalb b env)"
    1.26 +  "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
    1.27 +  "evalb (Neg b) env = (\<not> evalb b env)"
    1.28  
    1.29  text{*\noindent
    1.30  In the same fashion we also define two functions that perform substitution:
    1.31  *}
    1.32  
    1.33 -consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
    1.34 -       substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
    1.35 +consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
    1.36 +       substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
    1.37  
    1.38  text{*\noindent
    1.39  The first argument is a function mapping variables to expressions, the
    1.40 @@ -93,8 +93,8 @@
    1.41  theorems simultaneously:
    1.42  *}
    1.43  
    1.44 -lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
    1.45 -        evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
    1.46 +lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
    1.47 +        evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
    1.48  apply(induct_tac a and b);
    1.49  
    1.50  txt{*\noindent
    1.51 @@ -110,7 +110,7 @@
    1.52  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    1.53  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    1.54  \begin{isabelle}
    1.55 -\isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"}
    1.56 +\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
    1.57  \end{isabelle}
    1.58  
    1.59  \begin{exercise}