equal
deleted
inserted
replaced
225 (* 3 thms that do not hold generally! The lucky restriction here is |
225 (* 3 thms that do not hold generally! The lucky restriction here is |
226 the absence of internal actions. *) |
226 the absence of internal actions. *) |
227 goal Correctness.thy |
227 goal Correctness.thy |
228 "is_weak_pmap (%id.id) sender_ioa sender_ioa"; |
228 "is_weak_pmap (%id.id) sender_ioa sender_ioa"; |
229 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
229 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
|
230 by (rtac conjI 1); |
|
231 (* start states *) |
|
232 by (fast_tac set_cs 1); |
230 (* main-part *) |
233 (* main-part *) |
231 by (REPEAT (rtac allI 1)); |
234 by (REPEAT (rtac allI 1)); |
232 by (rtac imp_conj_lemma 1); |
235 by (rtac imp_conj_lemma 1); |
233 by (Action.action.induct_tac "a" 1); |
236 by (Action.action.induct_tac "a" 1); |
234 (* 7 cases *) |
237 (* 7 cases *) |
237 |
240 |
238 (* 2 copies of before *) |
241 (* 2 copies of before *) |
239 goal Correctness.thy |
242 goal Correctness.thy |
240 "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; |
243 "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; |
241 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
244 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
|
245 by (rtac conjI 1); |
|
246 (* start states *) |
|
247 by (fast_tac set_cs 1); |
242 (* main-part *) |
248 (* main-part *) |
243 by (REPEAT (rtac allI 1)); |
249 by (REPEAT (rtac allI 1)); |
244 by (rtac imp_conj_lemma 1); |
250 by (rtac imp_conj_lemma 1); |
245 by (Action.action.induct_tac "a" 1); |
251 by (Action.action.induct_tac "a" 1); |
246 (* 7 cases *) |
252 (* 7 cases *) |
248 qed"receiver_unchanged"; |
254 qed"receiver_unchanged"; |
249 |
255 |
250 goal Correctness.thy |
256 goal Correctness.thy |
251 "is_weak_pmap (%id.id) env_ioa env_ioa"; |
257 "is_weak_pmap (%id.id) env_ioa env_ioa"; |
252 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
258 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
|
259 by (rtac conjI 1); |
|
260 (* start states *) |
|
261 by (fast_tac set_cs 1); |
253 (* main-part *) |
262 (* main-part *) |
254 by (REPEAT (rtac allI 1)); |
263 by (REPEAT (rtac allI 1)); |
255 by (rtac imp_conj_lemma 1); |
264 by (rtac imp_conj_lemma 1); |
256 by (Action.action.induct_tac "a" 1); |
265 by (Action.action.induct_tac "a" 1); |
257 (* 7 cases *) |
266 (* 7 cases *) |