Theory Stack_Set

theory Stack_Set
  imports Stack 
begin

context 
  notes [simp] = IS_LEFT_UNIQUE_def (* Argh, the set parametricity lemmas use single_valued (K¯) here. *)
begin

  sepref_decl_op set_select: "(λs. SPEC (λ(x,s'). x ∈ s ∧ s' = s - {x}))" 
    :: "[λs. s≠{}]⇩f ⟨K⟩set_rel → K ×⇩r ⟨K⟩set_rel" where "IS_LEFT_UNIQUE K" "IS_RIGHT_UNIQUE K"  
    subgoal 
      apply rule
      apply (rule nres_relI)
      apply (rule RES_refine)
      apply clarsimp
    proof goal_cases
      case (1 x y a)
      then obtain aa where A: "aa ∈ y" "(a, aa) ∈ K" by (auto simp: set_rel_def)
      with 1 have B: "(x - {a}, y - {aa}) ∈ ⟨K⟩set_rel"
        by parametricity
      from A B show ?case by blast
    qed  
    subgoal by auto 
    done

end

  definition "stack_set_rel = br set distinct"

  lemma stack_set_rel_alt: "stack_set_rel = ⟨Id⟩list_set_rel"
    unfolding stack_set_rel_def list_set_rel_def by simp

  lemma "([],{}) ∈ stack_set_rel"
    by(auto simp: in_br_conv stack_set_rel_def)

  lemma list_set_is_empty_refine: "(mop_list_is_empty, mop_set_is_empty) ∈ stack_set_rel → ⟨bool_rel⟩nres_rel"
    by(auto simp: in_br_conv stack_set_rel_def intro!: nres_relI)

  lemma neq_Nil_conv_rev: "(xs ≠ []) = (∃y ys. xs = ys @ [y])"
    apply(cases xs rule: rev_cases)
    by auto

  lemma list_set_pop_refine: "(mop_list_pop_last, mop_set_select) ∈ stack_set_rel → ⟨Id ×⇩r stack_set_rel⟩nres_rel"
    apply (auto simp add: in_br_conv refine_pw_simps pw_nres_rel_iff neq_Nil_conv_rev stack_set_rel_def)
    done

  definition "stack_set_assn A = hr_comp (stack_assn A) (stack_set_rel)"
  abbreviation "stack_set_assn' TYPE('l::len2) ≡ stack_set_assn :: _ ⇒ _ ⇒ (_,'l) array_list ⇒ _"

  lemma stack_set_copy[sepref_gen_algo_rules]: "GEN_ALGO cp (is_copy A) ⟹ 4 < LENGTH('l::len2) ⟹ GEN_ALGO (stack_copy_ll' cp) (is_copy (stack_set_assn' TYPE('l::len2) A))"
    unfolding stack_set_assn_def 
    unfolding GEN_ALGO_def
    apply (rule is_copy_hr_comp)
    apply (rule stack_assn_copy[unfolded GEN_ALGO_def])
    .
  

lemmas [sepref_import_param] = list_set_is_empty_refine list_set_pop_refine

context 
  notes[fcomp_norm_simps] = stack_set_assn_def[symmetric] set_rel_id_simp
begin
  thm stack_pop_hnr[FCOMP list_set_pop_refine]
  private lemmas mop_set_select_id_fref = mop_set_select.fref[where K=Id, unfolded IS_LEFT_UNIQUE_def,simplified]
  thm stack_is_empty.refine list_set_is_empty_refine
  sepref_decl_impl (ismop) stack_pop_hnr[FCOMP list_set_pop_refine] uses mop_set_select_id_fref . 
  sepref_decl_impl (ismop) stack_is_empty.refine[FCOMP list_set_is_empty_refine] uses mop_set_is_empty.fref[where A=Id] .
end

lemma stack_set_assn_free[sepref_frame_free_rules]:
  assumes A: "MK_FREE A free_elem"
  shows "MK_FREE (stack_set_assn A) (stack_free free_elem)"
  unfolding stack_set_assn_def
  using assms
  by (intro sepref_frame_free_rules)
 

end