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"
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@924
    22
  aexp = N (nat)
clasohm@924
    23
       | X (loc)
clasohm@924
    24
       | Op1 (n2n, aexp)
clasohm@924
    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@924
    29
       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
clasohm@924
    30
translations
clasohm@924
    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@924
    37
    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
clasohm@924
    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@924
    47
       | ROp  (n2n2b, aexp, aexp)
clasohm@924
    48
       | noti (bexp)
clasohm@924
    49
       | andi (bexp,bexp)	(infixl 60)
clasohm@924
    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@924
    54
       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
clasohm@924
    55
clasohm@924
    56
translations
clasohm@924
    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@924
    63
    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
clasohm@924
    64
\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
clasohm@924
    65
    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
clasohm@924
    66
    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
clasohm@924
    67
\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
clasohm@924
    68
    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
clasohm@924
    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@924
    75
      | ":="   (loc,aexp)	 (infixl  60)
clasohm@924
    76
      | semic  (com,com)	 ("_; _"  [60, 60] 10)
clasohm@924
    77
      | whileC (bexp,com)	 ("while _ do _"  60)
clasohm@924
    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@924
    82
        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
clasohm@924
    83
	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
clasohm@924
    84
clasohm@924
    85
translations
clasohm@924
    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@924
    97
    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
clasohm@924
    98
\            ==> <c0 ; c1, s> -c-> s1"
clasohm@924
    99
clasohm@924
   100
    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
clasohm@924
   101
\            ==> <ifc b then c0 else c1, s> -c-> s1"
clasohm@924
   102
clasohm@924
   103
    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
clasohm@924
   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@924
   108
    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
clasohm@924
   109
\                  <while b do c, s2> -c-> s1 |] \
clasohm@924
   110
\               ==> <while b do c, s> -c-> s1 "
clasohm@924
   111
 
clasohm@924
   112
end