Theory Intf_Set

```section ‹\isaheader{Set Interface}›
theory Intf_Set
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" .