author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63219  a5697f7a3322 
permissions  rwrr 
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 redblack 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 redblack 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 redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

29 
"is_rbt (impl_of t)" 
b43b22f63665
theory RBT with abstract type of redblack 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 redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

33 
"RBT (impl_of t) = t" 
b43b22f63665
theory RBT with abstract type of redblack 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 . 
63194  70 

71 
lift_definition combine_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" 

72 
is RBT_Impl.rbt_union_with_key by (rule is_rbt_rbt_unionwk) 

73 

74 
lift_definition combine :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" 

75 
is RBT_Impl.rbt_union_with by (rule rbt_unionw_is_rbt) 

35617  76 

60500  77 
subsection \<open>Derived operations\<close> 
35617  78 

61076  79 
definition is_empty :: "('a::linorder, 'b) rbt \<Rightarrow> bool" where 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

80 
[code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True  _ \<Rightarrow> False)" 
35617  81 

63194  82 
(* TODO: Is deleting more efficient than rebuilding the tree? 
83 
(Probably more difficult to prove though *) 

84 
definition filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where 

85 
[code]: "filter P t = fold (\<lambda>k v t. if P k v then insert k v t else t) t empty" 

35617  86 

60500  87 
subsection \<open>Abstract lookup properties\<close> 
35617  88 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

89 
lemma lookup_RBT: 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset

90 
"is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t" 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

91 
by (simp add: lookup_def RBT_inverse) 
35617  92 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

93 
lemma lookup_impl_of: 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset

94 
"rbt_lookup (impl_of t) = lookup t" 
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

95 
by transfer (rule refl) 
35617  96 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

97 
lemma entries_impl_of: 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

98 
"RBT_Impl.entries (impl_of t) = entries t" 
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

99 
by transfer (rule refl) 
35617  100 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

101 
lemma keys_impl_of: 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

102 
"RBT_Impl.keys (impl_of t) = keys t" 
48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

103 
by transfer (rule refl) 
36111  104 

49927  105 
lemma lookup_keys: 
106 
"dom (lookup t) = set (keys t)" 

107 
by transfer (simp add: rbt_lookup_keys) 

108 

35617  109 
lemma lookup_empty [simp]: 
110 
"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

111 
by (simp add: empty_def lookup_RBT fun_eq_iff) 
35617  112 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

113 
lemma lookup_insert [simp]: 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36111
diff
changeset

114 
"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

115 
by transfer (rule rbt_lookup_rbt_insert) 
35617  116 

117 
lemma lookup_delete [simp]: 

118 
"lookup (delete k t) = (lookup t)(k := None)" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

119 
by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq) 
35617  120 

121 
lemma map_of_entries [simp]: 

122 
"map_of (entries t) = lookup t" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

123 
by transfer (simp add: map_of_entries) 
35617  124 

36111  125 
lemma entries_lookup: 
126 
"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

127 
by transfer (simp add: entries_rbt_lookup) 
36111  128 

35617  129 
lemma lookup_bulkload [simp]: 
130 
"lookup (bulkload xs) = map_of xs" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

131 
by transfer (rule rbt_lookup_rbt_bulkload) 
35617  132 

133 
lemma lookup_map_entry [simp]: 

55466  134 
"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

135 
by transfer (rule rbt_lookup_rbt_map_entry) 
35617  136 

137 
lemma lookup_map [simp]: 

55466  138 
"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

139 
by transfer (rule rbt_lookup_map) 
35617  140 

63194  141 
lemma lookup_combine_with_key [simp]: 
142 
"lookup (combine_with_key f t1 t2) k = combine_options (f k) (lookup t1 k) (lookup t2 k)" 

143 
by transfer (simp_all add: combine_options_def rbt_lookup_rbt_unionwk) 

144 

145 
lemma combine_altdef: "combine f t1 t2 = combine_with_key (\<lambda>_. f) t1 t2" 

146 
by transfer (simp add: rbt_union_with_def) 

147 

148 
lemma lookup_combine [simp]: 

149 
"lookup (combine f t1 t2) k = combine_options f (lookup t1 k) (lookup t2 k)" 

150 
by (simp add: combine_altdef) 

151 

35617  152 
lemma fold_fold: 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
53013
diff
changeset

153 
"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

154 
by transfer (rule RBT_Impl.fold_def) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

155 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

156 
lemma impl_of_empty: 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

157 
"impl_of empty = RBT_Impl.Empty" 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

158 
by transfer (rule refl) 
35617  159 

36111  160 
lemma is_empty_empty [simp]: 
161 
"is_empty t \<longleftrightarrow> t = empty" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

162 
unfolding is_empty_def by transfer (simp split: rbt.split) 
36111  163 

164 
lemma RBT_lookup_empty [simp]: (*FIXME*) 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
46565
diff
changeset

165 
"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

166 
by (cases t) (auto simp add: fun_eq_iff) 
36111  167 

168 
lemma lookup_empty_empty [simp]: 

169 
"lookup t = Map.empty \<longleftrightarrow> t = empty" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

170 
by transfer (rule RBT_lookup_empty) 
36111  171 

172 
lemma sorted_keys [iff]: 

173 
"sorted (keys t)" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

174 
by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries) 
36111  175 

176 
lemma distinct_keys [iff]: 

177 
"distinct (keys t)" 

48622
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

178 
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

179 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

180 
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

181 
by transfer simp 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

182 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

183 
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

184 
by transfer (simp add: rbt_lookup_rbt_union) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

185 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

186 
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

187 
by transfer (simp add: rbt_lookup_in_tree) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

188 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

189 
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

190 
by transfer (simp add: keys_entries) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

191 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

192 
lemma fold_def_alt: 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
53013
diff
changeset

193 
"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

194 
by transfer (auto simp: RBT_Impl.fold_def) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

195 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

196 
lemma distinct_entries: "distinct (List.map fst (entries t))" 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

197 
by transfer (simp add: distinct_entries) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

198 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

199 
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

200 
by transfer (simp add: non_empty_rbt_keys) 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

201 

caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

202 
lemma keys_def_alt: 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

203 
"keys t = List.map fst (entries t)" 
caaa1a02c650
use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents:
47450
diff
changeset

204 
by transfer (simp add: RBT_Impl.keys_def) 
36111  205 

63194  206 
context 
207 
begin 

208 

209 
private lemma lookup_filter_aux: 

210 
assumes "distinct (List.map fst xs)" 

211 
shows "lookup (List.fold (\<lambda>(k, v) t. if P k v then insert k v t else t) xs t) k = 

212 
(case map_of xs k of 

213 
None \<Rightarrow> lookup t k 

214 
 Some v \<Rightarrow> if P k v then Some v else lookup t k)" 

215 
using assms by (induction xs arbitrary: t) (force split: option.splits)+ 

216 

217 
lemma lookup_filter: 

218 
"lookup (filter P t) k = 

219 
(case lookup t k of None \<Rightarrow> None  Some v \<Rightarrow> if P k v then Some v else None)" 

220 
unfolding filter_def using lookup_filter_aux[of "entries t" P empty k] 

221 
by (simp add: fold_fold distinct_entries split: option.splits) 

222 

223 
end 

224 

225 

60500  226 
subsection \<open>Quickcheck generators\<close> 
45928
874845660119
adding quickcheck generators in some HOLLibrary theories
bulwahn
parents:
45694
diff
changeset

227 

46565  228 
quickcheck_generator rbt predicate: is_rbt constructors: empty, insert 
36111  229 

60500  230 
subsection \<open>Hide implementation details\<close> 
56019  231 

232 
lifting_update rbt.lifting 

233 
lifting_forget rbt.lifting 

234 

235 
hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi 

63219  236 
is_empty filter 
56019  237 
hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def 
63219  238 
union_def insert_def map_entry_def foldi_def is_empty_def filter_def 
56019  239 

35617  240 
end 