790 apply(unfold modules collector_defs mutator_defs) |
790 apply(unfold modules collector_defs mutator_defs) |
791 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
791 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
792 --{* 32 subgoals left *} |
792 --{* 32 subgoals left *} |
793 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
793 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
794 --{* 20 subgoals left *} |
794 --{* 20 subgoals left *} |
795 apply(tactic{* TRYALL Clarify_tac *}) |
795 apply(tactic{* TRYALL (clarify_tac @{claset}) *}) |
796 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
796 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
797 apply(tactic {* TRYALL (etac disjE) *}) |
797 apply(tactic {* TRYALL (etac disjE) *}) |
798 apply simp_all |
798 apply simp_all |
799 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *}) |
799 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *}) |
800 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *}) |
800 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *}) |
810 apply(simp_all add:collector_mutator_interfree) |
810 apply(simp_all add:collector_mutator_interfree) |
811 apply(unfold modules collector_defs mutator_defs) |
811 apply(unfold modules collector_defs mutator_defs) |
812 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
812 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
813 --{* 64 subgoals left *} |
813 --{* 64 subgoals left *} |
814 apply(simp_all add:nth_list_update Invariants Append_to_free0)+ |
814 apply(simp_all add:nth_list_update Invariants Append_to_free0)+ |
815 apply(tactic{* TRYALL Clarify_tac *}) |
815 apply(tactic{* TRYALL (clarify_tac @{claset}) *}) |
816 --{* 4 subgoals left *} |
816 --{* 4 subgoals left *} |
817 apply force |
817 apply force |
818 apply(simp add:Append_to_free2) |
818 apply(simp add:Append_to_free2) |
819 apply force |
819 apply force |
820 apply(simp add:Append_to_free2) |
820 apply(simp add:Append_to_free2) |