src/ZF/Constructible/WF_absolute.thy
changeset 13324 39d1b3a4c6f4
parent 13323 2c287f50c9f3
child 13339 0f89104dd377
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 15:39:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 17:25:42 2002 +0200
     1.3 @@ -111,41 +111,43 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 +  rtran_closure_mem :: "[i=>o,i,i,i] => o"
     1.8 +    --{*The property of belonging to @{text "rtran_closure(r)"}*}
     1.9 +    "rtran_closure_mem(M,A,r,p) ==
    1.10 +	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.11 +               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    1.12 +	       (\<exists>f[M]. typed_function(M,n',A,f) &
    1.13 +		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.14 +		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.15 +		  (\<forall>j[M]. j\<in>n --> 
    1.16 +		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.17 +		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.18 +		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
    1.19 +
    1.20    rtran_closure :: "[i=>o,i,i] => o"
    1.21 -    "rtran_closure(M,r,s) ==
    1.22 -        \<forall>A. M(A) --> is_field(M,r,A) -->
    1.23 - 	 (\<forall>p. M(p) -->
    1.24 -          (p \<in> s <->
    1.25 -           (\<exists>n\<in>nat. M(n) &
    1.26 -            (\<exists>n'. M(n') & successor(M,n,n') &
    1.27 -             (\<exists>f. M(f) & typed_function(M,n',A,f) &
    1.28 -              (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &
    1.29 -                   fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) &
    1.30 -              (\<forall>i\<in>n. M(i) -->
    1.31 -                (\<forall>i'. M(i') --> successor(M,i,i') -->
    1.32 -                 (\<forall>fi. M(fi) --> fun_apply(M,f,i,fi) -->
    1.33 -                  (\<forall>fi'. M(fi') --> fun_apply(M,f,i',fi') -->
    1.34 -                   (\<forall>q. M(q) --> pair(M,fi,fi',q) --> q \<in> r))))))))))"
    1.35 +    "rtran_closure(M,r,s) == 
    1.36 +        \<forall>A[M]. is_field(M,r,A) -->
    1.37 + 	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"
    1.38  
    1.39    tran_closure :: "[i=>o,i,i] => o"
    1.40      "tran_closure(M,r,t) ==
    1.41           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
    1.42  
    1.43 +lemma (in M_axioms) rtran_closure_mem_iff:
    1.44 +     "[|M(A); M(r); M(p)|]
    1.45 +      ==> rtran_closure_mem(M,A,r,p) <->
    1.46 +          (\<exists>n[M]. n\<in>nat & 
    1.47 +           (\<exists>f[M]. f \<in> succ(n) -> A &
    1.48 +            (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
    1.49 +                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
    1.50 +apply (simp add: rtran_closure_mem_def typed_apply_abs
    1.51 +                 Ord_succ_mem_iff nat_0_le [THEN ltD])
    1.52 +apply (blast intro: elim:); 
    1.53 +done
    1.54  
    1.55  locale M_trancl = M_axioms +
    1.56    assumes rtrancl_separation:
    1.57 -	 "[| M(r); M(A) |] ==>
    1.58 -	  separation (M, \<lambda>p. 
    1.59 -	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.60 -               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    1.61 -	       (\<exists>f[M]. 
    1.62 -		typed_function(M,n',A,f) &
    1.63 -		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.64 -		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.65 -		  (\<forall>j[M]. j\<in>n --> 
    1.66 -		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.67 -		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.68 -		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r))))"
    1.69 +	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    1.70        and wellfounded_trancl_separation:
    1.71  	 "[| M(r); M(Z) |] ==> 
    1.72  	  separation (M, \<lambda>x. 
    1.73 @@ -155,29 +157,16 @@
    1.74  
    1.75  lemma (in M_trancl) rtran_closure_rtrancl:
    1.76       "M(r) ==> rtran_closure(M,r,rtrancl(r))"
    1.77 -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
    1.78 -                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
    1.79 -                 Ord_succ_mem_iff M_nat  nat_0_le [THEN ltD], clarify)
    1.80 -apply (rule iffI)
    1.81 - apply clarify
    1.82 - apply simp
    1.83 - apply (rename_tac n f)
    1.84 - apply (rule_tac x=n in bexI)
    1.85 -  apply (rule_tac x=f in exI)
    1.86 -  apply simp
    1.87 -  apply (blast dest: finite_fun_closed dest: transM)
    1.88 - apply assumption
    1.89 -apply clarify
    1.90 -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)
    1.91 +apply (simp add: rtran_closure_def rtran_closure_mem_iff 
    1.92 +                 rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def)
    1.93 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
    1.94  done
    1.95  
    1.96  lemma (in M_trancl) rtrancl_closed [intro,simp]:
    1.97       "M(r) ==> M(rtrancl(r))"
    1.98  apply (insert rtrancl_separation [of r "field(r)"])
    1.99  apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
   1.100 -                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
   1.101 -                 Ord_succ_mem_iff M_nat nat_into_M
   1.102 -                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
   1.103 +                 rtrancl_alt_def rtran_closure_mem_iff)
   1.104  done
   1.105  
   1.106  lemma (in M_trancl) rtrancl_abs [simp]:
   1.107 @@ -187,20 +176,10 @@
   1.108   prefer 2 apply (blast intro: rtran_closure_rtrancl)
   1.109  apply (rule M_equalityI)
   1.110  apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
   1.111 -                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
   1.112 -                 Ord_succ_mem_iff M_nat
   1.113 -                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
   1.114 - prefer 2 apply assumption
   1.115 - prefer 2 apply blast
   1.116 -apply (rule iffI, clarify)
   1.117 -apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify, simp)
   1.118 - apply (rename_tac n f)
   1.119 - apply (rule_tac x=n in bexI)
   1.120 -  apply (rule_tac x=f in exI)
   1.121 -  apply (blast dest!: finite_fun_closed, assumption)
   1.122 +                 rtrancl_alt_def rtran_closure_mem_iff)
   1.123 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
   1.124  done
   1.125  
   1.126 -
   1.127  lemma (in M_trancl) trancl_closed [intro,simp]:
   1.128       "M(r) ==> M(trancl(r))"
   1.129  by (simp add: trancl_def comp_closed rtrancl_closed)