# HG changeset patch
# User paulson
# Date 1005843596 -3600
# Node ID 8213fd95acb56d2688998116e2d20f91f9814784
# Parent  113c1cd7a16439d6f55333dfcfddb88308209dd1
miniscoping of UN and INT

diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/Order.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -536,7 +536,9 @@
 by (ftac ord_iso_restrict_pred 1  THEN
     REPEAT1 (eresolve_tac [asm_rl, predI] 1));
 by (asm_full_simp_tac
-    (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
+    (simpset() addsplits [split_if_asm]
+	       addsimps [well_ord_is_trans_on, trans_pred_pred_eq,
+                         domain_UN, domain_Union]) 1);
 by (Blast_tac 1);
 qed "domain_ord_iso_map_subset";
 
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/QUniv.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -14,7 +14,7 @@
 qed "Transset_includes_summands";
 
 Goalw [sum_def] "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
-by (stac Int_Un_distrib 1);
+by (stac Int_Un_distrib2 1);
 by (blast_tac (claset() addDs [Transset_Pair_D]) 1);
 qed "Transset_sum_Int_subset";
 
@@ -160,7 +160,7 @@
 Goalw [QPair_def,sum_def]
  "Transset(X) ==>          \
 \      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
-by (stac Int_Un_distrib 1);
+by (stac Int_Un_distrib2 1);
 by (rtac Un_mono 1);
 by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
                       [Int_lower1, subset_refl] MRS Sigma_mono] 1));
@@ -190,6 +190,7 @@
 by (rtac (succI1 RS UN_upper) 1);
 (*Limit(i) case*)
 by (asm_simp_tac
-    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, 
+    (simpset() delsimps UN_simps
+	       addsimps [Limit_Vfrom_eq, Int_UN_distrib, 
 			 UN_mono, QPair_Int_Vset_subset_trans]) 1);
 qed "QPair_Int_Vset_subset_UN";
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/equalities.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -42,19 +42,36 @@
 Goal "A Int A = A";
 by (Blast_tac 1);
 qed "Int_absorb";
+Addsimps [Int_absorb];
+
+Goal "A Int (A Int B) = A Int B";
+by (Blast_tac 1);
+qed "Int_left_absorb";
 
 Goal "A Int B = B Int A";
 by (Blast_tac 1);
 qed "Int_commute";
 
+Goal "A Int (B Int C) = B Int (A Int C)";
+by (Blast_tac 1);
+qed "Int_left_commute";
+
 Goal "(A Int B) Int C  =  A Int (B Int C)";
 by (Blast_tac 1);
 qed "Int_assoc";
 
-Goal "(A Un B) Int C  =  (A Int C) Un (B Int C)";
+(*Intersection is an AC-operator*)
+bind_thms ("Int_ac", 
+           [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
+
+Goal "A Int (B Un C) = (A Int B) Un (A Int C)";
 by (Blast_tac 1);
 qed "Int_Un_distrib";
 
+Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
+by (Blast_tac 1);
+qed "Int_Un_distrib2";
+
 Goal "A<=B <-> A Int B = A";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Int_iff";
@@ -76,15 +93,27 @@
 Goal "A Un A = A";
 by (Blast_tac 1);
 qed "Un_absorb";
+Addsimps [Un_absorb];
+
+Goal "A Un (A Un B) = A Un B";
+by (Blast_tac 1);
+qed "Un_left_absorb";
 
 Goal "A Un B = B Un A";
 by (Blast_tac 1);
 qed "Un_commute";
 
+Goal "A Un (B Un C) = B Un (A Un C)";
+by (Blast_tac 1);
+qed "Un_left_commute";
+
 Goal "(A Un B) Un C  =  A Un (B Un C)";
 by (Blast_tac 1);
 qed "Un_assoc";
 
+(*Union is an AC-operator*)
+bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
+
 Goal "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (Blast_tac 1);
 qed "Un_Int_distrib";
@@ -97,19 +126,34 @@
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "subset_Un_iff2";
 
+Goal "(A Un B = 0) <-> (A = 0 & B = 0)";
+by (Blast_tac 1); 
+qed "Un_empty";
+AddIffs[Un_empty];
+
+Goal "A Un B = Union({A, B})";
+by (Blast_tac 1);
+qed "Un_eq_Union";
+
 (** Simple properties of Diff -- set difference **)
 
 Goal "A - A = 0";
 by (Blast_tac 1);
 qed "Diff_cancel";
 
+Goal "A  Int B = 0 ==> A - B = A";
+by (Blast_tac 1);
+qed "Diff_triv";
+
 Goal "0 - A = 0";
 by (Blast_tac 1);
 qed "empty_Diff";
+Addsimps[empty_Diff];
 
 Goal "A - 0 = A";
 by (Blast_tac 1);
 qed "Diff_0";
+Addsimps[Diff_0];
 
 Goal "A - B = 0 <-> A <= B";
 by (blast_tac (claset() addEs [equalityE]) 1);
@@ -158,6 +202,22 @@
 by (Blast_tac 1);
 qed "Diff_Int";
 
+Goal "(A Un B) - C = (A - C) Un (B - C)";
+by (Blast_tac 1);
+qed "Un_Diff";
+
+Goal "(A Int B) - C = A Int (B - C)";
+by (Blast_tac 1);
+qed "Int_Diff";
+
+Goal "C Int (A-B) = (C Int A) - (C Int B)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib";
+
+Goal "(A-B) Int C = (A Int C) - (B Int C)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib2";
+
 (*Halmos, Naive Set Theory, page 16.*)
 Goal "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
 by (blast_tac (claset() addSEs [equalityE]) 1);
@@ -169,6 +229,7 @@
 Goal "Union(cons(a,B)) = a Un Union(B)";
 by (Blast_tac 1);
 qed "Union_cons";
+Addsimps [Union_cons];
 
 Goal "Union(A Un B) = Union(A) Un Union(B)";
 by (Blast_tac 1);
@@ -207,6 +268,12 @@
 by (Blast_tac 1);
 qed "Inter_singleton";
 
+Goal "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"; 
+by (Simp_tac 1);
+by (Blast_tac 1); 
+qed "Inter_cons";
+Addsimps [Inter_cons];
+
 (** Unions and Intersections of Families **)
 
 Goal "Union(A) = (UN x:A. x)";
@@ -220,6 +287,26 @@
 Goal "(UN i:0. A(i)) = 0";
 by (Blast_tac 1);
 qed "UN_0";
+Addsimps [UN_0];
+
+Goal "(UN x:A. {x}) = A";
+by (Blast_tac 1);
+qed "UN_singleton";
+
+Goal "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))";
+by (Blast_tac 1);
+qed "UN_Un";
+
+Goal "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j) \
+\                             else if J=0 then INT i:I. A(i) \
+\                             else ((INT i:I. A(i)) Int  (INT j:J. A(j))))"; 
+by Auto_tac;
+by (blast_tac (claset() addSIs [equalityI]) 1);
+qed "INT_Un";
+
+Goal "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))";
+by (Blast_tac 1);
+qed "UN_UN_flatten";
 
 (*Halmos, Naive Set Theory, page 35.*)
 Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
@@ -250,12 +337,29 @@
 Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
 by (Blast_tac 1);
 qed "UN_RepFun";
+Addsimps [UN_RepFun];
 
-Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
+Goal "(INT x:RepFun(A,f). B(x))    = (INT a:A. B(f(a)))";
+by (auto_tac (claset(), simpset() addsimps [Inter_def])); 
+qed "INT_RepFun";
+Addsimps [INT_RepFun];
+
+Goal "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))";
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1); 
+by (subgoal_tac "ALL x:A. x~=0" 1);
+by (Blast_tac 2);
+by (rtac equalityI 1);   
+by (Clarify_tac 1); 
+by (blast_tac (claset() addIs []) 1); 
+by (blast_tac (claset() addSDs [bspec]) 1);   
+qed "INT_Union_eq";
+
+Goal "(ALL x:A. B(x) ~= 0) \
+\     ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))";
+by (stac INT_Union_eq 1);  
 by (Blast_tac 1);
-qed "INT_RepFun";
-
-Addsimps [UN_RepFun, INT_RepFun];
+by (simp_tac (simpset() addsimps [Inter_def]) 1); 
+qed "INT_UN_eq";
 
 
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
@@ -351,14 +455,17 @@
 Goal "domain(0) = 0";
 by (Blast_tac 1);
 qed "domain_0";
+Addsimps [domain_0];
 
 Goal "domain(cons(<a,b>,r)) = cons(a, domain(r))";
 by (Blast_tac 1);
 qed "domain_cons";
+Addsimps [domain_cons];
 
 Goal "domain(A Un B) = domain(A) Un domain(B)";
 by (Blast_tac 1);
 qed "domain_Un_eq";
+Addsimps [domain_Un_eq];
 
 Goal "domain(A Int B) <= domain(A) Int domain(B)";
 by (Blast_tac 1);
@@ -371,8 +478,15 @@
 Goal "domain(converse(r)) = range(r)";
 by (Blast_tac 1);
 qed "domain_converse";
+Addsimps [domain_converse];
 
-Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse];
+Goal "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))";
+by (Blast_tac 1); 
+qed "domain_UN";
+
+Goal "domain(Union(A)) = (UN x:A. domain(x))";
+by (Blast_tac 1); 
+qed "domain_Union";
 
 
 (** Range **)
@@ -486,15 +600,22 @@
 Goal "r-``0 = 0";
 by (Blast_tac 1);
 qed "vimage_0";
+Addsimps [vimage_0];
 
 Goal "r-``(A Un B) = (r-``A) Un (r-``B)";
 by (Blast_tac 1);
 qed "vimage_Un";
+Addsimps [vimage_Un];
 
 Goal "r-``(A Int B) <= (r-``A) Int (r-``B)";
 by (Blast_tac 1);
 qed "vimage_Int_subset";
 
+(*NOT suitable for rewriting*)
+Goal "f -``B = (UN y:B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
 Goalw [function_def] "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
 by (Blast_tac 1);
 qed "function_vimage_Int";
@@ -515,7 +636,6 @@
 by (Blast_tac 1);
 qed "vimage_Int_square";
 
-Addsimps [vimage_0, vimage_Un];
 
 
 (*Invese image laws for special relations*)
@@ -603,6 +723,13 @@
 Goal "{f(x).x:A}=0 <-> A=0";
 by (Blast_tac 1);
 qed "RepFun_eq_0_iff";
+Addsimps [RepFun_eq_0_iff];
+
+Goal "{c. x:A} = (if A=0 then 0 else {c})";
+by Auto_tac; 
+by (Blast_tac 1);
+qed "RepFun_constant";
+Addsimps [RepFun_constant];
 
 (** Collect **)
 
@@ -623,4 +750,3 @@
 by (simp_tac (simpset() addsplits [split_if]) 1);
 by (Blast_tac 1);
 qed "Collect_cons";
-
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/func.ML
--- a/src/ZF/func.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/func.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -446,4 +446,3 @@
     (asm_simp_tac (simpset() addsimps [restrict, fun_extend_apply1, 
                                       fun_extend_apply2])));
 qed "cons_fun_eq";
-
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/pair.ML
--- a/src/ZF/pair.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/pair.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -186,6 +186,3 @@
 Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
 by (Full_simp_tac 1);
 qed "splitD";
-
-
-
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Nov 15 16:48:05 2001 +0100
+++ b/src/ZF/simpdata.ML	Thu Nov 15 17:59:56 2001 +0100
@@ -6,74 +6,7 @@
 Rewriting for ZF set theory: specialized extraction of rewrites from theorems
 *)
 
-(** Rewriting **)
-
-local
-  (*For proving rewrite rules*)
-  fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1]));
-
-in
-
-val ball_simps = map prover
-    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
-     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
-     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
-     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
-     "(ALL x:0.P(x)) <-> True",
-     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
-     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
-     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
-     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
-     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
-     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
-
-val ball_conj_distrib = 
-    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
-
-val bex_simps = map prover
-    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
-     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
-     "(EX x:0.P(x)) <-> False",
-     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
-     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
-     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
-     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
-     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
-     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
-
-val bex_disj_distrib = 
-    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
-
-val Rep_simps = map prover
-    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
-     "{x:0. P(x)} = 0",		(*Collect*)
-     "{x:A. False} = 0",
-     "{x:A. True} = A",
-     "RepFun(0,f) = 0",		(*RepFun*)
-     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
-     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
-
-val misc_simps = map prover
-    ["0 Un A = A", "A Un 0 = A",
-     "0 Int A = 0", "A Int 0 = 0",
-     "0 - A = 0", "A - 0 = A",
-     "Union(0) = 0",
-     "Union(cons(b,A)) = b Un Union(A)",
-     "Inter({b}) = b"]
-
-end;
-
-bind_thms ("ball_simps", ball_simps);
-bind_thm ("ball_conj_distrib", ball_conj_distrib);
-bind_thms ("bex_simps", bex_simps);
-bind_thm ("bex_disj_distrib", bex_disj_distrib);
-bind_thms ("Rep_simps", Rep_simps);
-bind_thms ("misc_simps", misc_simps);
-
-Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
-
-
-(** New version of mk_rew_rules **)
+(*** New version of mk_rew_rules ***)
 
 (*Should False yield False<->True, or should it solve goals some other way?*)
 
@@ -125,6 +58,130 @@
 
 bind_thms ("if_splits", [split_if, split_if_asm]);
 
+
+(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
+
+local
+  (*For proving rewrite rules*)
+  fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s 
+                  (fn _ => [Simp_tac 1, 
+                            ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
+
+in
+
+val ball_simps = map prover
+    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
+     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
+     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
+     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
+     "(ALL x:0.P(x)) <-> True",
+     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
+     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
+     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
+     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
+     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
+     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
+
+val ball_conj_distrib = 
+    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
+
+val bex_simps = map prover
+    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
+     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
+     "(EX x:0.P(x)) <-> False",
+     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
+     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
+     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
+     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
+     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
+     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
+
+val bex_disj_distrib = 
+    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
+
+val Rep_simps = map prover
+    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
+     "{x:0. P(x)} = 0",		(*Collect*)
+     "{x:A. False} = 0",
+     "{x:A. True} = A",
+     "RepFun(0,f) = 0",		(*RepFun*)
+     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
+     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
+
+val misc_simps = map prover
+    ["0 Un A = A", "A Un 0 = A",
+     "0 Int A = 0", "A Int 0 = 0",
+     "0 - A = 0", "A - 0 = A",
+     "Union(0) = 0",
+     "Union(cons(b,A)) = b Un Union(A)",
+     "Inter({b}) = b"]
+
+
+val UN_simps = map prover 
+    ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
+     "(UN x:C. A(x) Un B)   = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
+     "(UN x:C. A Un B(x))   = (if C=0 then 0 else A Un (UN x:C. B(x)))",
+     "(UN x:C. A(x) Int B)  = ((UN x:C. A(x)) Int B)",
+     "(UN x:C. A Int B(x))  = (A Int (UN x:C. B(x)))",
+     "(UN x:C. A(x) - B)    = ((UN x:C. A(x)) - B)",
+     "(UN x:C. A - B(x))    = (if C=0 then 0 else A - (INT x:C. B(x)))",
+     "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))",
+     "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))",
+     "(UN x: RepFun(A,f). B(x))     = (UN a:A. B(f(a)))"];
+
+val INT_simps = map prover
+    ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B",
+     "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))",
+     "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B",
+     "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))",
+     "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))",
+     "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
+     "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
+
+(** The _extend_simps rules are oriented in the opposite direction, to 
+    pull UN and INT outwards. **)
+
+val UN_extend_simps = map prover 
+    ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
+     "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))",
+     "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))",
+     "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)",
+     "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))",
+     "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)",
+     "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))",
+     "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))",
+     "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))",
+     "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"];
+
+val INT_extend_simps = map prover
+    ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)",
+     "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))",
+     "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)",
+     "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))",
+     "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))",
+     "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))",
+     "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un B(x)))"];
+
+end;
+
+bind_thms ("ball_simps", ball_simps);
+bind_thm ("ball_conj_distrib", ball_conj_distrib);
+bind_thms ("bex_simps", bex_simps);
+bind_thm ("bex_disj_distrib", bex_disj_distrib);
+bind_thms ("Rep_simps", Rep_simps);
+bind_thms ("misc_simps", misc_simps);
+
+Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
+
+bind_thms ("UN_simps", UN_simps);
+bind_thms ("INT_simps", INT_simps);
+
+Addsimps (UN_simps @ INT_simps);
+
+bind_thms ("UN_extend_simps", UN_extend_simps);
+bind_thms ("INT_extend_simps", INT_extend_simps);
+
+
 (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
 
 Goal "(EX x:A. x=a) <-> (a:A)";
@@ -155,6 +212,7 @@
           bex_one_point1,bex_one_point2,
           ball_one_point1,ball_one_point2];
 
+
 let
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
     ("EX x:A. P(x) & Q(x)",FOLogic.oT)
@@ -180,4 +238,5 @@
 
 end;
 
+
 val ZF_ss = simpset();
diff -r 113c1cd7a164 -r 8213fd95acb5 src/ZF/simpdata.thy
--- a/src/ZF/simpdata.thy	Thu Nov 15 16:48:05 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-simpdata = "equalities" + "func"
-