src/ZF/Constructible/Internalize.thy

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 theory Internalize imports L_axioms Datatype_absolute begin
 
-subsection{*Internalized Forms of Data Structuring Operators*}
-
-subsubsection{*The Formula @{term is_Inl}, Internalized*}
+subsection\<open>Internalized Forms of Data Structuring Operators\<close>
+
+subsubsection\<open>The Formula @{term is_Inl}, Internalized\<close>
 
 (*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
 definition
   Inl_fm :: "[i,i]=>i" where
     "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"

 apply (simp only: is_Inl_def)
 apply (intro FOL_reflections function_reflections)
 done
 
 
-subsubsection{*The Formula @{term is_Inr}, Internalized*}
+subsubsection\<open>The Formula @{term is_Inr}, Internalized\<close>
 
 (*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
 definition
   Inr_fm :: "[i,i]=>i" where
     "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"

 apply (simp only: is_Inr_def)
 apply (intro FOL_reflections function_reflections)
 done
 
 
-subsubsection{*The Formula @{term is_Nil}, Internalized*}
+subsubsection\<open>The Formula @{term is_Nil}, Internalized\<close>
 
 (* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
 
 definition
   Nil_fm :: "i=>i" where

 apply (simp only: is_Nil_def)
 apply (intro FOL_reflections function_reflections Inl_reflection)
 done
 
 
-subsubsection{*The Formula @{term is_Cons}, Internalized*}
+subsubsection\<open>The Formula @{term is_Cons}, Internalized\<close>
 
 
 (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
 definition
   Cons_fm :: "[i,i,i]=>i" where

                \<lambda>i x. is_Cons(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Cons_def)
 apply (intro FOL_reflections pair_reflection Inr_reflection)
 done
 
-subsubsection{*The Formula @{term is_quasilist}, Internalized*}
+subsubsection\<open>The Formula @{term is_quasilist}, Internalized\<close>
 
 (* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
 
 definition
   quasilist_fm :: "i=>i" where

 apply (simp only: is_quasilist_def)
 apply (intro FOL_reflections Nil_reflection Cons_reflection)
 done
 
 
-subsection{*Absoluteness for the Function @{term nth}*}
-
-
-subsubsection{*The Formula @{term is_hd}, Internalized*}
+subsection\<open>Absoluteness for the Function @{term nth}\<close>
+
+
+subsubsection\<open>The Formula @{term is_hd}, Internalized\<close>
 
 (*   "is_hd(M,xs,H) == 
        (is_Nil(M,xs) \<longrightarrow> empty(M,H)) &
        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
        (is_quasilist(M,xs) | empty(M,H))" *)

 apply (intro FOL_reflections Nil_reflection Cons_reflection
              quasilist_reflection empty_reflection)  
 done
 
 
-subsubsection{*The Formula @{term is_tl}, Internalized*}
+subsubsection\<open>The Formula @{term is_tl}, Internalized\<close>
 
 (*     "is_tl(M,xs,T) ==
        (is_Nil(M,xs) \<longrightarrow> T=xs) &
        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
        (is_quasilist(M,xs) | empty(M,T))" *)

 apply (intro FOL_reflections Nil_reflection Cons_reflection
              quasilist_reflection empty_reflection)
 done
 
 
-subsubsection{*The Operator @{term is_bool_of_o}*}
+subsubsection\<open>The Operator @{term is_bool_of_o}\<close>
 
 (*   is_bool_of_o :: "[i=>o, o, i] => o"
    "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" *)
 
-text{*The formula @{term p} has no free variables.*}
+text\<open>The formula @{term p} has no free variables.\<close>
 definition
   bool_of_o_fm :: "[i, i]=>i" where
   "bool_of_o_fm(p,z) == 
     Or(And(p,number1_fm(z)),
        And(Neg(p),empty_fm(z)))"

 apply (simp (no_asm) only: is_bool_of_o_def)
 apply (intro FOL_reflections function_reflections, assumption+)
 done
 
 
-subsection{*More Internalizations*}
-
-subsubsection{*The Operator @{term is_lambda}*}
-
-text{*The two arguments of @{term p} are always 1, 0. Remember that
- @{term p} will be enclosed by three quantifiers.*}
+subsection\<open>More Internalizations\<close>
+
+subsubsection\<open>The Operator @{term is_lambda}\<close>
+
+text\<open>The two arguments of @{term p} are always 1, 0. Remember that
+ @{term p} will be enclosed by three quantifiers.\<close>
 
 (* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
     "is_lambda(M, A, is_b, z) == 
        \<forall>p[M]. p \<in> z \<longleftrightarrow>
         (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)

   "lambda_fm(p,A,z) == 
     Forall(Iff(Member(0,succ(z)),
             Exists(Exists(And(Member(1,A#+3),
                            And(pair_fm(1,0,2), p))))))"
 
-text{*We call @{term p} with arguments x, y by equating them with 
-  the corresponding quantified variables with de Bruijn indices 1, 0.*}
+text\<open>We call @{term p} with arguments x, y by equating them with 
+  the corresponding quantified variables with de Bruijn indices 1, 0.\<close>
 
 lemma is_lambda_type [TC]:
      "[| p \<in> formula; x \<in> nat; y \<in> nat |] 
       ==> lambda_fm(p,x,y) \<in> formula"
 by (simp add: lambda_fm_def) 

                \<lambda>i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i),x), f(x))]"
 apply (simp (no_asm_use) only: is_lambda_def)
 apply (intro FOL_reflections is_b_reflection pair_reflection)
 done
 
-subsubsection{*The Operator @{term is_Member}, Internalized*}
+subsubsection\<open>The Operator @{term is_Member}, Internalized\<close>
 
 (*    "is_Member(M,x,y,Z) ==
         \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
 definition
   Member_fm :: "[i,i,i]=>i" where

                \<lambda>i x. is_Member(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Member_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection)
 done
 
-subsubsection{*The Operator @{term is_Equal}, Internalized*}
+subsubsection\<open>The Operator @{term is_Equal}, Internalized\<close>
 
 (*    "is_Equal(M,x,y,Z) ==
         \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
 definition
   Equal_fm :: "[i,i,i]=>i" where

                \<lambda>i x. is_Equal(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Equal_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
 done
 
-subsubsection{*The Operator @{term is_Nand}, Internalized*}
+subsubsection\<open>The Operator @{term is_Nand}, Internalized\<close>
 
 (*    "is_Nand(M,x,y,Z) ==
         \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
 definition
   Nand_fm :: "[i,i,i]=>i" where

                \<lambda>i x. is_Nand(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Nand_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
 done
 
-subsubsection{*The Operator @{term is_Forall}, Internalized*}
+subsubsection\<open>The Operator @{term is_Forall}, Internalized\<close>
 
 (* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
 definition
   Forall_fm :: "[i,i]=>i" where
     "Forall_fm(x,Z) ==

 apply (simp only: is_Forall_def)
 apply (intro FOL_reflections pair_reflection Inr_reflection)
 done
 
 
-subsubsection{*The Operator @{term is_and}, Internalized*}
+subsubsection\<open>The Operator @{term is_and}, Internalized\<close>
 
 (* is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
                        (~number1(M,a) & empty(M,z)) *)
 definition
   and_fm :: "[i,i,i]=>i" where

 apply (simp only: is_and_def)
 apply (intro FOL_reflections function_reflections)
 done
 
 
-subsubsection{*The Operator @{term is_or}, Internalized*}
+subsubsection\<open>The Operator @{term is_or}, Internalized\<close>
 
 (* is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
                      (~number1(M,a) & z=b) *)
 
 definition

 apply (intro FOL_reflections function_reflections)
 done
 
 
 
-subsubsection{*The Operator @{term is_not}, Internalized*}
+subsubsection\<open>The Operator @{term is_not}, Internalized\<close>
 
 (* is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
                      (~number1(M,a) & number1(M,z)) *)
 definition
   not_fm :: "[i,i]=>i" where

     Inl_reflection Inr_reflection Nil_reflection Cons_reflection
     quasilist_reflection hd_reflection tl_reflection bool_of_o_reflection
     is_lambda_reflection Member_reflection Equal_reflection Nand_reflection
     Forall_reflection is_and_reflection is_or_reflection is_not_reflection
 
-subsection{*Well-Founded Recursion!*}
-
-subsubsection{*The Operator @{term M_is_recfun}*}
-
-text{*Alternative definition, minimizing nesting of quantifiers around MH*}
+subsection\<open>Well-Founded Recursion!\<close>
+
+subsubsection\<open>The Operator @{term M_is_recfun}\<close>
+
+text\<open>Alternative definition, minimizing nesting of quantifiers around MH\<close>
 lemma M_is_recfun_iff:
    "M_is_recfun(M,MH,r,a,f) \<longleftrightarrow>
     (\<forall>z[M]. z \<in> f \<longleftrightarrow> 
      (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M]. 
              MH(x, f_r_sx, y) & pair(M,x,y,z) &

                 pair(M,x,a,xa) & upair(M,x,x,sx) &
                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
                xa \<in> r)"
 *)
 
-text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
+text\<open>The three arguments of @{term p} are always 2, 1, 0 and z\<close>
 definition
   is_recfun_fm :: "[i, i, i, i]=>i" where
   "is_recfun_fm(p,r,a,f) == 
    Forall(Iff(Member(0,succ(f)),
     Exists(Exists(Exists(

   "[| 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)|]
    ==> M_is_recfun(##A, MH, x, y, z) \<longleftrightarrow> sats(A, is_recfun_fm(p,i,j,k), env)"
 by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) 
 
-text{*The additional variable in the premise, namely @{term f'}, is essential.
+text\<open>The additional variable in the premise, namely @{term f'}, is essential.
 It lets @{term MH} depend upon @{term x}, which seems often necessary.
-The same thing occurs in @{text is_wfrec_reflection}.*}
+The same thing occurs in @{text is_wfrec_reflection}.\<close>
 theorem is_recfun_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. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), 

 apply (simp (no_asm_use) only: M_is_recfun_def)
 apply (intro FOL_reflections function_reflections
              restriction_reflection MH_reflection)
 done
 
-subsubsection{*The Operator @{term is_wfrec}*}
-
-text{*The three arguments of @{term p} are always 2, 1, 0;
-      @{term p} is enclosed by 5 quantifiers.*}
+subsubsection\<open>The Operator @{term is_wfrec}\<close>
+
+text\<open>The three arguments of @{term p} are always 2, 1, 0;
+      @{term p} is enclosed by 5 quantifiers.\<close>
 
 (* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
     "is_wfrec(M,MH,r,a,z) == 
       \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
 definition

   "is_wfrec_fm(p,r,a,z) == 
     Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
            Exists(Exists(Exists(Exists(
              And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
 
-text{*We call @{term p} with arguments a, f, z by equating them with 
-  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
-
-text{*There's an additional existential quantifier to ensure that the
-      environments in both calls to MH have the same length.*}
+text\<open>We call @{term p} with arguments a, f, z by equating them with 
+  the corresponding quantified variables with de Bruijn indices 2, 1, 0.\<close>
+
+text\<open>There's an additional existential quantifier to ensure that the
+      environments in both calls to MH have the same length.\<close>
 
 lemma is_wfrec_type [TC]:
      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
       ==> is_wfrec_fm(p,x,y,z) \<in> formula"
 by (simp add: is_wfrec_fm_def) 

 apply (simp (no_asm_use) only: is_wfrec_def)
 apply (intro FOL_reflections MH_reflection is_recfun_reflection)
 done
 
 
-subsection{*For Datatypes*}
-
-subsubsection{*Binary Products, Internalized*}
+subsection\<open>For Datatypes\<close>
+
+subsubsection\<open>Binary Products, Internalized\<close>
 
 definition
   cartprod_fm :: "[i,i,i]=>i" where
 (* "cartprod(M,A,B,z) ==
         \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)

 apply (simp only: cartprod_def)
 apply (intro FOL_reflections pair_reflection)
 done
 
 
-subsubsection{*Binary Sums, Internalized*}
+subsubsection\<open>Binary Sums, Internalized\<close>
 
 (* "is_sum(M,A,B,Z) ==
        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
          3      2       1        0
        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &

 apply (simp only: is_sum_def)
 apply (intro FOL_reflections function_reflections cartprod_reflection)
 done
 
 
-subsubsection{*The Operator @{term quasinat}*}
+subsubsection\<open>The Operator @{term quasinat}\<close>
 
 (* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
 definition
   quasinat_fm :: "i=>i" where
     "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"

 apply (simp only: is_quasinat_def)
 apply (intro FOL_reflections function_reflections)
 done
 
 
-subsubsection{*The Operator @{term is_nat_case}*}
-text{*I could not get it to work with the more natural assumption that 
+subsubsection\<open>The Operator @{term is_nat_case}\<close>
+text\<open>I could not get it to work with the more natural assumption that 
  @{term is_b} takes two arguments.  Instead it must be a formula where 1 and 0
- stand for @{term m} and @{term b}, respectively.*}
+ stand for @{term m} and @{term b}, respectively.\<close>
 
 (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
     "is_nat_case(M, a, is_b, k, z) ==
        (empty(M,k) \<longrightarrow> z=a) &
        (\<forall>m[M]. successor(M,m,k) \<longrightarrow> is_b(m,z)) &
        (is_quasinat(M,k) | empty(M,z))" *)
-text{*The formula @{term is_b} has free variables 1 and 0.*}
+text\<open>The formula @{term is_b} has free variables 1 and 0.\<close>
 definition
   is_nat_case_fm :: "[i, i, i, i]=>i" where
  "is_nat_case_fm(a,is_b,k,z) == 
     And(Implies(empty_fm(k), Equal(z,a)),
         And(Forall(Implies(succ_fm(0,succ(k)), 

       i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
    ==> is_nat_case(##A, x, is_b, y, z) \<longleftrightarrow> sats(A, is_nat_case_fm(i,p,j,k), env)"
 by (simp add: sats_is_nat_case_fm [of A is_b])
 
 
-text{*The second argument of @{term is_b} gives it direct access to @{term x},
+text\<open>The second argument of @{term is_b} gives it direct access to @{term x},
   which is essential for handling free variable references.  Without this
-  argument, we cannot prove reflection for @{term iterates_MH}.*}
+  argument, we cannot prove reflection for @{term iterates_MH}.\<close>
 theorem is_nat_case_reflection:
   assumes is_b_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
                      \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),

 apply (intro FOL_reflections function_reflections
              restriction_reflection is_b_reflection quasinat_reflection)
 done
 
 
-subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
+subsection\<open>The Operator @{term iterates_MH}, Needed for Iteration\<close>
 
 (*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
    "iterates_MH(M,isF,v,n,g,z) ==
         is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
                     n, z)" *)

       i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
    ==> iterates_MH(##A, is_F, v, x, y, z) \<longleftrightarrow>
        sats(A, iterates_MH_fm(p,i',i,j,k), env)"
 by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) 
 
-text{*The second argument of @{term p} gives it direct access to @{term x},
+text\<open>The second argument of @{term p} gives it direct access to @{term x},
   which is essential for handling free variable references.  Without this
-  argument, we cannot prove reflection for @{term list_N}.*}
+  argument, we cannot prove reflection for @{term list_N}.\<close>
 theorem iterates_MH_reflection:
   assumes p_reflection:
     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
                      \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
  shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),

 apply (intro FOL_reflections function_reflections is_nat_case_reflection
              restriction_reflection p_reflection)
 done
 
 
-subsubsection{*The Operator @{term is_iterates}*}
-
-text{*The three arguments of @{term p} are always 2, 1, 0;
-      @{term p} is enclosed by 9 (??) quantifiers.*}
+subsubsection\<open>The Operator @{term is_iterates}\<close>
+
+text\<open>The three arguments of @{term p} are always 2, 1, 0;
+      @{term p} is enclosed by 9 (??) quantifiers.\<close>
 
 (*    "is_iterates(M,isF,v,n,Z) == 
       \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
        1       0       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*)
 

       And(succ_fm(n#+2,1),
        And(Memrel_fm(1,0),
               is_wfrec_fm(iterates_MH_fm(p, v#+7, 2, 1, 0), 
                           0, n#+2, Z#+2)))))"
 
-text{*We call @{term p} with arguments a, f, z by equating them with 
-  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
+text\<open>We call @{term p} with arguments a, f, z by equating them with 
+  the corresponding quantified variables with de Bruijn indices 2, 1, 0.\<close>
 
 
 lemma is_iterates_type [TC]:
      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
       ==> is_iterates_fm(p,x,y,z) \<in> formula"

       i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
    ==> is_iterates(##A, is_F, x, y, z) \<longleftrightarrow>
        sats(A, is_iterates_fm(p,i,j,k), env)"
 by (simp add: sats_is_iterates_fm [OF is_F_iff_sats]) 
 
-text{*The second argument of @{term p} gives it direct access to @{term x},
+text\<open>The second argument of @{term p} gives it direct access to @{term x},
   which is essential for handling free variable references.  Without this
-  argument, we cannot prove reflection for @{term list_N}.*}
+  argument, we cannot prove reflection for @{term list_N}.\<close>
 theorem is_iterates_reflection:
   assumes p_reflection:
     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
                      \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
  shows "REFLECTS[\<lambda>x. is_iterates(L, p(L,x), f(x), g(x), h(x)),

 apply (intro FOL_reflections function_reflections p_reflection
              is_wfrec_reflection iterates_MH_reflection)
 done
 
 
-subsubsection{*The Formula @{term is_eclose_n}, Internalized*}
+subsubsection\<open>The Formula @{term is_eclose_n}, Internalized\<close>
 
 (* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *)
 
 definition
   eclose_n_fm :: "[i,i,i]=>i" where

 apply (simp only: is_eclose_n_def)
 apply (intro FOL_reflections function_reflections is_iterates_reflection) 
 done
 
 
-subsubsection{*Membership in @{term "eclose(A)"}*}
+subsubsection\<open>Membership in @{term "eclose(A)"}\<close>
 
 (* mem_eclose(M,A,l) == 
       \<exists>n[M]. \<exists>eclosen[M]. 
        finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen *)
 definition

 apply (simp only: mem_eclose_def)
 apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
 done
 
 
-subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*}
+subsubsection\<open>The Predicate ``Is @{term "eclose(A)"}''\<close>
 
 (* is_eclose(M,A,Z) == \<forall>l[M]. l \<in> Z \<longleftrightarrow> mem_eclose(M,A,l) *)
 definition
   is_eclose_fm :: "[i,i]=>i" where
     "is_eclose_fm(A,Z) ==

 apply (simp only: is_eclose_def)
 apply (intro FOL_reflections mem_eclose_reflection)
 done
 
 
-subsubsection{*The List Functor, Internalized*}
+subsubsection\<open>The List Functor, Internalized\<close>
 
 definition
   list_functor_fm :: "[i,i,i]=>i" where
 (* "is_list_functor(M,A,X,Z) ==
         \<exists>n1[M]. \<exists>AX[M].

 apply (intro FOL_reflections number1_reflection
              cartprod_reflection sum_reflection)
 done
 
 
-subsubsection{*The Formula @{term is_list_N}, Internalized*}
+subsubsection\<open>The Formula @{term is_list_N}, Internalized\<close>
 
 (* "is_list_N(M,A,n,Z) == 
       \<exists>zero[M]. empty(M,zero) & 
                 is_iterates(M, is_list_functor(M,A), zero, n, Z)" *)
 

              is_iterates_reflection list_functor_reflection) 
 done
 
 
 
-subsubsection{*The Predicate ``Is A List''*}
+subsubsection\<open>The Predicate ``Is A List''\<close>
 
 (* mem_list(M,A,l) == 
       \<exists>n[M]. \<exists>listn[M]. 
        finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
 definition

 apply (simp only: mem_list_def)
 apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
 done
 
 
-subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
+subsubsection\<open>The Predicate ``Is @{term "list(A)"}''\<close>
 
 (* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z \<longleftrightarrow> mem_list(M,A,l) *)
 definition
   is_list_fm :: "[i,i]=>i" where
     "is_list_fm(A,Z) ==

 apply (simp only: is_list_def)
 apply (intro FOL_reflections mem_list_reflection)
 done
 
 
-subsubsection{*The Formula Functor, Internalized*}
+subsubsection\<open>The Formula Functor, Internalized\<close>
 
 definition formula_functor_fm :: "[i,i]=>i" where
 (*     "is_formula_functor(M,X,Z) ==
         \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
            4           3               2       1       0

 apply (intro FOL_reflections omega_reflection
              cartprod_reflection sum_reflection)
 done
 
 
-subsubsection{*The Formula @{term is_formula_N}, Internalized*}
+subsubsection\<open>The Formula @{term is_formula_N}, Internalized\<close>
 
 (*  "is_formula_N(M,n,Z) == 
       \<exists>zero[M]. empty(M,zero) & 
                 is_iterates(M, is_formula_functor(M), zero, n, Z)" *) 
 definition

              is_iterates_reflection formula_functor_reflection) 
 done
 
 
 
-subsubsection{*The Predicate ``Is A Formula''*}
+subsubsection\<open>The Predicate ``Is A Formula''\<close>
 
 (*  mem_formula(M,p) == 
       \<exists>n[M]. \<exists>formn[M]. 
        finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
 definition

 apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
 done
 
 
 
-subsubsection{*The Predicate ``Is @{term "formula"}''*}
+subsubsection\<open>The Predicate ``Is @{term "formula"}''\<close>
 
 (* is_formula(M,Z) == \<forall>p[M]. p \<in> Z \<longleftrightarrow> mem_formula(M,p) *)
 definition
   is_formula_fm :: "i=>i" where
     "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"

 apply (simp only: is_formula_def)
 apply (intro FOL_reflections mem_formula_reflection)
 done
 
 
-subsubsection{*The Operator @{term is_transrec}*}
-
-text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
+subsubsection\<open>The Operator @{term is_transrec}\<close>
+
+text\<open>The three arguments of @{term p} are always 2, 1, 0.  It is buried
    within eight quantifiers!
    We call @{term p} with arguments a, f, z by equating them with 
-  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
+  the corresponding quantified variables with de Bruijn indices 2, 1, 0.\<close>
 
 (* is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
    "is_transrec(M,MH,a,z) == 
       \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
        2       1         0