Theory DAList

(*  Title:      HOL/Library/DAList.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹Abstract type of association lists with unique keys›

theory DAList
imports AList
begin

text ‹This was based on some existing fragments in the AFP-Collection framework.›

subsection ‹Preliminaries›

lemma distinct_map_fst_filter:
  "distinct (map fst xs) ⟹ distinct (map fst (List.filter P xs))"
  by (induct xs) auto


subsection ‹Type ‹('key, 'value) alist››

typedef ('key, 'value) alist = "{xs :: ('key × 'value) list. (distinct ∘ map fst) xs}"
  morphisms impl_of Alist
proof
  show "[] ∈ {xs. (distinct ∘ map fst) xs}"
    by simp
qed

setup_lifting type_definition_alist

lemma alist_ext: "impl_of xs = impl_of ys ⟹ xs = ys"
  by (simp add: impl_of_inject)

lemma alist_eq_iff: "xs = ys ⟷ impl_of xs = impl_of ys"
  by (simp add: impl_of_inject)

lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
  using impl_of[of xs] by simp

lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
  by (rule impl_of_inverse)


subsection ‹Primitive operations›

lift_definition lookup :: "('key, 'value) alist ⇒ 'key ⇒ 'value option" is map_of  .

lift_definition empty :: "('key, 'value) alist" is "[]"
  by simp

lift_definition update :: "'key ⇒ 'value ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
  is AList.update
  by (simp add: distinct_update)

(* FIXME: we use an unoptimised delete operation. *)
lift_definition delete :: "'key ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
  is AList.delete
  by (simp add: distinct_delete)

lift_definition map_entry ::
    "'key ⇒ ('value ⇒ 'value) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
  is AList.map_entry
  by (simp add: distinct_map_entry)

lift_definition filter :: "('key × 'value ⇒ bool) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
  is List.filter
  by (simp add: distinct_map_fst_filter)

lift_definition map_default ::
    "'key ⇒ 'value ⇒ ('value ⇒ 'value) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
  is AList.map_default
  by (simp add: distinct_map_default)


subsection ‹Abstract operation properties›

(* FIXME: to be completed *)

lemma lookup_empty [simp]: "lookup empty k = None"
by (simp add: empty_def lookup_def Alist_inverse)

lemma lookup_update:
  "lookup (update k1 v xs) k2 = (if k1 = k2 then Some v else lookup xs k2)"
by(transfer)(simp add: update_conv')

lemma lookup_update_eq [simp]:
  "k1 = k2 ⟹ lookup (update k1 v xs) k2 = Some v"
by(simp add: lookup_update)

lemma lookup_update_neq [simp]:
  "k1 ≠ k2 ⟹ lookup (update k1 v xs) k2 = lookup xs k2"
by(simp add: lookup_update)

lemma update_update_eq [simp]:
  "k1 = k2 ⟹ update k2 v2 (update k1 v1 xs) = update k2 v2 xs"
by(transfer)(simp add: update_conv')

lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
  by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')


subsection ‹Further operations›

subsubsection ‹Equality›

instantiation alist :: (equal, equal) equal
begin

definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"

instance
  by standard (simp add: equal_alist_def impl_of_inject)

end


subsubsection ‹Size›

instantiation alist :: (type, type) size
begin

definition "size (al :: ('a, 'b) alist) = length (impl_of al)"

instance ..

end


subsection ‹Quickcheck generators›

context
  includes state_combinator_syntax term_syntax
begin

definition
  valterm_empty :: "('key :: typerep, 'value :: typerep) alist × (unit ⇒ Code_Evaluation.term)"
  where "valterm_empty = Code_Evaluation.valtermify empty"

definition
  valterm_update :: "'key :: typerep × (unit ⇒ Code_Evaluation.term) ⇒
  'value :: typerep × (unit ⇒ Code_Evaluation.term) ⇒
  ('key, 'value) alist × (unit ⇒ Code_Evaluation.term) ⇒
  ('key, 'value) alist × (unit ⇒ Code_Evaluation.term)" where
  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {⋅} k {⋅} v {⋅}a"

fun random_aux_alist
where
  "random_aux_alist i j =
    (if i = 0 then Pair valterm_empty
     else Quickcheck_Random.collapse
       (Random.select_weight
         [(i, Quickcheck_Random.random j ∘→ (λk. Quickcheck_Random.random j ∘→
           (λv. random_aux_alist (i - 1) j ∘→ (λa. Pair (valterm_update k v a))))),
          (1, Pair valterm_empty)]))"

end

instantiation alist :: (random, random) random
begin

definition random_alist
where
  "random_alist i = random_aux_alist i i"

instance ..

end

instantiation alist :: (exhaustive, exhaustive) exhaustive
begin

fun exhaustive_alist ::
  "(('a, 'b) alist ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option"
where
  "exhaustive_alist f i =
    (if i = 0 then None
     else
      case f empty of
        Some ts ⇒ Some ts
      | None ⇒
          exhaustive_alist
            (λa. Quickcheck_Exhaustive.exhaustive
              (λk. Quickcheck_Exhaustive.exhaustive (λv. f (update k v a)) (i - 1)) (i - 1))
            (i - 1))"

instance ..

end

instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
begin

fun full_exhaustive_alist ::
  "(('a, 'b) alist × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ natural ⇒
    (bool × term list) option"
where
  "full_exhaustive_alist f i =
    (if i = 0 then None
     else
      case f valterm_empty of
        Some ts ⇒ Some ts
      | None ⇒
          full_exhaustive_alist
            (λa.
              Quickcheck_Exhaustive.full_exhaustive
                (λk. Quickcheck_Exhaustive.full_exhaustive (λv. f (valterm_update k v a)) (i - 1))
              (i - 1))
            (i - 1))"

instance ..

end


section ‹alist is a BNF›

lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k × 'v) list"] for map: map rel: rel
  by auto

hide_const valterm_empty valterm_update random_aux_alist

hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel

end