Theory IICF_List_Set

theory IICF_List_Set
  imports "SepLogicTime_RBTreeBasic.LinkedList" 
      "../Intf/IICF_Set"  "../../../RefineMonadicVCG"
begin
 

subsection "library for some set implementation via linked list"
 

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

definition list_set_assn :: "_ set ⇒ _ os_list ⇒ assn"  where
  "list_set_assn S p =
        (∃⇩AL. os_list L p * ↑(distinct L ∧ S = set L))"


subsubsection "empty set init"
term os_empty
thm os_empty_rule
definition "list_set_empty = os_empty" 

lemma list_set_empty_rule: "<$ 1> list_set_empty <list_set_assn {}>"
  unfolding list_set_assn_def list_set_empty_def
  by(sep_auto heap: os_empty_rule simp: zero_time)


lemma mop_set_empty_rule[sepref_fr_rules]:
  "(uncurry0 list_set_empty, uncurry0 (PR_CONST (mop_set_empty t)))
     ∈ [λ_. 1 ≤ t]⇩a unit_assn⇧k → list_set_assn"
  apply sepref_to_hoare
  unfolding autoref_tag_defs mop_set_empty_def 
  apply (rule extract_cost_otherway'[OF _ list_set_empty_rule])
    apply (  solve_entails )
   apply (  solve_entails )  by (auto simp: ran_emb')   


subsubsection "pick element"

term os_pop
thm os_pop_rule
definition "list_set_pick_extract = os_pop" 
 
lemma Case_rule[sep_decon_rules]: "(c = None ⟹ <P> f <Q>) ⟹ (⋀b. c = Some b ⟹ <P> g b <Q>) ⟹ <P> case c of None ⇒ f | Some b ⇒ g b <Q>"
  by (auto split: option.splits) 

lemma raise_rule: "P ⟹⇩A false ⟹ <P> raise msg <Q>"
  by (simp add: hoare_triple_def)

lemma return_rule':
  "<$1> return x <λr. ↑(r = x)>" by auto2 

lemma list_set_pick_extract_rule :
  "S ≠ {} ⟹ <list_set_assn S p * $2>
   list_set_pick_extract p
   <λ(x,r'). list_set_assn (S-{x}) r' * ↑(x ∈ S)>⇩t"
  unfolding list_set_assn_def list_set_pick_extract_def os_pop_def
  apply(sep_auto heap: raise_rule) 
  subgoal  
    by (metis hd_Cons_tl mod_false' os_list.simps(3))
  subgoal for L apply (cases L) apply simp by simp
  subgoal for L pa
    apply (cases L) apply simp
    by(sep_auto heap: ref_rule return_rule' lookup_rule) 
  done
 

lemma mop_set_pick_extract_rule[sepref_fr_rules]:
  "(list_set_pick_extract, PR_CONST (mop_set_pick_extract t))
     ∈ [λx. 2 ≤ t x]⇩a list_set_assn⇧d → id_assn ×⇩a list_set_assn"
  apply sepref_to_hoare
  unfolding autoref_tag_defs mop_set_pick_extract_def
  apply(rule hnr_ASSERT)
  apply (rule extract_cost_otherway'[OF _ list_set_pick_extract_rule])
  apply (  solve_entails ) apply simp
  apply (case_tac r) 
   apply (  solve_entails )  defer apply(subst prod_assn_pair_conv) 
  apply (  solve_entails ) by (auto simp: ran_emb')   



subsubsection "insert new element"

term os_prepend

thm os_prepend_rule

definition "list_set_insert k b = os_prepend k b"

lemma list_set_insert_rule:
  "x∉S ⟹ <list_set_assn S n * $2> list_set_insert x n <list_set_assn (insert x S)>" 
  unfolding list_set_insert_def list_set_assn_def
  by (sep_auto heap: os_prepend_rule) 
 
lemma mop_set_insert_rule[sepref_fr_rules]:
  "(uncurry list_set_insert, uncurry (PR_CONST (mop_set_insert t)))
     ∈ [λ(a, b). 2 ≤ t b ∧ a∉b]⇩a id_assn⇧k *⇩a list_set_assn⇧d → list_set_assn"
  apply sepref_to_hoare
  unfolding autoref_tag_defs mop_set_insert_def
  apply (rule extract_cost_otherway'[OF _ list_set_insert_rule])
  apply solve_entails apply auto
  by solve_entails   




subsubsection "test emptiness"

term os_is_empty
thm os_is_empty_rule
definition "list_set_isempty = os_is_empty" 

lemma list_set_isempty_rule:
  "<list_set_assn S p * $ 1> list_set_isempty p <λr. list_set_assn S p * ↑ (r = (S = {}))>"
  unfolding list_set_isempty_def list_set_assn_def
  by(sep_auto heap: os_is_empty_rule simp: zero_time)

lemma mop_set_isempty_rule[sepref_fr_rules]:
    "(list_set_isempty, PR_CONST (mop_set_isempty t))
   ∈ [λS. 1 ≤ t S]⇩a list_set_assn⇧k → bool_assn"
  apply sepref_to_hoare
  unfolding autoref_tag_defs mop_set_isempty_def 
  apply (rule extract_cost_otherway'[OF _ list_set_isempty_rule])  
  apply solve_entails apply auto
  by solve_entails   
    
  
hide_type LinkedList.node 

end