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