src/HOL/IMP/Expr.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 27362 a6dc1769fdda
child 37736 2bf3a2cb5e58
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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 lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
    89   by (rule,cases set: evala) auto
    90 
    91 lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
    92   by (rule,cases set: evala) auto
    93 
    94 lemma   [simp]:
    95   "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
    96   by (rule,cases set: evala) auto
    97 
    98 lemma [simp]:
    99   "(Op2 f a1 a2,sigma) -a-> i =
   100   (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
   101   by (rule,cases set: evala) auto
   102 
   103 lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
   104   by (rule,cases set: evalb) auto
   105 
   106 lemma [simp]:
   107   "((false,sigma) -b-> w) = (w=False)"
   108   by (rule,cases set: evalb) auto
   109 
   110 lemma [simp]:
   111   "((ROp f a0 a1,sigma) -b-> w) =
   112   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
   113   by (rule,cases set: evalb) blast+
   114 
   115 lemma [simp]:
   116   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
   117   by (rule,cases set: evalb) blast+
   118 
   119 lemma [simp]:
   120   "((b0 andi b1,sigma) -b-> w) =
   121   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
   122   by (rule,cases set: evalb) blast+
   123 
   124 lemma [simp]:
   125   "((b0 ori b1,sigma) -b-> w) =
   126   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
   127   by (rule,cases set: evalb) blast+
   128 
   129 
   130 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
   131   by (induct a arbitrary: n) auto
   132 
   133 lemma bexp_iff:
   134   "((b,s) -b-> w) = (B b s = w)"
   135   by (induct b arbitrary: w) (auto simp add: aexp_iff)
   136 
   137 end