src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
changeset 42793 88bee9f6eec7
parent 39159 0dec18004e75
child 42795 66fcc9882784
     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