equal
deleted
inserted
replaced
165 |
165 |
166 (******************************************************************* |
166 (******************************************************************* |
167 C h a n n e l A b s t r a c t i o n |
167 C h a n n e l A b s t r a c t i o n |
168 *******************************************************************) |
168 *******************************************************************) |
169 |
169 |
|
170 Delsplits [expand_if]; |
170 goal Correctness.thy |
171 goal Correctness.thy |
171 "is_weak_ref_map reduce ch_ioa ch_fin_ioa"; |
172 "is_weak_ref_map reduce ch_ioa ch_fin_ioa"; |
172 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
173 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
173 (* ---------------- main-part ------------------- *) |
174 (* ---------------- main-part ------------------- *) |
174 by (REPEAT (rtac allI 1)); |
175 by (REPEAT (rtac allI 1)); |
251 by (rtac imp_conj_lemma 1); |
252 by (rtac imp_conj_lemma 1); |
252 by (Action.action.induct_tac "a" 1); |
253 by (Action.action.induct_tac "a" 1); |
253 (* 7 cases *) |
254 (* 7 cases *) |
254 by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if])))); |
255 by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if])))); |
255 qed"env_unchanged"; |
256 qed"env_unchanged"; |
|
257 Addsplits [expand_if]; |
256 |
258 |
257 goal Correctness.thy "compatible srch_ioa rsch_ioa"; |
259 goal Correctness.thy "compatible srch_ioa rsch_ioa"; |
258 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1); |
260 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1); |
259 by (rtac set_ext 1); |
261 by (rtac set_ext 1); |
260 by (Action.action.induct_tac "x" 1); |
262 by (Action.action.induct_tac "x" 1); |