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