Quelle  Procs_Stat_Vars_Stat.thy

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