src/HOL/IMP/Expr.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
     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 consts
    72   A     :: "aexp => state => nat"
    73   B     :: "bexp => state => bool"
    74 
    75 primrec
    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
    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 lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
    90   by (rule,cases set: evala) auto
    91 
    92 lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
    93   by (rule,cases set: evala) auto
    94 
    95 lemma   [simp]:
    96   "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
    97   by (rule,cases set: evala) auto
    98 
    99 lemma [simp]:
   100   "(Op2 f a1 a2,sigma) -a-> i =
   101   (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
   102   by (rule,cases set: evala) auto
   103 
   104 lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
   105   by (rule,cases set: evalb) auto
   106 
   107 lemma [simp]:
   108   "((false,sigma) -b-> w) = (w=False)"
   109   by (rule,cases set: evalb) auto
   110 
   111 lemma [simp]:
   112   "((ROp f a0 a1,sigma) -b-> w) =
   113   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
   114   by (rule,cases set: evalb) blast+
   115 
   116 lemma [simp]:
   117   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
   118   by (rule,cases set: evalb) blast+
   119 
   120 lemma [simp]:
   121   "((b0 andi b1,sigma) -b-> w) =
   122   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
   123   by (rule,cases set: evalb) blast+
   124 
   125 lemma [simp]:
   126   "((b0 ori b1,sigma) -b-> w) =
   127   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
   128   by (rule,cases set: evalb) blast+
   129 
   130 
   131 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
   132   by (induct a arbitrary: n) auto
   133 
   134 lemma bexp_iff:
   135   "((b,s) -b-> w) = (B b s = w)"
   136   by (induct b arbitrary: w) (auto simp add: aexp_iff)
   137 
   138 end