--- a/src/ZF/Constructible/Separation.thy Wed Jul 31 14:39:47 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy Wed Jul 31 14:40:40 2002 +0200
@@ -1,3 +1,9 @@
+(* Title: ZF/Constructible/Separation.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
+
header{*Early Instances of Separation and Strong Replacement*}
theory Separation = L_axioms + WF_absolute:
@@ -69,6 +75,26 @@
apply (simp_all add: succ_Un_distrib [symmetric])
done
+subsection{*Separation for Set Difference*}
+
+lemma Diff_Reflects:
+ "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]"
+by (intro FOL_reflections)
+
+lemma Diff_separation:
+ "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
+apply (rule separation_CollectI)
+apply (rule_tac A="{B,z}" in subset_LsetE, blast )
+apply (rule ReflectsE [OF Diff_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+ apply (simp_all add: lt_Ord2, clarify)
+apply (rule DPow_LsetI)
+apply (rule not_iff_sats)
+apply (rule_tac env="[x,B]" in mem_iff_sats)
+apply (rule sep_rules | simp)+
+done
+
subsection{*Separation for Cartesian Product*}
lemma cartprod_Reflects:
@@ -448,19 +474,21 @@
text{*Separation (and Strong Replacement) for basic set-theoretic constructions
such as intersection, Cartesian Product and image.*}
-theorem M_axioms_L: "PROP M_axioms(L)"
- apply (rule M_axioms.intro)
- apply (rule M_triv_axioms_L)
+lemma M_axioms_axioms_L: "M_axioms_axioms(L)"
apply (rule M_axioms_axioms.intro)
- apply (assumption | rule
- Inter_separation cartprod_separation image_separation
- converse_separation restrict_separation
- comp_separation pred_separation Memrel_separation
- funspace_succ_replacement well_ord_iso_separation
- obase_separation obase_equals_separation
- omap_replacement is_recfun_separation)+
+ apply (assumption | rule
+ Inter_separation Diff_separation cartprod_separation image_separation
+ converse_separation restrict_separation
+ comp_separation pred_separation Memrel_separation
+ funspace_succ_replacement well_ord_iso_separation
+ obase_separation obase_equals_separation
+ omap_replacement is_recfun_separation)+
done
+theorem M_axioms_L: "PROP M_axioms(L)"
+by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L])
+
+
lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
and sum_closed = M_axioms.sum_closed [OF M_axioms_L]