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