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 * ↑(r⟷s'≠{})>⇩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