--- a/src/HOL/Nominal/nominal_inductive.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 20 12:09:20 2008 +0100
@@ -110,7 +110,7 @@
fun inst_conj_all_tac k = EVERY
[TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
REPEAT_DETERM_N k (etac allE 1),
- simp_tac (HOL_basic_ss addsimps [id_apply]) 1];
+ simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
fun map_term f t u = (case f t u of
NONE => map_term' f t u | x => x)
@@ -305,7 +305,7 @@
(fn _ => EVERY
[etac exE 1,
full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
- full_simp_tac (HOL_basic_ss addsimps [id_apply]) 1,
+ full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
REPEAT (etac conjE 1)])
[ex] ctxt
in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
@@ -347,7 +347,7 @@
map (fold_rev (NominalPackage.mk_perm [])
(rev pis' @ pis)) params' @ [z])) ihyp;
fun mk_pi th =
- Simplifier.simplify (HOL_basic_ss addsimps [id_apply]
+ Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
addsimprocs [NominalPackage.perm_simproc])
(Simplifier.simplify eqvt_ss
(fold_rev (mk_perm_bool o cterm_of thy)
--- a/src/HOL/Nominal/nominal_package.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Thu Mar 20 12:09:20 2008 +0100
@@ -959,7 +959,7 @@
alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
perm_rep_perm_thms)) 1),
TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
- expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
+ @{thm expand_fun_eq} :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
end) (constrs ~~ constr_rep_thms)
end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
--- a/src/HOL/TLA/Memory/MemClerk.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Thu Mar 20 12:09:20 2008 +0100
@@ -84,6 +84,9 @@
lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
|- Calling send p & ~Calling rcv p & cst!p = #clkA
--> Enabled (MClkFwd send rcv cst p)"
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
+ @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
[thm "base_enabled", Pair_inject] 1 *})
@@ -100,10 +103,10 @@
|- Calling send p & ~Calling rcv p & cst!p = #clkB
--> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
apply (tactic {* action_simp_tac @{simpset}
- [thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
+ [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
apply (tactic {* action_simp_tac (@{simpset} addsimps
- [thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
- [exI] [thm "base_enabled", Pair_inject] 1 *})
+ [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+ [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
--- a/src/HOL/Tools/datatype_realizer.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Thu Mar 20 12:09:20 2008 +0100
@@ -123,7 +123,7 @@
[rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
rtac (cterm_instantiate inst induction) 1,
ALLGOALS ObjectLogic.atomize_prems_tac,
- rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
+ rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)]);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 20 12:09:20 2008 +0100
@@ -401,7 +401,7 @@
val rewrites = map mk_meta_eq iso_char_thms;
val inj_thms' = map snd newT_iso_inj_thms @
- map (fn r => r RS injD) inj_thms;
+ map (fn r => r RS @{thm injD}) inj_thms;
val inj_thm = Goal.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
@@ -425,7 +425,7 @@
Lim_inject :: fun_cong :: inj_thms')) 1),
atac 1]))])])])]);
- val inj_thms'' = map (fn r => r RS datatype_injI)
+ val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
(split_conj_thm inj_thm);
val elem_thm =
@@ -442,7 +442,7 @@
val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
([], map #3 newT_iso_axms) (tl descr);
val iso_inj_thms = map snd newT_iso_inj_thms @
- map (fn r => r RS injD) iso_inj_thms_unfolded;
+ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
(* prove dt_rep_set_i x --> x : range dt_Rep_i *)
@@ -461,7 +461,7 @@
(* all the theorems are proved by one single simultaneous induction *)
- val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
+ val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
iso_inj_thms_unfolded;
val iso_thms = if length descr = 1 then [] else
@@ -470,7 +470,7 @@
[(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq choice_eq ::
- symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
+ symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
rewrite_goals_tac (map symmetric range_eqs),
REPEAT (EVERY
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
@@ -495,7 +495,7 @@
fun prove_constr_rep_thm eqn =
let
val inj_thms = map fst newT_iso_inj_thms;
- val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
+ val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
--- a/src/HOL/Tools/record_package.ML Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Thu Mar 20 12:09:20 2008 +0100
@@ -64,8 +64,8 @@
val meta_allE = thm "Pure.meta_allE";
val prop_subst = thm "prop_subst";
val Pair_sel_convs = [fst_conv,snd_conv];
-val K_record_comp = thm "K_record_comp";
-val K_comp_convs = [o_apply, K_record_comp]
+val K_record_comp = @{thm "K_record_comp"};
+val K_comp_convs = [@{thm o_apply}, K_record_comp]
(** name components **)
@@ -2063,7 +2063,7 @@
in
prove_standard [assm] concl (fn {prems, ...} =>
try_param_tac rN induct_scheme 1
- THEN try_param_tac "more" unit_induct 1
+ THEN try_param_tac "more" @{thm unit_induct} 1
THEN resolve_tac prems 1)
end;
val induct = timeit_msg "record induct proof:" induct_prf;
--- a/src/HOLCF/IOA/Storage/Correctness.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Thu Mar 20 12:09:20 2008 +0100
@@ -33,7 +33,7 @@
apply (simp (no_asm) add: is_simulation_def)
apply (rule conjI)
txt {* start states *}
-apply (tactic "SELECT_GOAL (safe_tac set_cs) 1")
+apply (auto)[1]
apply (rule_tac x = " ({},False) " in exI)
apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def)
txt {* main-part *}
@@ -42,7 +42,7 @@
apply (rename_tac k b used c k' b' a)
apply (induct_tac "a")
apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def)
-apply (tactic "safe_tac set_cs")
+apply auto
txt {* NEW *}
apply (rule_tac x = "(used,True)" in exI)
apply simp
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Mar 20 12:09:20 2008 +0100
@@ -106,11 +106,7 @@
apply simp
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
txt {* main case *}
-apply (tactic "safe_tac set_cs")
-apply (simp add: is_abstraction_def)
-apply (frule reachable.reachable_n)
-apply assumption
-apply simp
+apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
done
@@ -131,8 +127,7 @@
==> validIOA C P"
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
done
@@ -161,8 +156,7 @@
apply auto
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
done
@@ -175,8 +169,7 @@
apply auto
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
done
@@ -185,7 +178,7 @@
lemma abstraction_is_ref_map:
"is_abstraction h C A ==> is_ref_map h C A"
apply (unfold is_abstraction_def is_ref_map_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "(a,h t) >>nil" in exI)
apply (simp add: move_def)
done
@@ -223,9 +216,9 @@
is_live_abstraction h (C,M) (A,L) |]
==> live_implements (C,M) (A,L)"
apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "cex_abs h ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
(* Traces coincide *)
apply (tactic {* pair_tac "ex" 1 *})
apply (rule traces_coincide_abs)
@@ -251,9 +244,7 @@
lemma implements_trans:
"[| A =<| B; B =<| C|] ==> A =<| C"
-apply (unfold ioa_implements_def)
-apply auto
-done
+by (auto simp add: ioa_implements_def)
subsection "Abstraction Rules for Automata"
@@ -373,7 +364,7 @@
apply (tactic {* Seq_Finite_induct_tac 1 *})
apply blast
(* main case *)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
(* UU case *)
@@ -425,9 +416,9 @@
"[| temp_strengthening P Q h |]
==> temp_strengthening ([] P) ([] Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
apply (frule ex2seq_tsuffix)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
apply (drule_tac h = "h" in cex_absSeq_tsuffix)
apply (simp add: ex2seq_abs_cex)
done
@@ -440,7 +431,7 @@
==> temp_strengthening (Init P) (Init Q) h"
apply (unfold temp_strengthening_def state_strengthening_def
temp_sat_def satisfies_def Init_def unlift_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
apply (tactic {* pair_tac "a" 1 *})
@@ -505,7 +496,7 @@
==> temp_strengthening (Next P) (Next Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
apply simp
-apply (tactic "safe_tac set_cs")
+apply auto
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
@@ -526,7 +517,7 @@
==> temp_weakening (Init P) (Init Q) h"
apply (simp add: temp_weakening_def2 state_weakening_def2
temp_sat_def satisfies_def Init_def unlift_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
apply (tactic {* pair_tac "a" 1 *})
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Mar 20 12:09:20 2008 +0100
@@ -399,7 +399,7 @@
==> input_enabled (A||B)"
apply (unfold input_enabled_def)
apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac set_cs")
+apply (tactic "safe_tac (claset_of @{theory Fun})")
apply (simp add: inp_is_act)
prefer 2
apply (simp add: inp_is_act)
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Mar 20 12:09:20 2008 +0100
@@ -218,9 +218,7 @@
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
(* main case *)
-apply (rename_tac ss a t)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2)
+apply (auto simp add: trans_of_defs2)
done
@@ -234,8 +232,7 @@
apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2)
+apply (auto simp add: trans_of_defs2)
done
@@ -249,8 +246,8 @@
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
thm "is_exec_frag_def"] 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2 actions_asig_comp asig_of_par)
+apply auto
+apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
done
@@ -268,10 +265,7 @@
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
thm "is_exec_frag_def", thm "stutter_def"] 1 *})
-apply (simp add: trans_of_defs1 actions_asig_comp asig_of_par)
-apply (tactic "safe_tac set_cs")
-apply simp
-apply simp
+apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
done
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Mar 20 12:09:20 2008 +0100
@@ -237,8 +237,8 @@
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
thm "sforall_def"] 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
-apply (auto simp add: trans_of_defs2 actions_asig_comp asig_of_par)
+apply auto
+apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
done
@@ -260,7 +260,7 @@
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
-apply (tactic "safe_tac set_cs")
+apply auto
(* Case y:A, y:B *)
apply (tactic {* Seq_case_simp_tac "exA" 1 *})
@@ -301,7 +301,7 @@
fun mkex_induct_tac sch exA exB =
EVERY1[Seq_induct_tac sch defs,
SIMPSET' asm_full_simp_tac,
- SELECT_GOAL (safe_tac set_cs),
+ SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
Seq_case_simp_tac exA,
Seq_case_simp_tac exB,
SIMPSET' asm_full_simp_tac,
@@ -502,7 +502,7 @@
Filter (%a. a:act B)$sch : schedules B &
Forall (%x. x:act (A||B)) sch)"
apply (simp (no_asm) add: schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
(* ==> *)
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
prefer 2
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Mar 20 12:09:20 2008 +0100
@@ -200,7 +200,7 @@
! schA schB. Forall (%x. x:act (A||B)) tr
--> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
apply (simp add: actions_of_par)
apply (case_tac "a:act A")
apply (case_tac "a:act B")
@@ -227,7 +227,7 @@
! schA schB. (Forall (%x. x:act B & x~:act A) tr
--> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
done
@@ -236,8 +236,7 @@
! schA schB. (Forall (%x. x:act A & x~:act B) tr
--> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
-apply simp
+apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
done
@@ -256,7 +255,7 @@
apply simp
(* main case *)
apply simp
-apply (tactic "safe_tac set_cs")
+apply auto
(* a: act A; a: act B *)
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
@@ -415,7 +414,7 @@
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
-apply (tactic "safe_tac set_cs")
+apply auto
(* Case a:A, a:B *)
apply (frule divide_Seq)
@@ -903,7 +902,7 @@
Forall (%x. x:ext(A||B)) tr)"
apply (simp (no_asm) add: traces_def has_trace_def)
-apply (tactic "safe_tac set_cs")
+apply auto
(* ==> *)
(* There is a schedule of A *)
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Thu Mar 20 12:09:20 2008 +0100
@@ -52,7 +52,7 @@
apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (simp add: compositionality_tr)
apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2")
prefer 2
@@ -60,7 +60,7 @@
apply (erule conjE)+
(* rewrite with proven subgoal *)
apply (simp add: externals_of_par)
-apply (tactic "safe_tac set_cs")
+apply auto
(* 2 goals, the 3rd has been solved automatically *)
(* 1: Filter A2 x : traces A2 *)
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Mar 20 12:09:20 2008 +0100
@@ -15,7 +15,7 @@
"[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]
==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A"
apply (simp add: schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (frule inp_is_act)
apply (simp add: executions_def)
apply (tactic {* pair_tac "ex" 1 *})
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Thu Mar 20 12:09:20 2008 +0100
@@ -60,9 +60,9 @@
is_live_ref_map f (C,M) (A,L) |]
==> live_implements (C,M) (A,L)"
apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
(* Traces coincide, Lemma 1 *)
apply (tactic {* pair_tac "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
@@ -80,8 +80,6 @@
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
- (* Liveness *)
-apply auto
done
end
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Mar 20 12:09:20 2008 +0100
@@ -183,12 +183,10 @@
apply (unfold corresp_ex_def)
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
(* cons case *)
-apply (tactic "safe_tac set_cs")
-apply (simp add: mk_traceConc)
+apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
apply assumption
apply (erule_tac x = "y" in allE)
-apply simp
apply (simp add: move_subprop4 split add: split_if)
done
@@ -214,8 +212,7 @@
apply (rule impI)
apply (tactic {* Seq_Finite_induct_tac 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "a" 1 *})
+apply (auto simp add: split_paired_all)
done
@@ -235,7 +232,7 @@
apply simp
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac t = "f y" in lemma_2_1)
(* Finite *)
@@ -270,7 +267,7 @@
apply (unfold traces_def)
apply (simp (no_asm) add: has_trace_def2)
- apply (tactic "safe_tac set_cs")
+ apply auto
(* give execution of abstract automata *)
apply (rule_tac x = "corresp_ex A f ex" in bexI)
@@ -322,9 +319,9 @@
!! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
==> fairtraces C <= fairtraces A"
apply (simp (no_asm) add: fairtraces_def fairexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
(* Traces coincide, Lemma 1 *)
apply (tactic {* pair_tac "ex" 1 *})
@@ -342,8 +339,6 @@
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
- (* Fairness *)
-apply auto
done
lemma fair_trace_inclusion2: "!! C A.
@@ -351,9 +346,10 @@
is_fair_ref_map f C A |]
==> fair_implements C A"
apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
+
(* Traces coincide, Lemma 1 *)
apply (tactic {* pair_tac "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
@@ -371,8 +367,6 @@
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
- (* Fairness *)
-apply auto
done
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Thu Mar 20 12:09:20 2008 +0100
@@ -73,12 +73,9 @@
"[| ext C = ext A;
is_weak_ref_map f C A |] ==> is_ref_map f C A"
apply (unfold is_weak_ref_map_def is_ref_map_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (case_tac "a:ext A")
-apply (rule transition_is_ex)
-apply (simp (no_asm_simp))
-apply (rule nothing_is_ex)
-apply simp
+apply (auto intro: transition_is_ex nothing_is_ex)
done
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Mar 20 12:09:20 2008 +0100
@@ -223,11 +223,11 @@
LastActExtsch A sch"
apply (unfold schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
apply (simp add: executions_def)
apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
apply (simp (no_asm_simp))
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Thu Mar 20 12:09:20 2008 +0100
@@ -174,14 +174,13 @@
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
(* cons case *)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rename_tac ex a t s s')
apply (simp add: mk_traceConc)
apply (frule reachable.reachable_n)
apply assumption
apply (erule_tac x = "t" in allE)
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
-apply simp
apply (simp add: move_subprop5_sim [unfolded Let_def]
move_subprop4_sim [unfolded Let_def] split add: split_if)
done
@@ -200,7 +199,7 @@
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
(* main case *)
-apply (tactic "safe_tac set_cs")
+apply auto
apply (rename_tac ex a t s s')
apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
@@ -262,7 +261,7 @@
apply (unfold traces_def)
apply (simp (no_asm) add: has_trace_def2)
- apply (tactic "safe_tac set_cs")
+ apply auto
(* give execution of abstract automata *)
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Thu Mar 20 12:09:20 2008 +0100
@@ -166,7 +166,7 @@
.--> (Next (Init (%(s,a,t).Q s))))"
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
apply (simp split add: split_if)
(* TL = UU *)
apply (rule conjI)
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Mar 20 12:09:20 2008 +0100
@@ -345,21 +345,7 @@
lemma has_trace_def2:
"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
-(* 1 *)
-apply (rule_tac x = "ex" in bexI)
-apply (simplesubst beta_cfun)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-(* 2 *)
-apply (rule_tac x = "filter_act$ (snd ex) " in bexI)
-apply (simplesubst beta_cfun)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
-apply (tactic "safe_tac set_cs")
-apply (rule_tac x = "ex" in bexI)
-apply simp_all
+apply auto
done
@@ -376,9 +362,7 @@
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
thm "Forall_def", thm "sforall_def"] 1 *})
(* main case *)
-apply (rename_tac ss a t)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: is_trans_of_def)
+apply (auto simp add: is_trans_of_def)
done
lemma exec_in_sig: