Theory Discipline_Cardinal
theory Discipline_Cardinal
imports
Discipline_Base
Discipline_Function
Least
FrecR
Arities
FrecR_Arities
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
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'
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'
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 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
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)"
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
definition
Powapply :: "[i,i] ⇒ i" where
"Powapply(f,y) ≡ Pow(f`y)"
reldb_add functional "Pow" "Pow_rel"
reldb_add relational "Pow" "is_Pow"
lemma subset_iff_sats [iff_sats]:
"nth(i, env) = x ⟹ nth(j, env) = y ⟹ i∈nat ⟹ j∈nat ⟹
env ∈ list(A) ⟹ subset(##A, x, y) ⟷ A, env ⊨ subset_fm(i, j)"
using sats_subset_fm' by simp
declare Replace_iff_sats[iff_sats]
synthesize "is_Pow" from_definition assuming "nonempty"
arity_theorem for "is_Pow_fm"
relativize functional "Powapply" "Powapply_rel"
relationalize "Powapply_rel" "is_Powapply"
synthesize "is_Powapply" from_definition assuming "nonempty"
arity_theorem for "is_Powapply_fm"
notation Powapply_rel (‹Powapply⇗_⇖'(_,_')›)
context M_basic
begin
rel_closed for "Powapply"
unfolding Powapply_rel_def
by simp
is_iff_rel for "Powapply"
using Pow_rel_iff
unfolding is_Powapply_def Powapply_rel_def
by simp
univalent for "Powapply"
using is_Powapply_iff
unfolding univalent_def
by simp
end
definition
HVfrom :: "[i,i,i] ⇒ i" where
"HVfrom(A,x,f) ≡ A ∪ (⋃y∈x. Powapply(f,y))"
relativize functional "HVfrom" "HVfrom_rel"
relationalize "HVfrom_rel" "is_HVfrom"
synthesize "is_HVfrom" from_definition assuming "nonempty"
arity_theorem for "is_HVfrom_fm"
notation HVfrom_rel (‹HVfrom⇗_⇖'(_,_,_')›)
locale M_HVfrom= M_eclose +
assumes
Powapply_replacement:
"M(K) ⟹ strong_replacement(M,λy z. z = Powapply⇗M⇖(f,y))"
begin
is_iff_rel for "HVfrom"
proof -
assume assms:"M(A)" "M(x)" "M(f)" "M(res)"
then
have "is_Replace(M,x,λy z. z = Powapply⇗M⇖(f,y),r) ⟷ r = {z . y∈x, z = Powapply⇗M⇖(f,y)}"
if "M(r)" for r
using that Powapply_rel_closed
Replace_abs[of x r "λy z. z = Powapply⇗M⇖(f,y)"] transM[of _ x]
by simp
moreover
have "is_Replace(M,x,is_Powapply(M,f),r) ⟷
is_Replace(M,x,λy z. z = Powapply⇗M⇖(f,y),r)" if "M(r)" for r
using assms that is_Powapply_iff is_Replace_cong
by simp
ultimately
have "is_Replace(M,x,is_Powapply(M,f),r) ⟷ r = {z . y∈x, z = Powapply⇗M⇖(f,y)}"
if "M(r)" for r
using that assms
by simp
moreover
have "M({z . y ∈ x, z = Powapply⇗M⇖(f,y)})"
using assms strong_replacement_closed[OF Powapply_replacement]
Powapply_rel_closed transM[of _ x]
by simp
moreover from assms
have "{z . y ∈ x, z = Powapply⇗M⇖(f,y)} = {y . w ∈ x, M(y) ∧ M(w) ∧ y = Powapply⇗M⇖(f,w)}"
by (auto dest:transM)
ultimately
show ?thesis
using assms
unfolding is_HVfrom_def HVfrom_rel_def
by (auto dest:transM)
qed
univalent for "HVfrom"
using is_HVfrom_iff
unfolding univalent_def
by simp
rel_closed for "HVfrom"
proof -
assume assms:"M(A)" "M(x)" "M(f)"
have "M({z . y ∈ x, z = Powapply⇗M⇖(f,y)})"
using assms strong_replacement_closed[OF Powapply_replacement]
Powapply_rel_closed transM[of _ x]
by simp
then
have "M(A ∪ ⋃({z . y∈x, z = Powapply⇗M⇖(f,y)}))"
using assms
by simp
moreover from assms
have "{z . y ∈ x, z = Powapply⇗M⇖(f,y)} = {y . w ∈ x, M(y) ∧ M(w) ∧ y = Powapply⇗M⇖(f,w)}"
by (auto dest:transM)
ultimately
show ?thesis
using assms
unfolding HVfrom_rel_def
by simp
qed
end
definition
Vfrom_rel :: "[i⇒o,i,i] ⇒ i" (‹Vfrom⇗_⇖'(_,_')›) where
"Vfrom⇗M⇖(A,i) = transrec(i, HVfrom_rel(M,A))"
definition
is_Vfrom :: "[i⇒o,i,i,i] ⇒ o" where
"is_Vfrom(M,A,i,z) ≡ is_transrec(M,is_HVfrom(M,A),i,z)"
locale M_Vfrom= M_HVfrom +
assumes
trepl_HVfrom : "⟦ M(A);M(i) ⟧ ⟹ transrec_replacement(M,is_HVfrom(M,A),i)"
begin
lemma Vfrom_rel_iff :
assumes "M(A)" "M(i)" "M(z)" "Ord(i)"
shows "is_Vfrom(M,A,i,z) ⟷ z = Vfrom⇗M⇖(A,i)"
proof -
have "relation2(M, is_HVfrom(M, A), HVfrom_rel(M, A))"
using assms is_HVfrom_iff
unfolding relation2_def
by simp
then
show ?thesis
using assms HVfrom_rel_closed trepl_HVfrom
transrec_abs[of "is_HVfrom(M,A)" i "HVfrom_rel(M,A)" z]
unfolding is_Vfrom_def Vfrom_rel_def
by simp
qed
end
end