# HG changeset patch
# User paulson
# Date 1025862464 -7200
# Node ID 43ef6c6dd9065d7fc27c61e955cb3671421bc71a
# Parent  60301202f91b5548961f7c834140e36629f03c9b
more separation instances

diff -r 60301202f91b -r 43ef6c6dd906 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 11:44:20 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 11:47:44 2002 +0200
@@ -619,43 +619,67 @@
 apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
+subsubsection{*Separation for Predecessors in an Order*}
+
+lemma pred_Reflects:
+     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
+                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"
+by fast
+
+lemma pred_separation:
+     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
+apply (rule separation_CollectI) 
+apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF pred_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2, clarify)
+apply (rule DPowI2)
+apply (rename_tac u) 
+apply (rule bex_iff_sats)
+apply (rule conj_iff_sats)
+apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI, simp) 
+apply (rule pair_iff_sats)
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI, simp_all)
+apply (simp_all add: succ_Un_distrib [symmetric])
+done
+
+
+subsubsection{*Separation for the Membership Relation*}
+
+lemma Memrel_Reflects:
+     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
+            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"
+by fast
+
+lemma Memrel_separation:
+     "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
+apply (rule separation_CollectI) 
+apply (rule_tac A="{z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Memrel_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (rule DPowI2)
+apply (rename_tac u) 
+apply (rule bex_iff_sats)+
+apply (rule conj_iff_sats)
+apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI, simp_all) 
+apply (rule mem_iff_sats)
+apply (blast intro: nth_0 nth_ConsI) 
+apply (blast intro: nth_0 nth_ConsI)
+apply (simp_all add: succ_Un_distrib [symmetric])
+done
+
+
 
 
 
 end
-
-(*
-
-  and pred_separation:
-     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
-  and Memrel_separation:
-     "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
-  and obase_separation:
-     --{*part of the order type formalization*}
-     "[| L(A); L(r) |] 
-      ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
-	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
-	     order_isomorphism(L,par,r,x,mx,g))"
-  and well_ord_iso_separation:
-     "[| L(A); L(f); L(r) |] 
-      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
-		     fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
-  and obase_equals_separation:
-     "[| L(A); L(r) |] 
-      ==> separation
-      (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
-	      ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
-	      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
-	      order_isomorphism(L,pxr,r,y,my,g)))))"
-  and is_recfun_separation:
-     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
-     "[| L(A); L(f); L(g); L(a); L(b) |] 
-     ==> separation(L, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
-  and omap_replacement:
-     "[| L(A); L(r) |] 
-      ==> strong_replacement(L,
-             \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
-	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
-	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
-
-*)
\ No newline at end of file