src/HOL/IMP/Procs.thy

stronger fact normalization

header "Extensions and Variations of IMP"

theory Procs imports BExp begin

subsection "Procedures and Local Variables"

type_synonym pname = string

datatype
  com = SKIP 
      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
      | Seq    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    vname com        ("(1{VAR _;/ _})")
      | Proc   pname com com    ("(1{PROC _ = _;/ _})")
      | CALL   pname

definition "test_com =
{VAR ''x'';
 {PROC ''p'' = ''x'' ::= N 1;
  {PROC ''q'' = CALL ''p'';
   {VAR ''x'';
    ''x'' ::= N 2;;
    {PROC ''p'' = ''x'' ::= N 3;
     CALL ''q'';; ''y'' ::= V ''x''}}}}}"

end