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