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