src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
changeset 44923 b80108b346a9
parent 44177 b4b5cbca2519
child 45212 e87feee00a4c
equal deleted inserted replaced
44911:884d27ede438 44923:b80108b346a9
    31 
    31 
    32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
    32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
    33 
    33 
    34 code_pred big_step .
    34 code_pred big_step .
    35 
    35 
       
    36 values "{map t [''x'', ''y'', ''z''] |t. 
       
    37             [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
    36 
    38 
    37 (* FIXME: example state syntax *)
    39 values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
    38 values "{map t [''x'', ''y'', ''z''] |t. 
       
    39             [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
       
    40 
       
    41 values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}"
       
    42 
    40 
    43 end
    41 end