More Separation proofs
authorpaulson
Tue Jul 09 10:44:53 2002 +0200 (2002-07-09)
changeset 1331923de7b3af453
parent 13318 3f475e54875c
child 13320 2c6ee189ae63
More Separation proofs
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WFrec.thy
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:41 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:53 2002 +0200
     1.3 @@ -764,9 +764,13 @@
     1.4  	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
     1.5  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
     1.6    and is_recfun_separation:
     1.7 -     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
     1.8 -     "[| M(A); M(f); M(g); M(a); M(b) |] 
     1.9 -     ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
    1.10 +     --{*for well-founded recursion*}
    1.11 +     "[| M(r); M(f); M(g); M(a); M(b) |] 
    1.12 +     ==> separation(M, 
    1.13 +            \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
    1.14 +                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
    1.15 +                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
    1.16 +                                   fx \<noteq> gx))"
    1.17  
    1.18  lemma (in M_axioms) cartprod_iff_lemma:
    1.19       "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
     2.1 --- a/src/ZF/Constructible/Separation.thy	Tue Jul 09 10:44:41 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Separation.thy	Tue Jul 09 10:44:53 2002 +0200
     2.3 @@ -349,7 +349,7 @@
     2.4  done
     2.5  
     2.6  
     2.7 -subsection{*Separation for @{term "well_ord_iso"}*}
     2.8 +subsection{*Separation for a Theorem about @{term "obase"}*}
     2.9  
    2.10  lemma obase_equals_reflects:
    2.11    "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. 
     3.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Jul 09 10:44:41 2002 +0200
     3.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Jul 09 10:44:53 2002 +0200
     3.3 @@ -64,6 +64,13 @@
     3.4  apply (blast intro: sym)+
     3.5  done
     3.6  
     3.7 +lemma (in M_axioms) is_recfun_separation':
     3.8 +    "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
     3.9 +        M(r); M(f); M(g); M(a); M(b) |] 
    3.10 +     ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
    3.11 +apply (insert is_recfun_separation [of r f g a b]) 
    3.12 +apply (simp add: typed_apply_abs vimage_singleton_iff)
    3.13 +done
    3.14  
    3.15  text{*Stated using @{term "trans(r)"} rather than
    3.16        @{term "transitive_rel(M,A,r)"} because the latter rewrites to
    3.17 @@ -82,7 +89,7 @@
    3.18  apply (simp add: is_recfun_def)
    3.19  apply (erule_tac a=x in wellfounded_induct, assumption+)
    3.20  txt{*Separation to justify the induction*}
    3.21 - apply (force intro: is_recfun_separation)
    3.22 + apply (blast intro: is_recfun_separation') 
    3.23  txt{*Now the inductive argument itself*}
    3.24  apply clarify 
    3.25  apply (erule ssubst)+