misc tuning;
authorwenzelm
Tue Feb 10 16:46:21 2015 +0100 (2015-02-10)
changeset 5949914095f771781
parent 59498 50b60f501b05
child 59500 59817f489ce3
misc tuning;
src/CCL/CCL.thy
src/CCL/Type.thy
src/CCL/Wfd.thy
src/Cube/Example.thy
src/HOL/HOL.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Purchase.thy
src/HOL/Set.thy
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/simpdata.ML
     1.1 --- a/src/CCL/CCL.thy	Tue Feb 10 14:48:26 2015 +0100
     1.2 +++ b/src/CCL/CCL.thy	Tue Feb 10 16:46:21 2015 +0100
     1.3 @@ -204,7 +204,8 @@
     1.4        fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
     1.5        val inj_lemmas = maps mk_inj_lemmas rews
     1.6      in
     1.7 -      CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
     1.8 +      CHANGED (REPEAT (assume_tac ctxt i ORELSE
     1.9 +        resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
    1.10          eresolve_tac ctxt inj_lemmas i ORELSE
    1.11          asm_simp_tac (ctxt addsimps rews) i))
    1.12      end;
     2.1 --- a/src/CCL/Type.thy	Tue Feb 10 14:48:26 2015 +0100
     2.2 +++ b/src/CCL/Type.thy	Tue Feb 10 16:46:21 2015 +0100
     2.3 @@ -127,9 +127,10 @@
     2.4  fun mk_ncanT_tac top_crls crls =
     2.5    SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
     2.6      resolve_tac ctxt ([major] RL top_crls) 1 THEN
     2.7 -    REPEAT_SOME (eresolve_tac ctxt (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
     2.8 +    REPEAT_SOME (eresolve_tac ctxt (crls @ @{thms exE bexE conjE disjE})) THEN
     2.9      ALLGOALS (asm_simp_tac ctxt) THEN
    2.10 -    ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
    2.11 +    ALLGOALS (assume_tac ctxt ORELSE' resolve_tac ctxt (prems RL [@{thm lem}])
    2.12 +      ORELSE' eresolve_tac ctxt @{thms bspec}) THEN
    2.13      safe_tac (ctxt addSIs prems))
    2.14  *}
    2.15  
     3.1 --- a/src/CCL/Wfd.thy	Tue Feb 10 14:48:26 2015 +0100
     3.2 +++ b/src/CCL/Wfd.thy	Tue Feb 10 16:46:21 2015 +0100
     3.3 @@ -451,10 +451,11 @@
     3.4    THEN eresolve_tac ctxt @{thms rcall_lemmas} i
     3.5  
     3.6  fun raw_step_tac ctxt prems i =
     3.7 -  ares_tac (prems@type_rls) i ORELSE
     3.8 +  assume_tac ctxt i ORELSE
     3.9 +  resolve_tac ctxt (prems @ type_rls) i ORELSE
    3.10    rcall_tac ctxt i ORELSE
    3.11 -  ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
    3.12 -  match_tac ctxt [@{thm SubtypeI}] i
    3.13 +  ematch_tac ctxt @{thms SubtypeE} i ORELSE
    3.14 +  match_tac ctxt @{thms SubtypeI} i
    3.15  
    3.16  fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
    3.17      if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
     4.1 --- a/src/Cube/Example.thy	Tue Feb 10 14:48:26 2015 +0100
     4.2 +++ b/src/Cube/Example.thy	Tue Feb 10 16:46:21 2015 +0100
     4.3 @@ -10,17 +10,17 @@
     4.4    J. Functional Programming.\<close>
     4.5  
     4.6  method_setup depth_solve =
     4.7 -  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
     4.8 -    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
     4.9 +  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
    4.10 +    (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
    4.11  
    4.12  method_setup depth_solve1 =
    4.13 -  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    4.14 -    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
    4.15 +  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
    4.16 +    (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
    4.17  
    4.18  method_setup strip_asms =
    4.19    \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
    4.20      REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN
    4.21 -    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))\<close>
    4.22 +    DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>
    4.23  
    4.24  
    4.25  subsection \<open>Simple types\<close>
     5.1 --- a/src/HOL/HOL.thy	Tue Feb 10 14:48:26 2015 +0100
     5.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 16:46:21 2015 +0100
     5.3 @@ -904,7 +904,8 @@
     5.4    shows R
     5.5  apply (rule ex1E [OF major])
     5.6  apply (rule prem)
     5.7 -apply (tactic {* ares_tac @{thms allI} 1 *})+
     5.8 +apply assumption
     5.9 +apply (rule allI)+
    5.10  apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
    5.11  apply iprover
    5.12  done
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Feb 10 14:48:26 2015 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Feb 10 16:46:21 2015 +0100
     6.3 @@ -1061,7 +1061,8 @@
     6.4           EVERY (map (fn (prem, r) => (EVERY
     6.5             [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
     6.6              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
     6.7 -            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
     6.8 +            DEPTH_SOLVE_1
     6.9 +              (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    6.10                  (prems ~~ constr_defs))]);
    6.11  
    6.12      val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
     7.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Feb 10 14:48:26 2015 +0100
     7.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Feb 10 16:46:21 2015 +0100
     7.3 @@ -538,7 +538,7 @@
     7.4  method_setup valid_certificate_tac = {*
     7.5    Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
     7.6      (fn i =>
     7.7 -      EVERY [ftac @{thm Gets_certificate_valid} i,
     7.8 +      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
     7.9               assume_tac ctxt i,
    7.10               etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
    7.11  *}
     8.1 --- a/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 14:48:26 2015 +0100
     8.2 +++ b/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 16:46:21 2015 +0100
     8.3 @@ -482,7 +482,7 @@
     8.4  method_setup valid_certificate_tac = {*
     8.5    Args.goal_spec >> (fn quant =>
     8.6      fn ctxt => SIMPLE_METHOD'' quant (fn i =>
     8.7 -      EVERY [ftac @{thm Gets_certificate_valid} i,
     8.8 +      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
     8.9               assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
    8.10  *}
    8.11  
     9.1 --- a/src/HOL/Set.thy	Tue Feb 10 14:48:26 2015 +0100
     9.2 +++ b/src/HOL/Set.thy	Tue Feb 10 16:46:21 2015 +0100
     9.3 @@ -75,7 +75,7 @@
     9.4        resolve_tac ctxt @{thms iffI} 1 THEN
     9.5        ALLGOALS
     9.6          (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
     9.7 -          DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
     9.8 +          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
     9.9  *}
    9.10  
    9.11  lemmas CollectE = CollectD [elim_format]
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 10 14:48:26 2015 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 10 16:46:21 2015 +0100
    10.3 @@ -94,7 +94,7 @@
    10.4     REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
    10.5  
    10.6  fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
    10.7 -  (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
    10.8 +  (EVERY' [rtac notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
    10.9    REPEAT_DETERM o FIRST'
   10.10      [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac ctxt wits],
   10.11      EVERY' [rtac subsetI, rtac FalseE, eresolve_tac ctxt wits],
    11.1 --- a/src/HOL/Tools/inductive.ML	Tue Feb 10 14:48:26 2015 +0100
    11.2 +++ b/src/HOL/Tools/inductive.ML	Tue Feb 10 16:46:21 2015 +0100
    11.3 @@ -452,7 +452,8 @@
    11.4               REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)),
    11.5               REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)),
    11.6               EVERY (map (fn prem =>
    11.7 -               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
    11.8 +               DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE
    11.9 +                resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
   11.10                  (tl prems))])
   11.11            |> singleton (Proof_Context.export ctxt'' ctxt'''),
   11.12           map #2 c_intrs, length Ts)
   11.13 @@ -746,9 +747,11 @@
   11.14           REPEAT (FIRSTGOAL
   11.15             (resolve_tac ctxt3 [conjI, impI] ORELSE'
   11.16             (eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))),
   11.17 -         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
   11.18 -             (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
   11.19 -           conjI, refl] 1)) prems)]);
   11.20 +         EVERY (map (fn prem =>
   11.21 +            DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE
   11.22 +              resolve_tac ctxt3
   11.23 +                [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
   11.24 +                  conjI, refl] 1)) prems)]);
   11.25  
   11.26      val lemma = Goal.prove_sorry ctxt'' [] []
   11.27        (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
    12.1 --- a/src/HOL/Tools/simpdata.ML	Tue Feb 10 14:48:26 2015 +0100
    12.2 +++ b/src/HOL/Tools/simpdata.ML	Tue Feb 10 16:46:21 2015 +0100
    12.3 @@ -73,8 +73,10 @@
    12.4            (mk_simp_implies @{prop "(x::'a) = y"})
    12.5            (fn {context = ctxt, prems} => EVERY
    12.6             [rewrite_goals_tac ctxt @{thms simp_implies_def},
    12.7 -            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
    12.8 -              map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
    12.9 +            REPEAT (assume_tac ctxt 1 ORELSE
   12.10 +              resolve_tac ctxt
   12.11 +                (@{thm meta_eq_to_obj_eq} ::
   12.12 +                  map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
   12.13        end
   12.14    end;
   12.15