src/HOL/IMPP/Natural.thy
changeset 17477 ceb42ea2f223
parent 8177 e59e93ad85eb
child 19803 aa2581752afb
     1.1 --- a/src/HOL/IMPP/Natural.thy	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/Natural.thy	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -2,88 +2,111 @@
     1.4      ID:         $Id$
     1.5      Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     1.6      Copyright   1999 TUM
     1.7 -
     1.8 -Natural semantics of commands
     1.9  *)
    1.10  
    1.11 -Natural = Com + 
    1.12 +header {* Natural semantics of commands *}
    1.13 +
    1.14 +theory Natural
    1.15 +imports Com
    1.16 +begin
    1.17  
    1.18  (** Execution of commands **)
    1.19 -consts	 evalc :: "(com * state *       state) set"
    1.20 -       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
    1.21 -	 evaln :: "(com * state * nat * state) set"
    1.22 -       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
    1.23 +consts
    1.24 +  evalc :: "(com * state *       state) set"
    1.25 +  evaln :: "(com * state * nat * state) set"
    1.26  
    1.27 -translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
    1.28 -              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
    1.29 +syntax
    1.30 +  "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
    1.31 +  "@evaln":: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
    1.32 +
    1.33 +translations
    1.34 +  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
    1.35 +  "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
    1.36  
    1.37  consts
    1.38    newlocs :: locals
    1.39 -  setlocs :: state => locals => state
    1.40 -  getlocs :: state => locals
    1.41 -  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
    1.42 +  setlocs :: "state => locals => state"
    1.43 +  getlocs :: "state => locals"
    1.44 +  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
    1.45  syntax (* IN Natural.thy *)
    1.46 -  loc :: state => locals    ("_<_>" [75,0] 75)
    1.47 +  loc :: "state => locals"    ("_<_>" [75,0] 75)
    1.48  translations
    1.49    "s<X>" == "getlocs s X"
    1.50  
    1.51  inductive evalc
    1.52 -  intrs
    1.53 -    Skip    "<SKIP,s> -c-> s"
    1.54 +  intros
    1.55 +    Skip:    "<SKIP,s> -c-> s"
    1.56  
    1.57 -    Assign  "<X :== a,s> -c-> s[X::=a s]"
    1.58 +    Assign:  "<X :== a,s> -c-> s[X::=a s]"
    1.59  
    1.60 -    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
    1.61 -             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
    1.62 +    Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
    1.63 +              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
    1.64  
    1.65 -    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
    1.66 -             <c0;; c1, s0> -c-> s2"
    1.67 +    Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
    1.68 +              <c0;; c1, s0> -c-> s2"
    1.69  
    1.70 -    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
    1.71 -             <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.72 +    IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
    1.73 +              <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.74  
    1.75 -    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
    1.76 -             <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.77 +    IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
    1.78 +              <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.79  
    1.80 -    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
    1.81 +    WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
    1.82  
    1.83 -    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
    1.84 -                <WHILE b DO c, s0> -c-> s2"
    1.85 +    WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
    1.86 +                 <WHILE b DO c, s0> -c-> s2"
    1.87  
    1.88 -    Body       "<the (body pn), s0> -c-> s1 ==>
    1.89 -                <BODY pn, s0> -c-> s1"
    1.90 +    Body:       "<the (body pn), s0> -c-> s1 ==>
    1.91 +                 <BODY pn, s0> -c-> s1"
    1.92  
    1.93 -    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
    1.94 -                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
    1.95 -                                         [X::=s1<Res>]"
    1.96 +    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
    1.97 +                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
    1.98 +                                          [X::=s1<Res>]"
    1.99  
   1.100  inductive evaln
   1.101 -  intrs
   1.102 -    Skip    "<SKIP,s> -n-> s"
   1.103 +  intros
   1.104 +    Skip:    "<SKIP,s> -n-> s"
   1.105 +
   1.106 +    Assign:  "<X :== a,s> -n-> s[X::=a s]"
   1.107  
   1.108 -    Assign  "<X :== a,s> -n-> s[X::=a s]"
   1.109 +    Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
   1.110 +              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
   1.111 +
   1.112 +    Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
   1.113 +              <c0;; c1, s0> -n-> s2"
   1.114  
   1.115 -    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
   1.116 -             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
   1.117 +    IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
   1.118 +              <IF b THEN c0 ELSE c1, s> -n-> s1"
   1.119  
   1.120 -    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
   1.121 -             <c0;; c1, s0> -n-> s2"
   1.122 +    IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
   1.123 +              <IF b THEN c0 ELSE c1, s> -n-> s1"
   1.124  
   1.125 -    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
   1.126 -             <IF b THEN c0 ELSE c1, s> -n-> s1"
   1.127 +    WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
   1.128 +
   1.129 +    WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
   1.130 +                 <WHILE b DO c, s0> -n-> s2"
   1.131  
   1.132 -    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
   1.133 -             <IF b THEN c0 ELSE c1, s> -n-> s1"
   1.134 +    Body:       "<the (body pn), s0> -    n-> s1 ==>
   1.135 +                 <BODY pn, s0> -Suc n-> s1"
   1.136  
   1.137 -    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
   1.138 +    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
   1.139 +                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
   1.140 +                                          [X::=s1<Res>]"
   1.141  
   1.142 -    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
   1.143 -                <WHILE b DO c, s0> -n-> s2"
   1.144  
   1.145 -    Body       "<the (body pn), s0> -    n-> s1 ==>
   1.146 -                <BODY pn, s0> -Suc n-> s1"
   1.147 +inductive_cases evalc_elim_cases:
   1.148 +  "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
   1.149 +  "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
   1.150 +  "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"
   1.151  
   1.152 -    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
   1.153 -                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
   1.154 -                                         [X::=s1<Res>]"
   1.155 +inductive_cases evaln_elim_cases:
   1.156 +  "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
   1.157 +  "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
   1.158 +  "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"
   1.159 +
   1.160 +inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
   1.161 +inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
   1.162 +
   1.163 +ML {* use_legacy_bindings (the_context ()) *}
   1.164 +
   1.165  end