src/HOL/IMP/Expr.thy
author wenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589 bbd861837ebc
parent 37736 2bf3a2cb5e58
child 42174 d0be2722ce9f
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/IMP/Expr.thy
     2     Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     3 *)
     4 
     5 header "Expressions"
     6 
     7 theory Expr imports Main begin
     8 
     9 text {*
    10   Arithmetic expressions and Boolean expressions.
    11   Not used in the rest of the language, but included for completeness.
    12 *}
    13 
    14 subsection "Arithmetic expressions"
    15 typedecl loc
    16 
    17 types
    18   state = "loc => nat"
    19 
    20 datatype
    21   aexp = N nat
    22        | X loc
    23        | Op1 "nat => nat" aexp
    24        | Op2 "nat => nat => nat" aexp aexp
    25 
    26 subsection "Evaluation of arithmetic expressions"
    27 
    28 inductive
    29   evala :: "[aexp*state,nat] => bool"  (infixl "-a->" 50)
    30 where
    31   N:   "(N(n),s) -a-> n"
    32 | X:   "(X(x),s) -a-> s(x)"
    33 | Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
    34 | Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
    35         ==> (Op2 f e0 e1,s) -a-> f n0 n1"
    36 
    37 lemmas [intro] = N X Op1 Op2
    38 
    39 
    40 subsection "Boolean expressions"
    41 
    42 datatype
    43   bexp = true
    44        | false
    45        | ROp  "nat => nat => bool" aexp aexp
    46        | noti bexp
    47        | andi bexp bexp         (infixl "andi" 60)
    48        | ori  bexp bexp         (infixl "ori" 60)
    49 
    50 subsection "Evaluation of boolean expressions"
    51 
    52 inductive
    53   evalb :: "[bexp*state,bool] => bool"  (infixl "-b->" 50)
    54   -- "avoid clash with ML constructors true, false"
    55 where
    56   tru:   "(true,s) -b-> True"
    57 | fls:   "(false,s) -b-> False"
    58 | ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
    59           ==> (ROp f a0 a1,s) -b-> f n0 n1"
    60 | noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
    61 | andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
    62           ==> (b0 andi b1,s) -b-> (w0 & w1)"
    63 | ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
    64           ==> (b0 ori b1,s) -b-> (w0 | w1)"
    65 
    66 lemmas [intro] = tru fls ROp noti andi ori
    67 
    68 subsection "Denotational semantics of arithmetic and boolean expressions"
    69 
    70 primrec A :: "aexp => state => nat"
    71 where
    72   "A(N(n)) = (%s. n)"
    73 | "A(X(x)) = (%s. s(x))"
    74 | "A(Op1 f a) = (%s. f(A a s))"
    75 | "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    76 
    77 primrec B :: "bexp => state => bool"
    78 where
    79   "B(true) = (%s. True)"
    80 | "B(false) = (%s. False)"
    81 | "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    82 | "B(noti(b)) = (%s. ~(B b s))"
    83 | "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    84 | "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    85 
    86 inductive_simps
    87   evala_simps [simp]:
    88   "(N(n),s) -a-> n'" 
    89   "(X(x),sigma) -a-> i"
    90   "(Op1 f e,sigma) -a-> i"
    91   "(Op2 f a1 a2,sigma) -a-> i"
    92   "((true,sigma) -b-> w)"
    93   "((false,sigma) -b-> w)"
    94   "((ROp f a0 a1,sigma) -b-> w)"
    95   "((noti(b),sigma) -b-> w)"
    96   "((b0 andi b1,sigma) -b-> w)"
    97   "((b0 ori b1,sigma) -b-> w)"
    98 
    99 
   100 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
   101   by (induct a arbitrary: n) auto
   102 
   103 lemma bexp_iff:
   104   "((b,s) -b-> w) = (B b s = w)"
   105   by (induct b arbitrary: w) (auto simp add: aexp_iff)
   106 
   107 end