src/Doc/Tutorial/Datatype/ABexpr.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)
     2 theory ABexpr imports Main begin
     3 (*>*)
     4 
     5 text{*
     6 \index{datatypes!mutually recursive}%
     7 Sometimes it is necessary to define two datatypes that depend on each
     8 other. This is called \textbf{mutual recursion}. As an example consider a
     9 language of arithmetic and boolean expressions where
    10 \begin{itemize}
    11 \item arithmetic expressions contain boolean expressions because there are
    12   conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'',
    13   and
    14 \item boolean expressions contain arithmetic expressions because of
    15   comparisons like ``$m<n$''.
    16 \end{itemize}
    17 In Isabelle this becomes
    18 *}
    19 
    20 datatype 'a aexp = IF   "'a bexp" "'a aexp" "'a aexp"
    21                  | Sum  "'a aexp" "'a aexp"
    22                  | Diff "'a aexp" "'a aexp"
    23                  | Var 'a
    24                  | Num nat
    25 and      'a bexp = Less "'a aexp" "'a aexp"
    26                  | And  "'a bexp" "'a bexp"
    27                  | Neg  "'a bexp"
    28 
    29 text{*\noindent
    30 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
    31 except that we have added an @{text IF} constructor,
    32 fixed the values to be of type @{typ"nat"} and declared the two binary
    33 operations @{text Sum} and @{term"Diff"}.  Boolean
    34 expressions can be arithmetic comparisons, conjunctions and negations.
    35 The semantics is given by two evaluation functions:
    36 *}
    37 
    38 primrec evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" and
    39          evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" where
    40 "evala (IF b a1 a2) env =
    41    (if evalb b env then evala a1 env else evala a2 env)" |
    42 "evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
    43 "evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
    44 "evala (Var v) env = env v" |
    45 "evala (Num n) env = n" |
    46 
    47 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
    48 "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
    49 "evalb (Neg b) env = (\<not> evalb b env)"
    50 
    51 text{*\noindent
    52 
    53 Both take an expression and an environment (a mapping from variables
    54 @{typ"'a"} to values @{typ"nat"}) and return its arithmetic/boolean
    55 value. Since the datatypes are mutually recursive, so are functions
    56 that operate on them. Hence they need to be defined in a single
    57 \isacommand{primrec} section. Notice the \isakeyword{and} separating
    58 the declarations of @{const evala} and @{const evalb}. Their defining
    59 equations need not be split into two groups;
    60 the empty line is purely for readability.
    61 
    62 In the same fashion we also define two functions that perform substitution:
    63 *}
    64 
    65 primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" and
    66          substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" where
    67 "substa s (IF b a1 a2) =
    68    IF (substb s b) (substa s a1) (substa s a2)" |
    69 "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
    70 "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" |
    71 "substa s (Var v) = s v" |
    72 "substa s (Num n) = Num n" |
    73 
    74 "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
    75 "substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
    76 "substb s (Neg b) = Neg (substb s b)"
    77 
    78 text{*\noindent
    79 Their first argument is a function mapping variables to expressions, the
    80 substitution. It is applied to all variables in the second argument. As a
    81 result, the type of variables in the expression may change from @{typ"'a"}
    82 to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
    83 
    84 Now we can prove a fundamental theorem about the interaction between
    85 evaluation and substitution: applying a substitution $s$ to an expression $a$
    86 and evaluating the result in an environment $env$ yields the same result as
    87 evaluation $a$ in the environment that maps every variable $x$ to the value
    88 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
    89 boolean expressions (by induction), you find that you always need the other
    90 theorem in the induction step. Therefore you need to state and prove both
    91 theorems simultaneously:
    92 *}
    93 
    94 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
    95         evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
    96 apply(induct_tac a and b)
    97 
    98 txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:
    99 *}
   100 
   101 apply simp_all
   102 (*<*)done(*>*)
   103 
   104 text{*
   105 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
   106 an inductive proof expects a goal of the form
   107 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
   108 where each variable $x@i$ is of type $\tau@i$. Induction is started by
   109 \begin{isabelle}
   110 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text ")"}
   111 \end{isabelle}
   112 
   113 \begin{exercise}
   114   Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that
   115   replaces @{term"IF"}s with complex boolean conditions by nested
   116   @{term"IF"}s; it should eliminate the constructors
   117   @{term"And"} and @{term"Neg"}, leaving only @{term"Less"}.
   118   Prove that @{text"norma"}
   119   preserves the value of an expression and that the result of @{text"norma"}
   120   is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
   121   it.  ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
   122   of type annotations following lemma @{text subst_id} below).
   123 \end{exercise}
   124 *}
   125 (*<*)
   126 primrec norma :: "'a aexp \<Rightarrow> 'a aexp" and
   127         normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp" where
   128 "norma (IF b t e)   = (normb b (norma t) (norma e))" |
   129 "norma (Sum a1 a2)  = Sum (norma a1) (norma a2)" |
   130 "norma (Diff a1 a2) = Diff (norma a1) (norma a2)" |
   131 "norma (Var v)      = Var v" |
   132 "norma (Num n)      = Num n" |
   133             
   134 "normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e" |
   135 "normb (And b1 b2)  t e = normb b1 (normb b2 t e) e" |
   136 "normb (Neg b)      t e = normb b e t"
   137 
   138 lemma " evala (norma a) env = evala a env 
   139       \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
   140 apply (induct_tac a and b)
   141 apply (simp_all)
   142 done
   143 
   144 primrec normala :: "'a aexp \<Rightarrow> bool" and
   145         normalb :: "'a bexp \<Rightarrow> bool" where
   146 "normala (IF b t e)   = (normalb b \<and> normala t \<and> normala e)" |
   147 "normala (Sum a1 a2)  = (normala a1 \<and> normala a2)" |
   148 "normala (Diff a1 a2) = (normala a1 \<and> normala a2)" |
   149 "normala (Var v)      = True" |
   150 "normala (Num n)      = True" |
   151 
   152 "normalb (Less a1 a2) = (normala a1 \<and> normala a2)" |
   153 "normalb (And b1 b2)  = False" |
   154 "normalb (Neg b)      = False"
   155 
   156 lemma "normala (norma (a::'a aexp)) \<and>
   157        (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
   158 apply (induct_tac a and b)
   159 apply (auto)
   160 done
   161 
   162 end
   163 (*>*)