Theory Collections.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  ab={}"
definition [simp]: "op_set_filter P s  {xs. P x}"
definition [simp]: "op_set_sel P s  SPEC (λx. xs  P x)"
definition [simp]: "op_set_pick s  SPEC (λx. xs)"
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"

  "ab={}  op_set_disjoint$a$b"

  "{xs. P x}  op_set_filter$P$s"

  "SPEC (λx. xs  P x)  op_set_sel$P$s"
  "SPEC (λx. P x  xs)  op_set_sel$P$s"

  "SPEC (λx. xs)  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 Iii_set"
  "insert ::i I i Iii_set i Iii_set"
  "op_set_delete ::i I i Iii_set i Iii_set"
  "(∈) ::i I i Iii_set i i_bool"
  "op_set_isEmpty ::i Iii_set i i_bool"
  "op_set_isSng ::i Iii_set i i_bool"
  "(∪) ::i Iii_set i Iii_set i Iii_set"
  "(∩) ::i Iii_set i Iii_set i Iii_set"
  "((-) :: 'a set  'a set  'a set) ::i Iii_set i Iii_set i Iii_set"
  "((=) :: 'a set  'a set  bool) ::i Iii_set i Iii_set i i_bool"
  "(⊆) ::i Iii_set i Iii_set i i_bool"
  "op_set_disjoint ::i Iii_set i Iii_set i i_bool"
  "Ball ::i Iii_set i (I i i_bool) i i_bool"
  "Bex ::i Iii_set i (I i i_bool) i i_bool"
  "op_set_filter ::i (I i i_bool) i Iii_set i Iii_set"
  "card ::i Iii_set i i_nat"
  "op_set_size_abort ::i i_nat i Iii_set i i_nat"
  "set ::i Iii_list i Iii_set"
  "op_set_sel ::i (I i i_bool) i Iii_set i Iii_nres"
  "op_set_pick ::i Iii_set i Iii_nres"
  "Sigma ::i Iaii_set i (Ia i Ibii_set) i Ia,Ibii_prodii_set"
  "(`) ::i (IaiIb) i Iaii_set i Ibii_set"
  "op_set_cart ::i IxiIsx i IyiIsy i Ix, Iyii_prodiIsp"
  "Union ::i Iii_setii_set i Iii_set"
  "atLeastLessThan ::i i_nat i i_nat i i_natii_set"
  by simp_all

lemma hom_set1[autoref_hom]:
  "CONSTRAINT {} (RRs)"
  "CONSTRAINT insert (RRRsRRs)"
  "CONSTRAINT (∈) (RRRsId)"
  "CONSTRAINT (∪) (RRsRRsRRs)"
  "CONSTRAINT (∩) (RRsRRsRRs)"
  "CONSTRAINT (-) (RRsRRsRRs)"
  "CONSTRAINT (=) (RRsRRsId)"
  "CONSTRAINT (⊆) (RRsRRsId)"
  "CONSTRAINT Ball (RRs(RId)Id)"
  "CONSTRAINT Bex (RRs(RId)Id)"
  "CONSTRAINT card (RRsId)"
  "CONSTRAINT set (RRlRRs)"
  "CONSTRAINT (`) ((RaRb)  RaRsRbRs)"
  "CONSTRAINT Union (RRiRo  RRi)"
  by simp_all

lemma hom_set2[autoref_hom]:
  "CONSTRAINT op_set_delete (RRRsRRs)"
  "CONSTRAINT op_set_isEmpty (RRsId)"
  "CONSTRAINT op_set_isSng (RRsId)"
  "CONSTRAINT op_set_size_abort (IdRRsId)"
  "CONSTRAINT op_set_disjoint (RRsRRsId)"
  "CONSTRAINT op_set_filter ((RId)RRsRRs)"
  "CONSTRAINT op_set_sel ((R  Id)RRsRRn)"
  "CONSTRAINT op_set_pick (RRsRRn)"
  by simp_all

lemma hom_set_Sigma[autoref_hom]:
  "CONSTRAINT Sigma (RaRs  (Ra  RbRs)  Ra,Rbprod_relRs2)"
  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