# 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.*