--- a/src/HOL/Filter.thy Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Filter.thy Sat Jul 18 20:47:08 2015 +0200
@@ -250,7 +250,7 @@
(Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
in
- CASES cases (rtac raw_elim_thm i)
+ CASES cases (resolve_tac ctxt [raw_elim_thm] i)
end)
*}
--- a/src/HOL/Library/Countable.thy Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Countable.thy Sat Jul 18 20:47:08 2015 +0200
@@ -186,10 +186,10 @@
val rules = @{thms finite_item.intros}
in
SOLVED' (fn i => EVERY
- [rtac @{thm countable_datatype} i,
- rtac typedef_thm i,
- etac induct_thm' i,
- REPEAT (resolve_tac ctxt rules i ORELSE atac i)]) 1
+ [resolve_tac ctxt @{thms countable_datatype} i,
+ resolve_tac ctxt [typedef_thm] i,
+ eresolve_tac ctxt [induct_thm'] i,
+ REPEAT (resolve_tac ctxt rules i ORELSE assume_tac ctxt i)]) 1
end)
\<close>
--- a/src/HOL/Library/Multiset.thy Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jul 18 20:47:08 2015 +0200
@@ -1898,23 +1898,25 @@
Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
mk_mset T [x] $ mk_mset T xs
- fun mset_member_tac m i =
+ fun mset_member_tac ctxt m i =
if m <= 0 then
- rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
+ resolve_tac ctxt @{thms multi_member_this} i ORELSE
+ resolve_tac ctxt @{thms multi_member_last} i
else
- rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i
-
- val mset_nonempty_tac =
- rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
+ resolve_tac ctxt @{thms multi_member_skip} i THEN mset_member_tac ctxt (m - 1) i
+
+ fun mset_nonempty_tac ctxt =
+ resolve_tac ctxt @{thms nonempty_plus} ORELSE'
+ resolve_tac ctxt @{thms nonempty_single}
fun regroup_munion_conv ctxt =
Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
(map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
- fun unfold_pwleq_tac i =
- (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
- ORELSE (rtac @{thm pw_leq_lstep} i)
- ORELSE (rtac @{thm pw_leq_empty} i)
+ fun unfold_pwleq_tac ctxt i =
+ (resolve_tac ctxt @{thms pw_leq_step} i THEN (fn st => unfold_pwleq_tac ctxt (i + 1) st))
+ ORELSE (resolve_tac ctxt @{thms pw_leq_lstep} i)
+ ORELSE (resolve_tac ctxt @{thms pw_leq_empty} i)
val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
@{thm Un_insert_left}, @{thm Un_empty_left}]
@@ -1925,7 +1927,7 @@
mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
- reduction_pair= @{thm ms_reduction_pair}
+ reduction_pair = @{thm ms_reduction_pair}
})
end
\<close>
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Sat Jul 18 20:47:08 2015 +0200
@@ -355,14 +355,14 @@
fun tag_rules thms = map_index (apsnd (pair NONE)) thms
fun tag_prems thms = map (pair ~1 o pair NONE) thms
- fun resolve (SOME thm) = rtac thm 1
- | resolve NONE = no_tac
+ fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
+ | resolve _ NONE = no_tac
fun tac prove ctxt rules =
CONVERSION (Old_SMT_Normalize.atomize_conv ctxt)
- THEN' rtac @{thm ccontr}
- THEN' SUBPROOF (fn {context, prems, ...} =>
- resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
+ THEN' resolve_tac ctxt @{thms ccontr}
+ THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
+ resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt
in
val smt_tac = tac safe_solve
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sat Jul 18 20:47:08 2015 +0200
@@ -33,7 +33,7 @@
fun prove_ite ctxt =
Old_Z3_Proof_Tools.by_tac ctxt (
CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
- THEN' rtac @{thm refl})
+ THEN' resolve_tac ctxt @{thms refl})
@@ -71,7 +71,7 @@
val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)]
in
Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
- |> apply (rtac @{thm injI})
+ |> apply (resolve_tac ctxt' @{thms injI})
|> apply (Tactic.solve_tac ctxt' [rule, rule RS @{thm sym}])
|> Goal.norm_result ctxt' o Goal.finish ctxt'
|> singleton (Variable.export ctxt' ctxt)
@@ -81,7 +81,7 @@
Old_Z3_Proof_Tools.by_tac ctxt (
CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
- THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
+ THEN' resolve_tac ctxt [@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]])
fun expand thm ct =
@@ -142,7 +142,7 @@
fun prove_injectivity ctxt =
Old_Z3_Proof_Tools.by_tac ctxt (
CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt))
- THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
+ THEN' CSUBGOAL (uncurry (resolve_tac ctxt o single o prove_inj_eq ctxt)))
end
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sat Jul 18 20:47:08 2015 +0200
@@ -413,7 +413,7 @@
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
- rtac thm ORELSE'
+ resolve_tac ctxt [thm] ORELSE'
(match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
(match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
@@ -602,7 +602,7 @@
in
fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
REPEAT_ALL_NEW (match_tac ctxt [rule])
- THEN' rtac @{thm excluded_middle})
+ THEN' resolve_tac ctxt @{thms excluded_middle})
end
@@ -640,10 +640,10 @@
apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
fun discharge_sk_tac ctxt i st = (
- rtac @{thm trans} i
+ resolve_tac ctxt @{thms trans} i
THEN resolve_tac ctxt sk_rules i
- THEN (rtac @{thm refl} ORELSE' discharge_sk_tac ctxt) (i+1)
- THEN rtac @{thm refl} i) st
+ THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1)
+ THEN resolve_tac ctxt @{thms refl} i) st
end
@@ -715,14 +715,14 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Old_Z3_Proof_Tools.by_tac ctxt' (
- (rtac @{thm iff_allI} ORELSE' K all_tac)
+ (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Old_Z3_Proof_Tools.by_tac ctxt' (
- (rtac @{thm iff_allI} ORELSE' K all_tac)
+ (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
@@ -731,7 +731,7 @@
Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Old_Z3_Proof_Tools.by_tac ctxt' (
- (rtac @{thm iff_allI} ORELSE' K all_tac)
+ (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sat Jul 18 20:47:08 2015 +0200
@@ -1007,12 +1007,12 @@
else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
in () end
-fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context, ...} =>
+fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context = ctxt, ...} =>
let
val _ = check_sos known_sos_constants concl
- val (ths, certificates) = real_sos prover context (Thm.dest_arg concl)
+ val (th, certificates) = real_sos prover ctxt (Thm.dest_arg concl)
val _ = print_cert certificates
- in rtac ths 1 end);
+ in resolve_tac ctxt [th] 1 end);
fun default_SOME _ NONE v = SOME v
| default_SOME _ (SOME v) _ = SOME v;
@@ -1050,7 +1050,7 @@
instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
(if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
- in rtac th i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
+ in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
--- a/src/HOL/Library/bnf_lfp_countable.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML Sat Jul 18 20:47:08 2015 +0200
@@ -29,11 +29,13 @@
fun meta_spec_mp_tac ctxt 0 = K all_tac
| meta_spec_mp_tac ctxt depth =
- dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' dtac ctxt meta_mp THEN' atac;
+ dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
+ dtac ctxt meta_mp THEN' assume_tac ctxt;
fun use_induction_hypothesis_tac ctxt =
DEEPEN (1, 64 (* large number *))
- (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN' atac THEN' atac) 0;
+ (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
+ assume_tac ctxt THEN' assume_tac ctxt) 0;
val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
id_apply snd_conv simp_thms};
@@ -44,7 +46,7 @@
(ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
- (atac ORELSE' use_induction_hypothesis_tac ctxt));
+ (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
fun distinct_ctrs_tac ctxt recs =
HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
--- a/src/HOL/Library/old_recdef.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Sat Jul 18 20:47:08 2015 +0200
@@ -262,19 +262,20 @@
struct
(* make a casethm from an induction thm *)
-val cases_thm_of_induct_thm =
- Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
+fun cases_thm_of_induct_thm ctxt =
+ Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
(* get the case_thm (my version) from a type *)
-fun case_thm_of_ty thy ty =
+fun case_thm_of_ty ctxt ty =
let
+ val thy = Proof_Context.theory_of ctxt
val ty_str = case ty of
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
| TVar((s,_),_) => error ("Free variable: " ^ s)
val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
in
- cases_thm_of_induct_thm induct
+ cases_thm_of_induct_thm ctxt induct
end;
@@ -287,7 +288,7 @@
val x = Free(vstr,ty);
val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
- val case_thm = case_thm_of_ty thy ty;
+ val case_thm = case_thm_of_ty ctxt ty;
val abs_ct = Thm.cterm_of ctxt abst;
val free_ct = Thm.cterm_of ctxt x;
@@ -2640,7 +2641,8 @@
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
fun meta_outer ctxt =
curry_rule ctxt o Drule.export_without_context o
- rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' etac conjE)));
+ rule_by_tactic ctxt
+ (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
(*Strip off the outer !P*)
val spec'=
--- a/src/HOL/List.thy Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/List.thy Sat Jul 18 20:47:08 2015 +0200
@@ -621,23 +621,25 @@
| NONE => NONE)
end
-fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
+fun tac ctxt [] =
+ resolve_tac ctxt [set_singleton] 1 ORELSE
+ resolve_tac ctxt [inst_Collect_mem_eq] 1
| tac ctxt (If :: cont) =
Splitter.split_tac ctxt @{thms split_if} 1
- THEN rtac @{thm conjI} 1
- THEN rtac @{thm impI} 1
+ THEN resolve_tac ctxt @{thms conjI} 1
+ THEN resolve_tac ctxt @{thms impI} 1
THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
CONVERSION (right_hand_set_comprehension_conv (K
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
then_conv
rewr_conv' @{lemma "(True \<and> P) = P" by simp})) ctxt') 1) ctxt 1
THEN tac ctxt cont
- THEN rtac @{thm impI} 1
+ THEN resolve_tac ctxt @{thms impI} 1
THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
CONVERSION (right_hand_set_comprehension_conv (K
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) ctxt') 1) ctxt 1
- THEN rtac set_Nil_I 1
+ THEN resolve_tac ctxt [set_Nil_I] 1
| tac ctxt (Case (T, i) :: cont) =
let
val SOME {injects, distincts, case_thms, split, ...} =
@@ -646,9 +648,9 @@
(* do case distinction *)
Splitter.split_tac ctxt [split] 1
THEN EVERY (map_index (fn (i', _) =>
- (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
- THEN REPEAT_DETERM (rtac @{thm allI} 1)
- THEN rtac @{thm impI} 1
+ (if i' < length case_thms - 1 then resolve_tac ctxt @{thms conjI} 1 else all_tac)
+ THEN REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1)
+ THEN resolve_tac ctxt @{thms impI} 1
THEN (if i' = i then
(* continue recursively *)
Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
@@ -683,7 +685,7 @@
Conv.repeat_conv
(Conv.bottom_conv
(K (rewr_conv' @{lemma "(\<exists>x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1
- THEN rtac set_Nil_I 1)) case_thms)
+ THEN resolve_tac ctxt [set_Nil_I] 1)) case_thms)
end
in
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Jul 18 20:47:08 2015 +0200
@@ -456,7 +456,7 @@
val wits = map (fn t => fold absfree (Term.add_frees t []) t)
(map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
- fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+ fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
@@ -547,7 +547,7 @@
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+ fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
@@ -629,7 +629,7 @@
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+ fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
@@ -883,8 +883,9 @@
(AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
(mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac ctxt = ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
- mk_simple_wit_tac (wit_thms_of_bnf bnf);
+ fun wit_tac ctxt =
+ ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
+ mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
val (bnf', lthy') =
bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -30,7 +30,7 @@
val mk_le_rel_OO_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
- val mk_simple_wit_tac: thm list -> tactic
+ val mk_simple_wit_tac: Proof.context -> thm list -> tactic
val mk_simplified_set_tac: Proof.context -> thm -> tactic
val bd_ordIso_natLeq_tac: tactic
end;
@@ -98,7 +98,7 @@
rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2},
rtac ctxt @{thm insertI1}, rtac ctxt (o_apply RS equalityD2 RS set_mp),
- etac ctxt @{thm imageI}, atac])
+ etac ctxt @{thm imageI}, assume_tac ctxt])
comp_set_alts))
map_cong0s) 1)
end;
@@ -158,8 +158,8 @@
unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
(REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
REPEAT_DETERM (CHANGED ((
- (rtac ctxt conjI THEN' (atac ORELSE' rtac ctxt subset_UNIV)) ORELSE'
- atac ORELSE'
+ (rtac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt subset_UNIV)) ORELSE'
+ assume_tac ctxt ORELSE'
(rtac ctxt subset_UNIV)) 1)) ORELSE rtac ctxt subset_UNIV 1));
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right
@@ -170,13 +170,13 @@
ALLGOALS (dtac ctxt @{thm in_Union_o_assoc}) THEN
unfold_thms_tac ctxt [collect_set_map] THEN
unfold_thms_tac ctxt comp_wit_thms THEN
- REPEAT_DETERM ((atac ORELSE'
+ REPEAT_DETERM ((assume_tac ctxt ORELSE'
REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN'
etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
(etac ctxt FalseE ORELSE'
hyp_subst_tac ctxt THEN'
dresolve_tac ctxt Fwit_thms THEN'
- (etac ctxt FalseE ORELSE' atac))) 1);
+ (etac ctxt FalseE ORELSE' assume_tac ctxt))) 1);
(* Kill operation *)
@@ -190,9 +190,9 @@
REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
rtac ctxt conjI THEN' rtac ctxt subset_UNIV) 1)) THEN
- (rtac ctxt subset_UNIV ORELSE' atac) 1 THEN
+ (rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN
REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
- REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' atac) 1))) ORELSE
+ REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE
((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1));
@@ -207,11 +207,11 @@
fun lift_in_alt_tac ctxt =
((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN
REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
- REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' atac) 1)) THEN
+ REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1)) THEN
REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN
- (rtac ctxt @{thm empty_subsetI} ORELSE' atac) 1) ORELSE
+ (rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE
((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1));
@@ -232,7 +232,8 @@
fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
-fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
+fun mk_simple_wit_tac ctxt wit_thms =
+ ALLGOALS (assume_tac ctxt ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
val csum_thms =
@{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -53,15 +53,15 @@
fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
fun mk_map_cong_tac ctxt cong0 =
(hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
- REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' atac)) 1;
+ REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
fun mk_in_mono_tac ctxt n = if n = 0 then rtac ctxt subset_UNIV 1
else (rtac ctxt subsetI THEN'
rtac ctxt CollectI) 1 THEN
REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN
REPEAT_DETERM_N (n - 1)
- ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' atac) 1) THEN
- (etac ctxt subset_trans THEN' atac) 1;
+ ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
+ (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
let
@@ -70,7 +70,7 @@
in
HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN'
REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
- REPEAT_DETERM_N n o atac))
+ REPEAT_DETERM_N n o assume_tac ctxt))
end;
fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
@@ -104,10 +104,12 @@
REPEAT_DETERM o
eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
- REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, atac],
+ REPEAT_DETERM_N n o
+ EVERY' [rtac ctxt @{thm Collect_split_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
rtac ctxt CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
- rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD}, etac ctxt @{thm set_mp}, atac])
+ rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_split_Grp_inD},
+ etac ctxt @{thm set_mp}, assume_tac ctxt])
set_maps,
rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
hyp_subst_tac ctxt,
@@ -120,7 +122,7 @@
rtac ctxt CollectI,
CONJ_WRAP' (fn thm =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
- rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, atac])
+ rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
set_maps])
@{thms fst_convol snd_convol} [map_id, refl])] 1
end;
@@ -146,11 +148,11 @@
unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
- CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, atac,
+ CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt,
rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
- dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, atac])
+ dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
end;
fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono =
@@ -194,7 +196,7 @@
val n = length set_maps;
fun in_tac nthO_in = rtac ctxt CollectI THEN'
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
- rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, atac]) set_maps;
+ rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
rtac ctxt (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
@@ -213,8 +215,8 @@
rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
rtac ctxt ballE, rtac ctxt subst,
- rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, atac, etac ctxt notE,
- etac ctxt set_mp, atac],
+ rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
+ etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
in_tac @{thm fstOp_in},
rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
@@ -226,14 +228,14 @@
end;
fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
- if null set_maps then atac 1
+ if null set_maps then assume_tac ctxt 1
else
unfold_tac ctxt [in_rel] THEN
REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN
hyp_subst_tac ctxt 1 THEN
EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
CONJ_WRAP' (fn thm =>
- (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
+ (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt))
set_maps] 1;
fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong =
@@ -241,7 +243,7 @@
fun last_tac iffD =
HEADGOAL (etac ctxt rel_mono_strong) THEN
REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN'
- REPEAT_DETERM o atac));
+ REPEAT_DETERM o assume_tac ctxt));
in
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
@@ -262,7 +264,8 @@
in
REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
- HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono, REPEAT_DETERM_N n o atac,
+ HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
+ REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt,
rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
@@ -316,12 +319,12 @@
else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI})
- (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps,
+ (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps,
rtac ctxt sym,
rtac ctxt (Drule.rotate_prems 1
((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
map_comp RS sym, map_id]) RSN (2, trans))),
- REPEAT_DETERM_N (2 * live) o atac,
+ REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
rtac ctxt refl,
rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
@@ -335,8 +338,10 @@
end;
fun mk_trivial_wit_tac ctxt wit_defs set_maps =
- unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
- dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
+ unfold_thms_tac ctxt wit_defs THEN
+ HEADGOAL (EVERY' (map (fn thm =>
+ dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN
+ ALLGOALS (assume_tac ctxt);
fun mk_set_transfer_tac ctxt in_rel set_maps =
Goal.conjunction_tac 1 THEN
@@ -345,7 +350,7 @@
@{thms exE conjE CollectE}))) THEN
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
rtac ctxt @{thm rel_setI}) THEN
- REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' atac THEN'
+ REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -113,39 +113,40 @@
unfold_thms_tac ctxt cases THEN
ALLGOALS (fn k => (select_prem_tac ctxt n (dtac ctxt asm_rl) k) k) THEN
ALLGOALS (REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt rel_funD THEN'
- (atac THEN' etac ctxt thin_rl ORELSE' rtac ctxt refl)) THEN' atac)
+ (assume_tac ctxt THEN' etac ctxt thin_rl ORELSE' rtac ctxt refl)) THEN' assume_tac ctxt)
end;
fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
HEADGOAL Goal.conjunction_tac THEN
ALLGOALS (REPEAT o (resolve_tac ctxt (rel_funI :: rel_intros) THEN'
- TRY o (REPEAT_DETERM1 o (atac ORELSE'
+ TRY o (REPEAT_DETERM1 o (assume_tac ctxt ORELSE'
K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac ctxt refl))));
fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc =
let
fun last_disc_tac iffD =
- HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' atac THEN'
- REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN' atac THEN'
- rotate_tac ~1 THEN' etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
+ HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' assume_tac ctxt THEN'
+ REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN'
+ assume_tac ctxt THEN' rotate_tac ~1 THEN'
+ etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
in
HEADGOAL Goal.conjunction_tac THEN
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI THEN' dtac ctxt (rel_sel RS iffD1) THEN'
- REPEAT_DETERM o (etac ctxt conjE) THEN' (atac ORELSE' rtac ctxt iffI))) THEN
+ REPEAT_DETERM o (etac ctxt conjE) THEN' (assume_tac ctxt ORELSE' rtac ctxt iffI))) THEN
TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
end;
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac ctxt sumEN') THEN
HEADGOAL (EVERY' (maps (fn k => [select_prem_tac ctxt n (rotate_tac 1) k,
- REPEAT_DETERM o dtac ctxt meta_spec, etac ctxt meta_mp, atac]) (1 upto n)));
+ REPEAT_DETERM o dtac ctxt meta_spec, etac ctxt meta_mp, assume_tac ctxt]) (1 upto n)));
fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
HEADGOAL (rtac ctxt iffI THEN'
EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
dtac ctxt (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
- atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
+ assume_tac ctxt) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs =
unfold_thms_tac ctxt (ctor_inject :: abs_inject :: @{thms sum.inject} @ ctr_defs) THEN
@@ -204,7 +205,7 @@
[mk_rel_funDN 2 case_sum_transfer_eq, mk_rel_funDN 2 case_sum_transfer])) THEN
HEADGOAL (select_prem_tac ctxt total_n (dtac ctxt asm_rl) (acc + n)) THEN
HEADGOAL (SELECT_GOAL (HEADGOAL
- (REPEAT_DETERM o (atac ORELSE' resolve_tac ctxt
+ (REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt
[mk_rel_funDN 1 case_prod_transfer_eq,
mk_rel_funDN 1 case_prod_transfer,
rel_funI]) THEN_ALL_NEW
@@ -255,12 +256,12 @@
HEADGOAL (Inl_Inr_Pair_tac THEN'
rtac ctxt (mk_rel_funDN 3 @{thm If_transfer}) THEN'
select_prem_tac ctxt total (dtac ctxt asm_rl) pos THEN'
- dtac ctxt rel_funD THEN' atac THEN' atac);
+ dtac ctxt rel_funD THEN' assume_tac ctxt THEN' assume_tac ctxt);
fun mk_unfold_Inl_Inr_Pair_tac total pos =
HEADGOAL (Inl_Inr_Pair_tac THEN'
select_prem_tac ctxt total (dtac ctxt asm_rl) pos THEN'
- dtac ctxt rel_funD THEN' atac THEN' atac);
+ dtac ctxt rel_funD THEN' assume_tac ctxt THEN' assume_tac ctxt);
fun mk_unfold_arg_tac qs gs =
EVERY (map (mk_unfold_If_tac num_pgs o prem_no_of) qs) THEN
@@ -307,7 +308,7 @@
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
- (rtac ctxt refl ORELSE' atac ORELSE' rtac ctxt @{thm singletonI});
+ (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
pre_set_defs =
@@ -323,7 +324,7 @@
REPEAT_DETERM_N m o (dtac ctxt meta_spec THEN' rotate_tac ~1)]) THEN
EVERY [REPEAT_DETERM_N r
(HEADGOAL (rotate_tac ~1 THEN' dtac ctxt meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
- if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
+ if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL (assume_tac ctxt),
mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
pre_set_defs]
end;
@@ -349,10 +350,10 @@
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
- (atac ORELSE' REPEAT o etac ctxt conjE THEN'
+ (assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
REPEAT o etac ctxt conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
- REPEAT o (resolve_tac ctxt [refl, conjI] ORELSE' atac));
+ REPEAT o (resolve_tac ctxt [refl, conjI] ORELSE' assume_tac ctxt));
fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
let
@@ -367,8 +368,8 @@
dtor_ctor exhaust ctr_defs discss selss =
let val ks = 1 upto n in
EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
- dtac ctxt meta_spec, dtac ctxt meta_mp, atac, rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
- hyp_subst_tac ctxt] @
+ dtac ctxt meta_spec, dtac ctxt meta_mp, assume_tac ctxt, rtac ctxt exhaust,
+ K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @
@{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
map2 (fn k' => fn discs' =>
@@ -413,7 +414,7 @@
True_implies_equals conj_imp_eq_imp_imp} @
map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
map (fn thm => thm RS eqTrueI) rel_injects) THEN
- TRYALL (atac ORELSE' etac ctxt FalseE ORELSE'
+ TRYALL (assume_tac ctxt ORELSE' etac ctxt FalseE ORELSE'
(REPEAT_DETERM o dtac ctxt @{thm meta_spec} THEN'
TRY o filter_prems_tac ctxt
(forall (curry (op <>) (HOLogic.mk_Trueprop @{term False})) o Logic.strip_imp_prems) THEN'
@@ -427,7 +428,7 @@
(rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
(dtac ctxt (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
@{thm arg_cong2} RS iffD1)) THEN'
- atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
+ assume_tac ctxt THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
REPEAT_DETERM o etac ctxt conjE))) 1 THEN
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
@@ -435,7 +436,7 @@
@{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN'
- (rtac ctxt refl ORELSE' atac))))
+ (rtac ctxt refl ORELSE' assume_tac ctxt))))
cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
abs_inverses);
@@ -445,13 +446,14 @@
fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
(rtac ctxt (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
- THEN' atac THEN' atac THEN' TRY o resolve_tac ctxt assms))) THEN
+ THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
@{thms id_bnf_def vimage2p_def}) THEN
TRYALL (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
Inr_Inl_False sum.inject prod.inject}) THEN
- TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE' (REPEAT_DETERM o etac ctxt conjE) THEN' atac))
+ TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE'
+ (REPEAT_DETERM o etac ctxt conjE) THEN' assume_tac ctxt))
cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs =
@@ -467,7 +469,7 @@
TRYALL Goal.conjunction_tac THEN
unfold_thms_tac ctxt (map (Drule.abs_def o Local_Defs.meta_rewrite_rule ctxt) sel_defs) THEN
ALLGOALS (rtac ctxt (mk_rel_funDN n case_transfer) THEN_ALL_NEW
- REPEAT_DETERM o (atac ORELSE' rtac ctxt rel_funI));
+ REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt rel_funI));
fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
TRYALL Goal.conjunction_tac THEN
@@ -480,7 +482,7 @@
ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE'
eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE'
hyp_subst_tac ctxt) THEN'
- (rtac ctxt @{thm singletonI} ORELSE' atac));
+ (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
fun mk_set_cases_tac ctxt ct assms exhaust sets =
HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
@@ -488,13 +490,14 @@
REPEAT_DETERM (HEADGOAL
(eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
hyp_subst_tac ctxt ORELSE'
- SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o atac)))));
+ SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o assume_tac ctxt)))));
fun mk_set_intros_tac ctxt sets =
TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
TRYALL (REPEAT o
(resolve_tac ctxt @{thms UnI1 UnI2} ORELSE'
- eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN' (rtac ctxt @{thm singletonI} ORELSE' atac));
+ eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN'
+ (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
Abs_pre_inverses =
@@ -502,7 +505,7 @@
val assms_tac =
let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
fold (curry (op ORELSE')) (map (fn thm =>
- funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' atac) (rtac ctxt thm)) assms')
+ funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms')
(etac ctxt FalseE)
end;
val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
@@ -512,7 +515,7 @@
TRYALL (resolve_tac ctxt exhausts' THEN_ALL_NEW
(resolve_tac ctxt (map (fn ct => refl RS
cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
- THEN' atac THEN' hyp_subst_tac ctxt)) THEN
+ THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt)) THEN
unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
@{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
Un_empty_right empty_iff singleton_iff}) THEN
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -53,33 +53,34 @@
val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
-fun distinct_in_prems_tac distincts =
- eresolve0_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
+fun distinct_in_prems_tac ctxt distincts =
+ eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
+ assume_tac ctxt;
fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
let val ks = 1 upto n in
- HEADGOAL (atac ORELSE'
+ HEADGOAL (assume_tac ctxt ORELSE'
cut_tac nchotomy THEN'
K (exhaust_inst_as_projs_tac ctxt frees) THEN'
EVERY' (map (fn k =>
(if k < n then etac ctxt disjE else K all_tac) THEN'
- REPEAT o (dtac ctxt meta_mp THEN' atac ORELSE'
- etac ctxt conjE THEN' dtac ctxt meta_mp THEN' atac ORELSE'
- atac))
+ REPEAT o (dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
+ etac ctxt conjE THEN' dtac ctxt meta_mp THEN' assume_tac ctxt ORELSE'
+ assume_tac ctxt))
ks))
end;
fun mk_primcorec_assumption_tac ctxt discIs =
SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
- SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' atac ORELSE' etac ctxt conjE ORELSE'
+ SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE'
eresolve_tac ctxt falseEs ORELSE'
resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
- dresolve_tac ctxt discIs THEN' atac ORELSE'
- etac ctxt notE THEN' atac ORELSE'
+ dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
+ etac ctxt notE THEN' assume_tac ctxt ORELSE'
etac ctxt disjE))));
fun ss_fst_snd_conv ctxt =
@@ -120,15 +121,16 @@
EVERY' (map (fn [] => etac ctxt FalseE
| fun_discs' as [fun_disc'] =>
if eq_list Thm.eq_thm (fun_discs', fun_discs) then
- REPEAT_DETERM o etac ctxt conjI THEN' (atac ORELSE' rtac ctxt TrueI)
+ REPEAT_DETERM o etac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt TrueI)
else
rtac ctxt FalseE THEN'
- (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o atac ORELSE'
+ (rotate_tac 1 THEN' dtac ctxt fun_disc' THEN' REPEAT o assume_tac ctxt ORELSE'
cut_tac fun_disc') THEN'
- dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' atac)
+ dresolve_tac ctxt distinct_discs THEN' etac ctxt notE THEN' assume_tac ctxt)
fun_discss) THEN'
(etac ctxt FalseE ORELSE'
- resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
+ resolve_tac ctxt
+ (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
m excludesss =
@@ -139,8 +141,8 @@
resolve_tac ctxt split_connectI ORELSE'
Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
Splitter.split_tac ctxt (split_if :: splits) ORELSE'
- eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
- etac ctxt notE THEN' atac ORELSE'
+ eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE'
+ etac ctxt notE THEN' assume_tac ctxt ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
mapsx @ map_ident0s @ map_comps))) ORELSE'
@@ -150,7 +152,7 @@
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
- (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
+ (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN
unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
fun inst_split_eq ctxt split =
@@ -174,13 +176,13 @@
prelude_tac ctxt [] (fun_ctr RS trans) THEN
HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
- (rtac ctxt refl ORELSE' atac ORELSE'
+ (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
Splitter.split_tac ctxt (split_if :: splits) ORELSE'
Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
mk_primcorec_assumption_tac ctxt discIs ORELSE'
- distinct_in_prems_tac distincts ORELSE'
- (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' atac)))))
+ distinct_in_prems_tac ctxt distincts ORELSE'
+ (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
end;
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
@@ -207,11 +209,11 @@
fun mk_primcorec_code_tac ctxt distincts splits raw =
HEADGOAL (rtac ctxt raw ORELSE' rtac ctxt (raw RS trans) THEN'
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
- (rtac ctxt refl ORELSE' atac ORELSE'
+ (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
resolve_tac ctxt split_connectI ORELSE'
Splitter.split_tac ctxt (split_if :: splits) ORELSE'
- distinct_in_prems_tac distincts ORELSE'
- rtac ctxt sym THEN' atac ORELSE'
- etac ctxt notE THEN' atac));
+ distinct_in_prems_tac ctxt distincts ORELSE'
+ rtac ctxt sym THEN' assume_tac ctxt ORELSE'
+ etac ctxt notE THEN' assume_tac ctxt));
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -116,15 +116,15 @@
fun mk_coalg_set_tac ctxt coalg_def =
dtac ctxt (coalg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac ctxt conjE 1) THEN
- EVERY' [dtac ctxt rev_bspec, atac] 1 THEN
- REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN atac 1;
+ EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
+ REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN assume_tac ctxt 1;
fun mk_mor_elim_tac ctxt mor_def =
(dtac ctxt (mor_def RS iffD1) THEN'
REPEAT o etac ctxt conjE THEN'
TRY o rtac ctxt @{thm image_subsetI} THEN'
etac ctxt bspec THEN'
- atac) 1;
+ assume_tac ctxt) 1;
fun mk_mor_incl_tac ctxt mor_def map_ids =
(rtac ctxt (mor_def RS iffD2) THEN'
@@ -137,10 +137,11 @@
fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
let
fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
- etac ctxt image, atac];
+ etac ctxt image, assume_tac ctxt];
fun mor_tac ((mor_image, morE), map_comp_id) =
EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
- etac ctxt (morE RS arg_cong), atac, etac ctxt morE, etac ctxt mor_image, atac];
+ etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
+ etac ctxt mor_image, assume_tac ctxt];
in
(rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
CONJ_WRAP' fbetw_tac mor_images THEN'
@@ -171,7 +172,7 @@
fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2,
- rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, atac]) 1;
+ rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
@@ -185,13 +186,13 @@
else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
(K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
- rtac ctxt subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
+ rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
rec_Sucs] 1;
fun mk_Jset_minimal_tac ctxt n col_minimal =
(CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal,
EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI,
- REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], atac])) (1 upto n)) 1
+ REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
@@ -204,14 +205,16 @@
if m = 0 then K all_tac
else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals},
rtac ctxt (nth passive_set_map0s (j - 1) RS sym),
- rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong), atac],
+ rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong),
+ assume_tac ctxt],
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
(fn (i, (set_map0, coalg_set)) =>
EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
- etac ctxt (morE RS sym RS arg_cong RS trans), atac, rtac ctxt set_map0,
+ etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
- ftac ctxt coalg_set, atac, dtac ctxt set_mp, atac, rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
- REPEAT_DETERM o etac ctxt allE, atac, atac])
+ ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
+ rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
+ REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
@@ -222,12 +225,12 @@
fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
- etac ctxt allE, etac ctxt allE, etac ctxt impE, atac, etac ctxt bexE,
+ etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
- atac])
+ assume_tac ctxt])
@{thms fst_diag_id snd_diag_id},
rtac ctxt CollectI,
CONJ_WRAP' (fn (i, thm) =>
@@ -241,24 +244,24 @@
fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
- etac ctxt allE, etac ctxt allE, etac ctxt impE, atac,
+ etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
dtac ctxt (in_rel RS @{thm iffD1}),
REPEAT_DETERM o eresolve0_tac ([CollectE, conjE, exE] @
@{thms CollectE Collect_split_in_rel_leE}),
rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
- atac, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
+ assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
rtac ctxt trans, rtac ctxt map_cong0,
- REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, atac],
+ REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt],
REPEAT_DETERM_N n o rtac ctxt refl,
- atac, rtac ctxt CollectI,
+ assume_tac ctxt, rtac ctxt CollectI,
CONJ_WRAP' (fn (i, thm) =>
if i <= m then rtac ctxt subset_UNIV
else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
- rtac ctxt trans_fun_cong_image_id_id_apply, atac])
+ rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt])
(1 upto (m + n) ~~ set_map0s)];
in
EVERY' [rtac ctxt (bis_def RS trans),
@@ -283,7 +286,7 @@
fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs =
EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1),
REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
- CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, atac])) rel_congs,
+ CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs,
CONJ_WRAP' (fn (rel_cong, le_rel_OO) =>
EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
@@ -294,7 +297,7 @@
REPEAT_DETERM o dtac ctxt prod_injectD,
etac ctxt conjE, hyp_subst_tac ctxt,
REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI},
- etac ctxt mp, atac, etac ctxt mp, atac]) (rel_congs ~~ le_rel_OOs)] 1;
+ etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1;
fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
@@ -313,14 +316,15 @@
unfold_thms_tac ctxt [bis_def] THEN
EVERY' [rtac ctxt conjI,
CONJ_WRAP' (fn i =>
- EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, atac,
+ EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt,
dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
CONJ_WRAP' (fn (i, in_mono) =>
- EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E}, dtac ctxt bspec, atac,
+ EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
+ dtac ctxt bspec, assume_tac ctxt,
dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
- atac, etac ctxt bexE, rtac ctxt bexI, atac, rtac ctxt in_mono,
+ assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono,
REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
- atac]) (ks ~~ in_monos)] 1
+ assume_tac ctxt]) (ks ~~ in_monos)] 1
end;
fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
@@ -334,15 +338,15 @@
fun mk_incl_lsbis_tac ctxt n i lsbis_def =
EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI,
- REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, atac, rtac ctxt equalityD2,
- rtac ctxt (mk_nth_conv n i)] 1;
+ REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
+ rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2),
rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2),
rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp,
- rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, atac, etac ctxt @{thm Id_onI},
+ rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},
rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2),
rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp,
@@ -351,7 +355,7 @@
rtac ctxt (@{thm trans_def} RS iffD2),
rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp,
rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
- etac ctxt @{thm relcompI}, atac] 1;
+ etac ctxt @{thm relcompI}, assume_tac ctxt] 1;
fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
let
@@ -369,20 +373,20 @@
etac ctxt equalityD1, etac ctxt CollectD,
rtac ctxt ballI,
CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD},
- dtac ctxt bspec, etac ctxt thin_rl, atac, dtac ctxt (mk_conjunctN n i),
+ dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
- rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
+ rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
- dtac ctxt bspec, atac, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
- etac ctxt @{thm set_mp[OF equalityD1]}, atac,
+ dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
+ etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans),
- REPEAT_DETERM_N m o (rtac ctxt conjI THEN' atac),
+ REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
@@ -408,12 +412,13 @@
(fn i =>
EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
- REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), etac ctxt mp, atac]) ks])
+ REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
+ etac ctxt mp, assume_tac ctxt]) ks])
Lev_Sucs] 1
end;
fun mk_length_Lev'_tac ctxt length_Lev =
- EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, atac] 1;
+ EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1;
fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
let
@@ -434,7 +439,7 @@
CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI,
rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans),
if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans),
- rtac ctxt (mk_sum_caseN n i RS trans), atac])
+ rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt])
ks])
rv_Conss)
ks)] 1
@@ -474,12 +479,12 @@
EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp),
rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
- rtac ctxt conjI, atac, dtac ctxt (sym RS trans RS sym),
+ rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
- dtac ctxt (mk_conjunctN n i), dtac ctxt mp, atac,
- dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, atac,
- dtac ctxt (mk_conjunctN n i''), etac ctxt mp, atac])
+ dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
+ dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
+ dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt])
ks)
ks])
(rev (ks ~~ from_to_sbds))])
@@ -528,14 +533,14 @@
(if k = i
then EVERY' [dtac ctxt (mk_InN_inject n i),
dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
- atac, atac, hyp_subst_tac ctxt] THEN'
+ assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans),
rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans),
etac ctxt (from_to_sbd RS arg_cong),
REPEAT_DETERM o etac ctxt allE,
- dtac ctxt (mk_conjunctN n i), dtac ctxt mp, atac,
- dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, atac,
+ dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
+ dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym])
ks
else etac ctxt (mk_InN_not_InM i k RS notE)))
@@ -572,13 +577,13 @@
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev,
- if n = 1 then rtac ctxt refl else atac, atac, rtac ctxt subsetI,
+ if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
REPEAT_DETERM_N 4 o etac ctxt thin_rl,
rtac ctxt set_image_Lev,
- atac, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
+ assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
- if n = 1 then rtac ctxt refl else atac])
+ if n = 1 then rtac ctxt refl else assume_tac ctxt])
(drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
(ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
(set_Levss ~~ set_image_Levss))))),
@@ -591,7 +596,7 @@
EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev,
rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
- atac, rtac ctxt subsetI,
+ assume_tac ctxt, rtac ctxt subsetI,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
@@ -621,12 +626,12 @@
dtac ctxt list_inject_iffD1, etac ctxt conjE,
if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
- atac, atac, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
+ assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]},
rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI,
- REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, atac,
+ REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
@@ -653,7 +658,7 @@
etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
EVERY' (map (fn equiv_LSBIS =>
- EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, atac])
+ EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt])
equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans),
etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1;
@@ -673,11 +678,12 @@
fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
CONJ_WRAP' (fn equiv_LSBIS =>
- EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, rtac ctxt equiv_LSBIS, atac])
+ EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
+ rtac ctxt equiv_LSBIS, assume_tac ctxt])
equiv_LSBISs,
CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
- rtac ctxt congruent_str_final, atac, rtac ctxt o_apply])
+ rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
(equiv_LSBISs ~~ congruent_str_finals)] 1;
fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
@@ -716,7 +722,8 @@
in
EVERY' [rtac ctxt rev_mp, ftac ctxt (bis_def RS iffD1),
REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
- rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, atac, rtac ctxt bis_Gr, rtac ctxt tcoalg,
+ rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
+ rtac ctxt bis_Gr, rtac ctxt tcoalg,
rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr},
rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT,
rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT,
@@ -728,7 +735,7 @@
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
- rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, atac,
+ rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
rtac ctxt Rep_inject])
(Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
@@ -787,7 +794,7 @@
EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE,
- EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, atac]) set_Jset_Jsets)])
+ EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
(1 upto n) set_Jsets set_Jset_Jsetss)] 1;
fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets =
@@ -840,7 +847,7 @@
rtac ctxt CollectI, etac ctxt CollectE,
REPEAT_DETERM o etac ctxt conjE,
CONJ_WRAP' (fn set_Jset_Jset =>
- EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, atac]) set_Jset_Jsets,
+ EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
rtac ctxt (conjI OF [refl, refl])])
(drop m set_map0s ~~ set_Jset_Jsetss)])
(map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
@@ -912,7 +919,7 @@
fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
- REPEAT_DETERM (atac 1 ORELSE
+ REPEAT_DETERM (assume_tac ctxt 1 ORELSE
EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
K (unfold_thms_tac ctxt dtor_ctors),
REPEAT_DETERM_N n o etac ctxt UnE,
@@ -966,14 +973,14 @@
CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
- CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
+ CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
(in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
- rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), atac])
+ rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
@{thms fst_conv snd_conv}];
val only_if_tac =
EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
@@ -981,7 +988,7 @@
CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
- rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, atac,
+ rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
@@ -993,20 +1000,20 @@
hyp_subst_tac ctxt,
dtac ctxt (in_Jrel RS iffD1),
dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], atac])
+ REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
(rev (active_set_map0s ~~ in_Jrels))])
(dtor_sets ~~ passive_set_map0s),
rtac ctxt conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map,
rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
- EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, atac,
+ EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
- dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, atac]) in_Jrels),
- atac]]
+ dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
+ assume_tac ctxt]]
in
EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
end;
@@ -1023,7 +1030,7 @@
fn dtor_unfold => fn dtor_map => fn in_rel =>
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
- select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
+ select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
@@ -1039,8 +1046,8 @@
CONJ_WRAP' (fn set_map0 =>
EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI},
- FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, atac,
- rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
+ FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
+ assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
set_map0s])
ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1
end;
@@ -1053,7 +1060,7 @@
rtac ctxt set_induct 1 THEN
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
- select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
+ select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
@@ -1062,11 +1069,12 @@
EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
EVERY' (map (fn set_map0 =>
EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
- select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, atac,
+ select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
- rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, atac, rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
+ rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
+ rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
(drop m set_map0s)))
unfolds set_map0ss ks) 1
end;
@@ -1082,16 +1090,18 @@
if null helper_inds then rtac ctxt UNIV_I
else rtac ctxt CollectI THEN'
CONJ_WRAP' (fn helper_ind =>
- EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
+ EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
- dtac ctxt bspec, atac, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
+ dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
etac ctxt (refl RSN (2, conjI))])
helper_inds,
rtac ctxt conjI,
- rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac ctxt thin_rl,
+ rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
+ REPEAT_DETERM_N n o etac ctxt thin_rl,
rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)),
- rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac ctxt thin_rl,
+ rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
+ REPEAT_DETERM_N n o etac ctxt thin_rl,
rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))])
(in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -92,7 +92,7 @@
fun mk_alg_set_tac ctxt alg_def =
EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
- REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), atac] 1;
+ REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
(EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
@@ -100,7 +100,7 @@
[EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
- FIRST' (map (fn thm => rtac ctxt thm THEN' atac) alg_sets)]] THEN'
+ FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
etac ctxt @{thm emptyE}) 1;
fun mk_mor_elim_tac ctxt mor_def =
@@ -108,7 +108,7 @@
REPEAT o etac ctxt conjE THEN'
TRY o rtac ctxt @{thm image_subsetI} THEN'
etac ctxt bspec THEN'
- atac) 1;
+ assume_tac ctxt) 1;
fun mk_mor_incl_tac ctxt mor_def map_ids =
(rtac ctxt (mor_def RS iffD2) THEN'
@@ -121,15 +121,16 @@
fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids =
let
val fbetw_tac =
- EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt bspec, etac ctxt bspec, atac];
+ EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
+ etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
fun mor_tac (set_map, map_comp_id) =
EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
- rtac ctxt trans, dtac ctxt rev_bspec, atac, etac ctxt arg_cong,
+ rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
REPEAT o eresolve0_tac [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
CONJ_WRAP' (fn thm =>
FIRST' [rtac ctxt subset_UNIV,
(EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
- etac ctxt bspec, etac ctxt set_mp, atac])]) set_map THEN'
+ etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
rtac ctxt (map_comp_id RS arg_cong);
in
(dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
@@ -195,11 +196,12 @@
CONJ_WRAP' (fn i =>
EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
(0 upto n - 1),
- atac] 1;
+ assume_tac ctxt] 1;
fun mk_min_algs_tac ctxt worel in_congs =
let
- val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec, atac, etac ctxt arg_cong];
+ val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
+ assume_tac ctxt, etac ctxt arg_cong];
fun minH_tac thm =
EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl];
@@ -212,8 +214,9 @@
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
- rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, atac, atac, rtac ctxt equalityD1,
- dtac ctxt @{thm notnotD}, hyp_subst_tac ctxt, rtac ctxt refl] 1;
+ rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
+ assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
+ hyp_subst_tac ctxt, rtac ctxt refl] 1;
fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
@@ -236,8 +239,10 @@
val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
- atac, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
- dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT o etac ctxt conjE, atac, rtac ctxt Asuc_Cinfinite]
+ assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
+ dtac ctxt mp, etac ctxt @{thm underS_E},
+ dtac ctxt mp, etac ctxt @{thm underS_Field},
+ REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans},
rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound},
@@ -265,8 +270,9 @@
val induct = worel RS
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
- val minG_tac = EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
- dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, atac];
+ val minG_tac =
+ EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
+ dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt];
fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
@@ -288,15 +294,17 @@
fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
- rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, atac,
+ rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
- rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl, atac, rtac ctxt set_mp,
- rtac ctxt equalityD2, rtac ctxt min_alg, atac, rtac ctxt UnI2, rtac ctxt @{thm image_eqI}, rtac ctxt refl,
+ rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
+ assume_tac ctxt, rtac ctxt set_mp,
+ rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
+ rtac ctxt @{thm image_eqI}, rtac ctxt refl,
rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
REPEAT_DETERM o etac ctxt conjE,
- CONJ_WRAP' (K (FIRST' [atac,
+ CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
- etac ctxt @{thm underS_I}, atac, atac]]))
+ etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
set_bds];
in
(rtac ctxt (alg_def RS iffD2) THEN'
@@ -307,24 +315,27 @@
EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
- rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of, REPEAT_DETERM o etac ctxt conjE, atac,
- rtac ctxt Asuc_Cinfinite] 1;
+ rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
+ REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
fun mk_least_min_alg_tac ctxt min_alg_def least =
- EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least}, dtac ctxt least, dtac ctxt mp, atac,
- REPEAT_DETERM o etac ctxt conjE, atac] 1;
+ EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least},
+ dtac ctxt least, dtac ctxt mp, assume_tac ctxt,
+ REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
fun mk_alg_select_tac ctxt Abs_inverse =
EVERY' [rtac ctxt ballI,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
- unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
+ unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
set_maps str_init_defs =
let
val n = length alg_sets;
val fbetw_tac =
- CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec, etac ctxt CollectE, atac])) alg_sets;
+ CONJ_WRAP'
+ (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
+ etac ctxt CollectE, assume_tac ctxt])) alg_sets;
val mor_tac =
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
fun alg_epi_tac ((alg_set, str_init_def), set_map) =
@@ -332,7 +343,7 @@
rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve0_tac set_map,
rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
- atac]];
+ assume_tac ctxt]];
in
EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp),
@@ -345,10 +356,11 @@
val n = length card_of_min_algs;
in
EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
- REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy, REPEAT_DETERM_N n o atac,
+ REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
+ REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt impI, REPEAT_DETERM o eresolve0_tac [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
- rtac ctxt conjI, rtac ctxt refl, atac,
+ rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
end;
@@ -361,11 +373,11 @@
fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
- REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' atac)];
+ REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
fun cong_tac ct map_cong0 = EVERY'
[rtac ctxt (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
REPEAT_DETERM_N m o rtac ctxt refl,
- REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' atac)];
+ REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
@@ -391,9 +403,10 @@
REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
- REPEAT_DETERM_N m o (rtac ctxt conjI THEN' atac),
+ REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
- CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' atac)) alg_sets];
+ CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
+ alg_sets];
fun mk_induct_tac least_min_alg =
rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
@@ -422,7 +435,8 @@
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
rtac ctxt (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
EVERY' (map (fn Abs_inverse =>
- EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse), atac])
+ EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
+ assume_tac ctxt])
Abs_inverses)])
(cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
@@ -436,8 +450,8 @@
fun mk_unique type_def =
EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
rtac ctxt ballI, resolve0_tac init_unique_mors,
- EVERY' (map (fn thm => atac ORELSE' rtac ctxt thm) Reps),
- rtac ctxt mor_comp, rtac ctxt mor_Abs, atac,
+ EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
+ rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
in
CONJ_WRAP' mk_unique type_defs 1
@@ -469,13 +483,14 @@
fun mk_IH_tac Rep_inv Abs_inv set_map =
DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
- hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp, atac, atac];
+ hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
+ assume_tac ctxt, assume_tac ctxt];
fun mk_closed_tac (k, (morE, set_maps)) =
EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
- rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), atac,
+ rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
- EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
+ EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
fun mk_induct_tac (Rep, Rep_inv) =
EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
@@ -495,13 +510,14 @@
select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i,
REPEAT_DETERM_N n o
EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
- REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp), atac],
- atac];
+ REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp),
+ assume_tac ctxt],
+ assume_tac ctxt];
in
EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct),
EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
- CONJ_WRAP' (K atac) ks] 1
+ CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
end;
fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 =
@@ -515,7 +531,7 @@
fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
rtac ctxt fold_unique 1 THEN
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
- ALLGOALS atac;
+ ALLGOALS (assume_tac ctxt);
fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1;
@@ -592,8 +608,8 @@
EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}),
REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
- rtac ctxt @{thm relcomppI}, atac, atac,
- REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, atac],
+ rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
+ REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
REPEAT_DETERM_N (length le_rel_OOs) o
EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
@@ -627,7 +643,7 @@
CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1;
fun mk_wit_tac ctxt n ctor_set wit =
- REPEAT_DETERM (atac 1 ORELSE
+ REPEAT_DETERM (assume_tac ctxt 1 ORELSE
EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
REPEAT_DETERM o
(TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
@@ -676,7 +692,7 @@
CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
- rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, atac,
+ rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
@@ -686,21 +702,23 @@
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], atac])
+ REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
(rev (active_set_map0s ~~ in_Irels))])
(ctor_sets ~~ passive_set_map0s),
rtac ctxt conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2),
rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
- EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, atac,
+ EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
+ dtac ctxt set_rev_mp, assume_tac ctxt,
dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
@{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
- dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, atac])
+ dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
+ REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
in_Irels),
- atac]]
+ assume_tac ctxt]]
in
EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
end;
@@ -753,7 +771,7 @@
rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer},
REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun},
- atac])
+ assume_tac ctxt])
map_transfers)])
end;
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -100,7 +100,8 @@
fun mk_map_cong0L_tac ctxt passive map_cong0 map_id =
(rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN
- REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, atac, rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
+ REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, assume_tac ctxt,
+ rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
rtac ctxt map_id 1;
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sat Jul 18 20:47:08 2015 +0200
@@ -54,17 +54,21 @@
fun mk_nchotomy_tac ctxt n exhaust =
HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN'
- EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, atac]) (1 upto n)));
+ EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
+ (1 upto n)));
fun mk_unique_disc_def_tac ctxt m uexhaust =
- HEADGOAL (EVERY' [rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI, atac, rtac ctxt refl]);
+ HEADGOAL (EVERY'
+ [rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI,
+ assume_tac ctxt, rtac ctxt refl]);
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
HEADGOAL (EVERY' ([rtac ctxt (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
rtac ctxt @{thm iffI_np}, REPEAT_DETERM o etac ctxt exE,
hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac ctxt allI,
rtac ctxt distinct, rtac ctxt uexhaust] @
- (([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, atac], [REPEAT_DETERM o rtac ctxt exI, atac])
+ (([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt],
+ [REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
|> k = 1 ? swap |> op @)));
fun mk_half_distinct_disc_tac ctxt m discD disc' =
@@ -77,7 +81,7 @@
fun mk_exhaust_disc_or_sel_tac ctxt n exhaust destIs =
HEADGOAL (rtac ctxt exhaust THEN'
EVERY' (map2 (fn k => fn destI => dtac ctxt destI THEN'
- select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' atac) (1 upto n) destIs));
+ select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' assume_tac ctxt) (1 upto n) destIs));
val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
@@ -88,7 +92,7 @@
fun mk_collapse_tac ctxt m discD sels =
HEADGOAL (dtac ctxt discD THEN'
(if m = 0 then
- atac
+ assume_tac ctxt
else
REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN'
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac ctxt refl));
@@ -105,26 +109,29 @@
distinct_discsss' =
if ms = [0] then
HEADGOAL (rtac ctxt (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
- TRY o EVERY' [rtac ctxt uexhaust_disc, atac, rtac ctxt vexhaust_disc, atac])
+ TRY o
+ EVERY' [rtac ctxt uexhaust_disc, assume_tac ctxt, rtac ctxt vexhaust_disc, assume_tac ctxt])
else
let val ks = 1 upto n in
HEADGOAL (rtac ctxt uexhaust_disc THEN'
EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
- EVERY' [rtac ctxt (uuncollapse RS trans) THEN' TRY o atac, rtac ctxt sym, rtac ctxt vexhaust_disc,
+ EVERY' [rtac ctxt (uuncollapse RS trans) THEN'
+ TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc,
EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
EVERY'
(if k' = k then
- [rtac ctxt (vuncollapse RS trans), TRY o atac] @
+ [rtac ctxt (vuncollapse RS trans), TRY o assume_tac ctxt] @
(if m = 0 then
[rtac ctxt refl]
else
- [if n = 1 then K all_tac else EVERY' [dtac ctxt meta_mp, atac, dtac ctxt meta_mp, atac],
+ [if n = 1 then K all_tac
+ else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt],
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
asm_simp_tac (ss_only [] ctxt)])
else
[dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')),
etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
- atac, atac]))
+ assume_tac ctxt, assume_tac ctxt]))
ks distinct_discss distinct_discss' uncollapses)])
ks ms distinct_discsss distinct_discsss' uncollapses))
end;
@@ -132,7 +139,7 @@
fun mk_case_same_ctr_tac ctxt injects =
REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN'
(case injects of
- [] => atac
+ [] => assume_tac ctxt
| [inject] => dtac ctxt (inject RS iffD1) THEN' REPEAT_DETERM o etac ctxt conjE THEN'
hyp_subst_tac ctxt THEN' rtac ctxt refl);
@@ -176,8 +183,10 @@
flat (nth distinctsss (k - 1))) ctxt)) k) THEN
ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN'
- hyp_subst_tac ctxt THEN' atac THEN' REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
- REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN' rtac ctxt refl THEN' atac)
+ hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
+ REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
+ REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
+ rtac ctxt refl THEN' assume_tac ctxt)
end;
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Jul 18 20:47:08 2015 +0200
@@ -275,8 +275,8 @@
let val (butlast, last) = split_last xs;
in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
-fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
-fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
+fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (resolve0_tac [conjI] 1) gen_tac;
+fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (resolve0_tac [conjI]) gen_tac;
fun rtac ctxt thm = resolve_tac ctxt [thm];
fun etac ctxt thm = eresolve_tac ctxt [thm];
--- a/src/HOL/Tools/Function/function_core.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Sat Jul 18 20:47:08 2015 +0200
@@ -692,7 +692,7 @@
subset_induct_rule
|> Thm.forall_intr (Thm.cterm_of ctxt D)
|> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
- |> atac 1 |> Seq.hd
+ |> assume_tac ctxt 1 |> Seq.hd
|> (curry op COMP) (acc_downward
|> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
|> Thm.forall_intr (Thm.cterm_of ctxt z)
--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 18 20:47:08 2015 +0200
@@ -104,17 +104,17 @@
(** Proof Reconstruction **)
-fun prove_row (c :: cs) =
- (case Lazy.force c of
- Less thm =>
- rtac @{thm "mlex_less"} 1
- THEN PRIMITIVE (Thm.elim_implies thm)
- | LessEq (thm, _) =>
- rtac @{thm "mlex_leq"} 1
- THEN PRIMITIVE (Thm.elim_implies thm)
- THEN prove_row cs
- | _ => raise General.Fail "lexicographic_order")
- | prove_row [] = no_tac;
+fun prove_row_tac ctxt (c :: cs) =
+ (case Lazy.force c of
+ Less thm =>
+ resolve_tac ctxt @{thms mlex_less} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ | LessEq (thm, _) =>
+ resolve_tac ctxt @{thms mlex_leq} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ THEN prove_row_tac ctxt cs
+ | _ => raise General.Fail "lexicographic_order")
+ | prove_row_tac _ [] = no_tac;
(** Error reporting **)
@@ -202,9 +202,9 @@
in (* 4: proof reconstruction *)
st |>
(PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
- THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
- THEN (rtac @{thm "wf_empty"} 1)
- THEN EVERY (map prove_row clean_table))
+ THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
+ THEN (resolve_tac ctxt @{thms wf_empty} 1)
+ THEN EVERY (map (prove_row_tac ctxt) clean_table))
end
end) 1 st;
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Jul 18 20:47:08 2015 +0200
@@ -17,9 +17,9 @@
msetT : typ -> typ,
mk_mset : typ -> term list -> term,
mset_regroup_conv : Proof.context -> int list -> conv,
- mset_member_tac : int -> int -> tactic,
- mset_nonempty_tac : int -> tactic,
- mset_pwleq_tac : int -> tactic,
+ mset_member_tac : Proof.context -> int -> int -> tactic,
+ mset_nonempty_tac : Proof.context -> int -> tactic,
+ mset_pwleq_tac : Proof.context -> int -> tactic,
set_of_simps : thm list,
smsI' : thm,
wmsI2'' : thm,
@@ -49,9 +49,9 @@
msetT : typ -> typ,
mk_mset : typ -> term list -> term,
mset_regroup_conv : Proof.context -> int list -> conv,
- mset_member_tac : int -> int -> tactic,
- mset_nonempty_tac : int -> tactic,
- mset_pwleq_tac : int -> tactic,
+ mset_member_tac : Proof.context -> int -> int -> tactic,
+ mset_nonempty_tac : Proof.context -> int -> tactic,
+ mset_pwleq_tac : Proof.context -> int -> tactic,
set_of_simps : thm list,
smsI' : thm,
wmsI2'' : thm,
@@ -116,13 +116,13 @@
(* General reduction pair application *)
fun rem_inv_img ctxt =
- rtac @{thm subsetI} 1
- THEN etac @{thm CollectE} 1
- THEN REPEAT (etac @{thm exE} 1)
+ resolve_tac ctxt @{thms subsetI} 1
+ THEN eresolve_tac ctxt @{thms CollectE} 1
+ THEN REPEAT (eresolve_tac ctxt @{thms exE} 1)
THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
- THEN rtac @{thm CollectI} 1
- THEN etac @{thm conjE} 1
- THEN etac @{thm ssubst} 1
+ THEN resolve_tac ctxt @{thms CollectI} 1
+ THEN eresolve_tac ctxt @{thms conjE} 1
+ THEN eresolve_tac ctxt @{thms ssubst} 1
THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
@@ -130,15 +130,15 @@
val setT = HOLogic.mk_setT
-fun set_member_tac m i =
- if m = 0 then rtac @{thm insertI1} i
- else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
+fun set_member_tac ctxt m i =
+ if m = 0 then resolve_tac ctxt @{thms insertI1} i
+ else resolve_tac ctxt @{thms insertI2} i THEN set_member_tac ctxt (m - 1) i
-val set_nonempty_tac = rtac @{thm insert_not_empty}
+fun set_nonempty_tac ctxt = resolve_tac ctxt @{thms insert_not_empty}
-fun set_finite_tac i =
- rtac @{thm finite.emptyI} i
- ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
+fun set_finite_tac ctxt i =
+ resolve_tac ctxt @{thms finite.emptyI} i
+ ORELSE (resolve_tac ctxt @{thms finite.insertI} i THEN (fn st => set_finite_tac ctxt i st))
(* Reconstruction *)
@@ -183,7 +183,7 @@
then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
in
- rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
+ resolve_tac ctxt [rule] 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
end
@@ -192,16 +192,16 @@
val (empty, step) = ord_intros_max strict
in
if length lq = 0
- then rtac empty 1 THEN set_finite_tac 1
- THEN (if strict then set_nonempty_tac 1 else all_tac)
+ then resolve_tac ctxt [empty] 1 THEN set_finite_tac ctxt 1
+ THEN (if strict then set_nonempty_tac ctxt 1 else all_tac)
else
let
val (j, b) :: rest = lq
val (i, a) = the (covering g strict j)
- fun choose xs = set_member_tac (find_index (curry op = (i, a)) xs) 1
+ fun choose xs = set_member_tac ctxt (find_index (curry op = (i, a)) xs) 1
val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
in
- rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+ resolve_tac ctxt [step] 1 THEN solve_tac THEN steps_tac MAX strict rest lp
end
end
| steps_tac MIN strict lq lp =
@@ -209,16 +209,16 @@
val (empty, step) = ord_intros_min strict
in
if length lp = 0
- then rtac empty 1
- THEN (if strict then set_nonempty_tac 1 else all_tac)
+ then resolve_tac ctxt [empty] 1
+ THEN (if strict then set_nonempty_tac ctxt 1 else all_tac)
else
let
val (i, a) :: rest = lp
val (j, b) = the (covering g strict i)
- fun choose xs = set_member_tac (find_index (curry op = (j, b)) xs) 1
+ fun choose xs = set_member_tac ctxt (find_index (curry op = (j, b)) xs) 1
val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
in
- rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+ resolve_tac ctxt [step] 1 THEN solve_tac THEN steps_tac MIN strict lq rest
end
end
| steps_tac MS strict lq lp =
@@ -243,10 +243,10 @@
end
in
CONVERSION goal_rewrite 1
- THEN (if strict then rtac smsI' 1
- else if qs = lq then rtac wmsI2'' 1
- else rtac wmsI1 1)
- THEN mset_pwleq_tac 1
+ THEN (if strict then resolve_tac ctxt [smsI'] 1
+ else if qs = lq then resolve_tac ctxt [wmsI2''] 1
+ else resolve_tac ctxt [wmsI1] 1)
+ THEN mset_pwleq_tac ctxt 1
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
then Local_Defs.unfold_tac ctxt set_of_simps
@@ -275,9 +275,9 @@
in
PROFILE "Proof Reconstruction"
(CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv ctxt sl))) 1
- THEN (rtac @{thm reduction_pair_lemma} 1)
- THEN (rtac @{thm rp_inv_image_rp} 1)
- THEN (rtac (order_rpair ms_rp label) 1)
+ THEN (resolve_tac ctxt @{thms reduction_pair_lemma} 1)
+ THEN (resolve_tac ctxt @{thms rp_inv_image_rp} 1)
+ THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
THEN unfold_tac ctxt @{thms rp_inv_image_def}
THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
@@ -300,7 +300,7 @@
NONE => no_tac
| SOME cert =>
SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
- THEN TRY (rtac @{thm wf_empty} i))
+ THEN TRY (resolve_tac ctxt @{thms wf_empty} i))
end)
fun gen_decomp_scnp_tac orders autom_tac ctxt =
@@ -315,7 +315,7 @@
fun gen_sizechange_tac orders autom_tac ctxt =
TRY (Function_Common.termination_rule_tac ctxt 1)
THEN TRY (Termination.wf_union_tac ctxt)
- THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
+ THEN (resolve_tac ctxt @{thms wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
fun sizechange_tac ctxt autom_tac =
gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
--- a/src/HOL/Tools/Function/termination.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sat Jul 18 20:47:08 2015 +0200
@@ -289,13 +289,13 @@
|> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
fun solve_membership_tac i =
- (EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *)
- THEN' (fn j => TRY (rtac @{thm UnI1} j))
- THEN' (rtac @{thm CollectI}) (* unfold comprehension *)
- THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *)
- THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
- ORELSE' ((rtac @{thm conjI})
- THEN' (rtac @{thm refl})
+ (EVERY' (replicate (i - 2) (resolve_tac ctxt @{thms UnI2})) (* pick the right component of the union *)
+ THEN' (fn j => TRY (resolve_tac ctxt @{thms UnI1} j))
+ THEN' (resolve_tac ctxt @{thms CollectI}) (* unfold comprehension *)
+ THEN' (fn i => REPEAT (resolve_tac ctxt @{thms exI} i)) (* Turn existentials into schematic Vars *)
+ THEN' ((resolve_tac ctxt @{thms refl}) (* unification instantiates all Vars *)
+ ORELSE' ((resolve_tac ctxt @{thms conjI})
+ THEN' (resolve_tac ctxt @{thms refl})
THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
@@ -318,10 +318,10 @@
then Term_Graph.add_edge (c2, c1) else I)
cs cs
-fun ucomp_empty_tac T =
- REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
- ORELSE' rtac @{thm union_comp_emptyL}
- ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
+fun ucomp_empty_tac ctxt T =
+ REPEAT_ALL_NEW (resolve_tac ctxt @{thms union_comp_emptyR}
+ ORELSE' resolve_tac ctxt @{thms union_comp_emptyL}
+ ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => resolve_tac ctxt [T c1 c2] i))
fun regroup_calls_tac ctxt cs = CALLS (fn (cs', i) =>
let
@@ -332,11 +332,13 @@
end)
-fun solve_trivial_tac D = CALLS (fn ([c], i) =>
- (case get_chain D c c of
- SOME (SOME thm) => rtac @{thm wf_no_loop} i
- THEN rtac thm i
- | _ => no_tac)
+fun solve_trivial_tac ctxt D =
+ CALLS (fn ([c], i) =>
+ (case get_chain D c c of
+ SOME (SOME thm) =>
+ resolve_tac ctxt @{thms wf_no_loop} i THEN
+ resolve_tac ctxt [thm] i
+ | _ => no_tac)
| _ => no_tac)
fun decompose_tac ctxt D = CALLS (fn (cs, i) =>
@@ -344,17 +346,17 @@
val G = mk_dgraph D cs
val sccs = Term_Graph.strong_conn G
- fun split [SCC] i = TRY (solve_trivial_tac D i)
+ fun split [SCC] i = TRY (solve_trivial_tac ctxt D i)
| split (SCC::rest) i =
regroup_calls_tac ctxt SCC i
- THEN rtac @{thm wf_union_compatible} i
- THEN rtac @{thm less_by_empty} (i + 2)
- THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
+ THEN resolve_tac ctxt @{thms wf_union_compatible} i
+ THEN resolve_tac ctxt @{thms less_by_empty} (i + 2)
+ THEN ucomp_empty_tac ctxt (the o the oo get_chain D) (i + 2)
THEN split rest (i + 1)
- THEN TRY (solve_trivial_tac D i)
+ THEN TRY (solve_trivial_tac ctxt D i)
in
if length sccs > 1 then split sccs i
- else solve_trivial_tac D i
+ else solve_trivial_tac ctxt D i
end)
end
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Jul 18 20:47:08 2015 +0200
@@ -413,7 +413,7 @@
case_tac exhaust_rule ctxt THEN_ALL_NEW (
EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
- REPEAT_DETERM o etac ctxt conjE, atac])) i
+ REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i
val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
@@ -560,7 +560,7 @@
fun non_empty_typedef_tac non_empty_pred ctxt i =
(Method.insert_tac [non_empty_pred] THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' atac) i
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
val uTname = unique_Tname (rty, qty)
val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Jul 18 20:47:08 2015 +0200
@@ -188,7 +188,9 @@
(fn (((name, mx), tvs), c) =>
Typedef.add_typedef_global false (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
- (fn ctxt => rtac exI 1 THEN rtac CollectI 1 THEN
+ (fn ctxt =>
+ resolve_tac ctxt [exI] 1 THEN
+ resolve_tac ctxt [CollectI] 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac ctxt rep_intrs 1)))
(types_syntax ~~ tyvars ~~ take (length newTs) rep_set_names)
@@ -355,7 +357,8 @@
val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
val char_thms' =
map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
- (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
+ (fn {context = ctxt, ...} =>
+ EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt [refl] 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -382,8 +385,11 @@
(map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
(r $ (a $ Old_Datatype_Aux.app_bnds f i)), f))))
- (fn {context = ctxt, ...} => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
- REPEAT (etac allE 1), rtac thm 1, assume_tac ctxt 1])
+ (fn {context = ctxt, ...} =>
+ EVERY [REPEAT_DETERM_N i (resolve_tac ctxt @{thms ext} 1),
+ REPEAT (eresolve_tac ctxt [allE] 1),
+ resolve_tac ctxt [thm] 1,
+ assume_tac ctxt 1])
end
in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
@@ -421,7 +427,7 @@
[(Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW
Object_Logic.atomize_prems_tac ctxt) 1,
REPEAT (EVERY
- [rtac allI 1, rtac impI 1,
+ [resolve_tac ctxt [allI] 1, resolve_tac ctxt [impI] 1,
Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1,
REPEAT (EVERY
[hyp_subst_tac ctxt 1,
@@ -431,9 +437,9 @@
ORELSE (EVERY
[REPEAT (eresolve_tac ctxt (Scons_inject ::
map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
- REPEAT (cong_tac ctxt 1), rtac refl 1,
+ REPEAT (cong_tac ctxt 1), resolve_tac ctxt [refl] 1,
REPEAT (assume_tac ctxt 1 ORELSE (EVERY
- [REPEAT (rtac @{thm ext} 1),
+ [REPEAT (resolve_tac ctxt @{thms ext} 1),
REPEAT (eresolve_tac ctxt (mp :: allE ::
map make_elim (Suml_inject :: Sumr_inject ::
Lim_inject :: inj_thms') @ fun_congs) 1),
@@ -450,7 +456,7 @@
Object_Logic.atomize_prems_tac ctxt) 1,
rewrite_goals_tac ctxt rewrites,
REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW
- ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
+ ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac elem_thms)) 1)]);
in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end;
@@ -485,7 +491,7 @@
(Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
[(Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
Object_Logic.atomize_prems_tac ctxt) 1,
- REPEAT (rtac TrueI 1),
+ REPEAT (resolve_tac ctxt [TrueI] 1),
rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
@@ -493,7 +499,7 @@
[REPEAT (eresolve_tac ctxt ([rangeE, @{thm ex1_implies_ex} RS exE] @
maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
TRY (hyp_subst_tac ctxt 1),
- rtac (sym RS range_eqI) 1,
+ resolve_tac ctxt [sym RS range_eqI] 1,
resolve_tac ctxt iso_char_thms 1])])));
val Abs_inverse_thms' =
@@ -518,7 +524,7 @@
(fn {context = ctxt, ...} => EVERY
[resolve_tac ctxt inj_thms 1,
rewrite_goals_tac ctxt rewrites,
- rtac refl 3,
+ resolve_tac ctxt [refl] 3,
resolve_tac ctxt rep_intrs 2,
REPEAT (resolve_tac ctxt iso_elem_thms 1)])
end;
@@ -560,12 +566,14 @@
in
Goal.prove_sorry_global thy5 [] [] t
(fn {context = ctxt, ...} => EVERY
- [rtac iffI 1,
- REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
- dresolve_tac ctxt rep_congs 1, dtac @{thm box_equals} 1,
+ [resolve_tac ctxt [iffI] 1,
+ REPEAT (eresolve_tac ctxt [conjE] 2), hyp_subst_tac ctxt 2,
+ resolve_tac ctxt [refl] 2,
+ dresolve_tac ctxt rep_congs 1,
+ dresolve_tac ctxt @{thms box_equals} 1,
REPEAT (resolve_tac ctxt rep_thms 1),
REPEAT (eresolve_tac ctxt inj_thms 1),
- REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
+ REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
REPEAT (eresolve_tac ctxt (make_elim fun_cong :: inj_thms) 1),
assume_tac ctxt 1]))])
end;
@@ -618,10 +626,10 @@
HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls)))
(fn {context = ctxt, ...} =>
EVERY
- [REPEAT (etac conjE 1),
+ [REPEAT (eresolve_tac ctxt [conjE] 1),
REPEAT (EVERY
- [TRY (rtac conjI 1), resolve_tac ctxt Rep_inverse_thms 1,
- etac mp 1, resolve_tac ctxt iso_elem_thms 1])]);
+ [TRY (resolve_tac ctxt [conjI] 1), resolve_tac ctxt Rep_inverse_thms 1,
+ eresolve_tac ctxt [mp] 1, resolve_tac ctxt iso_elem_thms 1])]);
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
val frees =
@@ -637,14 +645,14 @@
(Logic.strip_imp_concl dt_induct_prop)
(fn {context = ctxt, prems, ...} =>
EVERY
- [rtac indrule_lemma' 1,
+ [resolve_tac ctxt [indrule_lemma'] 1,
(Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
Object_Logic.atomize_prems_tac ctxt) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
+ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
(prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
val ([(_, [dt_induct'])], thy7) =
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Jul 18 20:47:08 2015 +0200
@@ -249,7 +249,7 @@
val thesis =
Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2))
case_th' OF prems2
- in rtac thesis 1 end
+ in resolve_tac ctxt2 [thesis] 1 end
in
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule
(fn {context = ctxt1, ...} =>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jul 18 20:47:08 2015 +0200
@@ -1106,7 +1106,7 @@
val tac =
Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
(@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
- THEN rtac @{thm Predicate.singleI} 1
+ THEN resolve_tac ctxt @{thms Predicate.singleI} 1
in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
neg_introtrm (fn _ => tac))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Jul 18 20:47:08 2015 +0200
@@ -166,8 +166,9 @@
val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
THEN (EVERY (map (fn y =>
- rtac (Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}) 1) ps))
- THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
+ resolve_tac ctxt'
+ [Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
+ THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
THEN TRY (assume_tac ctxt' 1)
in
Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Jul 18 20:47:08 2015 +0200
@@ -38,7 +38,7 @@
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps @{thms simp_thms Pair_eq}
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
- setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
+ setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
(* auxillary functions *)
@@ -74,13 +74,13 @@
end) ctxt 1
| Abs _ => raise Fail "prove_param: No valid parameter term")
in
- REPEAT_DETERM (rtac @{thm ext} 1)
+ REPEAT_DETERM (resolve_tac ctxt @{thms ext} 1)
THEN trace_tac ctxt options "prove_param"
THEN f_tac
THEN trace_tac ctxt options "after prove_param"
THEN (REPEAT_DETERM (assume_tac ctxt 1))
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
- THEN REPEAT_DETERM (rtac @{thm refl} 1)
+ THEN REPEAT_DETERM (resolve_tac ctxt @{thms refl} 1)
end
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
@@ -93,7 +93,7 @@
val ho_args = ho_args_of mode args
in
trace_tac ctxt options "before intro rule:"
- THEN rtac introrule 1
+ THEN resolve_tac ctxt [introrule] 1
THEN trace_tac ctxt options "after intro rule"
(* for the right assumption in first position *)
THEN rotate_tac premposition 1
@@ -118,7 +118,7 @@
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
param_prem
in
- rtac param_prem' 1
+ resolve_tac ctxt' [param_prem'] 1
end) ctxt 1
THEN trace_tac ctxt options "after prove parameter call")
@@ -144,9 +144,9 @@
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
THEN trace_tac ctxt options "after prove_match:"
THEN (DETERM (TRY
- (rtac eval_if_P 1
+ (resolve_tac ctxt [eval_if_P] 1
THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
- (REPEAT_DETERM (rtac @{thm conjI} 1
+ (REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1
THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
THEN trace_tac ctxt' options "if condition to be solved:"
THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
@@ -157,7 +157,7 @@
rewrite_goal_tac ctxt'
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
- THEN REPEAT_DETERM (rtac @{thm refl} 1))
+ THEN REPEAT_DETERM (resolve_tac ctxt' @{thms refl} 1))
THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
THEN trace_tac ctxt options "after if simplification"
end;
@@ -199,13 +199,13 @@
in
rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
- THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
+ THEN (resolve_tac ctxt [if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}] 1)
| prove_prems out_ts ((p, deriv) :: ps) =
let
val premposition = (find_index (equal p) clauses) + nargs
val mode = head_mode_of deriv
val rest_tac =
- rtac @{thm bindI} 1
+ resolve_tac ctxt @{thms bindI} 1
THEN (case p of Prem t =>
let
val (_, us) = strip_comb t
@@ -238,15 +238,15 @@
THEN (if (is_some name) then
trace_tac ctxt options "before applying not introduction rule"
THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
- rtac (the neg_intro_rule) 1
- THEN rtac (nth prems premposition) 1) ctxt 1
+ resolve_tac ctxt [the neg_intro_rule] 1
+ THEN resolve_tac ctxt [nth prems premposition] 1) ctxt 1
THEN trace_tac ctxt options "after applying not introduction rule"
THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
THEN (REPEAT_DETERM (assume_tac ctxt 1))
else
- rtac @{thm not_predI'} 1
+ resolve_tac ctxt @{thms not_predI'} 1
(* test: *)
- THEN dtac @{thm sym} 1
+ THEN dresolve_tac ctxt @{thms sym} 1
THEN asm_full_simp_tac
(put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
THEN simp_tac
@@ -254,7 +254,7 @@
THEN rec_tac
end
| Sidecond t =>
- rtac @{thm if_predI} 1
+ resolve_tac ctxt @{thms if_predI} 1
THEN trace_tac ctxt options "before sidecond:"
THEN prove_sidecond ctxt t
THEN trace_tac ctxt options "after sidecond:"
@@ -265,14 +265,14 @@
val prems_tac = prove_prems in_ts moded_ps
in
trace_tac ctxt options "Proving clause..."
- THEN rtac @{thm bindI} 1
- THEN rtac @{thm singleI} 1
+ THEN resolve_tac ctxt @{thms bindI} 1
+ THEN resolve_tac ctxt @{thms singleI} 1
THEN prems_tac
end
-fun select_sup 1 1 = []
- | select_sup _ 1 = [rtac @{thm supI1}]
- | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
+fun select_sup _ 1 1 = []
+ | select_sup ctxt _ 1 = [resolve_tac ctxt @{thms supI1}]
+ | select_sup ctxt n i = resolve_tac ctxt @{thms supI2} :: select_sup ctxt (n - 1) (i - 1);
fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
let
@@ -282,11 +282,11 @@
in
REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
THEN trace_tac ctxt options "before applying elim rule"
- THEN etac (predfun_elim_of ctxt pred mode) 1
- THEN etac pred_case_rule 1
+ THEN eresolve_tac ctxt [predfun_elim_of ctxt pred mode] 1
+ THEN eresolve_tac ctxt [pred_case_rule] 1
THEN trace_tac ctxt options "after applying elim rule"
THEN (EVERY (map
- (fn i => EVERY' (select_sup (length moded_clauses) i) i)
+ (fn i => EVERY' (select_sup ctxt (length moded_clauses) i) i)
(1 upto (length moded_clauses))))
THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
THEN trace_tac ctxt options "proved one direction"
@@ -313,15 +313,15 @@
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
THEN (REPEAT_DETERM_N (num_of_constrs - 1)
- (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
+ (eresolve_tac ctxt @{thms botE} 1 ORELSE eresolve_tac ctxt @{thms botE} 2)))
THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
THEN (EVERY (map split_term_tac ts))
end
else all_tac
in
split_term_tac (HOLogic.mk_tuple out_ts)
- THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
- THEN (etac @{thm botE} 2))))
+ THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms split_if_asm} 1)
+ THEN (eresolve_tac ctxt @{thms botE} 2))))
end
(* VERY LARGE SIMILIRATIY to function prove_param
@@ -357,15 +357,15 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
- etac @{thm bindE} 1
+ eresolve_tac ctxt @{thms bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
THEN trace_tac ctxt options "prove_expr2-before"
- THEN etac (predfun_elim_of ctxt name mode) 1
+ THEN eresolve_tac ctxt [predfun_elim_of ctxt name mode] 1
THEN trace_tac ctxt options "prove_expr2"
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
THEN trace_tac ctxt options "finished prove_expr2"
end
- | _ => etac @{thm bindE} 1)
+ | _ => eresolve_tac ctxt @{thms bindE} 1)
fun prove_sidecond2 options ctxt t =
let
@@ -399,15 +399,15 @@
trace_tac ctxt options "before prove_match2 - last call:"
THEN prove_match2 options ctxt out_ts
THEN trace_tac ctxt options "after prove_match2 - last call:"
- THEN (etac @{thm singleE} 1)
- THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
+ THEN (eresolve_tac ctxt @{thms singleE} 1)
+ THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1))
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
THEN TRY (
- (REPEAT_DETERM (etac @{thm Pair_inject} 1))
+ (REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1))
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
- THEN (rtac pred_intro_rule
+ THEN (resolve_tac ctxt [pred_intro_rule]
(* How to handle equality correctly? *)
THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
THEN' (assume_tac ctxt ORELSE'
@@ -438,20 +438,20 @@
val ho_args = ho_args_of mode args
in
trace_tac ctxt options "before neg prem 2"
- THEN etac @{thm bindE} 1
+ THEN eresolve_tac ctxt @{thms bindE} 1
THEN (if is_some name then
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
[predfun_definition_of ctxt (the name) mode]) 1
- THEN etac @{thm not_predE} 1
+ THEN eresolve_tac ctxt @{thms not_predE} 1
THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
else
- etac @{thm not_predE'} 1)
+ eresolve_tac ctxt @{thms not_predE'} 1)
THEN rec_tac
end
| Sidecond t =>
- etac @{thm bindE} 1
- THEN etac @{thm if_predE} 1
+ eresolve_tac ctxt @{thms bindE} 1
+ THEN eresolve_tac ctxt @{thms if_predE} 1
THEN prove_sidecond2 options ctxt t
THEN prove_prems2 [] ps)
in
@@ -463,9 +463,9 @@
val prems_tac = prove_prems2 in_ts ps
in
trace_tac ctxt options "starting prove_clause2"
- THEN etac @{thm bindE} 1
- THEN (etac @{thm singleE'} 1)
- THEN (TRY (etac @{thm Pair_inject} 1))
+ THEN eresolve_tac ctxt @{thms bindE} 1
+ THEN (eresolve_tac ctxt @{thms singleE'} 1)
+ THEN (TRY (eresolve_tac ctxt @{thms Pair_inject} 1))
THEN trace_tac ctxt options "after singleE':"
THEN prems_tac
end;
@@ -473,15 +473,15 @@
fun prove_other_direction options ctxt pred mode moded_clauses =
let
fun prove_clause clause i =
- (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
+ (if i < length moded_clauses then eresolve_tac ctxt @{thms supE} 1 else all_tac)
THEN (prove_clause2 options ctxt pred mode clause i)
in
- (DETERM (TRY (rtac @{thm unit.induct} 1)))
+ (DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
- THEN (rtac (predfun_intro_of ctxt pred mode) 1)
- THEN (REPEAT_DETERM (rtac @{thm refl} 2))
+ THEN (resolve_tac ctxt [predfun_intro_of ctxt pred mode] 1)
+ THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2))
THEN (
- if null moded_clauses then etac @{thm botE} 1
+ if null moded_clauses then eresolve_tac ctxt @{thms botE} 1
else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
end
@@ -496,7 +496,7 @@
Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
(if not (skip_proof options) then
(fn _ =>
- rtac @{thm pred_iffI} 1
+ resolve_tac ctxt @{thms pred_iffI} 1
THEN trace_tac ctxt options "after pred_iffI"
THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
THEN trace_tac ctxt options "proved one direction"
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sat Jul 18 20:47:08 2015 +0200
@@ -741,7 +741,7 @@
(case try (fn () =>
Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
NONE => no_tac
- | SOME r => rtac r i)
+ | SOME r => resolve_tac ctxt [r] i)
end)
end;
@@ -860,11 +860,11 @@
else Conv.arg_conv (conv ctxt) p
val p' = Thm.rhs_of cpth
val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
- in rtac th i end
+ in resolve_tac ctxt [th] i end
handle COOPER _ => no_tac);
-fun finish_tac q = SUBGOAL (fn (_, i) =>
- (if q then I else TRY) (rtac TrueI i));
+fun finish_tac ctxt q = SUBGOAL (fn (_, i) =>
+ (if q then I else TRY) (resolve_tac ctxt [TrueI] i));
fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
let
@@ -885,7 +885,7 @@
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW nat_to_int_tac ctxt
THEN_ALL_NEW core_tac ctxt
- THEN_ALL_NEW finish_tac elim
+ THEN_ALL_NEW finish_tac ctxt elim
end 1);
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Jul 18 20:47:08 2015 +0200
@@ -108,7 +108,7 @@
[(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
(cT_rhs, Thm.cterm_of lthy' t_rhs)]);
fun tac ctxt =
- ALLGOALS (rtac rule)
+ ALLGOALS (resolve_tac ctxt [rule])
THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Jul 18 20:47:08 2015 +0200
@@ -9,15 +9,12 @@
val add_quotient_def:
((binding * mixfix) * Attrib.binding) * (term * term) -> thm ->
local_theory -> Quotient_Info.quotconsts * local_theory
-
val quotient_def:
(binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
local_theory -> Proof.state
-
val quotient_def_cmd:
(binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
local_theory -> Proof.state
-
end;
structure Quotient_Def: QUOTIENT_DEF =
@@ -189,7 +186,9 @@
case thm_list of
[] => the maybe_proven_rsp_thm
| [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
- (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
+ (fn _ =>
+ resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
+ Proof_Context.fact_tac ctxt [thm] 1)
in
snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Jul 18 20:47:08 2015 +0200
@@ -61,7 +61,7 @@
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
- [rtac @{thm identity_quotient3},
+ [resolve_tac ctxt @{thms identity_quotient3},
resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))]))
val quotient_solver = mk_solver "Quotient goal solver" quotient_tac
@@ -250,7 +250,7 @@
val inst_thm = Drule.instantiate' ty_inst
([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
in
- (rtac inst_thm THEN' SOLVED' (quotient_tac ctxt)) 1
+ (resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1
end
| _ => no_tac
end)
@@ -266,7 +266,7 @@
in
case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
[SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
- SOME thm => rtac thm THEN' quotient_tac ctxt
+ SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
| NONE => K no_tac
end
| _ => K no_tac
@@ -282,7 +282,7 @@
case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
SOME t_inst =>
(case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
- SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
+ SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i
| NONE => no_tac)
| NONE => no_tac
end
@@ -315,48 +315,48 @@
(case bare_concl goal of
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
(Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
- => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
+ => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
| (Const (@{const_name HOL.eq},_) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+ => resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
| (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
+ => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
| Const (@{const_name HOL.eq},_) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+ => resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
| (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
+ => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
| (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
- => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
+ => resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
| (_ $
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
+ => resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
- (rtac @{thm refl} ORELSE'
+ (resolve_tac ctxt @{thms refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
(* reflexivity of operators arising from Cong_tac *)
- | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
+ | Const (@{const_name HOL.eq},_) $ _ $ _ => resolve_tac ctxt @{thms refl}
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *)
@@ -366,7 +366,7 @@
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
| _ $ _ $ _
- => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+ => (resolve_tac ctxt @{thms quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
ORELSE' rep_abs_rsp_tac ctxt
| _ => K no_tac) i)
@@ -388,7 +388,7 @@
assume_tac ctxt,
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
- rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
+ resolve_tac ctxt @{thms ext} THEN' quot_true_tac ctxt unlam,
(* reflexivity of the basic relations *)
(* R ... ... *)
@@ -522,7 +522,7 @@
map_fun_tac ctxt,
lambda_prs_tac ctxt,
simp_tac simpset,
- TRY o rtac refl]
+ TRY o resolve_tac ctxt [refl]]
end
@@ -531,8 +531,8 @@
fun inst_spec ctrm =
Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
-fun inst_spec_tac ctrms =
- EVERY' (map (dtac o inst_spec) ctrms)
+fun inst_spec_tac ctxt ctrms =
+ EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)
fun all_list xs trm =
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
@@ -548,9 +548,9 @@
val concl' = apply_under_Trueprop (all_list vrs) concl
val goal = Logic.mk_implies (concl', concl)
val rule = Goal.prove ctxt [] [] goal
- (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
+ (K (EVERY1 [inst_spec_tac ctxt (rev cvrs), assume_tac ctxt]))
in
- rtac rule i
+ resolve_tac ctxt [rule] i
end)
@@ -632,7 +632,7 @@
val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
val rule = procedure_inst ctxt rtrm goal
in
- rtac rule i
+ resolve_tac ctxt [rule] i
end)
end
@@ -681,7 +681,7 @@
val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
val rule = partiality_procedure_inst ctxt rtrm goal
in
- rtac rule i
+ resolve_tac ctxt [rule] i
end)
end
@@ -722,7 +722,7 @@
val rule = procedure_inst ctxt (Thm.prop_of rthm') goal
in
- (rtac rule THEN' rtac rthm') i
+ (resolve_tac ctxt [rule] THEN' resolve_tac ctxt [rthm']) i
end)
end
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Jul 18 20:47:08 2015 +0200
@@ -42,8 +42,8 @@
(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
let
- fun typedef_tac _ =
- EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
+ fun typedef_tac ctxt =
+ EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
in
Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
@@ -58,12 +58,12 @@
val abs_inv = #Abs_inverse typedef_info
val rep_inj = #Rep_inject typedef_info
in
- (rtac @{thm quot_type.intro} THEN' RANGE [
- rtac equiv_thm,
- rtac rep_thm,
- rtac rep_inv,
- rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt,
- rtac rep_inj]) 1
+ (resolve_tac ctxt @{thms quot_type.intro} THEN' RANGE [
+ resolve_tac ctxt [equiv_thm],
+ resolve_tac ctxt [rep_thm],
+ resolve_tac ctxt [rep_inv],
+ resolve_tac ctxt [abs_inv] THEN' resolve_tac ctxt [mem_def2] THEN' assume_tac ctxt,
+ resolve_tac ctxt [rep_inj]]) 1
end
(* proves the quot_type theorem for the new type *)
--- a/src/HOL/Tools/SMT/conj_disj_perm.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Sat Jul 18 20:47:08 2015 +0200
@@ -6,7 +6,7 @@
signature CONJ_DISJ_PERM =
sig
- val conj_disj_perm_tac: int -> tactic
+ val conj_disj_perm_tac: Proof.context -> int -> tactic
end
structure Conj_Disj_Perm: CONJ_DISJ_PERM =
@@ -118,10 +118,10 @@
| (True, Disj) => contrapos (prove_contradiction_eq false) cp
| _ => raise CTERM ("prove_conj_disj_perm", [ct]))
-val conj_disj_perm_tac = CSUBGOAL (fn (ct, i) =>
+fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) =>
(case Thm.term_of ct of
@{const HOL.Trueprop} $ (@{const HOL.eq(bool)} $ _ $ _) =>
- rtac (prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))) i
+ resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
| _ => no_tac))
end
--- a/src/HOL/Tools/SMT/smt_solver.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Jul 18 20:47:08 2015 +0200
@@ -289,13 +289,14 @@
"configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")
| SMT_Failure.SMT fail => error (str_of ctxt fail)
- fun resolve (SOME thm) = rtac thm 1
- | resolve NONE = no_tac
+ fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
+ | resolve _ NONE = no_tac
fun tac prove ctxt rules =
CONVERSION (SMT_Normalize.atomize_conv ctxt)
- THEN' rtac @{thm ccontr}
- THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve (prove ctxt' (rules @ prems))) ctxt
+ THEN' resolve_tac ctxt @{thms ccontr}
+ THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
+ resolve ctxt' (prove ctxt' (rules @ prems))) ctxt
in
val smt_tac = tac safe_solve
--- a/src/HOL/Tools/SMT/z3_replay.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay.ML Sat Jul 18 20:47:08 2015 +0200
@@ -148,10 +148,10 @@
in
fun discharge_sk_tac ctxt i st =
- (rtac @{thm trans} i
+ (resolve_tac ctxt @{thms trans} i
THEN resolve_tac ctxt sk_rules i
- THEN (rtac @{thm refl} ORELSE' discharge_sk_tac ctxt) (i+1)
- THEN rtac @{thm refl} i) st
+ THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1)
+ THEN resolve_tac ctxt @{thms refl} i) st
end
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sat Jul 18 20:47:08 2015 +0200
@@ -443,9 +443,9 @@
fun lift_ite_rewrite ctxt t =
prove ctxt t (fn ctxt =>
CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt)))
- THEN' rtac @{thm refl})
+ THEN' resolve_tac ctxt @{thms refl})
-fun prove_conj_disj_perm ctxt t = prove ctxt t (fn _ => Conj_Disj_Perm.conj_disj_perm_tac)
+fun prove_conj_disj_perm ctxt t = prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac
fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [
("rules", apply_rule ctxt),
@@ -492,8 +492,8 @@
val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
- REPEAT_ALL_NEW (rtac quant_inst_rule)
- THEN' rtac @{thm excluded_middle})
+ REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule])
+ THEN' resolve_tac ctxt @{thms excluded_middle})
(* propositional lemma *)
--- a/src/HOL/Tools/Transfer/transfer.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Sat Jul 18 20:47:08 2015 +0200
@@ -627,7 +627,7 @@
fun eq_rules_tac ctxt eq_rules =
TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules)
- THEN_ALL_NEW rtac @{thm is_equality_eq}
+ THEN_ALL_NEW resolve_tac ctxt @{thms is_equality_eq}
fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt)
@@ -646,8 +646,8 @@
val end_tac = if equiv then K all_tac else K no_tac
val err_msg = "Transfer failed to convert goal to an object-logic formula"
fun main_tac (t, i) =
- rtac start_rule i THEN
- (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
+ resolve_tac ctxt [start_rule] i THEN
+ (resolve_tac ctxt [transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)]
THEN_ALL_NEW
(SOLVED'
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
@@ -673,12 +673,13 @@
in
EVERY
[CONVERSION prep_conv i,
- rtac @{thm transfer_prover_start} i,
- ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
+ resolve_tac ctxt @{thms transfer_prover_start} i,
+ ((resolve_tac ctxt [rule1] ORELSE'
+ (CONVERSION expand_eq_in_rel THEN' resolve_tac ctxt [rule1]))
THEN_ALL_NEW
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
(DETERM o eq_rules_tac ctxt eq_rules))) (i + 1),
- rtac @{thm refl} i]
+ resolve_tac ctxt @{thms refl} i]
end)
(** Transfer attribute **)
@@ -702,7 +703,7 @@
val rule = transfer_rule_of_lhs ctxt' t
val tac =
resolve_tac ctxt' [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
- (rtac rule
+ (resolve_tac ctxt' [rule]
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
@@ -737,8 +738,8 @@
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
val rule = transfer_rule_of_term ctxt' true t
val tac =
- rtac (thm2 RS start_rule) 1 THEN
- (rtac rule
+ resolve_tac ctxt' [thm2 RS start_rule] 1 THEN
+ (resolve_tac ctxt' [rule]
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
--- a/src/HOL/Tools/datatype_realizer.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Sat Jul 18 20:47:08 2015 +0200
@@ -113,11 +113,11 @@
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
- rtac (cterm_instantiate inst induct) 1,
+ resolve_tac ctxt [cterm_instantiate inst induct] 1,
ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
- REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
+ REPEAT (eresolve_tac ctxt [allE] i) THEN assume_tac ctxt i)) 1)])
|> Drule.export_without_context;
val ind_name = Thm.derivation_name induct;
@@ -190,7 +190,7 @@
(HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
+ resolve_tac ctxt [cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust] 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
--- a/src/HOL/Tools/groebner.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/groebner.ML Sat Jul 18 20:47:08 2015 +0200
@@ -931,11 +931,11 @@
Object_Logic.full_atomize_tac ctxt
THEN' presimplify ctxt add_ths del_ths
THEN' CSUBGOAL (fn (p, i) =>
- rtac (let val form = Object_Logic.dest_judgment ctxt p
+ resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p
in case get_ring_ideal_convs ctxt form of
NONE => Thm.reflexive form
| SOME thy => #ring_conv thy ctxt form
- end) i
+ end] i
handle TERM _ => no_tac
| CTERM _ => no_tac
| THM _ => no_tac);
@@ -944,8 +944,9 @@
fun lhs t = case Thm.term_of t of
Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
- fun exitac NONE = no_tac
- | exitac (SOME y) = rtac (instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI) 1
+ fun exitac _ NONE = no_tac
+ | exitac ctxt (SOME y) =
+ resolve_tac ctxt [instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
val claset = claset_of @{context}
in
@@ -964,7 +965,7 @@
val ps = map_filter (try (lhs o Thm.dest_arg)) asms
val cfs = (map swap o #multi_ideal thy evs ps)
(map Thm.dest_arg1 (conjuncts bod))
- val ws = map (exitac o AList.lookup op aconvc cfs) evs
+ val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
in EVERY (rev ws) THEN Method.insert_tac prems 1
THEN ring_tac add_ths del_ths ctxt 1
end
--- a/src/HOL/Tools/inductive_realizer.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Jul 18 20:47:08 2015 +0200
@@ -393,11 +393,12 @@
val thm = Goal.prove_global thy []
(map attach_typeS prems) (attach_typeS concl)
(fn {context = ctxt, prems} => EVERY
- [rtac (#raw_induct ind_info) 1,
+ [resolve_tac ctxt [#raw_induct ind_info] 1,
rewrite_goals_tac ctxt rews,
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
- DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
+ DEPTH_SOLVE_1 o
+ FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]]]) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
@@ -456,11 +457,12 @@
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz')
(fn {context = ctxt, prems, ...} => EVERY
[cut_tac (hd prems) 1,
- etac elimR 1,
+ eresolve_tac ctxt [elimR] 1,
ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
rewrite_goals_tac ctxt rews,
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
- DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
+ DEPTH_SOLVE_1 o
+ FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
in
--- a/src/HOL/Tools/record.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/record.ML Sat Jul 18 20:47:08 2015 +0200
@@ -112,7 +112,7 @@
in
thy
|> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV repT) NONE (fn _ => rtac UNIV_witness 1)
+ (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
@@ -184,7 +184,7 @@
(case Symtab.lookup isthms (#1 is) of
SOME isthm => isthm
| NONE => err "no thm found for constant" (Const is));
- in rtac isthm i end);
+ in resolve_tac ctxt [isthm] i end);
end;
@@ -1380,7 +1380,7 @@
val thm = cterm_instantiate [(crec, cfree)] induct_thm;
in
simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
- rtac thm i THEN
+ resolve_tac ctxt [thm] i THEN
simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_rulify}) i
end;
@@ -1591,9 +1591,9 @@
(fn {context = ctxt, ...} =>
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
REPEAT_DETERM
- (rtac @{thm refl_conj_eq} 1 ORELSE
+ (resolve_tac ctxt @{thms refl_conj_eq} 1 ORELSE
Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
- rtac refl 1))));
+ resolve_tac ctxt [refl] 1))));
(*We need a surjection property r = (| f = f r, g = g r ... |)
@@ -1610,7 +1610,8 @@
val tactic1 =
simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1;
- val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
+ val tactic2 =
+ REPEAT (resolve_tac defs_ctxt [surject_assistI] 1 THEN resolve_tac defs_ctxt [refl] 1);
val [halfway] = Seq.list_of (tactic1 start);
val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
in
@@ -1621,10 +1622,11 @@
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
(fn {context = ctxt, ...} =>
EVERY1
- [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
- etac @{thm meta_allE}, assume_tac ctxt,
- rtac (@{thm prop_subst} OF [surject]),
- REPEAT o etac @{thm meta_allE}, assume_tac ctxt]));
+ [resolve_tac ctxt @{thms equal_intr_rule},
+ Goal.norm_hhf_tac ctxt,
+ eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt,
+ resolve_tac ctxt [@{thm prop_subst} OF [surject]],
+ REPEAT o eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt]));
val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
@@ -1748,7 +1750,7 @@
fun tac ctxt eq_def =
Class.intro_classes_tac ctxt []
THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
- THEN ALLGOALS (rtac @{thm refl});
+ THEN ALLGOALS (resolve_tac ctxt @{thms refl});
fun mk_eq thy eq_def =
rewrite_rule (Proof_Context.init_global thy)
[Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
@@ -1946,7 +1948,8 @@
val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars;
val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
val init_thm = named_cterm_instantiate insts updacc_eq_triv;
- val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
+ val terminal =
+ resolve_tac ext_ctxt [updacc_eq_idI] 1 THEN resolve_tac ext_ctxt [refl] 1;
val tactic =
simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal);
@@ -2131,11 +2134,11 @@
Goal.prove_sorry_global defs_thy [] [] surjective_prop
(fn {context = ctxt, ...} =>
EVERY
- [rtac surject_assist_idE 1,
+ [resolve_tac ctxt [surject_assist_idE] 1,
simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
REPEAT
(Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
- (rtac surject_assistI 1 THEN
+ (resolve_tac ctxt [surject_assistI] 1 THEN
simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
@@ -2143,7 +2146,7 @@
Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
(fn {context = ctxt, prems, ...} =>
resolve_tac ctxt prems 1 THEN
- rtac surjective 1));
+ resolve_tac ctxt [surjective] 1));
val cases = timeit_msg ctxt "record cases proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] cases_prop
@@ -2156,26 +2159,26 @@
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
(fn {context = ctxt', ...} =>
EVERY1
- [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
- etac @{thm meta_allE}, assume_tac ctxt',
- rtac (@{thm prop_subst} OF [surjective]),
- REPEAT o etac @{thm meta_allE}, assume_tac ctxt']));
+ [resolve_tac ctxt' @{thms equal_intr_rule}, Goal.norm_hhf_tac ctxt',
+ eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
+ resolve_tac ctxt' [@{thm prop_subst} OF [surjective]],
+ REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_object_prop
(fn {context = ctxt, ...} =>
- rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
+ resolve_tac ctxt [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
- rtac split_meta 1));
+ resolve_tac ctxt [split_meta] 1));
val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_ex_prop
(fn {context = ctxt, ...} =>
simp_tac
(put_simpset HOL_basic_ss ctxt addsimps
- (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} ::
+ (@{lemma "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> P x)" by simp} ::
@{thms not_not Not_eq_iff})) 1 THEN
- rtac split_object 1));
+ resolve_tac ctxt [split_object] 1));
val equality = timeit_msg ctxt "record equality proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] equality_prop
--- a/src/HOL/Tools/reification.ML Sat Jul 18 20:37:16 2015 +0200
+++ b/src/HOL/Tools/reification.ML Sat Jul 18 20:47:08 2015 +0200
@@ -32,7 +32,7 @@
val thm = conv ct;
in
if Thm.is_reflexive thm then no_tac
- else ALLGOALS (rtac (pure_subst OF [thm]))
+ else ALLGOALS (resolve_tac ctxt [pure_subst OF [thm]])
end) ctxt;
(* Make a congruence rule out of a defining equation for the interpretation
@@ -82,7 +82,7 @@
(Goal.prove ctxt'' [] (map mk_def env)
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
(fn {context, prems, ...} =>
- Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
+ Local_Defs.unfold_tac context (map tryext prems) THEN resolve_tac ctxt'' [th'] 1)) RS sym;
val (cong' :: vars') =
Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Thm.cterm_of ctxt'') vs);
val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';