author | wenzelm |
Wed, 07 Sep 2005 20:22:39 +0200 | |
changeset 17309 | c43ed29bd197 |
parent 9517 | f58863b1406a |
permissions | -rw-r--r-- |
17309 | 1 |
(* |
3807 | 2 |
File: ProcedureInterface.ML |
17309 | 3 |
ID: $Id$ |
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
6 |
||
6255 | 7 |
Procedure interface (theorems and proofs) |
3807 | 8 |
*) |
9 |
||
10 |
Addsimps [slice_def]; |
|
6255 | 11 |
val mem_css = (claset(), simpset()); |
3807 | 12 |
|
13 |
(* ---------------------------------------------------------------------------- *) |
|
14 |
||
17309 | 15 |
val Procedure_defs = [caller_def, rtrner_def, Calling_def, |
3807 | 16 |
Call_def, Return_def, |
17309 | 17 |
PLegalCaller_def, LegalCaller_def, |
18 |
PLegalReturner_def, LegalReturner_def]; |
|
3807 | 19 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
20 |
(* Calls and returns change their subchannel *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
21 |
Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
22 |
by (auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
23 |
qed "Call_changed"; |
3807 | 24 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
25 |
Goal "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
26 |
by (auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
27 |
qed "Return_changed"; |
6255 | 28 |