Re: [isabelle] How to unify the premises with my rule?



Thanks for your question. The problem here is that you aren't using Isabelle in the way it's designed to be used, specifically with regard to unification. Your problem would be trivial for first-order automatic provers. It is perhaps easy enough for Isabelle to prove with its "meson" method, but not using its basic tools.

To simplify your example considerably, if you have a formula like

    ALL x. P x & (EX y. Q(x,y)) --> R x

then its natural Isabelle form is

    [| P(x); Q(x,y) |] ==> R(x)

and this can trivially be used to reduce subgoals of the form R(...). That is, you need to express your big quantified formula as shown above and give it to the "rule" method.

Larry Paulson


On 17 Mar 2006, at 03:20, chen kun wrote:

You can see the last one of the premises is a derivation rule, and the others could satisfy the assumption of the rule. So it is supposed to prove the conclusion ,but I failed to unify the premises with the rule in the premises. Could anyone give me some help on this ? IF POSSIBLE , could you show the proof step by step?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.