Theory RBT_Compare_Order_Impl
subsection ‹Example: Modifying the Code-Equations of Red-Black-Trees›
theory RBT_Compare_Order_Impl
imports
Compare
"HOL-Library.RBT_Impl"
begin
text ‹In the following, we modify all code-equations of the red-black-tree
implementation that perform comparisons. As a positive result, they now all require
one invocation of comparator, where before two comparisons have been performed.
The disadvantage of this simple solution is the additional class constraint on
@{class compare_order}.›
compare_code ("'a") rbt_ins
compare_code ("'a") rbt_lookup
compare_code ("'a") rbt_del
compare_code ("'a") rbt_map_entry
compare_code ("'a") sunion_with
compare_code ("'a") sinter_with
compare_code ("'a") rbt_split
export_code rbt_ins rbt_lookup rbt_del rbt_map_entry rbt_union_with_key rbt_inter_with_key rbt_minus in Haskell
end