eliminated aliases;
authorwenzelm
Thu Oct 30 16:20:46 2014 +0100 (2014-10-30)
changeset 58837e84d900cd287
parent 58836 4037bb00d08e
child 58838 59203adfc33f
eliminated aliases;
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Tools/find_theorems.ML
src/Pure/goal.ML
src/Pure/skip_proof.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 30 16:17:56 2014 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 30 16:20:46 2014 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4          (fst o rules thy) sub];
     1.5      val classrel =
     1.6        Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
     1.7 -        (K (EVERY (map (TRYALL o rtac) intros)));
     1.8 +        (K (EVERY (map (TRYALL o resolve_tac o single) intros)));
     1.9      val diff_sort = Sign.complete_sort thy [sup]
    1.10        |> subtract (op =) (Sign.complete_sort thy [sub])
    1.11        |> filter (is_class thy);
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:17:56 2014 +0100
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:20:46 2014 +0100
     2.3 @@ -56,7 +56,7 @@
     2.4          val loc_intro_tac =
     2.5            (case Locale.intros_of thy class of
     2.6              (_, NONE) => all_tac
     2.7 -          | (_, SOME intro) => ALLGOALS (rtac intro));
     2.8 +          | (_, SOME intro) => ALLGOALS (resolve_tac [intro]));
     2.9          val tac = loc_intro_tac
    2.10            THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
    2.11        in Element.prove_witness empty_ctxt prop tac end) some_prop;
     3.1 --- a/src/Pure/Isar/element.ML	Thu Oct 30 16:17:56 2014 +0100
     3.2 +++ b/src/Pure/Isar/element.ML	Thu Oct 30 16:20:46 2014 +0100
     3.3 @@ -258,14 +258,15 @@
     3.4  fun prove_witness ctxt t tac =
     3.5    Witness (t,
     3.6      Thm.close_derivation
     3.7 -      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
     3.8 +      (Goal.prove ctxt [] [] (mark_witness t)
     3.9 +        (fn _ => resolve_tac [Drule.protectI] 1 THEN tac)));
    3.10  
    3.11  
    3.12  local
    3.13  
    3.14  val refine_witness =
    3.15    Proof.refine (Method.Basic (K (NO_CASES o
    3.16 -    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
    3.17 +    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac [Drule.protectI])))))))));
    3.18  
    3.19  fun gen_witness_proof proof after_qed wit_propss eq_props =
    3.20    let
     4.1 --- a/src/Pure/Isar/method.ML	Thu Oct 30 16:17:56 2014 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Thu Oct 30 16:20:46 2014 +0100
     4.3 @@ -100,7 +100,7 @@
     4.4  local
     4.5  
     4.6  fun cut_rule_tac rule =
     4.7 -  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
     4.8 +  resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
     4.9  
    4.10  in
    4.11  
    4.12 @@ -147,7 +147,7 @@
    4.13  
    4.14  (* this -- resolve facts directly *)
    4.15  
    4.16 -val this = METHOD (EVERY o map (HEADGOAL o rtac));
    4.17 +val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single));
    4.18  
    4.19  
    4.20  (* fact -- composition by facts from context *)
    4.21 @@ -162,7 +162,7 @@
    4.22  
    4.23  fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
    4.24    if cond (Logic.strip_assums_concl prop)
    4.25 -  then rtac rule i else no_tac);
    4.26 +  then resolve_tac [rule] i else no_tac);
    4.27  
    4.28  in
    4.29  
     5.1 --- a/src/Pure/Isar/proof.ML	Thu Oct 30 16:17:56 2014 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Thu Oct 30 16:20:46 2014 +0100
     5.3 @@ -442,12 +442,12 @@
     5.4        Goal.norm_hhf_tac ctxt THEN'
     5.5        SUBGOAL (fn (goal, i) =>
     5.6          if can Logic.unprotect (Logic.strip_assums_concl goal) then
     5.7 -          etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
     5.8 +          eresolve_tac [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
     5.9          else finish_tac ctxt (n - 1) (i + 1));
    5.10  
    5.11  fun goal_tac ctxt rule =
    5.12    Goal.norm_hhf_tac ctxt THEN'
    5.13 -  rtac rule THEN'
    5.14 +  resolve_tac [rule] THEN'
    5.15    finish_tac ctxt (Thm.nprems_of rule);
    5.16  
    5.17  fun FINDGOAL tac st =
    5.18 @@ -886,7 +886,7 @@
    5.19  fun refine_terms n =
    5.20    refine (Method.Basic (K (NO_CASES o
    5.21      K (HEADGOAL (PRECISE_CONJUNCTS n
    5.22 -      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
    5.23 +      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac [Drule.termI])))))))))
    5.24    #> Seq.hd;
    5.25  
    5.26  in
     6.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Oct 30 16:17:56 2014 +0100
     6.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 30 16:20:46 2014 +0100
     6.3 @@ -206,9 +206,10 @@
     6.4      val goal' = Thm.transfer thy' goal;
     6.5  
     6.6      fun limited_etac thm i =
     6.7 -      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o etac thm i;
     6.8 +      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
     6.9 +        eresolve_tac [thm] i;
    6.10      fun try_thm thm =
    6.11 -      if Thm.no_prems thm then rtac thm 1 goal'
    6.12 +      if Thm.no_prems thm then resolve_tac [thm] 1 goal'
    6.13        else
    6.14          (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
    6.15            1 goal';
     7.1 --- a/src/Pure/goal.ML	Thu Oct 30 16:17:56 2014 +0100
     7.2 +++ b/src/Pure/goal.ML	Thu Oct 30 16:20:46 2014 +0100
     7.3 @@ -293,7 +293,7 @@
     7.4  
     7.5  val adhoc_conjunction_tac = REPEAT_ALL_NEW
     7.6    (SUBGOAL (fn (goal, i) =>
     7.7 -    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
     7.8 +    if can Logic.dest_conjunction goal then resolve_tac [Conjunction.conjunctionI] i
     7.9      else no_tac));
    7.10  
    7.11  val conjunction_tac = SUBGOAL (fn (goal, i) =>
    7.12 @@ -317,7 +317,7 @@
    7.13  (* hhf normal form *)
    7.14  
    7.15  fun norm_hhf_tac ctxt =
    7.16 -  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    7.17 +  resolve_tac [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    7.18    THEN' SUBGOAL (fn (t, i) =>
    7.19      if Drule.is_norm_hhf t then all_tac
    7.20      else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
    7.21 @@ -335,7 +335,7 @@
    7.22      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    7.23      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    7.24      val tacs = Rs |> map (fn R =>
    7.25 -      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    7.26 +      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
    7.27    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
    7.28  
    7.29  end;
     8.1 --- a/src/Pure/skip_proof.ML	Thu Oct 30 16:17:56 2014 +0100
     8.2 +++ b/src/Pure/skip_proof.ML	Thu Oct 30 16:20:46 2014 +0100
     8.3 @@ -38,6 +38,6 @@
     8.4  (* cheat_tac *)
     8.5  
     8.6  fun cheat_tac i st =
     8.7 -  rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
     8.8 +  resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
     8.9  
    8.10  end;
     9.1 --- a/src/Pure/tactic.ML	Thu Oct 30 16:17:56 2014 +0100
     9.2 +++ b/src/Pure/tactic.ML	Thu Oct 30 16:20:46 2014 +0100
     9.3 @@ -181,7 +181,7 @@
     9.4  
     9.5  (*The conclusion of the rule gets assumed in subgoal i,
     9.6    while subgoal i+1,... are the premises of the rule.*)
     9.7 -fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
     9.8 +fun cut_tac rule i = resolve_tac [cut_rl] i THEN resolve_tac [rule] (i + 1);
     9.9  
    9.10  (*"Cut" a list of rules into the goal.  Their premises will become new
    9.11    subgoals.*)
    9.12 @@ -327,7 +327,7 @@
    9.13          | Then (SOME tac) tac' = SOME(tac THEN' tac');
    9.14        fun thins H (tac,n) =
    9.15          if p H then (tac,n+1)
    9.16 -        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
    9.17 +        else (Then tac (rotate_tac n THEN' eresolve_tac [thin_rl]),0);
    9.18    in SUBGOAL(fn (subg,n) =>
    9.19         let val Hs = Logic.strip_assums_hyp subg
    9.20         in case fst(fold thins Hs (NONE,0)) of
    10.1 --- a/src/Pure/thm.ML	Thu Oct 30 16:17:56 2014 +0100
    10.2 +++ b/src/Pure/thm.ML	Thu Oct 30 16:20:46 2014 +0100
    10.3 @@ -1390,7 +1390,7 @@
    10.4  
    10.5  (*Rotates a rule's premises to the left by k, leaving the first j premises
    10.6    unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
    10.7 -  number of premises.  Useful with etac and underlies defer_tac*)
    10.8 +  number of premises.  Useful with eresolve_tac and underlies defer_tac*)
    10.9  fun permute_prems j k rl =
   10.10    let
   10.11      val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl;