Theory Nonempty_Bounded_Set
section ‹Nonempty Sets Strictly Bounded by an Infinite Cardinal›
theory Nonempty_Bounded_Set
imports
"HOL-Cardinals.Bounded_Set"
begin
typedef ('a, 'k) nebset (‹_ set![_]› [22, 21] 21) =
"{A :: 'a set. A ≠ {} ∧ |A| <o natLeq +c |UNIV :: 'k set|}"
morphisms set_nebset Abs_nebset
apply (rule exI[of _ "{undefined}"], simp)
apply (rule Cfinite_ordLess_Cinfinite)
apply (auto simp: cfinite_def cinfinite_csum natLeq_cinfinite Card_order_csum)
done
setup_lifting type_definition_nebset
lift_definition map_nebset ::
"('a ⇒ 'b) ⇒ 'a set!['k] ⇒ 'b set!['k]" is image
using card_of_image ordLeq_ordLess_trans by blast
lift_definition rel_nebset ::
"('a ⇒ 'b ⇒ bool) ⇒ 'a set!['k] ⇒ 'b set!['k] ⇒ bool" is rel_set .
lift_definition nebinsert :: "'a ⇒ 'a set!['k] ⇒ 'a set!['k]" is "insert"
using infinite_card_of_insert ordIso_ordLess_trans Field_card_of Field_natLeq UNIV_Plus_UNIV
csum_def finite_Plus_UNIV_iff finite_insert finite_ordLess_infinite2 infinite_UNIV_nat
insert_not_empty by metis
lift_definition nebsingleton :: "'a ⇒ 'a set!['k]" is "λa. {a}"
apply simp
apply (rule Cfinite_ordLess_Cinfinite)
apply (auto simp: cfinite_def cinfinite_csum natLeq_cinfinite Card_order_csum)
done
lemma set_nebset_to_set_nebset: "A ≠ {} ⟹ |A| <o natLeq +c |UNIV :: 'k set| ⟹
set_nebset (the_inv set_nebset A :: 'a set!['k]) = A"
apply (rule f_the_inv_into_f[unfolded inj_on_def])
apply (simp add: set_nebset_inject range_eqI Abs_nebset_inverse[symmetric])
apply (rule range_eqI Abs_nebset_inverse[symmetric] CollectI)+
apply blast
done
lemma rel_nebset_aux_infinite:
fixes a :: "'a set!['k]" and b :: "'b set!['k]"
shows "(∀t ∈ set_nebset a. ∃u ∈ set_nebset b. R t u) ∧ (∀u ∈ set_nebset b. ∃t ∈ set_nebset a. R t u) ⟷
((BNF_Def.Grp {a. set_nebset a ⊆ {(a, b). R a b}} (map_nebset fst))¯¯ OO
BNF_Def.Grp {a. set_nebset a ⊆ {(a, b). R a b}} (map_nebset snd)) a b" (is "?L ⟷ ?R")
proof
assume ?L
define R' :: "('a × 'b) set!['k]"
where "R' = the_inv set_nebset (Collect (case_prod R) ∩ (set_nebset a × set_nebset b))"
(is "_ = the_inv set_nebset ?L'")
from ‹?L› have "?L' ≠ {}" by transfer auto
moreover
have "|?L'| <o natLeq +c |UNIV :: 'k set|"
unfolding csum_def Field_natLeq
by (intro ordLeq_ordLess_trans[OF card_of_mono1[OF Int_lower2]]
card_of_Times_ordLess_infinite)
(simp, (transfer, simp add: csum_def Field_natLeq)+)
ultimately have *: "set_nebset R' = ?L'" unfolding R'_def by (intro set_nebset_to_set_nebset)
show ?R unfolding Grp_def relcompp.simps conversep.simps
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
from * show "a = map_nebset fst R'" using conjunct1[OF ‹?L›]
by (transfer, auto simp add: image_def Int_def split: prod.splits)
from * show "b = map_nebset snd R'" using conjunct2[OF ‹?L›]
by (transfer, auto simp add: image_def Int_def split: prod.splits)
qed (auto simp add: *)
next
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
by transfer force
qed
bnf "'a set!['k]"
map: map_nebset
sets: set_nebset
bd: "natLeq +c card_suc |UNIV :: 'k set|"
rel: rel_nebset
proof -
show "map_nebset id = id" by (rule ext, transfer) simp
next
fix f g
show "map_nebset (f o g) = map_nebset f o map_nebset g" by (rule ext, transfer) auto
next
fix X f g
assume "⋀z. z ∈ set_nebset X ⟹ f z = g z"
then show "map_nebset f X = map_nebset g X" by transfer force
next
fix f
show "set_nebset ∘ map_nebset f = (`) f ∘ set_nebset" by (rule ext, transfer) auto
next
fix X :: "'a set!['k]"
show "|set_nebset X| <o natLeq +c card_suc |UNIV :: 'k set|"
by transfer
(elim conjE ordLess_ordLeq_trans csum_mono1;
simp add: card_suc_greater ordLess_imp_ordLeq Card_order_card_suc csum_mono2)
next
fix R S
show "rel_nebset R OO rel_nebset S ≤ rel_nebset (R OO S)"
by (rule predicate2I, transfer) (auto simp: rel_set_OO[symmetric])
next
fix R :: "'a ⇒ 'b ⇒ bool"
show "rel_nebset R = ((λx y. ∃z. set_nebset z ⊆ {(x, y). R x y} ∧
map_nebset fst z = x ∧ map_nebset snd z = y) :: 'a set!['k] ⇒ 'b set!['k] ⇒ bool)"
by (simp add: rel_nebset_def map_fun_def o_def rel_set_def
rel_nebset_aux_infinite[unfolded OO_Grp_alt])
qed (simp_all add: card_order_bd_fun Cinfinite_bd_fun regularCard_bd_fun)
lemma map_nebset_nebinsert[simp]: "map_nebset f (nebinsert x X) = nebinsert (f x) (map_nebset f X)"
by transfer auto
lemma map_nebset_nebsingleton: "map_nebset f (nebsingleton x) = nebsingleton (f x)"
by transfer auto
lemma nebsingleton_inj[simp]: "nebsingleton x = nebsingleton y ⟷ x = y"
by transfer auto
lemma rel_nebsingleton[simp]:
"rel_nebset R (nebsingleton x1) (nebsingleton x2) = R x1 x2"
by transfer (auto simp: rel_set_def)
lemma rel_nebset_nebsingleton[simp]:
"rel_nebset R (nebsingleton x1) X = (∀x2∈set_nebset X. R x1 x2)"
"rel_nebset R X (nebsingleton x2) = (∀x1∈set_nebset X. R x1 x2)"
by (transfer, force simp add: rel_set_def)+
lemma rel_nebset_False[simp]: "rel_nebset (λx y. False) x y = False"
by transfer (auto simp: rel_set_def)
lemmas set_nebset_nebsingleton[simp] = nebsingleton.rep_eq
lemma nebinsert_absorb[simp]: "nebinsert a (nebinsert a x) = nebinsert a x"
by transfer simp
lift_definition bset_of_nebset :: "'a set!['k] ⇒ 'a set['k]" is "λX. X" by (rule conjunct2)
lemma rel_bset_bset_of_nebset[simp]:
"rel_bset R (bset_of_nebset X) (bset_of_nebset Y) = rel_nebset R X Y"
by transfer (rule refl)
lemma rel_nebset_conj[simp]:
"rel_nebset (λx y. P ∧ Q x y) x y ⟷ P ∧ rel_nebset Q x y"
"rel_nebset (λx y. Q x y ∧ P) x y ⟷ P ∧ rel_nebset Q x y"
by (transfer, auto simp: rel_set_def)+
lemma set_bset_empty[simp]: "set_bset X = {} ⟷ X = bempty"
by transfer simp
end