src/HOL/IMPP/Natural.thy
author oheimb
Mon, 31 Jan 2000 18:30:35 +0100
changeset 8177 e59e93ad85eb
child 17477 ceb42ea2f223
permissions -rw-r--r--
added IMPP to HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/Natural.thy
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
Natural semantics of commands
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     7
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     8
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     9
Natural = Com + 
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    10
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
(** Execution of commands **)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
consts	 evalc :: "(com * state *       state) set"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    14
	 evaln :: "(com * state * nat * state) set"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    15
       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    18
              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    19
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    20
consts
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    21
  newlocs :: locals
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    22
  setlocs :: state => locals => state
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    23
  getlocs :: state => locals
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    24
  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
syntax (* IN Natural.thy *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
  loc :: state => locals    ("_<_>" [75,0] 75)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
translations
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    28
  "s<X>" == "getlocs s X"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    29
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    30
inductive evalc
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
  intrs
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    32
    Skip    "<SKIP,s> -c-> s"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    34
    Assign  "<X :== a,s> -c-> s[X::=a s]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    36
    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    37
             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    38
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    40
             <c0;; c1, s0> -c-> s2"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    42
    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    43
             <IF b THEN c0 ELSE c1, s> -c-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    45
    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    46
             <IF b THEN c0 ELSE c1, s> -c-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    48
    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    49
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    50
    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    51
                <WHILE b DO c, s0> -c-> s2"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    52
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    53
    Body       "<the (body pn), s0> -c-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    54
                <BODY pn, s0> -c-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    55
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    56
    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    57
                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    58
                                         [X::=s1<Res>]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    59
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    60
inductive evaln
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    61
  intrs
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    62
    Skip    "<SKIP,s> -n-> s"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    63
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    64
    Assign  "<X :== a,s> -n-> s[X::=a s]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    65
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    66
    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    67
             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    68
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    69
    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    70
             <c0;; c1, s0> -n-> s2"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    71
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    72
    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    73
             <IF b THEN c0 ELSE c1, s> -n-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    74
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    75
    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    76
             <IF b THEN c0 ELSE c1, s> -n-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    77
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    78
    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    79
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    80
    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    81
                <WHILE b DO c, s0> -n-> s2"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    82
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    83
    Body       "<the (body pn), s0> -    n-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    84
                <BODY pn, s0> -Suc n-> s1"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    85
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    86
    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    87
                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    88
                                         [X::=s1<Res>]"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    89
end