Theory Collections.SetByMap

(*  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: OrderedMap, transfer of iterators to OrderedSet

*)
section ‹\isaheader{Implementing Sets by Maps}›
theory SetByMap
imports 
  "../spec/SetSpec"
  "../spec/MapSpec"
  SetGA
  MapGA
begin
text_raw ‹\label{thy:SetByMap}›

text ‹
  In this theory, we show how to implement sets
  by maps.
›

(* TODO: We could also define some more operations directly,
  e.g. union, ball, bex, … *)

text ‹Auxiliary lemma›
lemma foldli_foldli_map_eq:
  "foldli (foldli l (λx. True) (λx l. l@[f x]) []) c f' σ0
    = foldli l c (f' o f) σ0"
proof -
  show ?thesis
    apply (simp add: map_by_foldl foldli_map foldli_foldl)
    done
qed

locale SetByMapDefs =
  map: StdBasicMapDefs ops
  for ops :: "('x,unit,'s,'more) map_basic_ops_scheme"
begin
  definition "α s ≡ dom (map.α s)"
  definition "invar s ≡ map.invar s"
  definition empty where "empty ≡ map.empty"
  definition "memb x s ≡ map.lookup x s ≠ None"
  definition "ins x s ≡ map.update x () s"
  definition "ins_dj x s ≡ map.update_dj x () s"
  definition "delete x s ≡ map.delete x s"
  definition list_it :: "'s ⇒ ('x,'x list) set_iterator" 
    where "list_it s c f σ0 ≡ it_to_it (map.list_it s) c (f o fst) σ0"

  local_setup ‹Locale_Code.lc_decl_del @{term list_it}›

  lemma list_it_alt: "list_it s = map_iterator_dom (map.iteratei s)"
  proof -
    have A: "⋀f. (λ(x,_). f x) = (λx. f (fst x))" by auto
    show ?thesis
      unfolding list_it_def[abs_def] map_iterator_dom_def
        poly_map_iteratei_defs.iteratei_def
        set_iterator_image_def set_iterator_image_filter_def
      by (auto simp: comp_def)
  qed

  lemma list_it_unfold:
    "it_to_it (list_it s) c f σ0 = map.iteratei s c (f o fst) σ0"
    unfolding list_it_def[abs_def] it_to_it_def
    unfolding poly_map_iteratei_defs.iteratei_def it_to_it_def
    by (simp add: foldli_foldli_map_eq comp_def)

  definition [icf_rec_def]: "dflt_basic_ops ≡ ⦇
    bset_op_α = α,
    bset_op_invar = invar,
    bset_op_empty = empty,
    bset_op_memb = memb,
    bset_op_ins = ins,
    bset_op_ins_dj = ins_dj,
    bset_op_delete = delete,
    bset_op_list_it = list_it
    ⦈"
  local_setup ‹Locale_Code.lc_decl_del @{term dflt_basic_ops}›

end

setup ‹
  (Record_Intf.add_unf_thms_global @{thms 
    SetByMapDefs.list_it_def[abs_def]
  })
› 


(*lemmas [code_unfold] = SetByMapDefs.list_it_def[abs_def]*)

locale SetByMap = SetByMapDefs ops +
  map: StdBasicMap ops
  for ops :: "('x,unit,'s,'more) map_basic_ops_scheme"
begin
  lemma empty_impl: "set_empty α invar empty"
    apply unfold_locales
    unfolding α_def invar_def empty_def
    by (auto simp: map.empty_correct)

  lemma memb_impl: "set_memb α invar memb"
    apply unfold_locales
    unfolding α_def invar_def memb_def
    by (auto simp: map.lookup_correct)

  lemma ins_impl: "set_ins α invar ins"
    apply unfold_locales
    unfolding α_def invar_def ins_def
    by (auto simp: map.update_correct)

  lemma ins_dj_impl: "set_ins_dj α invar ins_dj"
    apply unfold_locales
    unfolding α_def invar_def ins_dj_def
    by (auto simp: map.update_dj_correct)

  lemma delete_impl: "set_delete α invar delete"
    apply unfold_locales
    unfolding α_def invar_def delete_def
    by (auto simp: map.delete_correct)
  
  lemma list_it_impl: "poly_set_iteratei α invar list_it"
  proof
    fix s
    assume I: "invar s"
    hence I': "map.invar s" unfolding invar_def .

    have S: "⋀f. (λ(x,_). f x) = (λxy. f (fst xy))"
      by auto
  
    from map_iterator_dom_correct[OF map.iteratei_correct[OF I']] 
    show "set_iterator (list_it s) (α s)"
      unfolding α_def list_it_alt .

    show "finite (α s)"
      unfolding α_def by (simp add: map.finite[OF I'])
  qed

  lemma dflt_basic_ops_impl: "StdBasicSet dflt_basic_ops"
    apply (rule StdBasicSet.intro)
    apply (simp_all add: icf_rec_unf)
    apply (rule empty_impl memb_impl ins_impl
      ins_dj_impl delete_impl 
      list_it_impl[unfolded SetByMapDefs.list_it_def[abs_def]]
    )+
    done
end


locale OSetByOMapDefs = SetByMapDefs ops +
  map: StdBasicOMapDefs ops
  for ops :: "('x::linorder,unit,'s,'more) omap_basic_ops_scheme"
begin
  definition ordered_list_it :: "'s ⇒ ('x,'x list) set_iterator" 
    where "ordered_list_it s c f σ0 
    ≡ it_to_it (map.ordered_list_it s) c (f o fst) σ0"
    (*where "list_it s c f σ0 ≡ it_to_it (map.list_it s) c (f o fst) σ0"*)
  local_setup ‹Locale_Code.lc_decl_del @{term ordered_list_it}›

  definition rev_list_it :: "'s ⇒ ('x,'x list) set_iterator" 
    where "rev_list_it s c f σ0 ≡ it_to_it (map.rev_list_it s) c (f o fst) σ0"
    (*where "rev_list_it s c f σ0 ≡ map.rev_iterateoi s c (f o fst) σ0"*)
  local_setup ‹Locale_Code.lc_decl_del @{term rev_list_it}›


  definition [icf_rec_def]: "dflt_basic_oops ≡ 
    set_basic_ops.extend dflt_basic_ops ⦇
      bset_op_ordered_list_it = ordered_list_it,
      bset_op_rev_list_it = rev_list_it
      ⦈"
  local_setup ‹Locale_Code.lc_decl_del @{term dflt_basic_oops}›

end

setup ‹
  (Record_Intf.add_unf_thms_global @{thms 
    OSetByOMapDefs.ordered_list_it_def[abs_def]
    OSetByOMapDefs.rev_list_it_def[abs_def]
  })
› 

(*lemmas [code_unfold] = OSetByOMapDefs.ordered_list_it_def[abs_def]
  OSetByOMapDefs.rev_list_it_def[abs_def]*)

locale OSetByOMap = OSetByOMapDefs ops +
  SetByMap ops + map: StdBasicOMap ops
  for ops :: "('x::linorder,unit,'s,'more) omap_basic_ops_scheme"
begin
  lemma ordered_list_it_impl: "poly_set_iterateoi α invar ordered_list_it"
  proof
    fix s
    assume I: "invar s"
    hence I': "map.invar s" unfolding invar_def .

    have S: "⋀f. (λ(x,_). f x) = (λxy. f (fst xy))"
      by auto

    have A: "⋀s. ordered_list_it s = map_iterator_dom (map.iterateoi s)"
      unfolding ordered_list_it_def[abs_def] 
        map_iterator_dom_def set_iterator_image_alt_def map.iterateoi_def 
      by (simp add: S comp_def)
  
    from map_iterator_linord_dom_correct[OF map.iterateoi_correct[OF I']] 
    show "set_iterator_linord (ordered_list_it s) (α s)"
      unfolding α_def A .

    show "finite (α s)"
      unfolding α_def by (simp add: map.finite[OF I'])
  qed

  lemma rev_list_it_impl: "poly_set_rev_iterateoi α invar rev_list_it"
  proof
    fix s
    assume I: "invar s"
    hence I': "map.invar s" unfolding invar_def .

    have S: "⋀f. (λ(x,_). f x) = (λxy. f (fst xy))"
      by auto

    have A: "⋀s. rev_list_it s = map_iterator_dom (map.rev_iterateoi s)"
      unfolding rev_list_it_def[abs_def] 
        map_iterator_dom_def set_iterator_image_alt_def map.rev_iterateoi_def 
      by (simp add: S comp_def)
  
    from map_iterator_rev_linord_dom_correct[
      OF map.rev_iterateoi_correct[OF I']] 
    show "set_iterator_rev_linord (rev_list_it s) (α s)"
      unfolding α_def A .

    show "finite (α s)"
      unfolding α_def by (simp add: map.finite[OF I'])

  qed

  lemma dflt_basic_oops_impl: "StdBasicOSet dflt_basic_oops"
  proof -
    interpret aux: StdBasicSet dflt_basic_ops by (rule dflt_basic_ops_impl)

    show ?thesis
      apply (rule StdBasicOSet.intro)
      apply (rule StdBasicSet.intro)
      apply icf_locales
      apply (simp_all add: icf_rec_unf)
      apply (rule 
        ordered_list_it_impl[unfolded ordered_list_it_def[abs_def]] 
        rev_list_it_impl[unfolded rev_list_it_def[abs_def]]
      )+
      done
  qed
end

sublocale SetByMap < basic: StdBasicSet "dflt_basic_ops" 
  by (rule dflt_basic_ops_impl)

sublocale OSetByOMap < obasic: StdBasicOSet "dflt_basic_oops" 
  by (rule dflt_basic_oops_impl)

lemma proper_it'_map2set: "proper_it' it it' 
  ⟹ proper_it' (λs c f. it s c (f o fst)) (λs c f. it' s c (f o fst))"
  unfolding proper_it'_def
  apply clarsimp
  apply (drule_tac x=s in spec)
  apply (erule proper_itE)
  apply (rule proper_itI)
  apply (auto simp add: foldli_map[symmetric] intro!: ext)
  done


end