Theory M_Basic_No_Repl

theory M_Basic_No_Repl
  imports "ZF-Constructible.Relative"

txt‹This locale is exactly localeM_basic without its only replacement

locale M_basic_no_repl = M_trivial +
  assumes Inter_separation:
    "M(A) ==> separation(M, λx. y[M]. yA  xy)"
    and Diff_separation:
    "M(B) ==> separation(M, λx. x  B)"
    and cartprod_separation:
    "[| M(A); M(B) |]
      ==> separation(M, λz. x[M]. xA & (y[M]. yB & pair(M,x,y,z)))"
    and image_separation:
    "[| M(A); M(r) |]
      ==> separation(M, λy. p[M]. pr & (x[M]. xA & pair(M,x,y,p)))"
    and converse_separation:
    "M(r) ==> separation(M,
         λz. p[M]. pr & (x[M]. y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    and restrict_separation:
    "M(A) ==> separation(M, λz. x[M]. xA & (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) &
                  xys & yzr)"
    and pred_separation:
    "[| M(r); M(x) |] ==> separation(M, λy. p[M]. pr & 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. xA. yB. z = <x,y>})"
  apply (simp add: Pair_def cartprod_def, safe)
    defer 1
    apply (simp add: powerset_def)
   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)

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)

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)"
  by (simp add: sum_def)

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)).
       pr. x[M]. y[M]. p = x,y & z = y,x}"
  apply (rule equalityI)
   prefer 2 apply (blast dest: transM, clarify, simp)
  apply (simp add: Pair_def)
  apply (blast dest: transM)

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

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

subsubsection ‹image, preimage, domain, range›

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

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 (simp add: pre_image_def)
  apply (rule iffI)
   apply (blast intro!: equalityI dest: transM, blast)

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

subsubsection‹Domain, range and field›

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

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

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

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

subsubsection‹Relations, functions and application›

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

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)

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

lemma (in M_basic_no_repl) surjection_abs [simp]:
  "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f)  f  surj(A,B)"
  by (simp add: surjection_def surj_def)

lemma (in M_basic_no_repl) bijection_abs [simp]:
  "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f)  f  bij(A,B)"
  by (simp add: bijection_def bij_def)

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 (simp add: comp_def)
  apply (rule equalityI)
   apply clarify
   apply simp
   apply  (blast dest:  transM)+

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

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 termcomposition(M, r, s, r O s)
   prefer 2
   apply (simp add: composition_def comp_def)
   apply (blast dest: transM)
  txt‹Opposite implication›
  apply (rule M_equalityI)
    apply (simp add: composition_def comp_def)
    apply (blast del: allE dest: transM)+

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 (simp add: restriction_def ball_iff_equiv)
  apply (unfold function_def, blast)

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

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

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)

subsubsection‹Some Facts About Separation Axioms›

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
      add: separation_iff Collect_Int_Collect_eq [symmetric])

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
      add: separation_iff Collect_Un_Collect_eq [symmetric])

lemma (in M_basic_no_repl) separation_neg:
  "separation(M,P) ==> separation(M, λz. ~P(z))"
  by (simp del: separation_closed
      add: separation_iff Diff_Collect_eq [symmetric])

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]. yY  P(x,y))"
  apply (simp del: separation_closed rall_abs
      add: separation_iff Collect_rall_eq)
  apply (blast intro!:  RepFun_closed dest: transM)

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 (simp add: succ_fun_eq)
  apply (blast dest: transM)

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)")
   apply (simp add: quasilist_def, force)
  apply (simp add: non_list_case)

lemma (in M_basic_no_repl) tl'_closed: "M(x) ==> M(tl'(x))"
  apply (simp add: tl'_def)
  apply (force simp add: quasilist_def)

sublocale M_basic  mbnr:M_basic_no_repl
  using Inter_separation Diff_separation cartprod_separation image_separation
    converse_separation restrict_separation comp_separation pred_separation
    Memrel_separation is_recfun_separation power_ax by unfold_locales