Theory IICF_Rbt_Set

theory IICF_Rbt_Set
  imports "SepLogicTime_RBTreeBasic.RBTree_Impl" 
      "../Intf/IICF_Set"  "../../../RefineMonadicVCG" "../../Sepref"
begin

hide_const R B

subsection "library for some set implementation"


subsubsection "interface"
 




term rbt_map_assn
thm rbt_search rbt_insert_rule


definition Z :: "(('a, unit) Mapping_Str.map × 'a set) set"
  where "Z = {(c,a)|c a. keys_of c = a}"

subsubsection "empty set init via rbtree"

definition set_init_t :: "nat" where "set_init_t = 1"

definition set_init_SPEC :: "nat set nrest" where
  "set_init_SPEC ≡ SPECT [{} ↦ set_init_t ]"

definition rbt_map_assn' where "rbt_map_assn' a c =
        (∃⇩AM. rbt_map_assn M c * ↑((M,a)∈Z))"

definition rbt_set_assn :: "_ set ⇒ (_, unit) rbt_node ref option ⇒ assn"  where [rewrite_ent]:
  "rbt_set_assn S p =
        (∃⇩AM. rbt_map_assn M p * ↑(S = keys_of M))"

definition [rewrite]: "rbt_set_insert k b = rbt_insert k () b"

lemma g[rewrite]: "card (keys_of M) + 1 = sizeM1 M"
     by (auto simp: sizeM1_def)


definition rbt_pick where   "rbt_pick p = do {(case p of 
     None ⇒ return None |
     Some pp ⇒ do {
     t ← !pp;
     return (Some (key t))
   }) }"

lemma rbt_pick_rule [hoare_triple]:
  "<btree t p *$2>
   rbt_pick  p
   <λr. btree t p * ↑( (t = Leaf ⟶ r = None) ∧ (t≠Leaf ⟶ the r ∈ rbt_set t) )>⇩t"
@proof @case "t = Leaf"  @qed

definition  rbt_map_pick where    "rbt_map_pick p = rbt_pick p"

lemma rbt_map_Leaf: "rbt_map (Leaf) = empty_map"
  by (simp add: rbt_map_def)

lemma neq_ext: "(∃x. f x ≠  g x ) ⟹ f ≠ g" by auto


lemma meval_ext_neg: " M⟨x⟩ ≠ N⟨x⟩ ⟹ M ≠ N"
  apply (cases M) apply (cases N) by auto
 
  


lemma rbt_map_Leaf_conv: "M = rbt_map t ⟹ (t = Leaf) = (M = empty_map)"
  apply(cases t) apply (simp_all add: rbt_map_def empty_map_def) 
  subgoal for c l k v r apply(rule meval_ext_neg[where x=k])
    apply(simp only:  meval.simps)
    apply(simp only: map_of_alist_nil'[symmetric]) by simp 
  done

lemma empty_rbt_map_is_Leaf: "rbt_map t = empty_map ⟹ t = Leaf"
  by(simp add: rbt_map_Leaf_conv)

lemma rbt_map_Leaf_is_empty_map: "rbt_map Leaf = empty_map "
  by(simp add: rbt_map_def)

lemma dd: "M= rbt_map t ⟹ t = Leaf ⟹ M = empty_map"
  by(simp add: rbt_map_def)

declare rbt_set_keys_of [forward]

lemma rbt_map_pick_rule [hoare_triple]:
  "<rbt_map_assn M p * $ 2>
   rbt_map_pick  p
   <λr. rbt_map_assn M p * ↑( (M = empty_map ⟶ r = None) ∧ (M≠empty_map ⟶ the r ∈ keys_of M))>⇩t"
  by auto2



thm tree_is_empty_rule
declare tree_is_empty_rule [hoare_triple]

definition "rbt_map_isempty b = tree_is_empty b"
 

lemma rbt_map_isempty_rule[hoare_triple]: "<rbt_map_assn M b * $1> rbt_map_isempty b <λr. rbt_map_assn M b * ↑ (r ⟷ (M = empty_map))>⇩t"
  by auto2

setup {* fold del_prfstep_thm @{thms rbt_map_assn_def} *}   




definition  rbt_set_pick where    "rbt_set_pick p = do {
        s ← rbt_map_pick p;
        return (the s) }"

 
theorem rbt_set_pick_rule [hoare_triple]:
  "S≠{} ⟹ <rbt_set_assn S b * $4> rbt_set_pick b <λr. rbt_set_assn S b * ↑(r ∈ S)>⇩t"
  by auto2

definition  rbt_set_isempty where    "rbt_set_isempty p =rbt_map_isempty p"

lemma rbt_set_isempty_rule: "<rbt_set_assn S b * $1> rbt_set_isempty b <λr. rbt_set_assn S b * ↑ (r ⟷ (S = {}))>⇩t"
  by auto2


declare [[print_trace]]
thm rbt_insert_rule rbt_insert_rule'
theorem rbt_insert_rule_abs [hoare_triple]:
  "<rbt_set_assn S p * $(rbt_insert_logN (card S + 1))> rbt_set_insert x p <rbt_set_assn (insert x S)>⇩t"
  by auto2 

lemma a[rewrite]: "S = keys_of M ⟹ M⟨x⟩ = Some () ⟷ x ∈ S"  
  by (simp add: keys_of_iff)  



definition [rewrite]: "rbt_set_delete b k = rbt_delete k  b"

theorem rbt_delete_rule_abs [hoare_triple]:
  "<rbt_set_assn S p * $(rbt_delete_time_logN (card S + 1))> rbt_set_delete p x <rbt_set_assn (S -  {x})>⇩t"
  by auto2 

thm rbt_delete_rule


(*
theorem rbt_search_abs [hoare_triple]:
  "<rbt_set_assn S b * $(rbt_search_time_logN (card S + 1))> rbt_search x b <λr. rbt_set_assn S b * ↑(r = Some () ⟷ x ∈ S)>⇩t"
  by auto2
*)

definition rbt_mem :: "'a::{heap,linorder} ⇒ ('a, unit) rbt_node ref option ⇒ bool Heap" where [rewrite]:
  "rbt_mem x p = do {
      f ← rbt_search x p;
      return (f = Some ()) }"

     
theorem rbt_mem_rule [hoare_triple]:
  "<rbt_set_assn S b * $(rbt_search_time_logN (card S + 1) + 1)> rbt_mem x b <λr. rbt_set_assn S b * ↑(r = (x ∈ S))>⇩t"
  by auto2



definition paint :: "color ⇒ ('a::heap, 'b::heap) btree ⇒ unit Heap" where
  "paint c p = (case p of
    None ⇒ return ()
  | Some pp ⇒ do {
     t ← !pp;
     pp := Node (lsub t) c (key t) (val t) (rsub t)
   })"
  
lemma paint_rule [hoare_triple]:
  "<btree t p *$2>
   paint c p
   <λ_. btree (RBTree.paint c t) p>⇩t"
@proof @case "t = Leaf" @qed


definition "set_empty = tree_empty"

theorem set_empty_rule [hoare_triple]:
  "<$1> set_empty <rbt_set_assn {}>" by auto2
 

lemma keys_of_empty_Map_empty: "{} = keys_of M ⟷ M=Map Map.empty"
  by(auto simp: keys_of_def meval_ext )   


lemma inst_ex_assn: "A ⟹⇩A B x ⟹ A ⟹⇩A (∃⇩Ax. B x)"
  using entails_ex_post by blast 

lemma norm_ex_assn: "A ⟹⇩A (∃⇩Ax. B x * C)  ⟹ A ⟹⇩A (∃⇩Ax. B x) * C"
  by (simp)

lemma fl': "(b ⟹ A ⟹⇩A B) ⟹  ↑b *  A  ⟹⇩A B"  
  by (simp add: assn_times_comm entails_def)

lemma fl: "A ⟹⇩A B ⟹ b ⟹ A ⟹⇩A B * ↑b"  
  using entails_pure_post by blast  
lemma fl_: "A ⟹⇩A B ⟹ b ⟹ A ⟹⇩A ↑b * B "  
  using fl assn_times_comm  by simp

lemma set_init_hnr'_short:
  "hn_refine (emp) set_empty emp rbt_set_assn (set_init_SPEC)"
  unfolding set_init_SPEC_def
  apply (rule extract_cost_otherway[OF _ set_empty_rule, where Cost_lb=1 and F=emp])
  apply simp  
  subgoal 
    apply(rule ent_true_drop(2))
    by (auto intro!: inst_ex_assn fl entails_triv simp:   rbt_map_assn'_def )  
   by (auto intro: entails_triv simp: set_init_t_def)


lemma set_init_hnr':
  "hn_refine (emp) tree_empty emp rbt_map_assn' (set_init_SPEC)"
proof -
  from rbt_empty_rule[unfolded hoare_triple_def]
  have A: "⋀h as σ r n t.
     pHeap h as n ⊨ $ 1 ⟹
     run tree_empty (Some h) σ r t ⟹
     σ ≠ None ∧
     pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ rbt_map_assn empty_map r ∧
     t ≤ n ∧ relH {a. a < heap.lim h ∧ a ∉ as} h (the σ) ∧ heap.lim h ≤ heap.lim (the σ)" by blast

  thm entailsD
    
  show ?thesis unfolding hn_refine_def  set_init_SPEC_def set_init_t_def rbt_map_assn'_def
    apply auto
  proof (goal_cases)
    case (1 h as n)
    then have "pHeap h as (n + 1) ⊨ emp * $ 1"
      using diff_add_inverse2 le_add2 mod_timeCredit_dest by presburger 
    then have ph: "pHeap h as (n + 1) ⊨ $ 1" by simp

    note A[OF ph] run_and_execute
    have
      "(∃h' t r. execute tree_empty h = Some (r, h', t) ∧ (pHeap h' (new_addrs h as h') (n + 1 - t) ⊨ rbt_map_assn empty_map r ∧
    t ≤ n + 1 ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h'))" apply(simp only: run_and_execute[symmetric])
      using  A[OF ph]  by blast
    then obtain h' t and r:: "(nat, unit) rbt_node ref option" where
        heap: "pHeap h' (new_addrs h as h') (n + 1 - t) ⊨ rbt_map_assn empty_map r"
     and   "execute tree_empty h = Some (r, h', t)" 
                "t ≤ n + 1" " relH {a. a < heap.lim h ∧ a ∉ as} h h'" "heap.lim h ≤ heap.lim h'" by blast
    from heap have heap': "pHeap h' (new_addrs h as h') (Suc n - t) ⊨ rbt_map_assn empty_map r" by simp
    show ?case apply(rule exI[where x=h'])  apply(rule exI[where x=t])   apply(rule exI[where x=r]) 
      apply safe
      apply fact
        apply (rule exI[where x=1]) apply safe apply simp apply fact
      subgoal apply(auto simp: keys_of_empty_Map_empty empty_map_def Z_def) apply(rule entailsD[OF _ heap'])  
        unfolding empty_map_def 
        by (smt entails_def entails_ex_post entails_frame'' entails_true match_rest one_assn_rule pure_assn_rule)    
      apply fact
      apply fact
      done
  qed
qed

subsubsection "set insertion via rbtree"

definition set_ins_t :: "nat⇒nat" where "set_ins_t n = rbt_insert_logN (n+1)"

definition set_ins_SPEC where
  "set_ins_SPEC x S ≡ SPECT [insert x S ↦ set_ins_t (card S)]"

lemma ent_ex: "(⋀x. P x ⟹⇩A Q) ⟹ (∃⇩Ax. P x) ⟹⇩A Q"
  by (meson entails_ex) 


lemma isolate_first: "⋀A B C. Γ ⟹⇩A Γ' ⟹ A ⟹⇩A B ⟹ Γ * A ⟹⇩A Γ' * B"  
  by (simp add: ent_star_mono)  

lemma inZ_conv: "(M, S) ∈ Z ⟷ (S = keys_of M)" unfolding Z_def by auto


lemma set_ins_hnr_abs:
  "hn_refine (rbt_set_assn S p * hn_val Id x x') (rbt_set_insert x' p) (hn_val Id x x') rbt_set_assn (set_ins_SPEC x S)"

  unfolding set_ins_SPEC_def
  apply (rule extract_cost_otherway[OF _  rbt_insert_rule_abs ]) unfolding mult.assoc
    apply(rule match_first)
    apply rotatel apply(rule match_first) apply (rule entails_triv)

   apply rotatel apply rotatel apply takel apply taker apply(rule isolate_first)
  unfolding gr_def apply(simp only: ex_distrib_star')
    apply(rule inst_ex_assn)
    apply rotater unfolding hn_ctxt_def pure_def 
    apply(rule fl') apply (simp ) apply safe
  prefer 4  apply(rule entails_triv) 
  by (auto simp: set_ins_t_def) 

subsubsection "set membership via rbtree"

fun set_mem_t :: "nat⇒nat" where "set_mem_t n = rbt_search_time_logN (n + 1)"

definition set_mem_SPEC :: "'a ⇒ 'a set ⇒ bool nrest" where
  "set_mem_SPEC x S ≡ SPECT [ (x ∈ S) ↦ set_mem_t (card S)]"

definition Y :: "(unit option × bool) set" where
    "Y = {(c,a)|c a. c = Some () ⟷ a}"

definition Y' :: "bool ⇒ unit option ⇒ assn" where
  "Y' b v = ↑(  v = Some () ⟷ b )"
 
(* theorems that should be visible from the outside *)

(* init *)
thm set_init_hnr'_short set_init_SPEC_def
             
(* insert *)
thm set_ins_hnr_abs set_ins_SPEC_def

(* membership test *)
(* thm set_mem_hnr_abs set_mem_SPEC_def *)

subsubsection "implement the interface"

lemma mop_set_empty_rule[sepref_fr_rules]:
  "1≤n ⟹ hn_refine (emp) set_empty emp rbt_set_assn (PR_CONST (mop_set_empty n))"

  unfolding autoref_tag_defs mop_set_empty_def  
  apply (rule extract_cost_otherway[OF _ set_empty_rule, where Cost_lb=1 and F=emp])
  apply simp  
  subgoal 
    apply(rule ent_true_drop(2))
    by (auto intro!: inst_ex_assn fl entails_triv simp:   rbt_map_assn'_def )  
   by (auto intro: entails_triv simp: set_init_t_def)


lemma mop_set_insert_rule[sepref_fr_rules]:
  "rbt_insert_logN (card S + 1) ≤ t S ⟹ 
      hn_refine (hn_val Id x x' * hn_ctxt rbt_set_assn S p)
       (rbt_set_insert x' p)
       (hn_val Id x x' * hn_invalid rbt_set_assn S p) rbt_set_assn ( PR_CONST (mop_set_insert t) $ x $ S)"

  unfolding mop_set_insert_def autoref_tag_defs
  apply (rule extract_cost_otherway[OF _  rbt_insert_rule_abs, where F="hn_val Id x x' * hn_invalid rbt_set_assn S p" ])
  unfolding mult.assoc
    apply(rotatel)
    apply rotater  apply rotater  apply rotater   apply taker apply(rule isolate_first)
  apply (simp add: gr_def hn_ctxt_def)  apply(rule invalidate_clone)
  unfolding hn_ctxt_def
    apply(rule match_first)  apply (rule entails_triv)

   apply rotatel apply rotatel apply swapl apply takel apply swapr apply taker 
   apply(rule isolate_first) 
  unfolding gr_def apply(simp only: ex_distrib_star' pure_def)
    apply(rule inst_ex_assn) apply simp apply safe prefer 4 
     apply(rule entails_triv) 
  by (auto) 


lemma mop_set_delete_rule[sepref_fr_rules]:
  "rbt_delete_time_logN (card S + 1) ≤ t S ⟹ 
      hn_refine (hn_val Id x x' * hn_ctxt rbt_set_assn S p)
       (rbt_set_delete p x')
       (hn_val Id x x' * hn_invalid rbt_set_assn S p) rbt_set_assn ( PR_CONST (mop_set_del t) $ S $ x)"

  unfolding mop_set_del_def autoref_tag_defs
  apply (rule extract_cost_otherway[OF _  rbt_delete_rule_abs, where F="hn_val Id x x' * hn_invalid rbt_set_assn S p" ])
  unfolding mult.assoc
    apply(rotatel)
    apply rotater  apply rotater  apply rotater   apply taker apply(rule isolate_first)
  apply (simp add: gr_def hn_ctxt_def)  apply(rule invalidate_clone)
  unfolding hn_ctxt_def
    apply(rule match_first)  apply (rule entails_triv)

   apply rotatel apply rotatel apply swapl apply takel apply swapr apply taker 
   apply(rule isolate_first) 
  unfolding gr_def apply(simp only: ex_distrib_star' pure_def)
    apply(rule inst_ex_assn) apply simp apply safe prefer 4 
     apply(rule entails_triv) 
  by (auto) 



lemma mop_mem_set_rule[sepref_fr_rules]:
  "rbt_search_time_logN (card S + 1) + 1 ≤ t S ⟹
    hn_refine (hn_val Id x x' * hn_ctxt rbt_set_assn S p)
     (rbt_mem (x') p)
     (hn_ctxt (pure Id) x x' * hn_ctxt rbt_set_assn S p) id_assn ( PR_CONST (mop_set_member t) $  x $ S)"

  unfolding autoref_tag_defs mop_set_member_def
  apply (rule extract_cost_otherway[OF _  rbt_mem_rule]) unfolding mult.assoc
  unfolding hn_ctxt_def
    apply rotatel apply(rule match_first) apply(rule match_first)       
   apply (rule entails_triv)
  apply rotater
   apply(rule match_first) apply (simp add: pure_def)   apply safe
    apply(rule inst_ex_assn[where x="x ∈ S"])  by auto 


thm rbt_set_isempty_rule


lemma mop_set_isempty_rule[sepref_fr_rules]:
  "1 ≤ t S ⟹
    hn_refine (hn_ctxt rbt_set_assn S p)
     (rbt_set_isempty  p)
     (hn_ctxt rbt_set_assn S p) id_assn ( PR_CONST (mop_set_isempty t) $ S)"

  unfolding autoref_tag_defs mop_set_isempty_def             
  apply (rule extract_cost_otherway[OF _  rbt_set_isempty_rule, where F="emp" ]) unfolding mult.assoc
  unfolding hn_ctxt_def  apply(rule match_first) apply simp      
     apply (rule entails_triv)
   apply(rule match_first)   apply clarsimp   
   apply (simp add: pure_def)    
    apply(rule inst_ex_assn[where x="S = {}"]) apply (simp add: dom_emb'_eq)
  by (auto split: if_splits simp add: ran_def emb'_def)



lemma mop_set_pick_rule[sepref_fr_rules]:
  "4 ≤ t S ⟹
    hn_refine (hn_ctxt rbt_set_assn S p)
     (rbt_set_pick  p)
     (hn_ctxt rbt_set_assn S p) id_assn ( PR_CONST (mop_set_pick t) $ S)"

  unfolding autoref_tag_defs mop_set_pick_def
  apply(rule hnr_ASSERT)
  apply (rule extract_cost_otherway[OF _  rbt_set_pick_rule, where F = emp]) unfolding mult.assoc
  unfolding hn_ctxt_def  apply(rule match_first) apply simp      
     apply (rule entails_triv)
  apply simp 
   apply(rule match_first) apply clarsimp
   
   apply (simp add: pure_def)   subgoal for r
    apply(rule inst_ex_assn[where x="r"]) by (simp add: dom_emb'_eq)
  by (auto split: if_splits simp add: ran_def emb'_def)

thm mop_set_pick_rule[to_hfref]

lemma "(rbt_set_pick, PR_CONST (mop_set_pick t)) ∈ [λS. 4 ≤ t S]⇩a rbt_set_assn⇧k → id_assn"
  apply sepref_to_hoare
  unfolding autoref_tag_defs mop_set_pick_def
  apply(rule hnr_ASSERT)
  apply (rule extract_cost_otherway'[OF _ rbt_set_pick_rule])
     apply solve_entails apply auto[]
  oops
  


definition "rbt_set_pick_extract S = do { v ← mop_set_pick (λ_. 4) S;
                              C ← mop_set_del (λS. rbt_delete_time_logN (card S + 1)) S v;
                              RETURNT (v,C) }"

lemma rbt_set_pick_extract_refines: "rbt_delete_time_logN (card S + 1) + 4 ≤ t S ⟹ rbt_set_pick_extract S ≤ mop_set_pick_extract t S"
  unfolding mop_set_pick_extract_def rbt_set_pick_extract_def mop_set_pick_def mop_set_del_def
  apply(rule le_ASSERTI)
  apply(rule T_specifies_I)
  by (vcg' ‹simp add: Some_le_emb'_conv›)

lemma rbt_set_pick_extract_refines': "(rbt_set_pick_extract, PR_CONST (mop_set_pick_extract t)) ∈ [λS. rbt_delete_time_logN (card S + 1) + 4 ≤ t S]⇩f Id → ⟨Id⟩nrest_rel"
  apply(rule frefI)
  apply(rule nrest_relI) using rbt_set_pick_extract_refines by auto

schematic_goal mop_set_pick_extract_rule':
      notes [id_rules] = 
        itypeI[Pure.of S "TYPE('a set)"] 
      shows
  "hn_refine (hn_ctxt rbt_set_assn S p) (?c::?'c Heap) ?Γ' ?R (rbt_set_pick_extract S)"
  unfolding rbt_set_pick_extract_def
  apply sepref done

concrete_definition (in -) set_pick_extract uses mop_set_pick_extract_rule'
print_theorems

    sepref_register "set_pick_extract " 
 

lemmas kruskal_ref_spec[sepref_fr_rules] = set_pick_extract.refine[FCOMP rbt_set_pick_extract_refines']
 




end