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₁,s₁) → s₂; e ⊨ (c₂,s₂) → s₃ ] ==>
          e ⊨ (c₁;;c₂, s₁) → s₃" |

IfTrue:  "[ bval b (s ∘ venv e); e ⊨ (c₁,s) → t ] ==>
         e ⊨ (IF b THEN c₁ ELSE c₂, s) → t" |
IfFalse: "[ ¬bval b (s ∘ venv e); e ⊨ (c₂,s) → t ] ==>
         e ⊨ (IF b THEN c₁ ELSE c₂, s) → t" |

WhileFalse: "¬bval b (s ∘ venv e) ==> e ⊨ (WHILE b DO c,s) → s" |
WhileTrue:
  "[ bval b (s₁ ∘ venv e); e ⊨ (c,s₁) → s₂;
     e ⊨ (WHILE b DO c, s₂) → s₃ ] ==>
   e ⊨ (WHILE b DO c, s₁) → s₃" |

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