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
```