David Pratten (Dec 15 2023 at 01:39): David Pratten (Dec 15 2023 at 01:39):Hi All,
I'm looking for a Dict data structure implementation in Isabelle/HOL and found Brian Ford's examples: https://bford.info/isabelle/dict/. Unfortunately, they seem to be for an earlier version of Isabelle?
Does anyone have a better solution for Dicts or tips on how to get the *.thy files to work with Isabelle2023?
The first two lines generate errors ...
theory ListDict = Dict:
types ('a,'b) listdict = "('a * 'b) list"
Thanks
David
Mathias Fleury (Dec 15 2023 at 06:03):Given that the project from Brian Ford's goes back to 2002, I would assume that the version of Isabelle is at most 2002…
Mathias Fleury (Dec 15 2023 at 06:07):But the question is probably what do you want? The abstract representation is just a function to 'a option
Manuel Eberl (Dec 15 2023 at 09:03):Yes, abstractly, the right abstraction for a map is usually a function 'a ⇒ 'b option. There's a bunch of definitions and notation for that in HOL/Map.thy. There is also Library/Finite_Map.thy, which is an explicit type of partial maps with finite support. I personally never needed it ('a ⇒ 'b option was always enough for me), but it might be useful.
For implementation purposes, the easiest thing you can do is to use map_of :: ('a × 'b) list ⇒ 'a ⇒ 'b option, which turns a list of key–value pairs into such a partial function.
For more sophisticated applications there's also HOL-Library/Mapping.thy, which provides an abstract datatype for finite maps that can use a variety of different implementations, e.g. list of key–values pairs or red–black trees.
David Pratten (Dec 15 2023 at 21:10):Thanks @Manuel Eberl and @Mathias Fleury perfect. That is exactly what I was looking for!
Last updated: Apr 28 2024 at 08:19 UTC