qualified Subgoal.FOCUS;
authorwenzelm
Thu Jul 30 12:20:43 2009 +0200 (2009-07-30)
changeset 322833bebc195c124
parent 32282 853ef99c04cc
child 32284 d8ee8a956f19
qualified Subgoal.FOCUS;
src/CCL/Wfd.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Prolog/prolog.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/record.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/sat_funcs.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/trancl.ML
src/Pure/subgoal.ML
     1.1 --- a/src/CCL/Wfd.thy	Thu Jul 30 11:23:57 2009 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Thu Jul 30 12:20:43 2009 +0200
     1.3 @@ -499,7 +499,7 @@
     1.4  in
     1.5  
     1.6  fun eval_tac ths =
     1.7 -  FOCUS_PREMS (fn {context, prems, ...} =>
     1.8 +  Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
     1.9      DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
    1.10  
    1.11  val eval_setup =
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 30 11:23:57 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 30 12:20:43 2009 +0200
     2.3 @@ -3337,7 +3337,7 @@
     2.4        REPEAT (FIRST' [etac @{thm intervalE},
     2.5                        etac @{thm meta_eqE},
     2.6                        rtac @{thm impI}] i)
     2.7 -      THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
     2.8 +      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
     2.9        THEN TRY (filter_prems_tac (K false) i)
    2.10        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
    2.11        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
     3.1 --- a/src/HOL/Prolog/prolog.ML	Thu Jul 30 11:23:57 2009 +0200
     3.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Jul 30 12:20:43 2009 +0200
     3.3 @@ -67,7 +67,7 @@
     3.4          imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
     3.5          imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
     3.6  
     3.7 -(*val hyp_resolve_tac = FOCUS_PREMS (fn {prems, ...} =>
     3.8 +(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
     3.9                                    resolve_tac (maps atomizeD prems) 1);
    3.10    -- is nice, but cannot instantiate unknowns in the assumptions *)
    3.11  fun hyp_resolve_tac i st = let
     4.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 11:23:57 2009 +0200
     4.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 12:20:43 2009 +0200
     4.3 @@ -517,7 +517,7 @@
     4.4  
     4.5  fun cnf_rewrite_tac ctxt i =
     4.6  	(* cut the CNF formulas as new premises *)
     4.7 -	FOCUS (fn {prems, ...} =>
     4.8 +	Subgoal.FOCUS (fn {prems, ...} =>
     4.9  		let
    4.10  		  val thy = ProofContext.theory_of ctxt
    4.11  			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
    4.12 @@ -540,7 +540,7 @@
    4.13  
    4.14  fun cnfx_rewrite_tac ctxt i =
    4.15  	(* cut the CNF formulas as new premises *)
    4.16 -	FOCUS (fn {prems, ...} =>
    4.17 +	Subgoal.FOCUS (fn {prems, ...} =>
    4.18  		let
    4.19  		  val thy = ProofContext.theory_of ctxt;
    4.20  			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
     5.1 --- a/src/HOL/Tools/meson.ML	Thu Jul 30 11:23:57 2009 +0200
     5.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 30 12:20:43 2009 +0200
     5.3 @@ -586,9 +586,9 @@
     5.4    SELECT_GOAL
     5.5      (EVERY [ObjectLogic.atomize_prems_tac 1,
     5.6              rtac ccontr 1,
     5.7 -            FOCUS (fn {context = ctxt', prems = negs, ...} =>
     5.8 +            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
     5.9                        EVERY1 [skolemize_prems_tac ctxt negs,
    5.10 -                              FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    5.11 +                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    5.12    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    5.13  
    5.14  (** Best-first search versions **)
     6.1 --- a/src/HOL/Tools/record.ML	Thu Jul 30 11:23:57 2009 +0200
     6.2 +++ b/src/HOL/Tools/record.ML	Thu Jul 30 12:20:43 2009 +0200
     6.3 @@ -2161,7 +2161,7 @@
     6.4        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
     6.5          st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
     6.6          THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
     6.7 -        THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
     6.8 +        THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
     6.9               (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
    6.10        end);
    6.11       val equality = timeit_msg "record equality proof:" equality_prf;
     7.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jul 30 11:23:57 2009 +0200
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jul 30 12:20:43 2009 +0200
     7.3 @@ -517,7 +517,7 @@
     7.4    SUBGOAL (fn (prop, i) =>
     7.5      let val ts = Logic.strip_assums_hyp prop in
     7.6        EVERY'
     7.7 -       [FOCUS
     7.8 +       [Subgoal.FOCUS
     7.9           (fn {prems, ...} =>
    7.10             (Method.insert_tac
    7.11               (map forall_intr_vars (neg_clausify prems)) i)) ctxt,
     8.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 30 11:23:57 2009 +0200
     8.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 30 12:20:43 2009 +0200
     8.3 @@ -411,7 +411,7 @@
     8.4  (* ------------------------------------------------------------------------- *)
     8.5  
     8.6  fun rawsat_tac ctxt i =
     8.7 -  FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
     8.8 +  Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
     8.9  
    8.10  (* ------------------------------------------------------------------------- *)
    8.11  (* pre_cnf_tac: converts the i-th subgoal                                    *)
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 30 11:23:57 2009 +0200
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 30 12:20:43 2009 +0200
     9.3 @@ -788,7 +788,7 @@
     9.4            all_tac) THEN
     9.5            PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
     9.6            (* use theorems generated from the actual justifications *)
     9.7 -          FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
     9.8 +          Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
     9.9      in
    9.10        (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
    9.11        DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
    10.1 --- a/src/Provers/order.ML	Thu Jul 30 11:23:57 2009 +0200
    10.2 +++ b/src/Provers/order.ML	Thu Jul 30 12:20:43 2009 +0200
    10.3 @@ -1235,12 +1235,12 @@
    10.4     val prfs = gen_solve mkconcl thy (lesss, C);
    10.5     val (subgoals, prf) = mkconcl decomp less_thms thy C;
    10.6    in
    10.7 -   FOCUS (fn {prems = asms, ...} =>
    10.8 +   Subgoal.FOCUS (fn {prems = asms, ...} =>
    10.9       let val thms = map (prove (prems @ asms)) prfs
   10.10       in rtac (prove thms prf) 1 end) ctxt n st
   10.11    end
   10.12    handle Contr p =>
   10.13 -      (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
   10.14 +      (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
   10.15          handle Subscript => Seq.empty)
   10.16     | Cannot => Seq.empty
   10.17     | Subscript => Seq.empty)
    11.1 --- a/src/Provers/quasi.ML	Thu Jul 30 11:23:57 2009 +0200
    11.2 +++ b/src/Provers/quasi.ML	Thu Jul 30 12:20:43 2009 +0200
    11.3 @@ -560,11 +560,11 @@
    11.4  
    11.5    val (subgoal, prf) = mkconcl_trans thy C;
    11.6   in
    11.7 -  FOCUS (fn {prems, ...} =>
    11.8 +  Subgoal.FOCUS (fn {prems, ...} =>
    11.9      let val thms = map (prove prems) prfs
   11.10      in rtac (prove thms prf) 1 end) ctxt n st
   11.11   end
   11.12 - handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   11.13 + handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   11.14    | Cannot  => Seq.empty);
   11.15  
   11.16  
   11.17 @@ -580,12 +580,12 @@
   11.18    val prfs = solveQuasiOrder thy (lesss, C);
   11.19    val (subgoals, prf) = mkconcl_quasi thy C;
   11.20   in
   11.21 -  FOCUS (fn {prems, ...} =>
   11.22 +  Subgoal.FOCUS (fn {prems, ...} =>
   11.23      let val thms = map (prove prems) prfs
   11.24      in rtac (prove thms prf) 1 end) ctxt n st
   11.25   end
   11.26   handle Contr p =>
   11.27 -    (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   11.28 +    (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   11.29        handle Subscript => Seq.empty)
   11.30    | Cannot => Seq.empty
   11.31    | Subscript => Seq.empty);
    12.1 --- a/src/Provers/trancl.ML	Thu Jul 30 11:23:57 2009 +0200
    12.2 +++ b/src/Provers/trancl.ML	Thu Jul 30 12:20:43 2009 +0200
    12.3 @@ -541,7 +541,7 @@
    12.4    val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
    12.5    val prfs = solveTrancl (prems, C);
    12.6   in
    12.7 -  FOCUS (fn {prems, ...} =>
    12.8 +  Subgoal.FOCUS (fn {prems, ...} =>
    12.9      let val thms = map (prove thy rel prems) prfs
   12.10      in rtac (prove thy rel thms prf) 1 end) ctxt n st
   12.11   end
   12.12 @@ -558,7 +558,7 @@
   12.13    val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
   12.14    val prfs = solveRtrancl (prems, C);
   12.15   in
   12.16 -  FOCUS (fn {prems, ...} =>
   12.17 +  Subgoal.FOCUS (fn {prems, ...} =>
   12.18      let val thms = map (prove thy rel prems) prfs
   12.19      in rtac (prove thy rel thms prf) 1 end) ctxt n st
   12.20   end
    13.1 --- a/src/Pure/subgoal.ML	Thu Jul 30 11:23:57 2009 +0200
    13.2 +++ b/src/Pure/subgoal.ML	Thu Jul 30 12:20:43 2009 +0200
    13.3 @@ -133,8 +133,5 @@
    13.4  
    13.5  end;
    13.6  
    13.7 -val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
    13.8 -val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
    13.9 -val FOCUS = Subgoal.FOCUS;
   13.10  val SUBPROOF = Subgoal.SUBPROOF;
   13.11