--- 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";
-
--- 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();