Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Monoid or word homomorphism?

Email Gateway (May 29 2025 at 07:23):

From: Tobias Nipkow <nipkow@in.tum.de>
This is what I defined locally:

definition hom :: ‹('a list ⇒ 'b list) ⇒ bool› where
‹hom h = ((∀a b. h (a @ b) = (h a) @ h b) ∧ h [] = [])›

Maybe it exists already? Maybe as part of the monoid class? I couldn't find
anything. Maybe it should be added to theory List (named hom_list)?

Tobias

smime.p7s

Email Gateway (May 29 2025 at 12:31):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
I have this:

https://www.isa-afp.org/sessions/combinatorics_words/#Morphisms

Note, for example, that the empty to empty is a consequence.

Stepan

On 5/29/2025 9:23 AM, Tobias Nipkow wrote:

This is what I defined locally:

definition hom :: ‹('a list ⇒ 'b list) ⇒ bool› where
‹hom h = ((∀a b. h (a @ b) = (h a) @ h b) ∧ h [] = [])›

Maybe it exists already? Maybe as part of the monoid class? I couldn't
find anything. Maybe it should be added to theory List (named hom_list)?

Tobias

Email Gateway (May 29 2025 at 14:25):

From: Tobias Nipkow <nipkow@in.tum.de>
Thank you Stepan,

The first place I looked was your AFP entry, but I made the mistake of grepping
for "hom", not "morphism" ;-)

Tobias

On 29/05/2025 14:31, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

I have this:

https://www.isa-afp.org/sessions/combinatorics_words/#Morphisms

Note, for example, that the empty to empty is a consequence.

Stepan

On 5/29/2025 9:23 AM, Tobias Nipkow wrote:

This is what I defined locally:

definition hom :: ‹('a list ⇒ 'b list) ⇒ bool› where
‹hom h = ((∀a b. h (a @ b) = (h a) @ h b) ∧ h [] = [])›

Maybe it exists already? Maybe as part of the monoid class? I couldn't find
anything. Maybe it should be added to theory List (named hom_list)?

Tobias

smime.p7s

Email Gateway (May 29 2025 at 16:03):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Not sure why, but the term "morphism" is canonical in combinatorics on
words, see
https://link.springer.com/chapter/10.1007/978-3-642-59136-5_7
for example.

Stepan

On 29-May-25 4:25 PM, Tobias Nipkow wrote:

Thank you Stepan,

The first place I looked was your AFP entry, but I made the mistake of
grepping for "hom", not "morphism" ;-)

Tobias

On 29/05/2025 14:31, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:

I have this:

https://www.isa-afp.org/sessions/combinatorics_words/#Morphisms

Note, for example, that the empty to empty is a consequence.

Stepan

On 5/29/2025 9:23 AM, Tobias Nipkow wrote:

This is what I defined locally:

definition hom :: ‹('a list ⇒ 'b list) ⇒ bool› where
‹hom h = ((∀a b. h (a @ b) = (h a) @ h b) ∧ h [] = [])›

Maybe it exists already? Maybe as part of the monoid class? I
couldn't find anything. Maybe it should be added to theory List
(named hom_list)?

Tobias

Last updated: Jun 20 2025 at 16:26 UTC