src/HOL/IMP/Expr.thy
author berghofe
Thu Aug 08 11:34:29 1996 +0200 (1996-08-08)
changeset 1900 c7a869229091
parent 1789 aade046ec6d5
child 5102 8c782c25a11e
permissions -rw-r--r--
Simplified primrec definitions.
     1 (*  Title:      HOL/IMP/Expr.thy
     2     ID:         $Id$
     3     Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     4     Copyright   1994 TUM
     5 
     6 Arithmetic expressions and Boolean expressions.
     7 Not used in the rest of the language, but included for completeness.
     8 *)
     9 
    10 Expr = Arith +
    11 
    12 (** Arithmetic expressions **)
    13 types loc
    14       state = "loc => nat"
    15       n2n = "nat => nat"
    16       n2n2n = "nat => nat => nat"
    17 
    18 arities loc :: term
    19 
    20 datatype
    21   aexp = N nat
    22        | X loc
    23        | Op1 n2n aexp
    24        | Op2 n2n2n aexp aexp
    25 
    26 (** Evaluation of arithmetic expressions **)
    27 consts  evala    :: "((aexp*state) * nat) set"
    28        "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
    29 translations
    30     "aesig -a-> n" == "(aesig,n) : evala"
    31 inductive evala
    32   intrs 
    33     N   "(N(n),s) -a-> n"
    34     X   "(X(x),s) -a-> s(x)"
    35     Op1 "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
    36     Op2 "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |] 
    37            ==> (Op2 f e0 e1,s) -a-> f n0 n1"
    38 
    39 types n2n2b = "[nat,nat] => bool"
    40 
    41 (** Boolean expressions **)
    42 
    43 datatype
    44   bexp = true
    45        | false
    46        | ROp  n2n2b aexp aexp
    47        | noti bexp
    48        | andi bexp bexp         (infixl 60)
    49        | ori  bexp bexp         (infixl 60)
    50 
    51 (** Evaluation of boolean expressions **)
    52 consts evalb    :: "((bexp*state) * bool)set"       
    53        "-b->"   :: "[bexp*state,bool] => bool"         (infixl 50)
    54 
    55 translations
    56     "besig -b-> b" == "(besig,b) : evalb"
    57 
    58 inductive evalb
    59  intrs (*avoid clash with ML constructors true, false*)
    60     tru   "(true,s) -b-> True"
    61     fls   "(false,s) -b-> False"
    62     ROp   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] 
    63            ==> (ROp f a0 a1,s) -b-> f n0 n1"
    64     noti  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
    65     andi  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    66           ==> (b0 andi b1,s) -b-> (w0 & w1)"
    67     ori   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    68             ==> (b0 ori b1,s) -b-> (w0 | w1)"
    69 
    70 (** Denotational semantics of arithemtic and boolean expressions **)
    71 consts
    72   A     :: aexp => state => nat
    73   B     :: bexp => state => bool
    74 
    75 primrec A aexp
    76   "A(N(n)) = (%s. n)"
    77   "A(X(x)) = (%s. s(x))"
    78   "A(Op1 f a) = (%s. f(A a s))"
    79   "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    80 
    81 primrec B bexp
    82   "B(true) = (%s. True)"
    83   "B(false) = (%s. False)"
    84   "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    85   "B(noti(b)) = (%s. ~(B b s))"
    86   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    87   "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    88 
    89 end
    90