1200 apply(simp_all add:Graph10) |
1200 apply(simp_all add:Graph10) |
1201 --{* 47 subgoals left *} |
1201 --{* 47 subgoals left *} |
1202 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *}) |
1202 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *}) |
1203 --{* 41 subgoals left *} |
1203 --{* 41 subgoals left *} |
1204 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, |
1204 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, |
1205 force_tac (map_simpset_local (fn ss => ss addsimps |
1205 force_tac (map_simpset (fn ss => ss addsimps |
1206 [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *}) |
1206 [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *}) |
1207 --{* 35 subgoals left *} |
1207 --{* 35 subgoals left *} |
1208 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *}) |
1208 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *}) |
1209 --{* 31 subgoals left *} |
1209 --{* 31 subgoals left *} |
1210 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) |
1210 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) |
1211 --{* 29 subgoals left *} |
1211 --{* 29 subgoals left *} |
1212 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) |
1212 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) |
1213 --{* 25 subgoals left *} |
1213 --{* 25 subgoals left *} |
1214 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, |
1214 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, |
1215 force_tac (map_simpset_local (fn ss => ss addsimps |
1215 force_tac (map_simpset (fn ss => ss addsimps |
1216 [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *}) |
1216 [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *}) |
1217 --{* 10 subgoals left *} |
1217 --{* 10 subgoals left *} |
1218 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)+ |
1218 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)+ |
1219 done |
1219 done |
1220 |
1220 |