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,io]  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 ≈⇗MA"]
  unfolding cardinal_rel_def
  by simp
end ― ‹localeM_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 ≈⇗MA"]
    is_eqpoll_iff
  unfolding is_cardinal_def cardinal_rel_def
  by simp
end ― ‹localeM_Perm

reldb_add functional "Ord" "Ord"
reldb_add relational "Ord" "ordinal"
reldb_add functional "lt" "lt"
reldb_add relational "lt" "lt_rel"
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)"

subsection‹Disicpline for termcadd
relativize functional "cadd" "cadd_rel" external

abbreviation
  cadd_r :: "[i,io,i]  i" (‹_ ⊕⇗_ _› [66,1,66] 65) where
  "A ⊕⇗MB  cadd_rel(M,A,B)"

context M_basic
begin
rel_closed for "cadd"
  using cardinal_rel_closed
  unfolding cadd_rel_def
  by simp
end ― ‹localeM_basic

relationalize "cadd_rel" "is_cadd"

manual_schematic for "is_cadd" assuming "nonempty"
  unfolding is_cadd_def
  by (rule iff_sats sum_iff_sats | simp)+
synthesize "is_cadd" from_schematic

arity_theorem for "sum_fm"

arity_theorem for "is_cadd_fm"

context M_Perm
begin
is_iff_rel for "cadd"
  using is_cardinal_iff
  unfolding is_cadd_def cadd_rel_def
  by simp

end  ― ‹localeM_Perm

subsection‹Disicpline for termcmult

relativize functional "cmult" "cmult_rel" external

abbreviation
  cmult_r :: "[i,io,i]  i" (‹_ ⊗⇗_ _› [66,1,66] 65) where
  "A ⊗⇗MB  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 ― ‹localeM_Perm

end