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