|
1 (* Title: HOL/IOA/NTP/Abschannel.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Derived rules |
|
7 *) |
|
8 |
|
9 open Abschannel; |
|
10 |
|
11 val unfold_renaming = |
|
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, asig_of_def, |
|
14 actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, |
|
15 trans_of_def] @ asig_projections; |
|
16 |
|
17 goal Abschannel.thy |
|
18 "S_msg(m) ~: actions(srch_asig) & \ |
|
19 \ R_msg(m) ~: actions(srch_asig) & \ |
|
20 \ S_pkt(pkt) : actions(srch_asig) & \ |
|
21 \ R_pkt(pkt) : actions(srch_asig) & \ |
|
22 \ S_ack(b) ~: actions(srch_asig) & \ |
|
23 \ R_ack(b) ~: actions(srch_asig) & \ |
|
24 \ C_m_s ~: actions(srch_asig) & \ |
|
25 \ C_m_r ~: actions(srch_asig) & \ |
|
26 \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; |
|
27 |
|
28 by(simp_tac (!simpset addsimps unfold_renaming) 1); |
|
29 qed"in_srch_asig"; |
|
30 |
|
31 goal Abschannel.thy |
|
32 "S_msg(m) ~: actions(rsch_asig) & \ |
|
33 \ R_msg(m) ~: actions(rsch_asig) & \ |
|
34 \ S_pkt(pkt) ~: actions(rsch_asig) & \ |
|
35 \ R_pkt(pkt) ~: actions(rsch_asig) & \ |
|
36 \ S_ack(b) : actions(rsch_asig) & \ |
|
37 \ R_ack(b) : actions(rsch_asig) & \ |
|
38 \ C_m_s ~: actions(rsch_asig) & \ |
|
39 \ C_m_r ~: actions(rsch_asig) & \ |
|
40 \ C_r_s ~: actions(rsch_asig) & \ |
|
41 \ C_r_r(m) ~: actions(rsch_asig)"; |
|
42 |
|
43 by(simp_tac (!simpset addsimps unfold_renaming) 1); |
|
44 qed"in_rsch_asig"; |
|
45 |
|
46 goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)"; |
|
47 by(simp_tac (!simpset addsimps unfold_renaming) 1); |
|
48 qed"srch_ioa_thm"; |
|
49 |
|
50 goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)"; |
|
51 by(simp_tac (!simpset addsimps unfold_renaming) 1); |
|
52 qed"rsch_ioa_thm"; |
|
53 |