# HG changeset patch
# User blanchet
# Date 1357215064 -3600
# Node ID cace30ea5a2c826b89fe6de38573583029964370
# Parent  df8ae0590be22062e662b6e5f7b34b4dd9a230b2
avoid explosion in higher-order unification algorithm

diff -r df8ae0590be2 -r cace30ea5a2c src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 09:56:39 2013 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 13:11:04 2013 +0100
@@ -167,21 +167,36 @@
           (rename_bound_vars_RS th rl handle THM _ => tryall rls)
   in  tryall rls  end;
 
+(* Special version of "rtac" that works around an explosion in the unifier.
+   If the goal has the form "?P c", the danger is that unifying "?P" with a
+   formula of the form "... c ... c ... c ..." will lead to a huge unification
+   problem, due to the (spurious) choices between projection and imitation. The
+   workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
+fun quant_rtac th i st =
+  case (concl_of st, prop_of th) of
+    (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
+    let
+      val cc = cterm_of (theory_of_thm th) c
+      val ct = Thm.dest_arg (cprop_of th)
+    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+  | _ => rtac th i st
+
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   e.g. from conj_forward, should have the form
     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res ctxt nf st =
-  let fun forward_tacf [prem] = rtac (nf prem) 1
-        | forward_tacf prems =
-            error (cat_lines
-              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
-                Display.string_of_thm ctxt st ::
-                "Premises:" :: map (Display.string_of_thm ctxt) prems))
+  let
+    fun tacf [prem] = quant_rtac (nf prem) 1
+      | tacf prems =
+        error (cat_lines
+          ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
+            Display.string_of_thm ctxt st ::
+            "Premises:" :: map (Display.string_of_thm ctxt) prems))
   in
-    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
-    of SOME(th,_) => th
-     | NONE => raise THM("forward_res", 0, [st])
+    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of
+      SOME (th, _) => th
+    | NONE => raise THM ("forward_res", 0, [st])
   end;
 
 (*Are any of the logical connectives in "bs" present in the term?*)
@@ -635,7 +650,6 @@
 
 val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
 
-(* "RS" can fail if "unify_search_bound" is too small. *)
 fun try_skolemize_etc ctxt th =
   let
     val thy = Proof_Context.theory_of ctxt