src/ZF/Constructible/Rec_Separation.thy
 author paulson Tue Sep 10 16:51:31 2002 +0200 (2002-09-10) changeset 13564 1500a2e48d44 parent 13506 acc18a5d2b1a child 13566 52a419210d5c permissions -rw-r--r--
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
```     1 (*  Title:      ZF/Constructible/Rec_Separation.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   2002  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {*Separation for Facts About Recursion*}
```
```     8
```
```     9 theory Rec_Separation = Separation + Internalize:
```
```    10
```
```    11 text{*This theory proves all instances needed for locales @{text
```
```    12 "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
```
```    13
```
```    14 lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
```
```    15 by simp
```
```    16
```
```    17
```
```    18 subsection{*The Locale @{text "M_trancl"}*}
```
```    19
```
```    20 subsubsection{*Separation for Reflexive/Transitive Closure*}
```
```    21
```
```    22 text{*First, The Defining Formula*}
```
```    23
```
```    24 (* "rtran_closure_mem(M,A,r,p) ==
```
```    25       \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
```
```    26        omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
```
```    27        (\<exists>f[M]. typed_function(M,n',A,f) &
```
```    28         (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
```
```    29           fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
```
```    30         (\<forall>j[M]. j\<in>n -->
```
```    31           (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
```
```    32             fun_apply(M,f,j,fj) & successor(M,j,sj) &
```
```    33             fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
```
```    34 constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
```
```    35  "rtran_closure_mem_fm(A,r,p) ==
```
```    36    Exists(Exists(Exists(
```
```    37     And(omega_fm(2),
```
```    38      And(Member(1,2),
```
```    39       And(succ_fm(1,0),
```
```    40        Exists(And(typed_function_fm(1, A#+4, 0),
```
```    41         And(Exists(Exists(Exists(
```
```    42               And(pair_fm(2,1,p#+7),
```
```    43                And(empty_fm(0),
```
```    44                 And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
```
```    45             Forall(Implies(Member(0,3),
```
```    46              Exists(Exists(Exists(Exists(
```
```    47               And(fun_apply_fm(5,4,3),
```
```    48                And(succ_fm(4,2),
```
```    49                 And(fun_apply_fm(5,2,1),
```
```    50                  And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
```
```    51
```
```    52
```
```    53 lemma rtran_closure_mem_type [TC]:
```
```    54  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
```
```    55 by (simp add: rtran_closure_mem_fm_def)
```
```    56
```
```    57 lemma arity_rtran_closure_mem_fm [simp]:
```
```    58      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
```
```    59       ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
```
```    60 by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```    61
```
```    62 lemma sats_rtran_closure_mem_fm [simp]:
```
```    63    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```    64     ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
```
```    65         rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
```
```    66 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
```
```    67
```
```    68 lemma rtran_closure_mem_iff_sats:
```
```    69       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
```
```    70           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
```
```    71        ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
```
```    72 by (simp add: sats_rtran_closure_mem_fm)
```
```    73
```
```    74 theorem rtran_closure_mem_reflection:
```
```    75      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
```
```    76                \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
```
```    77 apply (simp only: rtran_closure_mem_def setclass_simps)
```
```    78 apply (intro FOL_reflections function_reflections fun_plus_reflections)
```
```    79 done
```
```    80
```
```    81 text{*Separation for @{term "rtrancl(r)"}.*}
```
```    82 lemma rtrancl_separation:
```
```    83      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
```
```    84 apply (rule separation_CollectI)
```
```    85 apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
```
```    86 apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
```
```    87 apply (drule subset_Lset_ltD, assumption)
```
```    88 apply (erule reflection_imp_L_separation)
```
```    89   apply (simp_all add: lt_Ord2)
```
```    90 apply (rule DPow_LsetI)
```
```    91 apply (rename_tac u)
```
```    92 apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
```
```    93 apply (rule sep_rules | simp)+
```
```    94 done
```
```    95
```
```    96
```
```    97 subsubsection{*Reflexive/Transitive Closure, Internalized*}
```
```    98
```
```    99 (*  "rtran_closure(M,r,s) ==
```
```   100         \<forall>A[M]. is_field(M,r,A) -->
```
```   101          (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
```
```   102 constdefs rtran_closure_fm :: "[i,i]=>i"
```
```   103  "rtran_closure_fm(r,s) ==
```
```   104    Forall(Implies(field_fm(succ(r),0),
```
```   105                   Forall(Iff(Member(0,succ(succ(s))),
```
```   106                              rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
```
```   107
```
```   108 lemma rtran_closure_type [TC]:
```
```   109      "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
```
```   110 by (simp add: rtran_closure_fm_def)
```
```   111
```
```   112 lemma arity_rtran_closure_fm [simp]:
```
```   113      "[| x \<in> nat; y \<in> nat |]
```
```   114       ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
```
```   115 by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```   116
```
```   117 lemma sats_rtran_closure_fm [simp]:
```
```   118    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
```
```   119     ==> sats(A, rtran_closure_fm(x,y), env) <->
```
```   120         rtran_closure(**A, nth(x,env), nth(y,env))"
```
```   121 by (simp add: rtran_closure_fm_def rtran_closure_def)
```
```   122
```
```   123 lemma rtran_closure_iff_sats:
```
```   124       "[| nth(i,env) = x; nth(j,env) = y;
```
```   125           i \<in> nat; j \<in> nat; env \<in> list(A)|]
```
```   126        ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
```
```   127 by simp
```
```   128
```
```   129 theorem rtran_closure_reflection:
```
```   130      "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
```
```   131                \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
```
```   132 apply (simp only: rtran_closure_def setclass_simps)
```
```   133 apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
```
```   134 done
```
```   135
```
```   136
```
```   137 subsubsection{*Transitive Closure of a Relation, Internalized*}
```
```   138
```
```   139 (*  "tran_closure(M,r,t) ==
```
```   140          \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
```
```   141 constdefs tran_closure_fm :: "[i,i]=>i"
```
```   142  "tran_closure_fm(r,s) ==
```
```   143    Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
```
```   144
```
```   145 lemma tran_closure_type [TC]:
```
```   146      "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
```
```   147 by (simp add: tran_closure_fm_def)
```
```   148
```
```   149 lemma arity_tran_closure_fm [simp]:
```
```   150      "[| x \<in> nat; y \<in> nat |]
```
```   151       ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
```
```   152 by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```   153
```
```   154 lemma sats_tran_closure_fm [simp]:
```
```   155    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
```
```   156     ==> sats(A, tran_closure_fm(x,y), env) <->
```
```   157         tran_closure(**A, nth(x,env), nth(y,env))"
```
```   158 by (simp add: tran_closure_fm_def tran_closure_def)
```
```   159
```
```   160 lemma tran_closure_iff_sats:
```
```   161       "[| nth(i,env) = x; nth(j,env) = y;
```
```   162           i \<in> nat; j \<in> nat; env \<in> list(A)|]
```
```   163        ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
```
```   164 by simp
```
```   165
```
```   166 theorem tran_closure_reflection:
```
```   167      "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
```
```   168                \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
```
```   169 apply (simp only: tran_closure_def setclass_simps)
```
```   170 apply (intro FOL_reflections function_reflections
```
```   171              rtran_closure_reflection composition_reflection)
```
```   172 done
```
```   173
```
```   174
```
```   175 subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
```
```   176
```
```   177 lemma wellfounded_trancl_reflects:
```
```   178   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
```
```   179                  w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
```
```   180    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
```
```   181        w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
```
```   182        wx \<in> rp]"
```
```   183 by (intro FOL_reflections function_reflections fun_plus_reflections
```
```   184           tran_closure_reflection)
```
```   185
```
```   186
```
```   187 lemma wellfounded_trancl_separation:
```
```   188          "[| L(r); L(Z) |] ==>
```
```   189           separation (L, \<lambda>x.
```
```   190               \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
```
```   191                w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
```
```   192 apply (rule separation_CollectI)
```
```   193 apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
```
```   194 apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
```
```   195 apply (drule subset_Lset_ltD, assumption)
```
```   196 apply (erule reflection_imp_L_separation)
```
```   197   apply (simp_all add: lt_Ord2)
```
```   198 apply (rule DPow_LsetI)
```
```   199 apply (rename_tac u)
```
```   200 apply (rule bex_iff_sats conj_iff_sats)+
```
```   201 apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
```
```   202 apply (rule sep_rules tran_closure_iff_sats | simp)+
```
```   203 done
```
```   204
```
```   205
```
```   206 subsubsection{*Instantiating the locale @{text M_trancl}*}
```
```   207
```
```   208 lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
```
```   209   apply (rule M_trancl_axioms.intro)
```
```   210    apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
```
```   211   done
```
```   212
```
```   213 theorem M_trancl_L: "PROP M_trancl(L)"
```
```   214 by (rule M_trancl.intro
```
```   215          [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
```
```   216
```
```   217 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
```
```   218   and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
```
```   219   and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
```
```   220   and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
```
```   221   and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
```
```   222   and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
```
```   223   and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
```
```   224   and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
```
```   225   and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
```
```   226   and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
```
```   227   and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
```
```   228   and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
```
```   229   and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
```
```   230
```
```   231 declare rtrancl_closed [intro,simp]
```
```   232 declare rtrancl_abs [simp]
```
```   233 declare trancl_closed [intro,simp]
```
```   234 declare trancl_abs [simp]
```
```   235
```
```   236
```
```   237 subsection{*The Locale @{text "M_wfrank"}*}
```
```   238
```
```   239 subsubsection{*Separation for @{term "wfrank"}*}
```
```   240
```
```   241 lemma wfrank_Reflects:
```
```   242  "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   243               ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
```
```   244       \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   245          ~ (\<exists>f \<in> Lset(i).
```
```   246             M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
```
```   247                         rplus, x, f))]"
```
```   248 by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
```
```   249
```
```   250 lemma wfrank_separation:
```
```   251      "L(r) ==>
```
```   252       separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   253          ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
```
```   254 apply (rule separation_CollectI)
```
```   255 apply (rule_tac A="{r,z}" in subset_LsetE, blast)
```
```   256 apply (rule ReflectsE [OF wfrank_Reflects], assumption)
```
```   257 apply (drule subset_Lset_ltD, assumption)
```
```   258 apply (erule reflection_imp_L_separation)
```
```   259   apply (simp_all add: lt_Ord2, clarify)
```
```   260 apply (rule DPow_LsetI)
```
```   261 apply (rename_tac u)
```
```   262 apply (rule ball_iff_sats imp_iff_sats)+
```
```   263 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
```
```   264 apply (rule sep_rules | simp)+
```
```   265 apply (rule sep_rules is_recfun_iff_sats | simp)+
```
```   266 done
```
```   267
```
```   268
```
```   269 subsubsection{*Replacement for @{term "wfrank"}*}
```
```   270
```
```   271 lemma wfrank_replacement_Reflects:
```
```   272  "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
```
```   273         (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   274          (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
```
```   275                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
```
```   276                         is_range(L,f,y))),
```
```   277  \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
```
```   278       (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   279        (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
```
```   280          M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
```
```   281          is_range(**Lset(i),f,y)))]"
```
```   282 by (intro FOL_reflections function_reflections fun_plus_reflections
```
```   283              is_recfun_reflection tran_closure_reflection)
```
```   284
```
```   285
```
```   286 lemma wfrank_strong_replacement:
```
```   287      "L(r) ==>
```
```   288       strong_replacement(L, \<lambda>x z.
```
```   289          \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   290          (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
```
```   291                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
```
```   292                         is_range(L,f,y)))"
```
```   293 apply (rule strong_replacementI)
```
```   294 apply (rule rallI)
```
```   295 apply (rename_tac B)
```
```   296 apply (rule separation_CollectI)
```
```   297 apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
```
```   298 apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
```
```   299 apply (drule subset_Lset_ltD, assumption)
```
```   300 apply (erule reflection_imp_L_separation)
```
```   301   apply (simp_all add: lt_Ord2)
```
```   302 apply (rule DPow_LsetI)
```
```   303 apply (rename_tac u)
```
```   304 apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
```
```   305 apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
```
```   306 apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+
```
```   307 done
```
```   308
```
```   309
```
```   310 subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
```
```   311
```
```   312 lemma Ord_wfrank_Reflects:
```
```   313  "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   314           ~ (\<forall>f[L]. \<forall>rangef[L].
```
```   315              is_range(L,f,rangef) -->
```
```   316              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
```
```   317              ordinal(L,rangef)),
```
```   318       \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   319           ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
```
```   320              is_range(**Lset(i),f,rangef) -->
```
```   321              M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
```
```   322                          rplus, x, f) -->
```
```   323              ordinal(**Lset(i),rangef))]"
```
```   324 by (intro FOL_reflections function_reflections is_recfun_reflection
```
```   325           tran_closure_reflection ordinal_reflection)
```
```   326
```
```   327 lemma  Ord_wfrank_separation:
```
```   328      "L(r) ==>
```
```   329       separation (L, \<lambda>x.
```
```   330          \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   331           ~ (\<forall>f[L]. \<forall>rangef[L].
```
```   332              is_range(L,f,rangef) -->
```
```   333              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
```
```   334              ordinal(L,rangef)))"
```
```   335 apply (rule separation_CollectI)
```
```   336 apply (rule_tac A="{r,z}" in subset_LsetE, blast)
```
```   337 apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
```
```   338 apply (drule subset_Lset_ltD, assumption)
```
```   339 apply (erule reflection_imp_L_separation)
```
```   340   apply (simp_all add: lt_Ord2, clarify)
```
```   341 apply (rule DPow_LsetI)
```
```   342 apply (rename_tac u)
```
```   343 apply (rule ball_iff_sats imp_iff_sats)+
```
```   344 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
```
```   345 apply (rule sep_rules is_recfun_iff_sats | simp)+
```
```   346 done
```
```   347
```
```   348
```
```   349 subsubsection{*Instantiating the locale @{text M_wfrank}*}
```
```   350
```
```   351 lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
```
```   352   apply (rule M_wfrank_axioms.intro)
```
```   353    apply (assumption | rule
```
```   354      wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
```
```   355   done
```
```   356
```
```   357 theorem M_wfrank_L: "PROP M_wfrank(L)"
```
```   358   apply (rule M_wfrank.intro)
```
```   359      apply (rule M_trancl.axioms [OF M_trancl_L])+
```
```   360   apply (rule M_wfrank_axioms_L)
```
```   361   done
```
```   362
```
```   363 lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
```
```   364   and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
```
```   365   and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]
```
```   366   and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L]
```
```   367   and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L]
```
```   368   and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L]
```
```   369   and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L]
```
```   370   and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L]
```
```   371   and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L]
```
```   372   and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L]
```
```   373   and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L]
```
```   374   and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L]
```
```   375   and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L]
```
```   376   and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L]
```
```   377   and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L]
```
```   378   and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L]
```
```   379   and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L]
```
```   380   and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L]
```
```   381   and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L]
```
```   382
```
```   383 declare iterates_closed [intro,simp]
```
```   384 declare Ord_wfrank_range [rule_format]
```
```   385 declare wf_abs [simp]
```
```   386 declare wf_on_abs [simp]
```
```   387
```
```   388
```
```   389 subsection{*@{term L} is Closed Under the Operator @{term list}*}
```
```   390
```
```   391 subsubsection{*Instances of Replacement for Lists*}
```
```   392
```
```   393 lemma list_replacement1_Reflects:
```
```   394  "REFLECTS
```
```   395    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
```
```   396          is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
```
```   397     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
```
```   398          is_wfrec(**Lset(i),
```
```   399                   iterates_MH(**Lset(i),
```
```   400                           is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
```
```   401 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   402           iterates_MH_reflection list_functor_reflection)
```
```   403
```
```   404
```
```   405 lemma list_replacement1:
```
```   406    "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
```
```   407 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
```
```   408 apply (rule strong_replacementI)
```
```   409 apply (rule rallI)
```
```   410 apply (rename_tac B)
```
```   411 apply (rule separation_CollectI)
```
```   412 apply (insert nonempty)
```
```   413 apply (subgoal_tac "L(Memrel(succ(n)))")
```
```   414 apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
```
```   415 apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
```
```   416 apply (drule subset_Lset_ltD, assumption)
```
```   417 apply (erule reflection_imp_L_separation)
```
```   418   apply (simp_all add: lt_Ord2 Memrel_closed)
```
```   419 apply (elim conjE)
```
```   420 apply (rule DPow_LsetI)
```
```   421 apply (rename_tac v)
```
```   422 apply (rule bex_iff_sats conj_iff_sats)+
```
```   423 apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
```
```   424 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
```
```   425             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
```
```   426 done
```
```   427
```
```   428
```
```   429 lemma list_replacement2_Reflects:
```
```   430  "REFLECTS
```
```   431    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
```
```   432          (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
```
```   433            is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
```
```   434                               msn, u, x)),
```
```   435     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
```
```   436          (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
```
```   437           successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
```
```   438            is_wfrec (**Lset(i),
```
```   439                  iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
```
```   440                      msn, u, x))]"
```
```   441 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   442           iterates_MH_reflection list_functor_reflection)
```
```   443
```
```   444
```
```   445 lemma list_replacement2:
```
```   446    "L(A) ==> strong_replacement(L,
```
```   447          \<lambda>n y. n\<in>nat &
```
```   448                (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
```
```   449                is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
```
```   450                         msn, n, y)))"
```
```   451 apply (rule strong_replacementI)
```
```   452 apply (rule rallI)
```
```   453 apply (rename_tac B)
```
```   454 apply (rule separation_CollectI)
```
```   455 apply (insert nonempty)
```
```   456 apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE)
```
```   457 apply (blast intro: L_nat)
```
```   458 apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
```
```   459 apply (drule subset_Lset_ltD, assumption)
```
```   460 apply (erule reflection_imp_L_separation)
```
```   461   apply (simp_all add: lt_Ord2)
```
```   462 apply (rule DPow_LsetI)
```
```   463 apply (rename_tac v)
```
```   464 apply (rule bex_iff_sats conj_iff_sats)+
```
```   465 apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
```
```   466 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
```
```   467             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
```
```   468 done
```
```   469
```
```   470
```
```   471 subsection{*@{term L} is Closed Under the Operator @{term formula}*}
```
```   472
```
```   473 subsubsection{*Instances of Replacement for Formulas*}
```
```   474
```
```   475 lemma formula_replacement1_Reflects:
```
```   476  "REFLECTS
```
```   477    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
```
```   478          is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
```
```   479     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
```
```   480          is_wfrec(**Lset(i),
```
```   481                   iterates_MH(**Lset(i),
```
```   482                           is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
```
```   483 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   484           iterates_MH_reflection formula_functor_reflection)
```
```   485
```
```   486 lemma formula_replacement1:
```
```   487    "iterates_replacement(L, is_formula_functor(L), 0)"
```
```   488 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
```
```   489 apply (rule strong_replacementI)
```
```   490 apply (rule rallI)
```
```   491 apply (rename_tac B)
```
```   492 apply (rule separation_CollectI)
```
```   493 apply (insert nonempty)
```
```   494 apply (subgoal_tac "L(Memrel(succ(n)))")
```
```   495 apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
```
```   496 apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
```
```   497 apply (drule subset_Lset_ltD, assumption)
```
```   498 apply (erule reflection_imp_L_separation)
```
```   499   apply (simp_all add: lt_Ord2 Memrel_closed)
```
```   500 apply (rule DPow_LsetI)
```
```   501 apply (rename_tac v)
```
```   502 apply (rule bex_iff_sats conj_iff_sats)+
```
```   503 apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
```
```   504 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
```
```   505             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
```
```   506 done
```
```   507
```
```   508 lemma formula_replacement2_Reflects:
```
```   509  "REFLECTS
```
```   510    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
```
```   511          (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
```
```   512            is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0),
```
```   513                               msn, u, x)),
```
```   514     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
```
```   515          (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
```
```   516           successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
```
```   517            is_wfrec (**Lset(i),
```
```   518                  iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0),
```
```   519                      msn, u, x))]"
```
```   520 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   521           iterates_MH_reflection formula_functor_reflection)
```
```   522
```
```   523
```
```   524 lemma formula_replacement2:
```
```   525    "strong_replacement(L,
```
```   526          \<lambda>n y. n\<in>nat &
```
```   527                (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
```
```   528                is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
```
```   529                         msn, n, y)))"
```
```   530 apply (rule strong_replacementI)
```
```   531 apply (rule rallI)
```
```   532 apply (rename_tac B)
```
```   533 apply (rule separation_CollectI)
```
```   534 apply (insert nonempty)
```
```   535 apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
```
```   536 apply (blast intro: L_nat)
```
```   537 apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption)
```
```   538 apply (drule subset_Lset_ltD, assumption)
```
```   539 apply (erule reflection_imp_L_separation)
```
```   540   apply (simp_all add: lt_Ord2)
```
```   541 apply (rule DPow_LsetI)
```
```   542 apply (rename_tac v)
```
```   543 apply (rule bex_iff_sats conj_iff_sats)+
```
```   544 apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
```
```   545 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
```
```   546             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
```
```   547 done
```
```   548
```
```   549 text{*NB The proofs for type @{term formula} are virtually identical to those
```
```   550 for @{term "list(A)"}.  It was a cut-and-paste job! *}
```
```   551
```
```   552
```
```   553 subsubsection{*The Formula @{term is_nth}, Internalized*}
```
```   554
```
```   555 (* "is_nth(M,n,l,Z) ==
```
```   556       \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
```
```   557        2       1       0
```
```   558        successor(M,n,sn) & membership(M,sn,msn) &
```
```   559        is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
```
```   560        is_hd(M,X,Z)" *)
```
```   561 constdefs nth_fm :: "[i,i,i]=>i"
```
```   562     "nth_fm(n,l,Z) ==
```
```   563        Exists(Exists(Exists(
```
```   564          And(succ_fm(n#+3,1),
```
```   565           And(Memrel_fm(1,0),
```
```   566            And(is_wfrec_fm(iterates_MH_fm(tl_fm(1,0),l#+8,2,1,0), 0, n#+3, 2), hd_fm(2,Z#+3)))))))"
```
```   567
```
```   568 lemma nth_fm_type [TC]:
```
```   569  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula"
```
```   570 by (simp add: nth_fm_def)
```
```   571
```
```   572 lemma sats_nth_fm [simp]:
```
```   573    "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```   574     ==> sats(A, nth_fm(x,y,z), env) <->
```
```   575         is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
```
```   576 apply (frule lt_length_in_nat, assumption)
```
```   577 apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm)
```
```   578 done
```
```   579
```
```   580 lemma nth_iff_sats:
```
```   581       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
```
```   582           i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
```
```   583        ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
```
```   584 by (simp add: sats_nth_fm)
```
```   585
```
```   586 theorem nth_reflection:
```
```   587      "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),
```
```   588                \<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
```
```   589 apply (simp only: is_nth_def setclass_simps)
```
```   590 apply (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   591              iterates_MH_reflection hd_reflection tl_reflection)
```
```   592 done
```
```   593
```
```   594
```
```   595 subsubsection{*An Instance of Replacement for @{term nth}*}
```
```   596
```
```   597 lemma nth_replacement_Reflects:
```
```   598  "REFLECTS
```
```   599    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
```
```   600          is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
```
```   601     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
```
```   602          is_wfrec(**Lset(i),
```
```   603                   iterates_MH(**Lset(i),
```
```   604                           is_tl(**Lset(i)), z), memsn, u, y))]"
```
```   605 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   606           iterates_MH_reflection list_functor_reflection tl_reflection)
```
```   607
```
```   608 lemma nth_replacement:
```
```   609    "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
```
```   610 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
```
```   611 apply (rule strong_replacementI)
```
```   612 apply (rule rallI)
```
```   613 apply (rule separation_CollectI)
```
```   614 apply (subgoal_tac "L(Memrel(succ(n)))")
```
```   615 apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
```
```   616 apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
```
```   617 apply (drule subset_Lset_ltD, assumption)
```
```   618 apply (erule reflection_imp_L_separation)
```
```   619   apply (simp_all add: lt_Ord2 Memrel_closed)
```
```   620 apply (elim conjE)
```
```   621 apply (rule DPow_LsetI)
```
```   622 apply (rename_tac v)
```
```   623 apply (rule bex_iff_sats conj_iff_sats)+
```
```   624 apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
```
```   625 apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
```
```   626             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
```
```   627 done
```
```   628
```
```   629
```
```   630
```
```   631 subsubsection{*Instantiating the locale @{text M_datatypes}*}
```
```   632
```
```   633 lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
```
```   634   apply (rule M_datatypes_axioms.intro)
```
```   635       apply (assumption | rule
```
```   636         list_replacement1 list_replacement2
```
```   637         formula_replacement1 formula_replacement2
```
```   638         nth_replacement)+
```
```   639   done
```
```   640
```
```   641 theorem M_datatypes_L: "PROP M_datatypes(L)"
```
```   642   apply (rule M_datatypes.intro)
```
```   643       apply (rule M_wfrank.axioms [OF M_wfrank_L])+
```
```   644  apply (rule M_datatypes_axioms_L)
```
```   645  done
```
```   646
```
```   647 lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
```
```   648   and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
```
```   649   and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
```
```   650   and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L]
```
```   651   and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L]
```
```   652
```
```   653 declare list_closed [intro,simp]
```
```   654 declare formula_closed [intro,simp]
```
```   655 declare list_abs [simp]
```
```   656 declare formula_abs [simp]
```
```   657 declare nth_abs [simp]
```
```   658
```
```   659
```
```   660 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
```
```   661
```
```   662 subsubsection{*Instances of Replacement for @{term eclose}*}
```
```   663
```
```   664 lemma eclose_replacement1_Reflects:
```
```   665  "REFLECTS
```
```   666    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
```
```   667          is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
```
```   668     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
```
```   669          is_wfrec(**Lset(i),
```
```   670                   iterates_MH(**Lset(i), big_union(**Lset(i)), A),
```
```   671                   memsn, u, y))]"
```
```   672 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   673           iterates_MH_reflection)
```
```   674
```
```   675 lemma eclose_replacement1:
```
```   676    "L(A) ==> iterates_replacement(L, big_union(L), A)"
```
```   677 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
```
```   678 apply (rule strong_replacementI)
```
```   679 apply (rule rallI)
```
```   680 apply (rename_tac B)
```
```   681 apply (rule separation_CollectI)
```
```   682 apply (subgoal_tac "L(Memrel(succ(n)))")
```
```   683 apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
```
```   684 apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
```
```   685 apply (drule subset_Lset_ltD, assumption)
```
```   686 apply (erule reflection_imp_L_separation)
```
```   687   apply (simp_all add: lt_Ord2 Memrel_closed)
```
```   688 apply (elim conjE)
```
```   689 apply (rule DPow_LsetI)
```
```   690 apply (rename_tac v)
```
```   691 apply (rule bex_iff_sats conj_iff_sats)+
```
```   692 apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
```
```   693 apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
```
```   694              is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
```
```   695 done
```
```   696
```
```   697
```
```   698 lemma eclose_replacement2_Reflects:
```
```   699  "REFLECTS
```
```   700    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
```
```   701          (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
```
```   702            is_wfrec (L, iterates_MH (L, big_union(L), A),
```
```   703                               msn, u, x)),
```
```   704     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
```
```   705          (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
```
```   706           successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
```
```   707            is_wfrec (**Lset(i),
```
```   708                  iterates_MH (**Lset(i), big_union(**Lset(i)), A),
```
```   709                      msn, u, x))]"
```
```   710 by (intro FOL_reflections function_reflections is_wfrec_reflection
```
```   711           iterates_MH_reflection)
```
```   712
```
```   713
```
```   714 lemma eclose_replacement2:
```
```   715    "L(A) ==> strong_replacement(L,
```
```   716          \<lambda>n y. n\<in>nat &
```
```   717                (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
```
```   718                is_wfrec(L, iterates_MH(L,big_union(L), A),
```
```   719                         msn, n, y)))"
```
```   720 apply (rule strong_replacementI)
```
```   721 apply (rule rallI)
```
```   722 apply (rename_tac B)
```
```   723 apply (rule separation_CollectI)
```
```   724 apply (rule_tac A="{A,B,z,nat}" in subset_LsetE)
```
```   725 apply (blast intro: L_nat)
```
```   726 apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
```
```   727 apply (drule subset_Lset_ltD, assumption)
```
```   728 apply (erule reflection_imp_L_separation)
```
```   729   apply (simp_all add: lt_Ord2)
```
```   730 apply (rule DPow_LsetI)
```
```   731 apply (rename_tac v)
```
```   732 apply (rule bex_iff_sats conj_iff_sats)+
```
```   733 apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
```
```   734 apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
```
```   735               is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
```
```   736 done
```
```   737
```
```   738
```
```   739 subsubsection{*Instantiating the locale @{text M_eclose}*}
```
```   740
```
```   741 lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
```
```   742   apply (rule M_eclose_axioms.intro)
```
```   743    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
```
```   744   done
```
```   745
```
```   746 theorem M_eclose_L: "PROP M_eclose(L)"
```
```   747   apply (rule M_eclose.intro)
```
```   748        apply (rule M_datatypes.axioms [OF M_datatypes_L])+
```
```   749   apply (rule M_eclose_axioms_L)
```
```   750   done
```
```   751
```
```   752 lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
```
```   753   and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
```
```   754   and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
```
```   755
```
```   756 end
```