# Theory Separation

Up to index of Isabelle/ZF/Constructible

theory Separation
imports L_axioms WF_absolute
begin

    (*  Title:      ZF/Constructible/Separation.thy
        ID:         $Id: Separation.thy,v 1.25 2005/06/17 14:15:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    *)

    header{*Early Instances of Separation and Strong Replacement*}

    theory Separation imports L_axioms WF_absolute begin

    text{*This theory proves all instances needed for locale @{text "M_basic"}*}

    text{*Helps us solve for de Bruijn indices!*}
    lemma nth_ConsI: "[|nth(n,l) = x; n ∈ nat|] ==> nth(succ(n), Cons(a,l)) = x"
    by simp

    lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
    lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
                       fun_plus_iff_sats

    lemma Collect_conj_in_DPow:
         "[| {x∈A. P(x)} ∈ DPow(A);  {x∈A. Q(x)} ∈ DPow(A) |]
          ==> {x∈A. P(x) & Q(x)} ∈ DPow(A)"
    by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])

    lemma Collect_conj_in_DPow_Lset:
         "[|z ∈ Lset(j); {x ∈ Lset(j). P(x)} ∈ DPow(Lset(j))|]
          ==> {x ∈ Lset(j). x ∈ z & P(x)} ∈ DPow(Lset(j))"
    apply (frule mem_Lset_imp_subset_Lset)
    apply (simp add: Collect_conj_in_DPow Collect_mem_eq
                     subset_Int_iff2 elem_subset_in_DPow)
    done

    lemma separation_CollectI:
         "(!!z. L(z) ==> L({x ∈ z . P(x)})) ==> separation(L, λx. P(x))"
    apply (unfold separation_def, clarify)
    apply (rule_tac x="{x∈z. P(x)}" in rexI)
    apply simp_all
    done

    text{*Reduces the original comprehension to the reflected one*}
    lemma reflection_imp_L_separation:
          "[| ∀x∈Lset(j). P(x) <-> Q(x);
              {x ∈ Lset(j) . Q(x)} ∈ DPow(Lset(j));
              Ord(j);  z ∈ Lset(j)|] ==> L({x ∈ z . P(x)})"
    apply (rule_tac i = "succ(j)" in L_I)
     prefer 2 apply simp
    apply (subgoal_tac "{x ∈ z. P(x)} = {x ∈ Lset(j). x ∈ z & (Q(x))}")
     prefer 2
     apply (blast dest: mem_Lset_imp_subset_Lset)
    apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
    done

    text{*Encapsulates the standard proof script for proving instances of
          Separation.*}
    lemma gen_separation:
     assumes reflection: "REFLECTS [P,Q]"
         and Lu:         "L(u)"
         and collI: "!!j. u ∈ Lset(j)
                    ==> Collect(Lset(j), Q(j)) ∈ DPow(Lset(j))"
     shows "separation(L,P)"
    apply (rule separation_CollectI)
    apply (rule_tac A="{u,z}" in subset_LsetE, blast intro: Lu)
    apply (rule ReflectsE [OF reflection], assumption)
    apply (drule subset_Lset_ltD, assumption)
    apply (erule reflection_imp_L_separation)
      apply (simp_all add: lt_Ord2, clarify)
    apply (rule collI, assumption)
    done

    text{*As above, but typically @{term u} is a finite enumeration such as
      @{term "{a,b}"}; thus the new subgoal gets the assumption
      @{term "{a,b} ⊆ Lset(i)"}, which is logically equivalent to
      @{term "a ∈ Lset(i)"} and @{term "b ∈ Lset(i)"}.*}
    lemma gen_separation_multi:
     assumes reflection: "REFLECTS [P,Q]"
         and Lu:         "L(u)"
         and collI: "!!j. u ⊆ Lset(j)
                    ==> Collect(Lset(j), Q(j)) ∈ DPow(Lset(j))"
     shows "separation(L,P)"
    apply (rule gen_separation [OF reflection Lu])
    apply (drule mem_Lset_imp_subset_Lset)
    apply (erule collI)
    done

    subsection{*Separation for Intersection*}

    lemma Inter_Reflects:
         "REFLECTS[λx. ∀y[L]. y∈A --> x ∈ y,
                   λi x. ∀y∈Lset(i). y∈A --> x ∈ y]"
    by (intro FOL_reflections)

    lemma Inter_separation:
         "L(A) ==> separation(L, λx. ∀y[L]. y∈A --> x∈y)"
    apply (rule gen_separation [OF Inter_Reflects], simp)
    apply (rule DPow_LsetI)
     txt{*I leave this one example of a manual proof.  The tedium of manually
          instantiating @{term i}, @{term j} and @{term env} is obvious. *}
    apply (rule ball_iff_sats)
    apply (rule imp_iff_sats)
    apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
    apply (rule_tac i=0 and j=2 in mem_iff_sats)
    apply (simp_all add: succ_Un_distrib [symmetric])
    done

    subsection{*Separation for Set Difference*}

    lemma Diff_Reflects:
         "REFLECTS[λx. x ∉ B, λi x. x ∉ B]"
    by (intro FOL_reflections)

    lemma Diff_separation:
         "L(B) ==> separation(L, λx. x ∉ B)"
    apply (rule gen_separation [OF Diff_Reflects], simp)
    apply (rule_tac env="[B]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Cartesian Product*}

    lemma cartprod_Reflects:
         "REFLECTS[λz. ∃x[L]. x∈A & (∃y[L]. y∈B & pair(L,x,y,z)),
                    λi z. ∃x∈Lset(i). x∈A & (∃y∈Lset(i). y∈B &
                                       pair(##Lset(i),x,y,z))]"
    by (intro FOL_reflections function_reflections)

    lemma cartprod_separation:
         "[| L(A); L(B) |]
          ==> separation(L, λz. ∃x[L]. x∈A & (∃y[L]. y∈B & pair(L,x,y,z)))"
    apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto)
    apply (rule_tac env="[A,B]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Image*}

    lemma image_Reflects:
         "REFLECTS[λy. ∃p[L]. p∈r & (∃x[L]. x∈A & pair(L,x,y,p)),
               λi y. ∃p∈Lset(i). p∈r & (∃x∈Lset(i). x∈A & pair(##Lset(i),x,y,p))]"
    by (intro FOL_reflections function_reflections)

    lemma image_separation:
         "[| L(A); L(r) |]
          ==> separation(L, λy. ∃p[L]. p∈r & (∃x[L]. x∈A & pair(L,x,y,p)))"
    apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto)
    apply (rule_tac env="[A,r]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Converse*}

    lemma converse_Reflects:
      "REFLECTS[λz. ∃p[L]. p∈r & (∃x[L]. ∃y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
         λi z. ∃p∈Lset(i). p∈r & (∃x∈Lset(i). ∃y∈Lset(i).
                         pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]"
    by (intro FOL_reflections function_reflections)

    lemma converse_separation:
         "L(r) ==> separation(L,
             λz. ∃p[L]. p∈r & (∃x[L]. ∃y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
    apply (rule gen_separation [OF converse_Reflects], simp)
    apply (rule_tac env="[r]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Restriction*}

    lemma restrict_Reflects:
         "REFLECTS[λz. ∃x[L]. x∈A & (∃y[L]. pair(L,x,y,z)),
            λi z. ∃x∈Lset(i). x∈A & (∃y∈Lset(i). pair(##Lset(i),x,y,z))]"
    by (intro FOL_reflections function_reflections)

    lemma restrict_separation:
       "L(A) ==> separation(L, λz. ∃x[L]. x∈A & (∃y[L]. pair(L,x,y,z)))"
    apply (rule gen_separation [OF restrict_Reflects], simp)
    apply (rule_tac env="[A]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Composition*}

    lemma comp_Reflects:
         "REFLECTS[λxz. ∃x[L]. ∃y[L]. ∃z[L]. ∃xy[L]. ∃yz[L].
                      pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                      xy∈s & yz∈r,
            λi xz. ∃x∈Lset(i). ∃y∈Lset(i). ∃z∈Lset(i). ∃xy∈Lset(i). ∃yz∈Lset(i).
                      pair(##Lset(i),x,z,xz) & pair(##Lset(i),x,y,xy) &
                      pair(##Lset(i),y,z,yz) & xy∈s & yz∈r]"
    by (intro FOL_reflections function_reflections)

    lemma comp_separation:
         "[| L(r); L(s) |]
          ==> separation(L, λxz. ∃x[L]. ∃y[L]. ∃z[L]. ∃xy[L]. ∃yz[L].
                      pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                      xy∈s & yz∈r)"
    apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto)
    txt{*Subgoals after applying general ``separation'' rule:
         @{subgoals[display,indent=0,margin=65]}*}
    apply (rule_tac env="[r,s]" in DPow_LsetI)
    txt{*Subgoals ready for automatic synthesis of a formula:
         @{subgoals[display,indent=0,margin=65]}*}
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for Predecessors in an Order*}

    lemma pred_Reflects:
         "REFLECTS[λy. ∃p[L]. p∈r & pair(L,y,x,p),
                        λi y. ∃p ∈ Lset(i). p∈r & pair(##Lset(i),y,x,p)]"
    by (intro FOL_reflections function_reflections)

    lemma pred_separation:
         "[| L(r); L(x) |] ==> separation(L, λy. ∃p[L]. p∈r & pair(L,y,x,p))"
    apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto)
    apply (rule_tac env="[r,x]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for the Membership Relation*}

    lemma Memrel_Reflects:
         "REFLECTS[λz. ∃x[L]. ∃y[L]. pair(L,x,y,z) & x ∈ y,
                λi z. ∃x ∈ Lset(i). ∃y ∈ Lset(i). pair(##Lset(i),x,y,z) & x ∈ y]"
    by (intro FOL_reflections function_reflections)

    lemma Memrel_separation:
         "separation(L, λz. ∃x[L]. ∃y[L]. pair(L,x,y,z) & x ∈ y)"
    apply (rule gen_separation [OF Memrel_Reflects nonempty])
    apply (rule_tac env="[]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Replacement for FunSpace*}

    lemma funspace_succ_Reflects:
     "REFLECTS[λz. ∃p[L]. p∈A & (∃f[L]. ∃b[L]. ∃nb[L]. ∃cnbf[L].
                pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
                upair(L,cnbf,cnbf,z)),
            λi z. ∃p ∈ Lset(i). p∈A & (∃f ∈ Lset(i). ∃b ∈ Lset(i).
                  ∃nb ∈ Lset(i). ∃cnbf ∈ Lset(i).
                    pair(##Lset(i),f,b,p) & pair(##Lset(i),n,b,nb) &
                    is_cons(##Lset(i),nb,f,cnbf) & upair(##Lset(i),cnbf,cnbf,z))]"
    by (intro FOL_reflections function_reflections)

    lemma funspace_succ_replacement:
         "L(n) ==>
          strong_replacement(L, λp z. ∃f[L]. ∃b[L]. ∃nb[L]. ∃cnbf[L].
                    pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
                    upair(L,cnbf,cnbf,z))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects],
           auto)
    apply (rule_tac env="[n,B]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Separation for a Theorem about @{term "is_recfun"}*}

    lemma is_recfun_reflects:
      "REFLECTS[λx. ∃xa[L]. ∃xb[L].
                    pair(L,x,a,xa) & xa ∈ r & pair(L,x,b,xb) & xb ∈ r &
                    (∃fx[L]. ∃gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                       fx ≠ gx),
       λi x. ∃xa ∈ Lset(i). ∃xb ∈ Lset(i).
              pair(##Lset(i),x,a,xa) & xa ∈ r & pair(##Lset(i),x,b,xb) & xb ∈ r &
                    (∃fx ∈ Lset(i). ∃gx ∈ Lset(i). fun_apply(##Lset(i),f,x,fx) &
                      fun_apply(##Lset(i),g,x,gx) & fx ≠ gx)]"
    by (intro FOL_reflections function_reflections fun_plus_reflections)

    lemma is_recfun_separation:
         --{*for well-founded recursion*}
         "[| L(r); L(f); L(g); L(a); L(b) |]
         ==> separation(L,
                λx. ∃xa[L]. ∃xb[L].
                    pair(L,x,a,xa) & xa ∈ r & pair(L,x,b,xb) & xb ∈ r &
                    (∃fx[L]. ∃gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                       fx ≠ gx))"
    apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"],
                auto)
    apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI)
    apply (rule sep_rules | simp)+
    done

    subsection{*Instantiating the locale @{text M_basic}*}
    text{*Separation (and Strong Replacement) for basic set-theoretic constructions
    such as intersection, Cartesian Product and image.*}

    lemma M_basic_axioms_L: "M_basic_axioms(L)"
      apply (rule M_basic_axioms.intro)
           apply (assumption | rule
             Inter_separation Diff_separation cartprod_separation image_separation
             converse_separation restrict_separation
             comp_separation pred_separation Memrel_separation
             funspace_succ_replacement is_recfun_separation)+
      done

    theorem M_basic_L: "PROP M_basic(L)"
    by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])

    interpretation M_basic [L] by (rule M_basic_axioms_L)

    end

lemma nth_ConsI:

      [| nth(n, l) = x; n ∈ nat |] ==> nth(succ(n), Cons(a, l)) = x

lemmas nth_rules:

      nth(0, Cons(a, l)) = a

      [| nth(n, l) = x; n ∈ nat |] ==> nth(succ(n), Cons(a, l)) = x

      0 ∈ nat

      n ∈ nat ==> succ(n) ∈ nat

lemmas nth_rules:

      nth(0, Cons(a, l)) = a

      [| nth(n, l) = x; n ∈ nat |] ==> nth(succ(n), Cons(a, l)) = x

      0 ∈ nat

      n ∈ nat ==> succ(n) ∈ nat

lemmas sep_rules:

      nth(0, Cons(a, l)) = a

      [| nth(n, l) = x; n ∈ nat |] ==> nth(succ(n), Cons(a, l)) = x

      [| nth(i, env) = x; nth(j, env) = y; env ∈ list(A) |]
      ==> x ∈ y <-> sats(A, Member(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; env ∈ list(A) |]
      ==> x = y <-> sats(A, Equal(i, j), env)

      [| P <-> sats(A, p, env); env ∈ list(A) |] ==> ¬ P <-> sats(A, Neg(p), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> P ∧ Q <-> sats(A, And(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> P ∨ Q <-> sats(A, Or(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P --> Q) <-> sats(A, Implies(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P <-> Q) <-> sats(A, Iff(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P --> Q) <-> sats(A, Implies(p, q), env)

      [| !!x. x ∈ A ==> P(x) <-> sats(A, p, Cons(x, env)); env ∈ list(A) |]
      ==> (∀x∈A. P(x)) <-> sats(A, Forall(p), env)

      [| !!x. x ∈ A ==> P(x) <-> sats(A, p, Cons(x, env)); env ∈ list(A) |]
      ==> (∃x∈A. P(x)) <-> sats(A, Exists(p), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> empty(##A, x) <-> sats(A, empty_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> number1(##A, x) <-> sats(A, number1_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> upair(##A, x, y, z) <-> sats(A, upair_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> pair(##A, x, y, z) <-> sats(A, pair_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> union(##A, x, y, z) <-> sats(A, union_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> big_union(##A, x, y) <-> sats(A, big_union_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> is_cons(##A, x, y, z) <-> sats(A, cons_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> successor(##A, x, y) <-> sats(A, succ_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> fun_apply(##A, x, y, z) <-> sats(A, fun_apply_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> membership(##A, x, y) <-> sats(A, Memrel_fm(i, j), env)

      [| nth(i, env) = U; nth(j, env) = x; nth(k, env) = r; nth(l, env) = B; i ∈ nat;
         j ∈ nat; k ∈ nat; l ∈ nat; env ∈ list(A) |]
      ==> pred_set(##A, U, x, r, B) <-> sats(A, pred_set_fm(i, j, k, l), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_domain(##A, x, y) <-> sats(A, domain_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_range(##A, x, y) <-> sats(A, range_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_field(##A, x, y) <-> sats(A, field_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> image(##A, x, y, z) <-> sats(A, image_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> pre_image(##A, x, y, z) <-> sats(A, pre_image_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> is_relation(##A, x) <-> sats(A, relation_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> is_function(##A, x) <-> sats(A, function_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> typed_function(##A, x, y, z) <-> sats(A, typed_function_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> composition(##A, x, y, z) <-> sats(A, composition_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> injection(##A, x, y, z) <-> sats(A, injection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> surjection(##A, x, y, z) <-> sats(A, surjection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> bijection(##A, x, y, z) <-> sats(A, bijection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> restriction(##A, x, y, z) <-> sats(A, restriction_fm(i, j, k), env)

      [| nth(i, env) = U; nth(j, env) = r; nth(k, env) = B; nth(j', env) = s;
         nth(k', env) = f; i ∈ nat; j ∈ nat; k ∈ nat; j' ∈ nat; k' ∈ nat;
         env ∈ list(A) |]
      ==> order_isomorphism(##A, U, r, B, s, f) <->
          sats(A, order_isomorphism_fm(i, j, k, j', k'), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> finite_ordinal(##A, x) <-> sats(A, finite_ordinal_fm(i), env)

      [| nth(i, env) = x; i ∈ nat; env ∈ list(A) |]
      ==> ordinal(##A, x) <-> sats(A, ordinal_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> limit_ordinal(##A, x) <-> sats(A, limit_ordinal_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> omega(##A, x) <-> sats(A, omega_fm(i), env)

lemmas sep_rules:

      nth(0, Cons(a, l)) = a

      [| nth(n, l) = x; n ∈ nat |] ==> nth(succ(n), Cons(a, l)) = x

      [| nth(i, env) = x; nth(j, env) = y; env ∈ list(A) |]
      ==> x ∈ y <-> sats(A, Member(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; env ∈ list(A) |]
      ==> x = y <-> sats(A, Equal(i, j), env)

      [| P <-> sats(A, p, env); env ∈ list(A) |] ==> ¬ P <-> sats(A, Neg(p), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> P ∧ Q <-> sats(A, And(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> P ∨ Q <-> sats(A, Or(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P --> Q) <-> sats(A, Implies(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P <-> Q) <-> sats(A, Iff(p, q), env)

      [| P <-> sats(A, p, env); Q <-> sats(A, q, env); env ∈ list(A) |]
      ==> (P --> Q) <-> sats(A, Implies(p, q), env)

      [| !!x. x ∈ A ==> P(x) <-> sats(A, p, Cons(x, env)); env ∈ list(A) |]
      ==> (∀x∈A. P(x)) <-> sats(A, Forall(p), env)

      [| !!x. x ∈ A ==> P(x) <-> sats(A, p, Cons(x, env)); env ∈ list(A) |]
      ==> (∃x∈A. P(x)) <-> sats(A, Exists(p), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> empty(##A, x) <-> sats(A, empty_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> number1(##A, x) <-> sats(A, number1_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> upair(##A, x, y, z) <-> sats(A, upair_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> pair(##A, x, y, z) <-> sats(A, pair_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> union(##A, x, y, z) <-> sats(A, union_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> big_union(##A, x, y) <-> sats(A, big_union_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> is_cons(##A, x, y, z) <-> sats(A, cons_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> successor(##A, x, y) <-> sats(A, succ_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> fun_apply(##A, x, y, z) <-> sats(A, fun_apply_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> membership(##A, x, y) <-> sats(A, Memrel_fm(i, j), env)

      [| nth(i, env) = U; nth(j, env) = x; nth(k, env) = r; nth(l, env) = B; i ∈ nat;
         j ∈ nat; k ∈ nat; l ∈ nat; env ∈ list(A) |]
      ==> pred_set(##A, U, x, r, B) <-> sats(A, pred_set_fm(i, j, k, l), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_domain(##A, x, y) <-> sats(A, domain_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_range(##A, x, y) <-> sats(A, range_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j ∈ nat; env ∈ list(A) |]
      ==> is_field(##A, x, y) <-> sats(A, field_fm(i, j), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> image(##A, x, y, z) <-> sats(A, image_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> pre_image(##A, x, y, z) <-> sats(A, pre_image_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> is_relation(##A, x) <-> sats(A, relation_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> is_function(##A, x) <-> sats(A, function_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> typed_function(##A, x, y, z) <-> sats(A, typed_function_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> composition(##A, x, y, z) <-> sats(A, composition_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> injection(##A, x, y, z) <-> sats(A, injection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> surjection(##A, x, y, z) <-> sats(A, surjection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> bijection(##A, x, y, z) <-> sats(A, bijection_fm(i, j, k), env)

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> restriction(##A, x, y, z) <-> sats(A, restriction_fm(i, j, k), env)

      [| nth(i, env) = U; nth(j, env) = r; nth(k, env) = B; nth(j', env) = s;
         nth(k', env) = f; i ∈ nat; j ∈ nat; k ∈ nat; j' ∈ nat; k' ∈ nat;
         env ∈ list(A) |]
      ==> order_isomorphism(##A, U, r, B, s, f) <->
          sats(A, order_isomorphism_fm(i, j, k, j', k'), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> finite_ordinal(##A, x) <-> sats(A, finite_ordinal_fm(i), env)

      [| nth(i, env) = x; i ∈ nat; env ∈ list(A) |]
      ==> ordinal(##A, x) <-> sats(A, ordinal_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> limit_ordinal(##A, x) <-> sats(A, limit_ordinal_fm(i), env)

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; env ∈ list(A) |]
      ==> omega(##A, x) <-> sats(A, omega_fm(i), env)

lemma Collect_conj_in_DPow:

      [| {x ∈ A . P(x)} ∈ DPow(A); {x ∈ A . Q(x)} ∈ DPow(A) |]
      ==> {x ∈ A . P(x) ∧ Q(x)} ∈ DPow(A)

lemma Collect_conj_in_DPow_Lset:

      [| z ∈ Lset(j); {x ∈ Lset(j) . P(x)} ∈ DPow(Lset(j)) |]
      ==> {x ∈ Lset(j) . x ∈ z ∧ P(x)} ∈ DPow(Lset(j))

lemma separation_CollectI:

      (!!z. L(z) ==> L({x ∈ z . P(x)})) ==> separation(L, %x. P(x))

lemma reflection_imp_L_separation:

      [| ∀x∈Lset(j). P(x) <-> Q(x); {x ∈ Lset(j) . Q(x)} ∈ DPow(Lset(j)); Ord(j);
         z ∈ Lset(j) |]
      ==> L({x ∈ z . P(x)})

lemma gen_separation:

      [| REFLECTS [P, Q]; L(u);
         !!j. u ∈ Lset(j) ==> Collect(Lset(j), Q(j)) ∈ DPow(Lset(j)) |]
      ==> separation(L, P)

lemma gen_separation_multi:

      [| REFLECTS [P, Q]; L(u);
         !!j. u ⊆ Lset(j) ==> Collect(Lset(j), Q(j)) ∈ DPow(Lset(j)) |]
      ==> separation(L, P)

### Separation for Intersection

lemma Inter_Reflects:

      REFLECTS [%x. ∀y[L]. y ∈ A --> x ∈ y, %i x. ∀y∈Lset(i). y ∈ A --> x ∈ y]

lemma Inter_separation:

      L(A) ==> separation(L, %x. ∀y[L]. y ∈ A --> x ∈ y)

### Separation for Set Difference

lemma Diff_Reflects:

      REFLECTS [%x. x ∉ B, %i x. x ∉ B]

lemma Diff_separation:

      L(B) ==> separation(L, %x. x ∉ B)

### Separation for Cartesian Product

lemma cartprod_Reflects:

      REFLECTS [%z. ∃x[L]. x ∈ A ∧ (∃y[L]. y ∈ B ∧ pair(L, x, y, z)),
         %i z. ∃x∈Lset(i). x ∈ A ∧ (∃y∈Lset(i). y ∈ B ∧ pair(##Lset(i), x, y, z))]

lemma cartprod_separation:

      [| L(A); L(B) |]
      ==> separation(L, %z. ∃x[L]. x ∈ A ∧ (∃y[L]. y ∈ B ∧ pair(L, x, y, z)))

### Separation for Image

lemma image_Reflects:

      REFLECTS [%y. ∃p[L]. p ∈ r ∧ (∃x[L]. x ∈ A ∧ pair(L, x, y, p)),
         %i y. ∃p∈Lset(i). p ∈ r ∧ (∃x∈Lset(i). x ∈ A ∧ pair(##Lset(i), x, y, p))]

lemma image_separation:

      [| L(A); L(r) |]
      ==> separation(L, %y. ∃p[L]. p ∈ r ∧ (∃x[L]. x ∈ A ∧ pair(L, x, y, p)))

### Separation for Converse

lemma converse_Reflects:

      REFLECTS
         [%z. ∃p[L]. p ∈ r ∧ (∃x[L]. ∃y[L]. pair(L, x, y, p) ∧ pair(L, y, x, z)),
         %i z. ∃p∈Lset(i).
                  p ∈ r ∧
                  (∃x∈Lset(i).
                      ∃y∈Lset(i).
                         pair(##Lset(i), x, y, p) ∧ pair(##Lset(i), y, x, z))]

lemma converse_separation:

      L(r)
      ==> separation
           (L, %z. ∃p[L]. p ∈ r ∧ (∃x[L]. ∃y[L]. pair(L, x, y, p) ∧ pair(L, y, x, z)))

### Separation for Restriction

lemma restrict_Reflects:

      REFLECTS [%z. ∃x[L]. x ∈ A ∧ (∃y[L]. pair(L, x, y, z)),
         %i z. ∃x∈Lset(i). x ∈ A ∧ (∃y∈Lset(i). pair(##Lset(i), x, y, z))]

lemma restrict_separation:

      L(A) ==> separation(L, %z. ∃x[L]. x ∈ A ∧ (∃y[L]. pair(L, x, y, z)))

### Separation for Composition

lemma comp_Reflects:

      REFLECTS
         [%xz. ∃x[L]. ∃y[L]. ∃z[L]. ∃xy[L].
                                       ∃yz[L].
                                          pair(L, x, z, xz) ∧
                                          pair(L, x, y, xy) ∧
                                          pair(L, y, z, yz) ∧ xy ∈ s ∧ yz ∈ r,
         %i xz. ∃x∈Lset(i).
                   ∃y∈Lset(i).
                      ∃z∈Lset(i).
                         ∃xy∈Lset(i).
                            ∃yz∈Lset(i).
                               pair(##Lset(i), x, z, xz) ∧
                               pair(##Lset(i), x, y, xy) ∧
                               pair(##Lset(i), y, z, yz) ∧ xy ∈ s ∧ yz ∈ r]

lemma comp_separation:

      [| L(r); L(s) |]
      ==> separation
           (L, %xz. ∃x[L]. ∃y[L]. ∃z[L]. ∃xy[L].
                                            ∃yz[L].
       pair(L, x, z, xz) ∧ pair(L, x, y, xy) ∧ pair(L, y, z, yz) ∧ xy ∈ s ∧ yz ∈ r)

### Separation for Predecessors in an Order

lemma pred_Reflects:

      REFLECTS [%y. ∃p[L]. p ∈ r ∧ pair(L, y, x, p),
         %i y. ∃p∈Lset(i). p ∈ r ∧ pair(##Lset(i), y, x, p)]

lemma pred_separation:

      [| L(r); L(x) |] ==> separation(L, %y. ∃p[L]. p ∈ r ∧ pair(L, y, x, p))

### Separation for the Membership Relation

lemma Memrel_Reflects:

      REFLECTS [%z. ∃x[L]. ∃y[L]. pair(L, x, y, z) ∧ x ∈ y,
         %i z. ∃x∈Lset(i). ∃y∈Lset(i). pair(##Lset(i), x, y, z) ∧ x ∈ y]

lemma Memrel_separation:

      separation(L, %z. ∃x[L]. ∃y[L]. pair(L, x, y, z) ∧ x ∈ y)

### Replacement for FunSpace

lemma funspace_succ_Reflects:

      REFLECTS
         [%z. ∃p[L]. p ∈ A ∧
                     (∃f[L]. ∃b[L]. ∃nb[L].
                                       ∃cnbf[L].
                                          pair(L, f, b, p) ∧
                                          pair(L, n, b, nb) ∧
                                          is_cons(L, nb, f, cnbf) ∧
                                          upair(L, cnbf, cnbf, z)),
         %i z. ∃p∈Lset(i).
                  p ∈ A ∧
                  (∃f∈Lset(i).
                      ∃b∈Lset(i).
                         ∃nb∈Lset(i).
                            ∃cnbf∈Lset(i).
                               pair(##Lset(i), f, b, p) ∧
                               pair(##Lset(i), n, b, nb) ∧
                               is_cons(##Lset(i), nb, f, cnbf) ∧
                               upair(##Lset(i), cnbf, cnbf, z))]

lemma funspace_succ_replacement:

      L(n)
      ==> strong_replacement
           (L, %p z. ∃f[L]. ∃b[L]. ∃nb[L].
                                      ∃cnbf[L].
                                         pair(L, f, b, p) ∧
                                         pair(L, n, b, nb) ∧
                                         is_cons(L, nb, f, cnbf) ∧
                                         upair(L, cnbf, cnbf, z))

### Separation for a Theorem about @{term "is_recfun"}

lemma is_recfun_reflects:

      REFLECTS
         [%x. ∃xa[L].
                 ∃xb[L].
                    pair(L, x, a, xa) ∧
                    xa ∈ r ∧
                    pair(L, x, b, xb) ∧
                    xb ∈ r ∧
                    (∃fx[L].
                        ∃gx[L].
                           fun_apply(L, f, x, fx) ∧ fun_apply(L, g, x, gx) ∧ fx ≠ gx),
         %i x. ∃xa∈Lset(i).
                  ∃xb∈Lset(i).
                     pair(##Lset(i), x, a, xa) ∧
                     xa ∈ r ∧
                     pair(##Lset(i), x, b, xb) ∧
                     xb ∈ r ∧
                     (∃fx∈Lset(i).
                         ∃gx∈Lset(i).
                            fun_apply(##Lset(i), f, x, fx) ∧
                            fun_apply(##Lset(i), g, x, gx) ∧ fx ≠ gx)]

lemma is_recfun_separation:

      [| L(r); L(f); L(g); L(a); L(b) |]
      ==> separation
           (L, %x. ∃xa[L].
                      ∃xb[L].
                         pair(L, x, a, xa) ∧
                         xa ∈ r ∧
                         pair(L, x, b, xb) ∧
                         xb ∈ r ∧
                         (∃fx[L].
                             ∃gx[L].
                                fun_apply(L, f, x, fx) ∧
                                fun_apply(L, g, x, gx) ∧ fx ≠ gx))

### Instantiating the locale @{text M_basic}

lemma M_basic_axioms_L:

      M_basic_axioms(L)

theorem M_basic_L:

      PROP M_basic(L)