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