more antiquotations
authorhaftmann
Thu Mar 20 12:09:20 2008 +0100 (2008-03-20)
changeset 263596d437bde2f1d
parent 26358 d6a508c16908
child 26360 cd956c4eadff
more antiquotations
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/record_package.ML
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:04:54 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:09:20 2008 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4  fun inst_conj_all_tac k = EVERY
     1.5    [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
     1.6     REPEAT_DETERM_N k (etac allE 1),
     1.7 -   simp_tac (HOL_basic_ss addsimps [id_apply]) 1];
     1.8 +   simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
     1.9  
    1.10  fun map_term f t u = (case f t u of
    1.11        NONE => map_term' f t u | x => x)
    1.12 @@ -305,7 +305,7 @@
    1.13            (fn _ => EVERY
    1.14              [etac exE 1,
    1.15               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.16 -             full_simp_tac (HOL_basic_ss addsimps [id_apply]) 1,
    1.17 +             full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
    1.18               REPEAT (etac conjE 1)])
    1.19            [ex] ctxt
    1.20        in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
    1.21 @@ -347,7 +347,7 @@
    1.22                      map (fold_rev (NominalPackage.mk_perm [])
    1.23                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.24                   fun mk_pi th =
    1.25 -                   Simplifier.simplify (HOL_basic_ss addsimps [id_apply]
    1.26 +                   Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
    1.27                         addsimprocs [NominalPackage.perm_simproc])
    1.28                       (Simplifier.simplify eqvt_ss
    1.29                         (fold_rev (mk_perm_bool o cterm_of thy)
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 12:04:54 2008 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 12:09:20 2008 +0100
     2.3 @@ -959,7 +959,7 @@
     2.4                    alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
     2.5                    perm_rep_perm_thms)) 1),
     2.6                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
     2.7 -                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
     2.8 +                  @{thm expand_fun_eq} :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
     2.9          end) (constrs ~~ constr_rep_thms)
    2.10        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
    2.11  
     3.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 12:04:54 2008 +0100
     3.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 12:09:20 2008 +0100
     3.3 @@ -84,6 +84,9 @@
     3.4  lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
     3.5        |- Calling send p & ~Calling rcv p & cst!p = #clkA   
     3.6           --> Enabled (MClkFwd send rcv cst p)"
     3.7 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
     3.8 +    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     3.9 +    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
    3.10    by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
    3.11      thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
    3.12      [thm "base_enabled", Pair_inject] 1 *})
    3.13 @@ -100,10 +103,10 @@
    3.14        |- Calling send p & ~Calling rcv p & cst!p = #clkB   
    3.15           --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
    3.16    apply (tactic {* action_simp_tac @{simpset}
    3.17 -    [thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
    3.18 +    [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
    3.19    apply (tactic {* action_simp_tac (@{simpset} addsimps
    3.20 -    [thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
    3.21 -    [exI] [thm "base_enabled", Pair_inject] 1 *})
    3.22 +    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
    3.23 +    [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
    3.24    done
    3.25  
    3.26  lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
     4.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 20 12:04:54 2008 +0100
     4.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Mar 20 12:09:20 2008 +0100
     4.3 @@ -123,7 +123,7 @@
     4.4           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
     4.5            rtac (cterm_instantiate inst induction) 1,
     4.6            ALLGOALS ObjectLogic.atomize_prems_tac,
     4.7 -          rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
     4.8 +          rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
     4.9            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
    4.10              REPEAT (etac allE i) THEN atac i)) 1)]);
    4.11  
     5.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:04:54 2008 +0100
     5.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:09:20 2008 +0100
     5.3 @@ -401,7 +401,7 @@
     5.4  
     5.5          val rewrites = map mk_meta_eq iso_char_thms;
     5.6          val inj_thms' = map snd newT_iso_inj_thms @
     5.7 -          map (fn r => r RS injD) inj_thms;
     5.8 +          map (fn r => r RS @{thm injD}) inj_thms;
     5.9  
    5.10          val inj_thm = Goal.prove_global thy5 [] []
    5.11            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    5.12 @@ -425,7 +425,7 @@
    5.13                               Lim_inject :: fun_cong :: inj_thms')) 1),
    5.14                           atac 1]))])])])]);
    5.15  
    5.16 -        val inj_thms'' = map (fn r => r RS datatype_injI)
    5.17 +        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
    5.18                               (split_conj_thm inj_thm);
    5.19  
    5.20          val elem_thm = 
    5.21 @@ -442,7 +442,7 @@
    5.22      val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
    5.23        ([], map #3 newT_iso_axms) (tl descr);
    5.24      val iso_inj_thms = map snd newT_iso_inj_thms @
    5.25 -      map (fn r => r RS injD) iso_inj_thms_unfolded;
    5.26 +      map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
    5.27  
    5.28      (* prove  dt_rep_set_i x --> x : range dt_Rep_i *)
    5.29  
    5.30 @@ -461,7 +461,7 @@
    5.31  
    5.32      (* all the theorems are proved by one single simultaneous induction *)
    5.33  
    5.34 -    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
    5.35 +    val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
    5.36        iso_inj_thms_unfolded;
    5.37  
    5.38      val iso_thms = if length descr = 1 then [] else
    5.39 @@ -470,7 +470,7 @@
    5.40             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    5.41              REPEAT (rtac TrueI 1),
    5.42              rewrite_goals_tac (mk_meta_eq choice_eq ::
    5.43 -              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
    5.44 +              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    5.45              rewrite_goals_tac (map symmetric range_eqs),
    5.46              REPEAT (EVERY
    5.47                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
    5.48 @@ -495,7 +495,7 @@
    5.49      fun prove_constr_rep_thm eqn =
    5.50        let
    5.51          val inj_thms = map fst newT_iso_inj_thms;
    5.52 -        val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    5.53 +        val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    5.54        in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
    5.55          [resolve_tac inj_thms 1,
    5.56           rewrite_goals_tac rewrites,
     6.1 --- a/src/HOL/Tools/record_package.ML	Thu Mar 20 12:04:54 2008 +0100
     6.2 +++ b/src/HOL/Tools/record_package.ML	Thu Mar 20 12:09:20 2008 +0100
     6.3 @@ -64,8 +64,8 @@
     6.4  val meta_allE = thm "Pure.meta_allE";
     6.5  val prop_subst = thm "prop_subst";
     6.6  val Pair_sel_convs = [fst_conv,snd_conv];
     6.7 -val K_record_comp = thm "K_record_comp";
     6.8 -val K_comp_convs = [o_apply, K_record_comp]
     6.9 +val K_record_comp = @{thm "K_record_comp"};
    6.10 +val K_comp_convs = [@{thm o_apply}, K_record_comp]
    6.11  
    6.12  (** name components **)
    6.13  
    6.14 @@ -2063,7 +2063,7 @@
    6.15        in
    6.16          prove_standard [assm] concl (fn {prems, ...} =>
    6.17            try_param_tac rN induct_scheme 1
    6.18 -          THEN try_param_tac "more" unit_induct 1
    6.19 +          THEN try_param_tac "more" @{thm unit_induct} 1
    6.20            THEN resolve_tac prems 1)
    6.21        end;
    6.22      val induct = timeit_msg "record induct proof:" induct_prf;
     7.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Thu Mar 20 12:04:54 2008 +0100
     7.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Thu Mar 20 12:09:20 2008 +0100
     7.3 @@ -33,7 +33,7 @@
     7.4  apply (simp (no_asm) add: is_simulation_def)
     7.5  apply (rule conjI)
     7.6  txt {* start states *}
     7.7 -apply (tactic "SELECT_GOAL (safe_tac set_cs) 1")
     7.8 +apply (auto)[1]
     7.9  apply (rule_tac x = " ({},False) " in exI)
    7.10  apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def)
    7.11  txt {* main-part *}
    7.12 @@ -42,7 +42,7 @@
    7.13  apply (rename_tac k b used c k' b' a)
    7.14  apply (induct_tac "a")
    7.15  apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def)
    7.16 -apply (tactic "safe_tac set_cs")
    7.17 +apply auto
    7.18  txt {* NEW *}
    7.19  apply (rule_tac x = "(used,True)" in exI)
    7.20  apply simp
     8.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Mar 20 12:04:54 2008 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Mar 20 12:09:20 2008 +0100
     8.3 @@ -106,11 +106,7 @@
     8.4  apply simp
     8.5  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
     8.6  txt {* main case *}
     8.7 -apply (tactic "safe_tac set_cs")
     8.8 -apply (simp add: is_abstraction_def)
     8.9 -apply (frule reachable.reachable_n)
    8.10 -apply assumption
    8.11 -apply simp
    8.12 +apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
    8.13  done
    8.14  
    8.15  
    8.16 @@ -131,8 +127,7 @@
    8.17            ==> validIOA C P"
    8.18  apply (drule abs_is_weakening)
    8.19  apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
    8.20 -apply (tactic "safe_tac set_cs")
    8.21 -apply (tactic {* pair_tac "ex" 1 *})
    8.22 +apply (auto simp add: split_paired_all)
    8.23  done
    8.24  
    8.25  
    8.26 @@ -161,8 +156,7 @@
    8.27  apply auto
    8.28  apply (drule abs_is_weakening)
    8.29  apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
    8.30 -apply (tactic "safe_tac set_cs")
    8.31 -apply (tactic {* pair_tac "ex" 1 *})
    8.32 +apply (auto simp add: split_paired_all)
    8.33  done
    8.34  
    8.35  
    8.36 @@ -175,8 +169,7 @@
    8.37  apply auto
    8.38  apply (drule abs_is_weakening)
    8.39  apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
    8.40 -apply (tactic "safe_tac set_cs")
    8.41 -apply (tactic {* pair_tac "ex" 1 *})
    8.42 +apply (auto simp add: split_paired_all)
    8.43  done
    8.44  
    8.45  
    8.46 @@ -185,7 +178,7 @@
    8.47  lemma abstraction_is_ref_map:
    8.48  "is_abstraction h C A ==> is_ref_map h C A"
    8.49  apply (unfold is_abstraction_def is_ref_map_def)
    8.50 -apply (tactic "safe_tac set_cs")
    8.51 +apply auto
    8.52  apply (rule_tac x = "(a,h t) >>nil" in exI)
    8.53  apply (simp add: move_def)
    8.54  done
    8.55 @@ -223,9 +216,9 @@
    8.56                     is_live_abstraction h (C,M) (A,L) |]
    8.57                  ==> live_implements (C,M) (A,L)"
    8.58  apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
    8.59 -apply (tactic "safe_tac set_cs")
    8.60 +apply auto
    8.61  apply (rule_tac x = "cex_abs h ex" in exI)
    8.62 -apply (tactic "safe_tac set_cs")
    8.63 +apply auto
    8.64    (* Traces coincide *)
    8.65    apply (tactic {* pair_tac "ex" 1 *})
    8.66    apply (rule traces_coincide_abs)
    8.67 @@ -251,9 +244,7 @@
    8.68  
    8.69  lemma implements_trans:
    8.70  "[| A =<| B; B =<| C|] ==> A =<| C"
    8.71 -apply (unfold ioa_implements_def)
    8.72 -apply auto
    8.73 -done
    8.74 +by (auto simp add: ioa_implements_def)
    8.75  
    8.76  
    8.77  subsection "Abstraction Rules for Automata"
    8.78 @@ -373,7 +364,7 @@
    8.79  apply (tactic {* Seq_Finite_induct_tac 1 *})
    8.80  apply blast
    8.81  (* main case *)
    8.82 -apply (tactic "clarify_tac set_cs 1")
    8.83 +apply clarify
    8.84  apply (tactic {* pair_tac "ex" 1 *})
    8.85  apply (tactic {* Seq_case_simp_tac "y" 1 *})
    8.86  (* UU case *)
    8.87 @@ -425,9 +416,9 @@
    8.88  "[| temp_strengthening P Q h |]
    8.89         ==> temp_strengthening ([] P) ([] Q) h"
    8.90  apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
    8.91 -apply (tactic "clarify_tac set_cs 1")
    8.92 +apply clarify
    8.93  apply (frule ex2seq_tsuffix)
    8.94 -apply (tactic "clarify_tac set_cs 1")
    8.95 +apply clarify
    8.96  apply (drule_tac h = "h" in cex_absSeq_tsuffix)
    8.97  apply (simp add: ex2seq_abs_cex)
    8.98  done
    8.99 @@ -440,7 +431,7 @@
   8.100         ==> temp_strengthening (Init P) (Init Q) h"
   8.101  apply (unfold temp_strengthening_def state_strengthening_def
   8.102    temp_sat_def satisfies_def Init_def unlift_def)
   8.103 -apply (tactic "safe_tac set_cs")
   8.104 +apply auto
   8.105  apply (tactic {* pair_tac "ex" 1 *})
   8.106  apply (tactic {* Seq_case_simp_tac "y" 1 *})
   8.107  apply (tactic {* pair_tac "a" 1 *})
   8.108 @@ -505,7 +496,7 @@
   8.109         ==> temp_strengthening (Next P) (Next Q) h"
   8.110  apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
   8.111  apply simp
   8.112 -apply (tactic "safe_tac set_cs")
   8.113 +apply auto
   8.114  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   8.115  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   8.116  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
   8.117 @@ -526,7 +517,7 @@
   8.118         ==> temp_weakening (Init P) (Init Q) h"
   8.119  apply (simp add: temp_weakening_def2 state_weakening_def2
   8.120    temp_sat_def satisfies_def Init_def unlift_def)
   8.121 -apply (tactic "safe_tac set_cs")
   8.122 +apply auto
   8.123  apply (tactic {* pair_tac "ex" 1 *})
   8.124  apply (tactic {* Seq_case_simp_tac "y" 1 *})
   8.125  apply (tactic {* pair_tac "a" 1 *})
     9.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Mar 20 12:04:54 2008 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Mar 20 12:09:20 2008 +0100
     9.3 @@ -399,7 +399,7 @@
     9.4        ==> input_enabled (A||B)"
     9.5  apply (unfold input_enabled_def)
     9.6  apply (simp add: Let_def inputs_of_par trans_of_par)
     9.7 -apply (tactic "safe_tac set_cs")
     9.8 +apply (tactic "safe_tac (claset_of @{theory Fun})")
     9.9  apply (simp add: inp_is_act)
    9.10  prefer 2
    9.11  apply (simp add: inp_is_act)
    10.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Mar 20 12:04:54 2008 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Mar 20 12:09:20 2008 +0100
    10.3 @@ -218,9 +218,7 @@
    10.4  
    10.5  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
    10.6  (* main case *)
    10.7 -apply (rename_tac ss a t)
    10.8 -apply (tactic "safe_tac set_cs")
    10.9 -apply (simp_all add: trans_of_defs2)
   10.10 +apply (auto simp add: trans_of_defs2)
   10.11  done
   10.12  
   10.13  
   10.14 @@ -234,8 +232,7 @@
   10.15  
   10.16  apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
   10.17  (* main case *)
   10.18 -apply (tactic "safe_tac set_cs")
   10.19 -apply (simp_all add: trans_of_defs2)
   10.20 +apply (auto simp add: trans_of_defs2)
   10.21  done
   10.22  
   10.23  
   10.24 @@ -249,8 +246,8 @@
   10.25  apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   10.26    thm "is_exec_frag_def"] 1 *})
   10.27  (* main case *)
   10.28 -apply (tactic "safe_tac set_cs")
   10.29 -apply (simp_all add: trans_of_defs2 actions_asig_comp asig_of_par)
   10.30 +apply auto
   10.31 +apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
   10.32  done
   10.33  
   10.34  
   10.35 @@ -268,10 +265,7 @@
   10.36  
   10.37  apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   10.38    thm "is_exec_frag_def", thm "stutter_def"] 1 *})
   10.39 -apply (simp add: trans_of_defs1 actions_asig_comp asig_of_par)
   10.40 -apply (tactic "safe_tac set_cs")
   10.41 -apply simp
   10.42 -apply simp
   10.43 +apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
   10.44  done
   10.45  
   10.46  
    11.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Mar 20 12:04:54 2008 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Mar 20 12:09:20 2008 +0100
    11.3 @@ -237,8 +237,8 @@
    11.4  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
    11.5    thm "sforall_def"] 1 *})
    11.6  (* main case *)
    11.7 -apply (tactic "safe_tac set_cs")
    11.8 -apply (auto simp add: trans_of_defs2 actions_asig_comp asig_of_par)
    11.9 +apply auto
   11.10 +apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
   11.11  done
   11.12  
   11.13  
   11.14 @@ -260,7 +260,7 @@
   11.15  
   11.16  (* main case *)
   11.17  (* splitting into 4 cases according to a:A, a:B *)
   11.18 -apply (tactic "safe_tac set_cs")
   11.19 +apply auto
   11.20  
   11.21  (* Case y:A, y:B *)
   11.22  apply (tactic {* Seq_case_simp_tac "exA" 1 *})
   11.23 @@ -301,7 +301,7 @@
   11.24  fun mkex_induct_tac sch exA exB =
   11.25      EVERY1[Seq_induct_tac sch defs,
   11.26             SIMPSET' asm_full_simp_tac,
   11.27 -           SELECT_GOAL (safe_tac set_cs),
   11.28 +           SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
   11.29             Seq_case_simp_tac exA,
   11.30             Seq_case_simp_tac exB,
   11.31             SIMPSET' asm_full_simp_tac,
   11.32 @@ -502,7 +502,7 @@
   11.33     Filter (%a. a:act B)$sch : schedules B &
   11.34     Forall (%x. x:act (A||B)) sch)"
   11.35  apply (simp (no_asm) add: schedules_def has_schedule_def)
   11.36 -apply (tactic "safe_tac set_cs")
   11.37 +apply auto
   11.38  (* ==> *)
   11.39  apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
   11.40  prefer 2
    12.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Mar 20 12:04:54 2008 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Mar 20 12:09:20 2008 +0100
    12.3 @@ -200,7 +200,7 @@
    12.4      ! schA schB. Forall (%x. x:act (A||B)) tr  
    12.5      --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
    12.6  apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
    12.7 -apply (tactic "safe_tac set_cs")
    12.8 +apply auto
    12.9  apply (simp add: actions_of_par)
   12.10  apply (case_tac "a:act A")
   12.11  apply (case_tac "a:act B")
   12.12 @@ -227,7 +227,7 @@
   12.13      ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
   12.14      --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
   12.15  apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   12.16 -apply (tactic "safe_tac set_cs")
   12.17 +apply auto
   12.18  apply (rule Forall_Conc_impl [THEN mp])
   12.19  apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
   12.20  done
   12.21 @@ -236,8 +236,7 @@
   12.22      ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
   12.23      --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
   12.24  apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   12.25 -apply (tactic "safe_tac set_cs")
   12.26 -apply simp
   12.27 +apply auto
   12.28  apply (rule Forall_Conc_impl [THEN mp])
   12.29  apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
   12.30  done
   12.31 @@ -256,7 +255,7 @@
   12.32  apply simp
   12.33  (* main case *)
   12.34  apply simp
   12.35 -apply (tactic "safe_tac set_cs")
   12.36 +apply auto
   12.37  
   12.38  (* a: act A; a: act B *)
   12.39  apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   12.40 @@ -415,7 +414,7 @@
   12.41  apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   12.42  (* main case *)
   12.43  (* splitting into 4 cases according to a:A, a:B *)
   12.44 -apply (tactic "safe_tac set_cs")
   12.45 +apply auto
   12.46  
   12.47  (* Case a:A, a:B *)
   12.48  apply (frule divide_Seq)
   12.49 @@ -903,7 +902,7 @@
   12.50                Forall (%x. x:ext(A||B)) tr)"
   12.51  
   12.52  apply (simp (no_asm) add: traces_def has_trace_def)
   12.53 -apply (tactic "safe_tac set_cs")
   12.54 +apply auto
   12.55  
   12.56  (* ==> *)
   12.57  (* There is a schedule of A *)
    13.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Mar 20 12:04:54 2008 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Mar 20 12:09:20 2008 +0100
    13.3 @@ -52,7 +52,7 @@
    13.4  apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
    13.5  apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
    13.6  apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
    13.7 -apply (tactic "safe_tac set_cs")
    13.8 +apply auto
    13.9  apply (simp add: compositionality_tr)
   13.10  apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2")
   13.11  prefer 2
   13.12 @@ -60,7 +60,7 @@
   13.13  apply (erule conjE)+
   13.14  (* rewrite with proven subgoal *)
   13.15  apply (simp add: externals_of_par)
   13.16 -apply (tactic "safe_tac set_cs")
   13.17 +apply auto
   13.18  
   13.19  (* 2 goals, the 3rd has been solved automatically *)
   13.20  (* 1: Filter A2 x : traces A2 *)
    14.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:04:54 2008 +0100
    14.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:09:20 2008 +0100
    14.3 @@ -15,7 +15,7 @@
    14.4    "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]  
    14.5            ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A"
    14.6  apply (simp add: schedules_def has_schedule_def)
    14.7 -apply (tactic "safe_tac set_cs")
    14.8 +apply auto
    14.9  apply (frule inp_is_act)
   14.10  apply (simp add: executions_def)
   14.11  apply (tactic {* pair_tac "ex" 1 *})
    15.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Mar 20 12:04:54 2008 +0100
    15.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Mar 20 12:09:20 2008 +0100
    15.3 @@ -60,9 +60,9 @@
    15.4                     is_live_ref_map f (C,M) (A,L) |]
    15.5                  ==> live_implements (C,M) (A,L)"
    15.6  apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
    15.7 -apply (tactic "safe_tac set_cs")
    15.8 +apply auto
    15.9  apply (rule_tac x = "corresp_ex A f ex" in exI)
   15.10 -apply (tactic "safe_tac set_cs")
   15.11 +apply auto
   15.12    (* Traces coincide, Lemma 1 *)
   15.13    apply (tactic {* pair_tac "ex" 1 *})
   15.14    apply (erule lemma_1 [THEN spec, THEN mp])
   15.15 @@ -80,8 +80,6 @@
   15.16    apply (erule lemma_2 [THEN spec, THEN mp])
   15.17    apply (simp add: reachable.reachable_0)
   15.18  
   15.19 - (* Liveness *)
   15.20 -apply auto
   15.21  done
   15.22  
   15.23  end
    16.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Mar 20 12:04:54 2008 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Mar 20 12:09:20 2008 +0100
    16.3 @@ -183,12 +183,10 @@
    16.4  apply (unfold corresp_ex_def)
    16.5  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
    16.6  (* cons case *)
    16.7 -apply (tactic "safe_tac set_cs")
    16.8 -apply (simp add: mk_traceConc)
    16.9 +apply (auto simp add: mk_traceConc)
   16.10  apply (frule reachable.reachable_n)
   16.11  apply assumption
   16.12  apply (erule_tac x = "y" in allE)
   16.13 -apply simp
   16.14  apply (simp add: move_subprop4 split add: split_if)
   16.15  done
   16.16  
   16.17 @@ -214,8 +212,7 @@
   16.18  apply (rule impI)
   16.19  apply (tactic {* Seq_Finite_induct_tac 1 *})
   16.20  (* main case *)
   16.21 -apply (tactic "safe_tac set_cs")
   16.22 -apply (tactic {* pair_tac "a" 1 *})
   16.23 +apply (auto simp add: split_paired_all)
   16.24  done
   16.25  
   16.26  
   16.27 @@ -235,7 +232,7 @@
   16.28  apply simp
   16.29  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
   16.30  (* main case *)
   16.31 -apply (tactic "safe_tac set_cs")
   16.32 +apply auto
   16.33  apply (rule_tac t = "f y" in lemma_2_1)
   16.34  
   16.35  (* Finite *)
   16.36 @@ -270,7 +267,7 @@
   16.37    apply (unfold traces_def)
   16.38  
   16.39    apply (simp (no_asm) add: has_trace_def2)
   16.40 -  apply (tactic "safe_tac set_cs")
   16.41 +  apply auto
   16.42  
   16.43    (* give execution of abstract automata *)
   16.44    apply (rule_tac x = "corresp_ex A f ex" in bexI)
   16.45 @@ -322,9 +319,9 @@
   16.46            !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
   16.47            ==> fairtraces C <= fairtraces A"
   16.48  apply (simp (no_asm) add: fairtraces_def fairexecutions_def)
   16.49 -apply (tactic "safe_tac set_cs")
   16.50 +apply auto
   16.51  apply (rule_tac x = "corresp_ex A f ex" in exI)
   16.52 -apply (tactic "safe_tac set_cs")
   16.53 +apply auto
   16.54  
   16.55    (* Traces coincide, Lemma 1 *)
   16.56    apply (tactic {* pair_tac "ex" 1 *})
   16.57 @@ -342,8 +339,6 @@
   16.58    apply (erule lemma_2 [THEN spec, THEN mp])
   16.59    apply (simp add: reachable.reachable_0)
   16.60  
   16.61 - (* Fairness *)
   16.62 -apply auto
   16.63  done
   16.64  
   16.65  lemma fair_trace_inclusion2: "!! C A.
   16.66 @@ -351,9 +346,10 @@
   16.67               is_fair_ref_map f C A |]
   16.68            ==> fair_implements C A"
   16.69  apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
   16.70 -apply (tactic "safe_tac set_cs")
   16.71 +apply auto
   16.72  apply (rule_tac x = "corresp_ex A f ex" in exI)
   16.73 -apply (tactic "safe_tac set_cs")
   16.74 +apply auto
   16.75 +
   16.76    (* Traces coincide, Lemma 1 *)
   16.77    apply (tactic {* pair_tac "ex" 1 *})
   16.78    apply (erule lemma_1 [THEN spec, THEN mp])
   16.79 @@ -371,8 +367,6 @@
   16.80    apply (erule lemma_2 [THEN spec, THEN mp])
   16.81    apply (simp add: reachable.reachable_0)
   16.82  
   16.83 - (* Fairness *)
   16.84 -apply auto
   16.85  done
   16.86  
   16.87  
    17.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Mar 20 12:04:54 2008 +0100
    17.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Mar 20 12:09:20 2008 +0100
    17.3 @@ -73,12 +73,9 @@
    17.4    "[| ext C = ext A;  
    17.5       is_weak_ref_map f C A |] ==> is_ref_map f C A"
    17.6  apply (unfold is_weak_ref_map_def is_ref_map_def)
    17.7 -apply (tactic "safe_tac set_cs")
    17.8 +apply auto
    17.9  apply (case_tac "a:ext A")
   17.10 -apply (rule transition_is_ex)
   17.11 -apply (simp (no_asm_simp))
   17.12 -apply (rule nothing_is_ex)
   17.13 -apply simp
   17.14 +apply (auto intro: transition_is_ex nothing_is_ex)
   17.15  done
   17.16  
   17.17  
    18.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Mar 20 12:04:54 2008 +0100
    18.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Mar 20 12:09:20 2008 +0100
    18.3 @@ -223,11 +223,11 @@
    18.4                 LastActExtsch A sch"
    18.5  
    18.6  apply (unfold schedules_def has_schedule_def)
    18.7 -apply (tactic "safe_tac set_cs")
    18.8 +apply auto
    18.9  apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
   18.10  apply (simp add: executions_def)
   18.11  apply (tactic {* pair_tac "ex" 1 *})
   18.12 -apply (tactic "safe_tac set_cs")
   18.13 +apply auto
   18.14  apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
   18.15  apply (simp (no_asm_simp))
   18.16  
    19.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 20 12:04:54 2008 +0100
    19.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 20 12:09:20 2008 +0100
    19.3 @@ -174,14 +174,13 @@
    19.4  
    19.5  apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
    19.6  (* cons case *)
    19.7 -apply (tactic "safe_tac set_cs")
    19.8 +apply auto
    19.9  apply (rename_tac ex a t s s')
   19.10  apply (simp add: mk_traceConc)
   19.11  apply (frule reachable.reachable_n)
   19.12  apply assumption
   19.13  apply (erule_tac x = "t" in allE)
   19.14  apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
   19.15 -apply simp
   19.16  apply (simp add: move_subprop5_sim [unfolded Let_def]
   19.17    move_subprop4_sim [unfolded Let_def] split add: split_if)
   19.18  done
   19.19 @@ -200,7 +199,7 @@
   19.20  
   19.21  apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
   19.22  (* main case *)
   19.23 -apply (tactic "safe_tac set_cs")
   19.24 +apply auto
   19.25  apply (rename_tac ex a t s s')
   19.26  apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
   19.27  
   19.28 @@ -262,7 +261,7 @@
   19.29    apply (unfold traces_def)
   19.30  
   19.31    apply (simp (no_asm) add: has_trace_def2)
   19.32 -  apply (tactic "safe_tac set_cs")
   19.33 +  apply auto
   19.34  
   19.35    (* give execution of abstract automata *)
   19.36    apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
    20.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:04:54 2008 +0100
    20.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:09:20 2008 +0100
    20.3 @@ -166,7 +166,7 @@
    20.4                .--> (Next (Init (%(s,a,t).Q s))))"
    20.5  apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
    20.6  
    20.7 -apply (tactic "clarify_tac set_cs 1")
    20.8 +apply clarify
    20.9  apply (simp split add: split_if)
   20.10  (* TL = UU *)
   20.11  apply (rule conjI)
    21.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Mar 20 12:04:54 2008 +0100
    21.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Mar 20 12:09:20 2008 +0100
    21.3 @@ -345,21 +345,7 @@
    21.4  lemma has_trace_def2: 
    21.5  "has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
    21.6  apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
    21.7 -apply (tactic "safe_tac set_cs")
    21.8 -(* 1 *)
    21.9 -apply (rule_tac x = "ex" in bexI)
   21.10 -apply (simplesubst beta_cfun)
   21.11 -apply (tactic "cont_tacR 1")
   21.12 -apply (simp (no_asm))
   21.13 -apply (simp (no_asm_simp))
   21.14 -(* 2 *)
   21.15 -apply (rule_tac x = "filter_act$ (snd ex) " in bexI)
   21.16 -apply (simplesubst beta_cfun)
   21.17 -apply (tactic "cont_tacR 1")
   21.18 -apply (simp (no_asm))
   21.19 -apply (tactic "safe_tac set_cs")
   21.20 -apply (rule_tac x = "ex" in bexI)
   21.21 -apply simp_all
   21.22 +apply auto
   21.23  done
   21.24  
   21.25  
   21.26 @@ -376,9 +362,7 @@
   21.27  apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
   21.28    thm "Forall_def", thm "sforall_def"] 1 *})
   21.29  (* main case *)
   21.30 -apply (rename_tac ss a t)
   21.31 -apply (tactic "safe_tac set_cs")
   21.32 -apply (simp_all add: is_trans_of_def)
   21.33 +apply (auto simp add: is_trans_of_def)
   21.34  done
   21.35  
   21.36  lemma exec_in_sig: