56 "_Return" == "CONST AReturn" |
56 "_Return" == "CONST AReturn" |
57 |
57 |
58 defs |
58 defs |
59 slice_def: "(PRED (x!i)) s == x s i" |
59 slice_def: "(PRED (x!i)) s == x s i" |
60 |
60 |
61 caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))" |
61 caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))" |
62 rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" |
62 rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))" |
63 |
63 |
64 Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" |
64 Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >" |
65 Call_def: "(ACT Call ch p v) == ACT ~ $Calling ch p |
65 Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p |
66 & (cbit<ch!p>$ ~= $rbit<ch!p>) |
66 & (cbit<ch!p>$ \<noteq> $rbit<ch!p>) |
67 & (arg<ch!p>$ = $v)" |
67 & (arg<ch!p>$ = $v)" |
68 Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
68 Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
69 & (rbit<ch!p>$ = $cbit<ch!p>) |
69 & (rbit<ch!p>$ = $cbit<ch!p>) |
70 & (res<ch!p>$ = $v)" |
70 & (res<ch!p>$ = $v)" |
71 PLegalCaller_def: "PLegalCaller ch p == TEMP |
71 PLegalCaller_def: "PLegalCaller ch p == TEMP |
72 Init(~ Calling ch p) |
72 Init(\<not> Calling ch p) |
73 & [][ ? a. Call ch p a ]_((caller ch)!p)" |
73 & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)" |
74 LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
74 LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)" |
75 PLegalReturner_def: "PLegalReturner ch p == TEMP |
75 PLegalReturner_def: "PLegalReturner ch p == TEMP |
76 [][ ? v. Return ch p v ]_((rtrner ch)!p)" |
76 \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)" |
77 LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
77 LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)" |
78 |
78 |
79 declare slice_def [simp] |
79 declare slice_def [simp] |
80 |
80 |
81 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def |
81 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def |
82 PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def |
82 PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def |