Quelle  Procs_Dyn_Vars_Dyn.thy

theory Procs_Dyn_Vars_Dyn imports Procs
begin

subsubsection "Dynamic Scoping of Procedures and Variables"

type_synonym penv = "pname ==> com"

inductive
  big_step :: "penv ==> com × state ==> state ==> bool" (‹_ ⊨ _ ==> _› [60,0,60] 55)
where
Skip:    "pe ⊨ (SKIP,s) ==> s" |
Assign:  "pe ⊨ (x ::= a,s) ==> s(x := aval a s)" |
Seq:     "[ pe ⊨ (c🪙1,s🪙1) ==> s🪙2; pe ⊨ (c🪙2,s🪙2) ==> s🪙3 ] ==>
          pe ⊨ (c🪙1;;c🪙2, s🪙1) ==> s🪙3" |

IfTrue:  "[ bval b s; pe ⊨ (c🪙1,s) ==> t ] ==>
         pe ⊨ (IF b THEN c🪙1 ELSE c🪙2, s) ==> t" |
IfFalse: "[ ¬bval b s; pe ⊨ (c🪙2,s) ==> t ] ==>
         pe ⊨ (IF b THEN c🪙1 ELSE c🪙2, s) ==> t" |

WhileFalse: "¬bval b s ==> pe ⊨ (WHILE b DO c,s) ==> s" |
WhileTrue:
  "[ bval b s🪙1; pe ⊨ (c,s🪙1) ==> s🪙2; pe ⊨ (WHILE b DO c, s🪙2) ==> s🪙3 ] ==>
   pe ⊨ (WHILE b DO c, s🪙1) ==> s🪙3" |

Var: "pe ⊨ (c,s) ==> t ==> pe ⊨ ({VAR x; c}, s) ==> t(x := s x)" |

Call: "pe ⊨ (pe p, s) ==> t ==> pe ⊨ (CALL p, s) ==> t" |

Proc: "pe(p := cp) ⊨ (c,s) ==> t ==> pe ⊨ ({PROC p = cp; c}, s) ==> t"

code_pred big_step .

values "{map t [''x'',''y''] |t. (λp. SKIP) ⊨ (test_com, <>) ==> t}"

end