diff --git a/src/ZF/Constructible/AC_in_L.thy b/src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy
+++ b/src/ZF/Constructible/AC_in_L.thy
@@ -1,479 +1,479 @@
 (*  Title:      ZF/Constructible/AC_in_L.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section \<open>The Axiom of Choice Holds in L!\<close>
 
 theory AC_in_L imports Formula Separation begin
 
 subsection\<open>Extending a Wellordering over a List -- Lexicographic Power\<close>
 
 text\<open>This could be moved into a library.\<close>
 
 consts
   rlist   :: "[i,i]=>i"
 
 inductive
   domains "rlist(A,r)" \<subseteq> "list(A) * list(A)"
   intros
     shorterI:
       "[| length(l') < length(l); l' \<in> list(A); l \<in> list(A) |]
        ==> <l', l> \<in> rlist(A,r)"
 
     sameI:
       "[| <l',l> \<in> rlist(A,r); a \<in> A |]
        ==> <Cons(a,l'), Cons(a,l)> \<in> rlist(A,r)"
 
     diffI:
       "[| length(l') = length(l); <a',a> \<in> r;
           l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |]
        ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)"
   type_intros list.intros
 
 
 subsubsection\<open>Type checking\<close>
 
 lemmas rlist_type = rlist.dom_subset
 
 lemmas field_rlist = rlist_type [THEN field_rel_subset]
 
 subsubsection\<open>Linearity\<close>
 
 lemma rlist_Nil_Cons [intro]:
     "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)"
 by (simp add: shorterI)
 
 lemma linear_rlist:
   assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))"
 proof -
   { fix xs ys
     have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r) "
     proof (induct xs arbitrary: ys rule: list.induct)
       case Nil 
       thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI)
     next
       case (Cons x xs)
       { fix y ys
         assume "y \<in> A" and "ys \<in> list(A)"
         with Cons
         have "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y & xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)" 
           apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt)
           apply (simp_all add: shorterI)
           apply (rule linearE [OF r, of x y]) 
           apply (auto simp add: diffI intro: sameI) 
           done
       }
       note yConsCase = this
       show ?case using \<open>ys \<in> list(A)\<close>
         by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) 
     qed
   }
   thus ?thesis by (simp add: linear_def) 
 qed
 
 
 subsubsection\<open>Well-foundedness\<close>
 
 text\<open>Nothing preceeds Nil in this ordering.\<close>
 inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)"
 
 inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)"
 
 lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)"
 by (blast intro: elim: rlist_NilE)
 
 lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)"
 apply (erule rlist.induct)
 apply (simp_all add: leI)
 done
 
 lemma wf_on_rlist_n:
   "[| n \<in> nat; wf[A](r) |] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))"
 apply (induct_tac n)
  apply (rule wf_onI2, simp)
 apply (rule wf_onI2, clarify)
 apply (erule_tac a=y in list.cases, clarify)
  apply (simp (no_asm_use))
 apply clarify
 apply (simp (no_asm_use))
 apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x \<longrightarrow> Cons(a,l2) \<in> B", blast)
 apply (erule_tac a=a in wf_on_induct, assumption)
 apply (rule ballI)
 apply (rule impI)
 apply (erule_tac a=l2 in wf_on_induct, blast, clarify)
 apply (rename_tac a' l2 l')
 apply (drule_tac x="Cons(a',l')" in bspec, typecheck)
 apply simp
 apply (erule mp, clarify)
 apply (erule rlist_ConsE, auto)
 done
 
 lemma list_eq_UN_length: "list(A) = (\<Union>n\<in>nat. {l \<in> list(A). length(l) = n})"
 by (blast intro: length_type)
 
 
 lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))"
 apply (subst list_eq_UN_length)
 apply (rule wf_on_Union)
   apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]])
  apply (simp add: wf_on_rlist_n)
 apply (frule rlist_type [THEN subsetD])
 apply (simp add: length_type)
 apply (drule rlist_imp_length_le)
 apply (erule leE)
 apply (simp_all add: lt_def)
 done
 
 
 lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))"
 apply (simp add: wf_iff_wf_on_field)
 apply (rule wf_on_subset_A [OF _ field_rlist])
 apply (blast intro: wf_on_rlist)
 done
 
 lemma well_ord_rlist:
      "well_ord(A,r) ==> well_ord(list(A), rlist(A,r))"
 apply (rule well_ordI)
 apply (simp add: well_ord_def wf_on_rlist)
 apply (simp add: well_ord_def tot_ord_def linear_rlist)
 done
 
 
 subsection\<open>An Injection from Formulas into the Natural Numbers\<close>
 
 text\<open>There is a well-known bijection between \<^term>\<open>nat*nat\<close> and \<^term>\<open>nat\<close> given by the expression f(m,n) = triangle(m+n) + m, where triangle(k)
 enumerates the triangular numbers and can be defined by triangle(0)=0,
 triangle(succ(k)) = succ(k + triangle(k)).  Some small amount of effort is
 needed to show that f is a bijection.  We already know that such a bijection exists by the theorem \<open>well_ord_InfCard_square_eq\<close>:
 @{thm[display] well_ord_InfCard_square_eq[no_vars]}
 
 However, this result merely states that there is a bijection between the two
 sets.  It provides no means of naming a specific bijection.  Therefore, we
 conduct the proofs under the assumption that a bijection exists.  The simplest
 way to organize this is to use a locale.\<close>
 
 text\<open>Locale for any arbitrary injection between \<^term>\<open>nat*nat\<close>
       and \<^term>\<open>nat\<close>\<close>
 locale Nat_Times_Nat =
   fixes fn
   assumes fn_inj: "fn \<in> inj(nat*nat, nat)"
 
 
 consts   enum :: "[i,i]=>i"
 primrec
   "enum(f, Member(x,y)) = f ` <0, f ` <x,y>>"
   "enum(f, Equal(x,y)) = f ` <1, f ` <x,y>>"
   "enum(f, Nand(p,q)) = f ` <2, f ` <enum(f,p), enum(f,q)>>"
   "enum(f, Forall(p)) = f ` <succ(2), enum(f,p)>"
 
 lemma (in Nat_Times_Nat) fn_type [TC,simp]:
     "[|x \<in> nat; y \<in> nat|] ==> fn`<x,y> \<in> nat"
 by (blast intro: inj_is_fun [OF fn_inj] apply_funtype)
 
 lemma (in Nat_Times_Nat) fn_iff:
     "[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|]
      ==> (fn`<x,y> = fn`<u,v>) \<longleftrightarrow> (x=u & y=v)"
 by (blast dest: inj_apply_equality [OF fn_inj])
 
 lemma (in Nat_Times_Nat) enum_type [TC,simp]:
     "p \<in> formula ==> enum(fn,p) \<in> nat"
 by (induct_tac p, simp_all)
 
 lemma (in Nat_Times_Nat) enum_inject [rule_format]:
     "p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) \<longrightarrow> p=q"
 apply (induct_tac p, simp_all)
    apply (rule ballI)
    apply (erule formula.cases)
    apply (simp_all add: fn_iff)
   apply (rule ballI)
   apply (erule formula.cases)
   apply (simp_all add: fn_iff)
  apply (rule ballI)
  apply (erule_tac a=qa in formula.cases)
  apply (simp_all add: fn_iff)
  apply blast
 apply (rule ballI)
 apply (erule_tac a=q in formula.cases)
 apply (simp_all add: fn_iff, blast)
 done
 
 lemma (in Nat_Times_Nat) inj_formula_nat:
     "(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)"
 apply (simp add: inj_def lam_type)
 apply (blast intro: enum_inject)
 done
 
 lemma (in Nat_Times_Nat) well_ord_formula:
     "well_ord(formula, measure(formula, enum(fn)))"
 apply (rule well_ord_measure, simp)
 apply (blast intro: enum_inject)
 done
 
 lemmas nat_times_nat_lepoll_nat =
     InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll]
 
 
 text\<open>Not needed--but interesting?\<close>
 theorem formula_lepoll_nat: "formula \<lesssim> nat"
 apply (insert nat_times_nat_lepoll_nat)
 apply (unfold lepoll_def)
 apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
 done
 
 
 subsection\<open>Defining the Wellordering on \<^term>\<open>DPow(A)\<close>\<close>
 
 text\<open>The objective is to build a wellordering on \<^term>\<open>DPow(A)\<close> from a
 given one on \<^term>\<open>A\<close>.  We first introduce wellorderings for environments,
 which are lists built over \<^term>\<open>A\<close>.  We combine it with the enumeration of
 formulas.  The order type of the resulting wellordering gives us a map from
 (environment, formula) pairs into the ordinals.  For each member of \<^term>\<open>DPow(A)\<close>, we take the minimum such ordinal.\<close>
 
 definition
   env_form_r :: "[i,i,i]=>i" where
     \<comment> \<open>wellordering on (environment, formula) pairs\<close>
    "env_form_r(f,r,A) ==
       rmult(list(A), rlist(A, r),
             formula, measure(formula, enum(f)))"
 
 definition
   env_form_map :: "[i,i,i,i]=>i" where
     \<comment> \<open>map from (environment, formula) pairs to ordinals\<close>
    "env_form_map(f,r,A,z)
       == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
 
 definition
   DPow_ord :: "[i,i,i,i,i]=>o" where
     \<comment> \<open>predicate that holds if \<^term>\<open>k\<close> is a valid index for \<^term>\<open>X\<close>\<close>
    "DPow_ord(f,r,A,X,k) ==
            \<exists>env \<in> list(A). \<exists>p \<in> formula.
              arity(p) \<le> succ(length(env)) &
              X = {x\<in>A. sats(A, p, Cons(x,env))} &
              env_form_map(f,r,A,<env,p>) = k"
 
 definition
   DPow_least :: "[i,i,i,i]=>i" where
     \<comment> \<open>function yielding the smallest index for \<^term>\<open>X\<close>\<close>
    "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
 
 definition
   DPow_r :: "[i,i,i]=>i" where
     \<comment> \<open>a wellordering on \<^term>\<open>DPow(A)\<close>\<close>
    "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"
 
 
 lemma (in Nat_Times_Nat) well_ord_env_form_r:
     "well_ord(A,r)
      ==> well_ord(list(A) * formula, env_form_r(fn,r,A))"
 by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula)
 
 lemma (in Nat_Times_Nat) Ord_env_form_map:
     "[|well_ord(A,r); z \<in> list(A) * formula|]
      ==> Ord(env_form_map(fn,r,A,z))"
 by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r)
 
 lemma DPow_imp_ex_DPow_ord:
     "X \<in> DPow(A) ==> \<exists>k. DPow_ord(fn,r,A,X,k)"
 apply (simp add: DPow_ord_def)
 apply (blast dest!: DPowD)
 done
 
 lemma (in Nat_Times_Nat) DPow_ord_imp_Ord:
      "[|DPow_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)"
 apply (simp add: DPow_ord_def, clarify)
 apply (simp add: Ord_env_form_map)
 done
 
 lemma (in Nat_Times_Nat) DPow_imp_DPow_least:
     "[|X \<in> DPow(A); well_ord(A,r)|]
      ==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))"
 apply (simp add: DPow_least_def)
 apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI)
 done
 
 lemma (in Nat_Times_Nat) env_form_map_inject:
     "[|env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r);
        u \<in> list(A) * formula;  v \<in> list(A) * formula|]
      ==> u=v"
 apply (simp add: env_form_map_def)
 apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij,
                                 OF well_ord_env_form_r], assumption+)
 done
 
 lemma (in Nat_Times_Nat) DPow_ord_unique:
     "[|DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)|]
      ==> X=Y"
 apply (simp add: DPow_ord_def, clarify)
 apply (drule env_form_map_inject, auto)
 done
 
 lemma (in Nat_Times_Nat) well_ord_DPow_r:
     "well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))"
 apply (simp add: DPow_r_def)
 apply (rule well_ord_measure)
  apply (simp add: DPow_least_def)
 apply (drule DPow_imp_DPow_least, assumption)+
 apply simp
 apply (blast intro: DPow_ord_unique)
 done
 
 lemma (in Nat_Times_Nat) DPow_r_type:
     "DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)"
 by (simp add: DPow_r_def measure_def, blast)
 
 
 subsection\<open>Limit Construction for Well-Orderings\<close>
 
 text\<open>Now we work towards the transfinite definition of wellorderings for
 \<^term>\<open>Lset(i)\<close>.  We assume as an inductive hypothesis that there is a family
 of wellorderings for smaller ordinals.\<close>
 
 definition
   rlimit :: "[i,i=>i]=>i" where
   \<comment> \<open>Expresses the wellordering at limit ordinals.  The conditional
       lets us remove the premise \<^term>\<open>Limit(i)\<close> from some theorems.\<close>
     "rlimit(i,r) ==
        if Limit(i) then 
          {z: Lset(i) * Lset(i).
           \<exists>x' x. z = <x',x> &
                  (lrank(x') < lrank(x) |
                   (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
        else 0"
 
 definition
   Lset_new :: "i=>i" where
   \<comment> \<open>This constant denotes the set of elements introduced at level
       \<^term>\<open>succ(i)\<close>\<close>
     "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
 
 lemma Limit_Lset_eq2:
     "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"
 apply (simp add: Limit_Lset_eq)
 apply (rule equalityI)
  apply safe
  apply (subgoal_tac "Ord(y)")
   prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
  apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
                       Ord_mem_iff_lt)
  apply (blast intro: lt_trans)
 apply (rule_tac x = "succ(lrank(x))" in bexI)
  apply (simp)
 apply (blast intro: Limit_has_succ ltD)
 done
 
 lemma wf_on_Lset:
     "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))"
 apply (simp add: wf_on_def Lset_new_def)
 apply (erule wf_subset)
 apply (simp add: rlimit_def, force)
 done
 
 lemma wf_on_rlimit:
     "(\<forall>j<i. wf[Lset(j)](r(j))) ==> wf[Lset(i)](rlimit(i,r))"
 apply (case_tac "Limit(i)") 
  prefer 2
  apply (simp add: rlimit_def wf_on_any_0)
 apply (simp add: Limit_Lset_eq2)
 apply (rule wf_on_Union)
   apply (rule wf_imp_wf_on [OF wf_Memrel [of i]])
  apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI)
 apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
                        Ord_mem_iff_lt)
 done
 
 lemma linear_rlimit:
     "[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |]
      ==> linear(Lset(i), rlimit(i,r))"
 apply (frule Limit_is_Ord)
 apply (simp add: Limit_Lset_eq2 Lset_new_def)
 apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt)
 apply (simp add: ltI, clarify)
 apply (rename_tac u v)
 apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) 
 apply (drule_tac x="succ(lrank(u) \<union> lrank(v))" in ospec)
  apply (simp add: ltI)
 apply (drule_tac x=u in spec, simp)
 apply (drule_tac x=v in spec, simp)
 done
 
 lemma well_ord_rlimit:
     "[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |]
      ==> well_ord(Lset(i), rlimit(i,r))"
 by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf
                            linear_rlimit well_ord_is_linear)
 
 lemma rlimit_cong:
      "(!!j. j<i ==> r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')"
 apply (simp add: rlimit_def, clarify) 
 apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
 apply (simp add: Limit_is_Ord Lset_lrank_lt)
 done
 
 
 subsection\<open>Transfinite Definition of the Wellordering on \<^term>\<open>L\<close>\<close>
 
 definition
   L_r :: "[i, i] => i" where
   "L_r(f) == %i.
       transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), 
                 \<lambda>x r. rlimit(x, \<lambda>y. r`y))"
 
 subsubsection\<open>The Corresponding Recursion Equations\<close>
 lemma [simp]: "L_r(f,0) = 0"
 by (simp add: L_r_def)
 
 lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))"
 by (simp add: L_r_def)
 
 text\<open>The limit case is non-trivial because of the distinction between
 object-level and meta-level abstraction.\<close>
 lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))"
 by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD)
 
 lemma (in Nat_Times_Nat) L_r_type:
     "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
 apply (induct i rule: trans_induct3)
   apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def
                        Transset_subset_DPow [OF Transset_Lset], blast)
 done
 
 lemma (in Nat_Times_Nat) well_ord_L_r:
     "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))"
 apply (induct i rule: trans_induct3)
 apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r
                      well_ord_rlimit ltD)
 done
 
 lemma well_ord_L_r:
     "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)"
 apply (insert nat_times_nat_lepoll_nat)
 apply (unfold lepoll_def)
 apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
 done
 
 
 text\<open>Every constructible set is well-ordered! Therefore the Wellordering Theorem and
       the Axiom of Choice hold in \<^term>\<open>L\<close>!!\<close>
 theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
   using Transset_Lset x
 apply (simp add: Transset_def L_def)
 apply (blast dest!: well_ord_L_r intro: well_ord_subset)
 done
 
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
 proof 
   fix x
   assume "L(x)"
   then obtain r where "well_ord(x,r)" 
     by (blast dest: L_implies_AC) 
   thus "\<exists>r. wellordered(L,x,r)" 
-    by (blast intro: well_ord_imp_relativized)
+    by (blast intro: L.well_ord_imp_relativized)
 qed
 
 text\<open>In order to prove \<^term>\<open> \<exists>r[L]. wellordered(L,x,r)\<close>, it's necessary to know 
 that \<^term>\<open>r\<close> is actually constructible. It follows from the assumption ``\<^term>\<open>V\<close> equals \<^term>\<open>L''\<close>, 
 but this reasoning doesn't appear to work in Isabelle.\<close>
 
 end
diff --git a/src/ZF/Constructible/DPow_absolute.thy b/src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy
+++ b/src/ZF/Constructible/DPow_absolute.thy
@@ -1,627 +1,627 @@
 (*  Title:      ZF/Constructible/DPow_absolute.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section \<open>Absoluteness for the Definable Powerset Function\<close>
 
 
 theory DPow_absolute imports Satisfies_absolute begin
 
 
 subsection\<open>Preliminary Internalizations\<close>
 
 subsubsection\<open>The Operator \<^term>\<open>is_formula_rec\<close>\<close>
 
 text\<open>The three arguments of \<^term>\<open>p\<close> are always 2, 1, 0.  It is buried
    within 11 quantifiers!!\<close>
 
 (* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
    "is_formula_rec(M,MH,p,z)  ==
       \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
        2       1      0
              successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
 *)
 
 definition
   formula_rec_fm :: "[i, i, i]=>i" where
  "formula_rec_fm(mh,p,z) == 
     Exists(Exists(Exists(
       And(finite_ordinal_fm(2),
        And(depth_fm(p#+3,2),
         And(succ_fm(2,1), 
           And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))"
 
 lemma is_formula_rec_type [TC]:
      "[| p \<in> formula; x \<in> nat; z \<in> nat |] 
       ==> formula_rec_fm(p,x,z) \<in> formula"
 by (simp add: formula_rec_fm_def) 
 
 lemma sats_formula_rec_fm:
   assumes MH_iff_sats: 
       "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
         ==> MH(a2, a1, a0) \<longleftrightarrow> 
             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,
                                   Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
   shows 
       "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
        ==> sats(A, formula_rec_fm(p,x,z), env) \<longleftrightarrow> 
            is_formula_rec(##A, MH, nth(x,env), nth(z,env))"
 by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def 
               MH_iff_sats [THEN iff_sym])
 
 lemma formula_rec_iff_sats:
   assumes MH_iff_sats: 
       "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
         ==> MH(a2, a1, a0) \<longleftrightarrow> 
             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,
                                   Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
   shows
   "[|nth(i,env) = x; nth(k,env) = z; 
       i \<in> nat; k \<in> nat; env \<in> list(A)|]
    ==> is_formula_rec(##A, MH, x, z) \<longleftrightarrow> sats(A, formula_rec_fm(p,i,k), env)" 
 by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
 
 theorem formula_rec_reflection:
   assumes MH_reflection:
     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
                      \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)), 
                \<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
 apply (simp (no_asm_use) only: is_formula_rec_def)
 apply (intro FOL_reflections function_reflections fun_plus_reflections
              depth_reflection is_transrec_reflection MH_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_satisfies\<close>\<close>
 
 (* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
 definition
   satisfies_fm :: "[i,i,i]=>i" where
     "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
 
 lemma is_satisfies_type [TC]:
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
 by (simp add: satisfies_fm_def)
 
 lemma sats_satisfies_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
         is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: satisfies_fm_def is_satisfies_def sats_formula_rec_fm)
 
 lemma satisfies_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
 by (simp)
 
 theorem satisfies_reflection:
      "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
                \<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_satisfies_def)
 apply (intro formula_rec_reflection satisfies_MH_reflection)
 done
 
 
 subsection \<open>Relativization of the Operator \<^term>\<open>DPow'\<close>\<close>
 
 lemma DPow'_eq: 
   "DPow'(A) = {z . ep \<in> list(A) * formula, 
                     \<exists>env \<in> list(A). \<exists>p \<in> formula. 
                        ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))}}"
 by (simp add: DPow'_def, blast) 
 
 
 text\<open>Relativize the use of \<^term>\<open>sats\<close> within \<^term>\<open>DPow'\<close>
 (the comprehension).\<close>
 definition
   is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
    "is_DPow_sats(M,A,env,p,x) ==
       \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
              is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
              fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1)"
 
 lemma (in M_satisfies) DPow_sats_abs:
     "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
     ==> is_DPow_sats(M,A,env,p,x) \<longleftrightarrow> sats(A, p, Cons(x,env))"
 apply (subgoal_tac "M(env)") 
  apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) 
 apply (blast dest: transM) 
 done
 
 lemma (in M_satisfies) Collect_DPow_sats_abs:
     "[| M(A); env \<in> list(A); p \<in> formula |]
     ==> Collect(A, is_DPow_sats(M,A,env,p)) = 
         {x \<in> A. sats(A, p, Cons(x,env))}"
 by (simp add: DPow_sats_abs transM [of _ A])
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_DPow_sats\<close>, Internalized\<close>
 
 (* is_DPow_sats(M,A,env,p,x) ==
       \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
              is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
              fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1) *)
 
 definition
   DPow_sats_fm :: "[i,i,i,i]=>i" where
   "DPow_sats_fm(A,env,p,x) ==
    Forall(Forall(Forall(
      Implies(satisfies_fm(A#+3,p#+3,0), 
        Implies(Cons_fm(x#+3,env#+3,1), 
          Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
 
 lemma is_DPow_sats_type [TC]:
      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
       ==> DPow_sats_fm(A,x,y,z) \<in> formula"
 by (simp add: DPow_sats_fm_def)
 
 lemma sats_DPow_sats_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, DPow_sats_fm(u,x,y,z), env) \<longleftrightarrow>
         is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: DPow_sats_fm_def is_DPow_sats_def)
 
 lemma DPow_sats_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    ==> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow>
        sats(A, DPow_sats_fm(u,x,y,z), env)"
 by simp
 
 theorem DPow_sats_reflection:
      "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold is_DPow_sats_def) 
 apply (intro FOL_reflections function_reflections extra_reflections
              satisfies_reflection)
 done
 
 
 subsection\<open>A Locale for Relativizing the Operator \<^term>\<open>DPow'\<close>\<close>
 
 locale M_DPow = M_satisfies +
  assumes sep:
    "[| M(A); env \<in> list(A); p \<in> formula |]
     ==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
  and rep: 
     "M(A)
     ==> strong_replacement (M, 
          \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
                   pair(M,env,p,ep) & 
                   is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))"
 
 lemma (in M_DPow) sep':
    "[| M(A); env \<in> list(A); p \<in> formula |]
     ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
 by (insert sep [of A env p], simp add: DPow_sats_abs)
 
 lemma (in M_DPow) rep':
    "M(A)
     ==> strong_replacement (M, 
          \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
                   ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
 by (insert rep [of A], simp add: Collect_DPow_sats_abs) 
 
 
 lemma univalent_pair_eq:
      "univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))"
 by (simp add: univalent_def, blast) 
 
 lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))"
 apply (simp add: DPow'_eq)
 apply (fast intro: rep' sep' univalent_pair_eq)  
 done
 
 text\<open>Relativization of the Operator \<^term>\<open>DPow'\<close>\<close>
 definition 
   is_DPow' :: "[i=>o,i,i] => o" where
     "is_DPow'(M,A,Z) == 
        \<forall>X[M]. X \<in> Z \<longleftrightarrow> 
          subset(M,X,A) & 
            (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
                     is_Collect(M, A, is_DPow_sats(M,A,env,p), X))"
 
 lemma (in M_DPow) DPow'_abs:
     "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) \<longleftrightarrow> Z = DPow'(A)"
 apply (rule iffI)
  prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) 
 apply (rule M_equalityI) 
 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption)
 apply (erule DPow'_closed)
 done
 
 
 subsection\<open>Instantiating the Locale \<open>M_DPow\<close>\<close>
 
 subsubsection\<open>The Instance of Separation\<close>
 
 lemma DPow_separation:
     "[| L(A); env \<in> list(A); p \<in> formula |]
      ==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
 apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], 
        auto intro: transL)
 apply (rule_tac env="[A,env,p]" in DPow_LsetI)
 apply (rule DPow_sats_iff_sats sep_rules | simp)+
 done
 
 
 
 subsubsection\<open>The Instance of Replacement\<close>
 
 lemma DPow_replacement_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
              (\<exists>env[L]. \<exists>p[L].
                mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) &
                is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
              (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
                mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) & 
                pair(##Lset(i),env,p,u) &
                is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
 apply (unfold is_Collect_def) 
 apply (intro FOL_reflections function_reflections mem_formula_reflection
           mem_list_reflection DPow_sats_reflection)
 done
 
 lemma DPow_replacement:
     "L(A)
     ==> strong_replacement (L, 
          \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
                   pair(L,env,p,ep) & 
                   is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B}" 
          in gen_separation_multi [OF DPow_replacement_Reflects], 
        auto)
 apply (unfold is_Collect_def) 
 apply (rule_tac env="[A,B]" in DPow_LsetI)
 apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
             DPow_sats_iff_sats | simp)+
 done
 
 
 subsubsection\<open>Actually Instantiating the Locale\<close>
 
 lemma M_DPow_axioms_L: "M_DPow_axioms(L)"
   apply (rule M_DPow_axioms.intro)
    apply (assumption | rule DPow_separation DPow_replacement)+
   done
 
 theorem M_DPow_L: "M_DPow(L)"
   apply (rule M_DPow.intro)
    apply (rule M_satisfies_L)
   apply (rule M_DPow_axioms_L)
   done
 
 lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
   and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_Collect\<close>\<close>
 
 text\<open>The formula \<^term>\<open>is_P\<close> has one free variable, 0, and it is
 enclosed within a single quantifier.\<close>
 
 (* is_Collect :: "[i=>o,i,i=>o,i] => o"
     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *)
 
 definition
   Collect_fm :: "[i, i, i]=>i" where
  "Collect_fm(A,is_P,z) == 
         Forall(Iff(Member(0,succ(z)),
                    And(Member(0,succ(A)), is_P)))"
 
 lemma is_Collect_type [TC]:
      "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
       ==> Collect_fm(x,is_P,y) \<in> formula"
 by (simp add: Collect_fm_def)
 
 lemma sats_Collect_fm:
   assumes is_P_iff_sats: 
       "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
   shows 
       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
        ==> sats(A, Collect_fm(x,p,y), env) \<longleftrightarrow>
            is_Collect(##A, nth(x,env), is_P, nth(y,env))"
 by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
 
 lemma Collect_iff_sats:
   assumes is_P_iff_sats: 
       "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
   shows 
   "[| nth(i,env) = x; nth(j,env) = y;
       i \<in> nat; j \<in> nat; env \<in> list(A)|]
    ==> is_Collect(##A, x, is_P, y) \<longleftrightarrow> sats(A, Collect_fm(i,p,j), env)"
 by (simp add: sats_Collect_fm [OF is_P_iff_sats])
 
 
 text\<open>The second argument of \<^term>\<open>is_P\<close> gives it direct access to \<^term>\<open>x\<close>,
   which is essential for handling free variable references.\<close>
 theorem Collect_reflection:
   assumes is_P_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
                      \<lambda>i x. is_P(##Lset(i), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
                \<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
 apply (simp (no_asm_use) only: is_Collect_def)
 apply (intro FOL_reflections is_P_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_Replace\<close>\<close>
 
 text\<open>BEWARE!  The formula \<^term>\<open>is_P\<close> has free variables 0, 1
  and not the usual 1, 0!  It is enclosed within two quantifiers.\<close>
 
 (*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
     "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *)
 
 definition
   Replace_fm :: "[i, i, i]=>i" where
   "Replace_fm(A,is_P,z) == 
         Forall(Iff(Member(0,succ(z)),
                    Exists(And(Member(0,A#+2), is_P))))"
 
 lemma is_Replace_type [TC]:
      "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
       ==> Replace_fm(x,is_P,y) \<in> formula"
 by (simp add: Replace_fm_def)
 
 lemma sats_Replace_fm:
   assumes is_P_iff_sats: 
       "!!a b. [|a \<in> A; b \<in> A|] 
               ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
   shows 
       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
        ==> sats(A, Replace_fm(x,p,y), env) \<longleftrightarrow>
            is_Replace(##A, nth(x,env), is_P, nth(y,env))"
 by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
 
 lemma Replace_iff_sats:
   assumes is_P_iff_sats: 
       "!!a b. [|a \<in> A; b \<in> A|] 
               ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
   shows 
   "[| nth(i,env) = x; nth(j,env) = y;
       i \<in> nat; j \<in> nat; env \<in> list(A)|]
    ==> is_Replace(##A, x, is_P, y) \<longleftrightarrow> sats(A, Replace_fm(i,p,j), env)"
 by (simp add: sats_Replace_fm [OF is_P_iff_sats])
 
 
 text\<open>The second argument of \<^term>\<open>is_P\<close> gives it direct access to \<^term>\<open>x\<close>,
   which is essential for handling free variable references.\<close>
 theorem Replace_reflection:
   assumes is_P_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
                      \<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
                \<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
 apply (simp (no_asm_use) only: is_Replace_def)
 apply (intro FOL_reflections is_P_reflection)
 done
 
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_DPow'\<close>, Internalized\<close>
 
 (*  "is_DPow'(M,A,Z) == 
        \<forall>X[M]. X \<in> Z \<longleftrightarrow> 
          subset(M,X,A) & 
            (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
                     is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
 
 definition
   DPow'_fm :: "[i,i]=>i" where
     "DPow'_fm(A,Z) == 
       Forall(
        Iff(Member(0,succ(Z)),
         And(subset_fm(0,succ(A)),
          Exists(Exists(
           And(mem_formula_fm(0),
            And(mem_list_fm(A#+3,1),
             Collect_fm(A#+3, 
                        DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))"
 
 lemma is_DPow'_type [TC]:
      "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
 by (simp add: DPow'_fm_def)
 
 lemma sats_DPow'_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, DPow'_fm(x,y), env) \<longleftrightarrow>
         is_DPow'(##A, nth(x,env), nth(y,env))"
 by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
 
 lemma DPow'_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
 by (simp)
 
 theorem DPow'_reflection:
      "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
                \<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]"
 apply (simp only: is_DPow'_def)
 apply (intro FOL_reflections function_reflections mem_formula_reflection
              mem_list_reflection Collect_reflection DPow_sats_reflection)
 done
 
 
 subsection\<open>A Locale for Relativizing the Operator \<^term>\<open>Lset\<close>\<close>
 
 definition
   transrec_body :: "[i=>o,i,i,i,i] => o" where
     "transrec_body(M,g,x) ==
       \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
 
 lemma (in M_DPow) transrec_body_abs:
      "[|M(x); M(g); M(z)|]
     ==> transrec_body(M,g,x,y,z) \<longleftrightarrow> y \<in> x & z = DPow'(g`y)"
 by (simp add: transrec_body_def DPow'_abs transM [of _ x])
 
 locale M_Lset = M_DPow +
  assumes strong_rep:
    "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
  and transrec_rep: 
     "M(i) ==> transrec_replacement(M, \<lambda>x f u. 
               \<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 
                      big_union(M, r, u), i)"
 
 
 lemma (in M_Lset) strong_rep':
    "[|M(x); M(g)|]
     ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
 by (insert strong_rep [of x g], simp add: transrec_body_abs)
 
 lemma (in M_Lset) DPow_apply_closed:
    "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
 by (blast intro: DPow'_closed dest: transM) 
 
 lemma (in M_Lset) RepFun_DPow_apply_closed:
    "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
 by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 
 
 lemma (in M_Lset) RepFun_DPow_abs:
      "[|M(x); M(f); M(r) |]
       ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) \<longleftrightarrow>
           r =  {DPow'(f`y). y\<in>x}"
 apply (simp add: transrec_body_abs RepFun_def) 
 apply (rule iff_trans) 
 apply (rule Replace_abs) 
 apply (simp_all add: DPow_apply_closed strong_rep') 
 done
 
 lemma (in M_Lset) transrec_rep':
    "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
 apply (insert transrec_rep [of i]) 
 apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 
        transrec_replacement_def) 
 done
 
 
 text\<open>Relativization of the Operator \<^term>\<open>Lset\<close>\<close>
 
 definition
   is_Lset :: "[i=>o, i, i] => o" where
    \<comment> \<open>We can use the term language below because \<^term>\<open>is_Lset\<close> will
        not have to be internalized: it isn't used in any instance of
        separation.\<close>
    "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
 
 lemma (in M_Lset) Lset_abs:
   "[|Ord(i);  M(i);  M(z)|] 
    ==> is_Lset(M,i,z) \<longleftrightarrow> z = Lset(i)"
 apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
 apply (rule transrec_abs)  
 apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed)
 done
 
 lemma (in M_Lset) Lset_closed:
   "[|Ord(i);  M(i)|] ==> M(Lset(i))"
 apply (simp add: Lset_eq_transrec_DPow') 
 apply (rule transrec_closed [OF transrec_rep']) 
 apply (simp_all add: relation2_def RepFun_DPow_apply_closed)
 done
 
 
 subsection\<open>Instantiating the Locale \<open>M_Lset\<close>\<close>
 
 subsubsection\<open>The First Instance of Replacement\<close>
 
 lemma strong_rep_Reflects:
  "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
                           v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
             v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]"
 by (intro FOL_reflections function_reflections DPow'_reflection)
 
 lemma strong_rep:
    "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
 apply (unfold transrec_body_def)  
 apply (rule strong_replacementI) 
 apply (rule_tac u="{x,g,B}" 
          in gen_separation_multi [OF strong_rep_Reflects], auto)
 apply (rule_tac env="[x,g,B]" in DPow_LsetI)
 apply (rule sep_rules DPow'_iff_sats | simp)+
 done
 
 
 subsubsection\<open>The Second Instance of Replacement\<close>
 
 lemma transrec_rep_Reflects:
  "REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B &
               (\<exists>y[L]. pair(L,v,y,x) &
              is_wfrec (L, \<lambda>x f u. \<exists>r[L].
                 is_Replace (L, x, \<lambda>y z. 
                      \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
                       is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
     \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
               (\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) &
              is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
                 is_Replace (##Lset(i), x, \<lambda>y z. 
                      \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & 
                       is_DPow'(##Lset(i),gy,z), r) & 
                       big_union(##Lset(i),r,u), mr, v, y))]" 
 apply (simp only: rex_setclass_is_bex [symmetric])
   \<comment> \<open>Convert \<open>\<exists>y\<in>Lset(i)\<close> to \<open>\<exists>y[##Lset(i)]\<close> within the body
        of the \<^term>\<open>is_wfrec\<close> application.\<close>
 apply (intro FOL_reflections function_reflections 
           is_wfrec_reflection Replace_reflection DPow'_reflection) 
 done
 
 
 lemma transrec_rep: 
     "[|L(j)|]
     ==> transrec_replacement(L, \<lambda>x f u. 
               \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
                      big_union(L, r, u), j)"
-apply (rule transrec_replacementI, assumption)
+apply (rule L.transrec_replacementI, assumption)
 apply (unfold transrec_body_def)  
 apply (rule strong_replacementI)
 apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
          in gen_separation_multi [OF transrec_rep_Reflects], auto)
 apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI)
 apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
        simp)+
 done
 
 
 subsubsection\<open>Actually Instantiating \<open>M_Lset\<close>\<close>
 
 lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
   apply (rule M_Lset_axioms.intro)
        apply (assumption | rule strong_rep transrec_rep)+
   done
 
 theorem M_Lset_L: "M_Lset(L)"
   apply (rule M_Lset.intro) 
    apply (rule M_DPow_L)
   apply (rule M_Lset_axioms_L) 
   done
 
 text\<open>Finally: the point of the whole theory!\<close>
 lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
    and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L]
 
 
 subsection\<open>The Notion of Constructible Set\<close>
 
 definition
   constructible :: "[i=>o,i] => o" where
     "constructible(M,x) ==
        \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
 
 theorem V_equals_L_in_L:
   "L(x) \<longleftrightarrow> constructible(L,x)"
 apply (simp add: constructible_def Lset_abs Lset_closed)
 apply (simp add: L_def)
 apply (blast intro: Ord_in_L) 
 done
 
 end
diff --git a/src/ZF/Constructible/L_axioms.thy b/src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy
+++ b/src/ZF/Constructible/L_axioms.thy
@@ -1,1403 +1,1403 @@
 (*  Title:      ZF/Constructible/L_axioms.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section \<open>The ZF Axioms (Except Separation) in L\<close>
 
 theory L_axioms imports Formula Relative Reflection MetaExists begin
 
 text \<open>The class L satisfies the premises of locale \<open>M_trivial\<close>\<close>
 
 lemma transL: "[| y\<in>x; 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="\<Union>(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 \<in> Pow(x). L(y)}" in rexI)
 apply (simp_all add: LPow_in_L, auto)
 apply (blast intro: transL)
 done
 
 text\<open>We don't actually need \<^term>\<open>L\<close> to satisfy the foundation axiom.\<close>
 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\<open>For L to satisfy Replacement\<close>
 
 (*Can't move these to Formula unless the definition of univalent is moved
 there too!*)
 
 lemma LReplace_in_Lset:
      "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|]
       ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
 apply (rule_tac x="\<Union>y \<in> 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)|]
       ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> 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]:
     "[| \<forall>B[L]. separation(L, %u. \<exists>x[L]. x\<in>B & 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\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
 text\<open>No instances of Separation yet.\<close>
 
 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)
+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\<open>Instantiation of the locale \<open>reflection\<close>\<close>
 
 text\<open>instances of locale constants\<close>
 
 definition
   L_F0 :: "[i=>o,i] => i" where
     "L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) \<longrightarrow> (\<exists>z\<in>Lset(b). P(<y,z>))"
 
 definition
   L_FF :: "[i=>o,i] => i" where
     "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
 
 definition
   L_ClEx :: "[i=>o,i] => o" where
     "L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"
 
 
 text\<open>We must use the meta-existential quantifier; otherwise the reflection
       terms become enormous!\<close>
 definition
   L_Reflects :: "[i=>o,[i,i]=>o] => prop"  (\<open>(3REFLECTS/ [_,/ _])\<close>) where
     "REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
                            (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
 
 
 theorem Triv_reflection:
      "REFLECTS[P, \<lambda>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[\<lambda>x. ~P(x), \<lambda>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[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
 apply (unfold L_Reflects_def)
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
 done
 
 theorem Or_reflection:
      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
       ==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
 apply (unfold L_Reflects_def)
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
 done
 
 theorem Imp_reflection:
      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
       ==> REFLECTS[\<lambda>x. P(x) \<longrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x)]"
 apply (unfold L_Reflects_def)
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
 done
 
 theorem Iff_reflection:
      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
       ==> REFLECTS[\<lambda>x. P(x) \<longleftrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x)]"
 apply (unfold L_Reflects_def)
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> 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[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(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[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<forall>z. L(z) \<longrightarrow> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(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[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
 apply (unfold rex_def)
 apply (intro And_reflection Ex_reflection, assumption)
 done
 
 theorem Rall_reflection:
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
 apply (unfold rall_def)
 apply (intro Imp_reflection All_reflection, assumption)
 done
 
 text\<open>This version handles an alternative form of the bounded quantifier
       in the second argument of \<open>REFLECTS\<close>.\<close>
 theorem Rex_reflection':
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
 apply (unfold setclass_def rex_def)
 apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
 done
 
 text\<open>As above.\<close>
 theorem Rall_reflection':
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>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)|]
       ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> 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;  \<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> Q(j,x)|] ==> R |]
       ==> R"
 by (drule ReflectsD, assumption, blast)
 
 lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B"
 by blast
 
 
 subsection\<open>Internalized Formulas for some Set-Theoretic Concepts\<close>
 
 subsubsection\<open>Some numbers to help write de Bruijn indices\<close>
 
 abbreviation
   digit3 :: i   (\<open>3\<close>) where "3 == succ(2)"
 
 abbreviation
   digit4 :: i   (\<open>4\<close>) where "4 == succ(3)"
 
 abbreviation
   digit5 :: i   (\<open>5\<close>) where "5 == succ(4)"
 
 abbreviation
   digit6 :: i   (\<open>6\<close>) where "6 == succ(5)"
 
 abbreviation
   digit7 :: i   (\<open>7\<close>) where "7 == succ(6)"
 
 abbreviation
   digit8 :: i   (\<open>8\<close>) where "8 == succ(7)"
 
 abbreviation
   digit9 :: i   (\<open>9\<close>) where "9 == succ(8)"
 
 
 subsubsection\<open>The Empty Set, Internalized\<close>
 
 definition
   empty_fm :: "i=>i" where
     "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
 
 lemma empty_type [TC]:
      "x \<in> nat ==> empty_fm(x) \<in> formula"
 by (simp add: empty_fm_def)
 
 lemma sats_empty_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, empty_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> empty(##A, x) \<longleftrightarrow> sats(A, empty_fm(i), env)"
 by simp
 
 theorem empty_reflection:
      "REFLECTS[\<lambda>x. empty(L,f(x)),
                \<lambda>i x. empty(##Lset(i),f(x))]"
 apply (simp only: empty_def)
 apply (intro FOL_reflections)
 done
 
 text\<open>Not used.  But maybe useful?\<close>
 lemma Transset_sats_empty_fm_eq_0:
    "[| n \<in> nat; env \<in> list(A); Transset(A)|]
     ==> sats(A, empty_fm(n), env) \<longleftrightarrow> 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\<open>Unordered Pairs, Internalized\<close>
 
 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
 by (simp add: upair_fm_def)
 
 lemma sats_upair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, upair_fm(x,y,z), env) \<longleftrightarrow>
             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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> upair(##A, x, y, z) \<longleftrightarrow> sats(A, upair_fm(i,j,k), env)"
 by (simp)
 
 text\<open>Useful? At least it refers to "real" unordered pairs\<close>
 lemma sats_upair_fm2 [simp]:
    "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|]
     ==> sats(A, upair_fm(x,y,z), env) \<longleftrightarrow>
         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[\<lambda>x. upair(L,f(x),g(x),h(x)),
                \<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]"
 apply (simp add: upair_def)
 apply (intro FOL_reflections)
 done
 
 subsubsection\<open>Ordered pairs, Internalized\<close>
 
 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
 by (simp add: pair_fm_def)
 
 lemma sats_pair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pair_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> pair(##A, x, y, z) \<longleftrightarrow> sats(A, pair_fm(i,j,k), env)"
 by (simp)
 
 theorem pair_reflection:
      "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
                \<lambda>i x. pair(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: pair_def)
 apply (intro FOL_reflections upair_reflection)
 done
 
 
 subsubsection\<open>Binary Unions, Internalized\<close>
 
 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
 by (simp add: union_fm_def)
 
 lemma sats_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, union_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> union(##A, x, y, z) \<longleftrightarrow> sats(A, union_fm(i,j,k), env)"
 by (simp)
 
 theorem union_reflection:
      "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
                \<lambda>i x. union(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: union_def)
 apply (intro FOL_reflections)
 done
 
 
 subsubsection\<open>Set ``Cons,'' Internalized\<close>
 
 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
 by (simp add: cons_fm_def)
 
 lemma sats_cons_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, cons_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_cons(##A, x, y, z) \<longleftrightarrow> sats(A, cons_fm(i,j,k), env)"
 by simp
 
 theorem cons_reflection:
      "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Successor Function, Internalized\<close>
 
 definition
   succ_fm :: "[i,i]=>i" where
     "succ_fm(x,y) == cons_fm(x,x,y)"
 
 lemma succ_type [TC]:
      "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
 by (simp add: succ_fm_def)
 
 lemma sats_succ_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, succ_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> successor(##A, x, y) \<longleftrightarrow> sats(A, succ_fm(i,j), env)"
 by simp
 
 theorem successor_reflection:
      "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
                \<lambda>i x. successor(##Lset(i),f(x),g(x))]"
 apply (simp only: successor_def)
 apply (intro cons_reflection)
 done
 
 
 subsubsection\<open>The Number 1, Internalized\<close>
 
 (* "number1(M,a) == (\<exists>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 \<in> nat ==> number1_fm(x) \<in> formula"
 by (simp add: number1_fm_def)
 
 lemma sats_number1_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, number1_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> number1(##A, x) \<longleftrightarrow> sats(A, number1_fm(i), env)"
 by simp
 
 theorem number1_reflection:
      "REFLECTS[\<lambda>x. number1(L,f(x)),
                \<lambda>i x. number1(##Lset(i),f(x))]"
 apply (simp only: number1_def)
 apply (intro FOL_reflections empty_reflection successor_reflection)
 done
 
 
 subsubsection\<open>Big Union, Internalized\<close>
 
 (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A & x \<in> 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 \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
 by (simp add: big_union_fm_def)
 
 lemma sats_big_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, big_union_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> big_union(##A, x, y) \<longleftrightarrow> sats(A, big_union_fm(i,j), env)"
 by simp
 
 theorem big_union_reflection:
      "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
                \<lambda>i x. big_union(##Lset(i),f(x),g(x))]"
 apply (simp only: big_union_def)
 apply (intro FOL_reflections)
 done
 
 
 subsubsection\<open>Variants of Satisfaction Definitions for Ordinals, etc.\<close>
 
 text\<open>The \<open>sats\<close> theorems below are standard versions of the ones proved
 in theory \<open>Formula\<close>.  They relate elements of type \<^term>\<open>formula\<close> to
 relativized concepts such as \<^term>\<open>subset\<close> or \<^term>\<open>ordinal\<close> rather than to
 real concepts such as \<^term>\<open>Ord\<close>.  Now that we have instantiated the locale
 \<open>M_trivial\<close>, we no longer require the earlier versions.\<close>
 
 lemma sats_subset_fm':
    "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, subset_fm(x,y), env) \<longleftrightarrow> subset(##A, nth(x,env), nth(y,env))"
 by (simp add: subset_fm_def Relative.subset_def)
 
 theorem subset_reflection:
      "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
                \<lambda>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 \<in> nat; env \<in> list(A)|]
     ==> sats(A, transset_fm(x), env) \<longleftrightarrow> transitive_set(##A, nth(x,env))"
 by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
 
 theorem transitive_set_reflection:
      "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
                \<lambda>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 \<in> nat; env \<in> list(A)|]
     ==> sats(A, ordinal_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> ordinal(##A, x) \<longleftrightarrow> sats(A, ordinal_fm(i), env)"
 by (simp add: sats_ordinal_fm')
 
 theorem ordinal_reflection:
      "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(##Lset(i),f(x))]"
 apply (simp only: ordinal_def)
 apply (intro FOL_reflections transitive_set_reflection)
 done
 
 
 subsubsection\<open>Membership Relation, Internalized\<close>
 
 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 \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
 by (simp add: Memrel_fm_def)
 
 lemma sats_Memrel_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, Memrel_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> membership(##A, x, y) \<longleftrightarrow> sats(A, Memrel_fm(i,j), env)"
 by simp
 
 theorem membership_reflection:
      "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
                \<lambda>i x. membership(##Lset(i),f(x),g(x))]"
 apply (simp only: membership_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 subsubsection\<open>Predecessor Set, Internalized\<close>
 
 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 \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
       ==> pred_set_fm(A,x,r,B) \<in> formula"
 by (simp add: pred_set_fm_def)
 
 lemma sats_pred_set_fm [simp]:
    "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
     ==> sats(A, pred_set_fm(U,x,r,B), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
        ==> pred_set(##A,U,x,r,B) \<longleftrightarrow> sats(A, pred_set_fm(i,j,k,l), env)"
 by (simp)
 
 theorem pred_set_reflection:
      "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
                \<lambda>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\<open>Domain of a Relation, Internalized\<close>
 
 (* "is_domain(M,r,z) ==
         \<forall>x[M]. (x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>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 \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
 by (simp add: domain_fm_def)
 
 lemma sats_domain_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, domain_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_domain(##A, x, y) \<longleftrightarrow> sats(A, domain_fm(i,j), env)"
 by simp
 
 theorem domain_reflection:
      "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
                \<lambda>i x. is_domain(##Lset(i),f(x),g(x))]"
 apply (simp only: is_domain_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
 subsubsection\<open>Range of a Relation, Internalized\<close>
 
 (* "is_range(M,r,z) ==
         \<forall>y[M]. (y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>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 \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
 by (simp add: range_fm_def)
 
 lemma sats_range_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, range_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_range(##A, x, y) \<longleftrightarrow> sats(A, range_fm(i,j), env)"
 by simp
 
 theorem range_reflection:
      "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
                \<lambda>i x. is_range(##Lset(i),f(x),g(x))]"
 apply (simp only: is_range_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
 subsubsection\<open>Field of a Relation, Internalized\<close>
 
 (* "is_field(M,r,z) ==
         \<exists>dr[M]. is_domain(M,r,dr) &
             (\<exists>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 \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
 by (simp add: field_fm_def)
 
 lemma sats_field_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, field_fm(x,y), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_field(##A, x, y) \<longleftrightarrow> sats(A, field_fm(i,j), env)"
 by simp
 
 theorem field_reflection:
      "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
                \<lambda>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\<open>Image under a Relation, Internalized\<close>
 
 (* "image(M,r,A,z) ==
         \<forall>y[M]. (y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
 by (simp add: image_fm_def)
 
 lemma sats_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, image_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> image(##A, x, y, z) \<longleftrightarrow> sats(A, image_fm(i,j,k), env)"
 by (simp)
 
 theorem image_reflection:
      "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Pre-Image under a Relation, Internalized\<close>
 
 (* "pre_image(M,r,A,z) ==
         \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
 by (simp add: pre_image_fm_def)
 
 lemma sats_pre_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pre_image_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> pre_image(##A, x, y, z) \<longleftrightarrow> sats(A, pre_image_fm(i,j,k), env)"
 by (simp)
 
 theorem pre_image_reflection:
      "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Function Application, Internalized\<close>
 
 (* "fun_apply(M,f,x,y) ==
         (\<exists>xs[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
 by (simp add: fun_apply_fm_def)
 
 lemma sats_fun_apply_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, fun_apply_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> fun_apply(##A, x, y, z) \<longleftrightarrow> sats(A, fun_apply_fm(i,j,k), env)"
 by simp
 
 theorem fun_apply_reflection:
      "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
                \<lambda>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\<open>The Concept of Relation, Internalized\<close>
 
 (* "is_relation(M,r) ==
         (\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>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 \<in> nat |] ==> relation_fm(x) \<in> formula"
 by (simp add: relation_fm_def)
 
 lemma sats_relation_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, relation_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> is_relation(##A, x) \<longleftrightarrow> sats(A, relation_fm(i), env)"
 by simp
 
 theorem is_relation_reflection:
      "REFLECTS[\<lambda>x. is_relation(L,f(x)),
                \<lambda>i x. is_relation(##Lset(i),f(x))]"
 apply (simp only: is_relation_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
 subsubsection\<open>The Concept of Function, Internalized\<close>
 
 (* "is_function(M,r) ==
         \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
            pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> 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 \<in> nat |] ==> function_fm(x) \<in> formula"
 by (simp add: function_fm_def)
 
 lemma sats_function_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, function_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> is_function(##A, x) \<longleftrightarrow> sats(A, function_fm(i), env)"
 by simp
 
 theorem is_function_reflection:
      "REFLECTS[\<lambda>x. is_function(L,f(x)),
                \<lambda>i x. is_function(##Lset(i),f(x))]"
 apply (simp only: is_function_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
 subsubsection\<open>Typed Functions, Internalized\<close>
 
 (* "typed_function(M,A,B,r) ==
         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
         (\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
 by (simp add: typed_function_fm_def)
 
 lemma sats_typed_function_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, typed_function_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    ==> typed_function(##A, x, y, z) \<longleftrightarrow> 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[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Composition of Relations, Internalized\<close>
 
 (* "composition(M,r,s,t) ==
         \<forall>p[M]. p \<in> t \<longleftrightarrow>
                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
                 xy \<in> s & yz \<in> 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
 by (simp add: composition_fm_def)
 
 lemma sats_composition_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, composition_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> composition(##A, x, y, z) \<longleftrightarrow> sats(A, composition_fm(i,j,k), env)"
 by simp
 
 theorem composition_reflection:
      "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
                \<lambda>i x. composition(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: composition_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
 subsubsection\<open>Injections, Internalized\<close>
 
 (* "injection(M,A,B,f) ==
         typed_function(M,A,B,f) &
         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
           pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
 by (simp add: injection_fm_def)
 
 lemma sats_injection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, injection_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    ==> injection(##A, x, y, z) \<longleftrightarrow> sats(A, injection_fm(i,j,k), env)"
 by simp
 
 theorem injection_reflection:
      "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Surjections, Internalized\<close>
 
 (*  surjection :: "[i=>o,i,i,i] => o"
     "surjection(M,A,B,f) ==
         typed_function(M,A,B,f) &
         (\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
 by (simp add: surjection_fm_def)
 
 lemma sats_surjection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, surjection_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    ==> surjection(##A, x, y, z) \<longleftrightarrow> sats(A, surjection_fm(i,j,k), env)"
 by simp
 
 theorem surjection_reflection:
      "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Bijections, Internalized\<close>
 
 (*   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 \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
 by (simp add: bijection_fm_def)
 
 lemma sats_bijection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, bijection_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    ==> bijection(##A, x, y, z) \<longleftrightarrow> sats(A, bijection_fm(i,j,k), env)"
 by simp
 
 theorem bijection_reflection:
      "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
                \<lambda>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\<open>Restriction of a Relation, Internalized\<close>
 
 
 (* "restriction(M,r,A,z) ==
         \<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
 by (simp add: restriction_fm_def)
 
 lemma sats_restriction_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, restriction_fm(x,y,z), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> restriction(##A, x, y, z) \<longleftrightarrow> sats(A, restriction_fm(i,j,k), env)"
 by simp
 
 theorem restriction_reflection:
      "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
                \<lambda>i x. restriction(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: restriction_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 subsubsection\<open>Order-Isomorphisms, Internalized\<close>
 
 (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
    "order_isomorphism(M,A,r,B,s,f) ==
         bijection(M,A,B,f) &
         (\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow>
           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
             pair(M,x,y,p) \<longrightarrow> fun_apply(M,f,x,fx) \<longrightarrow> fun_apply(M,f,y,fy) \<longrightarrow>
             pair(M,fx,fy,q) \<longrightarrow> (p\<in>r \<longleftrightarrow> q\<in>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 \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
       ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
 by (simp add: order_isomorphism_fm_def)
 
 lemma sats_order_isomorphism_fm [simp]:
    "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
     ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) \<longleftrightarrow>
         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 \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
    ==> order_isomorphism(##A,U,r,B,s,f) \<longleftrightarrow>
        sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
 by simp
 
 theorem order_isomorphism_reflection:
      "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
                \<lambda>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\<open>Limit Ordinals, Internalized\<close>
 
 text\<open>A limit ordinal is a non-empty, successor-closed ordinal\<close>
 
 (* "limit_ordinal(M,a) ==
         ordinal(M,a) & ~ empty(M,a) &
         (\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>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 \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
 by (simp add: limit_ordinal_fm_def)
 
 lemma sats_limit_ordinal_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, limit_ordinal_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> limit_ordinal(##A, x) \<longleftrightarrow> sats(A, limit_ordinal_fm(i), env)"
 by simp
 
 theorem limit_ordinal_reflection:
      "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
                \<lambda>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\<open>Finite Ordinals: The Predicate ``Is A Natural Number''\<close>
 
 (*     "finite_ordinal(M,a) == 
         ordinal(M,a) & ~ limit_ordinal(M,a) & 
         (\<forall>x[M]. x\<in>a \<longrightarrow> ~ 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 \<in> nat ==> finite_ordinal_fm(x) \<in> formula"
 by (simp add: finite_ordinal_fm_def)
 
 lemma sats_finite_ordinal_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, finite_ordinal_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> finite_ordinal(##A, x) \<longleftrightarrow> sats(A, finite_ordinal_fm(i), env)"
 by simp
 
 theorem finite_ordinal_reflection:
      "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
                \<lambda>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\<open>Omega: The Set of Natural Numbers\<close>
 
 (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ 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 \<in> nat ==> omega_fm(x) \<in> formula"
 by (simp add: omega_fm_def)
 
 lemma sats_omega_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, omega_fm(x), env) \<longleftrightarrow> 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 \<in> nat; env \<in> list(A)|]
        ==> omega(##A, x) \<longleftrightarrow> sats(A, omega_fm(i), env)"
 by simp
 
 theorem omega_reflection:
      "REFLECTS[\<lambda>x. omega(L,f(x)),
                \<lambda>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
diff --git a/src/ZF/Constructible/Rec_Separation.thy b/src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy
+++ b/src/ZF/Constructible/Rec_Separation.thy
@@ -1,440 +1,440 @@
 (*  Title:      ZF/Constructible/Rec_Separation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section \<open>Separation for Facts About Recursion\<close>
 
 theory Rec_Separation imports Separation Internalize begin
 
 text\<open>This theory proves all instances needed for locales \<open>M_trancl\<close> and \<open>M_datatypes\<close>\<close>
 
 lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
 by simp
 
 
 subsection\<open>The Locale \<open>M_trancl\<close>\<close>
 
 subsubsection\<open>Separation for Reflexive/Transitive Closure\<close>
 
 text\<open>First, The Defining Formula\<close>
 
 (* "rtran_closure_mem(M,A,r,p) ==
       \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
        omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
        (\<exists>f[M]. typed_function(M,n',A,f) &
         (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
           fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
         (\<forall>j[M]. j\<in>n \<longrightarrow>
           (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
             fun_apply(M,f,j,fj) & successor(M,j,sj) &
             fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
 definition
   rtran_closure_mem_fm :: "[i,i,i]=>i" where
  "rtran_closure_mem_fm(A,r,p) ==
    Exists(Exists(Exists(
     And(omega_fm(2),
      And(Member(1,2),
       And(succ_fm(1,0),
        Exists(And(typed_function_fm(1, A#+4, 0),
         And(Exists(Exists(Exists(
               And(pair_fm(2,1,p#+7),
                And(empty_fm(0),
                 And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
             Forall(Implies(Member(0,3),
              Exists(Exists(Exists(Exists(
               And(fun_apply_fm(5,4,3),
                And(succ_fm(4,2),
                 And(fun_apply_fm(5,2,1),
                  And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
 
 
 lemma rtran_closure_mem_type [TC]:
  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
 by (simp add: rtran_closure_mem_fm_def)
 
 lemma sats_rtran_closure_mem_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_mem_fm(x,y,z), env) \<longleftrightarrow>
         rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
 
 lemma rtran_closure_mem_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)"
 by (simp)
 
 lemma rtran_closure_mem_reflection:
      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
                \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: rtran_closure_mem_def)
 apply (intro FOL_reflections function_reflections fun_plus_reflections)
 done
 
 text\<open>Separation for \<^term>\<open>rtrancl(r)\<close>.\<close>
 lemma rtrancl_separation:
      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
 apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"],
        auto)
 apply (rule_tac env="[r,A]" in DPow_LsetI)
 apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+
 done
 
 
 subsubsection\<open>Reflexive/Transitive Closure, Internalized\<close>
 
 (*  "rtran_closure(M,r,s) ==
         \<forall>A[M]. is_field(M,r,A) \<longrightarrow>
          (\<forall>p[M]. p \<in> s \<longleftrightarrow> rtran_closure_mem(M,A,r,p))" *)
 definition
   rtran_closure_fm :: "[i,i]=>i" where
   "rtran_closure_fm(r,s) ==
    Forall(Implies(field_fm(succ(r),0),
                   Forall(Iff(Member(0,succ(succ(s))),
                              rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
 
 lemma rtran_closure_type [TC]:
      "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
 by (simp add: rtran_closure_fm_def)
 
 lemma sats_rtran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_fm(x,y), env) \<longleftrightarrow>
         rtran_closure(##A, nth(x,env), nth(y,env))"
 by (simp add: rtran_closure_fm_def rtran_closure_def)
 
 lemma rtran_closure_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> rtran_closure(##A, x, y) \<longleftrightarrow> sats(A, rtran_closure_fm(i,j), env)"
 by simp
 
 theorem rtran_closure_reflection:
      "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
                \<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]"
 apply (simp only: rtran_closure_def)
 apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
 done
 
 
 subsubsection\<open>Transitive Closure of a Relation, Internalized\<close>
 
 (*  "tran_closure(M,r,t) ==
          \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
 definition
   tran_closure_fm :: "[i,i]=>i" where
   "tran_closure_fm(r,s) ==
    Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
 
 lemma tran_closure_type [TC]:
      "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
 by (simp add: tran_closure_fm_def)
 
 lemma sats_tran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, tran_closure_fm(x,y), env) \<longleftrightarrow>
         tran_closure(##A, nth(x,env), nth(y,env))"
 by (simp add: tran_closure_fm_def tran_closure_def)
 
 lemma tran_closure_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> tran_closure(##A, x, y) \<longleftrightarrow> sats(A, tran_closure_fm(i,j), env)"
 by simp
 
 theorem tran_closure_reflection:
      "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
                \<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]"
 apply (simp only: tran_closure_def)
 apply (intro FOL_reflections function_reflections
              rtran_closure_reflection composition_reflection)
 done
 
 
 subsubsection\<open>Separation for the Proof of \<open>wellfounded_on_trancl\<close>\<close>
 
 lemma wellfounded_trancl_reflects:
   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                  w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
        w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) &
        wx \<in> rp]"
 by (intro FOL_reflections function_reflections fun_plus_reflections
           tran_closure_reflection)
 
 lemma wellfounded_trancl_separation:
          "[| L(r); L(Z) |] ==>
           separation (L, \<lambda>x.
               \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
 apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"],
        auto)
 apply (rule_tac env="[r,Z]" in DPow_LsetI)
 apply (rule sep_rules tran_closure_iff_sats | simp)+
 done
 
 
 subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close>
 
 lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   apply (rule M_trancl_axioms.intro)
    apply (assumption | rule rtrancl_separation wellfounded_trancl_separation L_nat)+
   done
 
 theorem M_trancl_L: "M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
-interpretation L?: M_trancl L by (rule M_trancl_L)
+interpretation L: M_trancl L by (rule M_trancl_L)
 
 
 subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>list\<close>\<close>
 
 subsubsection\<open>Instances of Replacement for Lists\<close>
 
 lemma list_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
          is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
          is_wfrec(##Lset(i),
                   iterates_MH(##Lset(i),
                           is_list_functor(##Lset(i), A), 0), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection list_functor_reflection)
 
 
 lemma list_replacement1:
    "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF list_replacement1_Reflects], 
        auto)
 apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 
 
 lemma list_replacement2_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, is_list_functor(L, A), 0, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
                is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]"
 by (intro FOL_reflections 
           is_iterates_reflection list_functor_reflection)
 
 lemma list_replacement2:
    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,0,nat}" 
          in gen_separation_multi [OF list_replacement2_Reflects], 
        auto)
 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
 
 subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>formula\<close>\<close>
 
 subsubsection\<open>Instances of Replacement for Formulas\<close>
 
 (*FIXME: could prove a lemma iterates_replacementI to eliminate the 
 need to expand iterates_replacement and wfrec_replacement*)
 lemma formula_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
          is_wfrec(##Lset(i),
                   iterates_MH(##Lset(i),
                           is_formula_functor(##Lset(i)), 0), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection formula_functor_reflection)
 
 lemma formula_replacement1:
    "iterates_replacement(L, is_formula_functor(L), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF formula_replacement1_Reflects], 
        auto)
 apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 
 lemma formula_replacement2_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, is_formula_functor(L), 0, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
                is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]"
 by (intro FOL_reflections 
           is_iterates_reflection formula_functor_reflection)
 
 lemma formula_replacement2:
    "strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,0,nat}" 
          in gen_separation_multi [OF formula_replacement2_Reflects], 
        auto)
 apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
 text\<open>NB The proofs for type \<^term>\<open>formula\<close> are virtually identical to those
 for \<^term>\<open>list(A)\<close>.  It was a cut-and-paste job!\<close>
 
 
 subsubsection\<open>The Formula \<^term>\<open>is_nth\<close>, Internalized\<close>
 
 (* "is_nth(M,n,l,Z) ==
       \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
 definition
   nth_fm :: "[i,i,i]=>i" where
     "nth_fm(n,l,Z) == 
        Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), 
               hd_fm(0,succ(Z))))"
 
 lemma nth_fm_type [TC]:
  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula"
 by (simp add: nth_fm_def)
 
 lemma sats_nth_fm [simp]:
    "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, nth_fm(x,y,z), env) \<longleftrightarrow>
         is_nth(##A, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) 
 done
 
 lemma nth_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)"
 by (simp)
 
 theorem nth_reflection:
      "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
                \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]"
 apply (simp only: is_nth_def)
 apply (intro FOL_reflections is_iterates_reflection
              hd_reflection tl_reflection) 
 done
 
 
 subsubsection\<open>An Instance of Replacement for \<^term>\<open>nth\<close>\<close>
 
 (*FIXME: could prove a lemma iterates_replacementI to eliminate the 
 need to expand iterates_replacement and wfrec_replacement*)
 lemma nth_replacement_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
          is_wfrec(##Lset(i),
                   iterates_MH(##Lset(i),
                           is_tl(##Lset(i)), z), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection tl_reflection)
 
 lemma nth_replacement:
    "L(w) ==> iterates_replacement(L, is_tl(L), w)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,w,Memrel(succ(n))}" 
          in gen_separation_multi [OF nth_replacement_Reflects], 
        auto)
 apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 
 
 subsubsection\<open>Instantiating the locale \<open>M_datatypes\<close>\<close>
 
 lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
   apply (rule M_datatypes_axioms.intro)
       apply (assumption | rule
         list_replacement1 list_replacement2
         formula_replacement1 formula_replacement2
         nth_replacement)+
   done
 
 theorem M_datatypes_L: "M_datatypes(L)"
   apply (rule M_datatypes.intro)
    apply (rule M_trancl_L)
   apply (rule M_datatypes_axioms_L) 
   done
 
-interpretation L?: M_datatypes L by (rule M_datatypes_L)
+interpretation L: M_datatypes L by (rule M_datatypes_L)
 
 
 subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>eclose\<close>\<close>
 
 subsubsection\<open>Instances of Replacement for \<^term>\<open>eclose\<close>\<close>
 
 lemma eclose_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
          is_wfrec(##Lset(i),
                   iterates_MH(##Lset(i), big_union(##Lset(i)), A),
                   memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection)
 
 lemma eclose_replacement1:
    "L(A) ==> iterates_replacement(L, big_union(L), A)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
          in gen_separation_multi [OF eclose_replacement1_Reflects], auto)
 apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
              is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
 done
 
 
 lemma eclose_replacement2_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, big_union(L), A, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
                is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]"
 by (intro FOL_reflections function_reflections is_iterates_reflection)
 
 lemma eclose_replacement2:
    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,nat}" 
          in gen_separation_multi [OF eclose_replacement2_Reflects],
        auto)
 apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
 done
 
 
 subsubsection\<open>Instantiating the locale \<open>M_eclose\<close>\<close>
 
 lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
   apply (rule M_eclose_axioms.intro)
    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done
 
 theorem M_eclose_L: "M_eclose(L)"
   apply (rule M_eclose.intro)
    apply (rule M_datatypes_L)
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation L?: M_eclose L by (rule M_eclose_L)
+interpretation L: M_eclose L by (rule M_eclose_L)
 
 
 end
diff --git a/src/ZF/Constructible/Satisfies_absolute.thy b/src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy
+++ b/src/ZF/Constructible/Satisfies_absolute.thy
@@ -1,1039 +1,1039 @@
 (*  Title:      ZF/Constructible/Satisfies_absolute.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section \<open>Absoluteness for the Satisfies Relation on Formulas\<close>
 
 theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 
 
 
 subsection \<open>More Internalization\<close>
 
 subsubsection\<open>The Formula \<^term>\<open>is_depth\<close>, Internalized\<close>
 
 (*    "is_depth(M,p,n) == 
        \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
          2          1                0
         is_formula_N(M,n,formula_n) & p \<notin> formula_n &
         successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
 definition
   depth_fm :: "[i,i]=>i" where
   "depth_fm(p,n) == 
      Exists(Exists(Exists(
        And(formula_N_fm(n#+3,1),
          And(Neg(Member(p#+3,1)),
           And(succ_fm(n#+3,2),
            And(formula_N_fm(2,0), Member(p#+3,0))))))))"
 
 lemma depth_fm_type [TC]:
  "[| x \<in> nat; y \<in> nat |] ==> depth_fm(x,y) \<in> formula"
 by (simp add: depth_fm_def)
 
 lemma sats_depth_fm [simp]:
    "[| x \<in> nat; y < length(env); env \<in> list(A)|]
     ==> sats(A, depth_fm(x,y), env) \<longleftrightarrow>
         is_depth(##A, nth(x,env), nth(y,env))"
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: depth_fm_def is_depth_def) 
 done
 
 lemma depth_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j < length(env); env \<in> list(A)|]
        ==> is_depth(##A, x, y) \<longleftrightarrow> sats(A, depth_fm(i,j), env)"
 by (simp)
 
 theorem depth_reflection:
      "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
                \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
 apply (simp only: is_depth_def)
 apply (intro FOL_reflections function_reflections formula_N_reflection) 
 done
 
 
 
 subsubsection\<open>The Operator \<^term>\<open>is_formula_case\<close>\<close>
 
 text\<open>The arguments of \<^term>\<open>is_a\<close> are always 2, 1, 0, and the formula
       will be enclosed by three quantifiers.\<close>
 
 (* is_formula_case :: 
     "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == 
       (\<forall>x[M]. \<forall>y[M]. x\<in>nat \<longrightarrow> y\<in>nat \<longrightarrow> is_Member(M,x,y,v) \<longrightarrow> is_a(x,y,z)) &
       (\<forall>x[M]. \<forall>y[M]. x\<in>nat \<longrightarrow> y\<in>nat \<longrightarrow> is_Equal(M,x,y,v) \<longrightarrow> is_b(x,y,z)) &
       (\<forall>x[M]. \<forall>y[M]. x\<in>formula \<longrightarrow> y\<in>formula \<longrightarrow> 
                      is_Nand(M,x,y,v) \<longrightarrow> is_c(x,y,z)) &
       (\<forall>x[M]. x\<in>formula \<longrightarrow> is_Forall(M,x,v) \<longrightarrow> is_d(x,z))" *)
 
 definition
   formula_case_fm :: "[i, i, i, i, i, i]=>i" where
   "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
         And(Forall(Forall(Implies(finite_ordinal_fm(1), 
                            Implies(finite_ordinal_fm(0), 
                             Implies(Member_fm(1,0,v#+2), 
                              Forall(Implies(Equal(0,z#+3), is_a))))))),
         And(Forall(Forall(Implies(finite_ordinal_fm(1), 
                            Implies(finite_ordinal_fm(0), 
                             Implies(Equal_fm(1,0,v#+2), 
                              Forall(Implies(Equal(0,z#+3), is_b))))))),
         And(Forall(Forall(Implies(mem_formula_fm(1), 
                            Implies(mem_formula_fm(0), 
                             Implies(Nand_fm(1,0,v#+2), 
                              Forall(Implies(Equal(0,z#+3), is_c))))))),
         Forall(Implies(mem_formula_fm(0), 
                        Implies(Forall_fm(0,succ(v)), 
                              Forall(Implies(Equal(0,z#+2), is_d))))))))"
 
 
 lemma is_formula_case_type [TC]:
      "[| is_a \<in> formula;  is_b \<in> formula;  is_c \<in> formula;  is_d \<in> formula;  
          x \<in> nat; y \<in> nat |] 
       ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula"
 by (simp add: formula_case_fm_def)
 
 lemma sats_formula_case_fm:
   assumes is_a_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_b_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_c_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_d_iff_sats: 
       "!!a0 a1. 
         [|a0\<in>A; a1\<in>A|]  
         ==> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   shows 
       "[|x \<in> nat; y < length(env); env \<in> list(A)|]
        ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) \<longleftrightarrow>
            is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: formula_case_fm_def is_formula_case_def 
                  is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
                  is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
 done
 
 lemma formula_case_iff_sats:
   assumes is_a_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_b_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_c_iff_sats: 
       "!!a0 a1 a2. 
         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
         ==> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   and is_d_iff_sats: 
       "!!a0 a1. 
         [|a0\<in>A; a1\<in>A|]  
         ==> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   shows 
       "[|nth(i,env) = x; nth(j,env) = y; 
       i \<in> nat; j < length(env); env \<in> list(A)|]
        ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) \<longleftrightarrow>
            sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
 by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 
                                        is_c_iff_sats is_d_iff_sats])
 
 
 text\<open>The second argument of \<^term>\<open>is_a\<close> gives it direct access to \<^term>\<open>x\<close>,
   which is essential for handling free variable references.  Treatment is
   based on that of \<open>is_nat_case_reflection\<close>.\<close>
 theorem is_formula_case_reflection:
   assumes is_a_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
                      \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_b_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
                      \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_c_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
                      \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_d_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
                      \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
                \<lambda>i x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_formula_case_def)
 apply (intro FOL_reflections function_reflections finite_ordinal_reflection
          mem_formula_reflection
          Member_reflection Equal_reflection Nand_reflection Forall_reflection
          is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
 done
 
 
 
 subsection \<open>Absoluteness for the Function \<^term>\<open>satisfies\<close>\<close>
 
 definition
   is_depth_apply :: "[i=>o,i,i,i] => o" where
    \<comment> \<open>Merely a useful abbreviation for the sequel.\<close>
   "is_depth_apply(M,h,p,z) ==
     \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
         finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
         fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"
 
 lemma (in M_datatypes) is_depth_apply_abs [simp]:
      "[|M(h); p \<in> formula; M(z)|] 
       ==> is_depth_apply(M,h,p,z) \<longleftrightarrow> z = h ` succ(depth(p)) ` p"
 by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)
 
 
 
 text\<open>There is at present some redundancy between the relativizations in
  e.g. \<open>satisfies_is_a\<close> and those in e.g. \<open>Member_replacement\<close>.\<close>
 
 text\<open>These constants let us instantiate the parameters \<^term>\<open>a\<close>, \<^term>\<open>b\<close>,
       \<^term>\<open>c\<close>, \<^term>\<open>d\<close>, etc., of the locale \<open>Formula_Rec\<close>.\<close>
 definition
   satisfies_a :: "[i,i,i]=>i" where
    "satisfies_a(A) == 
     \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
 
 definition
   satisfies_is_a :: "[i=>o,i,i,i,i]=>o" where
    "satisfies_is_a(M,A) == 
     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. is_bool_of_o(M, 
                       \<exists>nx[M]. \<exists>ny[M]. 
                        is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
                 zz)"
 
 definition
   satisfies_b :: "[i,i,i]=>i" where
    "satisfies_b(A) ==
     \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))"
 
 definition
   satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where
    \<comment> \<open>We simplify the formula to have just \<^term>\<open>nx\<close> rather than 
        introducing \<^term>\<open>ny\<close> with  \<^term>\<open>nx=ny\<close>\<close>
   "satisfies_is_b(M,A) == 
     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. is_bool_of_o(M, 
                       \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
                 zz)"
 
 definition 
   satisfies_c :: "[i,i,i,i,i]=>i" where
    "satisfies_c(A) == \<lambda>p q rp rq. \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
 
 definition
   satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o" where
    "satisfies_is_c(M,A,h) == 
     \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
                  (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
                  (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
                  (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
                 zz)"
 
 definition
   satisfies_d :: "[i,i,i]=>i" where
    "satisfies_d(A) 
     == \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)"
 
 definition
   satisfies_is_d :: "[i=>o,i,i,i,i]=>o" where
    "satisfies_is_d(M,A,h) == 
     \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
                     is_bool_of_o(M, 
                            \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
                               x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow> 
                               fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp),
                   z),
                zz)"
 
 definition
   satisfies_MH :: "[i=>o,i,i,i,i]=>o" where
     \<comment> \<open>The variable \<^term>\<open>u\<close> is unused, but gives \<^term>\<open>satisfies_MH\<close> 
         the correct arity.\<close>
   "satisfies_MH == 
     \<lambda>M A u f z. 
          \<forall>fml[M]. is_formula(M,fml) \<longrightarrow>
              is_lambda (M, fml, 
                is_formula_case (M, satisfies_is_a(M,A), 
                                 satisfies_is_b(M,A), 
                                 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
                z)"
 
 definition
   is_satisfies :: "[i=>o,i,i,i]=>o" where
   "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))"
 
 
 text\<open>This lemma relates the fragments defined above to the original primitive
       recursion in \<^term>\<open>satisfies\<close>.
       Induction is not required: the definitions are directly equal!\<close>
 lemma satisfies_eq:
   "satisfies(A,p) = 
    formula_rec (satisfies_a(A), satisfies_b(A), 
                 satisfies_c(A), satisfies_d(A), p)"
 by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def 
               satisfies_c_def satisfies_d_def) 
 
 text\<open>Further constraints on the class \<^term>\<open>M\<close> in order to prove
       absoluteness for the constants defined above.  The ultimate goal
       is the absoluteness of the function \<^term>\<open>satisfies\<close>.\<close>
 locale M_satisfies = M_eclose +
  assumes 
    Member_replacement:
     "[|M(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
               env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
               is_bool_of_o(M, nx \<in> ny, bo) &
               pair(M, env, bo, z))"
  and
    Equal_replacement:
     "[|M(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
               env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
               is_bool_of_o(M, nx = ny, bo) &
               pair(M, env, bo, z))"
  and
    Nand_replacement:
     "[|M(A); M(rp); M(rq)|]
      ==> strong_replacement
          (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. 
                fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & 
                is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & 
                env \<in> list(A) & pair(M, env, notpq, z))"
  and
   Forall_replacement:
    "[|M(A); M(rp)|]
     ==> strong_replacement
         (M, \<lambda>env z. \<exists>bo[M]. 
               env \<in> list(A) & 
               is_bool_of_o (M, 
                             \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. 
                                a\<in>A \<longrightarrow> is_Cons(M,a,env,co) \<longrightarrow>
                                fun_apply(M,rp,co,rpco) \<longrightarrow> number1(M, rpco), 
                             bo) &
               pair(M,env,bo,z))"
  and
   formula_rec_replacement: 
       \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
    "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
  and
   formula_rec_lambda_replacement:  
       \<comment> \<open>For the \<open>\<lambda>-abstraction\<close> in the \<^term>\<open>transrec\<close> body\<close>
    "[|M(g); M(A)|] ==>
     strong_replacement (M, 
        \<lambda>x y. mem_formula(M,x) &
              (\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A),
                                   satisfies_is_b(M,A),
                                   satisfies_is_c(M,A,g),
                                   satisfies_is_d(M,A,g), x, c) &
              pair(M, x, c, y)))"
 
 
 lemma (in M_satisfies) Member_replacement':
     "[|M(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (M, \<lambda>env z. env \<in> list(A) &
                      z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)"
 by (insert Member_replacement, simp) 
 
 lemma (in M_satisfies) Equal_replacement':
     "[|M(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (M, \<lambda>env z. env \<in> list(A) &
                      z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)"
 by (insert Equal_replacement, simp) 
 
 lemma (in M_satisfies) Nand_replacement':
     "[|M(A); M(rp); M(rq)|]
      ==> strong_replacement
          (M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)"
 by (insert Nand_replacement, simp) 
 
 lemma (in M_satisfies) Forall_replacement':
    "[|M(A); M(rp)|]
     ==> strong_replacement
         (M, \<lambda>env z.
                env \<in> list(A) &
                z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)"
 by (insert Forall_replacement, simp) 
 
 lemma (in M_satisfies) a_closed:
      "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_a(A,x,y))"
 apply (simp add: satisfies_a_def) 
 apply (blast intro: lam_closed2 Member_replacement') 
 done
 
 lemma (in M_satisfies) a_rel:
      "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
 apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
 done
 
 lemma (in M_satisfies) b_closed:
      "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_b(A,x,y))"
 apply (simp add: satisfies_b_def) 
 apply (blast intro: lam_closed2 Equal_replacement') 
 done
 
 lemma (in M_satisfies) b_rel:
      "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
 apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
 done
 
 lemma (in M_satisfies) c_closed:
      "[|M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)|] 
       ==> M(satisfies_c(A,x,y,rx,ry))"
 apply (simp add: satisfies_c_def) 
 apply (rule lam_closed2) 
 apply (rule Nand_replacement') 
 apply (simp_all add: formula_into_M list_into_M [of _ A])
 done
 
 lemma (in M_satisfies) c_rel:
  "[|M(A); M(f)|] ==> 
   Relation2 (M, formula, formula, 
                satisfies_is_c(M,A,f),
                \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
                                           f ` succ(depth(v)) ` v))"
 apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
 apply (auto del: iffI intro!: lambda_abs2 
             simp add: Relation1_def formula_into_M) 
 done
 
 lemma (in M_satisfies) d_closed:
      "[|M(A); x \<in> formula; M(rx)|] ==> M(satisfies_d(A,x,rx))"
 apply (simp add: satisfies_d_def) 
 apply (rule lam_closed2) 
 apply (rule Forall_replacement') 
 apply (simp_all add: formula_into_M list_into_M [of _ A])
 done
 
 lemma (in M_satisfies) d_rel:
  "[|M(A); M(f)|] ==> 
   Relation1(M, formula, satisfies_is_d(M,A,f), 
      \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
 apply (simp del: rall_abs 
             add: Relation1_def satisfies_is_d_def satisfies_d_def)
 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
 done
 
 
 lemma (in M_satisfies) fr_replace:
       "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 
 by (blast intro: formula_rec_replacement) 
 
 lemma (in M_satisfies) formula_case_satisfies_closed:
  "[|M(g); M(A); x \<in> formula|] ==>
   M(formula_case (satisfies_a(A), satisfies_b(A),
        \<lambda>u v. satisfies_c(A, u, v, 
                          g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
        \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
        x))"
 by (blast intro: a_closed b_closed c_closed d_closed) 
 
 lemma (in M_satisfies) fr_lam_replace:
    "[|M(g); M(A)|] ==>
     strong_replacement (M, \<lambda>x y. x \<in> formula &
             y = \<langle>x, 
                  formula_rec_case(satisfies_a(A),
                                   satisfies_b(A),
                                   satisfies_c(A),
                                   satisfies_d(A), g, x)\<rangle>)"
 apply (insert formula_rec_lambda_replacement) 
 apply (simp add: formula_rec_case_def formula_case_satisfies_closed
                  formula_case_abs [OF a_rel b_rel c_rel d_rel]) 
 done
 
 
 
 text\<open>Instantiate locale \<open>Formula_Rec\<close> for the 
       Function \<^term>\<open>satisfies\<close>\<close>
 
 lemma (in M_satisfies) Formula_Rec_axioms_M:
    "M(A) ==>
     Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A), 
                           satisfies_b(A), satisfies_is_b(M,A), 
                           satisfies_c(A), satisfies_is_c(M,A), 
                           satisfies_d(A), satisfies_is_d(M,A))"
 apply (rule Formula_Rec_axioms.intro)
 apply (assumption | 
        rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
        fr_replace [unfolded satisfies_MH_def]
        fr_lam_replace) +
 done
 
 
 theorem (in M_satisfies) Formula_Rec_M: 
     "M(A) ==>
      Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
                          satisfies_b(A), satisfies_is_b(M,A), 
                          satisfies_c(A), satisfies_is_c(M,A), 
                          satisfies_d(A), satisfies_is_d(M,A))"
   apply (rule Formula_Rec.intro)
    apply (rule M_satisfies.axioms, rule M_satisfies_axioms)
   apply (erule Formula_Rec_axioms_M) 
   done
 
 lemmas (in M_satisfies) 
     satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
 and satisfies_abs'    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
 
 
 lemma (in M_satisfies) satisfies_closed:
   "[|M(A); p \<in> formula|] ==> M(satisfies(A,p))"
 by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M]  
               satisfies_eq) 
 
 lemma (in M_satisfies) satisfies_abs:
   "[|M(A); M(z); p \<in> formula|] 
    ==> is_satisfies(M,A,p,z) \<longleftrightarrow> z = satisfies(A,p)"
 by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M]  
                satisfies_eq is_satisfies_def satisfies_MH_def)
 
 
 subsection\<open>Internalizations Needed to Instantiate \<open>M_satisfies\<close>\<close>
 
 subsubsection\<open>The Operator \<^term>\<open>is_depth_apply\<close>, Internalized\<close>
 
 (* is_depth_apply(M,h,p,z) ==
     \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
       2        1         0
         finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
         fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
 definition
   depth_apply_fm :: "[i,i,i]=>i" where
     "depth_apply_fm(h,p,z) ==
        Exists(Exists(Exists(
         And(finite_ordinal_fm(2),
          And(depth_fm(p#+3,2),
           And(succ_fm(2,1),
            And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"
 
 lemma depth_apply_type [TC]:
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> depth_apply_fm(x,y,z) \<in> formula"
 by (simp add: depth_apply_fm_def)
 
 lemma sats_depth_apply_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, depth_apply_fm(x,y,z), env) \<longleftrightarrow>
         is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: depth_apply_fm_def is_depth_apply_def)
 
 lemma depth_apply_iff_sats:
     "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
         i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
      ==> is_depth_apply(##A, x, y, z) \<longleftrightarrow> sats(A, depth_apply_fm(i,j,k), env)"
 by simp
 
 lemma depth_apply_reflection:
      "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
                \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_depth_apply_def)
 apply (intro FOL_reflections function_reflections depth_reflection 
              finite_ordinal_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>satisfies_is_a\<close>, Internalized\<close>
 
 (* satisfies_is_a(M,A) == 
     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. is_bool_of_o(M, 
                       \<exists>nx[M]. \<exists>ny[M]. 
                        is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
                 zz)  *)
 
 definition
   satisfies_is_a_fm :: "[i,i,i,i]=>i" where
   "satisfies_is_a_fm(A,x,y,z) ==
    Forall(
      Implies(is_list_fm(succ(A),0),
        lambda_fm(
          bool_of_o_fm(Exists(
                        Exists(And(nth_fm(x#+6,3,1), 
                                And(nth_fm(y#+6,3,0), 
                                    Member(1,0))))), 0), 
          0, succ(z))))"
 
 lemma satisfies_is_a_type [TC]:
      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
       ==> satisfies_is_a_fm(A,x,y,z) \<in> formula"
 by (simp add: satisfies_is_a_fm_def)
 
 lemma sats_satisfies_is_a_fm [simp]:
    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) \<longleftrightarrow>
         satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=x in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm 
                  sats_bool_of_o_fm)
 done
 
 lemma satisfies_is_a_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
    ==> satisfies_is_a(##A,nu,nx,ny,nz) \<longleftrightarrow>
        sats(A, satisfies_is_a_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_a_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_a_def) 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>satisfies_is_b\<close>, Internalized\<close>
 
 (* satisfies_is_b(M,A) == 
     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. is_bool_of_o(M, 
                       \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
                 zz) *)
 
 definition
   satisfies_is_b_fm :: "[i,i,i,i]=>i" where
  "satisfies_is_b_fm(A,x,y,z) ==
    Forall(
      Implies(is_list_fm(succ(A),0),
        lambda_fm(
          bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0), 
          0, succ(z))))"
 
 lemma satisfies_is_b_type [TC]:
      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
       ==> satisfies_is_b_fm(A,x,y,z) \<in> formula"
 by (simp add: satisfies_is_b_fm_def)
 
 lemma sats_satisfies_is_b_fm [simp]:
    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) \<longleftrightarrow>
         satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=x in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm 
                  sats_bool_of_o_fm)
 done
 
 lemma satisfies_is_b_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
    ==> satisfies_is_b(##A,nu,nx,ny,nz) \<longleftrightarrow>
        sats(A, satisfies_is_b_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_b_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_b_def) 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>satisfies_is_c\<close>, Internalized\<close>
 
 (* satisfies_is_c(M,A,h) == 
     \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
                  (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
                  (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
                  (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
                 zz) *)
 
 definition
   satisfies_is_c_fm :: "[i,i,i,i,i]=>i" where
  "satisfies_is_c_fm(A,h,p,q,zz) ==
    Forall(
      Implies(is_list_fm(succ(A),0),
        lambda_fm(
          Exists(Exists(
           And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
           And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
               Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
          0, succ(zz))))"
 
 lemma satisfies_is_c_type [TC]:
      "[| A \<in> nat; h \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
       ==> satisfies_is_c_fm(A,h,x,y,z) \<in> formula"
 by (simp add: satisfies_is_c_fm_def)
 
 lemma sats_satisfies_is_c_fm [simp]:
    "[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) \<longleftrightarrow>
         satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env), 
                             nth(y,env), nth(z,env))"  
 by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
 
 lemma satisfies_is_c_iff_sats:
   "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny; 
       nth(z,env) = nz;
       u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) \<longleftrightarrow>
        sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
 by simp
 
 theorem satisfies_is_c_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
                \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
 apply (unfold satisfies_is_c_def) 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
              is_list_reflection)
 done
 
 subsubsection\<open>The Operator \<^term>\<open>satisfies_is_d\<close>, Internalized\<close>
 
 (* satisfies_is_d(M,A,h) == 
     \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
              is_lambda(M, lA, 
                 \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
                     is_bool_of_o(M, 
                            \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
                               x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow> 
                               fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp),
                   z),
                zz) *)
 
 definition
   satisfies_is_d_fm :: "[i,i,i,i]=>i" where
  "satisfies_is_d_fm(A,h,p,zz) ==
    Forall(
      Implies(is_list_fm(succ(A),0),
        lambda_fm(
          Exists(
            And(depth_apply_fm(h#+5,p#+5,0),
                bool_of_o_fm(
                 Forall(Forall(Forall(
                  Implies(Member(2,A#+8),
                   Implies(Cons_fm(2,5,1),
                    Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
          0, succ(zz))))"
 
 lemma satisfies_is_d_type [TC]:
      "[| A \<in> nat; h \<in> nat; x \<in> nat; z \<in> nat |]
       ==> satisfies_is_d_fm(A,h,x,z) \<in> formula"
 by (simp add: satisfies_is_d_fm_def)
 
 lemma sats_satisfies_is_d_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) \<longleftrightarrow>
         satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
 by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
               sats_bool_of_o_fm)
 
 lemma satisfies_is_d_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    ==> satisfies_is_d(##A,nu,nx,ny,nz) \<longleftrightarrow>
        sats(A, satisfies_is_d_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_d_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_d_def) 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
              is_list_reflection)
 done
 
 
 subsubsection\<open>The Operator \<^term>\<open>satisfies_MH\<close>, Internalized\<close>
 
 (* satisfies_MH == 
     \<lambda>M A u f zz. 
          \<forall>fml[M]. is_formula(M,fml) \<longrightarrow>
              is_lambda (M, fml, 
                is_formula_case (M, satisfies_is_a(M,A), 
                                 satisfies_is_b(M,A), 
                                 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
                zz) *)
 
 definition
   satisfies_MH_fm :: "[i,i,i,i]=>i" where
  "satisfies_MH_fm(A,u,f,zz) ==
    Forall(
      Implies(is_formula_fm(0),
        lambda_fm(
          formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0), 
                          satisfies_is_b_fm(A#+7,2,1,0), 
                          satisfies_is_c_fm(A#+7,f#+7,2,1,0), 
                          satisfies_is_d_fm(A#+6,f#+6,1,0), 
                          1, 0),
          0, succ(zz))))"
 
 lemma satisfies_MH_type [TC]:
      "[| A \<in> nat; u \<in> nat; x \<in> nat; z \<in> nat |]
       ==> satisfies_MH_fm(A,u,x,z) \<in> formula"
 by (simp add: satisfies_MH_fm_def)
 
 lemma sats_satisfies_MH_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_MH_fm(u,x,y,z), env) \<longleftrightarrow>
         satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
 by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
               sats_formula_case_fm)
 
 lemma satisfies_MH_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    ==> satisfies_MH(##A,nu,nx,ny,nz) \<longleftrightarrow>
        sats(A, satisfies_MH_fm(u,x,y,z), env)"
 by simp 
 
 lemmas satisfies_reflections =
        is_lambda_reflection is_formula_reflection 
        is_formula_case_reflection
        satisfies_is_a_reflection satisfies_is_b_reflection 
        satisfies_is_c_reflection satisfies_is_d_reflection
 
 theorem satisfies_MH_reflection:
      "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_MH_def) 
 apply (intro FOL_reflections satisfies_reflections)
 done
 
 
 subsection\<open>Lemmas for Instantiating the Locale \<open>M_satisfies\<close>\<close>
 
 
 subsubsection\<open>The \<^term>\<open>Member\<close> Case\<close>
 
 lemma Member_Reflects:
  "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
           v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
           is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
              v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
              is_nth(##Lset(i), y, v, ny) \<and>
           is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
 by (intro FOL_reflections function_reflections nth_reflection 
           bool_of_o_reflection)
 
 
 lemma Member_replacement:
     "[|L(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
               is_bool_of_o(L, nx \<in> ny, bo) &
               pair(L, env, bo, z))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,x,y}" 
          in gen_separation_multi [OF Member_Reflects], 
        auto)
 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
 
 subsubsection\<open>The \<^term>\<open>Equal\<close> Case\<close>
 
 lemma Equal_Reflects:
  "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
           v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
           is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
              v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
              is_nth(##Lset(i), y, v, ny) \<and>
           is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
 by (intro FOL_reflections function_reflections nth_reflection 
           bool_of_o_reflection)
 
 
 lemma Equal_replacement:
     "[|L(A); x \<in> nat; y \<in> nat|]
      ==> strong_replacement
          (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
               is_bool_of_o(L, nx = ny, bo) &
               pair(L, env, bo, z))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,x,y}" 
          in gen_separation_multi [OF Equal_Reflects], 
        auto)
 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
 subsubsection\<open>The \<^term>\<open>Nand\<close> Case\<close>
 
 lemma Nand_Reflects:
     "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
                (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
                  fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
                  is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
                  u \<in> list(A) \<and> pair(L, u, notpq, x)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
      (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
        fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
        is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
        u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
 apply (unfold is_and_def is_not_def) 
 apply (intro FOL_reflections function_reflections)
 done
 
 lemma Nand_replacement:
     "[|L(A); L(rp); L(rq)|]
      ==> strong_replacement
          (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
                fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
                is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
                env \<in> list(A) & pair(L, env, notpq, z))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,rp,rq}" 
          in gen_separation_multi [OF Nand_Reflects],
        auto)
 apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
 apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
 done
 
 
 subsubsection\<open>The \<^term>\<open>Forall\<close> Case\<close>
 
 lemma Forall_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
                  is_bool_of_o (L,
      \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
                 is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
                 number1(L,rpco),
                            bo) \<and> pair(L,u,bo,x)),
  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
         is_bool_of_o (##Lset(i),
  \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
             is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
             number1(##Lset(i),rpco),
                        bo) \<and> pair(##Lset(i),u,bo,x))]"
 apply (unfold is_bool_of_o_def) 
 apply (intro FOL_reflections function_reflections Cons_reflection)
 done
 
 lemma Forall_replacement:
    "[|L(A); L(rp)|]
     ==> strong_replacement
         (L, \<lambda>env z. \<exists>bo[L]. 
               env \<in> list(A) & 
               is_bool_of_o (L, 
                             \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
                                a\<in>A \<longrightarrow> is_Cons(L,a,env,co) \<longrightarrow>
                                fun_apply(L,rp,co,rpco) \<longrightarrow> number1(L, rpco), 
                             bo) &
               pair(L,env,bo,z))"
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,list(A),B,rp}" 
          in gen_separation_multi [OF Forall_Reflects],
        auto)
 apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
 apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
 done
 
 subsubsection\<open>The \<^term>\<open>transrec_replacement\<close> Case\<close>
 
 lemma formula_rec_replacement_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
              is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
              is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
 by (intro FOL_reflections function_reflections satisfies_MH_reflection 
           is_wfrec_reflection) 
 
 lemma formula_rec_replacement: 
       \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
    "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
-apply (rule transrec_replacementI, simp add: nat_into_M) 
+apply (rule L.transrec_replacementI, simp add: L.nat_into_M)
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
          in gen_separation_multi [OF formula_rec_replacement_Reflects],
-       auto simp add: nat_into_M)
+       auto simp add: L.nat_into_M)
 apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
 done
 
 
 subsubsection\<open>The Lambda Replacement Case\<close>
 
 lemma formula_rec_lambda_replacement_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
      mem_formula(L,u) &
      (\<exists>c[L].
          is_formula_case
           (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
            satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
            u, c) &
          pair(L,u,c,x)),
   \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) &
      (\<exists>c \<in> Lset(i).
          is_formula_case
           (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
            satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
            u, c) &
          pair(##Lset(i),u,c,x))]"
 by (intro FOL_reflections function_reflections mem_formula_reflection
           is_formula_case_reflection satisfies_is_a_reflection
           satisfies_is_b_reflection satisfies_is_c_reflection
           satisfies_is_d_reflection)  
 
 lemma formula_rec_lambda_replacement: 
       \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
    "[|L(g); L(A)|] ==>
     strong_replacement (L, 
        \<lambda>x y. mem_formula(L,x) &
              (\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A),
                                   satisfies_is_b(L,A),
                                   satisfies_is_c(L,A,g),
                                   satisfies_is_d(L,A,g), x, c) &
              pair(L, x, c, y)))" 
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,g}"
          in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
        auto)
 apply (rule_tac env="[A,g,B]" in DPow_LsetI)
 apply (rule sep_rules mem_formula_iff_sats
           formula_case_iff_sats satisfies_is_a_iff_sats
           satisfies_is_b_iff_sats satisfies_is_c_iff_sats
           satisfies_is_d_iff_sats | simp)+
 done
 
 
 subsection\<open>Instantiating \<open>M_satisfies\<close>\<close>
 
 lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
   apply (rule M_satisfies_axioms.intro)
        apply (assumption | rule
          Member_replacement Equal_replacement 
          Nand_replacement Forall_replacement
          formula_rec_replacement formula_rec_lambda_replacement)+
   done
 
 theorem M_satisfies_L: "M_satisfies(L)"
   apply (rule M_satisfies.intro)
    apply (rule M_eclose_L)
   apply (rule M_satisfies_axioms_L)
   done
 
 text\<open>Finally: the point of the whole theory!\<close>
 lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
    and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]
 
 end
diff --git a/src/ZF/Constructible/Separation.thy b/src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy
+++ b/src/ZF/Constructible/Separation.thy
@@ -1,310 +1,310 @@
 (*  Title:      ZF/Constructible/Separation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 section\<open>Early Instances of Separation and Strong Replacement\<close>
 
 theory Separation imports L_axioms WF_absolute begin
 
 text\<open>This theory proves all instances needed for locale \<open>M_basic\<close>\<close>
 
 text\<open>Helps us solve for de Bruijn indices!\<close>
 lemma nth_ConsI: "[|nth(n,l) = x; n \<in> 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\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
       ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
 by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
 
 lemma Collect_conj_in_DPow_Lset:
      "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
       ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> 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:
      "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
 apply (unfold separation_def, clarify)
 apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
 apply simp_all
 done
 
 text\<open>Reduces the original comprehension to the reflected one\<close>
 lemma reflection_imp_L_separation:
       "[| \<forall>x\<in>Lset(j). P(x) \<longleftrightarrow> Q(x);
           {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
           Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
 apply (rule_tac i = "succ(j)" in L_I)
  prefer 2 apply simp
 apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> 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\<open>Encapsulates the standard proof script for proving instances of 
       Separation.\<close>
 lemma gen_separation:
  assumes reflection: "REFLECTS [P,Q]"
      and Lu:         "L(u)"
      and collI: "!!j. u \<in> Lset(j)
                 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> 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\<open>As above, but typically \<^term>\<open>u\<close> is a finite enumeration such as
   \<^term>\<open>{a,b}\<close>; thus the new subgoal gets the assumption
   \<^term>\<open>{a,b} \<subseteq> Lset(i)\<close>, which is logically equivalent to 
   \<^term>\<open>a \<in> Lset(i)\<close> and \<^term>\<open>b \<in> Lset(i)\<close>.\<close>
 lemma gen_separation_multi:
  assumes reflection: "REFLECTS [P,Q]"
      and Lu:         "L(u)"
      and collI: "!!j. u \<subseteq> Lset(j)
                 \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> 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\<open>Separation for Intersection\<close>
 
 lemma Inter_Reflects:
      "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x \<in> y,
                \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A \<longrightarrow> x \<in> y]"
 by (intro FOL_reflections)
 
 lemma Inter_separation:
      "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A \<longrightarrow> x\<in>y)"
 apply (rule gen_separation [OF Inter_Reflects], simp)
 apply (rule DPow_LsetI)
  txt\<open>I leave this one example of a manual proof.  The tedium of manually
       instantiating \<^term>\<open>i\<close>, \<^term>\<open>j\<close> and \<^term>\<open>env\<close> is obvious.\<close>
 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\<open>Separation for Set Difference\<close>
 
 lemma Diff_Reflects:
      "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]"
 by (intro FOL_reflections)  
 
 lemma Diff_separation:
      "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
 apply (rule gen_separation [OF Diff_Reflects], simp)
 apply (rule_tac env="[B]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
 subsection\<open>Separation for Cartesian Product\<close>
 
 lemma cartprod_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
                 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
                                    pair(##Lset(i),x,y,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma cartprod_separation:
      "[| L(A); L(B) |]
       ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>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\<open>Separation for Image\<close>
 
 lemma image_Reflects:
      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
            \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(##Lset(i),x,y,p))]"
 by (intro FOL_reflections function_reflections)
 
 lemma image_separation:
      "[| L(A); L(r) |]
       ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>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\<open>Separation for Converse\<close>
 
 lemma converse_Reflects:
   "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
      \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>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,
          \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>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\<open>Separation for Restriction\<close>
 
 lemma restrict_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
         \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma restrict_separation:
    "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>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\<open>Separation for Composition\<close>
 
 lemma comp_Reflects:
      "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                   xy\<in>s & yz\<in>r,
         \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
                   pair(##Lset(i),x,z,xz) & pair(##Lset(i),x,y,xy) &
                   pair(##Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
 by (intro FOL_reflections function_reflections)
 
 lemma comp_separation:
      "[| L(r); L(s) |]
       ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                   xy\<in>s & yz\<in>r)"
 apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto)
 txt\<open>Subgoals after applying general ``separation'' rule:
      @{subgoals[display,indent=0,margin=65]}\<close>
 apply (rule_tac env="[r,s]" in DPow_LsetI)
 txt\<open>Subgoals ready for automatic synthesis of a formula:
      @{subgoals[display,indent=0,margin=65]}\<close>
 apply (rule sep_rules | simp)+
 done
 
 
 subsection\<open>Separation for Predecessors in an Order\<close>
 
 lemma pred_Reflects:
      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
                     \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]"
 by (intro FOL_reflections function_reflections)
 
 lemma pred_separation:
      "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>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\<open>Separation for the Membership Relation\<close>
 
 lemma Memrel_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
             \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]"
 by (intro FOL_reflections function_reflections)
 
 lemma Memrel_separation:
      "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
 apply (rule gen_separation [OF Memrel_Reflects nonempty])
 apply (rule_tac env="[]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
 
 subsection\<open>Replacement for FunSpace\<close>
 
 lemma funspace_succ_Reflects:
  "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
             pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
             upair(L,cnbf,cnbf,z)),
         \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
               \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> 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, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>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\<open>Separation for a Theorem about \<^term>\<open>is_recfun\<close>\<close>
 
 lemma is_recfun_reflects:
   "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
                 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                    fx \<noteq> gx),
    \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
           pair(##Lset(i),x,a,xa) & xa \<in> r & pair(##Lset(i),x,b,xb) & xb \<in> r &
                 (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) &
                   fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
 lemma is_recfun_separation:
      \<comment> \<open>for well-founded recursion\<close>
      "[| L(r); L(f); L(g); L(a); L(b) |]
      ==> separation(L,
             \<lambda>x. \<exists>xa[L]. \<exists>xb[L].
                 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                    fx \<noteq> 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\<open>Instantiating the locale \<open>M_basic\<close>\<close>
 text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions
 such as intersection, Cartesian Product and image.\<close>
 
 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 power_ax)+
   done
 
 theorem M_basic_L: " M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 
 end