12 [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
12 [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
13 ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, |
13 ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, |
14 actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, |
14 actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, |
15 trans_of_def] @ asig_projections; |
15 trans_of_def] @ asig_projections; |
16 |
16 |
17 goal Abschannel.thy |
17 Goal |
18 "S_msg(m) ~: actions(srch_asig) & \ |
18 "S_msg(m) ~: actions(srch_asig) & \ |
19 \ R_msg(m) ~: actions(srch_asig) & \ |
19 \ R_msg(m) ~: actions(srch_asig) & \ |
20 \ S_pkt(pkt) : actions(srch_asig) & \ |
20 \ S_pkt(pkt) : actions(srch_asig) & \ |
21 \ R_pkt(pkt) : actions(srch_asig) & \ |
21 \ R_pkt(pkt) : actions(srch_asig) & \ |
22 \ S_ack(b) ~: actions(srch_asig) & \ |
22 \ S_ack(b) ~: actions(srch_asig) & \ |
26 \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; |
26 \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; |
27 |
27 |
28 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
28 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
29 qed"in_srch_asig"; |
29 qed"in_srch_asig"; |
30 |
30 |
31 goal Abschannel.thy |
31 Goal |
32 "S_msg(m) ~: actions(rsch_asig) & \ |
32 "S_msg(m) ~: actions(rsch_asig) & \ |
33 \ R_msg(m) ~: actions(rsch_asig) & \ |
33 \ R_msg(m) ~: actions(rsch_asig) & \ |
34 \ S_pkt(pkt) ~: actions(rsch_asig) & \ |
34 \ S_pkt(pkt) ~: actions(rsch_asig) & \ |
35 \ R_pkt(pkt) ~: actions(rsch_asig) & \ |
35 \ R_pkt(pkt) ~: actions(rsch_asig) & \ |
36 \ S_ack(b) : actions(rsch_asig) & \ |
36 \ S_ack(b) : actions(rsch_asig) & \ |
41 \ C_r_r(m) ~: actions(rsch_asig)"; |
41 \ C_r_r(m) ~: actions(rsch_asig)"; |
42 |
42 |
43 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
43 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
44 qed"in_rsch_asig"; |
44 qed"in_rsch_asig"; |
45 |
45 |
46 goal Abschannel.thy "srch_ioa = \ |
46 Goal "srch_ioa = \ |
47 \ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"; |
47 \ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"; |
48 by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def, |
48 by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def, |
49 wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1); |
49 wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1); |
50 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
50 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
51 qed"srch_ioa_thm"; |
51 qed"srch_ioa_thm"; |
52 |
52 |
53 goal Abschannel.thy "rsch_ioa = \ |
53 Goal "rsch_ioa = \ |
54 \ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"; |
54 \ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"; |
55 by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def, |
55 by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def, |
56 wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1); |
56 wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1); |
57 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
57 by (simp_tac (simpset() addsimps unfold_renaming) 1); |
58 qed"rsch_ioa_thm"; |
58 qed"rsch_ioa_thm"; |