Theory Separation_Logic_Imperative_HOL.Imp_Set_Spec

section ‹Interface for Sets›
theory Imp_Set_Spec
imports "../Sep_Main"
begin
text ‹
  This file specifies an abstract interface for set data structures. It can
  be implemented by concrete set data structures, as demonstrated in the 
  hash set example.
›

locale imp_set =
  fixes is_set :: "'a set  's  assn"
  assumes precise: "precise is_set"

locale imp_set_empty = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes empty :: "'s Heap"
  assumes empty_rule[sep_heap_rules]: "<emp> empty <is_set {}>t"

locale imp_set_is_empty = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes is_empty :: "'s  bool Heap"
  assumes is_empty_rule[sep_heap_rules]: 
    "<is_set s p> is_empty p <λr. is_set s p * (r  s={})>t"

locale imp_set_memb = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes memb :: "'a  's  bool Heap"
  assumes memb_rule[sep_heap_rules]: 
    "<is_set s p> memb a p <λr. is_set s p * (r  a  s)>t"

locale imp_set_ins = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes ins :: "'a  's  's Heap"
  assumes ins_rule[sep_heap_rules]: 
    "<is_set s p> ins a p <is_set (Set.insert a s)>t"
    
locale imp_set_delete = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes delete :: "'a  's  's Heap"
  assumes delete_rule[sep_heap_rules]: 
    "<is_set s p> delete a p <is_set (s - {a})>t"

locale imp_set_size = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes size :: "'s  nat Heap"
  assumes size_rule[sep_heap_rules]: 
    "<is_set s p> size p <λr. is_set s p * (r = card s)>t"

locale imp_set_iterate = imp_set +
  constrains is_set :: "'a set  's  assn"
  fixes is_it :: "'a set  's  'a set  'it  assn"
  fixes it_init :: "'s  ('it) Heap"
  fixes it_has_next :: "'it  bool Heap"
  fixes it_next :: "'it  ('a×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_set s p> it_init p <is_it s p s>t"
  assumes it_next_rule[sep_heap_rules]: "s'{}  
    <is_it s p s' it> 
      it_next it 
    <λ(a,it'). is_it s p (s' - {a}) it' * (a  s')>t"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it s p s' it> it_has_next it <λr. is_it s p s' it * (rs'{})>t"
  assumes quit_iteration:
    "is_it s p s' it A is_set s p * true"


locale imp_set_union = imp_set_iterate +
  fixes union :: "'s  's  's Heap"
  assumes union_rule[sep_heap_rules]: 
    "finite se  <(is_set s p) * (is_set se q)> union p q <λr.  
    As'. is_set s' r * (is_set se q)* true *   (s' = s  se)>"

(* TODO: Move Generic implementation*)

partial_function (heap) set_it_union
  where [code]: "set_it_union 
    it_has_next it_next set_ins it a = do {
      co  it_has_next it;
      if co then do {
        (x,it')  it_next it;
        insx <- set_ins x a;
        set_it_union it_has_next it_next set_ins it' (insx) 
      } else return a
    }"



lemma set_it_union_rule:
    assumes "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes "imp_set_ins is_set set_ins"
    assumes FIN: "finite it"
    shows "
    < is_it b q it iti * is_set a p> 
      set_it_union it_has_next it_next set_ins iti p 
    < λr. As'. is_set s' r *  is_set b q  * true *  (s' = a  it) >"
  proof -
    interpret imp_set_iterate is_set is_it it_init it_has_next it_next
        + imp_set_ins is_set set_ins
      by fact+

    from FIN show ?thesis
    proof (induction  arbitrary: a p iti rule: finite_psubset_induct)
      case (psubset it)
      show ?case
        apply (subst set_it_union.simps)
        using imp_set_iterate_axioms
        apply (sep_auto heap: psubset.IH)
        by (metis ent_refl_true ent_star_mono_true quit_iteration star_aci(2))
    qed
  qed


definition union_loop_ins  where 
"union_loop_ins it_init it_has_next it_next set_ins a b  do { 
    it <- (it_init b);
    set_it_union it_has_next it_next set_ins it a
    }"



lemma set_union_rule:
    assumes IT: "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes INS: "imp_set_ins is_set set_ins"
    assumes finb: "finite b"
    shows "
    <is_set a p * is_set b q>
   union_loop_ins it_init  it_has_next it_next set_ins p q
    <λr.  As'. is_set s' r * true * is_set b q *  (s' = a  b)>"
  proof -
    interpret 
      imp_set_iterate is_set is_it it_init it_has_next it_next
        + imp_set_ins is_set set_ins
      by fact+

    note it_aux[sep_heap_rules] = set_it_union_rule[OF IT INS finb]
    show ?thesis
      unfolding union_loop_ins_def
       apply (sep_auto)
      done
  qed


end