src/ZF/Constructible/Internalize.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 21404 eb85850d3eb7
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/Internalize.thy
     2     ID: $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 theory Internalize imports L_axioms Datatype_absolute begin
     7 
     8 subsection{*Internalized Forms of Data Structuring Operators*}
     9 
    10 subsubsection{*The Formula @{term is_Inl}, Internalized*}
    11 
    12 (*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
    13 definition
    14   Inl_fm :: "[i,i]=>i" where
    15     "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
    16 
    17 lemma Inl_type [TC]:
    18      "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
    19 by (simp add: Inl_fm_def)
    20 
    21 lemma sats_Inl_fm [simp]:
    22    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
    23     ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(##A, nth(x,env), nth(z,env))"
    24 by (simp add: Inl_fm_def is_Inl_def)
    25 
    26 lemma Inl_iff_sats:
    27       "[| nth(i,env) = x; nth(k,env) = z;
    28           i \<in> nat; k \<in> nat; env \<in> list(A)|]
    29        ==> is_Inl(##A, x, z) <-> sats(A, Inl_fm(i,k), env)"
    30 by simp
    31 
    32 theorem Inl_reflection:
    33      "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
    34                \<lambda>i x. is_Inl(##Lset(i),f(x),h(x))]"
    35 apply (simp only: is_Inl_def)
    36 apply (intro FOL_reflections function_reflections)
    37 done
    38 
    39 
    40 subsubsection{*The Formula @{term is_Inr}, Internalized*}
    41 
    42 (*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
    43 definition
    44   Inr_fm :: "[i,i]=>i" where
    45     "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
    46 
    47 lemma Inr_type [TC]:
    48      "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
    49 by (simp add: Inr_fm_def)
    50 
    51 lemma sats_Inr_fm [simp]:
    52    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
    53     ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(##A, nth(x,env), nth(z,env))"
    54 by (simp add: Inr_fm_def is_Inr_def)
    55 
    56 lemma Inr_iff_sats:
    57       "[| nth(i,env) = x; nth(k,env) = z;
    58           i \<in> nat; k \<in> nat; env \<in> list(A)|]
    59        ==> is_Inr(##A, x, z) <-> sats(A, Inr_fm(i,k), env)"
    60 by simp
    61 
    62 theorem Inr_reflection:
    63      "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
    64                \<lambda>i x. is_Inr(##Lset(i),f(x),h(x))]"
    65 apply (simp only: is_Inr_def)
    66 apply (intro FOL_reflections function_reflections)
    67 done
    68 
    69 
    70 subsubsection{*The Formula @{term is_Nil}, Internalized*}
    71 
    72 (* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
    73 
    74 definition
    75   Nil_fm :: "i=>i" where
    76     "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
    77 
    78 lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
    79 by (simp add: Nil_fm_def)
    80 
    81 lemma sats_Nil_fm [simp]:
    82    "[| x \<in> nat; env \<in> list(A)|]
    83     ==> sats(A, Nil_fm(x), env) <-> is_Nil(##A, nth(x,env))"
    84 by (simp add: Nil_fm_def is_Nil_def)
    85 
    86 lemma Nil_iff_sats:
    87       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
    88        ==> is_Nil(##A, x) <-> sats(A, Nil_fm(i), env)"
    89 by simp
    90 
    91 theorem Nil_reflection:
    92      "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
    93                \<lambda>i x. is_Nil(##Lset(i),f(x))]"
    94 apply (simp only: is_Nil_def)
    95 apply (intro FOL_reflections function_reflections Inl_reflection)
    96 done
    97 
    98 
    99 subsubsection{*The Formula @{term is_Cons}, Internalized*}
   100 
   101 
   102 (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
   103 definition
   104   Cons_fm :: "[i,i,i]=>i" where
   105     "Cons_fm(a,l,Z) ==
   106        Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
   107 
   108 lemma Cons_type [TC]:
   109      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
   110 by (simp add: Cons_fm_def)
   111 
   112 lemma sats_Cons_fm [simp]:
   113    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   114     ==> sats(A, Cons_fm(x,y,z), env) <->
   115        is_Cons(##A, nth(x,env), nth(y,env), nth(z,env))"
   116 by (simp add: Cons_fm_def is_Cons_def)
   117 
   118 lemma Cons_iff_sats:
   119       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   120           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   121        ==>is_Cons(##A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
   122 by simp
   123 
   124 theorem Cons_reflection:
   125      "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
   126                \<lambda>i x. is_Cons(##Lset(i),f(x),g(x),h(x))]"
   127 apply (simp only: is_Cons_def)
   128 apply (intro FOL_reflections pair_reflection Inr_reflection)
   129 done
   130 
   131 subsubsection{*The Formula @{term is_quasilist}, Internalized*}
   132 
   133 (* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
   134 
   135 definition
   136   quasilist_fm :: "i=>i" where
   137     "quasilist_fm(x) ==
   138        Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
   139 
   140 lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
   141 by (simp add: quasilist_fm_def)
   142 
   143 lemma sats_quasilist_fm [simp]:
   144    "[| x \<in> nat; env \<in> list(A)|]
   145     ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(##A, nth(x,env))"
   146 by (simp add: quasilist_fm_def is_quasilist_def)
   147 
   148 lemma quasilist_iff_sats:
   149       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
   150        ==> is_quasilist(##A, x) <-> sats(A, quasilist_fm(i), env)"
   151 by simp
   152 
   153 theorem quasilist_reflection:
   154      "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
   155                \<lambda>i x. is_quasilist(##Lset(i),f(x))]"
   156 apply (simp only: is_quasilist_def)
   157 apply (intro FOL_reflections Nil_reflection Cons_reflection)
   158 done
   159 
   160 
   161 subsection{*Absoluteness for the Function @{term nth}*}
   162 
   163 
   164 subsubsection{*The Formula @{term is_hd}, Internalized*}
   165 
   166 (*   "is_hd(M,xs,H) == 
   167        (is_Nil(M,xs) --> empty(M,H)) &
   168        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
   169        (is_quasilist(M,xs) | empty(M,H))" *)
   170 definition
   171   hd_fm :: "[i,i]=>i" where
   172     "hd_fm(xs,H) == 
   173        And(Implies(Nil_fm(xs), empty_fm(H)),
   174            And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
   175                Or(quasilist_fm(xs), empty_fm(H))))"
   176 
   177 lemma hd_type [TC]:
   178      "[| x \<in> nat; y \<in> nat |] ==> hd_fm(x,y) \<in> formula"
   179 by (simp add: hd_fm_def) 
   180 
   181 lemma sats_hd_fm [simp]:
   182    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   183     ==> sats(A, hd_fm(x,y), env) <-> is_hd(##A, nth(x,env), nth(y,env))"
   184 by (simp add: hd_fm_def is_hd_def)
   185 
   186 lemma hd_iff_sats:
   187       "[| nth(i,env) = x; nth(j,env) = y;
   188           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   189        ==> is_hd(##A, x, y) <-> sats(A, hd_fm(i,j), env)"
   190 by simp
   191 
   192 theorem hd_reflection:
   193      "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)), 
   194                \<lambda>i x. is_hd(##Lset(i),f(x),g(x))]"
   195 apply (simp only: is_hd_def)
   196 apply (intro FOL_reflections Nil_reflection Cons_reflection
   197              quasilist_reflection empty_reflection)  
   198 done
   199 
   200 
   201 subsubsection{*The Formula @{term is_tl}, Internalized*}
   202 
   203 (*     "is_tl(M,xs,T) ==
   204        (is_Nil(M,xs) --> T=xs) &
   205        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
   206        (is_quasilist(M,xs) | empty(M,T))" *)
   207 definition
   208   tl_fm :: "[i,i]=>i" where
   209     "tl_fm(xs,T) ==
   210        And(Implies(Nil_fm(xs), Equal(T,xs)),
   211            And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
   212                Or(quasilist_fm(xs), empty_fm(T))))"
   213 
   214 lemma tl_type [TC]:
   215      "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
   216 by (simp add: tl_fm_def)
   217 
   218 lemma sats_tl_fm [simp]:
   219    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   220     ==> sats(A, tl_fm(x,y), env) <-> is_tl(##A, nth(x,env), nth(y,env))"
   221 by (simp add: tl_fm_def is_tl_def)
   222 
   223 lemma tl_iff_sats:
   224       "[| nth(i,env) = x; nth(j,env) = y;
   225           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   226        ==> is_tl(##A, x, y) <-> sats(A, tl_fm(i,j), env)"
   227 by simp
   228 
   229 theorem tl_reflection:
   230      "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
   231                \<lambda>i x. is_tl(##Lset(i),f(x),g(x))]"
   232 apply (simp only: is_tl_def)
   233 apply (intro FOL_reflections Nil_reflection Cons_reflection
   234              quasilist_reflection empty_reflection)
   235 done
   236 
   237 
   238 subsubsection{*The Operator @{term is_bool_of_o}*}
   239 
   240 (*   is_bool_of_o :: "[i=>o, o, i] => o"
   241    "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" *)
   242 
   243 text{*The formula @{term p} has no free variables.*}
   244 definition
   245   bool_of_o_fm :: "[i, i]=>i" where
   246   "bool_of_o_fm(p,z) == 
   247     Or(And(p,number1_fm(z)),
   248        And(Neg(p),empty_fm(z)))"
   249 
   250 lemma is_bool_of_o_type [TC]:
   251      "[| p \<in> formula; z \<in> nat |] ==> bool_of_o_fm(p,z) \<in> formula"
   252 by (simp add: bool_of_o_fm_def)
   253 
   254 lemma sats_bool_of_o_fm:
   255   assumes p_iff_sats: "P <-> sats(A, p, env)"
   256   shows 
   257       "[|z \<in> nat; env \<in> list(A)|]
   258        ==> sats(A, bool_of_o_fm(p,z), env) <->
   259            is_bool_of_o(##A, P, nth(z,env))"
   260 by (simp add: bool_of_o_fm_def is_bool_of_o_def p_iff_sats [THEN iff_sym])
   261 
   262 lemma is_bool_of_o_iff_sats:
   263   "[| P <-> sats(A, p, env); nth(k,env) = z; k \<in> nat; env \<in> list(A)|]
   264    ==> is_bool_of_o(##A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
   265 by (simp add: sats_bool_of_o_fm)
   266 
   267 theorem bool_of_o_reflection:
   268      "REFLECTS [P(L), \<lambda>i. P(##Lset(i))] ==>
   269       REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
   270                \<lambda>i x. is_bool_of_o(##Lset(i), P(##Lset(i),x), f(x))]"
   271 apply (simp (no_asm) only: is_bool_of_o_def)
   272 apply (intro FOL_reflections function_reflections, assumption+)
   273 done
   274 
   275 
   276 subsection{*More Internalizations*}
   277 
   278 subsubsection{*The Operator @{term is_lambda}*}
   279 
   280 text{*The two arguments of @{term p} are always 1, 0. Remember that
   281  @{term p} will be enclosed by three quantifiers.*}
   282 
   283 (* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
   284     "is_lambda(M, A, is_b, z) == 
   285        \<forall>p[M]. p \<in> z <->
   286         (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
   287 definition
   288   lambda_fm :: "[i, i, i]=>i" where
   289   "lambda_fm(p,A,z) == 
   290     Forall(Iff(Member(0,succ(z)),
   291             Exists(Exists(And(Member(1,A#+3),
   292                            And(pair_fm(1,0,2), p))))))"
   293 
   294 text{*We call @{term p} with arguments x, y by equating them with 
   295   the corresponding quantified variables with de Bruijn indices 1, 0.*}
   296 
   297 lemma is_lambda_type [TC]:
   298      "[| p \<in> formula; x \<in> nat; y \<in> nat |] 
   299       ==> lambda_fm(p,x,y) \<in> formula"
   300 by (simp add: lambda_fm_def) 
   301 
   302 lemma sats_lambda_fm:
   303   assumes is_b_iff_sats: 
   304       "!!a0 a1 a2. 
   305         [|a0\<in>A; a1\<in>A; a2\<in>A|] 
   306         ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
   307   shows 
   308       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   309        ==> sats(A, lambda_fm(p,x,y), env) <-> 
   310            is_lambda(##A, nth(x,env), is_b, nth(y,env))"
   311 by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym]) 
   312 
   313 theorem is_lambda_reflection:
   314   assumes is_b_reflection:
   315     "!!f g h. REFLECTS[\<lambda>x. is_b(L, f(x), g(x), h(x)), 
   316                      \<lambda>i x. is_b(##Lset(i), f(x), g(x), h(x))]"
   317   shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)), 
   318                \<lambda>i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i),x), f(x))]"
   319 apply (simp (no_asm_use) only: is_lambda_def)
   320 apply (intro FOL_reflections is_b_reflection pair_reflection)
   321 done
   322 
   323 subsubsection{*The Operator @{term is_Member}, Internalized*}
   324 
   325 (*    "is_Member(M,x,y,Z) ==
   326 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
   327 definition
   328   Member_fm :: "[i,i,i]=>i" where
   329     "Member_fm(x,y,Z) ==
   330        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   331                       And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
   332 
   333 lemma is_Member_type [TC]:
   334      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Member_fm(x,y,z) \<in> formula"
   335 by (simp add: Member_fm_def)
   336 
   337 lemma sats_Member_fm [simp]:
   338    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   339     ==> sats(A, Member_fm(x,y,z), env) <->
   340         is_Member(##A, nth(x,env), nth(y,env), nth(z,env))"
   341 by (simp add: Member_fm_def is_Member_def)
   342 
   343 lemma Member_iff_sats:
   344       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   345           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   346        ==> is_Member(##A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
   347 by (simp add: sats_Member_fm)
   348 
   349 theorem Member_reflection:
   350      "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
   351                \<lambda>i x. is_Member(##Lset(i),f(x),g(x),h(x))]"
   352 apply (simp only: is_Member_def)
   353 apply (intro FOL_reflections pair_reflection Inl_reflection)
   354 done
   355 
   356 subsubsection{*The Operator @{term is_Equal}, Internalized*}
   357 
   358 (*    "is_Equal(M,x,y,Z) ==
   359 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
   360 definition
   361   Equal_fm :: "[i,i,i]=>i" where
   362     "Equal_fm(x,y,Z) ==
   363        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   364                       And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
   365 
   366 lemma is_Equal_type [TC]:
   367      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Equal_fm(x,y,z) \<in> formula"
   368 by (simp add: Equal_fm_def)
   369 
   370 lemma sats_Equal_fm [simp]:
   371    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   372     ==> sats(A, Equal_fm(x,y,z), env) <->
   373         is_Equal(##A, nth(x,env), nth(y,env), nth(z,env))"
   374 by (simp add: Equal_fm_def is_Equal_def)
   375 
   376 lemma Equal_iff_sats:
   377       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   378           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   379        ==> is_Equal(##A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
   380 by (simp add: sats_Equal_fm)
   381 
   382 theorem Equal_reflection:
   383      "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
   384                \<lambda>i x. is_Equal(##Lset(i),f(x),g(x),h(x))]"
   385 apply (simp only: is_Equal_def)
   386 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
   387 done
   388 
   389 subsubsection{*The Operator @{term is_Nand}, Internalized*}
   390 
   391 (*    "is_Nand(M,x,y,Z) ==
   392 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
   393 definition
   394   Nand_fm :: "[i,i,i]=>i" where
   395     "Nand_fm(x,y,Z) ==
   396        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   397                       And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
   398 
   399 lemma is_Nand_type [TC]:
   400      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Nand_fm(x,y,z) \<in> formula"
   401 by (simp add: Nand_fm_def)
   402 
   403 lemma sats_Nand_fm [simp]:
   404    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   405     ==> sats(A, Nand_fm(x,y,z), env) <->
   406         is_Nand(##A, nth(x,env), nth(y,env), nth(z,env))"
   407 by (simp add: Nand_fm_def is_Nand_def)
   408 
   409 lemma Nand_iff_sats:
   410       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   411           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   412        ==> is_Nand(##A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
   413 by (simp add: sats_Nand_fm)
   414 
   415 theorem Nand_reflection:
   416      "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
   417                \<lambda>i x. is_Nand(##Lset(i),f(x),g(x),h(x))]"
   418 apply (simp only: is_Nand_def)
   419 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
   420 done
   421 
   422 subsubsection{*The Operator @{term is_Forall}, Internalized*}
   423 
   424 (* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
   425 definition
   426   Forall_fm :: "[i,i]=>i" where
   427     "Forall_fm(x,Z) ==
   428        Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
   429 
   430 lemma is_Forall_type [TC]:
   431      "[| x \<in> nat; y \<in> nat |] ==> Forall_fm(x,y) \<in> formula"
   432 by (simp add: Forall_fm_def)
   433 
   434 lemma sats_Forall_fm [simp]:
   435    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   436     ==> sats(A, Forall_fm(x,y), env) <->
   437         is_Forall(##A, nth(x,env), nth(y,env))"
   438 by (simp add: Forall_fm_def is_Forall_def)
   439 
   440 lemma Forall_iff_sats:
   441       "[| nth(i,env) = x; nth(j,env) = y; 
   442           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   443        ==> is_Forall(##A, x, y) <-> sats(A, Forall_fm(i,j), env)"
   444 by (simp add: sats_Forall_fm)
   445 
   446 theorem Forall_reflection:
   447      "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
   448                \<lambda>i x. is_Forall(##Lset(i),f(x),g(x))]"
   449 apply (simp only: is_Forall_def)
   450 apply (intro FOL_reflections pair_reflection Inr_reflection)
   451 done
   452 
   453 
   454 subsubsection{*The Operator @{term is_and}, Internalized*}
   455 
   456 (* is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
   457                        (~number1(M,a) & empty(M,z)) *)
   458 definition
   459   and_fm :: "[i,i,i]=>i" where
   460     "and_fm(a,b,z) ==
   461        Or(And(number1_fm(a), Equal(z,b)),
   462           And(Neg(number1_fm(a)),empty_fm(z)))"
   463 
   464 lemma is_and_type [TC]:
   465      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> and_fm(x,y,z) \<in> formula"
   466 by (simp add: and_fm_def)
   467 
   468 lemma sats_and_fm [simp]:
   469    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   470     ==> sats(A, and_fm(x,y,z), env) <->
   471         is_and(##A, nth(x,env), nth(y,env), nth(z,env))"
   472 by (simp add: and_fm_def is_and_def)
   473 
   474 lemma is_and_iff_sats:
   475       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   476           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   477        ==> is_and(##A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
   478 by simp
   479 
   480 theorem is_and_reflection:
   481      "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
   482                \<lambda>i x. is_and(##Lset(i),f(x),g(x),h(x))]"
   483 apply (simp only: is_and_def)
   484 apply (intro FOL_reflections function_reflections)
   485 done
   486 
   487 
   488 subsubsection{*The Operator @{term is_or}, Internalized*}
   489 
   490 (* is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
   491                      (~number1(M,a) & z=b) *)
   492 
   493 definition
   494   or_fm :: "[i,i,i]=>i" where
   495     "or_fm(a,b,z) ==
   496        Or(And(number1_fm(a), number1_fm(z)),
   497           And(Neg(number1_fm(a)), Equal(z,b)))"
   498 
   499 lemma is_or_type [TC]:
   500      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> or_fm(x,y,z) \<in> formula"
   501 by (simp add: or_fm_def)
   502 
   503 lemma sats_or_fm [simp]:
   504    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   505     ==> sats(A, or_fm(x,y,z), env) <->
   506         is_or(##A, nth(x,env), nth(y,env), nth(z,env))"
   507 by (simp add: or_fm_def is_or_def)
   508 
   509 lemma is_or_iff_sats:
   510       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   511           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   512        ==> is_or(##A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
   513 by simp
   514 
   515 theorem is_or_reflection:
   516      "REFLECTS[\<lambda>x. is_or(L,f(x),g(x),h(x)),
   517                \<lambda>i x. is_or(##Lset(i),f(x),g(x),h(x))]"
   518 apply (simp only: is_or_def)
   519 apply (intro FOL_reflections function_reflections)
   520 done
   521 
   522 
   523 
   524 subsubsection{*The Operator @{term is_not}, Internalized*}
   525 
   526 (* is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
   527                      (~number1(M,a) & number1(M,z)) *)
   528 definition
   529   not_fm :: "[i,i]=>i" where
   530     "not_fm(a,z) ==
   531        Or(And(number1_fm(a), empty_fm(z)),
   532           And(Neg(number1_fm(a)), number1_fm(z)))"
   533 
   534 lemma is_not_type [TC]:
   535      "[| x \<in> nat; z \<in> nat |] ==> not_fm(x,z) \<in> formula"
   536 by (simp add: not_fm_def)
   537 
   538 lemma sats_is_not_fm [simp]:
   539    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
   540     ==> sats(A, not_fm(x,z), env) <-> is_not(##A, nth(x,env), nth(z,env))"
   541 by (simp add: not_fm_def is_not_def)
   542 
   543 lemma is_not_iff_sats:
   544       "[| nth(i,env) = x; nth(k,env) = z;
   545           i \<in> nat; k \<in> nat; env \<in> list(A)|]
   546        ==> is_not(##A, x, z) <-> sats(A, not_fm(i,k), env)"
   547 by simp
   548 
   549 theorem is_not_reflection:
   550      "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
   551                \<lambda>i x. is_not(##Lset(i),f(x),g(x))]"
   552 apply (simp only: is_not_def)
   553 apply (intro FOL_reflections function_reflections)
   554 done
   555 
   556 
   557 lemmas extra_reflections = 
   558     Inl_reflection Inr_reflection Nil_reflection Cons_reflection
   559     quasilist_reflection hd_reflection tl_reflection bool_of_o_reflection
   560     is_lambda_reflection Member_reflection Equal_reflection Nand_reflection
   561     Forall_reflection is_and_reflection is_or_reflection is_not_reflection
   562 
   563 subsection{*Well-Founded Recursion!*}
   564 
   565 subsubsection{*The Operator @{term M_is_recfun}*}
   566 
   567 text{*Alternative definition, minimizing nesting of quantifiers around MH*}
   568 lemma M_is_recfun_iff:
   569    "M_is_recfun(M,MH,r,a,f) <->
   570     (\<forall>z[M]. z \<in> f <-> 
   571      (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M]. 
   572              MH(x, f_r_sx, y) & pair(M,x,y,z) &
   573              (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. 
   574                 pair(M,x,a,xa) & upair(M,x,x,sx) &
   575                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   576                xa \<in> r)))"
   577 apply (simp add: M_is_recfun_def)
   578 apply (rule rall_cong, blast) 
   579 done
   580 
   581 
   582 (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
   583    "M_is_recfun(M,MH,r,a,f) ==
   584      \<forall>z[M]. z \<in> f <->
   585                2      1           0
   586 new def     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M]. 
   587              MH(x, f_r_sx, y) & pair(M,x,y,z) &
   588              (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. 
   589                 pair(M,x,a,xa) & upair(M,x,x,sx) &
   590                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   591                xa \<in> r)"
   592 *)
   593 
   594 text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
   595 definition
   596   is_recfun_fm :: "[i, i, i, i]=>i" where
   597   "is_recfun_fm(p,r,a,f) == 
   598    Forall(Iff(Member(0,succ(f)),
   599     Exists(Exists(Exists(
   600      And(p, 
   601       And(pair_fm(2,0,3),
   602        Exists(Exists(Exists(
   603 	And(pair_fm(5,a#+7,2),
   604 	 And(upair_fm(5,5,1),
   605 	  And(pre_image_fm(r#+7,1,0),
   606 	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
   607 
   608 lemma is_recfun_type [TC]:
   609      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   610       ==> is_recfun_fm(p,x,y,z) \<in> formula"
   611 by (simp add: is_recfun_fm_def)
   612 
   613 
   614 lemma sats_is_recfun_fm:
   615   assumes MH_iff_sats: 
   616       "!!a0 a1 a2 a3. 
   617         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|] 
   618         ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
   619   shows 
   620       "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   621        ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
   622            M_is_recfun(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
   623 by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
   624 
   625 lemma is_recfun_iff_sats:
   626   assumes MH_iff_sats: 
   627       "!!a0 a1 a2 a3. 
   628         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|] 
   629         ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
   630   shows
   631   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   632       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   633    ==> M_is_recfun(##A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
   634 by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) 
   635 
   636 text{*The additional variable in the premise, namely @{term f'}, is essential.
   637 It lets @{term MH} depend upon @{term x}, which seems often necessary.
   638 The same thing occurs in @{text is_wfrec_reflection}.*}
   639 theorem is_recfun_reflection:
   640   assumes MH_reflection:
   641     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
   642                      \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   643   shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), 
   644              \<lambda>i x. M_is_recfun(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
   645 apply (simp (no_asm_use) only: M_is_recfun_def)
   646 apply (intro FOL_reflections function_reflections
   647              restriction_reflection MH_reflection)
   648 done
   649 
   650 subsubsection{*The Operator @{term is_wfrec}*}
   651 
   652 text{*The three arguments of @{term p} are always 2, 1, 0;
   653       @{term p} is enclosed by 5 quantifiers.*}
   654 
   655 (* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
   656     "is_wfrec(M,MH,r,a,z) == 
   657       \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
   658 definition
   659   is_wfrec_fm :: "[i, i, i, i]=>i" where
   660   "is_wfrec_fm(p,r,a,z) == 
   661     Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
   662            Exists(Exists(Exists(Exists(
   663              And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
   664 
   665 text{*We call @{term p} with arguments a, f, z by equating them with 
   666   the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
   667 
   668 text{*There's an additional existential quantifier to ensure that the
   669       environments in both calls to MH have the same length.*}
   670 
   671 lemma is_wfrec_type [TC]:
   672      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   673       ==> is_wfrec_fm(p,x,y,z) \<in> formula"
   674 by (simp add: is_wfrec_fm_def) 
   675 
   676 lemma sats_is_wfrec_fm:
   677   assumes MH_iff_sats: 
   678       "!!a0 a1 a2 a3 a4. 
   679         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|] 
   680         ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
   681   shows 
   682       "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
   683        ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> 
   684            is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
   685 apply (frule_tac x=z in lt_length_in_nat, assumption)  
   686 apply (frule lt_length_in_nat, assumption)  
   687 apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) 
   688 done
   689 
   690 
   691 lemma is_wfrec_iff_sats:
   692   assumes MH_iff_sats: 
   693       "!!a0 a1 a2 a3 a4. 
   694         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|] 
   695         ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
   696   shows
   697   "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   698       i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
   699    ==> is_wfrec(##A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" 
   700 by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
   701 
   702 theorem is_wfrec_reflection:
   703   assumes MH_reflection:
   704     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
   705                      \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   706   shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), 
   707                \<lambda>i x. is_wfrec(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
   708 apply (simp (no_asm_use) only: is_wfrec_def)
   709 apply (intro FOL_reflections MH_reflection is_recfun_reflection)
   710 done
   711 
   712 
   713 subsection{*For Datatypes*}
   714 
   715 subsubsection{*Binary Products, Internalized*}
   716 
   717 definition
   718   cartprod_fm :: "[i,i,i]=>i" where
   719 (* "cartprod(M,A,B,z) ==
   720         \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   721     "cartprod_fm(A,B,z) ==
   722        Forall(Iff(Member(0,succ(z)),
   723                   Exists(And(Member(0,succ(succ(A))),
   724                          Exists(And(Member(0,succ(succ(succ(B)))),
   725                                     pair_fm(1,0,2)))))))"
   726 
   727 lemma cartprod_type [TC]:
   728      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
   729 by (simp add: cartprod_fm_def)
   730 
   731 lemma sats_cartprod_fm [simp]:
   732    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   733     ==> sats(A, cartprod_fm(x,y,z), env) <->
   734         cartprod(##A, nth(x,env), nth(y,env), nth(z,env))"
   735 by (simp add: cartprod_fm_def cartprod_def)
   736 
   737 lemma cartprod_iff_sats:
   738       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   739           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   740        ==> cartprod(##A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
   741 by (simp add: sats_cartprod_fm)
   742 
   743 theorem cartprod_reflection:
   744      "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
   745                \<lambda>i x. cartprod(##Lset(i),f(x),g(x),h(x))]"
   746 apply (simp only: cartprod_def)
   747 apply (intro FOL_reflections pair_reflection)
   748 done
   749 
   750 
   751 subsubsection{*Binary Sums, Internalized*}
   752 
   753 (* "is_sum(M,A,B,Z) ==
   754        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
   755          3      2       1        0
   756        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   757        cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   758 definition
   759   sum_fm :: "[i,i,i]=>i" where
   760     "sum_fm(A,B,Z) ==
   761        Exists(Exists(Exists(Exists(
   762         And(number1_fm(2),
   763             And(cartprod_fm(2,A#+4,3),
   764                 And(upair_fm(2,2,1),
   765                     And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
   766 
   767 lemma sum_type [TC]:
   768      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
   769 by (simp add: sum_fm_def)
   770 
   771 lemma sats_sum_fm [simp]:
   772    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   773     ==> sats(A, sum_fm(x,y,z), env) <->
   774         is_sum(##A, nth(x,env), nth(y,env), nth(z,env))"
   775 by (simp add: sum_fm_def is_sum_def)
   776 
   777 lemma sum_iff_sats:
   778       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   779           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   780        ==> is_sum(##A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
   781 by simp
   782 
   783 theorem sum_reflection:
   784      "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
   785                \<lambda>i x. is_sum(##Lset(i),f(x),g(x),h(x))]"
   786 apply (simp only: is_sum_def)
   787 apply (intro FOL_reflections function_reflections cartprod_reflection)
   788 done
   789 
   790 
   791 subsubsection{*The Operator @{term quasinat}*}
   792 
   793 (* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
   794 definition
   795   quasinat_fm :: "i=>i" where
   796     "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
   797 
   798 lemma quasinat_type [TC]:
   799      "x \<in> nat ==> quasinat_fm(x) \<in> formula"
   800 by (simp add: quasinat_fm_def)
   801 
   802 lemma sats_quasinat_fm [simp]:
   803    "[| x \<in> nat; env \<in> list(A)|]
   804     ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(##A, nth(x,env))"
   805 by (simp add: quasinat_fm_def is_quasinat_def)
   806 
   807 lemma quasinat_iff_sats:
   808       "[| nth(i,env) = x; nth(j,env) = y;
   809           i \<in> nat; env \<in> list(A)|]
   810        ==> is_quasinat(##A, x) <-> sats(A, quasinat_fm(i), env)"
   811 by simp
   812 
   813 theorem quasinat_reflection:
   814      "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
   815                \<lambda>i x. is_quasinat(##Lset(i),f(x))]"
   816 apply (simp only: is_quasinat_def)
   817 apply (intro FOL_reflections function_reflections)
   818 done
   819 
   820 
   821 subsubsection{*The Operator @{term is_nat_case}*}
   822 text{*I could not get it to work with the more natural assumption that 
   823  @{term is_b} takes two arguments.  Instead it must be a formula where 1 and 0
   824  stand for @{term m} and @{term b}, respectively.*}
   825 
   826 (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   827     "is_nat_case(M, a, is_b, k, z) ==
   828        (empty(M,k) --> z=a) &
   829        (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   830        (is_quasinat(M,k) | empty(M,z))" *)
   831 text{*The formula @{term is_b} has free variables 1 and 0.*}
   832 definition
   833   is_nat_case_fm :: "[i, i, i, i]=>i" where
   834  "is_nat_case_fm(a,is_b,k,z) == 
   835     And(Implies(empty_fm(k), Equal(z,a)),
   836         And(Forall(Implies(succ_fm(0,succ(k)), 
   837                    Forall(Implies(Equal(0,succ(succ(z))), is_b)))),
   838             Or(quasinat_fm(k), empty_fm(z))))"
   839 
   840 lemma is_nat_case_type [TC]:
   841      "[| is_b \<in> formula;  
   842          x \<in> nat; y \<in> nat; z \<in> nat |] 
   843       ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   844 by (simp add: is_nat_case_fm_def)
   845 
   846 lemma sats_is_nat_case_fm:
   847   assumes is_b_iff_sats: 
   848       "!!a. a \<in> A ==> is_b(a,nth(z, env)) <-> 
   849                       sats(A, p, Cons(nth(z,env), Cons(a, env)))"
   850   shows 
   851       "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   852        ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
   853            is_nat_case(##A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   854 apply (frule lt_length_in_nat, assumption)
   855 apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
   856 done
   857 
   858 lemma is_nat_case_iff_sats:
   859   "[| (!!a. a \<in> A ==> is_b(a,z) <->
   860                       sats(A, p, Cons(z, Cons(a,env))));
   861       nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   862       i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   863    ==> is_nat_case(##A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
   864 by (simp add: sats_is_nat_case_fm [of A is_b])
   865 
   866 
   867 text{*The second argument of @{term is_b} gives it direct access to @{term x},
   868   which is essential for handling free variable references.  Without this
   869   argument, we cannot prove reflection for @{term iterates_MH}.*}
   870 theorem is_nat_case_reflection:
   871   assumes is_b_reflection:
   872     "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
   873                      \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x))]"
   874   shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
   875                \<lambda>i x. is_nat_case(##Lset(i), f(x), is_b(##Lset(i), x), g(x), h(x))]"
   876 apply (simp (no_asm_use) only: is_nat_case_def)
   877 apply (intro FOL_reflections function_reflections
   878              restriction_reflection is_b_reflection quasinat_reflection)
   879 done
   880 
   881 
   882 subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
   883 
   884 (*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
   885    "iterates_MH(M,isF,v,n,g,z) ==
   886         is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   887                     n, z)" *)
   888 definition
   889   iterates_MH_fm :: "[i, i, i, i, i]=>i" where
   890  "iterates_MH_fm(isF,v,n,g,z) == 
   891     is_nat_case_fm(v, 
   892       Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), 
   893                      Forall(Implies(Equal(0,2), isF)))), 
   894       n, z)"
   895 
   896 lemma iterates_MH_type [TC]:
   897      "[| p \<in> formula;  
   898          v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   899       ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   900 by (simp add: iterates_MH_fm_def)
   901 
   902 lemma sats_iterates_MH_fm:
   903   assumes is_F_iff_sats:
   904       "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   905               ==> is_F(a,b) <->
   906                   sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   907   shows 
   908       "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   909        ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
   910            iterates_MH(##A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   911 apply (frule lt_length_in_nat, assumption)  
   912 apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   913               is_F_iff_sats [symmetric])
   914 apply (rule is_nat_case_cong) 
   915 apply (simp_all add: setclass_def)
   916 done
   917 
   918 lemma iterates_MH_iff_sats:
   919   assumes is_F_iff_sats:
   920       "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   921               ==> is_F(a,b) <->
   922                   sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   923   shows 
   924   "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   925       i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   926    ==> iterates_MH(##A, is_F, v, x, y, z) <->
   927        sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   928 by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) 
   929 
   930 text{*The second argument of @{term p} gives it direct access to @{term x},
   931   which is essential for handling free variable references.  Without this
   932   argument, we cannot prove reflection for @{term list_N}.*}
   933 theorem iterates_MH_reflection:
   934   assumes p_reflection:
   935     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
   936                      \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
   937  shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
   938                \<lambda>i x. iterates_MH(##Lset(i), p(##Lset(i),x), e(x), f(x), g(x), h(x))]"
   939 apply (simp (no_asm_use) only: iterates_MH_def)
   940 apply (intro FOL_reflections function_reflections is_nat_case_reflection
   941              restriction_reflection p_reflection)
   942 done
   943 
   944 
   945 subsubsection{*The Operator @{term is_iterates}*}
   946 
   947 text{*The three arguments of @{term p} are always 2, 1, 0;
   948       @{term p} is enclosed by 9 (??) quantifiers.*}
   949 
   950 (*    "is_iterates(M,isF,v,n,Z) == 
   951       \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   952        1       0       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*)
   953 
   954 definition
   955   is_iterates_fm :: "[i, i, i, i]=>i" where
   956   "is_iterates_fm(p,v,n,Z) == 
   957      Exists(Exists(
   958       And(succ_fm(n#+2,1),
   959        And(Memrel_fm(1,0),
   960               is_wfrec_fm(iterates_MH_fm(p, v#+7, 2, 1, 0), 
   961                           0, n#+2, Z#+2)))))"
   962 
   963 text{*We call @{term p} with arguments a, f, z by equating them with 
   964   the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
   965 
   966 
   967 lemma is_iterates_type [TC]:
   968      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   969       ==> is_iterates_fm(p,x,y,z) \<in> formula"
   970 by (simp add: is_iterates_fm_def) 
   971 
   972 lemma sats_is_iterates_fm:
   973   assumes is_F_iff_sats:
   974       "!!a b c d e f g h i j k. 
   975               [| a \<in> A; b \<in> A; c \<in> A; d \<in> A; e \<in> A; f \<in> A; 
   976                  g \<in> A; h \<in> A; i \<in> A; j \<in> A; k \<in> A|]
   977               ==> is_F(a,b) <->
   978                   sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f, 
   979                       Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))"
   980   shows 
   981       "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
   982        ==> sats(A, is_iterates_fm(p,x,y,z), env) <->
   983            is_iterates(##A, is_F, nth(x,env), nth(y,env), nth(z,env))"
   984 apply (frule_tac x=z in lt_length_in_nat, assumption)  
   985 apply (frule lt_length_in_nat, assumption)  
   986 apply (simp add: is_iterates_fm_def is_iterates_def sats_is_nat_case_fm 
   987               is_F_iff_sats [symmetric] sats_is_wfrec_fm sats_iterates_MH_fm)
   988 done
   989 
   990 
   991 lemma is_iterates_iff_sats:
   992   assumes is_F_iff_sats:
   993       "!!a b c d e f g h i j k. 
   994               [| a \<in> A; b \<in> A; c \<in> A; d \<in> A; e \<in> A; f \<in> A; 
   995                  g \<in> A; h \<in> A; i \<in> A; j \<in> A; k \<in> A|]
   996               ==> is_F(a,b) <->
   997                   sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f, 
   998                       Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))"
   999   shows 
  1000   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  1001       i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
  1002    ==> is_iterates(##A, is_F, x, y, z) <->
  1003        sats(A, is_iterates_fm(p,i,j,k), env)"
  1004 by (simp add: sats_is_iterates_fm [OF is_F_iff_sats]) 
  1005 
  1006 text{*The second argument of @{term p} gives it direct access to @{term x},
  1007   which is essential for handling free variable references.  Without this
  1008   argument, we cannot prove reflection for @{term list_N}.*}
  1009 theorem is_iterates_reflection:
  1010   assumes p_reflection:
  1011     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
  1012                      \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
  1013  shows "REFLECTS[\<lambda>x. is_iterates(L, p(L,x), f(x), g(x), h(x)),
  1014                \<lambda>i x. is_iterates(##Lset(i), p(##Lset(i),x), f(x), g(x), h(x))]"
  1015 apply (simp (no_asm_use) only: is_iterates_def)
  1016 apply (intro FOL_reflections function_reflections p_reflection
  1017              is_wfrec_reflection iterates_MH_reflection)
  1018 done
  1019 
  1020 
  1021 subsubsection{*The Formula @{term is_eclose_n}, Internalized*}
  1022 
  1023 (* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *)
  1024 
  1025 definition
  1026   eclose_n_fm :: "[i,i,i]=>i" where
  1027   "eclose_n_fm(A,n,Z) == is_iterates_fm(big_union_fm(1,0), A, n, Z)"
  1028 
  1029 lemma eclose_n_fm_type [TC]:
  1030  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> eclose_n_fm(x,y,z) \<in> formula"
  1031 by (simp add: eclose_n_fm_def)
  1032 
  1033 lemma sats_eclose_n_fm [simp]:
  1034    "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
  1035     ==> sats(A, eclose_n_fm(x,y,z), env) <->
  1036         is_eclose_n(##A, nth(x,env), nth(y,env), nth(z,env))"
  1037 apply (frule_tac x=z in lt_length_in_nat, assumption)  
  1038 apply (frule_tac x=y in lt_length_in_nat, assumption)  
  1039 apply (simp add: eclose_n_fm_def is_eclose_n_def 
  1040                  sats_is_iterates_fm) 
  1041 done
  1042 
  1043 lemma eclose_n_iff_sats:
  1044       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1045           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
  1046        ==> is_eclose_n(##A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
  1047 by (simp add: sats_eclose_n_fm)
  1048 
  1049 theorem eclose_n_reflection:
  1050      "REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),  
  1051                \<lambda>i x. is_eclose_n(##Lset(i), f(x), g(x), h(x))]"
  1052 apply (simp only: is_eclose_n_def)
  1053 apply (intro FOL_reflections function_reflections is_iterates_reflection) 
  1054 done
  1055 
  1056 
  1057 subsubsection{*Membership in @{term "eclose(A)"}*}
  1058 
  1059 (* mem_eclose(M,A,l) == 
  1060       \<exists>n[M]. \<exists>eclosen[M]. 
  1061        finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen *)
  1062 definition
  1063   mem_eclose_fm :: "[i,i]=>i" where
  1064     "mem_eclose_fm(x,y) ==
  1065        Exists(Exists(
  1066          And(finite_ordinal_fm(1),
  1067            And(eclose_n_fm(x#+2,1,0), Member(y#+2,0)))))"
  1068 
  1069 lemma mem_eclose_type [TC]:
  1070      "[| x \<in> nat; y \<in> nat |] ==> mem_eclose_fm(x,y) \<in> formula"
  1071 by (simp add: mem_eclose_fm_def)
  1072 
  1073 lemma sats_mem_eclose_fm [simp]:
  1074    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1075     ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(##A, nth(x,env), nth(y,env))"
  1076 by (simp add: mem_eclose_fm_def mem_eclose_def)
  1077 
  1078 lemma mem_eclose_iff_sats:
  1079       "[| nth(i,env) = x; nth(j,env) = y;
  1080           i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1081        ==> mem_eclose(##A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
  1082 by simp
  1083 
  1084 theorem mem_eclose_reflection:
  1085      "REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
  1086                \<lambda>i x. mem_eclose(##Lset(i),f(x),g(x))]"
  1087 apply (simp only: mem_eclose_def)
  1088 apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
  1089 done
  1090 
  1091 
  1092 subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*}
  1093 
  1094 (* is_eclose(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_eclose(M,A,l) *)
  1095 definition
  1096   is_eclose_fm :: "[i,i]=>i" where
  1097     "is_eclose_fm(A,Z) ==
  1098        Forall(Iff(Member(0,succ(Z)), mem_eclose_fm(succ(A),0)))"
  1099 
  1100 lemma is_eclose_type [TC]:
  1101      "[| x \<in> nat; y \<in> nat |] ==> is_eclose_fm(x,y) \<in> formula"
  1102 by (simp add: is_eclose_fm_def)
  1103 
  1104 lemma sats_is_eclose_fm [simp]:
  1105    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1106     ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(##A, nth(x,env), nth(y,env))"
  1107 by (simp add: is_eclose_fm_def is_eclose_def)
  1108 
  1109 lemma is_eclose_iff_sats:
  1110       "[| nth(i,env) = x; nth(j,env) = y;
  1111           i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1112        ==> is_eclose(##A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
  1113 by simp
  1114 
  1115 theorem is_eclose_reflection:
  1116      "REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
  1117                \<lambda>i x. is_eclose(##Lset(i),f(x),g(x))]"
  1118 apply (simp only: is_eclose_def)
  1119 apply (intro FOL_reflections mem_eclose_reflection)
  1120 done
  1121 
  1122 
  1123 subsubsection{*The List Functor, Internalized*}
  1124 
  1125 definition
  1126   list_functor_fm :: "[i,i,i]=>i" where
  1127 (* "is_list_functor(M,A,X,Z) ==
  1128         \<exists>n1[M]. \<exists>AX[M].
  1129          number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
  1130     "list_functor_fm(A,X,Z) ==
  1131        Exists(Exists(
  1132         And(number1_fm(1),
  1133             And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
  1134 
  1135 lemma list_functor_type [TC]:
  1136      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
  1137 by (simp add: list_functor_fm_def)
  1138 
  1139 lemma sats_list_functor_fm [simp]:
  1140    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1141     ==> sats(A, list_functor_fm(x,y,z), env) <->
  1142         is_list_functor(##A, nth(x,env), nth(y,env), nth(z,env))"
  1143 by (simp add: list_functor_fm_def is_list_functor_def)
  1144 
  1145 lemma list_functor_iff_sats:
  1146   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1147       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1148    ==> is_list_functor(##A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
  1149 by simp
  1150 
  1151 theorem list_functor_reflection:
  1152      "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
  1153                \<lambda>i x. is_list_functor(##Lset(i),f(x),g(x),h(x))]"
  1154 apply (simp only: is_list_functor_def)
  1155 apply (intro FOL_reflections number1_reflection
  1156              cartprod_reflection sum_reflection)
  1157 done
  1158 
  1159 
  1160 subsubsection{*The Formula @{term is_list_N}, Internalized*}
  1161 
  1162 (* "is_list_N(M,A,n,Z) == 
  1163       \<exists>zero[M]. empty(M,zero) & 
  1164                 is_iterates(M, is_list_functor(M,A), zero, n, Z)" *)
  1165 
  1166 definition
  1167   list_N_fm :: "[i,i,i]=>i" where
  1168   "list_N_fm(A,n,Z) == 
  1169      Exists(
  1170        And(empty_fm(0),
  1171            is_iterates_fm(list_functor_fm(A#+9#+3,1,0), 0, n#+1, Z#+1)))"
  1172 
  1173 lemma list_N_fm_type [TC]:
  1174  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
  1175 by (simp add: list_N_fm_def)
  1176 
  1177 lemma sats_list_N_fm [simp]:
  1178    "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
  1179     ==> sats(A, list_N_fm(x,y,z), env) <->
  1180         is_list_N(##A, nth(x,env), nth(y,env), nth(z,env))"
  1181 apply (frule_tac x=z in lt_length_in_nat, assumption)  
  1182 apply (frule_tac x=y in lt_length_in_nat, assumption)  
  1183 apply (simp add: list_N_fm_def is_list_N_def sats_is_iterates_fm) 
  1184 done
  1185 
  1186 lemma list_N_iff_sats:
  1187       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1188           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
  1189        ==> is_list_N(##A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
  1190 by (simp add: sats_list_N_fm)
  1191 
  1192 theorem list_N_reflection:
  1193      "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),  
  1194                \<lambda>i x. is_list_N(##Lset(i), f(x), g(x), h(x))]"
  1195 apply (simp only: is_list_N_def)
  1196 apply (intro FOL_reflections function_reflections 
  1197              is_iterates_reflection list_functor_reflection) 
  1198 done
  1199 
  1200 
  1201 
  1202 subsubsection{*The Predicate ``Is A List''*}
  1203 
  1204 (* mem_list(M,A,l) == 
  1205       \<exists>n[M]. \<exists>listn[M]. 
  1206        finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
  1207 definition
  1208   mem_list_fm :: "[i,i]=>i" where
  1209     "mem_list_fm(x,y) ==
  1210        Exists(Exists(
  1211          And(finite_ordinal_fm(1),
  1212            And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))"
  1213 
  1214 lemma mem_list_type [TC]:
  1215      "[| x \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
  1216 by (simp add: mem_list_fm_def)
  1217 
  1218 lemma sats_mem_list_fm [simp]:
  1219    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1220     ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(##A, nth(x,env), nth(y,env))"
  1221 by (simp add: mem_list_fm_def mem_list_def)
  1222 
  1223 lemma mem_list_iff_sats:
  1224       "[| nth(i,env) = x; nth(j,env) = y;
  1225           i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1226        ==> mem_list(##A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
  1227 by simp
  1228 
  1229 theorem mem_list_reflection:
  1230      "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
  1231                \<lambda>i x. mem_list(##Lset(i),f(x),g(x))]"
  1232 apply (simp only: mem_list_def)
  1233 apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
  1234 done
  1235 
  1236 
  1237 subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
  1238 
  1239 (* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
  1240 definition
  1241   is_list_fm :: "[i,i]=>i" where
  1242     "is_list_fm(A,Z) ==
  1243        Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
  1244 
  1245 lemma is_list_type [TC]:
  1246      "[| x \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
  1247 by (simp add: is_list_fm_def)
  1248 
  1249 lemma sats_is_list_fm [simp]:
  1250    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1251     ==> sats(A, is_list_fm(x,y), env) <-> is_list(##A, nth(x,env), nth(y,env))"
  1252 by (simp add: is_list_fm_def is_list_def)
  1253 
  1254 lemma is_list_iff_sats:
  1255       "[| nth(i,env) = x; nth(j,env) = y;
  1256           i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1257        ==> is_list(##A, x, y) <-> sats(A, is_list_fm(i,j), env)"
  1258 by simp
  1259 
  1260 theorem is_list_reflection:
  1261      "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
  1262                \<lambda>i x. is_list(##Lset(i),f(x),g(x))]"
  1263 apply (simp only: is_list_def)
  1264 apply (intro FOL_reflections mem_list_reflection)
  1265 done
  1266 
  1267 
  1268 subsubsection{*The Formula Functor, Internalized*}
  1269 
  1270 definition formula_functor_fm :: "[i,i]=>i" where
  1271 (*     "is_formula_functor(M,X,Z) ==
  1272         \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
  1273            4           3               2       1       0
  1274           omega(M,nat') & cartprod(M,nat',nat',natnat) &
  1275           is_sum(M,natnat,natnat,natnatsum) &
  1276           cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
  1277           is_sum(M,natnatsum,X3,Z)" *)
  1278     "formula_functor_fm(X,Z) ==
  1279        Exists(Exists(Exists(Exists(Exists(
  1280         And(omega_fm(4),
  1281          And(cartprod_fm(4,4,3),
  1282           And(sum_fm(3,3,2),
  1283            And(cartprod_fm(X#+5,X#+5,1),
  1284             And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))"
  1285 
  1286 lemma formula_functor_type [TC]:
  1287      "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
  1288 by (simp add: formula_functor_fm_def)
  1289 
  1290 lemma sats_formula_functor_fm [simp]:
  1291    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1292     ==> sats(A, formula_functor_fm(x,y), env) <->
  1293         is_formula_functor(##A, nth(x,env), nth(y,env))"
  1294 by (simp add: formula_functor_fm_def is_formula_functor_def)
  1295 
  1296 lemma formula_functor_iff_sats:
  1297   "[| nth(i,env) = x; nth(j,env) = y;
  1298       i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1299    ==> is_formula_functor(##A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
  1300 by simp
  1301 
  1302 theorem formula_functor_reflection:
  1303      "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
  1304                \<lambda>i x. is_formula_functor(##Lset(i),f(x),g(x))]"
  1305 apply (simp only: is_formula_functor_def)
  1306 apply (intro FOL_reflections omega_reflection
  1307              cartprod_reflection sum_reflection)
  1308 done
  1309 
  1310 
  1311 subsubsection{*The Formula @{term is_formula_N}, Internalized*}
  1312 
  1313 (*  "is_formula_N(M,n,Z) == 
  1314       \<exists>zero[M]. empty(M,zero) & 
  1315                 is_iterates(M, is_formula_functor(M), zero, n, Z)" *) 
  1316 definition
  1317   formula_N_fm :: "[i,i]=>i" where
  1318   "formula_N_fm(n,Z) == 
  1319      Exists(
  1320        And(empty_fm(0),
  1321            is_iterates_fm(formula_functor_fm(1,0), 0, n#+1, Z#+1)))"
  1322 
  1323 lemma formula_N_fm_type [TC]:
  1324  "[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
  1325 by (simp add: formula_N_fm_def)
  1326 
  1327 lemma sats_formula_N_fm [simp]:
  1328    "[| x < length(env); y < length(env); env \<in> list(A)|]
  1329     ==> sats(A, formula_N_fm(x,y), env) <->
  1330         is_formula_N(##A, nth(x,env), nth(y,env))"
  1331 apply (frule_tac x=y in lt_length_in_nat, assumption)  
  1332 apply (frule lt_length_in_nat, assumption)  
  1333 apply (simp add: formula_N_fm_def is_formula_N_def sats_is_iterates_fm) 
  1334 done
  1335 
  1336 lemma formula_N_iff_sats:
  1337       "[| nth(i,env) = x; nth(j,env) = y; 
  1338           i < length(env); j < length(env); env \<in> list(A)|]
  1339        ==> is_formula_N(##A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
  1340 by (simp add: sats_formula_N_fm)
  1341 
  1342 theorem formula_N_reflection:
  1343      "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),  
  1344                \<lambda>i x. is_formula_N(##Lset(i), f(x), g(x))]"
  1345 apply (simp only: is_formula_N_def)
  1346 apply (intro FOL_reflections function_reflections 
  1347              is_iterates_reflection formula_functor_reflection) 
  1348 done
  1349 
  1350 
  1351 
  1352 subsubsection{*The Predicate ``Is A Formula''*}
  1353 
  1354 (*  mem_formula(M,p) == 
  1355       \<exists>n[M]. \<exists>formn[M]. 
  1356        finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
  1357 definition
  1358   mem_formula_fm :: "i=>i" where
  1359     "mem_formula_fm(x) ==
  1360        Exists(Exists(
  1361          And(finite_ordinal_fm(1),
  1362            And(formula_N_fm(1,0), Member(x#+2,0)))))"
  1363 
  1364 lemma mem_formula_type [TC]:
  1365      "x \<in> nat ==> mem_formula_fm(x) \<in> formula"
  1366 by (simp add: mem_formula_fm_def)
  1367 
  1368 lemma sats_mem_formula_fm [simp]:
  1369    "[| x \<in> nat; env \<in> list(A)|]
  1370     ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(##A, nth(x,env))"
  1371 by (simp add: mem_formula_fm_def mem_formula_def)
  1372 
  1373 lemma mem_formula_iff_sats:
  1374       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
  1375        ==> mem_formula(##A, x) <-> sats(A, mem_formula_fm(i), env)"
  1376 by simp
  1377 
  1378 theorem mem_formula_reflection:
  1379      "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
  1380                \<lambda>i x. mem_formula(##Lset(i),f(x))]"
  1381 apply (simp only: mem_formula_def)
  1382 apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
  1383 done
  1384 
  1385 
  1386 
  1387 subsubsection{*The Predicate ``Is @{term "formula"}''*}
  1388 
  1389 (* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
  1390 definition
  1391   is_formula_fm :: "i=>i" where
  1392     "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
  1393 
  1394 lemma is_formula_type [TC]:
  1395      "x \<in> nat ==> is_formula_fm(x) \<in> formula"
  1396 by (simp add: is_formula_fm_def)
  1397 
  1398 lemma sats_is_formula_fm [simp]:
  1399    "[| x \<in> nat; env \<in> list(A)|]
  1400     ==> sats(A, is_formula_fm(x), env) <-> is_formula(##A, nth(x,env))"
  1401 by (simp add: is_formula_fm_def is_formula_def)
  1402 
  1403 lemma is_formula_iff_sats:
  1404       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
  1405        ==> is_formula(##A, x) <-> sats(A, is_formula_fm(i), env)"
  1406 by simp
  1407 
  1408 theorem is_formula_reflection:
  1409      "REFLECTS[\<lambda>x. is_formula(L,f(x)),
  1410                \<lambda>i x. is_formula(##Lset(i),f(x))]"
  1411 apply (simp only: is_formula_def)
  1412 apply (intro FOL_reflections mem_formula_reflection)
  1413 done
  1414 
  1415 
  1416 subsubsection{*The Operator @{term is_transrec}*}
  1417 
  1418 text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
  1419    within eight quantifiers!
  1420    We call @{term p} with arguments a, f, z by equating them with 
  1421   the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
  1422 
  1423 (* is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
  1424    "is_transrec(M,MH,a,z) == 
  1425       \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
  1426        2       1         0
  1427        upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
  1428        is_wfrec(M,MH,mesa,a,z)" *)
  1429 definition
  1430   is_transrec_fm :: "[i, i, i]=>i" where
  1431  "is_transrec_fm(p,a,z) == 
  1432     Exists(Exists(Exists(
  1433       And(upair_fm(a#+3,a#+3,2),
  1434        And(is_eclose_fm(2,1),
  1435         And(Memrel_fm(1,0), is_wfrec_fm(p,0,a#+3,z#+3)))))))"
  1436 
  1437 
  1438 lemma is_transrec_type [TC]:
  1439      "[| p \<in> formula; x \<in> nat; z \<in> nat |] 
  1440       ==> is_transrec_fm(p,x,z) \<in> formula"
  1441 by (simp add: is_transrec_fm_def) 
  1442 
  1443 lemma sats_is_transrec_fm:
  1444   assumes MH_iff_sats: 
  1445       "!!a0 a1 a2 a3 a4 a5 a6 a7. 
  1446         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A|] 
  1447         ==> MH(a2, a1, a0) <-> 
  1448             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
  1449                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))"
  1450   shows 
  1451       "[|x < length(env); z < length(env); env \<in> list(A)|]
  1452        ==> sats(A, is_transrec_fm(p,x,z), env) <-> 
  1453            is_transrec(##A, MH, nth(x,env), nth(z,env))"
  1454 apply (frule_tac x=z in lt_length_in_nat, assumption)  
  1455 apply (frule_tac x=x in lt_length_in_nat, assumption)  
  1456 apply (simp add: is_transrec_fm_def sats_is_wfrec_fm is_transrec_def MH_iff_sats [THEN iff_sym]) 
  1457 done
  1458 
  1459 
  1460 lemma is_transrec_iff_sats:
  1461   assumes MH_iff_sats: 
  1462       "!!a0 a1 a2 a3 a4 a5 a6 a7. 
  1463         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A|] 
  1464         ==> MH(a2, a1, a0) <-> 
  1465             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
  1466                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))"
  1467   shows
  1468   "[|nth(i,env) = x; nth(k,env) = z; 
  1469       i < length(env); k < length(env); env \<in> list(A)|]
  1470    ==> is_transrec(##A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)" 
  1471 by (simp add: sats_is_transrec_fm [OF MH_iff_sats])
  1472 
  1473 theorem is_transrec_reflection:
  1474   assumes MH_reflection:
  1475     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
  1476                      \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
  1477   shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)), 
  1478                \<lambda>i x. is_transrec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
  1479 apply (simp (no_asm_use) only: is_transrec_def)
  1480 apply (intro FOL_reflections function_reflections MH_reflection 
  1481              is_wfrec_reflection is_eclose_reflection)
  1482 done
  1483 
  1484 end