src/HOL/Library/RBT.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 49939 eb8b434158c8 child 51375 d9e62d9c98de permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
1 (*  Title:      HOL/Library/RBT.thy
2     Author:     Lukas Bulwahn and Ondrej Kuncar
3 *)
5 header {* Abstract type of RBT trees *}
7 theory RBT
8 imports Main RBT_Impl
9 begin
11 subsection {* Type definition *}
13 typedef ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
14   morphisms impl_of RBT
15 proof -
16   have "RBT_Impl.Empty \<in> ?rbt" by simp
17   then show ?thesis ..
18 qed
20 lemma rbt_eq_iff:
21   "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
24 lemma rbt_eqI:
25   "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
28 lemma is_rbt_impl_of [simp, intro]:
29   "is_rbt (impl_of t)"
30   using impl_of [of t] by simp
32 lemma RBT_impl_of [simp, code abstype]:
33   "RBT (impl_of t) = t"
36 subsection {* Primitive operations *}
38 setup_lifting type_definition_rbt
40 lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
41 by simp
43 lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
46 lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert"
47 by simp
49 lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
50 by simp
52 lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
53 by simp
55 lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
56 by simp
58 lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
59 by simp
61 lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
62 by simp
64 lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
65 by simp
67 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold
68 by simp
70 lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
73 lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
74   is RBT_Impl.foldi by simp
76 subsection {* Derived operations *}
78 definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
79   [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
82 subsection {* Abstract lookup properties *}
84 lemma lookup_RBT:
85   "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
86   by (simp add: lookup_def RBT_inverse)
88 lemma lookup_impl_of:
89   "rbt_lookup (impl_of t) = lookup t"
90   by transfer (rule refl)
92 lemma entries_impl_of:
93   "RBT_Impl.entries (impl_of t) = entries t"
94   by transfer (rule refl)
96 lemma keys_impl_of:
97   "RBT_Impl.keys (impl_of t) = keys t"
98   by transfer (rule refl)
100 lemma lookup_keys:
101   "dom (lookup t) = set (keys t)"
102   by transfer (simp add: rbt_lookup_keys)
104 lemma lookup_empty [simp]:
105   "lookup empty = Map.empty"
106   by (simp add: empty_def lookup_RBT fun_eq_iff)
108 lemma lookup_insert [simp]:
109   "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
110   by transfer (rule rbt_lookup_rbt_insert)
112 lemma lookup_delete [simp]:
113   "lookup (delete k t) = (lookup t)(k := None)"
114   by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
116 lemma map_of_entries [simp]:
117   "map_of (entries t) = lookup t"
118   by transfer (simp add: map_of_entries)
120 lemma entries_lookup:
121   "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
122   by transfer (simp add: entries_rbt_lookup)
125   "lookup (bulkload xs) = map_of xs"
128 lemma lookup_map_entry [simp]:
129   "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
130   by transfer (rule rbt_lookup_rbt_map_entry)
132 lemma lookup_map [simp]:
133   "lookup (map f t) k = Option.map (f k) (lookup t k)"
134   by transfer (rule rbt_lookup_map)
136 lemma fold_fold:
137   "fold f t = List.fold (prod_case f) (entries t)"
138   by transfer (rule RBT_Impl.fold_def)
140 lemma impl_of_empty:
141   "impl_of empty = RBT_Impl.Empty"
142   by transfer (rule refl)
144 lemma is_empty_empty [simp]:
145   "is_empty t \<longleftrightarrow> t = empty"
146   unfolding is_empty_def by transfer (simp split: rbt.split)
148 lemma RBT_lookup_empty [simp]: (*FIXME*)
149   "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
150   by (cases t) (auto simp add: fun_eq_iff)
152 lemma lookup_empty_empty [simp]:
153   "lookup t = Map.empty \<longleftrightarrow> t = empty"
154   by transfer (rule RBT_lookup_empty)
156 lemma sorted_keys [iff]:
157   "sorted (keys t)"
158   by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
160 lemma distinct_keys [iff]:
161   "distinct (keys t)"
162   by transfer (simp add: RBT_Impl.keys_def distinct_entries)
164 lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
165   by transfer simp
167 lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
168   by transfer (simp add: rbt_lookup_rbt_union)
170 lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
171   by transfer (simp add: rbt_lookup_in_tree)
173 lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
174   by transfer (simp add: keys_entries)
176 lemma fold_def_alt:
177   "fold f t = List.fold (prod_case f) (entries t)"
178   by transfer (auto simp: RBT_Impl.fold_def)
180 lemma distinct_entries: "distinct (List.map fst (entries t))"
181   by transfer (simp add: distinct_entries)
183 lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
184   by transfer (simp add: non_empty_rbt_keys)
186 lemma keys_def_alt:
187   "keys t = List.map fst (entries t)"
188   by transfer (simp add: RBT_Impl.keys_def)
190 subsection {* Quickcheck generators *}
192 quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
194 end