Theory IICF_Set

section ‹Set Interface›
theory IICF_Set
imports "../../Sepref"
begin

subsection ‹Operations›

(*
definition [simp]: "op_set_is_empty s ≡ s={}"
lemma op_set_is_empty_param[param]: "(op_set_is_empty,op_set_is_empty)∈⟨A⟩set_rel → bool_rel" by auto
*)


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


context
  fixes t ::  "nat"
begin
  definition "mop_set_empty = SPECT [ {} ↦ enat t ]"

  lemma mop_set_empty: "tt ≤ lst (SPECT [ {} ↦ t ]) Q ⟹ tt
           ≤ lst (mop_set_empty) Q" unfolding mop_set_empty_def by simp

  sepref_register "mop_set_empty" 
  print_theorems 
end


context
  fixes t ::  "'c set ⇒ nat"
begin
  definition "mop_set_isempty S = SPECT [ S={} ↦ t S ]"

  lemma  mop_set_isempty: "tt ≤ lst (SPECT [ S={} ↦ t S ])  Q
        ⟹ tt ≤ lst (mop_set_isempty S) Q" unfolding mop_set_isempty_def by simp
 
  sepref_register "mop_set_isempty" 
  print_theorems 
end


context
  fixes t ::  "'c set ⇒ nat"
begin
  definition "mop_set_pick S = do { ASSERT (S≠{}); SPECT (emb (λx. x∈S) (t S)) }"

  lemma  mop_set_pick: "tt ≤ lst (SPECT (emb (λx. x∈S) (t S)))  Q
        ⟹ S ≠ {} ⟹ tt ≤ lst (mop_set_pick S) Q" unfolding mop_set_pick_def by simp

  thm progress_rules

  lemma progress_mop_set_pick[progress_rules]: "t S > 0 ⟹ progress (mop_set_pick S)"
    unfolding mop_set_pick_def by (auto intro!: progress_rules simp add:   zero_enat_def) 

  sepref_register "mop_set_pick" 
  print_theorems 
end

context
  fixes t ::  "'c set ⇒ nat"
begin
  definition "mop_set_pick_extract S = do { ASSERT (S≠{}); SPECT (emb (λ(x,C). x∈S ∧ C=S-{x}) (t S)) }"

  lemma  mop_set_pick_extract: "tt ≤ lst (SPECT (emb (λ(x,C). x∈S ∧ C=S-{x}) (t S))) Q
        ⟹ S ≠ {} ⟹ tt ≤ lst (mop_set_pick_extract S) Q" unfolding mop_set_pick_extract_def by simp

  thm progress_rules

  lemma progress_mop_set_pick_extract[progress_rules]: "t S > 0 ⟹ progress (mop_set_pick_extract S)"
    unfolding mop_set_pick_extract_def by (auto intro!: progress_rules simp add:   zero_enat_def) 

  sepref_register "mop_set_pick_extract" 
  print_theorems 
end
 


context
  fixes t:: "'a set ⇒ nat" 
begin
  definition "mop_set_member x S = SPECT [ x ∈ S ↦ enat (t S) ]"
  sepref_register "mop_set_member" 
  print_theorems 
end

 

context
  fixes t ::  "'c set ⇒ nat"
begin
  definition "mop_set_del S x = SPECT [ S - {x} ↦ (t S)]"

  lemma  mop_set_del: "tt ≤ lst (SPECT [ S - {x} ↦ (t S)])  Q
        ⟹ tt ≤ lst (mop_set_del S x) Q" unfolding mop_set_del_def by simp


  lemma progress_mop_set_del[progress_rules]: "t S > 0 ⟹ progress (mop_set_del S x)"
      unfolding mop_set_del_def  by (auto intro: progress_rules simp add:   zero_enat_def) 

  sepref_register "mop_set_del" 
  print_theorems 
end


context 
  fixes t :: "'c set ⇒ nat"
begin

  definition "mop_set_insert x S = SPECT [insert x S ↦ t S]"

  lemma mop_set_insert: "tt ≤ lst (SPECT [ (insert x S) ↦ t S]) Q ⟹
         tt ≤ lst (mop_set_insert x S) Q" unfolding mop_set_insert_def by simp

  sepref_register "mop_set_insert" 
  print_theorems 
end

(*
sepref_decl_op set_empty: "{}" :: "⟨A⟩set_rel" .
sepref_decl_op (no_def) set_is_empty: op_set_is_empty :: "⟨A⟩set_rel → bool_rel" .
sepref_decl_op set_member: "(∈)" :: "A → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_insert: Set.insert :: "A → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_delete: "λx s. s - {x}" :: "A → ⟨A⟩set_rel → ⟨A⟩set_rel" 
  where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_union: "(∪)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" .
sepref_decl_op set_inter: "(∩)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_diff: "(-) ::_ set ⇒ _" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subseteq: "(⊆)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subset: "(⊂)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .

(* TODO: We may want different operations here: pick with predicate returning option,
  pick with remove, ... *)    
sepref_decl_op set_pick: "REST" :: "[λs. s≠{}]⇩f ⟨K⟩set_rel → K" by auto
*)


end

(* TODO: Set-pick. Move from where it is already defined! *)

subsection ‹Patterns›

(*
lemma pat_set[def_pat_rules]:
  "{} ≡ op_set_empty"
  "(∈) ≡ op_set_member"    
  "Set.insert ≡ op_set_insert"
  "(∪) ≡ op_set_union"
  "(∩) ≡ op_set_inter"
  "(-) ≡ op_set_diff"
  "(⊆) ≡ op_set_subseteq"
  "(⊂) ≡ op_set_subset"
  by (auto intro!: eq_reflection)
  
lemma pat_set2[pat_rules]: 
  "(=) $s${} ≡ op_set_is_empty$s"
  "(=) ${}$s ≡ op_set_is_empty$s"

  "(-) $s$(Set.insert$x${}) ≡ op_set_delete$x$s"
  "SPEC$(λ⇩2x. (∈) $x$s) ≡ op_set_pick s"
  "RES$s ≡ op_set_pick s"
  by (auto intro!: eq_reflection)
*)

(*
locale set_custom_empty = 
  fixes empty and op_custom_empty :: "'a set"
  assumes op_custom_empty_def: "op_custom_empty = op_set_empty"
begin
  sepref_register op_custom_empty :: "'ax set"

  lemma fold_custom_empty:
    "{} = op_custom_empty"
    "op_set_empty = op_custom_empty"
    "mop_set_empty = RETURN op_custom_empty"
    unfolding op_custom_empty_def by simp_all
end
*)


end