Well, it's not that "perfect", having seen the double "p" in ``x /\ p /\ p /\ ~q`` returned by normalForms.DNF_CONV. Maybe this indicates some possible improvements in normalForms.CONTRACT_CONV. Let me try ...
--Chun On Tue, Oct 1, 2019 at 11:01 AM Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > 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 > > > > -- ---- Chun Tian (binghe) Fondazione Bruno Kessler (Italy)
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
