# Theory Discipline_Function

```section‹Basic relativization of function spaces›

theory Discipline_Function
imports
Arities
begin

subsection‹Discipline for \<^term>‹fst› and \<^term>‹snd››

arity_theorem for "empty_fm"
arity_theorem for "upair_fm"
arity_theorem for "pair_fm"
definition
is_fst :: "(i⇒o)⇒i⇒i⇒o" where
"is_fst(M,x,t) ≡ (∃z[M]. pair(M,t,z,x)) ∨
(¬(∃z[M]. ∃w[M]. pair(M,w,z,x)) ∧ empty(M,t))"
synthesize "fst" from_definition "is_fst"
notation fst_fm (‹⋅fst'(_') is _⋅›)

arity_theorem for "fst_fm"

definition fst_rel ::  "[i⇒o,i] ⇒ i"  where
"fst_rel(M,p) ≡ THE d. M(d) ∧ is_fst(M,p,d)"

definition
is_snd :: "(i⇒o)⇒i⇒i⇒o" where
"is_snd(M,x,t) ≡ (∃z[M]. pair(M,z,t,x)) ∨
(¬(∃z[M]. ∃w[M]. pair(M,z,w,x)) ∧ empty(M,t))"
synthesize "snd" from_definition "is_snd"
notation snd_fm (‹⋅snd'(_') is _⋅›)
arity_theorem for "snd_fm"

definition snd_rel ::  "[i⇒o,i] ⇒ i"  where
"snd_rel(M,p) ≡ THE d. M(d) ∧ is_snd(M,p,d)"

context M_trans
begin

lemma fst_snd_closed:
assumes "M(p)"
shows "M(fst(p)) ∧ M(snd(p))"
unfolding fst_def snd_def using assms
by (cases "∃a. ∃b. p = ⟨a, b⟩";auto)

lemma fst_closed[intro,simp]: "M(x) ⟹ M(fst(x))"
using fst_snd_closed by auto

lemma snd_closed[intro,simp]: "M(x) ⟹ M(snd(x))"
using fst_snd_closed by auto

lemma fst_abs [absolut]:
"⟦M(p); M(x) ⟧ ⟹ is_fst(M,p,x) ⟷ x = fst(p)"
unfolding is_fst_def fst_def
by (cases "∃a. ∃b. p = ⟨a, b⟩";auto)

lemma snd_abs [absolut]:
"⟦M(p); M(y) ⟧ ⟹ is_snd(M,p,y) ⟷ y = snd(p)"
unfolding is_snd_def snd_def
by (cases "∃a. ∃b. p = ⟨a, b⟩";auto)

lemma empty_rel_abs : "M(x) ⟹ M(0) ⟹ x = 0 ⟷ x = (THE d. M(d) ∧ empty(M, d))"
unfolding the_def
using transM
by auto

lemma fst_rel_abs:
assumes "M(p)"
shows "fst_rel(M,p) = fst(p)"
using fst_abs assms
unfolding fst_def fst_rel_def
by (cases "∃a. ∃b. p = ⟨a, b⟩";auto;rule_tac the_equality[symmetric],simp_all)

lemma snd_rel_abs:
assumes "M(p)"
shows " snd_rel(M,p) = snd(p)"
using snd_abs assms
unfolding snd_def snd_rel_def
by (cases "∃a. ∃b. p = ⟨a, b⟩";auto;rule_tac the_equality[symmetric],simp_all)

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

subsection‹Discipline for \<^term>‹minimum››

relativize functional "first" "first_rel" external
relativize functional "minimum" "minimum_rel" external
context M_trans
begin

lemma minimum_closed[simp,intro]:
assumes "M(A)"
shows "M(minimum(r,A))"
using first_is_elem the_equality_if transM[OF _ ‹M(A)›]
by(cases "∃x . first(x,A,r)",auto simp:minimum_def)

lemma first_abs :
assumes "M(B)"
shows "first(z,B,r) ⟷ first_rel(M,z,B,r)"
unfolding first_def first_rel_def using assms by auto

lemma minimum_abs:
assumes "M(B)"
shows "minimum(r,B) = minimum_rel(M,r,B)"
proof -
from assms
have "first(b, B, r) ⟷ M(b) ∧ first_rel(M,b,B,r)" for b
using first_abs
proof (auto)
fix b
assume "first_rel(M,b,B,r)"
with ‹M(B)›
have "b∈B" using first_abs first_is_elem by simp
with ‹M(B)›
show "M(b)" using transM[OF ‹b∈B›] by simp
qed
with assms
show ?thesis unfolding minimum_rel_def minimum_def
by simp
qed

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

subsection‹Discipline for \<^term>‹function_space››

definition
is_function_space :: "[i⇒o,i,i,i] ⇒ o"  where
"is_function_space(M,A,B,fs) ≡ M(fs) ∧ is_funspace(M,A,B,fs)"

definition
function_space_rel :: "[i⇒o,i,i] ⇒ i"  where
"function_space_rel(M,A,B) ≡ THE d. is_function_space(M,A,B,d)"

reldb_rem absolute "Pi"

abbreviation
function_space_r :: "[i,i⇒o,i] ⇒ i" (‹_ →⇗_⇖ _› [61,1,61] 60) where
"A →⇗M⇖ B ≡ function_space_rel(M,A,B)"

abbreviation
function_space_r_set ::  "[i,i,i] ⇒ i" (‹_ →⇗_⇖ _› [61,1,61] 60) where
"function_space_r_set(A,M) ≡ function_space_rel(##M,A)"

context M_Pi
begin

lemma is_function_space_uniqueness:
assumes
"M(r)" "M(B)"
"is_function_space(M,r,B,d)" "is_function_space(M,r,B,d')"
shows
"d=d'"
using assms extensionality_trans
unfolding is_function_space_def is_funspace_def
by simp

lemma is_function_space_witness:
assumes "M(A)" "M(B)"
shows "∃d[M]. is_function_space(M,A,B,d)"
proof -
from assms
interpret M_Pi_assumptions M A "λ_. B"
using Pi_replacement Pi_separation
by unfold_locales (auto dest:transM simp add:Sigfun_def)
have "∀f[M]. f ∈ Pi_rel(M,A, λ_. B) ⟷ f ∈ A → B"
using Pi_rel_char by simp
with assms
show ?thesis unfolding is_funspace_def is_function_space_def by auto
qed

lemma is_function_space_closed :
"is_function_space(M,A,B,d) ⟹ M(d)"
unfolding is_function_space_def by simp

― ‹adding closure to simpset and claset›
lemma function_space_rel_closed[intro,simp]:
assumes "M(x)" "M(y)"
shows "M(function_space_rel(M,x,y))"
proof -
have "is_function_space(M, x, y, THE xa. is_function_space(M, x, y, xa))"
using assms
theI[OF ex1I[of "is_function_space(M,x,y)"], OF _ is_function_space_uniqueness[of x y]]
is_function_space_witness
by auto
then show ?thesis
using assms is_function_space_closed
unfolding function_space_rel_def
by blast
qed

lemmas trans_function_space_rel_closed[trans_closed] = transM[OF _ function_space_rel_closed]

lemma is_function_space_iff:
assumes "M(x)" "M(y)" "M(d)"
shows "is_function_space(M,x,y,d) ⟷ d = function_space_rel(M,x,y)"
proof (intro iffI)
assume "d = function_space_rel(M,x,y)"
moreover
note assms
moreover from this
obtain e where "M(e)" "is_function_space(M,x,y,e)"
using is_function_space_witness by blast
ultimately
show "is_function_space(M, x, y, d)"
using is_function_space_uniqueness[of x y] is_function_space_witness
theI[OF ex1I[of "is_function_space(M,x,y)"], OF _ is_function_space_uniqueness[of x y], of e]
unfolding function_space_rel_def
by auto
next
assume "is_function_space(M, x, y, d)"
with assms
show "d = function_space_rel(M,x,y)"
using is_function_space_uniqueness unfolding function_space_rel_def
by (blast del:the_equality intro:the_equality[symmetric])
qed

lemma def_function_space_rel:
assumes "M(A)" "M(y)"
shows "function_space_rel(M,A,y) = Pi_rel(M,A,λ_. y)"
proof -
from assms
interpret M_Pi_assumptions M A "λ_. y"
using Pi_replacement Pi_separation
by unfold_locales (auto dest:transM simp add:Sigfun_def)
from assms
have "x∈function_space_rel(M,A,y) ⟷ x∈Pi_rel(M,A,λ_. y)" if "M(x)" for x
using that
is_function_space_iff[of A y, OF _ _ function_space_rel_closed, of A y]
def_Pi_rel Pi_rel_char mbnr.Pow_rel_char
unfolding is_function_space_def is_funspace_def by (simp add:Pi_def)
with assms
show ?thesis ― ‹At this point, quoting "trans\_rules" doesn't work›
using transM[OF _ function_space_rel_closed, OF _ ‹M(A)› ‹M(y)›]
transM[OF _ Pi_rel_closed] by blast
qed

lemma function_space_rel_char:
assumes "M(A)" "M(y)"
shows "function_space_rel(M,A,y) = {f ∈ A → y. M(f)}"
proof -
from assms
interpret M_Pi_assumptions M A "λ_. y"
using Pi_replacement Pi_separation
by unfold_locales (auto dest:transM simp add:Sigfun_def)
show ?thesis
using assms def_function_space_rel Pi_rel_char
by simp
qed

lemma mem_function_space_rel_abs:
assumes "M(A)" "M(y)" "M(f)"
shows "f ∈ function_space_rel(M,A,y) ⟷  f ∈ A → y"
using assms function_space_rel_char by simp

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

locale M_N_Pi = M:M_Pi + N:M_Pi N for N +
assumes
M_imp_N:"M(x) ⟹ N(x)"
begin

lemma function_space_rel_transfer: "M(A) ⟹ M(B) ⟹
function_space_rel(M,A,B) ⊆ function_space_rel(N,A,B)"
using M.function_space_rel_char N.function_space_rel_char
by (auto dest!:M_imp_N)

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

abbreviation
"is_apply ≡ fun_apply"
― ‹It is not necessary to perform the Discipline for \<^term>‹is_apply›
since it is absolute in this context›

subsection‹Discipline for \<^term>‹Collect› terms.›

text‹We have to isolate the predicate involved and apply the
Discipline to it.›

definition ― ‹completely relational›
injP_rel:: "[i⇒o,i,i]⇒o" where
"injP_rel(M,A,f) ≡ ∀w[M]. ∀x[M]. ∀fw[M]. ∀fx[M]. w∈A ∧ x∈A ∧
is_apply(M,f,w,fw) ∧ is_apply(M,f,x,fx) ∧ fw=fx⟶ w=x"

synthesize "injP_rel" from_definition assuming "nonempty"

arity_theorem for "injP_rel_fm"

context M_basic
begin

― ‹I'm undecided on keeping the relative quantifiers here.
Same with \<^term>‹surjP› below. It might relieve from changing
@{thm [source] exI allI} to @{thm [source] rexI rallI} in some proofs.
I wonder if this escalates well. Assuming that all terms
appearing in the "def\_" theorem are in \<^term>‹M› and using
@{thm [source] transM}, it might do.›
lemma def_injP_rel:
assumes
"M(A)" "M(f)"
shows
"injP_rel(M,A,f) ⟷ (∀w[M]. ∀x[M]. w∈A ∧ x∈A ∧ f`w=f`x ⟶ w=x)"
using assms unfolding injP_rel_def by simp

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

subsection‹Discipline for \<^term>‹inj››

definition ― ‹completely relational›
is_inj   :: "[i⇒o,i,i,i]⇒o"  where
"is_inj(M,A,B,I) ≡ M(I) ∧ (∃F[M]. is_function_space(M,A,B,F) ∧
is_Collect(M,F,injP_rel(M,A),I))"

declare typed_function_iff_sats Collect_iff_sats [iff_sats]

synthesize "is_funspace" from_definition assuming "nonempty"
arity_theorem for "is_funspace_fm"

synthesize "is_function_space" from_definition assuming "nonempty"
notation is_function_space_fm (‹⋅_ → _ is _⋅›)

arity_theorem for "is_function_space_fm"

synthesize "is_inj" from_definition assuming "nonempty"
notation is_inj_fm (‹⋅inj'(_,_') is _⋅›)

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 simp:pred_Un_distrib arity)

definition
inj_rel :: "[i⇒o,i,i] ⇒ i" (‹inj⇗_⇖'(_,_')›) where
"inj_rel(M,A,B) ≡ THE d. is_inj(M,A,B,d)"

abbreviation
inj_r_set ::  "[i,i,i] ⇒ i" (‹inj⇗_⇖'(_,_')›) where
"inj_r_set(M) ≡ inj_rel(##M)"

locale M_inj = M_Pi +
assumes
injP_separation: "M(r) ⟹ separation(M,injP_rel(M, r))"
begin

lemma is_inj_uniqueness:
assumes
"M(r)" "M(B)"
"is_inj(M,r,B,d)" "is_inj(M,r,B,d')"
shows
"d=d'"
using assms is_function_space_iff extensionality_trans
unfolding is_inj_def by simp

lemma is_inj_witness: "M(r) ⟹ M(B)⟹ ∃d[M]. is_inj(M,r,B,d)"
using injP_separation is_function_space_iff
unfolding is_inj_def by simp

lemma is_inj_closed :
"is_inj(M,x,y,d) ⟹ M(d)"
unfolding is_inj_def by simp

lemma inj_rel_closed[intro,simp]:
assumes "M(x)" "M(y)"
shows "M(inj_rel(M,x,y))"
proof -
have "is_inj(M, x, y, THE xa. is_inj(M, x, y, xa))"
using assms
theI[OF ex1I[of "is_inj(M,x,y)"], OF _ is_inj_uniqueness[of x y]]
is_inj_witness
by auto
then show ?thesis
using assms is_inj_closed
unfolding inj_rel_def
by blast
qed

lemmas trans_inj_rel_closed[trans_closed] = transM[OF _ inj_rel_closed]

lemma inj_rel_iff:
assumes "M(x)" "M(y)" "M(d)"
shows "is_inj(M,x,y,d) ⟷ d = inj_rel(M,x,y)"
proof (intro iffI)
assume "d = inj_rel(M,x,y)"
moreover
note assms
moreover from this
obtain e where "M(e)" "is_inj(M,x,y,e)"
using is_inj_witness by blast
ultimately
show "is_inj(M, x, y, d)"
using is_inj_uniqueness[of x y] is_inj_witness
theI[OF ex1I[of "is_inj(M,x,y)"], OF _ is_inj_uniqueness[of x y], of e]
unfolding inj_rel_def
by auto
next
assume "is_inj(M, x, y, d)"
with assms
show "d = inj_rel(M,x,y)"
using is_inj_uniqueness unfolding inj_rel_def
by (blast del:the_equality intro:the_equality[symmetric])
qed

lemma def_inj_rel:
assumes "M(A)" "M(B)"
shows "inj_rel(M,A,B) =
{f ∈ function_space_rel(M,A,B).  ∀w[M]. ∀x[M]. w∈A ∧ x∈A ∧ f`w = f`x ⟶ w=x}"
(is "_ = Collect(_,?P)")
proof -
from assms
have "inj_rel(M,A,B) ⊆ function_space_rel(M,A,B)"
using inj_rel_iff[of A B "inj_rel(M,A,B)"] is_function_space_iff
unfolding is_inj_def by auto
moreover from assms
have "f ∈ inj_rel(M,A,B) ⟹ ?P(f)" for f
using inj_rel_iff[of A B "inj_rel(M,A,B)"] is_function_space_iff
def_injP_rel transM[OF _ function_space_rel_closed, OF _ ‹M(A)› ‹M(B)›]
unfolding is_inj_def by auto
moreover from assms
have "f ∈ function_space_rel(M,A,B) ⟹ ?P(f) ⟹ f ∈ inj_rel(M,A,B)" for f
using inj_rel_iff[of A B "inj_rel(M,A,B)"] is_function_space_iff
def_injP_rel transM[OF _ function_space_rel_closed, OF _ ‹M(A)› ‹M(B)›]
unfolding is_inj_def by auto
ultimately
show ?thesis by force
qed

lemma inj_rel_char:
assumes "M(A)" "M(B)"
shows "inj_rel(M,A,B) = {f ∈ inj(A,B). M(f)}"
proof -
from assms
interpret M_Pi_assumptions M A "λ_. B"
using Pi_replacement Pi_separation
by unfold_locales (auto dest:transM simp add:Sigfun_def)
from assms
show ?thesis
using def_inj_rel[OF assms] def_function_space_rel[OF assms]
transM[OF _ ‹M(A)›] Pi_rel_char
unfolding inj_def
by auto
qed

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

locale M_N_inj = M:M_inj + N:M_inj N for N +
assumes
M_imp_N:"M(x) ⟹ N(x)"
begin

lemma inj_rel_transfer: "M(A) ⟹ M(B) ⟹ inj_rel(M,A,B) ⊆ inj_rel(N,A,B)"
using M.inj_rel_char N.inj_rel_char
by (auto dest!:M_imp_N)

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

subsection‹Discipline for \<^term>‹surj››

definition
surjP_rel:: "[i⇒o,i,i,i]⇒o" where
"surjP_rel(M,A,B,f) ≡
∀y[M]. ∃x[M]. ∃fx[M]. y∈B ⟶ x∈A ∧ is_apply(M,f,x,fx) ∧ fx=y"

synthesize "surjP_rel" from_definition assuming "nonempty"

context M_basic
begin

lemma def_surjP_rel:
assumes
"M(A)" "M(B)" "M(f)"
shows
"surjP_rel(M,A,B,f) ⟷ (∀y[M]. ∃x[M]. y∈B ⟶ x∈A ∧ f`x=y)"
using assms unfolding surjP_rel_def by auto

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

subsection‹Discipline for \<^term>‹surj››

definition ― ‹completely relational›
is_surj   :: "[i⇒o,i,i,i]⇒o"  where
"is_surj(M,A,B,I) ≡ M(I) ∧ (∃F[M]. is_function_space(M,A,B,F) ∧
is_Collect(M,F,surjP_rel(M,A,B),I))"

synthesize "is_surj" from_definition assuming "nonempty"
notation is_surj_fm (‹⋅surj'(_,_') is _⋅›)

definition
surj_rel :: "[i⇒o,i,i] ⇒ i" (‹surj⇗_⇖'(_,_')›) where
"surj_rel(M,A,B) ≡ THE d. is_surj(M,A,B,d)"

abbreviation
surj_r_set ::  "[i,i,i] ⇒ i" (‹surj⇗_⇖'(_,_')›) where
"surj_r_set(M) ≡ surj_rel(##M)"

locale M_surj = M_Pi +
assumes
surjP_separation: "M(A)⟹M(B)⟹separation(M,λx. surjP_rel(M,A,B,x))"
begin

lemma is_surj_uniqueness:
assumes
"M(r)" "M(B)"
"is_surj(M,r,B,d)" "is_surj(M,r,B,d')"
shows
"d=d'"
using assms is_function_space_iff extensionality_trans
unfolding is_surj_def by simp

lemma is_surj_witness: "M(r) ⟹ M(B)⟹ ∃d[M]. is_surj(M,r,B,d)"
using surjP_separation is_function_space_iff
unfolding is_surj_def by simp

lemma is_surj_closed :
"is_surj(M,x,y,d) ⟹ M(d)"
unfolding is_surj_def by simp

lemma surj_rel_closed[intro,simp]:
assumes "M(x)" "M(y)"
shows "M(surj_rel(M,x,y))"
proof -
have "is_surj(M, x, y, THE xa. is_surj(M, x, y, xa))"
using assms
theI[OF ex1I[of "is_surj(M,x,y)"], OF _ is_surj_uniqueness[of x y]]
is_surj_witness
by auto
then show ?thesis
using assms is_surj_closed
unfolding surj_rel_def
by blast
qed

lemmas trans_surj_rel_closed[trans_closed] = transM[OF _ surj_rel_closed]

lemma surj_rel_iff:
assumes "M(x)" "M(y)" "M(d)"
shows "is_surj(M,x,y,d) ⟷ d = surj_rel(M,x,y)"
proof (intro iffI)
assume "d = surj_rel(M,x,y)"
moreover
note assms
moreover from this
obtain e where "M(e)" "is_surj(M,x,y,e)"
using is_surj_witness by blast
ultimately
show "is_surj(M, x, y, d)"
using is_surj_uniqueness[of x y] is_surj_witness
theI[OF ex1I[of "is_surj(M,x,y)"], OF _ is_surj_uniqueness[of x y], of e]
unfolding surj_rel_def
by auto
next
assume "is_surj(M, x, y, d)"
with assms
show "d = surj_rel(M,x,y)"
using is_surj_uniqueness unfolding surj_rel_def
by (blast del:the_equality intro:the_equality[symmetric])
qed

lemma def_surj_rel:
assumes "M(A)" "M(B)"
shows "surj_rel(M,A,B) =
{f ∈ function_space_rel(M,A,B). ∀y[M]. ∃x[M]. y∈B ⟶ x∈A ∧ f`x=y }"
(is "_ = Collect(_,?P)")
proof -
from assms
have "surj_rel(M,A,B) ⊆ function_space_rel(M,A,B)"
using surj_rel_iff[of A B "surj_rel(M,A,B)"] is_function_space_iff
unfolding is_surj_def by auto
moreover from assms
have "f ∈ surj_rel(M,A,B) ⟹ ?P(f)" for f
using surj_rel_iff[of A B "surj_rel(M,A,B)"] is_function_space_iff
def_surjP_rel transM[OF _ function_space_rel_closed, OF _ ‹M(A)› ‹M(B)›]
unfolding is_surj_def by auto
moreover from assms
have "f ∈ function_space_rel(M,A,B) ⟹ ?P(f) ⟹ f ∈ surj_rel(M,A,B)" for f
using surj_rel_iff[of A B "surj_rel(M,A,B)"] is_function_space_iff
def_surjP_rel transM[OF _ function_space_rel_closed, OF _ ‹M(A)› ‹M(B)›]
unfolding is_surj_def by auto
ultimately
show ?thesis by force
qed

lemma surj_rel_char:
assumes "M(A)" "M(B)"
shows "surj_rel(M,A,B) = {f ∈ surj(A,B). M(f)}"
proof -
from assms
interpret M_Pi_assumptions M A "λ_. B"
using Pi_replacement Pi_separation
by unfold_locales (auto dest:transM simp add:Sigfun_def)
from assms
show ?thesis
using def_surj_rel[OF assms] def_function_space_rel[OF assms]
transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›] Pi_rel_char
unfolding surj_def
by auto
qed

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

locale M_N_surj = M:M_surj + N:M_surj N for N +
assumes
M_imp_N:"M(x) ⟹ N(x)"
begin

lemma surj_rel_transfer: "M(A) ⟹ M(B) ⟹ surj_rel(M,A,B) ⊆ surj_rel(N,A,B)"
using M.surj_rel_char N.surj_rel_char
by (auto dest!:M_imp_N)

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

subsection‹Discipline for \<^term>‹Inter››

definition
is_Int :: "[i⇒o,i,i,i]⇒o"  where
"is_Int(M,A,B,I) ≡ M(I) ∧ (∀x[M]. x ∈ I ⟷ x ∈ A ∧ x ∈ B)"

reldb_rem relational "inter"

synthesize "is_Int" from_definition assuming "nonempty"
notation is_Int_fm (‹_ ∩ _ is _›)

context M_basic
begin

lemma is_Int_closed :
"is_Int(M,A,B,I) ⟹ M(I)"
unfolding is_Int_def by simp

lemma is_Int_abs:
assumes
"M(A)" "M(B)" "M(I)"
shows
"is_Int(M,A,B,I) ⟷ I = A ∩ B"
using assms transM[OF _ ‹M(B)›] transM[OF _ ‹M(I)›]
unfolding is_Int_def by blast

lemma is_Int_uniqueness:
assumes
"M(r)" "M(B)"
"is_Int(M,r,B,d)" "is_Int(M,r,B,d')"
shows
"d=d'"
proof -
have "M(d)" and "M(d')"
using assms is_Int_closed by simp+
then show ?thesis
using assms is_Int_abs by simp
qed

text‹Note: @{thm [source] Int_closed} already in \<^theory>‹ZF-Constructible.Relative›.›

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

subsection‹Discipline for \<^term>‹bij››

relativize functional "bij" "bij_rel" external
relationalize "bij_rel" "is_bij"

synthesize "is_bij" from_definition assuming "nonempty"
notation is_bij_fm (‹⋅bij'(_,_') is _⋅›)

abbreviation
bij_r_class ::  "[i⇒o,i,i] ⇒ i" (‹bij⇗_⇖'(_,_')›) where
"bij_r_class ≡ bij_rel"

abbreviation
bij_r_set ::  "[i,i,i] ⇒ i" (‹bij⇗_⇖'(_,_')›) where
"bij_r_set(M) ≡ bij_rel(##M)"

locale M_Perm = M_Pi + M_inj + M_surj
begin

lemma is_bij_closed : "is_bij(M,f,y,d) ⟹ M(d)"
unfolding is_bij_def using is_Int_closed is_inj_witness is_surj_witness by auto

lemma bij_rel_closed[intro,simp]:
assumes "M(x)" "M(y)"
shows "M(bij_rel(M,x,y))"
unfolding bij_rel_def
using assms Int_closed surj_rel_closed inj_rel_closed
by auto

lemmas trans_bij_rel_closed[trans_closed] = transM[OF _ bij_rel_closed]

lemma bij_rel_iff:
assumes "M(x)" "M(y)" "M(d)"
shows "is_bij(M,x,y,d) ⟷ d = bij_rel(M,x,y)"
unfolding is_bij_def bij_rel_def
using assms surj_rel_iff inj_rel_iff is_Int_abs
by auto

lemma def_bij_rel:
assumes "M(A)" "M(B)"
shows "bij_rel(M,A,B) = inj_rel(M,A,B) ∩ surj_rel(M,A,B)"
using assms bij_rel_iff inj_rel_iff surj_rel_iff
is_Int_abs― ‹For absolute terms, "\_abs" replaces "\_iff".
Also, in this case "\_closed" is in the simpset.›
unfolding is_bij_def by simp

lemma bij_rel_char:
assumes "M(A)" "M(B)"
shows "bij_rel(M,A,B) = {f ∈ bij(A,B). M(f)}"
using assms def_bij_rel inj_rel_char surj_rel_char
unfolding bij_def― ‹Unfolding this might be a pattern already›
by auto

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

locale M_N_Perm = M_N_Pi + M_N_inj + M_N_surj + M:M_Perm + N:M_Perm N

begin

lemma bij_rel_transfer: "M(A) ⟹ M(B) ⟹ bij_rel(M,A,B) ⊆ bij_rel(N,A,B)"
using M.bij_rel_char N.bij_rel_char
by (auto dest!:M_imp_N)

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

context M_Perm
begin

lemma mem_bij_rel: "⟦f ∈ bij⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈bij(A,B)"
using bij_rel_char by simp

lemma mem_inj_rel: "⟦f ∈ inj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈inj(A,B)"
using inj_rel_char by simp

lemma mem_surj_rel: "⟦f ∈ surj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈surj(A,B)"
using surj_rel_char by simp

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

subsection‹Discipline for \<^term>‹eqpoll››

relativize functional "eqpoll" "eqpoll_rel" external
relationalize "eqpoll_rel" "is_eqpoll"

synthesize "is_eqpoll" from_definition assuming "nonempty"
arity_theorem for "is_eqpoll_fm"
notation is_eqpoll_fm (‹⋅_ ≈ _⋅›)

context M_Perm begin

is_iff_rel for "eqpoll"
using bij_rel_iff unfolding is_eqpoll_def eqpoll_rel_def by simp

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

abbreviation
eqpoll_r :: "[i,i⇒o,i] => o" (‹_ ≈⇗_⇖ _› [51,1,51] 50) where
"A ≈⇗M⇖ B ≡ eqpoll_rel(M,A,B)"

abbreviation
eqpoll_r_set ::  "[i,i,i] ⇒ o" (‹_ ≈⇗_⇖ _› [51,1,51] 50) where
"eqpoll_r_set(A,M) ≡ eqpoll_rel(##M,A)"

context M_Perm
begin

lemma def_eqpoll_rel:
assumes
"M(A)" "M(B)"
shows
"eqpoll_rel(M,A,B) ⟷ (∃f[M]. f ∈ bij_rel(M,A,B))"
using assms bij_rel_iff
unfolding eqpoll_rel_def by simp

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

context M_N_Perm
begin

text‹The next lemma is not part of the discipline›
lemma eqpoll_rel_transfer: assumes "A ≈⇗M⇖ B" "M(A)" "M(B)"
shows "A ≈⇗N⇖ B"
proof -
note assms
moreover from this
obtain f where "f ∈ bij⇗M⇖(A,B)" "N(f)"
using M.def_eqpoll_rel by (auto dest!:M_imp_N)
moreover from calculation
have "f ∈ bij⇗N⇖(A,B)"
using bij_rel_transfer by (auto)
ultimately
show ?thesis
using N.def_eqpoll_rel by (blast dest!:M_imp_N)
qed

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

subsection‹Discipline for \<^term>‹lepoll››

relativize functional "lepoll" "lepoll_rel" external
relationalize "lepoll_rel" "is_lepoll"

synthesize "is_lepoll" from_definition assuming "nonempty"
notation is_lepoll_fm (‹⋅_ ≲ _⋅›)
arity_theorem for "is_lepoll_fm"

context M_inj begin

is_iff_rel for "lepoll"
using inj_rel_iff unfolding is_lepoll_def lepoll_rel_def by simp

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

abbreviation
lepoll_r :: "[i,i⇒o,i] => o" (‹_ ≲⇗_⇖ _› [51,1,51] 50) where
"A ≲⇗M⇖ B ≡ lepoll_rel(M,A,B)"

abbreviation
lepoll_r_set ::  "[i,i,i] ⇒ o" (‹_ ≲⇗_⇖ _› [51,1,51] 50) where
"lepoll_r_set(A,M) ≡ lepoll_rel(##M,A)"

context M_Perm
begin

lemma def_lepoll_rel:
assumes
"M(A)" "M(B)"
shows
"lepoll_rel(M,A,B) ⟷ (∃f[M]. f ∈ inj_rel(M,A,B))"
using assms inj_rel_iff
unfolding lepoll_rel_def by simp

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

context M_N_Perm
begin

― ‹This lemma is not part of the discipline.›
lemma lepoll_rel_transfer: assumes "A ≲⇗M⇖ B" "M(A)" "M(B)"
shows "A ≲⇗N⇖ B"
proof -
note assms
moreover from this
obtain f where "f ∈ inj⇗M⇖(A,B)" "N(f)"
using M.def_lepoll_rel by (auto dest!:M_imp_N)
moreover from calculation
have "f ∈ inj⇗N⇖(A,B)"
using inj_rel_transfer by (auto)
ultimately
show ?thesis
using N.def_lepoll_rel by (blast dest!:M_imp_N)
qed

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

subsection‹Discipline for \<^term>‹lesspoll››

relativize functional "lesspoll" "lesspoll_rel" external
relationalize "lesspoll_rel" "is_lesspoll"

synthesize "is_lesspoll" from_definition assuming "nonempty"
notation is_lesspoll_fm (‹⋅_ ≺ _⋅›)
arity_theorem for "is_lesspoll_fm"

context M_Perm begin

is_iff_rel for "lesspoll"
using is_lepoll_iff is_eqpoll_iff
unfolding is_lesspoll_def lesspoll_rel_def by simp

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

abbreviation
lesspoll_r :: "[i,i⇒o,i] => o" (‹_ ≺⇗_⇖ _› [51,1,51] 50) where
"A ≺⇗M⇖ B ≡ lesspoll_rel(M,A,B)"

abbreviation
lesspoll_r_set ::  "[i,i,i] ⇒ o" (‹_ ≺⇗_⇖ _› [51,1,51] 50) where
"lesspoll_r_set(A,M) ≡ lesspoll_rel(##M,A)"

text‹Since \<^term>‹lesspoll_rel› is defined as a propositional
combination of older terms, there is no need for a separate ``def''
theorem for it.›

text‹Note that \<^term>‹lesspoll_rel› is neither \$\Sigma_1^{\mathit{ZF}}\$ nor
\$\Pi_1^{\mathit{ZF}}\$, so there is no ``transfer'' theorem for it.›

definition
Powapply :: "[i,i] ⇒ i"  where
"Powapply(f,y) ≡ Pow(f`y)"

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

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

end```