src/HOL/IMP/Com.thy
author clasohm
Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476 608483c2122a
parent 1374 5e407f2a3323
child 1481 03f096efa26d
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     1
(*  Title:      HOL/IMP/Com.thy
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     3
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TUM
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     5
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     6
Arithmetic expressions, Boolean expressions, Commands
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     7
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     8
And their Operational semantics
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     9
*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    10
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
Com = Arith +
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    12
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    13
(** Arithmetic expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    14
types loc
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    15
      state = "loc => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    16
      n2n = "nat => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    17
      n2n2n = "nat => nat => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    18
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    19
arities loc :: term
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    20
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    21
datatype
977
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    22
  aexp = N nat
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    23
       | X loc
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    24
       | Op1 n2n aexp
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    25
       | Op2 n2n2n aexp aexp
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    26
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    27
(** Evaluation of arithmetic expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    28
consts  evala    :: "(aexp*state*nat)set"
1374
5e407f2a3323 removed quotes from consts and syntax sections
clasohm
parents: 1151
diff changeset
    29
       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    30
translations
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 965
diff changeset
    31
    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    32
inductive "evala"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    33
  intrs 
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    34
    N   "<N(n),s> -a-> n"
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    35
    X   "<X(x),s> -a-> s(x)"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    36
    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    37
    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    38
           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    39
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    40
types n2n2b = "[nat,nat] => bool"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    41
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    42
(** Boolean expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    43
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    44
datatype
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    45
  bexp = true
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    46
       | false
977
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    47
       | ROp  n2n2b aexp aexp
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 972
diff changeset
    48
       | noti bexp
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    49
       | andi bexp bexp         (infixl 60)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    50
       | ori  bexp bexp         (infixl 60)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    51
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    52
(** Evaluation of boolean expressions **)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    53
consts evalb    :: "(bexp*state*bool)set"       
1374
5e407f2a3323 removed quotes from consts and syntax sections
clasohm
parents: 1151
diff changeset
    54
       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    55
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    56
translations
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 965
diff changeset
    57
    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    58
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    59
inductive "evalb"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    60
 intrs (*avoid clash with ML constructors true, false*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    61
    tru   "<true,s> -b-> True"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    62
    fls   "<false,s> -b-> False"
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    63
    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    64
           ==> <ROp f a0 a1,s> -b-> f n0 n1"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    65
    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    66
    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    67
          ==> <b0 andi b1,s> -b-> (w0 & w1)"
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    68
    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    69
            ==> <b0 ori b1,s> -b-> (w0 | w1)"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    70
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    71
(** Commands **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    72
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    73
datatype
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    74
  com = skip
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    75
      | ":="   loc aexp          (infixl  60)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    76
      | semic  com com           ("_; _"  [60, 60] 10)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    77
      | whileC bexp com          ("while _ do _"  60)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    78
      | ifC    bexp com com      ("ifc _ then _ else _"  60)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    79
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    80
(** Execution of commands **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    81
consts  evalc    :: "(com*state*state)set"
1374
5e407f2a3323 removed quotes from consts and syntax sections
clasohm
parents: 1151
diff changeset
    82
        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    83
        "assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    84
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    85
translations
972
e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents: 965
diff changeset
    86
       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    87
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    88
rules 
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    89
        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    90
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    91
inductive "evalc"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    92
  intrs
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    93
    skip    "<skip,s> -c-> s"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    94
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    95
    assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    96
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    97
    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
    98
            ==> <c0 ; c1, s> -c-> s1"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    99
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   100
    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   101
            ==> <ifc b then c0 else c1, s> -c-> s1"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   102
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   103
    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   104
             ==> <ifc b then c0 else c1, s> -c-> s1"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   105
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   106
    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   107
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   108
    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   109
                  <while b do c, s2> -c-> s1 |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 977
diff changeset
   110
               ==> <while b do c, s> -c-> s1 "
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   111
 
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   112
end