a couple of additions to RBT formalization to allow us to implement RBT_Set

--- a/src/HOL/Library/RBT_Impl.thy	Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Tue Jul 31 13:55:39 2012 +0200
@@ -62,6 +62,9 @@
   "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
   by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
 
+lemma non_empty_rbt_keys: 
+  "t \<noteq> rbt.Empty \<Longrightarrow> keys t \<noteq> []"
+  by (cases t) simp_all
 
 subsubsection {* Search tree properties *}
 
@@ -121,6 +124,11 @@
   (force simp: sorted_append sorted_Cons rbt_ord_props 
       dest!: entry_in_tree_keys)+
 
+lemma distinct_keys:
+  "rbt_sorted t \<Longrightarrow> distinct (keys t)"
+  by (simp add: distinct_entries keys_def)
+
+
 subsubsection {* Tree lookup *}
 
 primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
@@ -1059,7 +1067,7 @@
     qed
   qed
 
-  from Branch have is_rbt: "is_rbt (RBT_Impl.rbt_union (RBT_Impl.rbt_insert k v s) l)"
+  from Branch have is_rbt: "is_rbt (rbt_union (rbt_insert k v s) l)"
     by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
   with Branch have IHs:
     "rbt_lookup (rbt_union (rbt_union (rbt_insert k v s) l) r) = rbt_lookup (rbt_union (rbt_insert k v s) l) ++ rbt_lookup r"
@@ -1148,6 +1156,20 @@
   "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
   by (simp_all add: fold_def fun_eq_iff)
 
+(* fold with continuation predicate *)
+
+fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
+  where
+  "foldi c f Empty s = s" |
+  "foldi c f (Branch col l k v r) s = (
+    if (c s) then
+      let s' = foldi c f l s in
+        if (c s') then
+          foldi c f r (f k v s')
+        else s'
+    else 
+      s
+  )"
 
 subsection {* Bulkloading a tree *}
 

--- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Jul 31 13:55:39 2012 +0200
@@ -69,7 +69,13 @@
 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
 by simp
 
-export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
+lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
+by (simp add: rbt_union_is_rbt)
+
+lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+  is RBT_Impl.foldi by simp
+
+export_code lookup empty insert delete entries keys bulkload map_entry map fold union foldi in SML
 
 subsection {* Derived operations *}
 
@@ -155,5 +161,30 @@
   "distinct (keys t)"
   by transfer (simp add: RBT_Impl.keys_def distinct_entries)
 
+lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
+  by transfer simp
+
+lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
+  by transfer (simp add: rbt_lookup_rbt_union)
+
+lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
+  by transfer (simp add: rbt_lookup_in_tree)
+
+lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
+  by transfer (simp add: keys_entries)
+
+lemma fold_def_alt:
+  "fold f t = List.fold (prod_case f) (entries t)"
+  by transfer (auto simp: RBT_Impl.fold_def)
+
+lemma distinct_entries: "distinct (List.map fst (entries t))"
+  by transfer (simp add: distinct_entries)
+
+lemma non_empty_keys: "t \<noteq> Lift_RBT.empty \<Longrightarrow> keys t \<noteq> []"
+  by transfer (simp add: non_empty_rbt_keys)
+
+lemma keys_def_alt:
+  "keys t = List.map fst (entries t)"
+  by transfer (simp add: RBT_Impl.keys_def)
 
 end
\ No newline at end of file