author | wenzelm |
Fri, 26 Jun 2015 11:44:22 +0200 | |
changeset 60587 | 0318b43ee95c |
parent 58889 | 5b7a9633cfa8 |
child 60588 | 750c533459b1 |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Memory/ProcedureInterface.thy |
2 |
Author: Stephan Merz, University of Munich |
|
21624 | 3 |
*) |
3807 | 4 |
|
58889 | 5 |
section {* Procedure interface for RPC-Memory components *} |
3807 | 6 |
|
17309 | 7 |
theory ProcedureInterface |
26351 | 8 |
imports "../TLA" RPCMemoryParams |
17309 | 9 |
begin |
3807 | 10 |
|
42018 | 11 |
typedecl ('a,'r) chan |
3807 | 12 |
(* type of channels with argument type 'a and return type 'r. |
17309 | 13 |
we model a channel as an array of variables (of type chan) |
14 |
rather than a single array-valued variable because the |
|
3807 | 15 |
notation gets a little simpler. |
16 |
*) |
|
42018 | 17 |
type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun" |
3807 | 18 |
|
19 |
consts |
|
20 |
(* data-level functions *) |
|
17309 | 21 |
cbit :: "('a,'r) chan => bit" |
22 |
rbit :: "('a,'r) chan => bit" |
|
3807 | 23 |
arg :: "('a,'r) chan => 'a" |
24 |
res :: "('a,'r) chan => 'r" |
|
25 |
||
26 |
(* state functions *) |
|
17309 | 27 |
caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun" |
3807 | 28 |
rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun" |
29 |
||
30 |
(* state predicates *) |
|
31 |
Calling :: "('a,'r) channel => PrIds => stpred" |
|
32 |
||
33 |
(* actions *) |
|
6255 | 34 |
ACall :: "('a,'r) channel => PrIds => 'a stfun => action" |
35 |
AReturn :: "('a,'r) channel => PrIds => 'r stfun => action" |
|
3807 | 36 |
|
37 |
(* temporal formulas *) |
|
38 |
PLegalCaller :: "('a,'r) channel => PrIds => temporal" |
|
39 |
LegalCaller :: "('a,'r) channel => temporal" |
|
40 |
PLegalReturner :: "('a,'r) channel => PrIds => temporal" |
|
41 |
LegalReturner :: "('a,'r) channel => temporal" |
|
42 |
||
6255 | 43 |
(* slice through array-valued state function *) |
44 |
slice :: "('a => 'b) stfun => 'a => 'b stfun" |
|
45 |
||
46 |
syntax |
|
17309 | 47 |
"_slice" :: "[lift, 'a] => lift" ("(_!_)" [70,70] 70) |
6255 | 48 |
|
17309 | 49 |
"_Call" :: "['a, 'b, lift] => lift" ("(Call _ _ _)" [90,90,90] 90) |
50 |
"_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90) |
|
3807 | 51 |
|
6255 | 52 |
translations |
35068 | 53 |
"_slice" == "CONST slice" |
6255 | 54 |
|
35068 | 55 |
"_Call" == "CONST ACall" |
56 |
"_Return" == "CONST AReturn" |
|
6255 | 57 |
|
17309 | 58 |
defs |
59 |
slice_def: "(PRED (x!i)) s == x s i" |
|
3807 | 60 |
|
60587 | 61 |
caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))" |
62 |
rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))" |
|
3807 | 63 |
|
60587 | 64 |
Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >" |
65 |
Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p |
|
66 |
& (cbit<ch!p>$ \<noteq> $rbit<ch!p>) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
67 |
& (arg<ch!p>$ = $v)" |
17309 | 68 |
Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
69 |
& (rbit<ch!p>$ = $cbit<ch!p>) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
70 |
& (res<ch!p>$ = $v)" |
17309 | 71 |
PLegalCaller_def: "PLegalCaller ch p == TEMP |
60587 | 72 |
Init(\<not> Calling ch p) |
73 |
& \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)" |
|
74 |
LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)" |
|
17309 | 75 |
PLegalReturner_def: "PLegalReturner ch p == TEMP |
60587 | 76 |
\<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)" |
77 |
LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)" |
|
17309 | 78 |
|
21624 | 79 |
declare slice_def [simp] |
80 |
||
81 |
lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def |
|
82 |
PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def |
|
83 |
||
84 |
(* Calls and returns change their subchannel *) |
|
85 |
lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)" |
|
86 |
by (auto simp: angle_def Call_def caller_def Calling_def) |
|
87 |
||
88 |
lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)" |
|
89 |
by (auto simp: angle_def Return_def rtrner_def Calling_def) |
|
3807 | 90 |
|
91 |
end |