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 (*>*)