bulwahn@46237: (*  Title:      HOL/Library/DAList.thy
bulwahn@46167:     Author:     Lukas Bulwahn, TU Muenchen *)
bulwahn@46167: 
bulwahn@46167: header {* Abstract type of association lists with unique keys *}
bulwahn@46167: 
bulwahn@46237: theory DAList
bulwahn@46238: imports AList
bulwahn@46167: begin
bulwahn@46167: 
bulwahn@46167: text {* This was based on some existing fragments in the AFP-Collection framework. *}
bulwahn@46167: 
bulwahn@47143: subsection {* Preliminaries *}
bulwahn@47143: 
bulwahn@47143: lemma distinct_map_fst_filter:
bulwahn@47143:    "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
bulwahn@47143: by (induct xs) auto
bulwahn@47143: 
bulwahn@46167: subsection {* Type @{text "('key, 'value) alist" } *}
bulwahn@46167: 
wenzelm@49834: typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
wenzelm@46507:   morphisms impl_of Alist
wenzelm@46507: proof
bulwahn@47143:   show "[] \<in> {xs. (distinct o map fst) xs}" by simp
wenzelm@46507: qed
bulwahn@46167: 
bulwahn@47143: setup_lifting type_definition_alist
bulwahn@47143: 
bulwahn@46167: lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
bulwahn@46167: by(simp add: impl_of_inject)
bulwahn@46167: 
bulwahn@46167: lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
bulwahn@46167: by(simp add: impl_of_inject)
bulwahn@46167: 
bulwahn@46167: lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
bulwahn@46167: using impl_of[of xs] by simp
bulwahn@46167: 
bulwahn@46167: lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
bulwahn@46167: by(rule impl_of_inverse)
bulwahn@46167: 
bulwahn@46167: subsection {* Primitive operations *}
bulwahn@46167: 
kuncar@55565: lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  .
bulwahn@46167: 
kuncar@47308: lift_definition empty :: "('key, 'value) alist" is "[]" by simp
bulwahn@46167: 
kuncar@47308: lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308:   is AList.update
bulwahn@47143: by (simp add: distinct_update)
bulwahn@46167: 
bulwahn@46167: (* FIXME: we use an unoptimised delete operation. *)
kuncar@47308: lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308:   is AList.delete
bulwahn@47143: by (simp add: distinct_delete)
bulwahn@46167: 
kuncar@47308: lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308:   is AList.map_entry
bulwahn@47143: by (simp add: distinct_map_entry)
bulwahn@46167: 
kuncar@47308: lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308:   is List.filter
bulwahn@47143: by (simp add: distinct_map_fst_filter)
bulwahn@46167: 
kuncar@47308: lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
kuncar@47308:   is AList.map_default
bulwahn@47143: by (simp add: distinct_map_default)
bulwahn@46167: 
bulwahn@46167: subsection {* Abstract operation properties *}
bulwahn@46167: 
bulwahn@46167: (* FIXME: to be completed *)
bulwahn@46167: 
bulwahn@46167: lemma lookup_empty [simp]: "lookup empty k = None"
bulwahn@46167: by(simp add: empty_def lookup_def Alist_inverse)
bulwahn@46167: 
bulwahn@46167: lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
bulwahn@46167: by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
bulwahn@46167: 
bulwahn@46167: subsection {* Further operations *}
bulwahn@46167: 
bulwahn@46167: subsubsection {* Equality *}
bulwahn@46167: 
bulwahn@46167: instantiation alist :: (equal, equal) equal begin
bulwahn@46167: 
bulwahn@46167: definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
bulwahn@46167: 
bulwahn@46167: instance
bulwahn@46167: proof
bulwahn@46167: qed (simp add: equal_alist_def impl_of_inject)
bulwahn@46167: 
bulwahn@46167: end
bulwahn@46167: 
bulwahn@46167: subsubsection {* Size *}
bulwahn@46167: 
bulwahn@46167: instantiation alist :: (type, type) size begin
bulwahn@46167: 
bulwahn@46167: definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
bulwahn@46167: 
bulwahn@46167: instance ..
bulwahn@46167: 
bulwahn@46167: end
bulwahn@46167: 
bulwahn@46167: subsection {* Quickcheck generators *}
bulwahn@46167: 
bulwahn@46167: notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167: notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167: 
bulwahn@46167: definition (in term_syntax)
bulwahn@46167:   valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
bulwahn@46167: where
bulwahn@46167:   "valterm_empty = Code_Evaluation.valtermify empty"
bulwahn@46167: 
bulwahn@46167: definition (in term_syntax)
bulwahn@46167:   valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167:   'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167:   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167:   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
bulwahn@46167:   [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
bulwahn@46167: 
bulwahn@46167: fun (in term_syntax) random_aux_alist 
bulwahn@46167: where
haftmann@51126:   "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck_Random.collapse (Random.select_weight [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (%k. Quickcheck_Random.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
bulwahn@46167: 
bulwahn@46167: instantiation alist :: (random, random) random
bulwahn@46167: begin
bulwahn@46167: 
bulwahn@46167: definition random_alist
bulwahn@46167: where
bulwahn@46167:   "random_alist i = random_aux_alist i i"
bulwahn@46167:  
bulwahn@46167: instance ..
bulwahn@46167: 
bulwahn@46167: end
bulwahn@46167: 
bulwahn@46167: no_notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167: no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167: 
bulwahn@46167: instantiation alist :: (exhaustive, exhaustive) exhaustive
bulwahn@46167: begin
bulwahn@46167: 
haftmann@51143: fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => natural => (bool * term list) option"
bulwahn@46167: where
bulwahn@46167:   "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
bulwahn@46167:      exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
bulwahn@46167: 
bulwahn@46167: instance ..
bulwahn@46167: 
bulwahn@46167: end
bulwahn@46167: 
bulwahn@46167: instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
bulwahn@46167: begin
bulwahn@46167: 
haftmann@51143: fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
bulwahn@46167: where
bulwahn@46167:   "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
bulwahn@46167:      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))"
bulwahn@46167: 
bulwahn@46167: instance ..
bulwahn@46167: 
bulwahn@46167: end
bulwahn@46167: 
bulwahn@46167: hide_const valterm_empty valterm_update random_aux_alist
bulwahn@46167: 
bulwahn@46171: hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
bulwahn@46167: hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
bulwahn@46167: 
bulwahn@46238: end