# HG changeset patch # User wenzelm # Date 1437768999 -7200 # Node ID 6c28d8ed2488b0e6f25b07c54f55bcc1739254e2 # Parent d09c66a0ea10ebd3a6e25c9a31feee32c965011c proper context; diff -r d09c66a0ea10 -r 6c28d8ed2488 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/FOLP/simp.ML Fri Jul 24 22:16:39 2015 +0200 @@ -36,7 +36,7 @@ val delrews : simpset * thm list -> simpset val dest_ss : simpset -> thm list * thm list val print_ss : Proof.context -> simpset -> unit - val setauto : simpset * (int -> tactic) -> simpset + val setauto : simpset * (Proof.context -> int -> tactic) -> simpset val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic val ASM_SIMP_TAC : Proof.context -> simpset -> int -> tactic val CASE_TAC : Proof.context -> simpset -> int -> tactic @@ -235,14 +235,14 @@ (* SIMPSET *) datatype simpset = - SS of {auto_tac: int -> tactic, + SS of {auto_tac: Proof.context -> int -> tactic, congs: thm list, cong_net: thm Net.net, mk_simps: Proof.context -> thm -> thm list, simps: (thm * thm list) list, simp_net: thm Net.net} -val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, +val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty, mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty}; (** Insertion of congruences and rewrites **) @@ -446,7 +446,7 @@ else (ss,thm,anet,ats,cs); fun try_true(thm,ss,anet,ats,cs) = - case Seq.pull(auto_tac i thm) of + case Seq.pull(auto_tac ctxt i thm) of SOME(thm',_) => (ss,thm',anet,ats,cs) | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs in if !tracing @@ -486,7 +486,7 @@ (fn thm => if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm))) - THEN TRY(auto_tac i) + THEN TRY(auto_tac ctxt i) end; fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false); diff -r d09c66a0ea10 -r 6c28d8ed2488 src/FOLP/simpdata.ML --- a/src/FOLP/simpdata.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/FOLP/simpdata.ML Fri Jul 24 22:16:39 2015 +0200 @@ -76,7 +76,7 @@ open FOLP_Simp; -val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; +val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI}); val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews; diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Jul 24 22:16:39 2015 +0200 @@ -2550,7 +2550,7 @@ *--------------------------------------------------------------------------*) fun std_postprocessor ctxt strict wfs = Prim.postprocess ctxt strict - {wf_tac = REPEAT (ares_tac wfs 1), + {wf_tac = REPEAT (ares_tac ctxt wfs 1), terminator = asm_simp_tac ctxt 1 THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Jul 24 22:16:39 2015 +0200 @@ -456,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 eresolve_tac ctxt [allE]) THEN' ares_tac elem_thms)) 1)]); + ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac ctxt elem_thms)) 1)]); in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end; @@ -573,7 +573,7 @@ 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 (resolve_tac ctxt @{thms ext} 1), + REPEAT (ares_tac ctxt [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; @@ -652,7 +652,7 @@ [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 eresolve_tac ctxt [allE] 1)])) + DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)])) (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]); val ([(_, [dt_induct'])], thy7) = diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Jul 24 22:16:39 2015 +0200 @@ -178,7 +178,7 @@ (EVERY [DETERM tac, REPEAT (eresolve_tac ctxt @{thms ex1E} 1), resolve_tac ctxt @{thms ex1I} 1, - DEPTH_SOLVE_1 (ares_tac [intr] 1), + DEPTH_SOLVE_1 (ares_tac ctxt [intr] 1), REPEAT_DETERM_N k (eresolve_tac ctxt [thin_rl] 1 THEN rotate_tac 1 1), eresolve_tac ctxt [elim] 1, REPEAT_DETERM_N j distinct_tac, diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Jul 24 22:16:39 2015 +0200 @@ -41,7 +41,7 @@ [REPEAT (Always_Int_tac ctxt 1), eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) - REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, + REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2, diff -r d09c66a0ea10 -r 6c28d8ed2488 src/HOL/ex/MT.thy --- a/src/HOL/ex/MT.thy Thu Jul 23 22:13:42 2015 +0200 +++ b/src/HOL/ex/MT.thy Fri Jul 24 22:16:39 2015 +0200 @@ -276,7 +276,7 @@ (* ############################################################ *) ML {* -val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1) +fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1) *} lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))" @@ -395,7 +395,7 @@ lemma eval_fun_mono: "mono(eval_fun)" unfolding mono_def eval_fun_def -apply (tactic infsys_mono_tac) +apply (tactic "infsys_mono_tac @{context}") done (* Introduction rules *) @@ -519,7 +519,7 @@ lemma elab_fun_mono: "mono(elab_fun)" unfolding mono_def elab_fun_def -apply (tactic infsys_mono_tac) +apply (tactic "infsys_mono_tac @{context}") done (* Introduction rules *) @@ -747,7 +747,7 @@ lemma mono_hasty_fun: "mono(hasty_fun)" unfolding mono_def hasty_fun_def -apply (tactic infsys_mono_tac) +apply (tactic "infsys_mono_tac @{context}") apply blast done diff -r d09c66a0ea10 -r 6c28d8ed2488 src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/Provers/quantifier1.ML Fri Jul 24 22:16:39 2015 +0200 @@ -144,7 +144,7 @@ ALLGOALS (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE], resolve_tac ctxt [Data.exI], - DEPTH_SOLVE_1 o ares_tac [Data.conjI]]) + DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]]) end; (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) = @@ -157,7 +157,7 @@ REPEAT o resolve_tac ctxt [Data.impI], eresolve_tac ctxt [Data.mp], REPEAT o eresolve_tac ctxt [Data.conjE], - REPEAT o ares_tac [Data.conjI]]); + REPEAT o ares_tac ctxt [Data.conjI]]); val allcomm = Data.all_comm RS Data.iff_trans; in fun prove_one_point_all_tac ctxt = diff -r d09c66a0ea10 -r 6c28d8ed2488 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/Pure/tactic.ML Fri Jul 24 22:16:39 2015 +0200 @@ -27,7 +27,7 @@ val dtac: thm -> int -> tactic val etac: thm -> int -> tactic val ftac: thm -> int -> tactic - val ares_tac: thm list -> int -> tactic + val ares_tac: Proof.context -> thm list -> int -> tactic val solve_tac: Proof.context -> thm list -> int -> tactic val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic val match_tac: Proof.context -> thm list -> int -> tactic @@ -144,8 +144,8 @@ fun etac rl = eresolve0_tac [rl]; fun ftac rl = forward0_tac [rl]; -(*Use an assumption or some rules ... A popular combination!*) -fun ares_tac rules = atac ORELSE' resolve0_tac rules; +(*Use an assumption or some rules*) +fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules; fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt; diff -r d09c66a0ea10 -r 6c28d8ed2488 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Jul 24 22:16:39 2015 +0200 @@ -189,7 +189,7 @@ Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1, - REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]); + REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]); val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs); @@ -306,9 +306,9 @@ (*Minimizes backtracking by delivering the correct premise to each goal. Intro rules with extra Vars in premises still cause some backtracking *) - fun ind_tac [] 0 = all_tac - | ind_tac(prem::prems) i = - DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1); + fun ind_tac _ [] 0 = all_tac + | ind_tac ctxt (prem::prems) i = + DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1); val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT); @@ -349,7 +349,7 @@ some premise involves disjunction.*) REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm exE}, @{thm conjE}] ORELSE' (bound_hyp_subst_tac ctxt))), - ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]); + ind_tac ctxt (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]); val dummy = if ! Ind_Syntax.trace then @@ -474,7 +474,7 @@ REPEAT (resolve_tac ctxt @{thms impI} 1) THEN resolve_tac ctxt [rewrite_rule ctxt all_defs prem] 1 THEN (*prem must not be REPEATed below: could loop!*) - DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE' + DEPTH_SOLVE (FIRSTGOAL (ares_tac ctxt [@{thm impI}] ORELSE' eresolve_tac ctxt (@{thm conjE} :: @{thm mp} :: cmonos)))) ) i) THEN mutual_ind_tac ctxt prems (i-1); diff -r d09c66a0ea10 -r 6c28d8ed2488 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/ZF/Tools/typechk.ML Fri Jul 24 22:16:39 2015 +0200 @@ -102,7 +102,7 @@ fun type_solver_tac ctxt hyps = SELECT_GOAL (DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1 ORELSE resolve_from_net_tac ctxt basic_net 1 - ORELSE (ares_tac hyps 1 + ORELSE (ares_tac ctxt hyps 1 APPEND typecheck_step_tac ctxt))); val type_solver = diff -r d09c66a0ea10 -r 6c28d8ed2488 src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Jul 23 22:13:42 2015 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Fri Jul 24 22:16:39 2015 +0200 @@ -355,7 +355,7 @@ (EVERY [REPEAT (Always_Int_tac ctxt 1), eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) - REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, + REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,