src/HOL/Library/DAList.thy
changeset 47308 9caab698dbe4
parent 47178 2ae2b6fa9c84
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/DAList.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Library/DAList.thy	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -39,33 +39,29 @@
     1.4  
     1.5  subsection {* Primitive operations *}
     1.6  
     1.7 -(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) 
     1.8 -
     1.9 -quotient_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    1.10 -where "lookup" is "map_of :: ('key * 'value) list \<Rightarrow> 'key \<Rightarrow> 'value option" ..
    1.11 +lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  ..
    1.12  
    1.13 -quotient_definition empty :: "('key, 'value) alist"
    1.14 -where "empty" is "[] :: ('key * 'value) list" by simp
    1.15 +lift_definition empty :: "('key, 'value) alist" is "[]" by simp
    1.16  
    1.17 -quotient_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.18 -where "update" is "AList.update :: 'key \<Rightarrow> 'value \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.19 +lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.20 +  is AList.update
    1.21  by (simp add: distinct_update)
    1.22  
    1.23  (* FIXME: we use an unoptimised delete operation. *)
    1.24 -quotient_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.25 -where "delete" is "AList.delete :: 'key \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.26 +lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.27 +  is AList.delete
    1.28  by (simp add: distinct_delete)
    1.29  
    1.30 -quotient_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.31 -where "map_entry" is "AList.map_entry :: 'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.32 +lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.33 +  is AList.map_entry
    1.34  by (simp add: distinct_map_entry)
    1.35  
    1.36 -quotient_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.37 -where "filter" is "List.filter :: ('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.38 +lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.39 +  is List.filter
    1.40  by (simp add: distinct_map_fst_filter)
    1.41  
    1.42 -quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.43 -where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
    1.44 +lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.45 +  is AList.map_default
    1.46  by (simp add: distinct_map_default)
    1.47  
    1.48  subsection {* Abstract operation properties *}