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