Theory Discipline_Function

theory Discipline_Function
  imports
    Arities
begin

(**********************************************************)
paragraphDiscipline for termfst


(* ftype(p) ≡ THE a. ∃b. p = ⟨a, b⟩ *)
arity_theorem for "empty_fm"
arity_theorem for "upair_fm"
arity_theorem for "pair_fm"
definition
  is_fst :: "(io)iio" 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 ::  "[io,i]  i"  where
  "fst_rel(M,p)  THE d. M(d)  is_fst(M,p,d)"

reldb_add relational "fst" "is_fst"
reldb_add functional "fst" "fst_rel"

definition
  is_snd :: "(io)iio" 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 ::  "[io,i]  i"  where
  "snd_rel(M,p)  THE d. M(d)  is_snd(M,p,d)"


reldb_add relational "snd" "is_snd"
reldb_add functional "snd" "snd_rel"

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(p) = fst_rel(M,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(p) = snd_rel(M,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 ― ‹localeM_trans

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

(* FIXME: find a naming convention for absoluteness results like this.*)
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 "bB" using first_abs first_is_elem by simp
    with M(B)
    show "M(b)" using transM[OF bB] by simp
  qed
  with assms
  show ?thesis unfolding minimum_rel_def minimum_def
    by simp
qed

end ― ‹localeM_trans

subsectionDiscipline for termfunction_space

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

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

reldb_rem absolute "Pi"
reldb_add relational "Pi" "is_function_space"
reldb_add functional "Pi" "function_space_rel"

abbreviation
  function_space_r :: "[i,io,i]  i" (_ →⇗_ _ [61,1,61] 60) where
  "A →⇗MB  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 function_space_rel_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 "xfunction_space_rel(M,A,y)  xPi_rel(M,A,λ_. y)" if "M(x)" for x
    using that
      function_space_rel_iff[of A y, OF _ _ function_space_rel_closed, of A y]
      def_Pi_rel Pi_rel_char 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 ― ‹localeM_Pi



(*
definition
  is_function_space :: "[i⇒o,i,i,i] ⇒ o"  where
  "is_function_space(M,A,B,fs) ≡ is_Pi(M,A,λ_. B,fs)"

definition
  function_space_rel :: "[i⇒o,i,i] ⇒ i"  where
  "function_space_rel(M,A,B) ≡ Pi_rel(M,A,λ_. B)"

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 is_Pi_uniqueness[of r "λ_. B"] assms
  unfolding is_function_space_def
  by blast

lemma is_function_space_witness:
  assumes "M(A)" "M(B)"
  shows "∃d[M]. is_function_space(M,A,B,d)"
  using is_Pi_witness[of A "λ_. B"] assms
  unfolding is_function_space_def
  by simp

― ‹adding closure to simpset and claset›
lemma function_space_rel_closed[intro,simp]:
  "M(x) ⟹ M(y) ⟹ M(function_space_rel(M,x,y))"
  unfolding function_space_rel_def
  by simp

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

lemma function_space_rel_iff:
  assumes "M(x)" "M(y)" "M(d)"
  shows "is_function_space(M,x,y,d) ⟷ d = function_space_rel(M,x,y)"
  using Pi_rel_iff[of x "λ_. y"] assms
  unfolding is_function_space_def function_space_rel_def
  by simp

lemma def_function_space_rel:
  assumes "M(A)" "M(y)"
  shows "A →M y = PiM(A,λ_. y)"
proof -
  from assms
  interpret M_Pi_assumptions M A "λ_. y"
    using Pi_replacement Pi_separation
    by unfold_locales (simp_all add:Sigfun_def)
  from assms
  have "x∈A →M y ⟷ x∈PiM(A,λ_. y)" if "M(x)" for x
    using that
      function_space_rel_iff[of A y, OF _ _ function_space_rel_closed, of A y]
      def_Pi_rel Pi_rel_char Pow_rel_char
    unfolding 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 "A →M y = {f ∈ A → y. M(f)}"
proof -
  from assms
  interpret M_Pi_assumptions M A "λ_. y"
    using Pi_replacement Pi_separation
    by unfold_locales (simp_all 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 ∈ A →M 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 ― ‹localeM_N_Pi

(*****************  end Discipline  ***********************)

abbreviation
  "is_apply  fun_apply"
  ― ‹It is not necessary to perform the Discipline for termis_apply
  since it is absolute in this context

subsectionDiscipline for termCollect terms.

textWe have to isolate the predicate involved and apply the
Discipline to it.

(*************** Discipline for injP ******************)


definition (* completely relational *)
  injP_rel:: "[io,i,i]o" where
  "injP_rel(M,A,f)  w[M]. x[M]. fw[M]. fx[M]. wA  xA 
            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 termsurjP below. It might relieve from changing
    @{thm exI allI} to @{thm rexI rallI} in some proofs.
    I wonder if this escalates well. Assuming that all terms
    appearing in the "def\_" theorem are in termM and using
    @{thm transM}, it might do.
lemma def_injP_rel:
  assumes
    "M(A)" "M(f)"
  shows
    "injP_rel(M,A,f)  (w[M]. x[M]. wA  xA  f`w=f`x  w=x)"
  using assms unfolding injP_rel_def by simp

end ― ‹localeM_basic

(******************  end Discipline  **********************)

(**********************************************************)
subsectionDiscipline for terminj

definition (* completely relational *)
  is_inj   :: "[io,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 :: "[io,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 function_space_rel_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 function_space_rel_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]. wA  xA  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)"] function_space_rel_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)"] function_space_rel_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)"] function_space_rel_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 ― ‹localeM_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 ― ‹localeM_N_inj


(***************  end Discipline  *********************)

(*************** Discipline for surjP ******************)

definition
  surjP_rel:: "[io,i,i,i]o" where
  "surjP_rel(M,A,B,f) 
    y[M]. x[M]. fx[M]. yB  xA  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]. yB  xA  f`x=y)"
  using assms unfolding surjP_rel_def by auto

end ― ‹localeM_basic

(******************  end Discipline  **********************)

(**********************************************************)
subsectionDiscipline for termsurj

definition (* completely relational *)
  is_surj   :: "[io,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 :: "[io,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 function_space_rel_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 function_space_rel_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]. yB  xA  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)"] function_space_rel_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)"] function_space_rel_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)"] function_space_rel_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 ― ‹localeM_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 ― ‹localeM_N_surj

(***************  end Discipline  *********************)

definition
  is_Int :: "[io,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"
reldb_add absolute relational "ZF_Base.Int" "is_Int"

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

textNote: @{thm Int_closed} already in theoryZF-Constructible.Relative.

end ― ‹localeM_basic

(**********************************************************)
subsectionDiscipline for termbij

reldb_add functional "inj" "inj_rel"
reldb_add functional relational "inj_rel" "is_inj"
reldb_add functional "surj" "surj_rel"
reldb_add functional relational "surj_rel" "is_surj"
relativize functional "bij" "bij_rel" external
relationalize "bij_rel" "is_bij"

(* definition (* completely relational *)
  is_bij   :: "[i⇒o,i,i,i]⇒o"  where
  "is_bij(M,A,B,bj) ≡ M(bj) ∧ is_hcomp2_2(M,is_Int,is_inj,is_surj,A,B,bj)"

definition
  bij_rel :: "[i⇒o,i,i] ⇒ i" (‹bij_'(_,_')›) where
  "bij_rel(M,A,B) ≡ THE d. is_bij(M,A,B,d)" *)

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

abbreviation
  bij_r_class ::  "[io,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_uniqueness:
  assumes
    "M(A)" "M(B)"
    "is_bij(M,A,B,d)" "is_bij(M,A,B,d')"
  shows
    "d=d'"
  using assms hcomp2_2_uniqueness[of M is_Int is_inj is_surj A B d d']
    is_Int_uniqueness is_inj_uniqueness is_surj_uniqueness
    is_Int_closed is_inj_closed is_surj_closed
  unfolding is_bij_def
  by auto

lemma is_bij_witness: "M(A) ⟹ M(B)⟹ ∃d[M]. is_bij(M,A,B,d)"
  using hcomp2_2_witness[of M is_Int is_inj is_surj A B]
    is_inj_witness is_surj_witness is_Int_abs
  unfolding is_bij_def by simp

lemma is_bij_closed : "is_bij(M,f,y,d) ⟹ M(d)"
  unfolding is_bij_def by simp *)

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

(* lemma bij_rel_closed[intro,simp]:
  assumes "M(x)" "M(y)"
  shows "M(bij_rel(M,x,y))"
proof -
  have "is_bij(M, x, y, THE xa. is_bij(M, x, y, xa))"
    using assms
          theI[OF ex1I[of "λd. is_bij(M,x,y,d)"], OF _ is_bij_uniqueness[of x y]]
          is_bij_witness
    by auto
  then show ?thesis
    using assms is_bij_closed
    unfolding bij_rel_def
    by blast
qed *)

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

(*proof (intro iffI)
  assume "d = bij_rel(M,x,y)"
  moreover
  note assms
  moreover from this
  obtain e where "M(e)" "is_bij(M,x,y,e)"
    using is_bij_witness by blast)
  ultimately
  show "is_bij(M, x, y, d)"
    using is_bij_uniqueness[of x y] is_bij_witness
      theI[OF ex1I[of "is_bij(M,x,y)"], OF _ is_bij_uniqueness[of x y], of e]
    unfolding bij_rel_def
    by auto)
next
  assume "is_bij(M, x, y, d)"
  with assms
  show "d = bij_rel(M,x,y)"
    using is_bij_uniqueness unfolding bij_rel_def
    by (blast del:the_equality intro:the_equality[symmetric]))
qed*)

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 ― ‹localeM_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 ― ‹localeM_N_Perm

(***************  end Discipline  *********************)

(******************************************************)
subsectionDiscipline for termeqpoll

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 ― ‹localeM_Perm

abbreviation
  eqpoll_r :: "[i,io,i] => o" (_ ≈⇗_ _ [51,1,51] 50) where
  "A ≈⇗MB  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 ― ‹localeM_Perm

context M_N_Perm
begin

(* the next lemma is not part of the discipline *)
lemma eqpoll_rel_transfer: assumes "A ≈⇗MB" "M(A)" "M(B)"
  shows "A ≈⇗NB"
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 ― ‹localeM_N_Perm

(******************  end Discipline  ******************)

(******************************************************)
subsectionDiscipline for termlepoll

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 ― ‹localeM_inj

abbreviation
  lepoll_r :: "[i,io,i] => o" (_ ≲⇗_ _ [51,1,51] 50) where
  "A ≲⇗MB  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 ― ‹localeM_Perm

context M_N_Perm
begin

(* the next lemma is not part of the discipline *)
lemma lepoll_rel_transfer: assumes "A ≲⇗MB" "M(A)" "M(B)"
  shows "A ≲⇗NB"
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 ― ‹localeM_N_Perm

(******************  end Discipline  ******************)

(******************************************************)
subsectionDiscipline for termlesspoll

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 ― ‹localeM_Perm

abbreviation
  lesspoll_r :: "[i,io,i] => o" (_ ≺⇗_ _ [51,1,51] 50) where
  "A ≺⇗MB  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)"

textSince termlesspoll_rel is defined as a propositional
combination of older terms, there is no need for a separate ``def''
theorem for it.

textNote that termlesspoll_rel is neither $\Sigma_1^{\mathit{ZF}}$ nor
 $\Pi_1^{\mathit{ZF}}$, so there is no ``transfer'' theorem for it.



end