src/HOL/Tools/Meson/meson.ML
changeset 50695 cace30ea5a2c
parent 47956 2a420750248b
child 50702 70c2a6d513fd
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 09:56:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 13:11:04 2013 +0100
     1.3 @@ -167,21 +167,36 @@
     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 +   If the goal has the form "?P c", the danger is that unifying "?P" with a
     1.9 +   formula of the form "... c ... c ... c ..." will lead to a huge unification
    1.10 +   problem, due to the (spurious) choices between projection and imitation. The
    1.11 +   workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
    1.12 +fun quant_rtac th i st =
    1.13 +  case (concl_of st, prop_of th) of
    1.14 +    (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    1.15 +    let
    1.16 +      val cc = cterm_of (theory_of_thm th) c
    1.17 +      val ct = Thm.dest_arg (cprop_of th)
    1.18 +    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.19 +  | _ => rtac th i st
    1.20 +
    1.21  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    1.22    e.g. from conj_forward, should have the form
    1.23      "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
    1.24    and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    1.25  fun forward_res ctxt nf st =
    1.26 -  let fun forward_tacf [prem] = rtac (nf prem) 1
    1.27 -        | forward_tacf prems =
    1.28 -            error (cat_lines
    1.29 -              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    1.30 -                Display.string_of_thm ctxt st ::
    1.31 -                "Premises:" :: map (Display.string_of_thm ctxt) prems))
    1.32 +  let
    1.33 +    fun tacf [prem] = quant_rtac (nf prem) 1
    1.34 +      | tacf prems =
    1.35 +        error (cat_lines
    1.36 +          ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    1.37 +            Display.string_of_thm ctxt st ::
    1.38 +            "Premises:" :: map (Display.string_of_thm ctxt) prems))
    1.39    in
    1.40 -    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
    1.41 -    of SOME(th,_) => th
    1.42 -     | NONE => raise THM("forward_res", 0, [st])
    1.43 +    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of
    1.44 +      SOME (th, _) => th
    1.45 +    | NONE => raise THM ("forward_res", 0, [st])
    1.46    end;
    1.47  
    1.48  (*Are any of the logical connectives in "bs" present in the term?*)
    1.49 @@ -635,7 +650,6 @@
    1.50  
    1.51  val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
    1.52  
    1.53 -(* "RS" can fail if "unify_search_bound" is too small. *)
    1.54  fun try_skolemize_etc ctxt th =
    1.55    let
    1.56      val thy = Proof_Context.theory_of ctxt