Theory Discipline_Cardinal

theory Discipline_Cardinal
  imports
    Discipline_Function
begin

declare [[syntax_ambiguity_warning = false]]

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

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

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)"

relativize functional "cadd" "cadd_rel" external

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

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

(* relativization *)

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

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)"

(* relativization *)
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

end