26 2. enabledness of calls and returns |
26 2. enabledness of calls and returns |
27 NB: action_simp_tac is significantly faster than auto_tac |
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. base_var ((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 "Return_enabled" ProcedureInterface.thy |
35 qed_goal "Return_enabled" ProcedureInterface.thy |
36 "!!p. base_var ((rtrner ch)@p) ==> $(Calling ch p) .-> $(Enabled (Return ch p (#v)))" |
36 "!!p. base_var ((rtrner ch)@p) ==> $(Calling ch p) .-> $(Enabled (Return ch p (#v)))" |
37 (fn _ => [action_simp_tac (!simpset addsimps [rtrner_def, Return_def]) |
37 (fn _ => [action_simp_tac (simpset() addsimps [rtrner_def, Return_def]) |
38 [] [base_enabled,Pair_inject] 1 |
38 [] [base_enabled,Pair_inject] 1 |
39 ]); |
39 ]); |
40 |
40 |
41 *) |
41 *) |
42 |
42 |
43 (* Calls and returns change their subchannel *) |
43 (* Calls and returns change their subchannel *) |
44 qed_goal "Call_changed" ProcedureInterface.thy |
44 qed_goal "Call_changed" ProcedureInterface.thy |
45 "Call ch p v .-> <Call ch p v>_((caller ch)@p)" |
45 "Call ch p v .-> <Call ch p v>_((caller ch)@p)" |
46 (fn _ => [auto_tac (!claset, |
46 (fn _ => [auto_tac (claset(), |
47 !simpset addsimps [angle_def,Call_def,caller_def, |
47 simpset() addsimps [angle_def,Call_def,caller_def, |
48 action_rewrite Calling_def]) |
48 action_rewrite Calling_def]) |
49 ]); |
49 ]); |
50 |
50 |
51 qed_goal "Return_changed" ProcedureInterface.thy |
51 qed_goal "Return_changed" ProcedureInterface.thy |
52 "Return ch p v .-> <Return ch p v>_((rtrner ch)@p)" |
52 "Return ch p v .-> <Return ch p v>_((rtrner ch)@p)" |
53 (fn _ => [auto_tac (!claset, |
53 (fn _ => [auto_tac (claset(), |
54 !simpset addsimps [angle_def,Return_def,rtrner_def, |
54 simpset() addsimps [angle_def,Return_def,rtrner_def, |
55 action_rewrite Calling_def]) |
55 action_rewrite Calling_def]) |
56 ]); |
56 ]); |
57 |
57 |
58 (* For convenience, generate elimination rules. |
58 (* For convenience, generate elimination rules. |
59 These rules loop if angle_def is active! *) |
59 These rules loop if angle_def is active! *) |