renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
authorwenzelm
Thu Jul 05 20:01:26 2007 +0200 (2007-07-05)
changeset 23590ad95084a5c63
parent 23589 aaba731fce86
child 23591 d32a85385e17
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
src/HOL/Complex/ex/linrtac.ML
src/HOL/Complex/ex/mirtac.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp_methods.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/coopertac.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/HOL/Complex/ex/linrtac.ML	Thu Jul 05 19:59:01 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Thu Jul 05 20:01:26 2007 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5  
     1.6  fun linr_tac ctxt q i = 
     1.7 -    (ObjectLogic.atomize_tac i) 
     1.8 +    (ObjectLogic.atomize_prems_tac i) 
     1.9  	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
    1.10  	THEN (fn st =>
    1.11    let
     2.1 --- a/src/HOL/Complex/ex/mirtac.ML	Thu Jul 05 19:59:01 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/mirtac.ML	Thu Jul 05 20:01:26 2007 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4  
     2.5  
     2.6  fun mir_tac ctxt q i = 
     2.7 -    (ObjectLogic.atomize_tac i)
     2.8 +    (ObjectLogic.atomize_prems_tac i)
     2.9  	THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
    2.10  	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
    2.11  	THEN (fn st =>
    2.12 @@ -161,4 +161,4 @@
    2.13       "decision procedure for MIR arithmetic");
    2.14  
    2.15  
    2.16 -end
    2.17 \ No newline at end of file
    2.18 +end
     3.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Jul 05 19:59:01 2007 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jul 05 20:01:26 2007 +0200
     3.3 @@ -1083,7 +1083,7 @@
     3.4        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
     3.5        (fn prems => EVERY
     3.6          [rtac indrule_lemma' 1,
     3.7 -         (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
     3.8 +         (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     3.9           EVERY (map (fn (prem, r) => (EVERY
    3.10             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
    3.11              simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
     4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 05 19:59:01 2007 +0200
     4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 05 20:01:26 2007 +0200
     4.3 @@ -215,7 +215,7 @@
     4.4          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
     4.5            (map cert insts)) induct;
     4.6          val (tac, _) = Library.foldl mk_unique_tac
     4.7 -          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
     4.8 +          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
     4.9                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
    4.10              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    4.11  
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 19:59:01 2007 +0200
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 20:01:26 2007 +0200
     5.3 @@ -122,7 +122,7 @@
     5.4        (fn prems =>
     5.5           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
     5.6            rtac (cterm_instantiate inst induction) 1,
     5.7 -          ALLGOALS ObjectLogic.atomize_tac,
     5.8 +          ALLGOALS ObjectLogic.atomize_prems_tac,
     5.9            rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
    5.10            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
    5.11              REPEAT (etac allE i) THEN atac i)) 1)]);
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 05 19:59:01 2007 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 05 20:01:26 2007 +0200
     6.3 @@ -403,7 +403,7 @@
     6.4  
     6.5          val inj_thm = Goal.prove_global thy5 [] []
     6.6            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
     6.7 -            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
     6.8 +            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     6.9               REPEAT (EVERY
    6.10                 [rtac allI 1, rtac impI 1,
    6.11                  exh_tac (exh_thm_of dt_info) 1,
    6.12 @@ -429,7 +429,7 @@
    6.13          val elem_thm = 
    6.14              Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    6.15                (fn _ =>
    6.16 -               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.17 +               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.18                  rewrite_goals_tac rewrites,
    6.19                  REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    6.20                    ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    6.21 @@ -465,7 +465,7 @@
    6.22      val iso_thms = if length descr = 1 then [] else
    6.23        Library.drop (length newTs, split_conj_thm
    6.24          (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
    6.25 -           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.26 +           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.27              REPEAT (rtac TrueI 1),
    6.28              rewrite_goals_tac (mk_meta_eq choice_eq ::
    6.29                symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
    6.30 @@ -606,7 +606,7 @@
    6.31        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    6.32        (fn prems => EVERY
    6.33          [rtac indrule_lemma' 1,
    6.34 -         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.35 +         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.36           EVERY (map (fn (prem, r) => (EVERY
    6.37             [REPEAT (eresolve_tac Abs_inverse_thms 1),
    6.38              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 19:59:01 2007 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 20:01:26 2007 +0200
     7.3 @@ -388,7 +388,7 @@
     7.4            [rtac (#raw_induct ind_info) 1,
     7.5             rewrite_goals_tac rews,
     7.6             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
     7.7 -             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
     7.8 +             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
     7.9                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    7.10          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    7.11            (NameSpace.qualified qualifier "induct" :: vs @ Ps @
    7.12 @@ -449,7 +449,7 @@
    7.13             etac elimR 1,
    7.14             ALLGOALS (asm_simp_tac HOL_basic_ss),
    7.15             rewrite_goals_tac rews,
    7.16 -           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
    7.17 +           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
    7.18               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    7.19          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    7.20            (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
     8.1 --- a/src/HOL/Tools/meson.ML	Thu Jul 05 19:59:01 2007 +0200
     8.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 05 20:01:26 2007 +0200
     8.3 @@ -556,7 +556,7 @@
     8.4    Function mkcl converts theorems to clauses.*)
     8.5  fun MESON mkcl cltac i st = 
     8.6    SELECT_GOAL
     8.7 -    (EVERY [ObjectLogic.atomize_tac 1,
     8.8 +    (EVERY [ObjectLogic.atomize_prems_tac 1,
     8.9              rtac ccontr 1,
    8.10  	    METAHYPS (fn negs =>
    8.11  		      EVERY1 [skolemize_prems_tac negs,
     9.1 --- a/src/HOL/Tools/res_atp_methods.ML	Thu Jul 05 19:59:01 2007 +0200
     9.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Thu Jul 05 20:01:26 2007 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4    
     9.5  (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
     9.6  fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
     9.7 -    (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
     9.8 +    (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
     9.9  		  METAHYPS(fn negs =>
    9.10  			      HEADGOAL(Tactic.rtac 
    9.11  					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    10.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 05 19:59:01 2007 +0200
    10.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 05 20:01:26 2007 +0200
    10.3 @@ -428,7 +428,7 @@
    10.4  
    10.5  val pre_cnf_tac =
    10.6          rtac ccontr THEN'
    10.7 -        ObjectLogic.atomize_tac THEN'
    10.8 +        ObjectLogic.atomize_prems_tac THEN'
    10.9          CONVERSION Drule.beta_eta_conversion;
   10.10  
   10.11  (* ------------------------------------------------------------------------- *)
    11.1 --- a/src/HOL/ex/coopertac.ML	Thu Jul 05 19:59:01 2007 +0200
    11.2 +++ b/src/HOL/ex/coopertac.ML	Thu Jul 05 20:01:26 2007 +0200
    11.3 @@ -65,7 +65,7 @@
    11.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    11.5  
    11.6  
    11.7 -fun linz_tac ctxt q i = ObjectLogic.atomize_tac i THEN (fn st =>
    11.8 +fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
    11.9    let
   11.10      val g = List.nth (prems_of st, i - 1)
   11.11      val thy = ProofContext.theory_of ctxt
   11.12 @@ -140,4 +140,4 @@
   11.13       linz_args linz_method,
   11.14       "decision procedure for linear integer arithmetic");
   11.15  
   11.16 -end
   11.17 \ No newline at end of file
   11.18 +end
    12.1 --- a/src/Pure/Isar/method.ML	Thu Jul 05 19:59:01 2007 +0200
    12.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 05 20:01:26 2007 +0200
    12.3 @@ -196,7 +196,7 @@
    12.4  
    12.5  (* atomize rule statements *)
    12.6  
    12.7 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
    12.8 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
    12.9    | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
   12.10  
   12.11  
   12.12 @@ -525,7 +525,7 @@
   12.13    bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
   12.14      (fn n => fn prems => fn ctxt => METHOD (fn facts =>
   12.15        HEADGOAL (insert_tac (prems @ facts) THEN'
   12.16 -      ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
   12.17 +      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
   12.18  
   12.19  end;
   12.20