is there builtin hashmap function in Isabelle?

Question

In perl there are hashes, key-value pairs. Does Isabelle/HOL have a builtin such function with the corresponding theorems?

Answer 1

Typically in Isabelle/HOL, you would just use a function of type 'key ⇒ 'value. For instance:

definition "num_animals 
    ≡ (λ_. 0)(''dog'' := 3, ''cat'' := 42, ''mouse'' := 12)"

lemma "num_animals ''dog'' = 3"
  by (simp add: num_animals_def)

Here, (λ_. 0) is a function that returns 0 for all input values, while the syntax (''dog'' := 3) modifies the existing function so that the input dog returns 3.

If you want to be able to determine if a function does not contain a particular key, you can use Isabelle/HOL's option type:

definition "num_animals 
    ≡ (λ_. None)(''dog'' := Some 3, ''cat'' := Some 42, ''mouse'' := Some 12)"

lemma "num_animals ''elephant'' = None"
  by (simp add: num_animals_def)

There are numerous differences between this and a hash-table. For example, Isabelle will have to perform at least O(n) steps to look up a value in the function in this format. Also, no hashing is going on: key values are stored and compared explicitly. Usually, though, because you are reasoning about these things, and not typically trying to execute these things, this is not a problem.

If you are dealing with larger proof terms, you may need to look into other representations of functions, such as Binary Search Trees in the AFP, though these will be harder to work with.