Theory Intf_Set

theory Intf_Set
imports Refine_Monadic
header {* \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_by_rel 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_by_rel ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. set l = s ∧ sorted_by_rel ordR l ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ set l = s ∧ sorted_by_rel ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ sorted_by_rel ordR l ∧ set l = s) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_by_rel ordR l ∧ distinct l ∧ set l = s) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_by_rel ordR l ∧ set l = s ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"

    "SPEC (λl. s = set l ∧ distinct l ∧ sorted_by_rel ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. s = set l ∧ sorted_by_rel ordR l ∧ distinct l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ s = set l ∧ sorted_by_rel ordR l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. distinct l ∧ sorted_by_rel ordR l ∧ s = set l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_by_rel ordR l ∧ distinct l ∧ s = set l) 
    ≡ OP (op_set_to_sorted_list ordR)$s"
    "SPEC (λl. sorted_by_rel 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"
  "op ∈ ::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"
  "op ∪ ::i ⟨I⟩ii_set ->i ⟨I⟩ii_set ->i ⟨I⟩ii_set"
  "op ∩ ::i ⟨I⟩ii_set ->i ⟨I⟩ii_set ->i ⟨I⟩ii_set"
  "(op - :: 'a set => 'a set => 'a set) ::i ⟨I⟩ii_set ->i ⟨I⟩ii_set ->i ⟨I⟩ii_set"
  "(op = :: 'a set => 'a set => bool) ::i ⟨I⟩ii_set ->i ⟨I⟩ii_set ->i i_bool"
  "op ⊆ ::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"
  "op ` ::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 op ∈ (R->⟨R⟩Rs->Id)"
  "CONSTRAINT op ∪ (⟨R⟩Rs->⟨R⟩Rs->⟨R⟩Rs)"
  "CONSTRAINT op ∩ (⟨R⟩Rs->⟨R⟩Rs->⟨R⟩Rs)"
  "CONSTRAINT op - (⟨R⟩Rs->⟨R⟩Rs->⟨R⟩Rs)"
  "CONSTRAINT op = (⟨R⟩Rs->⟨R⟩Rs->Id)"
  "CONSTRAINT op ⊆ (⟨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 op ` ((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