equal
deleted
inserted
replaced
182 "is_weak_pmap reduce ch_ioa ch_fin_ioa"; |
182 "is_weak_pmap reduce ch_ioa ch_fin_ioa"; |
183 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
183 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
184 by (rtac conjI 1); |
184 by (rtac conjI 1); |
185 (* -------------- start states ----------------- *) |
185 (* -------------- start states ----------------- *) |
186 by (Simp_tac 1); |
186 by (Simp_tac 1); |
187 br ballI 1; |
187 by (rtac ballI 1); |
188 by (Asm_full_simp_tac 1); |
188 by (Asm_full_simp_tac 1); |
189 (* ---------------- main-part ------------------- *) |
189 (* ---------------- main-part ------------------- *) |
190 by (REPEAT (rtac allI 1)); |
190 by (REPEAT (rtac allI 1)); |
191 by (rtac imp_conj_lemma 1); |
191 by (rtac imp_conj_lemma 1); |
192 by (act.induct_tac "a" 1); |
192 by (act.induct_tac "a" 1); |
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); |
230 by (rtac conjI 1); |
231 (* start states *) |
231 (* start states *) |
232 br ballI 1; |
232 by (rtac ballI 1); |
233 by (Simp_tac 1); |
233 by (Simp_tac 1); |
234 (* main-part *) |
234 (* main-part *) |
235 by (REPEAT (rtac allI 1)); |
235 by (REPEAT (rtac allI 1)); |
236 by (rtac imp_conj_lemma 1); |
236 by (rtac imp_conj_lemma 1); |
237 by (Action.action.induct_tac "a" 1); |
237 by (Action.action.induct_tac "a" 1); |
243 goal Correctness.thy |
243 goal Correctness.thy |
244 "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; |
244 "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; |
245 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
245 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
246 by (rtac conjI 1); |
246 by (rtac conjI 1); |
247 (* start states *) |
247 (* start states *) |
248 br ballI 1; |
248 by (rtac ballI 1); |
249 by (Simp_tac 1); |
249 by (Simp_tac 1); |
250 (* main-part *) |
250 (* main-part *) |
251 by (REPEAT (rtac allI 1)); |
251 by (REPEAT (rtac allI 1)); |
252 by (rtac imp_conj_lemma 1); |
252 by (rtac imp_conj_lemma 1); |
253 by (Action.action.induct_tac "a" 1); |
253 by (Action.action.induct_tac "a" 1); |
258 goal Correctness.thy |
258 goal Correctness.thy |
259 "is_weak_pmap (%id.id) env_ioa env_ioa"; |
259 "is_weak_pmap (%id.id) env_ioa env_ioa"; |
260 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
260 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); |
261 by (rtac conjI 1); |
261 by (rtac conjI 1); |
262 (* start states *) |
262 (* start states *) |
263 br ballI 1; |
263 by (rtac ballI 1); |
264 by (Simp_tac 1); |
264 by (Simp_tac 1); |
265 (* main-part *) |
265 (* main-part *) |
266 by (REPEAT (rtac allI 1)); |
266 by (REPEAT (rtac allI 1)); |
267 by (rtac imp_conj_lemma 1); |
267 by (rtac imp_conj_lemma 1); |
268 by (Action.action.induct_tac "a" 1); |
268 by (Action.action.induct_tac "a" 1); |