1 (* |
1 (* |
2 File: ProcedureInterface.ML |
2 File: ProcedureInterface.ML |
3 Author: Stephan Merz |
3 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
4 Copyright: 1997 University of Munich |
5 |
5 |
6 Procedure interface (ML file) |
6 Procedure interface (theorems and proofs) |
7 *) |
7 *) |
8 |
8 |
9 Addsimps [slice_def]; |
9 Addsimps [slice_def]; |
|
10 val mem_css = (claset(), simpset()); |
10 |
11 |
11 (* ---------------------------------------------------------------------------- *) |
12 (* ---------------------------------------------------------------------------- *) |
12 |
13 |
13 val Procedure_defs = [caller_def, rtrner_def, action_rewrite Calling_def, |
14 val Procedure_defs = [caller_def, rtrner_def, Calling_def, |
14 Call_def, Return_def, |
15 Call_def, Return_def, |
15 PLegalCaller_def, LegalCaller_def, |
16 PLegalCaller_def, LegalCaller_def, |
16 PLegalReturner_def, LegalReturner_def]; |
17 PLegalReturner_def, LegalReturner_def]; |
17 |
18 |
18 (* sample theorems (not used in the proof): |
19 (* sample theorems (not used in the proof): |
19 1. calls and returns are mutually exclusive |
20 1. calls and returns are mutually exclusive |
20 |
21 |
21 qed_goal "CallReturnMutex" ProcedureInterface.thy |
22 qed_goal "CallNotReturn" ProcedureInterface.thy |
22 "Call ch p v .-> .~ Return ch p w" |
23 "|- Call ch p v --> ~ Return ch p w" |
23 (fn prems => [ auto_tac (action_css addsimps2 [Call_def,Return_def]) ]); |
24 (fn prems => [ auto_tac (temp_css addsimps2 [Call_def,Return_def]) ]); |
24 |
25 |
25 |
26 |
26 2. enabledness of calls and returns |
27 2. enabledness of calls and returns |
27 NB: action_simp_tac is significantly faster than auto_tac |
|
28 |
28 |
29 qed_goal "Call_enabled" ProcedureInterface.thy |
29 qed_goal "Call_enabled" ProcedureInterface.thy |
30 "!!p. base_var ((caller ch)@p) ==> (.~ $(Calling ch p) .-> $(Enabled (Call ch p (#v))))" |
30 "!!p. basevars ((caller ch)!p) ==> |- ~ Calling ch p --> Enabled (Call ch p v)" |
31 (fn _ => [action_simp_tac (simpset() addsimps [caller_def, Call_def]) |
31 (fn _ => [action_simp_tac (simpset() addsimps [caller_def, Call_def]) |
32 [] [base_enabled,Pair_inject] 1 |
32 [] [base_enabled,Pair_inject] 1 |
33 ]); |
33 ]); |
34 |
34 |
|
35 qed_goal "Call_enabled_rew" ProcedureInterface.thy |
|
36 "basevars ((caller ch)!p) ==> |- Enabled (Call ch p v) = (~Calling ch p)" |
|
37 (fn [prem] => [auto_tac (mem_css addsimps2 [Call_def]), |
|
38 force_tac (mem_css addsimps2 [enabled_def]) 1, |
|
39 enabled_tac prem 1, |
|
40 action_simp_tac (simpset() addsimps [caller_def]) [] [Pair_inject] 1 |
|
41 ]); |
|
42 |
35 qed_goal "Return_enabled" ProcedureInterface.thy |
43 qed_goal "Return_enabled" ProcedureInterface.thy |
36 "!!p. base_var ((rtrner ch)@p) ==> $(Calling ch p) .-> $(Enabled (Return ch p (#v)))" |
44 "!!p. basevars ((rtrner ch)!p) ==> |- Calling ch p --> Enabled (Return ch p v)" |
37 (fn _ => [action_simp_tac (simpset() addsimps [rtrner_def, Return_def]) |
45 (fn _ => [action_simp_tac (simpset() addsimps [rtrner_def, Return_def]) |
38 [] [base_enabled,Pair_inject] 1 |
46 [] [base_enabled,Pair_inject] 1 |
39 ]); |
47 ]); |
40 |
48 |
41 *) |
49 *) |
42 |
50 |
43 (* Calls and returns change their subchannel *) |
51 (* Calls and returns change their subchannel *) |
44 qed_goal "Call_changed" ProcedureInterface.thy |
52 qed_goal "Call_changed" ProcedureInterface.thy |
45 "Call ch p v .-> <Call ch p v>_((caller ch)@p)" |
53 "|- Call ch p v --> <Call ch p v>_((caller ch)!p)" |
46 (fn _ => [auto_tac (claset(), |
54 (fn _ => [ auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def]) ]); |
47 simpset() addsimps [angle_def,Call_def,caller_def, |
|
48 action_rewrite Calling_def]) |
|
49 ]); |
|
50 |
55 |
51 qed_goal "Return_changed" ProcedureInterface.thy |
56 qed_goal "Return_changed" ProcedureInterface.thy |
52 "Return ch p v .-> <Return ch p v>_((rtrner ch)@p)" |
57 "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)" |
53 (fn _ => [auto_tac (claset(), |
58 (fn _ => [ auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def]) ]); |
54 simpset() addsimps [angle_def,Return_def,rtrner_def, |
|
55 action_rewrite Calling_def]) |
|
56 ]); |
|
57 |
59 |
58 (* For convenience, generate elimination rules. |
|
59 These rules loop if angle_def is active! *) |
|
60 bind_thm("Call_changedE", action_impE Call_changed); |
|
61 bind_thm("Return_changedE", action_impE Return_changed); |
|
62 |
60 |