162 |
162 |
163 declare split_if [split] |
163 declare split_if [split] |
164 |
164 |
165 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" |
165 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" |
166 apply (tactic {* |
166 apply (tactic {* |
167 simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", |
167 simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
168 thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", |
168 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
169 thm "channel_abstraction"]) 1 *}) |
169 @{thm channel_abstraction}]) 1 *}) |
170 done |
170 done |
171 |
171 |
172 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" |
172 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" |
173 apply (tactic {* |
173 apply (tactic {* |
174 simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", |
174 simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
175 thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", |
175 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
176 thm "channel_abstraction"]) 1 *}) |
176 @{thm channel_abstraction}]) 1 *}) |
177 done |
177 done |
178 |
178 |
179 |
179 |
180 text {* 3 thms that do not hold generally! The lucky restriction here is |
180 text {* 3 thms that do not hold generally! The lucky restriction here is |
181 the absence of internal actions. *} |
181 the absence of internal actions. *} |