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