author | blanchet |

Thu Jan 03 13:11:04 2013 +0100 (2013-01-03) | |

changeset 50695 | cace30ea5a2c |

parent 50694 | df8ae0590be2 |

child 50696 | 85f944352d55 |

avoid explosion in higher-order unification algorithm

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