1198 apply(tactic {* TRYALL (etac disjE) *}) |
1198 apply(tactic {* TRYALL (etac disjE) *}) |
1199 apply(tactic {* TRYALL (etac disjE) *}) |
1199 apply(tactic {* TRYALL (etac disjE) *}) |
1200 --{* 72 subgoals left *} |
1200 --{* 72 subgoals left *} |
1201 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
1201 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
1202 --{* 35 subgoals left *} |
1202 --{* 35 subgoals left *} |
1203 apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *}) |
1203 apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *}) |
1204 --{* 28 subgoals left *} |
1204 --{* 28 subgoals left *} |
1205 apply(tactic {* TRYALL (etac conjE) *}) |
1205 apply(tactic {* TRYALL (etac conjE) *}) |
1206 apply(tactic {* TRYALL (etac disjE) *}) |
1206 apply(tactic {* TRYALL (etac disjE) *}) |
1207 --{* 34 subgoals left *} |
1207 --{* 34 subgoals left *} |
1208 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) |
1208 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) |
1209 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) |
1209 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) |
1210 apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *}) |
1210 apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *}) |
1211 apply(simp_all add:Graph10) |
1211 apply(simp_all add:Graph10) |
1212 --{* 47 subgoals left *} |
1212 --{* 47 subgoals left *} |
1213 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *}) |
1213 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) |
1214 --{* 41 subgoals left *} |
1214 --{* 41 subgoals left *} |
1215 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *}) |
1215 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) |
1216 --{* 35 subgoals left *} |
1216 --{* 35 subgoals left *} |
1217 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *}) |
1217 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *}) |
1218 --{* 31 subgoals left *} |
1218 --{* 31 subgoals left *} |
1219 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *}) |
1219 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) |
1220 --{* 29 subgoals left *} |
1220 --{* 29 subgoals left *} |
1221 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *}) |
1221 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) |
1222 --{* 25 subgoals left *} |
1222 --{* 25 subgoals left *} |
1223 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *}) |
1223 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) |
1224 --{* 10 subgoals left *} |
1224 --{* 10 subgoals left *} |
1225 apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+ |
1225 apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+ |
1226 done |
1226 done |
1227 |
1227 |
1228 subsubsection {* Interference freedom Mutator-Collector *} |
1228 subsubsection {* Interference freedom Mutator-Collector *} |