src/HOL/IMP/Expr.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18372 2bffdf62fe7f
child 20503 503ac4c5ef91
permissions -rw-r--r--
adaptions to codegen_package
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"
paulson@1729
    29
consts  evala    :: "((aexp*state) * nat) set"
wenzelm@12546
    30
syntax "_evala"  :: "[aexp*state,nat] => bool"         (infixl "-a->" 50)
nipkow@1697
    31
translations
paulson@1729
    32
    "aesig -a-> n" == "(aesig,n) : evala"
paulson@1789
    33
inductive evala
wenzelm@12546
    34
  intros
kleing@12431
    35
  N:   "(N(n),s) -a-> n"
kleing@12431
    36
  X:   "(X(x),s) -a-> s(x)"
kleing@12431
    37
  Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
wenzelm@12546
    38
  Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
kleing@12431
    39
        ==> (Op2 f e0 e1,s) -a-> f n0 n1"
kleing@12431
    40
kleing@12431
    41
lemmas [intro] = N X Op1 Op2
nipkow@1697
    42
nipkow@1697
    43
kleing@12431
    44
subsection "Boolean expressions"
nipkow@1697
    45
nipkow@1697
    46
datatype
nipkow@1697
    47
  bexp = true
nipkow@1697
    48
       | false
wenzelm@12546
    49
       | ROp  "nat => nat => bool" aexp aexp
nipkow@1697
    50
       | noti bexp
nipkow@1697
    51
       | andi bexp bexp         (infixl 60)
nipkow@1697
    52
       | ori  bexp bexp         (infixl 60)
nipkow@1697
    53
kleing@12431
    54
subsection "Evaluation of boolean expressions"
wenzelm@12546
    55
consts evalb    :: "((bexp*state) * bool)set"
wenzelm@12546
    56
syntax "_evalb" :: "[bexp*state,bool] => bool"         (infixl "-b->" 50)
nipkow@1697
    57
nipkow@1697
    58
translations
paulson@1729
    59
    "besig -b-> b" == "(besig,b) : evalb"
nipkow@1697
    60
paulson@1789
    61
inductive evalb
kleing@12431
    62
  -- "avoid clash with ML constructors true, false"
kleing@12431
    63
  intros
kleing@12431
    64
  tru:   "(true,s) -b-> True"
kleing@12431
    65
  fls:   "(false,s) -b-> False"
wenzelm@12546
    66
  ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
kleing@12431
    67
          ==> (ROp f a0 a1,s) -b-> f n0 n1"
kleing@12431
    68
  noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
wenzelm@12546
    69
  andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
paulson@1729
    70
          ==> (b0 andi b1,s) -b-> (w0 & w1)"
wenzelm@12546
    71
  ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
kleing@12431
    72
          ==> (b0 ori b1,s) -b-> (w0 | w1)"
kleing@12431
    73
kleing@12431
    74
lemmas [intro] = tru fls ROp noti andi ori
nipkow@1697
    75
kleing@12431
    76
subsection "Denotational semantics of arithmetic and boolean expressions"
nipkow@1697
    77
consts
kleing@12431
    78
  A     :: "aexp => state => nat"
kleing@12431
    79
  B     :: "bexp => state => bool"
nipkow@1697
    80
berghofe@5183
    81
primrec
berghofe@1900
    82
  "A(N(n)) = (%s. n)"
berghofe@1900
    83
  "A(X(x)) = (%s. s(x))"
berghofe@1900
    84
  "A(Op1 f a) = (%s. f(A a s))"
berghofe@1900
    85
  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
nipkow@1697
    86
berghofe@5183
    87
primrec
berghofe@1900
    88
  "B(true) = (%s. True)"
berghofe@1900
    89
  "B(false) = (%s. False)"
berghofe@1900
    90
  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
berghofe@1900
    91
  "B(noti(b)) = (%s. ~(B b s))"
berghofe@1900
    92
  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
berghofe@1900
    93
  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
nipkow@1697
    94
kleing@12431
    95
lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
kleing@12431
    96
  by (rule,cases set: evala) auto
kleing@12431
    97
wenzelm@12546
    98
lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
kleing@12431
    99
  by (rule,cases set: evala) auto
kleing@12431
   100
wenzelm@12546
   101
lemma   [simp]:
wenzelm@12546
   102
  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
kleing@12431
   103
  by (rule,cases set: evala) auto
kleing@12431
   104
kleing@12431
   105
lemma [simp]:
wenzelm@12546
   106
  "(Op2 f a1 a2,sigma) -a-> i =
kleing@12431
   107
  (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
kleing@12431
   108
  by (rule,cases set: evala) auto
kleing@12431
   109
wenzelm@12546
   110
lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
kleing@12431
   111
  by (rule,cases set: evalb) auto
kleing@12431
   112
kleing@12431
   113
lemma [simp]:
wenzelm@12546
   114
  "((false,sigma) -b-> w) = (w=False)"
kleing@12431
   115
  by (rule,cases set: evalb) auto
kleing@12431
   116
kleing@12431
   117
lemma [simp]:
wenzelm@12546
   118
  "((ROp f a0 a1,sigma) -b-> w) =
wenzelm@12546
   119
  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
kleing@12431
   120
  by (rule,cases set: evalb) auto
kleing@12431
   121
wenzelm@12546
   122
lemma [simp]:
wenzelm@12546
   123
  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
wenzelm@12546
   124
  by (rule,cases set: evalb) auto
wenzelm@12546
   125
wenzelm@12546
   126
lemma [simp]:
wenzelm@12546
   127
  "((b0 andi b1,sigma) -b-> w) =
wenzelm@12546
   128
  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
kleing@12431
   129
  by (rule,cases set: evalb) auto
kleing@12431
   130
kleing@12431
   131
lemma [simp]:
wenzelm@12546
   132
  "((b0 ori b1,sigma) -b-> w) =
wenzelm@12546
   133
  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
kleing@12431
   134
  by (rule,cases set: evalb) auto
kleing@12431
   135
kleing@12431
   136
wenzelm@18372
   137
lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
wenzelm@18372
   138
  by (induct a fixing: n) auto
kleing@12431
   139
wenzelm@12546
   140
lemma bexp_iff:
wenzelm@18372
   141
  "((b,s) -b-> w) = (B b s = w)"
wenzelm@18372
   142
  by (induct b fixing: w) (auto simp add: aexp_iff)
kleing@12431
   143
nipkow@1697
   144
end