Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] map_ran's type in HOL-Library.AList is too...


view this post on Zulip Email Gateway (May 11 2021 at 07:11):

From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Isabelle developers,

I noticed that the map_ran function from HOL-Library is defined with the
following type annotation.

definition map_ran :: "('key ⇒ 'val ⇒ 'val) ⇒ ('key × 'val) list ⇒ ('key
× 'val) list"
where "map_ran f = map (λ(k, v). (k, f k v))"

This means that it is not possible to use map_ran to map an association
list from one range type to another. This would be possible if it had
the following type annotation (or no type annotation at all).

('key ⇒ 'val1 ⇒ 'val2) ⇒ ('key × 'val1) list ⇒ ('key × 'val2) list

I cannot think of any case where it would pose a problem for map_ran to
have this general type so I tried to changed it. I noticed no resulting
problem in the HOL distribution. I also checked in the AFP and found
that only the following sessions use this constant: Call_Arity,
Launchbury, LTL_to_DRA, and Collections. I also noticed no problem in
these sessions with the general type.

Is there an historical reason why map_ran has this restrictive type
annotation?

Is there any objection to me pushing this change?

While I am at it, I also have the following two small lemmas that I
found useful and would like to add to HOL-Library.AList. Note that
map_ran_Cons is only a generalization of map_ran_simps(2) that avoids
the need for a case analysis of the product x. Is there any objection?

lemma map_fst_map_ran[simp]: "map fst (map_ran f xs) = map fst xs"
by (simp add: map_ran_def case_prod_beta)

lemma map_ran_Cons: "map_ran f (x # xs) = (fst x, f (fst x) (snd x)) #
map_ran f xs"
by (simp add: map_ran_def case_prod_beta)

Regards,
Martin Desharnais
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature

view this post on Zulip Email Gateway (May 12 2021 at 06:35):

From: Tobias Nipkow <nipkow@in.tum.de>
Hi Martin,

On 11/05/2021 09:11, Martin Desharnais wrote:

Dear Isabelle developers,

I noticed that the map_ran function from HOL-Library is defined with the
following type annotation.

definition map_ran :: "('key ⇒ 'val ⇒ 'val) ⇒ ('key × 'val) list ⇒ ('key × 'val)
list"
  where "map_ran f = map (λ(k, v). (k, f k v))"

Somebody wasn't thinking when they fixed that type. I have generalized it as you
suggested and everything still works, as expected.

This means that it is not possible to use map_ran to map an association list
from one range type to another. This would be possible if it had the following
type annotation (or no type annotation at all).

('key ⇒ 'val1 ⇒ 'val2) ⇒ ('key × 'val1) list ⇒ ('key × 'val2) list

While I am at it, I also have the following two small lemmas that I found useful
and would like to add to HOL-Library.AList. Note that map_ran_Cons is only a
generalization of map_ran_simps(2) that avoids the need for a case analysis of
the product x. Is there any objection?

lemma map_fst_map_ran[simp]: "map fst (map_ran f xs) = map fst xs"
  by (simp add: map_ran_def case_prod_beta)

lemma map_ran_Cons: "map_ran f (x # xs) = (fst x, f (fst x) (snd x)) # map_ran f
xs"
  by (simp add: map_ran_def case_prod_beta)

No objections.

Tobias

Regards,
Martin Desharnais


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

smime.p7s


Last updated: Mar 04 2024 at 10:08 UTC