# HG changeset patch
# User paulson
# Date 878733127 -3600
# Node ID 4aff9b7e55974372f96530db2c80d945a275ad25
# Parent  47c7490c74feffcf5670469b69681cbd8e01386d
UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves

diff -r 47c7490c74fe -r 4aff9b7e5597 src/HOL/Set.ML
--- 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))";
diff -r 47c7490c74fe -r 4aff9b7e5597 src/HOL/Set.thy
--- 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)}"
 
diff -r 47c7490c74fe -r 4aff9b7e5597 src/HOL/equalities.ML
--- 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);
diff -r 47c7490c74fe -r 4aff9b7e5597 src/HOL/mono.ML
--- 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";
diff -r 47c7490c74fe -r 4aff9b7e5597 src/HOL/subset.ML
--- 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";