Theory Discipline_Function

theory Discipline_Function
  imports
    Arities
begin

(**********************************************************)
paragraph‹Discipline for \<^term>‹fst››


(* 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 :: "(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)"

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

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


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 ― ‹\<^locale>‹M_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 "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"
reldb_add relational "Pi" "is_function_space"
reldb_add functional "Pi" "function_space_rel"

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 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 "x∈function_space_rel(M,A,y) ⟷ x∈Pi_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 ― ‹\<^locale>‹M_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 = Pi⇗M⇖(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∈Pi⇗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_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 ― ‹\<^locale>‹M_N_Pi››

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

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.›

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


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 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 \<^term>‹M› 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]. w∈A ∧ x∈A ∧ f`w=f`x ⟶ w=x)"
  using assms unfolding injP_rel_def by simp

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

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

(**********************************************************)
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 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]. 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)"] 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 ― ‹\<^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››


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

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

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››

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

(**********************************************************)
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 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]. 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)"] 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 ― ‹\<^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››

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

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

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

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

(**********************************************************)
subsection‹Discipline for \<^term>‹bij››

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 ::  "[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_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 ― ‹\<^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››

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

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

(* 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››

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

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

(* the next 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››

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

(******************************************************)
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.›



end