src/HOL/Induct/Exp.thy
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3120 c58423c20740
child 4264 5e21f41ccd21
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);

(*  Title:      HOL/Induct/Exp
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
*)

Exp = Com +

(** Evaluation of arithmetic expressions **)
consts  eval    :: "((exp*state) * (nat*state)) set"
       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
translations
    "esig -|-> (n,s)" <= "(esig,n,s) : eval"
    "esig -|-> ns"    == "(esig,ns) : eval"
  
inductive eval
  intrs 
    N      "(N(n),s) -|-> (n,s)"

    X      "(X(x),s) -|-> (s(x),s)"

    Op     "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
            ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"

    valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
            ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"

  monos "[exec_mono]"

end