|
1 local |
|
2 val SS = action_ss addsimps |
|
3 (Channels.srch_asig_def :: |
|
4 Channels.rsch_asig_def :: |
|
5 actions_def :: asig_projections_def :: set_lemmas) |
|
6 in |
|
7 val _ = goal Channels.thy |
|
8 "S_msg(m) ~: actions(srch_asig) & \ |
|
9 \ R_msg(m) ~: actions(srch_asig) & \ |
|
10 \ S_pkt(pkt) : actions(srch_asig) & \ |
|
11 \ R_pkt(pkt) : actions(srch_asig) & \ |
|
12 \ S_ack(b) ~: actions(srch_asig) & \ |
|
13 \ R_ack(b) ~: actions(srch_asig) & \ |
|
14 \ C_m_s ~: actions(srch_asig) & \ |
|
15 \ C_m_r ~: actions(srch_asig) & \ |
|
16 \ C_r_s ~: actions(srch_asig) & \ |
|
17 \ C_r_r(m) ~: actions(srch_asig)"; |
|
18 |
|
19 val _ = by (simp_tac SS 1); |
|
20 |
|
21 val in_srch_asig = result(); |
|
22 |
|
23 val _ = goal Channels.thy |
|
24 "S_msg(m) ~: actions(rsch_asig) & \ |
|
25 \ R_msg(m) ~: actions(rsch_asig) & \ |
|
26 \ S_pkt(pkt) ~: actions(rsch_asig) & \ |
|
27 \ R_pkt(pkt) ~: actions(rsch_asig) & \ |
|
28 \ S_ack(b) : actions(rsch_asig) & \ |
|
29 \ R_ack(b) : actions(rsch_asig) & \ |
|
30 \ C_m_s ~: actions(rsch_asig) & \ |
|
31 \ C_m_r ~: actions(rsch_asig) & \ |
|
32 \ C_r_s ~: actions(rsch_asig) & \ |
|
33 \ C_r_r(m) ~: actions(rsch_asig)"; |
|
34 |
|
35 val _ = by (simp_tac SS 1); |
|
36 |
|
37 val in_rsch_asig = result(); |
|
38 |
|
39 end; |