src/HOL/IMP/Procs.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Procs.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,27 @@
+header "Extensions and Variations of IMP"
+
+theory Procs imports BExp begin
+
+subsection "Procedures and Local Variables"
+
+datatype
+  com = SKIP 
+      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
+      | Semi   com  com          ("_;/ _"  [60, 61] 60)
+      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
+      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
+      | Var    name com         ("(1{VAR _;;/ _})")
+      | Proc   name com com     ("(1{PROC _ = _;;/ _})")
+      | CALL   name
+
+definition "test_com =
+{VAR ''x'';;
+ ''x'' ::= N 0;
+ {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
+  {PROC ''q'' = CALL ''p'';;
+   {VAR ''x'';;
+    ''x'' ::= N 5;
+    {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
+     CALL ''q''; ''y'' ::= V ''x''}}}}}"
+
+end