UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves
--- a/src/HOL/Set.ML Wed Nov 05 13:29:47 1997 +0100
+++ b/src/HOL/Set.ML Wed Nov 05 13:32:07 1997 +0100
@@ -211,6 +211,29 @@
qed "setup_induction";
+section "The universal set -- UNIV";
+
+qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
+ (fn _ => [rtac CollectI 1, rtac TrueI 1]);
+
+AddIffs [UNIV_I];
+
+qed_goal "subset_UNIV" Set.thy "A <= UNIV"
+ (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
+
+(** Eta-contracting these two rules (to remove P) causes them to be ignored
+ because of their interaction with congruence rules. **)
+
+goalw Set.thy [Ball_def] "Ball UNIV P = All P";
+by (Simp_tac 1);
+qed "ball_UNIV";
+
+goalw Set.thy [Bex_def] "Bex UNIV P = Ex P";
+by (Simp_tac 1);
+qed "bex_UNIV";
+Addsimps [ball_UNIV, bex_UNIV];
+
+
section "The empty set -- {}";
qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
@@ -233,6 +256,21 @@
qed_goal "equals0D" Set.thy "!!a. [| A={}; a:A |] ==> P"
(fn _ => [ (Blast_tac 1) ]);
+goalw Set.thy [Ball_def] "Ball {} P = True";
+by (Simp_tac 1);
+qed "ball_empty";
+
+goalw Set.thy [Bex_def] "Bex {} P = False";
+by (Simp_tac 1);
+qed "bex_empty";
+Addsimps [ball_empty, bex_empty];
+
+goal thy "UNIV ~= {}";
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "UNIV_not_empty";
+AddIffs [UNIV_not_empty];
+
+
section "The Powerset operator -- Pow";
@@ -418,14 +456,6 @@
qed "singleton_conv";
Addsimps [singleton_conv];
-section "The universal set -- UNIV";
-
-qed_goal "UNIV_I" Set.thy "x : UNIV"
- (fn _ => [rtac ComplI 1, etac emptyE 1]);
-
-qed_goal "subset_UNIV" Set.thy "A <= UNIV"
- (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
-
section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
@@ -494,52 +524,6 @@
qed "INT_cong";
-section "Unions over a type; UNION1(B) = Union(range(B))";
-
-goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "UN1_iff";
-
-Addsimps [UN1_iff];
-
-(*The order of the premises presupposes that A is rigid; b may be flexible*)
-goal Set.thy "!!b. b: B(x) ==> b: (UN x. B(x))";
-by (Auto_tac());
-qed "UN1_I";
-
-val major::prems = goalw Set.thy [UNION1_def]
- "[| b : (UN x. B(x)); !!x. b: B(x) ==> R |] ==> R";
-by (rtac (major RS UN_E) 1);
-by (REPEAT (ares_tac prems 1));
-qed "UN1_E";
-
-AddIs [UN1_I];
-AddSEs [UN1_E];
-
-
-section "Intersections over a type; INTER1(B) = Inter(range(B))";
-
-goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "INT1_iff";
-
-Addsimps [INT1_iff];
-
-val prems = goalw Set.thy [INTER1_def]
- "(!!x. b: B(x)) ==> b : (INT x. B(x))";
-by (REPEAT (ares_tac (INT_I::prems) 1));
-qed "INT1_I";
-
-goal Set.thy "!!b. b : (INT x. B(x)) ==> b: B(a)";
-by (Asm_full_simp_tac 1);
-qed "INT1_D";
-
-AddSIs [INT1_I];
-AddDs [INT1_D];
-
-
section "Union";
goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
@@ -662,9 +646,7 @@
(*Each of these has ALREADY been added to simpset() above.*)
val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff,
- mem_Collect_eq,
- UN_iff, UN1_iff, Union_iff,
- INT_iff, INT1_iff, Inter_iff];
+ mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
(*Not for Addsimps -- it can cause goals to blow up!*)
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
--- a/src/HOL/Set.thy Wed Nov 05 13:29:47 1997 +0100
+++ b/src/HOL/Set.thy Wed Nov 05 13:32:07 1997 +0100
@@ -25,14 +25,13 @@
consts
"{}" :: 'a set ("{}")
+ UNIV :: 'a set
insert :: ['a, 'a set] => 'a set
Collect :: ('a => bool) => 'a set (*comprehension*)
Compl :: ('a set) => 'a set (*complement*)
Int :: ['a set, 'a set] => 'a set (infixl 70)
Un :: ['a set, 'a set] => 'a set (infixl 65)
UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*)
- UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10)
- INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10)
Union, Inter :: (('a set) set) => 'a set (*of a set*)
Pow :: 'a set => 'a set set (*powerset*)
range :: ('a => 'b) => 'b set (*of function*)
@@ -47,8 +46,6 @@
syntax
- UNIV :: 'a set
-
(* Infix syntax for non-membership *)
"op ~:" :: ['a, 'a set] => bool ("op ~:")
@@ -61,6 +58,9 @@
(* Big Intersection / Union *)
+ INTER1 :: [pttrns, 'a => 'b set] => 'b set ("(3INT _./ _)" 10)
+ UNION1 :: [pttrns, 'a => 'b set] => 'b set ("(3UN _./ _)" 10)
+
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3INT _:_./ _)" 10)
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10)
@@ -72,14 +72,17 @@
"*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10)
translations
- "UNIV" == "Compl {}"
"range f" == "f``UNIV"
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"
"{x. P}" == "Collect (%x. P)"
+ "UN x y. B" == "UN x. UN y. B"
+ "UN x. B" == "UNION UNIV (%x. B)"
+ "INT x y. B" == "INT x. INT y. B"
+ "INT x. B" == "INTER UNIV (%x. B)"
+ "UN x:A. B" == "UNION A (%x. B)"
"INT x:A. B" == "INTER A (%x. B)"
- "UN x:A. B" == "UNION A (%x. B)"
"! x:A. P" == "Ball A (%x. P)"
"? x:A. P" == "Bex A (%x. P)"
"ALL x:A. P" => "Ball A (%x. P)"
@@ -104,6 +107,8 @@
"op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50)
"UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10)
"INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10)
+ "UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union> _./ _)" 10)
+ "INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter> _./ _)" 10)
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10)
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10)
Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90)
@@ -145,12 +150,11 @@
set_diff_def "A - B == {x. x:A & ~x:B}"
INTER_def "INTER A B == {y. ! x:A. y: B(x)}"
UNION_def "UNION A B == {y. ? x:A. y: B(x)}"
- INTER1_def "INTER1 B == INTER {x. True} B"
- UNION1_def "UNION1 B == UNION {x. True} B"
Inter_def "Inter S == (INT x:S. x)"
Union_def "Union S == (UN x:S. x)"
Pow_def "Pow A == {B. B <= A}"
empty_def "{} == {x. False}"
+ UNIV_def "UNIV == {x. True}"
insert_def "insert a B == {x. x=a} Un B"
image_def "f``A == {y. ? x:A. y=f(x)}"
--- a/src/HOL/equalities.ML Wed Nov 05 13:29:47 1997 +0100
+++ b/src/HOL/equalities.ML Wed Nov 05 13:32:07 1997 +0100
@@ -75,10 +75,6 @@
by (Blast_tac 1);
qed "UN_insert_distrib";
-goal thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
-by (Blast_tac 1);
-qed "UN1_insert_distrib";
-
section "``";
goal thy "f``{} = {}";
@@ -340,8 +336,7 @@
qed"Union_empty_conv";
AddIffs [Union_empty_conv];
-val prems = goal thy
- "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
+goal thy "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "Union_disjoint";
@@ -387,21 +382,11 @@
qed "UN_empty2";
Addsimps[UN_empty2];
-goal thy "(UN x:UNIV. B x) = (UN x. B x)";
-by (Blast_tac 1);
-qed "UN_UNIV";
-Addsimps[UN_UNIV];
-
goal thy "(INT x:{}. B x) = UNIV";
by (Blast_tac 1);
qed "INT_empty";
Addsimps[INT_empty];
-goal thy "(INT x:UNIV. B x) = (INT x. B x)";
-by (Blast_tac 1);
-qed "INT_UNIV";
-Addsimps[INT_UNIV];
-
goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
by (Blast_tac 1);
qed "UN_insert";
@@ -421,10 +406,6 @@
by (Blast_tac 1);
qed "INT_insert_distrib";
-goal thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
-by (Blast_tac 1);
-qed "INT1_insert_distrib";
-
goal thy "Union(B``A) = (UN x:A. B(x))";
by (Blast_tac 1);
qed "Union_image_eq";
@@ -433,23 +414,15 @@
by (Blast_tac 1);
qed "Inter_image_eq";
-goal thy "!!A. a: A ==> (UN y:A. c) = c";
+goal thy "!!A. A~={} ==> (UN y:A. c) = c";
by (Blast_tac 1);
qed "UN_constant";
+Addsimps[UN_constant];
-goal thy "!!A. a: A ==> (INT y:A. c) = c";
+goal thy "!!A. A~={} ==> (INT y:A. c) = c";
by (Blast_tac 1);
qed "INT_constant";
-
-goal thy "(UN x. B) = B";
-by (Blast_tac 1);
-qed "UN1_constant";
-Addsimps[UN1_constant];
-
-goal thy "(INT x. B) = B";
-by (Blast_tac 1);
-qed "INT1_constant";
-Addsimps[INT1_constant];
+Addsimps[INT_constant];
goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
by (Blast_tac 1);
@@ -646,38 +619,24 @@
local
fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
in
-val UN1_simps = map prover
- ["(UN x. insert a (B x)) = insert a (UN x. B x)",
- "(UN x. A x Int B) = ((UN x. A x) Int B)",
- "(UN x. A Int B x) = (A Int (UN x. B x))",
- "(UN x. A x Un B) = ((UN x. A x) Un B)",
- "(UN x. A Un B x) = (A Un (UN x. B x))",
- "(UN x. A x - B) = ((UN x. A x) - B)",
- "(UN x. A - B x) = (A - (INT x. B x))"];
-
-val INT1_simps = map prover
- ["(INT x. insert a (B x)) = insert a (INT x. B x)",
- "(INT x. A x Int B) = ((INT x. A x) Int B)",
- "(INT x. A Int B x) = (A Int (INT x. B x))",
- "(INT x. A x Un B) = ((INT x. A x) Un B)",
- "(INT x. A Un B x) = (A Un (INT x. B x))",
- "(INT x. A x - B) = ((INT x. A x) - B)",
- "(INT x. A - B x) = (A - (UN x. B x))"];
-
val UN_simps = map prover
- ["(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) = (A - (INT x:C. B x))"];
+ ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
+ "!!C. C ~= {} ==> (UN x:C. A x Un B) = ((UN x:C. A x) Un B)",
+ "!!C. C ~= {} ==> (UN x:C. A Un B x) = (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) = (A - (INT x:C. B x))"];
val INT_simps = map prover
- ["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
- "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)",
- "(INT x:C. A Un B x) = (A Un (INT x:C. B x))"];
+ ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
+ "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
+ "!!C. C ~= {} ==> (INT x:C. A x - B) = ((INT x:C. A x) - B)",
+ "!!C. C ~= {} ==> (INT x:C. A - B x) = (A - (UN x:C. B x))",
+ "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
+ "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)",
+ "(INT x:C. A Un B x) = (A Un (INT x:C. B x))"];
-(*The missing laws for bounded Unions and Intersections are conditional
- on the index set's being non-empty. Thus they are probably NOT worth
- adding as default rewrites.*)
val ball_simps = map prover
["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
@@ -711,5 +670,4 @@
end;
-Addsimps (UN1_simps @ INT1_simps @ UN_simps @ INT_simps @
- ball_simps @ bex_simps);
+Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
--- a/src/HOL/mono.ML Wed Nov 05 13:29:47 1997 +0100
+++ b/src/HOL/mono.ML Wed Nov 05 13:32:07 1997 +0100
@@ -28,23 +28,13 @@
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "UN_mono";
-val [prem] = goal Set.thy
- "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
-by (blast_tac (claset() addIs [prem RS subsetD]) 1);
-qed "UN1_mono";
-
+(*The last inclusion is POSITIVE! *)
val prems = goal Set.thy
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (INT x:A. f(x)) <= (INT x:A. g(x))";
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "INT_anti_mono";
-(*The inclusion is POSITIVE! *)
-val [prem] = goal Set.thy
- "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
-by (blast_tac (claset() addIs [prem RS subsetD]) 1);
-qed "INT1_mono";
-
goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
by (Blast_tac 1);
qed "insert_mono";
--- a/src/HOL/subset.ML Wed Nov 05 13:29:47 1997 +0100
+++ b/src/HOL/subset.ML Wed Nov 05 13:32:07 1997 +0100
@@ -42,15 +42,6 @@
by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
qed "UN_least";
-goal Set.thy "B(a) <= (UN x. B(x))";
-by (REPEAT (ares_tac [UN1_I RS subsetI] 1));
-qed "UN1_upper";
-
-val [prem] = goal Set.thy "[| !!x. B(x)<=C |] ==> (UN x. B(x)) <= C";
-by (rtac subsetI 1);
-by (REPEAT (eresolve_tac [asm_rl, UN1_E, prem RS subsetD] 1));
-qed "UN1_least";
-
(*** Big Intersection -- greatest lower bound of a set ***)
@@ -75,16 +66,6 @@
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
qed "INT_greatest";
-goal Set.thy "(INT x. B(x)) <= B(a)";
-by (Blast_tac 1);
-qed "INT1_lower";
-
-val [prem] = goal Set.thy
- "[| !!x. C<=B(x) |] ==> C <= (INT x. B(x))";
-by (rtac (INT1_I RS subsetI) 1);
-by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
-qed "INT1_greatest";
-
(*** Finite Union -- the least upper bound of 2 sets ***)
goal Set.thy "A <= A Un B";