Theory Separation_Instances
subsection‹More Instances of Separation›
theory Separation_Instances
imports
Interface
begin
text‹The following instances are mostly the same repetitive task; and we just
copied and pasted, tweaking some lemmas if needed (for example, we might have
needed to use some closure results).›
definition radd_body :: "[i,i,i] ⇒ o" where
"radd_body(R,S) ≡ λz. (∃x y. z = ⟨Inl(x), Inr(y)⟩) ∨
(∃x' x. z = ⟨Inl(x'), Inl(x)⟩ ∧ ⟨x', x⟩ ∈ R) ∨
(∃y' y. z = ⟨Inr(y'), Inr(y)⟩ ∧ ⟨y', y⟩ ∈ S)"
relativize functional "radd_body" "radd_body_rel"
relationalize "radd_body_rel" "is_radd_body"
synthesize "is_radd_body" from_definition
arity_theorem for "is_radd_body_fm"
definition rmult_body :: "[i,i,i] ⇒ o" where
"rmult_body(b,d) ≡ λz. ∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ b ∨
x' = x ∧ ⟨y', y⟩ ∈ d)"
relativize functional "rmult_body" "rmult_body_rel"
relationalize "rmult_body_rel" "is_rmult_body"
synthesize "is_rmult_body" from_definition
arity_theorem for "is_rmult_body_fm"
lemma (in M_replacement) separation_well_ord_iso:
"(M)(f) ⟹ (M)(r) ⟹ (M)(A) ⟹ separation
(M, λx. x ∈ A ⟶ (∃y[M]. ∃p[M]. is_apply(M, f, x, y) ∧ pair(M, y, x, p) ∧ p ∈ r))"
using separation_imp separation_in lam_replacement_identity lam_replacement_constant
lam_replacement_apply[of f] lam_replacement_product
by simp
definition is_obase_body :: "[i⇒o,i,i,i] ⇒ o" where
"is_obase_body(N,A,r,x) ≡ x ∈ A ⟶
¬ (∃y[N].
∃g[N].
ordinal(N, y) ∧
(∃my[N].
∃pxr[N].
membership(N, y, my) ∧
pred_set(N, A, x, r, pxr) ∧
order_isomorphism(N, pxr, r, y, my, g)))"
synthesize "is_obase_body" from_definition
arity_theorem for "is_obase_body_fm"
definition is_obase_equals :: "[i⇒o,i,i,i] ⇒ o" where
"is_obase_equals(N,A,r,a) ≡ ∃x[N].
∃g[N].
∃mx[N].
∃par[N].
ordinal(N, x) ∧
membership(N, x, mx) ∧
pred_set(N, A, a, r, par) ∧ order_isomorphism(N, par, r, x, mx, g)"
synthesize "is_obase_equals" from_definition
arity_theorem for "is_obase_equals_fm"
synthesize "PiP_rel" from_definition assuming "nonempty"
arity_theorem for "PiP_rel_fm"
synthesize "injP_rel" from_definition assuming "nonempty"
arity_theorem for "injP_rel_fm"
synthesize "surjP_rel" from_definition assuming "nonempty"
arity_theorem for "surjP_rel_fm"
context M_ZF1_trans
begin
lemma radd_body_abs:
assumes "(##M)(R)" "(##M)(S)" "(##M)(x)"
shows "is_radd_body(##M,R,S,x) ⟷ radd_body(R,S,x)"
using assms pair_in_M_iff Inl_in_M_iff Inr_in_M_iff
unfolding radd_body_def is_radd_body_def
by (auto)
lemma separation_radd_body:
"(##M)(R) ⟹ (##M)(S) ⟹ separation
(##M, λz. (∃x y. z = ⟨Inl(x), Inr(y)⟩) ∨
(∃x' x. z = ⟨Inl(x'), Inl(x)⟩ ∧ ⟨x', x⟩ ∈ R) ∨
(∃y' y. z = ⟨Inr(y'), Inr(y)⟩ ∧ ⟨y', y⟩ ∈ S))"
using separation_in_ctm[where φ="is_radd_body_fm(1,2,0)" and env="[R,S]"]
is_radd_body_def arity_is_radd_body_fm ord_simp_union is_radd_body_fm_type radd_body_abs
unfolding radd_body_def
by simp
lemma rmult_body_abs:
assumes "(##M)(b)" "(##M)(d)" "(##M)(x)"
shows "is_rmult_body(##M,b,d,x) ⟷ rmult_body(b,d,x)"
using assms pair_in_M_iff apply_closed
unfolding rmult_body_def is_rmult_body_def
by (auto)
lemma separation_rmult_body:
"(##M)(b) ⟹ (##M)(d) ⟹ separation
(##M, λz. ∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ b ∨ x' = x ∧ ⟨y', y⟩ ∈ d))"
using separation_in_ctm[where φ="is_rmult_body_fm(1,2,0)" and env="[b,d]"]
is_rmult_body_def arity_is_rmult_body_fm ord_simp_union is_rmult_body_fm_type rmult_body_abs
unfolding rmult_body_def
by simp
lemma separation_is_obase:
"(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation
(##M, λx. x ∈ A ⟶
¬ (∃y[##M].
∃g[##M].
ordinal(##M, y) ∧
(∃my[##M].
∃pxr[##M].
membership(##M, y, my) ∧
pred_set(##M, A, x, r, pxr) ∧
order_isomorphism(##M, pxr, r, y, my, g))))"
using separation_in_ctm[where φ="is_obase_body_fm(1,2,0)" and env="[A,r]"]
is_obase_body_def arity_is_obase_body_fm ord_simp_union is_obase_body_fm_type
by simp
lemma separation_obase_equals:
"(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation
(##M, λa. ∃x[##M].
∃g[##M].
∃mx[##M].
∃par[##M].
ordinal(##M, x) ∧
membership(##M, x, mx) ∧
pred_set(##M, A, a, r, par) ∧ order_isomorphism(##M, par, r, x, mx, g))"
using separation_in_ctm[where φ="is_obase_equals_fm(1,2,0)" and env="[A,r]"]
is_obase_equals_def arity_is_obase_equals_fm ord_simp_union is_obase_equals_fm_type
by simp
lemma separation_PiP_rel:
"(##M)(A) ⟹ separation(##M, PiP_rel(##M,A))"
using separation_in_ctm[where env="[A]" and φ="PiP_rel_fm(1,0)"]
nonempty PiP_rel_iff_sats[symmetric] arity_PiP_rel_fm PiP_rel_fm_type
by(simp_all add: ord_simp_union)
lemma separation_injP_rel:
"(##M)(A) ⟹ separation(##M, injP_rel(##M,A))"
using separation_in_ctm[where env="[A]" and φ="injP_rel_fm(1,0)"]
nonempty injP_rel_iff_sats[symmetric] arity_injP_rel_fm injP_rel_fm_type
by(simp_all add: ord_simp_union)
lemma separation_surjP_rel:
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, surjP_rel(##M,A,B))"
using separation_in_ctm[where env="[A,B]" and φ="surjP_rel_fm(1,2,0)"]
nonempty surjP_rel_iff_sats[symmetric] arity_surjP_rel_fm surjP_rel_fm_type
by(simp_all add: ord_simp_union)
lemma separation_is_function:
"separation(##M, is_function(##M))"
using separation_in_ctm[where env="[]" and φ="function_fm(0)"] arity_function_fm
by simp
end
definition fstsnd_in_sndsnd :: "[i] ⇒ o" where
"fstsnd_in_sndsnd ≡ λx. fst(snd(x)) ∈ snd(snd(x))"
relativize "fstsnd_in_sndsnd" "is_fstsnd_in_sndsnd"
synthesize "is_fstsnd_in_sndsnd" from_definition assuming "nonempty"
arity_theorem for "is_fstsnd_in_sndsnd_fm"
definition sndfst_eq_fstsnd :: "[i] ⇒ o" where
"sndfst_eq_fstsnd ≡ λx. snd(fst(x)) = fst(snd(x))"
relativize "sndfst_eq_fstsnd" "is_sndfst_eq_fstsnd"
synthesize "is_sndfst_eq_fstsnd" from_definition assuming "nonempty"
arity_theorem for "is_sndfst_eq_fstsnd_fm"
context M_ZF1_trans
begin
lemma fstsnd_in_sndsnd_abs:
assumes "(##M)(x)"
shows "is_fstsnd_in_sndsnd(##M,x) ⟷ fstsnd_in_sndsnd(x)"
using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
unfolding fstsnd_in_sndsnd_def is_fstsnd_in_sndsnd_def
by auto
lemma separation_fstsnd_in_sndsnd:
"separation(##M, λx. fst(snd(x)) ∈ snd(snd(x)))"
using separation_in_ctm[where env="[]" and φ="is_fstsnd_in_sndsnd_fm(0)" and Q=fstsnd_in_sndsnd]
nonempty fstsnd_in_sndsnd_abs arity_is_fstsnd_in_sndsnd_fm
unfolding fstsnd_in_sndsnd_def
by simp
lemma sndfst_eq_fstsnd_abs:
assumes "(##M)(x)"
shows "is_sndfst_eq_fstsnd(##M,x) ⟷ sndfst_eq_fstsnd(x)"
using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
unfolding sndfst_eq_fstsnd_def is_sndfst_eq_fstsnd_def
by auto
lemma separation_sndfst_eq_fstsnd:
"separation(##M, λx. snd(fst(x)) = fst(snd(x)))"
using separation_in_ctm[where env="[]" and φ="is_sndfst_eq_fstsnd_fm(0)" and Q=sndfst_eq_fstsnd]
nonempty sndfst_eq_fstsnd_abs arity_is_sndfst_eq_fstsnd_fm
unfolding sndfst_eq_fstsnd_def
by simp
end
end