# HG changeset patch # User wenzelm # Date 1437245228 -7200 # Node ID b48830b670a1c7351dae9ae4ce9514ecb117dbac # Parent 83f04804696cc1aca327a1e78399f1a0f82e31da prefer tactics with explicit context; diff -r 83f04804696c -r b48830b670a1 src/HOL/Filter.thy --- 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) *} diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Countable.thy --- 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) \ diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Multiset.thy --- 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 \ diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Old_SMT/old_smt_solver.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- 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') diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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); diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/bnf_lfp_countable.ML --- 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)); diff -r 83f04804696c -r b48830b670a1 src/HOL/Library/old_recdef.ML --- 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'= diff -r 83f04804696c -r b48830b670a1 src/HOL/List.thy --- 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 \ 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 \ 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 "(\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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_comp.ML --- 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) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- 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]}; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_def_tactics.ML --- 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); diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- 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; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- 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; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/BNF/bnf_tactics.ML --- 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; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- 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}; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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]; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Function/function_core.ML --- 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) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Function/lexicographic_order.ML --- 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; diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Function/scnp_reconstruct.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Function/termination.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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) = diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Predicate_Compile/core_data.ML --- 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, ...} => diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- 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" diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Qelim/cooper.ML --- 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); diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Quickcheck/random_generators.ML --- 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); diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Quotient/quotient_type.ML --- 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 *) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/SMT/conj_disj_perm.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/SMT/z3_replay.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 *) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/Transfer/transfer.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/datatype_realizer.ML --- 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)])]) diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/groebner.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/inductive_realizer.ML --- 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/record.ML --- 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 \ Trueprop B \ 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 "\x. P x \ \ (\x. \ 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 diff -r 83f04804696c -r b48830b670a1 src/HOL/Tools/reification.ML --- 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';