92 C_m_s => None | |
92 C_m_s => None | |
93 C_m_r => None | |
93 C_m_r => None | |
94 C_r_s => None | |
94 C_r_s => None | |
95 C_r_r(m) => None" |
95 C_r_r(m) => None" |
96 |
96 |
97 ML {* use_legacy_bindings (the_context ()) *} |
97 lemmas unfold_renaming = |
|
98 srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def |
|
99 ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def |
|
100 actions_def srch_trans_def rsch_trans_def ch_trans_def starts_of_def |
|
101 trans_of_def asig_projections |
|
102 |
|
103 lemma in_srch_asig: |
|
104 "S_msg(m) ~: actions(srch_asig) & |
|
105 R_msg(m) ~: actions(srch_asig) & |
|
106 S_pkt(pkt) : actions(srch_asig) & |
|
107 R_pkt(pkt) : actions(srch_asig) & |
|
108 S_ack(b) ~: actions(srch_asig) & |
|
109 R_ack(b) ~: actions(srch_asig) & |
|
110 C_m_s ~: actions(srch_asig) & |
|
111 C_m_r ~: actions(srch_asig) & |
|
112 C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)" |
|
113 |
|
114 by (simp add: unfold_renaming) |
|
115 |
|
116 lemma in_rsch_asig: |
|
117 "S_msg(m) ~: actions(rsch_asig) & |
|
118 R_msg(m) ~: actions(rsch_asig) & |
|
119 S_pkt(pkt) ~: actions(rsch_asig) & |
|
120 R_pkt(pkt) ~: actions(rsch_asig) & |
|
121 S_ack(b) : actions(rsch_asig) & |
|
122 R_ack(b) : actions(rsch_asig) & |
|
123 C_m_s ~: actions(rsch_asig) & |
|
124 C_m_r ~: actions(rsch_asig) & |
|
125 C_r_s ~: actions(rsch_asig) & |
|
126 C_r_r(m) ~: actions(rsch_asig)" |
|
127 by (simp add: unfold_renaming) |
|
128 |
|
129 lemma srch_ioa_thm: "srch_ioa = |
|
130 (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)" |
|
131 apply (simp (no_asm) add: srch_asig_def srch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def srch_wfair_def srch_sfair_def) |
|
132 apply (simp (no_asm) add: unfold_renaming) |
|
133 done |
|
134 |
|
135 lemma rsch_ioa_thm: "rsch_ioa = |
|
136 (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)" |
|
137 apply (simp (no_asm) add: rsch_asig_def rsch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def rsch_wfair_def rsch_sfair_def) |
|
138 apply (simp (no_asm) add: unfold_renaming) |
|
139 done |
98 |
140 |
99 end |
141 end |