
diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Natural.thy
--- a/src/HOL/IMPP/Natural.thy	Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Natural.thy	Sat Sep 17 20:14:30 2005 +0200
@@ -2,88 +2,111 @@
     ID:         $Id$
     Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     Copyright   1999 TUM
-
-Natural semantics of commands
 *)
 
-Natural = Com + 
+header {* Natural semantics of commands *}
+
+theory Natural
+imports Com
+begin
 
 (** Execution of commands **)
-consts	 evalc :: "(com * state *       state) set"
-       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
-	 evaln :: "(com * state * nat * state) set"
-       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
+consts
+  evalc :: "(com * state *       state) set"
+  evaln :: "(com * state * nat * state) set"
 
-translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
-              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
+syntax
+  "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
+  "@evaln":: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
+
+translations
+  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
+  "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
 
 consts
   newlocs :: locals
-  setlocs :: state => locals => state
-  getlocs :: state => locals
-  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
+  setlocs :: "state => locals => state"
+  getlocs :: "state => locals"
+  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
 syntax (* IN Natural.thy *)
-  loc :: state => locals    ("_<_>" [75,0] 75)
+  loc :: "state => locals"    ("_<_>" [75,0] 75)
 translations
   "s<X>" == "getlocs s X"
 
 inductive evalc
-  intrs
-    Skip    "<SKIP,s> -c-> s"
+  intros
+    Skip:    "<SKIP,s> -c-> s"
 
-    Assign  "<X :== a,s> -c-> s[X::=a s]"
+    Assign:  "<X :== a,s> -c-> s[X::=a s]"
 
-    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
-             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
+    Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
+              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
 
-    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
-             <c0;; c1, s0> -c-> s2"
+    Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
+              <c0;; c1, s0> -c-> s2"
 
-    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -c-> s1"
+    IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -c-> s1"
+    IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
+    WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
 
-    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
-                <WHILE b DO c, s0> -c-> s2"
+    WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
+                 <WHILE b DO c, s0> -c-> s2"
 
-    Body       "<the (body pn), s0> -c-> s1 ==>
-                <BODY pn, s0> -c-> s1"
+    Body:       "<the (body pn), s0> -c-> s1 ==>
+                 <BODY pn, s0> -c-> s1"
 
-    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
-                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
-                                         [X::=s1<Res>]"
+    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
+                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
+                                          [X::=s1<Res>]"
 
 inductive evaln
-  intrs
-    Skip    "<SKIP,s> -n-> s"
+  intros
+    Skip:    "<SKIP,s> -n-> s"
+
+    Assign:  "<X :== a,s> -n-> s[X::=a s]"
 
-    Assign  "<X :== a,s> -n-> s[X::=a s]"
+    Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
+              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+
+    Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
+              <c0;; c1, s0> -n-> s2"
 
-    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
-             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+    IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -n-> s1"
 
-    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
-             <c0;; c1, s0> -n-> s2"
+    IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
+              <IF b THEN c0 ELSE c1, s> -n-> s1"
 
-    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -n-> s1"
+    WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
+
+    WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
+                 <WHILE b DO c, s0> -n-> s2"
 
-    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
-             <IF b THEN c0 ELSE c1, s> -n-> s1"
+    Body:       "<the (body pn), s0> -    n-> s1 ==>
+                 <BODY pn, s0> -Suc n-> s1"
 
-    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
+    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
+                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
+                                          [X::=s1<Res>]"
 
-    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
-                <WHILE b DO c, s0> -n-> s2"
 
-    Body       "<the (body pn), s0> -    n-> s1 ==>
-                <BODY pn, s0> -Suc n-> s1"
+inductive_cases evalc_elim_cases:
+  "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
+  "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
+  "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"
 
-    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
-                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
-                                         [X::=s1<Res>]"
+inductive_cases evaln_elim_cases:
+  "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
+  "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
+  "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"
+
+inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
+inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end




