Theory L_axioms

(*  Title:      ZF/Constructible/L_axioms.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹The ZF Axioms (Except Separation) in L›

theory L_axioms imports Formula Relative Reflection MetaExists begin

text ‹The class L satisfies the premises of locale M_trivial›

lemma transL: "[| yx; L(x) |] ==> L(y)"
apply (insert Transset_Lset)
apply (simp add: Transset_def L_def, blast)
done

lemma nonempty: "L(0)"
apply (simp add: L_def)
apply (blast intro: zero_in_Lset)
done

theorem upair_ax: "upair_ax(L)"
apply (simp add: upair_ax_def upair_def, clarify)
apply (rule_tac x="{x,y}" in rexI)
apply (simp_all add: doubleton_in_L)
done

theorem Union_ax: "Union_ax(L)"
apply (simp add: Union_ax_def big_union_def, clarify)
apply (rule_tac x="(x)" in rexI)
apply (simp_all add: Union_in_L, auto)
apply (blast intro: transL)
done

theorem power_ax: "power_ax(L)"
apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
apply (rule_tac x="{y  Pow(x). L(y)}" in rexI)
apply (simp_all add: LPow_in_L, auto)
apply (blast intro: transL)
done

text‹We don't actually need term‹L› to satisfy the foundation axiom.›
theorem foundation_ax: "foundation_ax(L)"
apply (simp add: foundation_ax_def)
apply (rule rallI) 
apply (cut_tac A=x in foundation)
apply (blast intro: transL)
done

subsection‹For L to satisfy Replacement›

(*Can't move these to Formula unless the definition of univalent is moved
there too!*)

lemma LReplace_in_Lset:
     "[|X  Lset(i); univalent(L,X,Q); Ord(i)|]
      ==> j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y))  Lset(j)"
apply (rule_tac x="y  Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"
       in exI)
apply simp
apply clarify
apply (rule_tac a=x in UN_I)
 apply (simp_all add: Replace_iff univalent_def)
apply (blast dest: transL L_I)
done

lemma LReplace_in_L:
     "[|L(X); univalent(L,X,Q)|]
      ==> Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y))  Y"
apply (drule L_D, clarify)
apply (drule LReplace_in_Lset, assumption+)
apply (blast intro: L_I Lset_in_Lset_succ)
done

theorem replacement: "replacement(L,P)"
apply (simp add: replacement_def, clarify)
apply (frule LReplace_in_L, assumption+, clarify)
apply (rule_tac x=Y in rexI)
apply (simp_all add: Replace_iff univalent_def, blast)
done

lemma strong_replacementI [rule_format]:
    "[| B[L]. separation(L, %u. x[L]. xB & P(x,u)) |]
     ==> strong_replacement(L,P)"
apply (simp add: strong_replacement_def, clarify)
apply (frule replacementD [OF replacement], assumption, clarify)
apply (drule_tac x=A in rspec, clarify)
apply (drule_tac z=Y in separationD, assumption, clarify)
apply (rule_tac x=y in rexI, force, assumption)
done


subsection‹Instantiating the locale M_trivial›
text‹No instances of Separation yet.›

lemma Lset_mono_le: "mono_le_subset(Lset)"
by (simp add: mono_le_subset_def le_imp_subset Lset_mono)

lemma Lset_cont: "cont_Ord(Lset)"
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)

lemmas L_nat = Ord_in_L [OF Ord_nat]

theorem M_trivial_L: "M_trivial(L)"
  apply (rule M_trivial.intro)
  apply (rule M_trans.intro)
    apply (erule (1) transL)
   apply(rule exI,rule  nonempty)
  apply (rule M_trivial_axioms.intro)
      apply (rule upair_ax)
   apply (rule Union_ax)
  done

interpretation L: M_trivial L by (rule M_trivial_L)

(* Replaces the following declarations...
lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
  and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
...
declare rall_abs [simp]
declare rex_abs [simp]
...and dozens of similar ones.
*)

subsection‹Instantiation of the locale reflection›

text‹instances of locale constants›

definition
  L_F0 :: "[i=>o,i] => i" where
    "L_F0(P,y) == μ b. (z. L(z)  P(<y,z>))  (zLset(b). P(<y,z>))"

definition
  L_FF :: "[i=>o,i] => i" where
    "L_FF(P)   == λa. yLset(a). L_F0(P,y)"

definition
  L_ClEx :: "[i=>o,i] => o" where
    "L_ClEx(P) == λa. Limit(a)  normalize(L_FF(P),a) = a"


text‹We must use the meta-existential quantifier; otherwise the reflection
      terms become enormous!›
definition
  L_Reflects :: "[i=>o,[i,i]=>o] => prop"  ((3REFLECTS/ [_,/ _])) where
    "REFLECTS[P,Q] == (Cl. Closed_Unbounded(Cl) &
                           (a. Cl(a)  (x  Lset(a). P(x)  Q(a,x))))"


theorem Triv_reflection:
     "REFLECTS[P, λa x. P(x)]"
apply (simp add: L_Reflects_def)
apply (rule meta_exI)
apply (rule Closed_Unbounded_Ord)
done

theorem Not_reflection:
     "REFLECTS[P,Q] ==> REFLECTS[λx. ~P(x), λa x. ~Q(a,x)]"
apply (unfold L_Reflects_def)
apply (erule meta_exE)
apply (rule_tac x=Cl in meta_exI, simp)
done

theorem And_reflection:
     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
      ==> REFLECTS[λx. P(x)  P'(x), λa x. Q(a,x)  Q'(a,x)]"
apply (unfold L_Reflects_def)
apply (elim meta_exE)
apply (rule_tac x="λa. Cl(a)  Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
done

theorem Or_reflection:
     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
      ==> REFLECTS[λx. P(x)  P'(x), λa x. Q(a,x)  Q'(a,x)]"
apply (unfold L_Reflects_def)
apply (elim meta_exE)
apply (rule_tac x="λa. Cl(a)  Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
done

theorem Imp_reflection:
     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
      ==> REFLECTS[λx. P(x)  P'(x), λa x. Q(a,x)  Q'(a,x)]"
apply (unfold L_Reflects_def)
apply (elim meta_exE)
apply (rule_tac x="λa. Cl(a)  Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
done

theorem Iff_reflection:
     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
      ==> REFLECTS[λx. P(x)  P'(x), λa x. Q(a,x)  Q'(a,x)]"
apply (unfold L_Reflects_def)
apply (elim meta_exE)
apply (rule_tac x="λa. Cl(a)  Cla(a)" in meta_exI)
apply (simp add: Closed_Unbounded_Int, blast)
done


lemma reflection_Lset: "reflection(Lset)"
by (blast intro: reflection.intro Lset_mono_le Lset_cont 
                 Formula.Pair_in_LLimit)+


theorem Ex_reflection:
     "REFLECTS[λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z. L(z)  P(x,z), λa x. zLset(a). Q(a,x,z)]"
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
apply (elim meta_exE)
apply (rule meta_exI)
apply (erule reflection.Ex_reflection [OF reflection_Lset])
done

theorem All_reflection:
     "REFLECTS[λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z. L(z)  P(x,z), λa x. zLset(a). Q(a,x,z)]"
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
apply (elim meta_exE)
apply (rule meta_exI)
apply (erule reflection.All_reflection [OF reflection_Lset])
done

theorem Rex_reflection:
     "REFLECTS[ λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z[L]. P(x,z), λa x. zLset(a). Q(a,x,z)]"
apply (unfold rex_def)
apply (intro And_reflection Ex_reflection, assumption)
done

theorem Rall_reflection:
     "REFLECTS[λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z[L]. P(x,z), λa x. zLset(a). Q(a,x,z)]"
apply (unfold rall_def)
apply (intro Imp_reflection All_reflection, assumption)
done

text‹This version handles an alternative form of the bounded quantifier
      in the second argument of REFLECTS›.›
theorem Rex_reflection':
     "REFLECTS[λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z[L]. P(x,z), λa x. z[##Lset(a)]. Q(a,x,z)]"
apply (unfold setclass_def rex_def)
apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
done

text‹As above.›
theorem Rall_reflection':
     "REFLECTS[λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))]
      ==> REFLECTS[λx. z[L]. P(x,z), λa x. z[##Lset(a)]. Q(a,x,z)]"
apply (unfold setclass_def rall_def)
apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
done

lemmas FOL_reflections =
        Triv_reflection Not_reflection And_reflection Or_reflection
        Imp_reflection Iff_reflection Ex_reflection All_reflection
        Rex_reflection Rall_reflection Rex_reflection' Rall_reflection'

lemma ReflectsD:
     "[|REFLECTS[P,Q]; Ord(i)|]
      ==> j. i<j & (x  Lset(j). P(x)  Q(j,x))"
apply (unfold L_Reflects_def Closed_Unbounded_def)
apply (elim meta_exE, clarify)
apply (blast dest!: UnboundedD)
done

lemma ReflectsE:
     "[| REFLECTS[P,Q]; Ord(i);
         !!j. [|i<j;  x  Lset(j). P(x)  Q(j,x)|] ==> R |]
      ==> R"
by (drule ReflectsD, assumption, blast)

lemma Collect_mem_eq: "{xA. xB} = A  B"
by blast


subsection‹Internalized Formulas for some Set-Theoretic Concepts›

subsubsection‹Some numbers to help write de Bruijn indices›

abbreviation
  digit3 :: i   (3) where "3 == succ(2)"

abbreviation
  digit4 :: i   (4) where "4 == succ(3)"

abbreviation
  digit5 :: i   (5) where "5 == succ(4)"

abbreviation
  digit6 :: i   (6) where "6 == succ(5)"

abbreviation
  digit7 :: i   (7) where "7 == succ(6)"

abbreviation
  digit8 :: i   (8) where "8 == succ(7)"

abbreviation
  digit9 :: i   (9) where "9 == succ(8)"


subsubsection‹The Empty Set, Internalized›

definition
  empty_fm :: "i=>i" where
    "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"

lemma empty_type [TC]:
     "x  nat ==> empty_fm(x)  formula"
by (simp add: empty_fm_def)

lemma sats_empty_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, empty_fm(x), env)  empty(##A, nth(x,env))"
by (simp add: empty_fm_def empty_def)

lemma empty_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> empty(##A, x)  sats(A, empty_fm(i), env)"
by simp

theorem empty_reflection:
     "REFLECTS[λx. empty(L,f(x)),
               λi x. empty(##Lset(i),f(x))]"
apply (simp only: empty_def)
apply (intro FOL_reflections)
done

text‹Not used.  But maybe useful?›
lemma Transset_sats_empty_fm_eq_0:
   "[| n  nat; env  list(A); Transset(A)|]
    ==> sats(A, empty_fm(n), env)  nth(n,env) = 0"
apply (simp add: empty_fm_def empty_def Transset_def, auto)
apply (case_tac "n < length(env)")
apply (frule nth_type, assumption+, blast)
apply (simp_all add: not_lt_iff_le nth_eq_0)
done


subsubsection‹Unordered Pairs, Internalized›

definition
  upair_fm :: "[i,i,i]=>i" where
    "upair_fm(x,y,z) ==
       And(Member(x,z),
           And(Member(y,z),
               Forall(Implies(Member(0,succ(z)),
                              Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"

lemma upair_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> upair_fm(x,y,z)  formula"
by (simp add: upair_fm_def)

lemma sats_upair_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, upair_fm(x,y,z), env) 
            upair(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: upair_fm_def upair_def)

lemma upair_iff_sats:
      "[| 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)"
by (simp)

text‹Useful? At least it refers to "real" unordered pairs›
lemma sats_upair_fm2 [simp]:
   "[| x  nat; y  nat; z < length(env); env  list(A); Transset(A)|]
    ==> sats(A, upair_fm(x,y,z), env) 
        nth(z,env) = {nth(x,env), nth(y,env)}"
apply (frule lt_length_in_nat, assumption)
apply (simp add: upair_fm_def Transset_def, auto)
apply (blast intro: nth_type)
done

theorem upair_reflection:
     "REFLECTS[λx. upair(L,f(x),g(x),h(x)),
               λi x. upair(##Lset(i),f(x),g(x),h(x))]"
apply (simp add: upair_def)
apply (intro FOL_reflections)
done

subsubsection‹Ordered pairs, Internalized›

definition
  pair_fm :: "[i,i,i]=>i" where
    "pair_fm(x,y,z) ==
       Exists(And(upair_fm(succ(x),succ(x),0),
              Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
                         upair_fm(1,0,succ(succ(z)))))))"

lemma pair_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> pair_fm(x,y,z)  formula"
by (simp add: pair_fm_def)

lemma sats_pair_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, pair_fm(x,y,z), env) 
        pair(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: pair_fm_def pair_def)

lemma pair_iff_sats:
      "[| 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)"
by (simp)

theorem pair_reflection:
     "REFLECTS[λx. pair(L,f(x),g(x),h(x)),
               λi x. pair(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: pair_def)
apply (intro FOL_reflections upair_reflection)
done


subsubsection‹Binary Unions, Internalized›

definition
  union_fm :: "[i,i,i]=>i" where
    "union_fm(x,y,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Or(Member(0,succ(x)),Member(0,succ(y)))))"

lemma union_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> union_fm(x,y,z)  formula"
by (simp add: union_fm_def)

lemma sats_union_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, union_fm(x,y,z), env) 
        union(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: union_fm_def union_def)

lemma union_iff_sats:
      "[| 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)"
by (simp)

theorem union_reflection:
     "REFLECTS[λx. union(L,f(x),g(x),h(x)),
               λi x. union(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: union_def)
apply (intro FOL_reflections)
done


subsubsection‹Set ``Cons,'' Internalized›

definition
  cons_fm :: "[i,i,i]=>i" where
    "cons_fm(x,y,z) ==
       Exists(And(upair_fm(succ(x),succ(x),0),
                  union_fm(0,succ(y),succ(z))))"


lemma cons_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> cons_fm(x,y,z)  formula"
by (simp add: cons_fm_def)

lemma sats_cons_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, cons_fm(x,y,z), env) 
        is_cons(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: cons_fm_def is_cons_def)

lemma cons_iff_sats:
      "[| 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)"
by simp

theorem cons_reflection:
     "REFLECTS[λx. is_cons(L,f(x),g(x),h(x)),
               λi x. is_cons(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_cons_def)
apply (intro FOL_reflections upair_reflection union_reflection)
done


subsubsection‹Successor Function, Internalized›

definition
  succ_fm :: "[i,i]=>i" where
    "succ_fm(x,y) == cons_fm(x,x,y)"

lemma succ_type [TC]:
     "[| x  nat; y  nat |] ==> succ_fm(x,y)  formula"
by (simp add: succ_fm_def)

lemma sats_succ_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, succ_fm(x,y), env) 
        successor(##A, nth(x,env), nth(y,env))"
by (simp add: succ_fm_def successor_def)

lemma successor_iff_sats:
      "[| 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)"
by simp

theorem successor_reflection:
     "REFLECTS[λx. successor(L,f(x),g(x)),
               λi x. successor(##Lset(i),f(x),g(x))]"
apply (simp only: successor_def)
apply (intro cons_reflection)
done


subsubsection‹The Number 1, Internalized›

(* "number1(M,a) == (∃x[M]. empty(M,x) & successor(M,x,a))" *)
definition
  number1_fm :: "i=>i" where
    "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"

lemma number1_type [TC]:
     "x  nat ==> number1_fm(x)  formula"
by (simp add: number1_fm_def)

lemma sats_number1_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, number1_fm(x), env)  number1(##A, nth(x,env))"
by (simp add: number1_fm_def number1_def)

lemma number1_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> number1(##A, x)  sats(A, number1_fm(i), env)"
by simp

theorem number1_reflection:
     "REFLECTS[λx. number1(L,f(x)),
               λi x. number1(##Lset(i),f(x))]"
apply (simp only: number1_def)
apply (intro FOL_reflections empty_reflection successor_reflection)
done


subsubsection‹Big Union, Internalized›

(*  "big_union(M,A,z) == ∀x[M]. x ∈ z ⟷ (∃y[M]. y∈A & x ∈ y)" *)
definition
  big_union_fm :: "[i,i]=>i" where
    "big_union_fm(A,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"

lemma big_union_type [TC]:
     "[| x  nat; y  nat |] ==> big_union_fm(x,y)  formula"
by (simp add: big_union_fm_def)

lemma sats_big_union_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, big_union_fm(x,y), env) 
        big_union(##A, nth(x,env), nth(y,env))"
by (simp add: big_union_fm_def big_union_def)

lemma big_union_iff_sats:
      "[| 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)"
by simp

theorem big_union_reflection:
     "REFLECTS[λx. big_union(L,f(x),g(x)),
               λi x. big_union(##Lset(i),f(x),g(x))]"
apply (simp only: big_union_def)
apply (intro FOL_reflections)
done


subsubsection‹Variants of Satisfaction Definitions for Ordinals, etc.›

text‹The sats› theorems below are standard versions of the ones proved
in theory Formula›.  They relate elements of type term‹formula› to
relativized concepts such as term‹subset› or term‹ordinal› rather than to
real concepts such as term‹Ord›.  Now that we have instantiated the locale
M_trivial›, we no longer require the earlier versions.›

lemma sats_subset_fm':
   "[|x  nat; y  nat; env  list(A)|]
    ==> sats(A, subset_fm(x,y), env)  subset(##A, nth(x,env), nth(y,env))"
by (simp add: subset_fm_def Relative.subset_def)

theorem subset_reflection:
     "REFLECTS[λx. subset(L,f(x),g(x)),
               λi x. subset(##Lset(i),f(x),g(x))]"
apply (simp only: Relative.subset_def)
apply (intro FOL_reflections)
done

lemma sats_transset_fm':
   "[|x  nat; env  list(A)|]
    ==> sats(A, transset_fm(x), env)  transitive_set(##A, nth(x,env))"
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)

theorem transitive_set_reflection:
     "REFLECTS[λx. transitive_set(L,f(x)),
               λi x. transitive_set(##Lset(i),f(x))]"
apply (simp only: transitive_set_def)
apply (intro FOL_reflections subset_reflection)
done

lemma sats_ordinal_fm':
   "[|x  nat; env  list(A)|]
    ==> sats(A, ordinal_fm(x), env)  ordinal(##A,nth(x,env))"
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)

lemma ordinal_iff_sats:
      "[| nth(i,env) = x;  i  nat; env  list(A)|]
       ==> ordinal(##A, x)  sats(A, ordinal_fm(i), env)"
by (simp add: sats_ordinal_fm')

theorem ordinal_reflection:
     "REFLECTS[λx. ordinal(L,f(x)), λi x. ordinal(##Lset(i),f(x))]"
apply (simp only: ordinal_def)
apply (intro FOL_reflections transitive_set_reflection)
done


subsubsection‹Membership Relation, Internalized›

definition
  Memrel_fm :: "[i,i]=>i" where
    "Memrel_fm(A,r) ==
       Forall(Iff(Member(0,succ(r)),
                  Exists(And(Member(0,succ(succ(A))),
                             Exists(And(Member(0,succ(succ(succ(A)))),
                                        And(Member(1,0),
                                            pair_fm(1,0,2))))))))"

lemma Memrel_type [TC]:
     "[| x  nat; y  nat |] ==> Memrel_fm(x,y)  formula"
by (simp add: Memrel_fm_def)

lemma sats_Memrel_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, Memrel_fm(x,y), env) 
        membership(##A, nth(x,env), nth(y,env))"
by (simp add: Memrel_fm_def membership_def)

lemma Memrel_iff_sats:
      "[| 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)"
by simp

theorem membership_reflection:
     "REFLECTS[λx. membership(L,f(x),g(x)),
               λi x. membership(##Lset(i),f(x),g(x))]"
apply (simp only: membership_def)
apply (intro FOL_reflections pair_reflection)
done

subsubsection‹Predecessor Set, Internalized›

definition
  pred_set_fm :: "[i,i,i,i]=>i" where
    "pred_set_fm(A,x,r,B) ==
       Forall(Iff(Member(0,succ(B)),
                  Exists(And(Member(0,succ(succ(r))),
                             And(Member(1,succ(succ(A))),
                                 pair_fm(1,succ(succ(x)),0))))))"


lemma pred_set_type [TC]:
     "[| A  nat; x  nat; r  nat; B  nat |]
      ==> pred_set_fm(A,x,r,B)  formula"
by (simp add: pred_set_fm_def)

lemma sats_pred_set_fm [simp]:
   "[| U  nat; x  nat; r  nat; B  nat; env  list(A)|]
    ==> sats(A, pred_set_fm(U,x,r,B), env) 
        pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
by (simp add: pred_set_fm_def pred_set_def)

lemma pred_set_iff_sats:
      "[| 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)"
by (simp)

theorem pred_set_reflection:
     "REFLECTS[λx. pred_set(L,f(x),g(x),h(x),b(x)),
               λi x. pred_set(##Lset(i),f(x),g(x),h(x),b(x))]"
apply (simp only: pred_set_def)
apply (intro FOL_reflections pair_reflection)
done



subsubsection‹Domain of a Relation, Internalized›

(* "is_domain(M,r,z) ==
        ∀x[M]. (x ∈ z ⟷ (∃w[M]. w∈r & (∃y[M]. pair(M,x,y,w))))" *)
definition
  domain_fm :: "[i,i]=>i" where
    "domain_fm(r,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Exists(And(Member(0,succ(succ(r))),
                             Exists(pair_fm(2,0,1))))))"

lemma domain_type [TC]:
     "[| x  nat; y  nat |] ==> domain_fm(x,y)  formula"
by (simp add: domain_fm_def)

lemma sats_domain_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, domain_fm(x,y), env) 
        is_domain(##A, nth(x,env), nth(y,env))"
by (simp add: domain_fm_def is_domain_def)

lemma domain_iff_sats:
      "[| 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)"
by simp

theorem domain_reflection:
     "REFLECTS[λx. is_domain(L,f(x),g(x)),
               λi x. is_domain(##Lset(i),f(x),g(x))]"
apply (simp only: is_domain_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Range of a Relation, Internalized›

(* "is_range(M,r,z) ==
        ∀y[M]. (y ∈ z ⟷ (∃w[M]. w∈r & (∃x[M]. pair(M,x,y,w))))" *)
definition
  range_fm :: "[i,i]=>i" where
    "range_fm(r,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Exists(And(Member(0,succ(succ(r))),
                             Exists(pair_fm(0,2,1))))))"

lemma range_type [TC]:
     "[| x  nat; y  nat |] ==> range_fm(x,y)  formula"
by (simp add: range_fm_def)

lemma sats_range_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, range_fm(x,y), env) 
        is_range(##A, nth(x,env), nth(y,env))"
by (simp add: range_fm_def is_range_def)

lemma range_iff_sats:
      "[| 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)"
by simp

theorem range_reflection:
     "REFLECTS[λx. is_range(L,f(x),g(x)),
               λi x. is_range(##Lset(i),f(x),g(x))]"
apply (simp only: is_range_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Field of a Relation, Internalized›

(* "is_field(M,r,z) ==
        ∃dr[M]. is_domain(M,r,dr) &
            (∃rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
definition
  field_fm :: "[i,i]=>i" where
    "field_fm(r,z) ==
       Exists(And(domain_fm(succ(r),0),
              Exists(And(range_fm(succ(succ(r)),0),
                         union_fm(1,0,succ(succ(z)))))))"

lemma field_type [TC]:
     "[| x  nat; y  nat |] ==> field_fm(x,y)  formula"
by (simp add: field_fm_def)

lemma sats_field_fm [simp]:
   "[| x  nat; y  nat; env  list(A)|]
    ==> sats(A, field_fm(x,y), env) 
        is_field(##A, nth(x,env), nth(y,env))"
by (simp add: field_fm_def is_field_def)

lemma field_iff_sats:
      "[| 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)"
by simp

theorem field_reflection:
     "REFLECTS[λx. is_field(L,f(x),g(x)),
               λi x. is_field(##Lset(i),f(x),g(x))]"
apply (simp only: is_field_def)
apply (intro FOL_reflections domain_reflection range_reflection
             union_reflection)
done


subsubsection‹Image under a Relation, Internalized›

(* "image(M,r,A,z) ==
        ∀y[M]. (y ∈ z ⟷ (∃w[M]. w∈r & (∃x[M]. x∈A & pair(M,x,y,w))))" *)
definition
  image_fm :: "[i,i,i]=>i" where
    "image_fm(r,A,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Exists(And(Member(0,succ(succ(r))),
                             Exists(And(Member(0,succ(succ(succ(A)))),
                                        pair_fm(0,2,1)))))))"

lemma image_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> image_fm(x,y,z)  formula"
by (simp add: image_fm_def)

lemma sats_image_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, image_fm(x,y,z), env) 
        image(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: image_fm_def Relative.image_def)

lemma image_iff_sats:
      "[| 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)"
by (simp)

theorem image_reflection:
     "REFLECTS[λx. image(L,f(x),g(x),h(x)),
               λi x. image(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: Relative.image_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Pre-Image under a Relation, Internalized›

(* "pre_image(M,r,A,z) ==
        ∀x[M]. x ∈ z ⟷ (∃w[M]. w∈r & (∃y[M]. y∈A & pair(M,x,y,w)))" *)
definition
  pre_image_fm :: "[i,i,i]=>i" where
    "pre_image_fm(r,A,z) ==
       Forall(Iff(Member(0,succ(z)),
                  Exists(And(Member(0,succ(succ(r))),
                             Exists(And(Member(0,succ(succ(succ(A)))),
                                        pair_fm(2,0,1)))))))"

lemma pre_image_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> pre_image_fm(x,y,z)  formula"
by (simp add: pre_image_fm_def)

lemma sats_pre_image_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, pre_image_fm(x,y,z), env) 
        pre_image(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: pre_image_fm_def Relative.pre_image_def)

lemma pre_image_iff_sats:
      "[| 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)"
by (simp)

theorem pre_image_reflection:
     "REFLECTS[λx. pre_image(L,f(x),g(x),h(x)),
               λi x. pre_image(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: Relative.pre_image_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Function Application, Internalized›

(* "fun_apply(M,f,x,y) ==
        (∃xs[M]. ∃fxs[M].
         upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
definition
  fun_apply_fm :: "[i,i,i]=>i" where
    "fun_apply_fm(f,x,y) ==
       Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
                         And(image_fm(succ(succ(f)), 1, 0),
                             big_union_fm(0,succ(succ(y)))))))"

lemma fun_apply_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> fun_apply_fm(x,y,z)  formula"
by (simp add: fun_apply_fm_def)

lemma sats_fun_apply_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, fun_apply_fm(x,y,z), env) 
        fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: fun_apply_fm_def fun_apply_def)

lemma fun_apply_iff_sats:
      "[| 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)"
by simp

theorem fun_apply_reflection:
     "REFLECTS[λx. fun_apply(L,f(x),g(x),h(x)),
               λi x. fun_apply(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: fun_apply_def)
apply (intro FOL_reflections upair_reflection image_reflection
             big_union_reflection)
done


subsubsection‹The Concept of Relation, Internalized›

(* "is_relation(M,r) ==
        (∀z[M]. z∈r ⟶ (∃x[M]. ∃y[M]. pair(M,x,y,z)))" *)
definition
  relation_fm :: "i=>i" where
    "relation_fm(r) ==
       Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"

lemma relation_type [TC]:
     "[| x  nat |] ==> relation_fm(x)  formula"
by (simp add: relation_fm_def)

lemma sats_relation_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, relation_fm(x), env)  is_relation(##A, nth(x,env))"
by (simp add: relation_fm_def is_relation_def)

lemma relation_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> is_relation(##A, x)  sats(A, relation_fm(i), env)"
by simp

theorem is_relation_reflection:
     "REFLECTS[λx. is_relation(L,f(x)),
               λi x. is_relation(##Lset(i),f(x))]"
apply (simp only: is_relation_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹The Concept of Function, Internalized›

(* "is_function(M,r) ==
        ∀x[M]. ∀y[M]. ∀y'[M]. ∀p[M]. ∀p'[M].
           pair(M,x,y,p) ⟶ pair(M,x,y',p') ⟶ p∈r ⟶ p'∈r ⟶ y=y'" *)
definition
  function_fm :: "i=>i" where
    "function_fm(r) ==
       Forall(Forall(Forall(Forall(Forall(
         Implies(pair_fm(4,3,1),
                 Implies(pair_fm(4,2,0),
                         Implies(Member(1,r#+5),
                                 Implies(Member(0,r#+5), Equal(3,2))))))))))"

lemma function_type [TC]:
     "[| x  nat |] ==> function_fm(x)  formula"
by (simp add: function_fm_def)

lemma sats_function_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, function_fm(x), env)  is_function(##A, nth(x,env))"
by (simp add: function_fm_def is_function_def)

lemma is_function_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> is_function(##A, x)  sats(A, function_fm(i), env)"
by simp

theorem is_function_reflection:
     "REFLECTS[λx. is_function(L,f(x)),
               λi x. is_function(##Lset(i),f(x))]"
apply (simp only: is_function_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Typed Functions, Internalized›

(* "typed_function(M,A,B,r) ==
        is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
        (∀u[M]. u∈r ⟶ (∀x[M]. ∀y[M]. pair(M,x,y,u) ⟶ y∈B))" *)

definition
  typed_function_fm :: "[i,i,i]=>i" where
    "typed_function_fm(A,B,r) ==
       And(function_fm(r),
         And(relation_fm(r),
           And(domain_fm(r,A),
             Forall(Implies(Member(0,succ(r)),
                  Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))"

lemma typed_function_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> typed_function_fm(x,y,z)  formula"
by (simp add: typed_function_fm_def)

lemma sats_typed_function_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, typed_function_fm(x,y,z), env) 
        typed_function(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: typed_function_fm_def typed_function_def)

lemma typed_function_iff_sats:
  "[| 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)"
by simp

lemmas function_reflections =
        empty_reflection number1_reflection
        upair_reflection pair_reflection union_reflection
        big_union_reflection cons_reflection successor_reflection
        fun_apply_reflection subset_reflection
        transitive_set_reflection membership_reflection
        pred_set_reflection domain_reflection range_reflection field_reflection
        image_reflection pre_image_reflection
        is_relation_reflection is_function_reflection

lemmas function_iff_sats =
        empty_iff_sats number1_iff_sats
        upair_iff_sats pair_iff_sats union_iff_sats
        big_union_iff_sats cons_iff_sats successor_iff_sats
        fun_apply_iff_sats  Memrel_iff_sats
        pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
        image_iff_sats pre_image_iff_sats
        relation_iff_sats is_function_iff_sats


theorem typed_function_reflection:
     "REFLECTS[λx. typed_function(L,f(x),g(x),h(x)),
               λi x. typed_function(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: typed_function_def)
apply (intro FOL_reflections function_reflections)
done


subsubsection‹Composition of Relations, Internalized›

(* "composition(M,r,s,t) ==
        ∀p[M]. p ∈ t ⟷
               (∃x[M]. ∃y[M]. ∃z[M]. ∃xy[M]. ∃yz[M].
                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
                xy ∈ s & yz ∈ r)" *)
definition
  composition_fm :: "[i,i,i]=>i" where
  "composition_fm(r,s,t) ==
     Forall(Iff(Member(0,succ(t)),
             Exists(Exists(Exists(Exists(Exists(
              And(pair_fm(4,2,5),
               And(pair_fm(4,3,1),
                And(pair_fm(3,2,0),
                 And(Member(1,s#+6), Member(0,r#+6))))))))))))"

lemma composition_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> composition_fm(x,y,z)  formula"
by (simp add: composition_fm_def)

lemma sats_composition_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, composition_fm(x,y,z), env) 
        composition(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: composition_fm_def composition_def)

lemma composition_iff_sats:
      "[| 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)"
by simp

theorem composition_reflection:
     "REFLECTS[λx. composition(L,f(x),g(x),h(x)),
               λi x. composition(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: composition_def)
apply (intro FOL_reflections pair_reflection)
done


subsubsection‹Injections, Internalized›

(* "injection(M,A,B,f) ==
        typed_function(M,A,B,f) &
        (∀x[M]. ∀x'[M]. ∀y[M]. ∀p[M]. ∀p'[M].
          pair(M,x,y,p) ⟶ pair(M,x',y,p') ⟶ p∈f ⟶ p'∈f ⟶ x=x')" *)
definition
  injection_fm :: "[i,i,i]=>i" where
  "injection_fm(A,B,f) ==
    And(typed_function_fm(A,B,f),
       Forall(Forall(Forall(Forall(Forall(
         Implies(pair_fm(4,2,1),
                 Implies(pair_fm(3,2,0),
                         Implies(Member(1,f#+5),
                                 Implies(Member(0,f#+5), Equal(4,3)))))))))))"


lemma injection_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> injection_fm(x,y,z)  formula"
by (simp add: injection_fm_def)

lemma sats_injection_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, injection_fm(x,y,z), env) 
        injection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: injection_fm_def injection_def)

lemma injection_iff_sats:
  "[| 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)"
by simp

theorem injection_reflection:
     "REFLECTS[λx. injection(L,f(x),g(x),h(x)),
               λi x. injection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: injection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done


subsubsection‹Surjections, Internalized›

(*  surjection :: "[i=>o,i,i,i] => o"
    "surjection(M,A,B,f) ==
        typed_function(M,A,B,f) &
        (∀y[M]. y∈B ⟶ (∃x[M]. x∈A & fun_apply(M,f,x,y)))" *)
definition
  surjection_fm :: "[i,i,i]=>i" where
  "surjection_fm(A,B,f) ==
    And(typed_function_fm(A,B,f),
       Forall(Implies(Member(0,succ(B)),
                      Exists(And(Member(0,succ(succ(A))),
                                 fun_apply_fm(succ(succ(f)),0,1))))))"

lemma surjection_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> surjection_fm(x,y,z)  formula"
by (simp add: surjection_fm_def)

lemma sats_surjection_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, surjection_fm(x,y,z), env) 
        surjection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: surjection_fm_def surjection_def)

lemma surjection_iff_sats:
  "[| 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)"
by simp

theorem surjection_reflection:
     "REFLECTS[λx. surjection(L,f(x),g(x),h(x)),
               λi x. surjection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: surjection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done



subsubsection‹Bijections, Internalized›

(*   bijection :: "[i=>o,i,i,i] => o"
    "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
definition
  bijection_fm :: "[i,i,i]=>i" where
  "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"

lemma bijection_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> bijection_fm(x,y,z)  formula"
by (simp add: bijection_fm_def)

lemma sats_bijection_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, bijection_fm(x,y,z), env) 
        bijection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: bijection_fm_def bijection_def)

lemma bijection_iff_sats:
  "[| 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)"
by simp

theorem bijection_reflection:
     "REFLECTS[λx. bijection(L,f(x),g(x),h(x)),
               λi x. bijection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: bijection_def)
apply (intro And_reflection injection_reflection surjection_reflection)
done


subsubsection‹Restriction of a Relation, Internalized›


(* "restriction(M,r,A,z) ==
        ∀x[M]. x ∈ z ⟷ (x ∈ r & (∃u[M]. u∈A & (∃v[M]. pair(M,u,v,x))))" *)
definition
  restriction_fm :: "[i,i,i]=>i" where
    "restriction_fm(r,A,z) ==
       Forall(Iff(Member(0,succ(z)),
                  And(Member(0,succ(r)),
                      Exists(And(Member(0,succ(succ(A))),
                                 Exists(pair_fm(1,0,2)))))))"

lemma restriction_type [TC]:
     "[| x  nat; y  nat; z  nat |] ==> restriction_fm(x,y,z)  formula"
by (simp add: restriction_fm_def)

lemma sats_restriction_fm [simp]:
   "[| x  nat; y  nat; z  nat; env  list(A)|]
    ==> sats(A, restriction_fm(x,y,z), env) 
        restriction(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: restriction_fm_def restriction_def)

lemma restriction_iff_sats:
      "[| 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)"
by simp

theorem restriction_reflection:
     "REFLECTS[λx. restriction(L,f(x),g(x),h(x)),
               λi x. restriction(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: restriction_def)
apply (intro FOL_reflections pair_reflection)
done

subsubsection‹Order-Isomorphisms, Internalized›

(*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   "order_isomorphism(M,A,r,B,s,f) ==
        bijection(M,A,B,f) &
        (∀x[M]. x∈A ⟶ (∀y[M]. y∈A ⟶
          (∀p[M]. ∀fx[M]. ∀fy[M]. ∀q[M].
            pair(M,x,y,p) ⟶ fun_apply(M,f,x,fx) ⟶ fun_apply(M,f,y,fy) ⟶
            pair(M,fx,fy,q) ⟶ (p∈r ⟷ q∈s))))"
  *)

definition
  order_isomorphism_fm :: "[i,i,i,i,i]=>i" where
 "order_isomorphism_fm(A,r,B,s,f) ==
   And(bijection_fm(A,B,f),
     Forall(Implies(Member(0,succ(A)),
       Forall(Implies(Member(0,succ(succ(A))),
         Forall(Forall(Forall(Forall(
           Implies(pair_fm(5,4,3),
             Implies(fun_apply_fm(f#+6,5,2),
               Implies(fun_apply_fm(f#+6,4,1),
                 Implies(pair_fm(2,1,0),
                   Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))"

lemma order_isomorphism_type [TC]:
     "[| A  nat; r  nat; B  nat; s  nat; f  nat |]
      ==> order_isomorphism_fm(A,r,B,s,f)  formula"
by (simp add: order_isomorphism_fm_def)

lemma sats_order_isomorphism_fm [simp]:
   "[| U  nat; r  nat; B  nat; s  nat; f  nat; env  list(A)|]
    ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) 
        order_isomorphism(##A, nth(U,env), nth(r,env), nth(B,env),
                               nth(s,env), nth(f,env))"
by (simp add: order_isomorphism_fm_def order_isomorphism_def)

lemma order_isomorphism_iff_sats:
  "[| 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)"
by simp

theorem order_isomorphism_reflection:
     "REFLECTS[λx. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
               λi x. order_isomorphism(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
apply (simp only: order_isomorphism_def)
apply (intro FOL_reflections function_reflections bijection_reflection)
done

subsubsection‹Limit Ordinals, Internalized›

text‹A limit ordinal is a non-empty, successor-closed ordinal›

(* "limit_ordinal(M,a) ==
        ordinal(M,a) & ~ empty(M,a) &
        (∀x[M]. x∈a ⟶ (∃y[M]. y∈a & successor(M,x,y)))" *)

definition
  limit_ordinal_fm :: "i=>i" where
    "limit_ordinal_fm(x) ==
        And(ordinal_fm(x),
            And(Neg(empty_fm(x)),
                Forall(Implies(Member(0,succ(x)),
                               Exists(And(Member(0,succ(succ(x))),
                                          succ_fm(1,0)))))))"

lemma limit_ordinal_type [TC]:
     "x  nat ==> limit_ordinal_fm(x)  formula"
by (simp add: limit_ordinal_fm_def)

lemma sats_limit_ordinal_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, limit_ordinal_fm(x), env)  limit_ordinal(##A, nth(x,env))"
by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')

lemma limit_ordinal_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> limit_ordinal(##A, x)  sats(A, limit_ordinal_fm(i), env)"
by simp

theorem limit_ordinal_reflection:
     "REFLECTS[λx. limit_ordinal(L,f(x)),
               λi x. limit_ordinal(##Lset(i),f(x))]"
apply (simp only: limit_ordinal_def)
apply (intro FOL_reflections ordinal_reflection
             empty_reflection successor_reflection)
done

subsubsection‹Finite Ordinals: The Predicate ``Is A Natural Number''›

(*     "finite_ordinal(M,a) == 
        ordinal(M,a) & ~ limit_ordinal(M,a) & 
        (∀x[M]. x∈a ⟶ ~ limit_ordinal(M,x))" *)
definition
  finite_ordinal_fm :: "i=>i" where
    "finite_ordinal_fm(x) ==
       And(ordinal_fm(x),
          And(Neg(limit_ordinal_fm(x)),
           Forall(Implies(Member(0,succ(x)),
                          Neg(limit_ordinal_fm(0))))))"

lemma finite_ordinal_type [TC]:
     "x  nat ==> finite_ordinal_fm(x)  formula"
by (simp add: finite_ordinal_fm_def)

lemma sats_finite_ordinal_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, finite_ordinal_fm(x), env)  finite_ordinal(##A, nth(x,env))"
by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)

lemma finite_ordinal_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> finite_ordinal(##A, x)  sats(A, finite_ordinal_fm(i), env)"
by simp

theorem finite_ordinal_reflection:
     "REFLECTS[λx. finite_ordinal(L,f(x)),
               λi x. finite_ordinal(##Lset(i),f(x))]"
apply (simp only: finite_ordinal_def)
apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
done


subsubsection‹Omega: The Set of Natural Numbers›

(* omega(M,a) == limit_ordinal(M,a) & (∀x[M]. x∈a ⟶ ~ limit_ordinal(M,x)) *)
definition
  omega_fm :: "i=>i" where
    "omega_fm(x) ==
       And(limit_ordinal_fm(x),
           Forall(Implies(Member(0,succ(x)),
                          Neg(limit_ordinal_fm(0)))))"

lemma omega_type [TC]:
     "x  nat ==> omega_fm(x)  formula"
by (simp add: omega_fm_def)

lemma sats_omega_fm [simp]:
   "[| x  nat; env  list(A)|]
    ==> sats(A, omega_fm(x), env)  omega(##A, nth(x,env))"
by (simp add: omega_fm_def omega_def)

lemma omega_iff_sats:
      "[| nth(i,env) = x; nth(j,env) = y;
          i  nat; env  list(A)|]
       ==> omega(##A, x)  sats(A, omega_fm(i), env)"
by simp

theorem omega_reflection:
     "REFLECTS[λx. omega(L,f(x)),
               λi x. omega(##Lset(i),f(x))]"
apply (simp only: omega_def)
apply (intro FOL_reflections limit_ordinal_reflection)
done


lemmas fun_plus_reflections =
        typed_function_reflection composition_reflection
        injection_reflection surjection_reflection
        bijection_reflection restriction_reflection
        order_isomorphism_reflection finite_ordinal_reflection 
        ordinal_reflection limit_ordinal_reflection omega_reflection

lemmas fun_plus_iff_sats =
        typed_function_iff_sats composition_iff_sats
        injection_iff_sats surjection_iff_sats
        bijection_iff_sats restriction_iff_sats
        order_isomorphism_iff_sats finite_ordinal_iff_sats
        ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats

end