Re: [Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

[Mario Xerxes Castelán Castro]

I wrote a “ssfrag” to simplify conjunctions and disjunctions in the
aforementioned way plus normalization to right associativity, based on
AC_Sort. It is in my repository of HOL4 developments
, file “marioxcc_lib.sml”.



signature.asc
Description: OpenPGP digital signature
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

[Mario Xerxes Castelán Castro]

Thanks.

On 21/02/18 11:57, Thomas Tuerk wrote:
> Hi,
> 
> the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
> description manual). AC normalisation would sort multiple occurrences of
> the same operant next to each other. Therefore these multiple
> occurrences can then be removed by providing 2 idempotency rewrite rules:
> 
> f x x = x
> 
> f x (f x y) = f x y
> 
> This provides a very high level simple way to do what you want, I believe.
> 
> If you want something lower level, more efficient with finer control,
> you could use "sort" from structure "AC_Sort". It provides a conversion
> that does what you want if instantiated properly. However, I never used
> it myself, so I don't have first hand experience with it.
> 
> There is also the structure "AC" from refute. However, I believe in
> contrast to "AC_Sort", there is no direct support for idempotency in "AC".
> 
> Cheers
> 
> Thomas



signature.asc
Description: OpenPGP digital signature
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

[Thomas Tuerk]

Hi,

the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
description manual). AC normalisation would sort multiple occurrences of
the same operant next to each other. Therefore these multiple
occurrences can then be removed by providing 2 idempotency rewrite rules:

f x x = x

f x (f x y) = f x y

This provides a very high level simple way to do what you want, I believe.

If you want something lower level, more efficient with finer control,
you could use "sort" from structure "AC_Sort". It provides a conversion
that does what you want if instantiated properly. However, I never used
it myself, so I don't have first hand experience with it.

There is also the structure "AC" from refute. However, I believe in
contrast to "AC_Sort", there is no direct support for idempotency in "AC".

Cheers

Thomas


On 21.02.2018 18:34, Mario Xerxes Castelán Castro wrote:
> Hello.
>
> Is there an existing tactic for removing multiple appearances of an
> operand under an operator «f» that has the property «f x x = x» and is
> associative-commutative? For example, conjunction and disjunction.
>
> If not, I can write one for HOL4, but I do not want to duplicate
> existing work.
>
> Thanks.
>
>
>
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Simplifying expressions like «P ∧ P ∧ Q»

[Mario Xerxes Castelán Castro]

Hello.

Is there an existing tactic for removing multiple appearances of an
operand under an operator «f» that has the property «f x x = x» and is
associative-commutative? For example, conjunction and disjunction.

If not, I can write one for HOL4, but I do not want to duplicate
existing work.

Thanks.



signature.asc
Description: OpenPGP digital signature
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info