1.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
1.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
1.3 @@ -132,7 +132,7 @@
1.4 apply(simp_all add:mul_mutator_interfree)
1.5 apply(simp_all add: mul_mutator_defs)
1.6 apply(tactic {* TRYALL (interfree_aux_tac) *})
1.7 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
1.8 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
1.9 apply (simp_all add:nth_list_update)
1.10 done
1.11
1.12 @@ -1123,7 +1123,7 @@
1.13 interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
1.14 apply (unfold mul_modules)
1.15 apply interfree_aux
1.16 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
1.17 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
1.18 apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
1.19 apply(erule_tac x=j in allE, force dest:Graph3)+
1.20 done
1.21 @@ -1132,7 +1132,7 @@
1.22 interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
1.23 apply (unfold mul_modules)
1.24 apply interfree_aux
1.25 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
1.26 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
1.27 apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update)
1.28 done
1.29
1.30 @@ -1140,7 +1140,7 @@
1.31 interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
1.32 apply (unfold mul_modules)
1.33 apply interfree_aux
1.34 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
1.35 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
1.36 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
1.37 Graph12 nth_list_update)
1.38 done
1.39 @@ -1149,7 +1149,7 @@
1.40 interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
1.41 apply (unfold mul_modules)
1.42 apply interfree_aux
1.43 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
1.44 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
1.45 apply(simp_all add: mul_mutator_defs nth_list_update)
1.46 apply(simp add:Mul_AppendInv_def Append_to_free0)
1.47 done
1.48 @@ -1178,7 +1178,7 @@
1.49 --{* 24 subgoals left *}
1.50 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
1.51 --{* 14 subgoals left *}
1.52 -apply(tactic {* TRYALL (clarify_tac @{claset}) *})
1.53 +apply(tactic {* TRYALL (clarify_tac @{context}) *})
1.54 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
1.55 apply(tactic {* TRYALL (rtac conjI) *})
1.56 apply(tactic {* TRYALL (rtac impI) *})
1.57 @@ -1189,7 +1189,7 @@
1.58 --{* 72 subgoals left *}
1.59 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
1.60 --{* 35 subgoals left *}
1.61 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
1.62 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
1.63 --{* 28 subgoals left *}
1.64 apply(tactic {* TRYALL (etac conjE) *})
1.65 apply(tactic {* TRYALL (etac disjE) *})
1.66 @@ -1199,17 +1199,21 @@
1.67 apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
1.68 apply(simp_all add:Graph10)
1.69 --{* 47 subgoals left *}
1.70 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
1.71 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
1.72 --{* 41 subgoals left *}
1.73 -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}])]) *})
1.74 +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
1.75 + force_tac (map_simpset_local (fn ss => ss addsimps
1.76 + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
1.77 --{* 35 subgoals left *}
1.78 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
1.79 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
1.80 --{* 31 subgoals left *}
1.81 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
1.82 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
1.83 --{* 29 subgoals left *}
1.84 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
1.85 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
1.86 --{* 25 subgoals left *}
1.87 -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}])]) *})
1.88 +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
1.89 + force_tac (map_simpset_local (fn ss => ss addsimps
1.90 + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
1.91 --{* 10 subgoals left *}
1.92 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)+
1.93 done