theory Procs_Stat_Vars_Stat imports Util Procs begin subsubsection "Static Scoping of Procedures and Variables" types addr = nat venv = "name \ addr" store = "addr \ nat" penv = "(name \ 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))" | Semi: "\ e \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; e \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ e \ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b (s \ venv e); e \ (c\<^isub>1,s) \ t \ \ e \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \ t" | IfFalse: "\ \bval b (s \ venv e); e \ (c\<^isub>2,s) \ t \ \ e \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \ t" | WhileFalse: "\bval b (s \ venv e) \ e \ (WHILE b DO c,s) \ s" | WhileTrue: "\ bval b (s\<^isub>1 \ venv e); e \ (c,s\<^isub>1) \ s\<^isub>2; e \ (WHILE b DO c, s\<^isub>2) \ s\<^isub>3 \ \ e \ (WHILE b DO c, s\<^isub>1) \ s\<^isub>3" | Var: "(pe,ve(x:=f),f+1) \ (c,s) \ t \ (pe,ve,f) \ ({VAR x;; c}, s) \ t(f := s f)" | 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 . inductive exec where "([], \n. n, 0) \ (c,nth ns) \ s \ exec c ns (list s (length ns))" code_pred exec . values "{ns. exec (CALL 0) [42,43] ns}" values "{ns. exec test_com [0,0] ns}" end