equal
deleted
inserted
replaced
1 (* |
|
2 File: ProcedureInterface.ML |
|
3 ID: $Id$ |
|
4 Author: Stephan Merz |
|
5 Copyright: 1997 University of Munich |
|
6 |
|
7 Procedure interface (theorems and proofs) |
|
8 *) |
|
9 |
|
10 Addsimps [slice_def]; |
|
11 val mem_css = (claset(), simpset()); |
|
12 |
|
13 (* ---------------------------------------------------------------------------- *) |
|
14 |
|
15 val Procedure_defs = [caller_def, rtrner_def, Calling_def, |
|
16 Call_def, Return_def, |
|
17 PLegalCaller_def, LegalCaller_def, |
|
18 PLegalReturner_def, LegalReturner_def]; |
|
19 |
|
20 (* Calls and returns change their subchannel *) |
|
21 Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"; |
|
22 by (auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def])); |
|
23 qed "Call_changed"; |
|
24 |
|
25 Goal "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"; |
|
26 by (auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def])); |
|
27 qed "Return_changed"; |
|
28 |
|