src/HOL/IMP/Expr.thy
author nipkow
Sat, 27 Apr 1996 18:49:21 +0200
changeset 1697 687f0710c22d
child 1729 e4f8682eea2e
permissions -rw-r--r--
Arithemtic and boolean expressions are now in a separate theory. The commands don not use them directly. Instead they are based on the semantics (rather than the syntax) of expressions.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1697
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/IMP/Expr.thy
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     3
    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     4
    Copyright   1994 TUM
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     5
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     6
Arithmetic expressions and Boolean expressions.
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     7
Not used in the rest of the language, but included for completeness.
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     8
*)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
     9
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    10
Expr = Arith +
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    11
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    12
(** Arithmetic expressions **)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    13
types loc
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    14
      state = "loc => nat"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    15
      n2n = "nat => nat"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    16
      n2n2n = "nat => nat => nat"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    17
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    18
arities loc :: term
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    19
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    20
datatype
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    21
  aexp = N nat
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    22
       | X loc
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    23
       | Op1 n2n aexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    24
       | Op2 n2n2n aexp aexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    25
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    26
(** Evaluation of arithmetic expressions **)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    27
consts  evala    :: "(aexp*state*nat)set"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    28
       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    29
translations
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    30
    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    31
inductive "evala"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    32
  intrs 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    33
    N   "<N(n),s> -a-> n"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    34
    X   "<X(x),s> -a-> s(x)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    35
    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    36
    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    37
           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    38
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    39
types n2n2b = "[nat,nat] => bool"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    40
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    41
(** Boolean expressions **)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    42
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    43
datatype
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    44
  bexp = true
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    45
       | false
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    46
       | ROp  n2n2b aexp aexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    47
       | noti bexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    48
       | andi bexp bexp         (infixl 60)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    49
       | ori  bexp bexp         (infixl 60)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    50
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    51
(** Evaluation of boolean expressions **)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    52
consts evalb    :: "(bexp*state*bool)set"       
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    53
       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    54
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    55
translations
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    56
    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    57
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    58
inductive "evalb"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    59
 intrs (*avoid clash with ML constructors true, false*)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    60
    tru   "<true,s> -b-> True"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    61
    fls   "<false,s> -b-> False"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    62
    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    63
           ==> <ROp f a0 a1,s> -b-> f n0 n1"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    64
    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    65
    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    66
          ==> <b0 andi b1,s> -b-> (w0 & w1)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    67
    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    68
            ==> <b0 ori b1,s> -b-> (w0 | w1)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    69
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    70
(** Denotational semantics of arithemtic and boolean expressions **)
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    71
consts
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    72
  A     :: aexp => state => nat
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    73
  B     :: bexp => state => bool
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    74
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    75
primrec A aexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    76
  A_nat "A(N(n)) = (%s. n)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    77
  A_loc "A(X(x)) = (%s. s(x))" 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    78
  A_op1 "A(Op1 f a) = (%s. f(A a s))"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    79
  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    80
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    81
primrec B bexp
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    82
  B_true  "B(true) = (%s. True)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    83
  B_false "B(false) = (%s. False)"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    84
  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    85
  B_not   "B(noti(b)) = (%s. ~(B b s))"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    86
  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    87
  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    88
687f0710c22d Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff changeset
    89
end