[isabelle] Simplifier problem

Dear all,

I came across with a simplifier problem which
I would like to understand.

In a proofstate with a large formula phi in the
assumptions of a goal:

    1.) phi ==> Xi

simplification with a very simple rule R of
the form "(C(D x)) == True" (yes, x is polymorphic,
any instance of a redex in phi is monomorphic)

    apply (simp add: R)

does not compute a normal form.

If I swap via

    apply(erule contrapos_pp)


    1.) ~Xi ==> ~phi

the method:

    apply (simp add: R)

does the trick.

Why? It seems to be dependent on the size of phi -
is there a way to control this behaviour by some
flag or depth parameter?

Best regards,


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