Theory Separation_Logic_Imperative_HOL.To_List_GA

section ‹Generic Algorithm to Convert Sets to Lists›
theory To_List_GA
imports Imp_Set_Spec Imp_List_Spec Hash_Set_Impl Open_List
begin
  text ‹This theory demonstrates how to develop a generic to-list 
    algorithm, and gives a sample instantiation for hash sets and open lists.
›

  subsection ‹Algorithm›
  partial_function (heap) to_list_ga_rec where [code]: 
    "to_list_ga_rec 
      it_has_next it_next 
      l_prepend
      it l 
    =
    do {
      b ← it_has_next it;
      if b then do {
        (x,it) ← it_next it;
        l ← l_prepend x l;
        to_list_ga_rec it_has_next it_next 
          l_prepend it l
      } else
        return l
    }
    "

  lemma to_list_ga_rec_rule:
    assumes "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes "imp_list_prepend is_list l_prepend"
    assumes FIN: "finite it"
    shows "
    < is_it s si it iti * is_list l li > 
      to_list_ga_rec it_has_next it_next l_prepend iti li
    < λr. ∃⇩Al'. is_set s si 
      * is_list l' r
      * ↑(set l' = set l ∪ it) >⇩t"
  proof -
    interpret imp_set_iterate is_set is_it it_init it_has_next it_next
      + imp_list_prepend is_list l_prepend
      by fact+

    from FIN show ?thesis
    proof (induction arbitrary: l li iti rule: finite_psubset_induct)
      case (psubset it)
      show ?case
        apply (subst to_list_ga_rec.simps)
        apply (sep_auto heap: psubset.IH)
        apply (rule ent_frame_fwd[OF quit_iteration])
        apply frame_inference
        apply solve_entails
        done
    qed
  qed

  definition "to_list_ga 
    it_init it_has_next it_next
    l_empty l_prepend s 
    ≡ do {
      it ← it_init s;
      l ← l_empty;
      l ← to_list_ga_rec it_has_next it_next l_prepend it l;
      return l
    }"

  lemma to_list_ga_rule:
    assumes IT: "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes EM: "imp_list_empty is_list l_empty"
    assumes PREP: "imp_list_prepend is_list l_prepend"
    assumes FIN: "finite s"
    shows "
    <is_set s si>
    to_list_ga it_init it_has_next it_next
      l_empty l_prepend si
    <λr. ∃⇩Al. is_set s si * is_list l r * true * ↑(set l = s)>"
  proof -
    interpret imp_list_empty is_list l_empty +
      imp_set_iterate is_set is_it it_init it_has_next it_next
      by fact+

    note [sep_heap_rules] = to_list_ga_rec_rule[OF IT PREP]
    show ?thesis
      unfolding to_list_ga_def
      by (sep_auto simp: FIN)
  qed

  subsection ‹Sample Instantiation for hash set and open list›
  definition "hs_to_ol 
    ≡ to_list_ga hs_it_init hs_it_has_next hs_it_next
        os_empty os_prepend"
  
  lemmas hs_to_ol_rule[sep_heap_rules] =
    to_list_ga_rule[OF hs_iterate_impl os_empty_impl os_prepend_impl,
    folded hs_to_ol_def] 


  export_code hs_to_ol checking SML_imp

end