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;
nipkow@1697
     1
(*  Title:      HOL/IMP/Expr.thy
nipkow@1697
     2
    ID:         $Id$
nipkow@1697
     3
    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
nipkow@1697
     4
    Copyright   1994 TUM
nipkow@1697
     5
*)
nipkow@1697
     6
kleing@12431
     7
header "Expressions"
kleing@12431
     8
haftmann@16417
     9
theory Expr imports Main begin
nipkow@1697
    10
kleing@12431
    11
text {*
kleing@12431
    12
  Arithmetic expressions and Boolean expressions.
kleing@12431
    13
  Not used in the rest of the language, but included for completeness.
kleing@12431
    14
*}
nipkow@1697
    15
kleing@12431
    16
subsection "Arithmetic expressions"
wenzelm@12546
    17
typedecl loc
kleing@12431
    18
kleing@12431
    19
types
kleing@12431
    20
  state = "loc => nat"
nipkow@1697
    21
nipkow@1697
    22
datatype
nipkow@1697
    23
  aexp = N nat
nipkow@1697
    24
       | X loc
wenzelm@12546
    25
       | Op1 "nat => nat" aexp
wenzelm@12546
    26
       | Op2 "nat => nat => nat" aexp aexp
nipkow@1697
    27
kleing@12431
    28
subsection "Evaluation of arithmetic expressions"
berghofe@23746
    29
berghofe@23746
    30
inductive
berghofe@23746
    31
  evala :: "[aexp*state,nat] => bool"  (infixl "-a->" 50)
berghofe@23746
    32
where
kleing@12431
    33
  N:   "(N(n),s) -a-> n"
berghofe@23746
    34
| X:   "(X(x),s) -a-> s(x)"
berghofe@23746
    35
| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
berghofe@23746
    36
| Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
kleing@12431
    37
        ==> (Op2 f e0 e1,s) -a-> f n0 n1"
kleing@12431
    38
kleing@12431
    39
lemmas [intro] = N X Op1 Op2
nipkow@1697
    40
nipkow@1697
    41
kleing@12431
    42
subsection "Boolean expressions"
nipkow@1697
    43
nipkow@1697
    44
datatype
nipkow@1697
    45
  bexp = true
nipkow@1697
    46
       | false
wenzelm@12546
    47
       | ROp  "nat => nat => bool" aexp aexp
nipkow@1697
    48
       | noti bexp
wenzelm@22818
    49
       | andi bexp bexp         (infixl "andi" 60)
wenzelm@22818
    50
       | ori  bexp bexp         (infixl "ori" 60)
nipkow@1697
    51
kleing@12431
    52
subsection "Evaluation of boolean expressions"
nipkow@1697
    53
berghofe@23746
    54
inductive
berghofe@23746
    55
  evalb :: "[bexp*state,bool] => bool"  (infixl "-b->" 50)
kleing@12431
    56
  -- "avoid clash with ML constructors true, false"
berghofe@23746
    57
where
kleing@12431
    58
  tru:   "(true,s) -b-> True"
berghofe@23746
    59
| fls:   "(false,s) -b-> False"
berghofe@23746
    60
| ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
kleing@12431
    61
          ==> (ROp f a0 a1,s) -b-> f n0 n1"
berghofe@23746
    62
| noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
berghofe@23746
    63
| andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
paulson@1729
    64
          ==> (b0 andi b1,s) -b-> (w0 & w1)"
berghofe@23746
    65
| ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
kleing@12431
    66
          ==> (b0 ori b1,s) -b-> (w0 | w1)"
kleing@12431
    67
kleing@12431
    68
lemmas [intro] = tru fls ROp noti andi ori
nipkow@1697
    69
kleing@12431
    70
subsection "Denotational semantics of arithmetic and boolean expressions"
nipkow@1697
    71
consts
kleing@12431
    72
  A     :: "aexp => state => nat"
kleing@12431
    73
  B     :: "bexp => state => bool"
nipkow@1697
    74
berghofe@5183
    75
primrec
berghofe@1900
    76
  "A(N(n)) = (%s. n)"
berghofe@1900
    77
  "A(X(x)) = (%s. s(x))"
berghofe@1900
    78
  "A(Op1 f a) = (%s. f(A a s))"
berghofe@1900
    79
  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
nipkow@1697
    80
berghofe@5183
    81
primrec
berghofe@1900
    82
  "B(true) = (%s. True)"
berghofe@1900
    83
  "B(false) = (%s. False)"
berghofe@1900
    84
  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
berghofe@1900
    85
  "B(noti(b)) = (%s. ~(B b s))"
berghofe@1900
    86
  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
berghofe@1900
    87
  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
nipkow@1697
    88
kleing@12431
    89
lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
kleing@12431
    90
  by (rule,cases set: evala) auto
kleing@12431
    91
wenzelm@12546
    92
lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
kleing@12431
    93
  by (rule,cases set: evala) auto
kleing@12431
    94
wenzelm@12546
    95
lemma   [simp]:
wenzelm@12546
    96
  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
kleing@12431
    97
  by (rule,cases set: evala) auto
kleing@12431
    98
kleing@12431
    99
lemma [simp]:
wenzelm@12546
   100
  "(Op2 f a1 a2,sigma) -a-> i =
kleing@12431
   101
  (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
kleing@12431
   102
  by (rule,cases set: evala) auto
kleing@12431
   103
wenzelm@12546
   104
lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
kleing@12431
   105
  by (rule,cases set: evalb) auto
kleing@12431
   106
kleing@12431
   107
lemma [simp]:
wenzelm@12546
   108
  "((false,sigma) -b-> w) = (w=False)"
kleing@12431
   109
  by (rule,cases set: evalb) auto
kleing@12431
   110
kleing@12431
   111
lemma [simp]:
wenzelm@12546
   112
  "((ROp f a0 a1,sigma) -b-> w) =
wenzelm@12546
   113
  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
berghofe@23746
   114
  by (rule,cases set: evalb) blast+
kleing@12431
   115
wenzelm@12546
   116
lemma [simp]:
wenzelm@12546
   117
  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
berghofe@23746
   118
  by (rule,cases set: evalb) blast+
wenzelm@12546
   119
wenzelm@12546
   120
lemma [simp]:
wenzelm@12546
   121
  "((b0 andi b1,sigma) -b-> w) =
wenzelm@12546
   122
  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
berghofe@23746
   123
  by (rule,cases set: evalb) blast+
kleing@12431
   124
kleing@12431
   125
lemma [simp]:
wenzelm@12546
   126
  "((b0 ori b1,sigma) -b-> w) =
wenzelm@12546
   127
  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
berghofe@23746
   128
  by (rule,cases set: evalb) blast+
kleing@12431
   129
kleing@12431
   130
wenzelm@18372
   131
lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
wenzelm@20503
   132
  by (induct a arbitrary: n) auto
kleing@12431
   133
wenzelm@12546
   134
lemma bexp_iff:
wenzelm@18372
   135
  "((b,s) -b-> w) = (B b s = w)"
wenzelm@20503
   136
  by (induct b arbitrary: w) (auto simp add: aexp_iff)
kleing@12431
   137
nipkow@1697
   138
end