# Theory Procs_Stat_Vars_Stat

theory Procs_Stat_Vars_Stat imports Procs
begin

subsubsection "Static Scoping of Procedures and Variables"

type_synonym penv =

fun venv ::  where
"venv(_,ve,_) = ve"

inductive
big_step ::
("_  _  _" [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  (c1,s1)  s2;  e  (c2,s2)  s3
e  (c1;;c2, s1)  s3" |

IfTrue:  " bval b (s  venv e);  e  (c1,s)  t
e  (IF b THEN c1 ELSE c2, s)  t" |
IfFalse: " ¬bval b (s  venv e);  e  (c2,s)  t
e  (IF b THEN c1 ELSE c2, s)  t" |

WhileFalse: "¬bval b (s  venv e)  e  (WHILE b DO c,s)  s" |
WhileTrue:
" bval b (s1  venv e);  e  (c,s1)  s2;
e  (WHILE b DO c, s2)  s3
e  (WHILE b DO c, s1)  s3" |

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  .

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

end