equal
deleted
inserted
replaced
1 (* |
1 (* |
2 File: ProcedureInterface.thy |
2 File: ProcedureInterface.thy |
3 ID: $Id$ |
3 ID: $Id$ |
4 Author: Stephan Merz |
4 Author: Stephan Merz |
5 Copyright: 1997 University of Munich |
5 Copyright: 1997 University of Munich |
|
6 *) |
6 |
7 |
7 Theory Name: ProcedureInterface |
8 header {* Procedure interface for RPC-Memory components *} |
8 Logic Image: TLA |
|
9 |
|
10 Procedure interface for RPC-Memory components. |
|
11 *) |
|
12 |
9 |
13 theory ProcedureInterface |
10 theory ProcedureInterface |
14 imports TLA RPCMemoryParams |
11 imports TLA RPCMemoryParams |
15 begin |
12 begin |
16 |
13 |
82 LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
79 LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
83 PLegalReturner_def: "PLegalReturner ch p == TEMP |
80 PLegalReturner_def: "PLegalReturner ch p == TEMP |
84 [][ ? v. Return ch p v ]_((rtrner ch)!p)" |
81 [][ ? v. Return ch p v ]_((rtrner ch)!p)" |
85 LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
82 LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
86 |
83 |
87 ML {* use_legacy_bindings (the_context ()) *} |
84 declare slice_def [simp] |
|
85 |
|
86 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def |
|
87 PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def |
|
88 |
|
89 (* Calls and returns change their subchannel *) |
|
90 lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)" |
|
91 by (auto simp: angle_def Call_def caller_def Calling_def) |
|
92 |
|
93 lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)" |
|
94 by (auto simp: angle_def Return_def rtrner_def Calling_def) |
88 |
95 |
89 end |
96 end |