Quelle  Procs_Stat_Vars_Dyn.thy

theory Procs_Stat_Vars_Dyn imports Procs
begin

subsubsection "Static Scoping of Procedures, Dynamic of Variables"

type_synonym penv = "(pname × com) list"

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)" |

Call1: "(p,c)#pe ⊨ (c, s) ==> t ==> (p,c)#pe ⊨ (CALL p, s) ==> t" |
Call2: "[ p' ≠ p; pe ⊨ (CALL p, s) ==> t ] ==>
       (p',c)#pe ⊨ (CALL p, s) ==> t" |

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

code_pred big_step .

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

end