Theory Intf_Set

section ‹\isaheader{Set Interface}›
theory Intf_Set
imports Refine_Monadic.Refine_Monadic
begin
consts i_set :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of set_rel i_set]


definition [simp]: "op_set_delete x s ≡ s - {x}"
definition [simp]: "op_set_isEmpty s ≡ s = {}"
definition [simp]: "op_set_isSng s ≡ card s = 1"
definition [simp]: "op_set_size_abort m s ≡ min m (card s)"
definition [simp]: "op_set_disjoint a b ≡ a∩b={}"
definition [simp]: "op_set_filter P s ≡ {x∈s. P x}"
definition [simp]: "op_set_sel P s ≡ SPEC (λx. x∈s ∧ P x)"
definition [simp]: "op_set_pick s ≡ SPEC (λx. x∈s)"
definition [simp]: "op_set_to_sorted_list ordR s 
  ≡ SPEC (λl. set l = s ∧ distinct l ∧ sorted_wrt ordR l)"
definition [simp]: "op_set_to_list s ≡ SPEC (λl. set l = s ∧ distinct l)"
definition [simp]: "op_set_cart x y ≡ x × y"

(* TODO: Do op_set_pick_remove (like op_map_pick_remove) *)

context begin interpretation autoref_syn .
lemma [autoref_op_pat]:
  fixes s a b :: "'a set" and x::'a and P :: "'a ⇒ bool"
  shows
  "s - {x} ≡ op_set_delete$x$s"

  "s = {} ≡ op_set_isEmpty$s"
  "{}=s ≡ op_set_isEmpty$s"

  "card s = 1 ≡ op_set_isSng$s"
  "∃x. s={x} ≡ op_set_isSng$s"
  "∃x. {x}=s ≡ op_set_isSng$s"

  "min m (card s) ≡ op_set_size_abort$m$s"
  "min (card s) m ≡ op_set_size_abort$m$s"

  "a∩b={} ≡ op_set_disjoint$a$b"

  "{x∈s. P x} ≡ op_set_filter$P$s"

  "SPEC (λx. x∈s ∧ P x) ≡ op_set_sel$P$s"
  "SPEC (λx. P x ∧ x∈s) ≡ op_set_sel$P$s"

  "SPEC (λx. x∈s) ≡ op_set_pick$s"
  by (auto intro!: eq_reflection simp: card_Suc_eq)

lemma [autoref_op_pat]:
  "a × b ≡ op_set_cart a b"
  by (auto intro!: eq_reflection simp: card_Suc_eq)

lemma [autoref_op_pat]:
  "SPEC (λ(u,v). (u,v)∈s) ≡ op_set_pick$s"
  "SPEC (λ(u,v). P u v ∧ (u,v)∈s) ≡ op_set_sel$(case_prod P)$s"
  "SPEC (λ(u,v). (u,v)∈s ∧ P u v) ≡ op_set_sel$(case_prod P)$s"
  by (auto intro!: eq_reflection)

  lemma [autoref_op_pat]:
    "SPEC (λl. set l = s ∧ distinct l ∧ sorted_wrt ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. set l = s ∧ sorted_wrt ordR l ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ set l = s ∧ sorted_wrt ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ sorted_wrt ordR l ∧ set l = s) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_wrt ordR l ∧ distinct l ∧ set l = s) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_wrt ordR l ∧ set l = s ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"

    "SPEC (λl. s = set l ∧ distinct l ∧ sorted_wrt ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. s = set l ∧ sorted_wrt ordR l ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ s = set l ∧ sorted_wrt ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ sorted_wrt ordR l ∧ s = set l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_wrt ordR l ∧ distinct l ∧ s = set l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_wrt ordR l ∧ s = set l ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"

    "SPEC (λl. set l = s ∧ distinct l) ≡ op_set_to_list$s"
    "SPEC (λl. distinct l ∧ set l = s) ≡ op_set_to_list$s"

    "SPEC (λl. s = set l ∧ distinct l) ≡ op_set_to_list$s"
    "SPEC (λl. distinct l ∧ s = set l) ≡ op_set_to_list$s"
    by (auto intro!: eq_reflection)

end

lemma [autoref_itype]:
  "{} ::i ⟨I⟩ii_set"
  "insert ::i I →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "op_set_delete ::i I →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "(∈) ::i I →i ⟨I⟩ii_set →i i_bool"
  "op_set_isEmpty ::i ⟨I⟩ii_set →i i_bool"
  "op_set_isSng ::i ⟨I⟩ii_set →i i_bool"
  "(∪) ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "(∩) ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "((-) :: 'a set ⇒ 'a set ⇒ 'a set) ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "((=) :: 'a set ⇒ 'a set ⇒ bool) ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i i_bool"
  "(⊆) ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i i_bool"
  "op_set_disjoint ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i i_bool"
  "Ball ::i ⟨I⟩ii_set →i (I →i i_bool) →i i_bool"
  "Bex ::i ⟨I⟩ii_set →i (I →i i_bool) →i i_bool"
  "op_set_filter ::i (I →i i_bool) →i ⟨I⟩ii_set →i ⟨I⟩ii_set"
  "card ::i ⟨I⟩ii_set →i i_nat"
  "op_set_size_abort ::i i_nat →i ⟨I⟩ii_set →i i_nat"
  "set ::i ⟨I⟩ii_list →i ⟨I⟩ii_set"
  "op_set_sel ::i (I →i i_bool) →i ⟨I⟩ii_set →i ⟨I⟩ii_nres"
  "op_set_pick ::i ⟨I⟩ii_set →i ⟨I⟩ii_nres"
  "Sigma ::i ⟨Ia⟩ii_set →i (Ia →i ⟨Ib⟩ii_set) →i ⟨⟨Ia,Ib⟩ii_prod⟩ii_set"
  "(`) ::i (Ia→iIb) →i ⟨Ia⟩ii_set →i ⟨Ib⟩ii_set"
  "op_set_cart ::i ⟨Ix⟩iIsx →i ⟨Iy⟩iIsy →i ⟨⟨Ix, Iy⟩ii_prod⟩iIsp"
  "Union ::i ⟨⟨I⟩ii_set⟩ii_set →i ⟨I⟩ii_set"
  "atLeastLessThan ::i i_nat →i i_nat →i ⟨i_nat⟩ii_set"
  by simp_all

lemma hom_set1[autoref_hom]:
  "CONSTRAINT {} (⟨R⟩Rs)"
  "CONSTRAINT insert (R→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT (∈) (R→⟨R⟩Rs→Id)"
  "CONSTRAINT (∪) (⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT (∩) (⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT (-) (⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT (=) (⟨R⟩Rs→⟨R⟩Rs→Id)"
  "CONSTRAINT (⊆) (⟨R⟩Rs→⟨R⟩Rs→Id)"
  "CONSTRAINT Ball (⟨R⟩Rs→(R→Id)→Id)"
  "CONSTRAINT Bex (⟨R⟩Rs→(R→Id)→Id)"
  "CONSTRAINT card (⟨R⟩Rs→Id)"
  "CONSTRAINT set (⟨R⟩Rl→⟨R⟩Rs)"
  "CONSTRAINT (`) ((Ra→Rb) → ⟨Ra⟩Rs→⟨Rb⟩Rs)"
  "CONSTRAINT Union (⟨⟨R⟩Ri⟩Ro → ⟨R⟩Ri)"
  by simp_all

lemma hom_set2[autoref_hom]:
  "CONSTRAINT op_set_delete (R→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT op_set_isEmpty (⟨R⟩Rs→Id)"
  "CONSTRAINT op_set_isSng (⟨R⟩Rs→Id)"
  "CONSTRAINT op_set_size_abort (Id→⟨R⟩Rs→Id)"
  "CONSTRAINT op_set_disjoint (⟨R⟩Rs→⟨R⟩Rs→Id)"
  "CONSTRAINT op_set_filter ((R→Id)→⟨R⟩Rs→⟨R⟩Rs)"
  "CONSTRAINT op_set_sel ((R → Id)→⟨R⟩Rs→⟨R⟩Rn)"
  "CONSTRAINT op_set_pick (⟨R⟩Rs→⟨R⟩Rn)"
  by simp_all

lemma hom_set_Sigma[autoref_hom]:
  "CONSTRAINT Sigma (⟨Ra⟩Rs → (Ra → ⟨Rb⟩Rs) → ⟨⟨Ra,Rb⟩prod_rel⟩Rs2)"
  by simp_all
  
definition "finite_set_rel R ≡ Range R ⊆ Collect (finite)"

lemma finite_set_rel_trigger: "finite_set_rel R ⟹ finite_set_rel R" .

declaration ‹Tagged_Solver.add_triggers 
  "Relators.relator_props_solver" @{thms finite_set_rel_trigger}›

end