src/HOL/Tools/Meson/meson.ML
changeset 59498 50b60f501b05
parent 59171 75ec7271b426
child 59580 cbc38731d42f
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -170,14 +170,14 @@
     1.4     property of the form "... c ... c ... c ..." will lead to a huge unification
     1.5     problem, due to the (spurious) choices between projection and imitation. The
     1.6     workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
     1.7 -fun quant_resolve_tac th i st =
     1.8 +fun quant_resolve_tac ctxt th i st =
     1.9    case (concl_of st, prop_of th) of
    1.10      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    1.11      let
    1.12        val cc = cterm_of (theory_of_thm th) c
    1.13        val ct = Thm.dest_arg (cprop_of th)
    1.14 -    in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.15 -  | _ => resolve_tac [th] i st
    1.16 +    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.17 +  | _ => resolve_tac ctxt [th] i st
    1.18  
    1.19  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    1.20    e.g. from conj_forward, should have the form
    1.21 @@ -185,7 +185,7 @@
    1.22    and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    1.23  fun forward_res ctxt nf st =
    1.24    let
    1.25 -    fun tacf [prem] = quant_resolve_tac (nf prem) 1
    1.26 +    fun tacf [prem] = quant_resolve_tac ctxt (nf prem) 1
    1.27        | tacf prems =
    1.28          error (cat_lines
    1.29            ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    1.30 @@ -287,7 +287,7 @@
    1.31    case Seq.pull
    1.32          (REPEAT
    1.33           (Misc_Legacy.METAHYPS ctxt
    1.34 -           (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
    1.35 +           (fn major::minors => resolve_tac ctxt [nf (minors @ hyps) major] 1) 1)
    1.36           st)
    1.37    of SOME(th,_) => th
    1.38     | NONE => raise THM("forward_res2", 0, [st]);
    1.39 @@ -390,7 +390,7 @@
    1.40                  cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean
    1.41                  variable created by resolution with disj_forward. Since (cnf_nil prem)
    1.42                  returns a LIST of theorems, we can backtrack to get all combinations.*)
    1.43 -              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1
    1.44 +              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac ctxt (cnf_nil prem) 1) 1
    1.45                in  Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths  end
    1.46            | _ => nodups ctxt th :: ths  (*no work to do*)
    1.47        and cnf_nil th = cnf_aux (th, [])
    1.48 @@ -500,7 +500,7 @@
    1.49  
    1.50  (* resolve_from_net_tac actually made it slower... *)
    1.51  fun prolog_step_tac ctxt horns i =
    1.52 -    (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
    1.53 +    (assume_tac ctxt i APPEND resolve_tac ctxt horns i) THEN check_tac THEN
    1.54      TRYALL_eq_assume_tac;
    1.55  
    1.56  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
    1.57 @@ -698,14 +698,14 @@
    1.58  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    1.59  
    1.60  fun skolemize_prems_tac ctxt prems =
    1.61 -  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
    1.62 +  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac ctxt [exE]
    1.63  
    1.64  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    1.65    Function mkcl converts theorems to clauses.*)
    1.66  fun MESON preskolem_tac mkcl cltac ctxt i st =
    1.67    SELECT_GOAL
    1.68      (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
    1.69 -            resolve_tac @{thms ccontr} 1,
    1.70 +            resolve_tac ctxt @{thms ccontr} 1,
    1.71              preskolem_tac,
    1.72              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
    1.73                        EVERY1 [skolemize_prems_tac ctxt negs,
    1.74 @@ -719,7 +719,7 @@
    1.75  fun best_meson_tac sizef ctxt =
    1.76    MESON all_tac (make_clauses ctxt)
    1.77      (fn cls =>
    1.78 -         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
    1.79 +         THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1)
    1.80                           (has_fewer_prems 1, sizef)
    1.81                           (prolog_step_tac ctxt (make_horns cls) 1))
    1.82      ctxt
    1.83 @@ -732,7 +732,7 @@
    1.84  
    1.85  fun depth_meson_tac ctxt =
    1.86    MESON all_tac (make_clauses ctxt)
    1.87 -    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
    1.88 +    (fn cls => EVERY [resolve_tac ctxt (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
    1.89      ctxt
    1.90  
    1.91  (** Iterative deepening version **)
    1.92 @@ -764,7 +764,7 @@
    1.93                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.94          in
    1.95            THEN_ITER_DEEPEN iter_deepen_limit
    1.96 -            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
    1.97 +            (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
    1.98          end));
    1.99  
   1.100  fun meson_tac ctxt ths =