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

[Tobias Nipkow]

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 at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210512/b4165d65/attachment.bin>