author | wenzelm |
Thu, 05 Nov 2015 10:39:49 +0100 | |
changeset 61585 | a9599d3d7610 |
parent 61260 | e6f03fae14d5 |
child 63194 | 0b7bdb75f451 |
permissions | -rw-r--r-- |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
1 |
(* Title: HOL/Library/RBT.thy |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
2 |
Author: Lukas Bulwahn and Ondrej Kuncar |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
3 |
*) |
35617 | 4 |
|
60500 | 5 |
section \<open>Abstract type of RBT trees\<close> |
35617 | 6 |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
7 |
theory RBT |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51375
diff
changeset
|
8 |
imports Main RBT_Impl |
35617 | 9 |
begin |
10 |
||
60500 | 11 |
subsection \<open>Type definition\<close> |
35617 | 12 |
|
61260 | 13 |
typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}" |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
14 |
morphisms impl_of RBT |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
15 |
proof - |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
16 |
have "RBT_Impl.Empty \<in> ?rbt" by simp |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
17 |
then show ?thesis .. |
35617 | 18 |
qed |
19 |
||
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
20 |
lemma rbt_eq_iff: |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
21 |
"t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2" |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
22 |
by (simp add: impl_of_inject) |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
23 |
|
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
24 |
lemma rbt_eqI: |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
25 |
"impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2" |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
26 |
by (simp add: rbt_eq_iff) |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
27 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
28 |
lemma is_rbt_impl_of [simp, intro]: |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
29 |
"is_rbt (impl_of t)" |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
30 |
using impl_of [of t] by simp |
35617 | 31 |
|
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
32 |
lemma RBT_impl_of [simp, code abstype]: |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
33 |
"RBT (impl_of t) = t" |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
34 |
by (simp add: impl_of_inverse) |
35617 | 35 |
|
60500 | 36 |
subsection \<open>Primitive operations\<close> |
35617 | 37 |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
38 |
setup_lifting type_definition_rbt |
35617 | 39 |
|
61076 | 40 |
lift_definition lookup :: "('a::linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" . |
35617 | 41 |
|
61076 | 42 |
lift_definition empty :: "('a::linorder, 'b) rbt" is RBT_Impl.Empty |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
43 |
by (simp add: empty_def) |
35617 | 44 |
|
61076 | 45 |
lift_definition insert :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
46 |
by simp |
35617 | 47 |
|
61076 | 48 |
lift_definition delete :: "'a::linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
49 |
by simp |
35617 | 50 |
|
61076 | 51 |
lift_definition entries :: "('a::linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries . |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55466
diff
changeset
|
52 |
|
61076 | 53 |
lift_definition keys :: "('a::linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys . |
35617 | 54 |
|
61076 | 55 |
lift_definition bulkload :: "('a::linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" .. |
35617 | 56 |
|
61076 | 57 |
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
58 |
by simp |
35617 | 59 |
|
61076 | 60 |
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
61 |
by simp |
35617 | 62 |
|
61076 | 63 |
lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold . |
35617 | 64 |
|
61076 | 65 |
lift_definition union :: "('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
66 |
by (simp add: rbt_union_is_rbt) |
35617 | 67 |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
68 |
lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55466
diff
changeset
|
69 |
is RBT_Impl.foldi . |
35617 | 70 |
|
60500 | 71 |
subsection \<open>Derived operations\<close> |
35617 | 72 |
|
61076 | 73 |
definition is_empty :: "('a::linorder, 'b) rbt \<Rightarrow> bool" where |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
74 |
[code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)" |
35617 | 75 |
|
76 |
||
60500 | 77 |
subsection \<open>Abstract lookup properties\<close> |
35617 | 78 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
79 |
lemma lookup_RBT: |
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset
|
80 |
"is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t" |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
81 |
by (simp add: lookup_def RBT_inverse) |
35617 | 82 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
83 |
lemma lookup_impl_of: |
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset
|
84 |
"rbt_lookup (impl_of t) = lookup t" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
85 |
by transfer (rule refl) |
35617 | 86 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
87 |
lemma entries_impl_of: |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
88 |
"RBT_Impl.entries (impl_of t) = entries t" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
89 |
by transfer (rule refl) |
35617 | 90 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
91 |
lemma keys_impl_of: |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
92 |
"RBT_Impl.keys (impl_of t) = keys t" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
93 |
by transfer (rule refl) |
36111 | 94 |
|
49927 | 95 |
lemma lookup_keys: |
96 |
"dom (lookup t) = set (keys t)" |
|
97 |
by transfer (simp add: rbt_lookup_keys) |
|
98 |
||
35617 | 99 |
lemma lookup_empty [simp]: |
100 |
"lookup empty = Map.empty" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
101 |
by (simp add: empty_def lookup_RBT fun_eq_iff) |
35617 | 102 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
103 |
lemma lookup_insert [simp]: |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset
|
104 |
"lookup (insert k v t) = (lookup t)(k \<mapsto> v)" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
105 |
by transfer (rule rbt_lookup_rbt_insert) |
35617 | 106 |
|
107 |
lemma lookup_delete [simp]: |
|
108 |
"lookup (delete k t) = (lookup t)(k := None)" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
109 |
by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq) |
35617 | 110 |
|
111 |
lemma map_of_entries [simp]: |
|
112 |
"map_of (entries t) = lookup t" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
113 |
by transfer (simp add: map_of_entries) |
35617 | 114 |
|
36111 | 115 |
lemma entries_lookup: |
116 |
"entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
117 |
by transfer (simp add: entries_rbt_lookup) |
36111 | 118 |
|
35617 | 119 |
lemma lookup_bulkload [simp]: |
120 |
"lookup (bulkload xs) = map_of xs" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
121 |
by transfer (rule rbt_lookup_rbt_bulkload) |
35617 | 122 |
|
123 |
lemma lookup_map_entry [simp]: |
|
55466 | 124 |
"lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
125 |
by transfer (rule rbt_lookup_rbt_map_entry) |
35617 | 126 |
|
127 |
lemma lookup_map [simp]: |
|
55466 | 128 |
"lookup (map f t) k = map_option (f k) (lookup t k)" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
129 |
by transfer (rule rbt_lookup_map) |
35617 | 130 |
|
131 |
lemma fold_fold: |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
53013
diff
changeset
|
132 |
"fold f t = List.fold (case_prod f) (entries t)" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
133 |
by transfer (rule RBT_Impl.fold_def) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
134 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
135 |
lemma impl_of_empty: |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
136 |
"impl_of empty = RBT_Impl.Empty" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
137 |
by transfer (rule refl) |
35617 | 138 |
|
36111 | 139 |
lemma is_empty_empty [simp]: |
140 |
"is_empty t \<longleftrightarrow> t = empty" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
141 |
unfolding is_empty_def by transfer (simp split: rbt.split) |
36111 | 142 |
|
143 |
lemma RBT_lookup_empty [simp]: (*FIXME*) |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset
|
144 |
"rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
145 |
by (cases t) (auto simp add: fun_eq_iff) |
36111 | 146 |
|
147 |
lemma lookup_empty_empty [simp]: |
|
148 |
"lookup t = Map.empty \<longleftrightarrow> t = empty" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
149 |
by transfer (rule RBT_lookup_empty) |
36111 | 150 |
|
151 |
lemma sorted_keys [iff]: |
|
152 |
"sorted (keys t)" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
153 |
by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries) |
36111 | 154 |
|
155 |
lemma distinct_keys [iff]: |
|
156 |
"distinct (keys t)" |
|
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
157 |
by transfer (simp add: RBT_Impl.keys_def distinct_entries) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
158 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
159 |
lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
160 |
by transfer simp |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
161 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
162 |
lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
163 |
by transfer (simp add: rbt_lookup_rbt_union) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
164 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
165 |
lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
166 |
by transfer (simp add: rbt_lookup_in_tree) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
167 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
168 |
lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
169 |
by transfer (simp add: keys_entries) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
170 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
171 |
lemma fold_def_alt: |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
53013
diff
changeset
|
172 |
"fold f t = List.fold (case_prod f) (entries t)" |
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
173 |
by transfer (auto simp: RBT_Impl.fold_def) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
174 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
175 |
lemma distinct_entries: "distinct (List.map fst (entries t))" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
176 |
by transfer (simp add: distinct_entries) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
177 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
178 |
lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
179 |
by transfer (simp add: non_empty_rbt_keys) |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
180 |
|
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
181 |
lemma keys_def_alt: |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
182 |
"keys t = List.map fst (entries t)" |
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset
|
183 |
by transfer (simp add: RBT_Impl.keys_def) |
36111 | 184 |
|
60500 | 185 |
subsection \<open>Quickcheck generators\<close> |
45928
874845660119
adding quickcheck generators in some HOL-Library theories
bulwahn
parents:
45694
diff
changeset
|
186 |
|
46565 | 187 |
quickcheck_generator rbt predicate: is_rbt constructors: empty, insert |
36111 | 188 |
|
60500 | 189 |
subsection \<open>Hide implementation details\<close> |
56019 | 190 |
|
191 |
lifting_update rbt.lifting |
|
192 |
lifting_forget rbt.lifting |
|
193 |
||
194 |
hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi |
|
195 |
is_empty |
|
196 |
hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def |
|
197 |
union_def insert_def map_entry_def foldi_def is_empty_def |
|
198 |
||
35617 | 199 |
end |