Of course, it’s possible to be surprised by the behaviour of the simplifier,
and simplification wrt conjuncts is a bit “out of the ordinary” perhaps, but in
principle it is no riskier than rewriting wrt assumptions or terms that appear
to the left of an implication. E.g., if
P /\ Q ==> R
induces looping in R because of the P and Q, then the same thing may happen in
P /\ Q /\ R.
Michael
From: Thomas Sewell <sew...@chalmers.se>
Date: Tuesday, 1 October 2019 at 18:43
To: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Simplify/normalize propositional logic terms?
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
