src/HOL/IMP/Procs.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45212 e87feee00a4c
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
header "Extensions and Variations of IMP"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory Procs imports BExp begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
subsection "Procedures and Local Variables"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
     7
type_synonym pname = string
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
     8
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
datatype
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
  com = SKIP 
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
    11
      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
      | Semi   com  com          ("_;/ _"  [60, 61] 60)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
    15
      | Var    vname com        ("(1{VAR _;;/ _})")
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
    16
      | Proc   pname com com    ("(1{PROC _ = _;;/ _})")
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
    17
      | CALL   pname
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
definition "test_com =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
{VAR ''x'';;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
 ''x'' ::= N 0;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
 {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
  {PROC ''q'' = CALL ''p'';;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
   {VAR ''x'';;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
    ''x'' ::= N 5;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
    {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
     CALL ''q''; ''y'' ::= V ''x''}}}}}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
end