src/ZF/Constructible/Rec_Separation.thy
changeset 13493 5aa68c051725
parent 13441 d6d620639243
child 13496 6f0c57def6d5
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Aug 12 17:59:57 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Aug 12 18:01:44 2002 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
     1.5  by simp
     1.6  
     1.7 +
     1.8  subsection{*The Locale @{text "M_trancl"}*}
     1.9  
    1.10  subsubsection{*Separation for Reflexive/Transitive Closure*}
    1.11 @@ -1264,14 +1265,31 @@
    1.12         2       1       0
    1.13         successor(M,n,sn) & membership(M,sn,msn) &
    1.14         is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
    1.15 -       is_hd(M,X,Z)"
    1.16 +       is_hd(M,X,Z)" *)
    1.17  constdefs nth_fm :: "[i,i,i]=>i"
    1.18      "nth_fm(n,l,Z) == 
    1.19         Exists(Exists(Exists(
    1.20 -         And(successor_fm(n#+3,1),
    1.21 -          And(membership_fm(1,0),
    1.22 -           And(
    1.23 - *)
    1.24 +         And(succ_fm(n#+3,1),
    1.25 +          And(Memrel_fm(1,0),
    1.26 +           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)))))))"
    1.27 +
    1.28 +lemma nth_fm_type [TC]:
    1.29 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula"
    1.30 +by (simp add: nth_fm_def)
    1.31 +
    1.32 +lemma sats_nth_fm [simp]:
    1.33 +   "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.34 +    ==> sats(A, nth_fm(x,y,z), env) <->
    1.35 +        is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
    1.36 +apply (frule lt_length_in_nat, assumption)  
    1.37 +apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm) 
    1.38 +done
    1.39 +
    1.40 +lemma nth_iff_sats:
    1.41 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    1.42 +          i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.43 +       ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
    1.44 +by (simp add: sats_nth_fm)
    1.45  
    1.46  theorem nth_reflection:
    1.47       "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),