Thanks to both of you. That SIMP_CONV indeed works: (it also explains why just using bool_ss doesn't work)
> SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] ``(q \/ p /\ x) /\ p /\ ~q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ ~q: thm
But now I realized that, what I'm looking for is actually a conversion to DNF
forms with possible simplifications. The normalForms.DNF_CONV (in src/metis, by
Joe Hurd) did this work perfectly: (by using the CONTRACT_CONV in the same lib)
> normalForms.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ p /\ ~q: thm
while refuteLib.DNF_CONV doesn't do any simplification:
> refuteLib.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> q /\ p /\ ~q \/ p /\ x /\ p /\ ~q: thm
P. S. "src/metis/normalForms.sml" is currently broken due to the "tight
equality" changes. To reproduce my above demos, you need to (temporarily) put a
val _ = ParseExtras.temp_loose_equality()
at the beginning of that file. I'm preparing a PR to fix this issue.
Regards,
Chun Tian
Il 01/10/19 10:42, Thomas Sewell ha scritto:
> 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
>> 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
>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
