Theory Procs_Stat_Vars_Stat

theory Procs_Stat_Vars_Stat imports Procs
begin

subsubsection "Static Scoping of Procedures and Variables"

type_synonym addr = nat
type_synonym venv = "vname ⇒ addr"
type_synonym store = "addr ⇒ val"
type_synonym penv = "(pname × com × venv) list"

fun venv :: "penv × venv × nat ⇒ venv" where
"venv(_,ve,_) = ve"

inductive
  big_step :: "penv × venv × nat ⇒ com × store ⇒ store ⇒ bool"
  ("_ ⊢ _ ⇒ _" [60,0,60] 55)
where
Skip:    "e ⊢ (SKIP,s) ⇒ s" |
Assign:  "(pe,ve,f) ⊢ (x ::= a,s) ⇒ s(ve x := aval a (s o ve))" |
Seq:     "⟦ e ⊢ (c⇩1,s⇩1) ⇒ s⇩2;  e ⊢ (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹
          e ⊢ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |

IfTrue:  "⟦ bval b (s ∘ venv e);  e ⊢ (c⇩1,s) ⇒ t ⟧ ⟹
         e ⊢ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b (s ∘ venv e);  e ⊢ (c⇩2,s) ⇒ t ⟧ ⟹
         e ⊢ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |

WhileFalse: "¬bval b (s ∘ venv e) ⟹ e ⊢ (WHILE b DO c,s) ⇒ s" |
WhileTrue:
  "⟦ bval b (s⇩1 ∘ venv e);  e ⊢ (c,s⇩1) ⇒ s⇩2;
     e ⊢ (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧ ⟹
   e ⊢ (WHILE b DO c, s⇩1) ⇒ s⇩3" |

Var: "(pe,ve(x:=f),f+1) ⊢ (c,s) ⇒ t  ⟹
      (pe,ve,f) ⊢ ({VAR x; c}, s) ⇒ t" |

Call1: "((p,c,ve)#pe,ve,f) ⊢ (c, s) ⇒ t  ⟹
        ((p,c,ve)#pe,ve',f) ⊢ (CALL p, s) ⇒ t" |
Call2: "⟦ p' ≠ p;  (pe,ve,f) ⊢ (CALL p, s) ⇒ t ⟧ ⟹
       ((p',c,ve')#pe,ve,f) ⊢ (CALL p, s) ⇒ t" |

Proc: "((p,cp,ve)#pe,ve,f) ⊢ (c,s) ⇒ t
      ⟹  (pe,ve,f) ⊢ ({PROC p = cp; c}, s) ⇒ t"

code_pred big_step .


values "{map t [10,11] |t.
  ([], <''x'' := 10, ''y'' := 11>, 12)
  ⊢ (test_com, <>) ⇒ t}"

end