# Theory M_Basic_No_Repl

```theory M_Basic_No_Repl
imports "ZF-Constructible.Relative"
begin

txt‹This locale is exactly \<^locale>‹M_basic› without its only replacement
instance.›

locale M_basic_no_repl = M_trivial +
assumes Inter_separation:
"M(A) ==> separation(M, λx. ∀y[M]. y∈A ⟶ x∈y)"
and Diff_separation:
"M(B) ==> separation(M, λx. x ∉ B)"
and cartprod_separation:
"[| M(A); M(B) |]
==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. y∈B & pair(M,x,y,z)))"
and image_separation:
"[| M(A); M(r) |]
==> separation(M, λy. ∃p[M]. p∈r & (∃x[M]. x∈A & pair(M,x,y,p)))"
and converse_separation:
"M(r) ==> separation(M,
λz. ∃p[M]. p∈r & (∃x[M]. ∃y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
and restrict_separation:
"M(A) ==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. pair(M,x,y,z)))"
and comp_separation:
"[| M(r); M(s) |]
==> separation(M, λxz. ∃x[M]. ∃y[M]. ∃z[M]. ∃xy[M]. ∃yz[M].
pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
xy∈s & yz∈r)"
and pred_separation:
"[| M(r); M(x) |] ==> separation(M, λy. ∃p[M]. p∈r & pair(M,y,x,p))"
and Memrel_separation:
"separation(M, λz. ∃x[M]. ∃y[M]. pair(M,x,y,z) & x ∈ y)"
and is_recfun_separation:
― ‹for well-founded recursion: used to prove ‹is_recfun_equal››
"[| M(r); M(f); M(g); M(a); M(b) |]
==> separation(M,
λx. ∃xa[M]. ∃xb[M].
pair(M,x,a,xa) & xa ∈ r & pair(M,x,b,xb) & xb ∈ r &
(∃fx[M]. ∃gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
fx ≠ gx))"
and power_ax:         "power_ax(M)"

lemma (in M_basic_no_repl) cartprod_iff:
"[| M(A); M(B); M(C) |]
==> cartprod(M,A,B,C) ⟷
(∃p1[M]. ∃p2[M]. powerset(M,A ∪ B,p1) & powerset(M,p1,p2) &
C = {z ∈ p2. ∃x∈A. ∃y∈B. z = <x,y>})"
apply (simp add: Pair_def cartprod_def, safe)
defer 1
apply blast
txt‹Final, difficult case: the left-to-right direction of the theorem.›
apply (insert power_ax, simp add: power_ax_def)
apply (frule_tac x="A ∪ B" and P="λx. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
apply (drule_tac x=z and P="λx. rex(M,Q(x))" for Q in rspec)
apply assumption
apply (blast intro: cartprod_iff_lemma)
done

lemma (in M_basic_no_repl) cartprod_closed_lemma:
"[| M(A); M(B) |] ==> ∃C[M]. cartprod(M,A,B,C)"
apply (simp del: cartprod_abs add: cartprod_iff)
apply (insert power_ax, simp add: power_ax_def)
apply (frule_tac x="A ∪ B" and P="λx. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
apply (drule_tac x=z and P="λx. rex(M,Q(x))" for Q in rspec, auto)
apply (intro rexI conjI, simp+)
apply (insert cartprod_separation [of A B], simp)
done

text‹All the lemmas above are necessary because Powerset is not absolute.
I should have used Replacement instead!›
lemma (in M_basic_no_repl) cartprod_closed [intro,simp]:
"[| M(A); M(B) |] ==> M(A*B)"
by (frule cartprod_closed_lemma, assumption, force)

lemma (in M_basic_no_repl) sum_closed [intro,simp]:
"[| M(A); M(B) |] ==> M(A+B)"

lemma (in M_basic_no_repl) sum_abs [simp]:
"[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) ⟷ (Z = A+B)"
by (simp add: is_sum_def sum_def singleton_0 nat_into_M)

lemma (in M_basic_no_repl) M_converse_iff:
"M(r) ==>
converse(r) =
{z ∈ ⋃(⋃(r)) * ⋃(⋃(r)).
∃p∈r. ∃x[M]. ∃y[M]. p = ⟨x,y⟩ & z = ⟨y,x⟩}"
apply (rule equalityI)
prefer 2 apply (blast dest: transM, clarify, simp)
apply (blast dest: transM)
done

lemma (in M_basic_no_repl) converse_closed [intro,simp]:
"M(r) ==> M(converse(r))"
apply (insert converse_separation [of r], simp)
done

lemma (in M_basic_no_repl) converse_abs [simp]:
"[| M(r); M(z) |] ==> is_converse(M,r,z) ⟷ z = converse(r)"
apply (rule iffI)
prefer 2 apply blast
apply (rule M_equalityI)
apply simp
apply (blast dest: transM)+
done

subsubsection ‹image, preimage, domain, range›

lemma (in M_basic_no_repl) image_closed [intro,simp]:
"[| M(A); M(r) |] ==> M(r``A)"
apply (insert image_separation [of A r], simp)
done

lemma (in M_basic_no_repl) vimage_abs [simp]:
"[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) ⟷ z = r-``A"
apply (rule iffI)
apply (blast intro!: equalityI dest: transM, blast)
done

lemma (in M_basic_no_repl) vimage_closed [intro,simp]:
"[| M(A); M(r) |] ==> M(r-``A)"

subsubsection‹Domain, range and field›

lemma (in M_basic_no_repl) domain_closed [intro,simp]:
"M(r) ==> M(domain(r))"
done

lemma (in M_basic_no_repl) range_closed [intro,simp]:
"M(r) ==> M(range(r))"
done

lemma (in M_basic_no_repl) field_abs [simp]:
"[| M(r); M(z) |] ==> is_field(M,r,z) ⟷ z = field(r)"

lemma (in M_basic_no_repl) field_closed [intro,simp]:
"M(r) ==> M(field(r))"

subsubsection‹Relations, functions and application›

lemma (in M_basic_no_repl) apply_closed [intro,simp]:
"[|M(f); M(a)|] ==> M(f`a)"

lemma (in M_basic_no_repl) apply_abs [simp]:
"[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) ⟷ f`x = y"
apply (simp add: fun_apply_def apply_def, blast)
done

lemma (in M_basic_no_repl) injection_abs [simp]:
"[| M(A); M(f) |] ==> injection(M,A,B,f) ⟷ f ∈ inj(A,B)"
apply (simp add: injection_def apply_iff inj_def)
apply (blast dest: transM [of _ A])
done

lemma (in M_basic_no_repl) surjection_abs [simp]:
"[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) ⟷ f ∈ surj(A,B)"

lemma (in M_basic_no_repl) bijection_abs [simp]:
"[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) ⟷ f ∈ bij(A,B)"

subsubsection‹Composition of relations›

lemma (in M_basic_no_repl) M_comp_iff:
"[| M(r); M(s) |]
==> r O s =
{xz ∈ domain(s) * range(r).
∃x[M]. ∃y[M]. ∃z[M]. xz = ⟨x,z⟩ & ⟨x,y⟩ ∈ s & ⟨y,z⟩ ∈ r}"
apply (rule equalityI)
apply clarify
apply simp
apply  (blast dest:  transM)+
done

lemma (in M_basic_no_repl) comp_closed [intro,simp]:
"[| M(r); M(s) |] ==> M(r O s)"
apply (insert comp_separation [of r s], simp)
done

lemma (in M_basic_no_repl) composition_abs [simp]:
"[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) ⟷ t = r O s"
apply safe
txt‹Proving \<^term>‹composition(M, r, s, r O s)››
prefer 2
apply (blast dest: transM)
txt‹Opposite implication›
apply (rule M_equalityI)
apply (blast del: allE dest: transM)+
done

text‹no longer needed›
lemma (in M_basic_no_repl) restriction_is_function:
"[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
==> function(z)"
apply (unfold function_def, blast)
done

lemma (in M_basic_no_repl) restrict_closed [intro,simp]:
"[| M(A); M(r) |] ==> M(restrict(r,A))"
apply (insert restrict_separation [of A], simp)
done

lemma (in M_basic_no_repl) Inter_closed [intro,simp]:
"M(A) ==> M(⋂(A))"
by (insert Inter_separation, simp add: Inter_def)

lemma (in M_basic_no_repl) Int_closed [intro,simp]:
"[| M(A); M(B) |] ==> M(A ∩ B)"
apply (subgoal_tac "M({A,B})")
apply (frule Inter_closed, force+)
done

lemma (in M_basic_no_repl) Diff_closed [intro,simp]:
"[|M(A); M(B)|] ==> M(A-B)"
by (insert Diff_separation, simp add: Diff_def)

lemma (in M_basic_no_repl) separation_conj:
"[|separation(M,P); separation(M,Q)|] ==> separation(M, λz. P(z) & Q(z))"
by (simp del: separation_closed

lemma (in M_basic_no_repl) separation_disj:
"[|separation(M,P); separation(M,Q)|] ==> separation(M, λz. P(z) | Q(z))"
by (simp del: separation_closed

lemma (in M_basic_no_repl) separation_neg:
"separation(M,P) ==> separation(M, λz. ~P(z))"
by (simp del: separation_closed

lemma (in M_basic_no_repl) separation_imp:
"[|separation(M,P); separation(M,Q)|]
==> separation(M, λz. P(z) ⟶ Q(z))"
by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])

text‹This result is a hint of how little can be done without the Reflection
Theorem.  The quantifier has to be bounded by a set.  We also need another
instance of Separation!›
lemma (in M_basic_no_repl) separation_rall:
"[|M(Y); ∀y[M]. separation(M, λx. P(x,y));
∀z[M]. strong_replacement(M, λx y. y = {u ∈ z . P(u,x)})|]
==> separation(M, λx. ∀y[M]. y∈Y ⟶ P(x,y))"
apply (simp del: separation_closed rall_abs
apply (blast intro!:  RepFun_closed dest: transM)
done

subsubsection‹Functions and function space›

lemma (in M_basic_no_repl) succ_fun_eq2:
"[|M(B); M(n->B)|] ==>
succ(n) -> B =
⋃{z. p ∈ (n->B)*B, ∃f[M]. ∃b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
apply (blast dest: transM)
done

lemma (in M_basic_no_repl) list_case'_closed [intro,simp]:
"[|M(k); M(a); ∀x[M]. ∀y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
apply (case_tac "quasilist(k)")
done

lemma (in M_basic_no_repl) tl'_closed: "M(x) ==> M(tl'(x))"