author paulson Tue, 09 Jul 2002 10:44:53 +0200 changeset 13319 23de7b3af453 parent 13318 3f475e54875c child 13320 2c6ee189ae63
More Separation proofs
 src/ZF/Constructible/Relative.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Separation.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/WFrec.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:41 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 10:44:53 2002 +0200
@@ -764,9 +764,13 @@
ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
and is_recfun_separation:
-     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
-     "[| M(A); M(f); M(g); M(a); M(b) |]
-     ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
+     --{*for well-founded recursion*}
+     "[| M(r); M(f); M(g); M(a); M(b) |]
+     ==> separation(M,
+            \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
+                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
+                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
+                                   fx \<noteq> gx))"

lemma (in M_axioms) cartprod_iff_lemma:
"[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); ```
```--- a/src/ZF/Constructible/Separation.thy	Tue Jul 09 10:44:41 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Tue Jul 09 10:44:53 2002 +0200
@@ -349,7 +349,7 @@
done

-subsection{*Separation for @{term "well_ord_iso"}*}
+subsection{*Separation for a Theorem about @{term "obase"}*}

lemma obase_equals_reflects:
"REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. ```
```--- a/src/ZF/Constructible/WFrec.thy	Tue Jul 09 10:44:41 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Tue Jul 09 10:44:53 2002 +0200
@@ -64,6 +64,13 @@
apply (blast intro: sym)+
done

+lemma (in M_axioms) is_recfun_separation':
+    "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
+        M(r); M(f); M(g); M(a); M(b) |]
+     ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
+apply (insert is_recfun_separation [of r f g a b])