proper context;
authorwenzelm
Fri Jul 24 22:16:39 2015 +0200 (2015-07-24)
changeset 607746c28d8ed2488
parent 60773 d09c66a0ea10
child 60775 4592a9118d0b
proper context;
src/FOLP/simp.ML
src/FOLP/simpdata.ML
src/HOL/Library/old_recdef.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/ex/MT.thy
src/Provers/quantifier1.ML
src/Pure/tactic.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/FOLP/simp.ML	Thu Jul 23 22:13:42 2015 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri Jul 24 22:16:39 2015 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    val delrews   : simpset * thm list -> simpset
     1.5    val dest_ss   : simpset -> thm list * thm list
     1.6    val print_ss  : Proof.context -> simpset -> unit
     1.7 -  val setauto   : simpset * (int -> tactic) -> simpset
     1.8 +  val setauto   : simpset * (Proof.context -> int -> tactic) -> simpset
     1.9    val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
    1.10    val ASM_SIMP_TAC      : Proof.context -> simpset -> int -> tactic
    1.11    val CASE_TAC          : Proof.context -> simpset -> int -> tactic
    1.12 @@ -235,14 +235,14 @@
    1.13  (* SIMPSET *)
    1.14  
    1.15  datatype simpset =
    1.16 -        SS of {auto_tac: int -> tactic,
    1.17 +        SS of {auto_tac: Proof.context -> int -> tactic,
    1.18                 congs: thm list,
    1.19                 cong_net: thm Net.net,
    1.20                 mk_simps: Proof.context -> thm -> thm list,
    1.21                 simps: (thm * thm list) list,
    1.22                 simp_net: thm Net.net}
    1.23  
    1.24 -val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty,
    1.25 +val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty,
    1.26                    mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty};
    1.27  
    1.28  (** Insertion of congruences and rewrites **)
    1.29 @@ -446,7 +446,7 @@
    1.30              else (ss,thm,anet,ats,cs);
    1.31  
    1.32  fun try_true(thm,ss,anet,ats,cs) =
    1.33 -    case Seq.pull(auto_tac i thm) of
    1.34 +    case Seq.pull(auto_tac ctxt i thm) of
    1.35        SOME(thm',_) => (ss,thm',anet,ats,cs)
    1.36      | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    1.37                in if !tracing
    1.38 @@ -486,7 +486,7 @@
    1.39      (fn thm =>
    1.40       if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
    1.41       else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
    1.42 -    THEN TRY(auto_tac i)
    1.43 +    THEN TRY(auto_tac ctxt i)
    1.44  end;
    1.45  
    1.46  fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false);
     2.1 --- a/src/FOLP/simpdata.ML	Thu Jul 23 22:13:42 2015 +0200
     2.2 +++ b/src/FOLP/simpdata.ML	Fri Jul 24 22:16:39 2015 +0200
     2.3 @@ -76,7 +76,7 @@
     2.4  
     2.5  open FOLP_Simp;
     2.6  
     2.7 -val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
     2.8 +val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI});
     2.9  
    2.10  val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews;
    2.11  
     3.1 --- a/src/HOL/Library/old_recdef.ML	Thu Jul 23 22:13:42 2015 +0200
     3.2 +++ b/src/HOL/Library/old_recdef.ML	Fri Jul 24 22:16:39 2015 +0200
     3.3 @@ -2550,7 +2550,7 @@
     3.4   *--------------------------------------------------------------------------*)
     3.5  fun std_postprocessor ctxt strict wfs =
     3.6    Prim.postprocess ctxt strict
     3.7 -   {wf_tac = REPEAT (ares_tac wfs 1),
     3.8 +   {wf_tac = REPEAT (ares_tac ctxt wfs 1),
     3.9      terminator =
    3.10        asm_simp_tac ctxt 1
    3.11        THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
     4.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Jul 23 22:13:42 2015 +0200
     4.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Jul 24 22:16:39 2015 +0200
     4.3 @@ -456,7 +456,7 @@
     4.4                    Object_Logic.atomize_prems_tac ctxt) 1,
     4.5                  rewrite_goals_tac ctxt rewrites,
     4.6                  REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW
     4.7 -                  ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac elem_thms)) 1)]);
     4.8 +                  ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac ctxt elem_thms)) 1)]);
     4.9  
    4.10        in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end;
    4.11  
    4.12 @@ -573,7 +573,7 @@
    4.13               dresolve_tac ctxt @{thms box_equals} 1,
    4.14               REPEAT (resolve_tac ctxt rep_thms 1),
    4.15               REPEAT (eresolve_tac ctxt inj_thms 1),
    4.16 -             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
    4.17 +             REPEAT (ares_tac ctxt [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
    4.18                 REPEAT (eresolve_tac ctxt (make_elim fun_cong :: inj_thms) 1),
    4.19                 assume_tac ctxt 1]))])
    4.20        end;
    4.21 @@ -652,7 +652,7 @@
    4.22               [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
    4.23                simp_tac (put_simpset HOL_basic_ss ctxt
    4.24                  addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
    4.25 -              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    4.26 +              DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    4.27                    (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
    4.28  
    4.29      val ([(_, [dt_induct'])], thy7) =
     5.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Jul 23 22:13:42 2015 +0200
     5.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Fri Jul 24 22:16:39 2015 +0200
     5.3 @@ -178,7 +178,7 @@
     5.4              (EVERY
     5.5                [DETERM tac,
     5.6                  REPEAT (eresolve_tac ctxt @{thms ex1E} 1), resolve_tac ctxt @{thms ex1I} 1,
     5.7 -                DEPTH_SOLVE_1 (ares_tac [intr] 1),
     5.8 +                DEPTH_SOLVE_1 (ares_tac ctxt [intr] 1),
     5.9                  REPEAT_DETERM_N k (eresolve_tac ctxt [thin_rl] 1 THEN rotate_tac 1 1),
    5.10                  eresolve_tac ctxt [elim] 1,
    5.11                  REPEAT_DETERM_N j distinct_tac,
     6.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Jul 23 22:13:42 2015 +0200
     6.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Jul 24 22:16:39 2015 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4       [REPEAT (Always_Int_tac ctxt 1),
     6.5        eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
     6.6            ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
     6.7 -          REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
     6.8 +          REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
     6.9                              @{thm EnsuresI}, @{thm ensuresI}] 1),
    6.10        (*now there are two subgoals: co & transient*)
    6.11        simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
     7.1 --- a/src/HOL/ex/MT.thy	Thu Jul 23 22:13:42 2015 +0200
     7.2 +++ b/src/HOL/ex/MT.thy	Fri Jul 24 22:16:39 2015 +0200
     7.3 @@ -276,7 +276,7 @@
     7.4  (* ############################################################ *)
     7.5  
     7.6  ML {*
     7.7 -val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
     7.8 +fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
     7.9  *}
    7.10  
    7.11  lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
    7.12 @@ -395,7 +395,7 @@
    7.13  
    7.14  lemma eval_fun_mono: "mono(eval_fun)"
    7.15  unfolding mono_def eval_fun_def
    7.16 -apply (tactic infsys_mono_tac)
    7.17 +apply (tactic "infsys_mono_tac @{context}")
    7.18  done
    7.19  
    7.20  (* Introduction rules *)
    7.21 @@ -519,7 +519,7 @@
    7.22  
    7.23  lemma elab_fun_mono: "mono(elab_fun)"
    7.24  unfolding mono_def elab_fun_def
    7.25 -apply (tactic infsys_mono_tac)
    7.26 +apply (tactic "infsys_mono_tac @{context}")
    7.27  done
    7.28  
    7.29  (* Introduction rules *)
    7.30 @@ -747,7 +747,7 @@
    7.31  
    7.32  lemma mono_hasty_fun: "mono(hasty_fun)"
    7.33  unfolding mono_def hasty_fun_def
    7.34 -apply (tactic infsys_mono_tac)
    7.35 +apply (tactic "infsys_mono_tac @{context}")
    7.36  apply blast
    7.37  done
    7.38  
     8.1 --- a/src/Provers/quantifier1.ML	Thu Jul 23 22:13:42 2015 +0200
     8.2 +++ b/src/Provers/quantifier1.ML	Fri Jul 24 22:16:39 2015 +0200
     8.3 @@ -144,7 +144,7 @@
     8.4      ALLGOALS
     8.5        (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
     8.6          resolve_tac ctxt [Data.exI],
     8.7 -        DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
     8.8 +        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
     8.9  end;
    8.10  
    8.11  (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
    8.12 @@ -157,7 +157,7 @@
    8.13          REPEAT o resolve_tac ctxt [Data.impI],
    8.14          eresolve_tac ctxt [Data.mp],
    8.15          REPEAT o eresolve_tac ctxt [Data.conjE],
    8.16 -        REPEAT o ares_tac [Data.conjI]]);
    8.17 +        REPEAT o ares_tac ctxt [Data.conjI]]);
    8.18    val allcomm = Data.all_comm RS Data.iff_trans;
    8.19  in
    8.20    fun prove_one_point_all_tac ctxt =
     9.1 --- a/src/Pure/tactic.ML	Thu Jul 23 22:13:42 2015 +0200
     9.2 +++ b/src/Pure/tactic.ML	Fri Jul 24 22:16:39 2015 +0200
     9.3 @@ -27,7 +27,7 @@
     9.4    val dtac: thm -> int -> tactic
     9.5    val etac: thm -> int -> tactic
     9.6    val ftac: thm -> int -> tactic
     9.7 -  val ares_tac: thm list -> int -> tactic
     9.8 +  val ares_tac: Proof.context -> thm list -> int -> tactic
     9.9    val solve_tac: Proof.context -> thm list -> int -> tactic
    9.10    val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
    9.11    val match_tac: Proof.context -> thm list -> int -> tactic
    9.12 @@ -144,8 +144,8 @@
    9.13  fun etac rl = eresolve0_tac [rl];
    9.14  fun ftac rl =  forward0_tac [rl];
    9.15  
    9.16 -(*Use an assumption or some rules ... A popular combination!*)
    9.17 -fun ares_tac rules = atac  ORELSE'  resolve0_tac rules;
    9.18 +(*Use an assumption or some rules*)
    9.19 +fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
    9.20  
    9.21  fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt;
    9.22  
    10.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jul 23 22:13:42 2015 +0200
    10.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Jul 24 22:16:39 2015 +0200
    10.3 @@ -189,7 +189,7 @@
    10.4      Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
    10.5        (fn {context = ctxt, ...} => EVERY
    10.6          [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
    10.7 -         REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
    10.8 +         REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
    10.9  
   10.10    val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
   10.11  
   10.12 @@ -306,9 +306,9 @@
   10.13  
   10.14       (*Minimizes backtracking by delivering the correct premise to each goal.
   10.15         Intro rules with extra Vars in premises still cause some backtracking *)
   10.16 -     fun ind_tac [] 0 = all_tac
   10.17 -       | ind_tac(prem::prems) i =
   10.18 -             DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1);
   10.19 +     fun ind_tac _ [] 0 = all_tac
   10.20 +       | ind_tac ctxt (prem::prems) i =
   10.21 +             DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1);
   10.22  
   10.23       val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
   10.24  
   10.25 @@ -349,7 +349,7 @@
   10.26                some premise involves disjunction.*)
   10.27              REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm exE}, @{thm conjE}]
   10.28                                 ORELSE' (bound_hyp_subst_tac ctxt))),
   10.29 -            ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
   10.30 +            ind_tac ctxt (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
   10.31  
   10.32       val dummy =
   10.33        if ! Ind_Syntax.trace then
   10.34 @@ -474,7 +474,7 @@
   10.35                     REPEAT (resolve_tac ctxt @{thms impI} 1)  THEN
   10.36                     resolve_tac ctxt [rewrite_rule ctxt all_defs prem] 1  THEN
   10.37                     (*prem must not be REPEATed below: could loop!*)
   10.38 -                   DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
   10.39 +                   DEPTH_SOLVE (FIRSTGOAL (ares_tac ctxt [@{thm impI}] ORELSE'
   10.40                                             eresolve_tac ctxt (@{thm conjE} :: @{thm mp} :: cmonos))))
   10.41                 ) i)
   10.42              THEN mutual_ind_tac ctxt prems (i-1);
    11.1 --- a/src/ZF/Tools/typechk.ML	Thu Jul 23 22:13:42 2015 +0200
    11.2 +++ b/src/ZF/Tools/typechk.ML	Fri Jul 24 22:16:39 2015 +0200
    11.3 @@ -102,7 +102,7 @@
    11.4  fun type_solver_tac ctxt hyps = SELECT_GOAL
    11.5      (DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1
    11.6                    ORELSE resolve_from_net_tac ctxt basic_net 1
    11.7 -                  ORELSE (ares_tac hyps 1
    11.8 +                  ORELSE (ares_tac ctxt hyps 1
    11.9                            APPEND typecheck_step_tac ctxt)));
   11.10  
   11.11  val type_solver =
    12.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Jul 23 22:13:42 2015 +0200
    12.2 +++ b/src/ZF/UNITY/SubstAx.thy	Fri Jul 24 22:16:39 2015 +0200
    12.3 @@ -355,7 +355,7 @@
    12.4      (EVERY [REPEAT (Always_Int_tac ctxt 1),
    12.5              eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
    12.6                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    12.7 -                REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    12.8 +                REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    12.9                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
   12.10              (*now there are two subgoals: co & transient*)
   12.11              simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,