src/ZF/Constructible/WF_absolute.thy
changeset 32960 69916a850301
parent 21404 eb85850d3eb7
child 46823 57bf0cecb366
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      ZF/Constructible/WF_absolute.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7  *)
     1.8  
     1.9 @@ -56,28 +55,28 @@
    1.10  
    1.11  lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
    1.12  by (blast del: subsetI
    1.13 -	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
    1.14 +          intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
    1.15  
    1.16  
    1.17  definition
    1.18    rtran_closure_mem :: "[i=>o,i,i,i] => o" where
    1.19      --{*The property of belonging to @{text "rtran_closure(r)"}*}
    1.20      "rtran_closure_mem(M,A,r,p) ==
    1.21 -	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.22 +              \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.23                 omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    1.24 -	       (\<exists>f[M]. typed_function(M,n',A,f) &
    1.25 -		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.26 -		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.27 -		  (\<forall>j[M]. j\<in>n --> 
    1.28 -		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.29 -		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.30 -		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
    1.31 +               (\<exists>f[M]. typed_function(M,n',A,f) &
    1.32 +                (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.33 +                  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.34 +                  (\<forall>j[M]. j\<in>n --> 
    1.35 +                    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.36 +                      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.37 +                      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
    1.38  
    1.39  definition
    1.40    rtran_closure :: "[i=>o,i,i] => o" where
    1.41      "rtran_closure(M,r,s) == 
    1.42          \<forall>A[M]. is_field(M,r,A) -->
    1.43 - 	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"
    1.44 +         (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"
    1.45  
    1.46  definition
    1.47    tran_closure :: "[i=>o,i,i] => o" where
    1.48 @@ -96,12 +95,12 @@
    1.49  
    1.50  locale M_trancl = M_basic +
    1.51    assumes rtrancl_separation:
    1.52 -	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    1.53 +         "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    1.54        and wellfounded_trancl_separation:
    1.55 -	 "[| M(r); M(Z) |] ==> 
    1.56 -	  separation (M, \<lambda>x. 
    1.57 -	      \<exists>w[M]. \<exists>wx[M]. \<exists>rp[M]. 
    1.58 -	       w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"
    1.59 +         "[| M(r); M(Z) |] ==> 
    1.60 +          separation (M, \<lambda>x. 
    1.61 +              \<exists>w[M]. \<exists>wx[M]. \<exists>rp[M]. 
    1.62 +               w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"
    1.63  
    1.64  
    1.65  lemma (in M_trancl) rtran_closure_rtrancl: