# Theory Discipline_Cardinal

```section‹Basic relativization of cardinality›

theory Discipline_Cardinal
imports
Discipline_Function
begin

relativize functional "cardinal" "cardinal_rel" external
relationalize "cardinal_rel" "is_cardinal"
synthesize "is_cardinal" from_definition assuming "nonempty"

notation is_cardinal_fm (‹cardinal'(_') is _›)

abbreviation
cardinal_r :: "[i,i⇒o] ⇒ i" (‹|_|⇗_⇖›) where
"|x|⇗M⇖ ≡ cardinal_rel(M,x)"

abbreviation
cardinal_r_set :: "[i,i]⇒i"  (‹|_|⇗_⇖›) where
"|x|⇗M⇖ ≡ cardinal_rel(##M,x)"

context M_trivial
begin
rel_closed for "cardinal"
using Least_closed'[of "λi. M(i) ∧ i ≈⇗M⇖ A"]
unfolding cardinal_rel_def
by simp
end ― ‹\<^locale>‹M_trivial››

manual_arity intermediate for "is_Int_fm"
unfolding is_Int_fm_def
using arity pred_Un_distrib
by (simp)

arity_theorem for "is_Int_fm"

arity_theorem for "is_funspace_fm"

arity_theorem for "is_function_space_fm"

arity_theorem for "surjP_rel_fm"

arity_theorem intermediate for "is_surj_fm"

lemma arity_is_surj_fm [arity] :
"A ∈ nat ⟹ B ∈ nat ⟹ I ∈ nat ⟹ arity(is_surj_fm(A, B, I)) = succ(A) ∪ succ(B) ∪ succ(I)"
using arity_is_surj_fm' pred_Un_distrib
by auto

arity_theorem for "injP_rel_fm"

arity_theorem intermediate for "is_inj_fm"

lemma arity_is_inj_fm [arity]:
"A ∈ nat ⟹ B ∈ nat ⟹ I ∈ nat ⟹ arity(is_inj_fm(A, B, I)) = succ(A) ∪ succ(B) ∪ succ(I)"
using arity_is_inj_fm' pred_Un_distrib
by auto

arity_theorem for "is_bij_fm"

arity_theorem for "is_eqpoll_fm"

arity_theorem for "is_cardinal_fm"

context M_Perm
begin
is_iff_rel for "cardinal"
using least_abs'[of "λi. M(i) ∧ i ≈⇗M⇖ A"]
is_eqpoll_iff
unfolding is_cardinal_def cardinal_rel_def
by simp
end ― ‹\<^locale>‹M_Perm››

synthesize "lt_rel" from_definition
notation lt_rel_fm (‹⋅_ < _⋅›)
arity_theorem intermediate for "lt_rel_fm"

lemma arity_lt_rel_fm[arity]: "a ∈ nat ⟹ b ∈ nat ⟹ arity(lt_rel_fm(a, b)) = succ(a) ∪ succ(b)"
using arity_lt_rel_fm'
by auto

relativize functional "Card" "Card_rel" external
relationalize "Card_rel" "is_Card"
synthesize "is_Card" from_definition assuming "nonempty"
notation is_Card_fm (‹⋅Card'(_')⋅›)
arity_theorem for "is_Card_fm"

notation Card_rel (‹Card⇗_⇖'(_')›)

lemma (in M_Perm) is_Card_iff: "M(A) ⟹ is_Card(M, A) ⟷ Card⇗M⇖(A)"
using is_cardinal_iff
unfolding is_Card_def Card_rel_def by simp

abbreviation
Card_r_set  :: "[i,i]⇒o"  (‹Card⇗_⇖'(_')›) where
"Card⇗M⇖(i) ≡ Card_rel(##M,i)"

relativize functional "InfCard" "InfCard_rel" external
relationalize "InfCard_rel" "is_InfCard"
synthesize "is_InfCard" from_definition assuming "nonempty"
notation is_InfCard_fm (‹⋅InfCard'(_')⋅›)
arity_theorem for "is_InfCard_fm"

notation InfCard_rel (‹InfCard⇗_⇖'(_')›)

abbreviation
InfCard_r_set  :: "[i,i]⇒o"  (‹InfCard⇗_⇖'(_')›) where
"InfCard⇗M⇖(i) ≡ InfCard_rel(##M,i)"

abbreviation
cadd_r :: "[i,i⇒o,i] ⇒ i" (‹_ ⊕⇗_⇖ _› [66,1,66] 65) where

context M_basic
begin
using cardinal_rel_closed
by simp
end ― ‹\<^locale>‹M_basic››

by (rule iff_sats sum_iff_sats | simp)+

arity_theorem for "sum_fm"

context M_Perm
begin
using is_cardinal_iff
by simp

end  ― ‹\<^locale>‹M_Perm››

subsection‹Disicpline for \<^term>‹cmult››

relativize functional "cmult" "cmult_rel" external

abbreviation
cmult_r :: "[i,i⇒o,i] ⇒ i" (‹_ ⊗⇗_⇖ _› [66,1,66] 65) where
"A ⊗⇗M⇖ B ≡ cmult_rel(M,A,B)"

relationalize "cmult_rel" "is_cmult"

declare cartprod_iff_sats [iff_sats]

synthesize "is_cmult" from_definition assuming "nonempty"

arity_theorem for "is_cmult_fm"

context M_Perm
begin
rel_closed for "cmult"
using cardinal_rel_closed
unfolding cmult_rel_def
by simp

is_iff_rel for "cmult"
using is_cardinal_iff
unfolding is_cmult_def cmult_rel_def
by simp

end ― ‹\<^locale>‹M_Perm››

end```