Theory Collections.ListSetImpl

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section ‹\isaheader{Set Implementation by List}›
theory ListSetImpl
imports "../spec/SetSpec" "../gen_algo/SetGA" "../../Lib/Dlist_add"
begin
text_raw ‹\label{thy:ListSetImpl}›

(*@impl Set
  @type 'a ls
  @abbrv ls,l
  Sets implemented by distinct lists. For efficient 
  @{text "insert_dj"}-operations, use the version with explicit invariant (lsi).
*)

type_synonym
  'a ls = "'a dlist"

subsection "Definitions"

definition ls_α :: "'a ls ⇒ 'a set" where "ls_α l == set (list_of_dlist l)"

definition ls_basic_ops :: "('a,'a ls) set_basic_ops" where
  [icf_rec_def]: "ls_basic_ops ≡ ⦇
    bset_op_α = ls_α,
    bset_op_invar = λ_. True,
    bset_op_empty = λ_. Dlist.empty,
    bset_op_memb = (λx s. Dlist.member s x),
    bset_op_ins = Dlist.insert,
    bset_op_ins_dj = Dlist.insert,
    bset_op_delete = dlist_remove',
    bset_op_list_it = dlist_iteratei
    ⦈"

setup Locale_Code.open_block
interpretation ls_basic: StdBasicSet ls_basic_ops
  apply unfold_locales
  unfolding ls_basic_ops_def ls_α_def[abs_def]
  apply (auto simp: dlist_member_empty Dlist.member_def List.member_def
    dlist_iteratei_correct
    dlist_remove'_correct set_dlist_remove1'
  )
  done
setup Locale_Code.close_block

definition [icf_rec_def]: "ls_ops ≡ ls_basic.dflt_ops⦇ 
  set_op_to_list := list_of_dlist
  ⦈"

setup Locale_Code.open_block
interpretation ls: StdSetDefs ls_ops .
interpretation ls: StdSet ls_ops
proof -
  interpret aux: StdSet ls_basic.dflt_ops
    by (rule ls_basic.dflt_ops_impl)

  show "StdSet ls_ops"
    unfolding ls_ops_def
    apply (rule StdSet_intro)
    apply icf_locales
    apply (simp_all add: icf_rec_unf)
    apply (unfold_locales)
    apply (simp_all add: ls_α_def)
    done
qed

interpretation ls: StdSet_no_invar ls_ops
  by unfold_locales (simp add: icf_rec_unf)
setup Locale_Code.close_block

setup ‹ICF_Tools.revert_abbrevs "ls"›

lemma pi_ls[proper_it]:
  "proper_it' dlist_iteratei dlist_iteratei"
  apply (rule proper_it'I)
  unfolding dlist_iteratei_def
  by (intro icf_proper_iteratorI)

lemma pi_ls'[proper_it]: 
  "proper_it' ls.iteratei ls.iteratei"
  apply (rule proper_it'I)
  unfolding ls.iteratei_def
  by (intro icf_proper_iteratorI)

interpretation pi_ls: proper_it_loc dlist_iteratei dlist_iteratei
  apply unfold_locales by (rule pi_ls)

interpretation pi_ls': proper_it_loc ls.iteratei ls.iteratei
  apply unfold_locales by (rule pi_ls')

definition test_codegen where "test_codegen ≡ (
  ls.empty,
  ls.memb,
  ls.ins,
  ls.delete,
  ls.list_it,
  ls.sng,
  ls.isEmpty,
  ls.isSng,
  ls.ball,
  ls.bex,
  ls.size,
  ls.size_abort,
  ls.union,
  ls.union_dj,
  ls.diff,
  ls.filter,
  ls.inter,
  ls.subset,
  ls.equal,
  ls.disjoint,
  ls.disjoint_witness,
  ls.sel,
  ls.to_list,
  ls.from_list
)"

export_code test_codegen checking SML

end