Try this:
SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] `` (q \/ p /\ x) /\ p /\ ~q ``;
That CONJ_ss just adds a congruence rule that uses each side of a conjunction
to simplify the other.
I found it by investigating bossLib.csimp, which you might also want to know
about.
Once upon a time in Isabelle I had a problem with such congruences, since they
might locally add rewrites which might be looping or inefficient. Is there a
similar risk in HOL4?
Cheers,
Thomas.
On 2019-09-30 23:49, Konrad Slind wrote:
A couple of places to look in HOLindex: refuteLib and normalForms structure.
On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe)
<binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote:
Hi,
it can be proven (by DECIDE_TAC) that,
|- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x
but is there any conversion function available in HOL4 such that from LHS of
above equation I can directly get the RHS - something like a canonical form?
--Chun
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
