doc-src/TutorialI/Datatype/ABexpr.thy
author nipkow
Wed Jan 24 12:29:10 2001 +0100 (2001-01-24)
changeset 10971 6852682eaf16
parent 10171 59d6633835fa
child 11309 d666f11ca2d4
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)
     2 theory ABexpr = Main:;
     3 (*>*)
     4 
     5 text{*
     6 Sometimes it is necessary to define two datatypes that depend on each
     7 other. This is called \textbf{mutual recursion}. As an example consider a
     8 language of arithmetic and boolean expressions where
     9 \begin{itemize}
    10 \item arithmetic expressions contain boolean expressions because there are
    11   conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
    12   and
    13 \item boolean expressions contain arithmetic expressions because of
    14   comparisons like ``$m<n$''.
    15 \end{itemize}
    16 In Isabelle this becomes
    17 *}
    18 
    19 datatype 'a aexp = IF   "'a bexp" "'a aexp" "'a aexp"
    20                  | Sum  "'a aexp" "'a aexp"
    21                  | Diff "'a aexp" "'a aexp"
    22                  | Var 'a
    23                  | Num nat
    24 and      'a bexp = Less "'a aexp" "'a aexp"
    25                  | And  "'a bexp" "'a bexp"
    26                  | Neg  "'a bexp";
    27 
    28 text{*\noindent
    29 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
    30 except that we have fixed the values to be of type @{typ"nat"} and that we
    31 have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
    32 expressions can be arithmetic comparisons, conjunctions and negations.
    33 The semantics is fixed via two evaluation functions
    34 *}
    35 
    36 consts  evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
    37         evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
    38 
    39 text{*\noindent
    40 that take an expression and an environment (a mapping from variables @{typ"'a"} to values
    41 @{typ"nat"}) and return its arithmetic/boolean
    42 value. Since the datatypes are mutually recursive, so are functions that
    43 operate on them. Hence they need to be defined in a single \isacommand{primrec}
    44 section:
    45 *}
    46 
    47 primrec
    48   "evala (IF b a1 a2) env =
    49      (if evalb b env then evala a1 env else evala a2 env)"
    50   "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
    51   "evala (Diff a1 a2) env = evala a1 env - evala a2 env"
    52   "evala (Var v) env = env v"
    53   "evala (Num n) env = n"
    54 
    55   "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
    56   "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
    57   "evalb (Neg b) env = (\<not> evalb b env)"
    58 
    59 text{*\noindent
    60 In the same fashion we also define two functions that perform substitution:
    61 *}
    62 
    63 consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
    64        substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
    65 
    66 text{*\noindent
    67 The first argument is a function mapping variables to expressions, the
    68 substitution. It is applied to all variables in the second argument. As a
    69 result, the type of variables in the expression may change from @{typ"'a"}
    70 to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
    71 *}
    72 
    73 primrec
    74   "substa s (IF b a1 a2) =
    75      IF (substb s b) (substa s a1) (substa s a2)"
    76   "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
    77   "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
    78   "substa s (Var v) = s v"
    79   "substa s (Num n) = Num n"
    80 
    81   "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
    82   "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
    83   "substb s (Neg b) = Neg (substb s b)";
    84 
    85 text{*
    86 Now we can prove a fundamental theorem about the interaction between
    87 evaluation and substitution: applying a substitution $s$ to an expression $a$
    88 and evaluating the result in an environment $env$ yields the same result as
    89 evaluation $a$ in the environment that maps every variable $x$ to the value
    90 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
    91 boolean expressions (by induction), you find that you always need the other
    92 theorem in the induction step. Therefore you need to state and prove both
    93 theorems simultaneously:
    94 *}
    95 
    96 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
    97         evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
    98 apply(induct_tac a and b);
    99 
   100 txt{*\noindent
   101 The resulting 8 goals (one for each constructor) are proved in one fell swoop:
   102 *}
   103 
   104 apply simp_all;
   105 (*<*)done(*>*)
   106 
   107 text{*
   108 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
   109 an inductive proof expects a goal of the form
   110 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
   111 where each variable $x@i$ is of type $\tau@i$. Induction is started by
   112 \begin{isabelle}
   113 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
   114 \end{isabelle}
   115 
   116 \begin{exercise}
   117   Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that
   118   replaces @{term"IF"}s with complex boolean conditions by nested
   119   @{term"IF"}s where each condition is a @{term"Less"} --- @{term"And"} and
   120   @{term"Neg"} should be eliminated completely. Prove that @{text"norma"}
   121   preserves the value of an expression and that the result of @{text"norma"}
   122   is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
   123   it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
   124 \end{exercise}
   125 *}
   126 (*<*)
   127 end
   128 (*>*)