src/HOL/Tools/Meson/meson.ML
changeset 58839 ccda99401bc8
parent 56245 84fc7dfa3cd4
child 58957 c9e744ea8a38
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 16:55:29 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 22:45:19 2014 +0100
     1.3 @@ -167,19 +167,19 @@
     1.4            (rename_bound_vars_RS th rl handle THM _ => tryall rls)
     1.5    in  tryall rls  end;
     1.6  
     1.7 -(* Special version of "rtac" that works around an explosion in the unifier.
     1.8 +(* Special version of "resolve_tac" that works around an explosion in the unifier.
     1.9     If the goal has the form "?P c", the danger is that resolving it against a
    1.10     property of the form "... c ... c ... c ..." will lead to a huge unification
    1.11     problem, due to the (spurious) choices between projection and imitation. The
    1.12     workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
    1.13 -fun quant_rtac th i st =
    1.14 +fun quant_resolve_tac th i st =
    1.15    case (concl_of st, prop_of th) of
    1.16      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    1.17      let
    1.18        val cc = cterm_of (theory_of_thm th) c
    1.19        val ct = Thm.dest_arg (cprop_of th)
    1.20 -    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.21 -  | _ => rtac th i st
    1.22 +    in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.23 +  | _ => resolve_tac [th] i st
    1.24  
    1.25  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    1.26    e.g. from conj_forward, should have the form
    1.27 @@ -187,7 +187,7 @@
    1.28    and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    1.29  fun forward_res ctxt nf st =
    1.30    let
    1.31 -    fun tacf [prem] = quant_rtac (nf prem) 1
    1.32 +    fun tacf [prem] = quant_resolve_tac (nf prem) 1
    1.33        | tacf prems =
    1.34          error (cat_lines
    1.35            ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    1.36 @@ -288,7 +288,7 @@
    1.37  fun forward_res2 nf hyps st =
    1.38    case Seq.pull
    1.39          (REPEAT
    1.40 -         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    1.41 +         (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
    1.42           st)
    1.43    of SOME(th,_) => th
    1.44     | NONE => raise THM("forward_res2", 0, [st]);
    1.45 @@ -700,14 +700,14 @@
    1.46  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    1.47  
    1.48  fun skolemize_prems_tac ctxt prems =
    1.49 -  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
    1.50 +  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
    1.51  
    1.52  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    1.53    Function mkcl converts theorems to clauses.*)
    1.54  fun MESON preskolem_tac mkcl cltac ctxt i st =
    1.55    SELECT_GOAL
    1.56      (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
    1.57 -            rtac @{thm ccontr} 1,
    1.58 +            resolve_tac @{thms ccontr} 1,
    1.59              preskolem_tac,
    1.60              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
    1.61                        EVERY1 [skolemize_prems_tac ctxt negs,