Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: wolff <bwolff@inf.ethz.ch>
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)
to
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,
bu
Last updated: May 03 2024 at 01:09 UTC