# HG changeset patch
# User Andreas Lochbihler
# Date 1348154240 -7200
# Node ID 4632b867fba75a23bf767234d88336184ff32ecb
# Parent  504f0a38f608c4ec9c0dcf4743379e482474a9e8
more efficient code setup

diff -r 504f0a38f608 -r 4632b867fba7 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Thu Sep 20 13:32:48 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Thu Sep 20 17:17:20 2012 +0200
@@ -1197,6 +1197,8 @@
 
 end
 
+subsection {* Code generator setup *}
+
 lemmas [code] =
   ord.rbt_less_prop
   ord.rbt_greater_prop
@@ -1217,6 +1219,36 @@
   ord.rbt_map_entry.simps
   ord.rbt_bulkload_def
 
+text {* More efficient implementations for @{term entries} and @{term keys} *}
+
+definition gen_entries :: 
+  "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
+where
+  "gen_entries kvts t = entries t @ concat (List.map (\<lambda>(kv, t). kv # entries t) kvts)"
+
+lemma gen_entries_simps [simp, code]:
+  "gen_entries [] Empty = []"
+  "gen_entries ((kv, t) # kvts) Empty = kv # gen_entries kvts t"
+  "gen_entries kvts (Branch c l k v r) = gen_entries (((k, v), r) # kvts) l"
+by(simp_all add: gen_entries_def)
+
+lemma entries_code [code]:
+  "entries = gen_entries []"
+by(simp add: gen_entries_def fun_eq_iff)
+
+definition gen_keys :: "('a \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a list"
+where "gen_keys kts t = RBT_Impl.keys t @ concat (List.map (\<lambda>(k, t). k # keys t) kts)"
+
+lemma gen_keys_simps [simp, code]:
+  "gen_keys [] Empty = []"
+  "gen_keys ((k, t) # kts) Empty = k # gen_keys kts t"
+  "gen_keys kts (Branch c l k v r) = gen_keys ((k, r) # kts) l"
+by(simp_all add: gen_keys_def)
+
+lemma keys_code [code]:
+  "keys = gen_keys []"
+by(simp add: gen_keys_def fun_eq_iff)
+
 text {* Restore original type constraints for constants *}
 setup {*
   fold Sign.add_const_constraint
@@ -1240,6 +1272,6 @@
      (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
 *}
 
-hide_const (open) R B Empty entries keys map fold
+hide_const (open) R B Empty entries keys map fold gen_keys gen_entries
 
 end