src/HOL/Library/RBT_Impl.thy
changeset 49480 4632b867fba7
parent 48621 877df57629e3
child 49770 cf6a78acf445
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Sep 20 13:32:48 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Thu Sep 20 17:17:20 2012 +0200
     1.3 @@ -1197,6 +1197,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +subsection {* Code generator setup *}
     1.8 +
     1.9  lemmas [code] =
    1.10    ord.rbt_less_prop
    1.11    ord.rbt_greater_prop
    1.12 @@ -1217,6 +1219,36 @@
    1.13    ord.rbt_map_entry.simps
    1.14    ord.rbt_bulkload_def
    1.15  
    1.16 +text {* More efficient implementations for @{term entries} and @{term keys} *}
    1.17 +
    1.18 +definition gen_entries :: 
    1.19 +  "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    1.20 +where
    1.21 +  "gen_entries kvts t = entries t @ concat (List.map (\<lambda>(kv, t). kv # entries t) kvts)"
    1.22 +
    1.23 +lemma gen_entries_simps [simp, code]:
    1.24 +  "gen_entries [] Empty = []"
    1.25 +  "gen_entries ((kv, t) # kvts) Empty = kv # gen_entries kvts t"
    1.26 +  "gen_entries kvts (Branch c l k v r) = gen_entries (((k, v), r) # kvts) l"
    1.27 +by(simp_all add: gen_entries_def)
    1.28 +
    1.29 +lemma entries_code [code]:
    1.30 +  "entries = gen_entries []"
    1.31 +by(simp add: gen_entries_def fun_eq_iff)
    1.32 +
    1.33 +definition gen_keys :: "('a \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a list"
    1.34 +where "gen_keys kts t = RBT_Impl.keys t @ concat (List.map (\<lambda>(k, t). k # keys t) kts)"
    1.35 +
    1.36 +lemma gen_keys_simps [simp, code]:
    1.37 +  "gen_keys [] Empty = []"
    1.38 +  "gen_keys ((k, t) # kts) Empty = k # gen_keys kts t"
    1.39 +  "gen_keys kts (Branch c l k v r) = gen_keys ((k, r) # kts) l"
    1.40 +by(simp_all add: gen_keys_def)
    1.41 +
    1.42 +lemma keys_code [code]:
    1.43 +  "keys = gen_keys []"
    1.44 +by(simp add: gen_keys_def fun_eq_iff)
    1.45 +
    1.46  text {* Restore original type constraints for constants *}
    1.47  setup {*
    1.48    fold Sign.add_const_constraint
    1.49 @@ -1240,6 +1272,6 @@
    1.50       (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
    1.51  *}
    1.52  
    1.53 -hide_const (open) R B Empty entries keys map fold
    1.54 +hide_const (open) R B Empty entries keys map fold gen_keys gen_entries
    1.55  
    1.56  end