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