Theory RBTSetImpl

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
(*
  Changes since submission on 2009-11-26:

  2009-12-10: OrderedSet, implemented iterators, min, max, to_sorted_list

*)

header {* \isaheader{Set Implementation by Red-Black-Tree} *}
theory RBTSetImpl
imports 
  "../spec/SetSpec"
  "RBTMapImpl"
  "../gen_algo/SetByMap"
  "../gen_algo/SetGA"
begin
text_raw {*\label{thy:RBTSetImpl}*}
(*@impl Set
  @type ('a::linorder) rs
  @abbrv rs,r
  Sets over linearly ordered elements implemented by red-black trees.
*)

subsection "Definitions"
type_synonym
  'a rs = "('a::linorder,unit) rm"

definition rs_α :: "'a::linorder rs => 'a set" where "rs_α == s_α rm_α"
abbreviation (input) rs_invar :: "'a::linorder rs => bool" where "rs_invar == rm_invar"
definition rs_empty :: "unit => 'a::linorder rs" where "rs_empty == s_empty rm_empty"
definition rs_memb :: "'a::linorder => 'a rs => bool" 
  where "rs_memb == s_memb rm_lookup"
definition rs_ins :: "'a::linorder => 'a rs => 'a rs" 
  where "rs_ins == s_ins rm_update"
definition rs_ins_dj :: "'a::linorder => 'a rs => 'a rs" where
  "rs_ins_dj == s_ins_dj rm_update_dj"
definition rs_delete :: "'a::linorder => 'a rs => 'a rs" 
  where "rs_delete == s_delete rm_delete"
definition rs_sel :: "'a::linorder rs => ('a => 'r option) => 'r option" 
  where "rs_sel == s_sel rm_sel"
definition "rs_sel' = sel_sel' rs_sel"
definition rs_isEmpty :: "'a::linorder rs => bool"
  where "rs_isEmpty == s_isEmpty rm_isEmpty"

definition rs_iteratei :: "'a::linorder rs => ('a,'σ) set_iterator" 
  where "rs_iteratei == s_iteratei rm_iteratei"

definition rs_iterateoi :: "'a::linorder rs => ('a,'σ) set_iterator" 
  where "rs_iterateoi == s_iteratei rm_iterateoi"

definition rs_reverse_iterateoi :: "'a::linorder rs => ('a,'σ) set_iterator" 
  where "rs_reverse_iterateoi == s_iteratei rm_reverse_iterateoi"

definition rs_union :: "'a::linorder rs => 'a rs => 'a rs" 
  where "rs_union == s_union rm_add"
definition rs_union_dj :: "'a::linorder rs => 'a rs => 'a rs" 
  where "rs_union_dj == s_union_dj rm_add_dj"
definition rs_inter :: "'a::linorder rs => 'a rs => 'a rs" 
  where "rs_inter == it_inter rs_iteratei rs_memb rs_empty rs_ins_dj"

definition rs_image_filter 
  where "rs_image_filter == it_image_filter rs_iteratei rs_empty rs_ins"
definition rs_inj_image_filter 
  where "rs_inj_image_filter == it_inj_image_filter rs_iteratei rs_empty rs_ins_dj"

definition rs_image where "rs_image == iflt_image rs_image_filter"
definition rs_inj_image where "rs_inj_image == iflt_inj_image rs_inj_image_filter"

definition "rs_to_list == it_set_to_list rs_reverse_iterateoi"
definition "list_to_rs == gen_list_to_set rs_empty rs_ins"

definition "rs_min == iti_sel_no_map rs_iterateoi"
definition "rs_max == iti_sel_no_map rs_reverse_iterateoi"

subsection "Correctness"

lemmas rs_defs =
  list_to_rs_def
  rs_α_def
  rs_delete_def
  rs_empty_def
  rs_image_def
  rs_image_filter_def
  rs_inj_image_def
  rs_inj_image_filter_def
  rs_ins_def
  rs_ins_dj_def
  rs_inter_def
  rs_isEmpty_def
  rs_iteratei_def
  rs_iterateoi_def
  rs_reverse_iterateoi_def
  rs_memb_def
  rs_sel_def
  rs_sel'_def
  rs_to_list_def
  rs_union_def
  rs_union_dj_def
  rs_min_def
  rs_max_def


lemmas rs_empty_impl = s_empty_correct[OF rm_empty_impl, folded rs_defs]
lemmas rs_memb_impl = s_memb_correct[OF rm_lookup_impl, folded rs_defs]
lemmas rs_ins_impl = s_ins_correct[OF rm_update_impl, folded rs_defs]
lemmas rs_ins_dj_impl = s_ins_dj_correct[OF rm_update_dj_impl, folded rs_defs]
lemmas rs_delete_impl = s_delete_correct[OF rm_delete_impl, folded rs_defs]
lemmas rs_iteratei_impl = s_iteratei_correct[OF rm_iteratei_impl, folded rs_defs]
lemmas rs_iterateoi_impl = s_iterateoi_correct[OF rm_iterateoi_impl, folded rs_defs]
lemmas rs_reverse_iterateoi_impl = s_reverse_iterateoi_correct[OF rm_reverse_iterateoi_impl, folded rs_defs]
lemmas rs_isEmpty_impl = s_isEmpty_correct[OF rm_isEmpty_impl, folded rs_defs]
lemmas rs_union_impl = s_union_correct[OF rm_add_impl, folded rs_defs]
lemmas rs_union_dj_impl = s_union_dj_correct[OF rm_add_dj_impl, folded rs_defs]
lemmas rs_sel_impl = s_sel_correct[OF rm_sel_impl, folded rs_defs]
lemmas rs_sel'_impl = sel_sel'_correct[OF rs_sel_impl, folded rs_sel'_def]
lemmas rs_inter_impl = it_inter_correct[OF rs_iteratei_impl rs_memb_impl rs_empty_impl rs_ins_dj_impl, folded rs_inter_def]
lemmas rs_image_filter_impl = it_image_filter_correct[OF rs_iteratei_impl rs_empty_impl rs_ins_impl, folded rs_image_filter_def]
lemmas rs_inj_image_filter_impl = it_inj_image_filter_correct[OF rs_iteratei_impl rs_empty_impl rs_ins_dj_impl, folded rs_inj_image_filter_def]
lemmas rs_image_impl = iflt_image_correct[OF rs_image_filter_impl, folded rs_image_def]
lemmas rs_inj_image_impl = iflt_inj_image_correct[OF rs_inj_image_filter_impl, folded rs_inj_image_def]
lemmas rs_to_list_impl = rito_set_to_sorted_list_correct[OF rs_reverse_iterateoi_impl, folded rs_to_list_def]
lemmas list_to_rs_impl = gen_list_to_set_correct[OF rs_empty_impl rs_ins_impl, folded list_to_rs_def]

lemmas rs_min_impl = itoi_min_correct[OF rs_iterateoi_impl, folded rs_defs]
lemmas rs_max_impl = ritoi_max_correct[OF rs_reverse_iterateoi_impl, folded rs_defs]

interpretation rs: set_iteratei rs_α rs_invar rs_iteratei using rs_iteratei_impl .                               
interpretation rs: set_iterateoi rs_α rs_invar rs_iterateoi using rs_iterateoi_impl .                               
interpretation rs: set_reverse_iterateoi rs_α rs_invar rs_reverse_iterateoi using rs_reverse_iterateoi_impl .                               

interpretation rs: set_inj_image_filter rs_α rs_invar rs_α rs_invar rs_inj_image_filter using rs_inj_image_filter_impl .
interpretation rs: set_image_filter rs_α rs_invar rs_α rs_invar rs_image_filter using rs_image_filter_impl .
interpretation rs: set_inj_image rs_α rs_invar rs_α rs_invar rs_inj_image using rs_inj_image_impl .
interpretation rs: set_union_dj rs_α rs_invar rs_α rs_invar rs_α rs_invar rs_union_dj using rs_union_dj_impl .
interpretation rs: set_union rs_α rs_invar rs_α rs_invar rs_α rs_invar rs_union using rs_union_impl .
interpretation rs: set_inter rs_α rs_invar rs_α rs_invar rs_α rs_invar rs_inter using rs_inter_impl .
interpretation rs: set_image rs_α rs_invar rs_α rs_invar rs_image using rs_image_impl .
interpretation rs: set_sel rs_α rs_invar rs_sel using rs_sel_impl .
interpretation rs: set_sel' rs_α rs_invar rs_sel' using rs_sel'_impl .
interpretation rs: set_ins_dj rs_α rs_invar rs_ins_dj using rs_ins_dj_impl .
interpretation rs: set_delete rs_α rs_invar rs_delete using rs_delete_impl .
interpretation rs: set_ins rs_α rs_invar rs_ins using rs_ins_impl .
interpretation rs: set_memb rs_α rs_invar rs_memb using rs_memb_impl .
interpretation rs: set_to_sorted_list rs_α rs_invar rs_to_list using rs_to_list_impl .
interpretation rs: list_to_set rs_α rs_invar list_to_rs using list_to_rs_impl .
interpretation rs: set_isEmpty rs_α rs_invar rs_isEmpty using rs_isEmpty_impl .
interpretation rs: set_empty rs_α rs_invar rs_empty using rs_empty_impl .
interpretation rs: set_min rs_α rs_invar rs_min using rs_min_impl .
interpretation rs: set_max rs_α rs_invar rs_max using rs_max_impl .


lemmas rs_correct = 
  rs.inj_image_filter_correct
  rs.image_filter_correct
  rs.inj_image_correct
  rs.union_dj_correct
  rs.union_correct
  rs.inter_correct
  rs.image_correct
  rs.ins_dj_correct
  rs.delete_correct
  rs.ins_correct
  rs.memb_correct
  rs.to_list_correct
  rs.to_set_correct
  rs.isEmpty_correct
  rs.empty_correct


subsection "Code Generation"
export_code
  rs_iteratei
  rs_iterateoi
  rs_reverse_iterateoi
  rs_inj_image_filter
  rs_image_filter
  rs_inj_image
  rs_union_dj
  rs_union
  rs_inter
  rs_image
  rs_sel
  rs_sel'
  rs_ins_dj
  rs_delete
  rs_ins
  rs_memb
  rs_to_list
  list_to_rs
  rs_isEmpty
  rs_empty
  rs_min
  rs_max
  in SML
  module_name RBTSet
  file -

end