UNIV now a constant; UNION1, INTER1 now translations and no longer have
authorpaulson
Wed Nov 05 13:32:07 1997 +0100 (1997-11-05)
changeset 41594aff9b7e5597
parent 4158 47c7490c74fe
child 4160 59826ea67cba
UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/equalities.ML
src/HOL/mono.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Set.ML	Wed Nov 05 13:29:47 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Nov 05 13:32:07 1997 +0100
     1.3 @@ -211,6 +211,29 @@
     1.4  qed "setup_induction";
     1.5  
     1.6  
     1.7 +section "The universal set -- UNIV";
     1.8 +
     1.9 +qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
    1.10 +  (fn _ => [rtac CollectI 1, rtac TrueI 1]);
    1.11 +
    1.12 +AddIffs [UNIV_I];
    1.13 +
    1.14 +qed_goal "subset_UNIV" Set.thy "A <= UNIV"
    1.15 +  (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
    1.16 +
    1.17 +(** Eta-contracting these two rules (to remove P) causes them to be ignored
    1.18 +    because of their interaction with congruence rules. **)
    1.19 +
    1.20 +goalw Set.thy [Ball_def] "Ball UNIV P = All P";
    1.21 +by (Simp_tac 1);
    1.22 +qed "ball_UNIV";
    1.23 +
    1.24 +goalw Set.thy [Bex_def] "Bex UNIV P = Ex P";
    1.25 +by (Simp_tac 1);
    1.26 +qed "bex_UNIV";
    1.27 +Addsimps [ball_UNIV, bex_UNIV];
    1.28 +
    1.29 +
    1.30  section "The empty set -- {}";
    1.31  
    1.32  qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
    1.33 @@ -233,6 +256,21 @@
    1.34  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.35   (fn _ => [ (Blast_tac 1) ]);
    1.36  
    1.37 +goalw Set.thy [Ball_def] "Ball {} P = True";
    1.38 +by (Simp_tac 1);
    1.39 +qed "ball_empty";
    1.40 +
    1.41 +goalw Set.thy [Bex_def] "Bex {} P = False";
    1.42 +by (Simp_tac 1);
    1.43 +qed "bex_empty";
    1.44 +Addsimps [ball_empty, bex_empty];
    1.45 +
    1.46 +goal thy "UNIV ~= {}";
    1.47 +by (blast_tac (claset() addEs [equalityE]) 1);
    1.48 +qed "UNIV_not_empty";
    1.49 +AddIffs [UNIV_not_empty];
    1.50 +
    1.51 +
    1.52  
    1.53  section "The Powerset operator -- Pow";
    1.54  
    1.55 @@ -418,14 +456,6 @@
    1.56  qed "singleton_conv";
    1.57  Addsimps [singleton_conv];
    1.58  
    1.59 -section "The universal set -- UNIV";
    1.60 -
    1.61 -qed_goal "UNIV_I" Set.thy "x : UNIV"
    1.62 -  (fn _ => [rtac ComplI 1, etac emptyE 1]);
    1.63 -
    1.64 -qed_goal "subset_UNIV" Set.thy "A <= UNIV"
    1.65 -  (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
    1.66 -
    1.67  
    1.68  section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
    1.69  
    1.70 @@ -494,52 +524,6 @@
    1.71  qed "INT_cong";
    1.72  
    1.73  
    1.74 -section "Unions over a type; UNION1(B) = Union(range(B))";
    1.75 -
    1.76 -goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
    1.77 -by (Simp_tac 1);
    1.78 -by (Blast_tac 1);
    1.79 -qed "UN1_iff";
    1.80 -
    1.81 -Addsimps [UN1_iff];
    1.82 -
    1.83 -(*The order of the premises presupposes that A is rigid; b may be flexible*)
    1.84 -goal Set.thy "!!b. b: B(x) ==> b: (UN x. B(x))";
    1.85 -by (Auto_tac());
    1.86 -qed "UN1_I";
    1.87 -
    1.88 -val major::prems = goalw Set.thy [UNION1_def]
    1.89 -    "[| b : (UN x. B(x));  !!x. b: B(x) ==> R |] ==> R";
    1.90 -by (rtac (major RS UN_E) 1);
    1.91 -by (REPEAT (ares_tac prems 1));
    1.92 -qed "UN1_E";
    1.93 -
    1.94 -AddIs  [UN1_I];
    1.95 -AddSEs [UN1_E];
    1.96 -
    1.97 -
    1.98 -section "Intersections over a type; INTER1(B) = Inter(range(B))";
    1.99 -
   1.100 -goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
   1.101 -by (Simp_tac 1);
   1.102 -by (Blast_tac 1);
   1.103 -qed "INT1_iff";
   1.104 -
   1.105 -Addsimps [INT1_iff];
   1.106 -
   1.107 -val prems = goalw Set.thy [INTER1_def]
   1.108 -    "(!!x. b: B(x)) ==> b : (INT x. B(x))";
   1.109 -by (REPEAT (ares_tac (INT_I::prems) 1));
   1.110 -qed "INT1_I";
   1.111 -
   1.112 -goal Set.thy "!!b. b : (INT x. B(x)) ==> b: B(a)";
   1.113 -by (Asm_full_simp_tac 1);
   1.114 -qed "INT1_D";
   1.115 -
   1.116 -AddSIs [INT1_I]; 
   1.117 -AddDs  [INT1_D];
   1.118 -
   1.119 -
   1.120  section "Union";
   1.121  
   1.122  goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
   1.123 @@ -662,9 +646,7 @@
   1.124  
   1.125  (*Each of these has ALREADY been added to simpset() above.*)
   1.126  val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
   1.127 -                 mem_Collect_eq, 
   1.128 -		 UN_iff, UN1_iff, Union_iff, 
   1.129 -		 INT_iff, INT1_iff, Inter_iff];
   1.130 +                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
   1.131  
   1.132  (*Not for Addsimps -- it can cause goals to blow up!*)
   1.133  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
     2.1 --- a/src/HOL/Set.thy	Wed Nov 05 13:29:47 1997 +0100
     2.2 +++ b/src/HOL/Set.thy	Wed Nov 05 13:32:07 1997 +0100
     2.3 @@ -25,14 +25,13 @@
     2.4  
     2.5  consts
     2.6    "{}"          :: 'a set                           ("{}")
     2.7 +  UNIV          :: 'a set
     2.8    insert        :: ['a, 'a set] => 'a set
     2.9    Collect       :: ('a => bool) => 'a set               (*comprehension*)
    2.10    Compl         :: ('a set) => 'a set                   (*complement*)
    2.11    Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    2.12    Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    2.13    UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    2.14 -  UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    2.15 -  INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    2.16    Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    2.17    Pow           :: 'a set => 'a set set                 (*powerset*)
    2.18    range         :: ('a => 'b) => 'b set                 (*of function*)
    2.19 @@ -47,8 +46,6 @@
    2.20  
    2.21  syntax
    2.22  
    2.23 -  UNIV          :: 'a set
    2.24 -
    2.25    (* Infix syntax for non-membership *)
    2.26  
    2.27    "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    2.28 @@ -61,6 +58,9 @@
    2.29  
    2.30    (* Big Intersection / Union *)
    2.31  
    2.32 +  INTER1        :: [pttrns, 'a => 'b set] => 'b set   ("(3INT _./ _)" 10)
    2.33 +  UNION1        :: [pttrns, 'a => 'b set] => 'b set   ("(3UN _./ _)" 10)
    2.34 +
    2.35    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    2.36    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    2.37  
    2.38 @@ -72,14 +72,17 @@
    2.39    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    2.40  
    2.41  translations
    2.42 -  "UNIV"        == "Compl {}"
    2.43    "range f"     == "f``UNIV"
    2.44    "x ~: y"      == "~ (x : y)"
    2.45    "{x, xs}"     == "insert x {xs}"
    2.46    "{x}"         == "insert x {}"
    2.47    "{x. P}"      == "Collect (%x. P)"
    2.48 +  "UN x y. B"   == "UN x. UN y. B"
    2.49 +  "UN x. B"     == "UNION UNIV (%x. B)"
    2.50 +  "INT x y. B"   == "INT x. INT y. B"
    2.51 +  "INT x. B"    == "INTER UNIV (%x. B)"
    2.52 +  "UN x:A. B"   == "UNION A (%x. B)"
    2.53    "INT x:A. B"  == "INTER A (%x. B)"
    2.54 -  "UN x:A. B"   == "UNION A (%x. B)"
    2.55    "! x:A. P"    == "Ball A (%x. P)"
    2.56    "? x:A. P"    == "Bex A (%x. P)"
    2.57    "ALL x:A. P"  => "Ball A (%x. P)"
    2.58 @@ -104,6 +107,8 @@
    2.59    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    2.60    "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    2.61    "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    2.62 +  "UNION1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
    2.63 +  "INTER1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
    2.64    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    2.65    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    2.66    Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    2.67 @@ -145,12 +150,11 @@
    2.68    set_diff_def  "A - B          == {x. x:A & ~x:B}"
    2.69    INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    2.70    UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    2.71 -  INTER1_def    "INTER1 B       == INTER {x. True} B"
    2.72 -  UNION1_def    "UNION1 B       == UNION {x. True} B"
    2.73    Inter_def     "Inter S        == (INT x:S. x)"
    2.74    Union_def     "Union S        == (UN x:S. x)"
    2.75    Pow_def       "Pow A          == {B. B <= A}"
    2.76    empty_def     "{}             == {x. False}"
    2.77 +  UNIV_def      "UNIV           == {x. True}"
    2.78    insert_def    "insert a B     == {x. x=a} Un B"
    2.79    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    2.80  
     3.1 --- a/src/HOL/equalities.ML	Wed Nov 05 13:29:47 1997 +0100
     3.2 +++ b/src/HOL/equalities.ML	Wed Nov 05 13:32:07 1997 +0100
     3.3 @@ -75,10 +75,6 @@
     3.4  by (Blast_tac 1);
     3.5  qed "UN_insert_distrib";
     3.6  
     3.7 -goal thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
     3.8 -by (Blast_tac 1);
     3.9 -qed "UN1_insert_distrib";
    3.10 -
    3.11  section "``";
    3.12  
    3.13  goal thy "f``{} = {}";
    3.14 @@ -340,8 +336,7 @@
    3.15  qed"Union_empty_conv"; 
    3.16  AddIffs [Union_empty_conv];
    3.17  
    3.18 -val prems = goal thy
    3.19 -   "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
    3.20 +goal thy "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
    3.21  by (blast_tac (claset() addSEs [equalityE]) 1);
    3.22  qed "Union_disjoint";
    3.23  
    3.24 @@ -387,21 +382,11 @@
    3.25  qed "UN_empty2";
    3.26  Addsimps[UN_empty2];
    3.27  
    3.28 -goal thy "(UN x:UNIV. B x) = (UN x. B x)";
    3.29 -by (Blast_tac 1);
    3.30 -qed "UN_UNIV";
    3.31 -Addsimps[UN_UNIV];
    3.32 -
    3.33  goal thy "(INT x:{}. B x) = UNIV";
    3.34  by (Blast_tac 1);
    3.35  qed "INT_empty";
    3.36  Addsimps[INT_empty];
    3.37  
    3.38 -goal thy "(INT x:UNIV. B x) = (INT x. B x)";
    3.39 -by (Blast_tac 1);
    3.40 -qed "INT_UNIV";
    3.41 -Addsimps[INT_UNIV];
    3.42 -
    3.43  goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
    3.44  by (Blast_tac 1);
    3.45  qed "UN_insert";
    3.46 @@ -421,10 +406,6 @@
    3.47  by (Blast_tac 1);
    3.48  qed "INT_insert_distrib";
    3.49  
    3.50 -goal thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
    3.51 -by (Blast_tac 1);
    3.52 -qed "INT1_insert_distrib";
    3.53 -
    3.54  goal thy "Union(B``A) = (UN x:A. B(x))";
    3.55  by (Blast_tac 1);
    3.56  qed "Union_image_eq";
    3.57 @@ -433,23 +414,15 @@
    3.58  by (Blast_tac 1);
    3.59  qed "Inter_image_eq";
    3.60  
    3.61 -goal thy "!!A. a: A ==> (UN y:A. c) = c";
    3.62 +goal thy "!!A. A~={} ==> (UN y:A. c) = c";
    3.63  by (Blast_tac 1);
    3.64  qed "UN_constant";
    3.65 +Addsimps[UN_constant];
    3.66  
    3.67 -goal thy "!!A. a: A ==> (INT y:A. c) = c";
    3.68 +goal thy "!!A. A~={} ==> (INT y:A. c) = c";
    3.69  by (Blast_tac 1);
    3.70  qed "INT_constant";
    3.71 -
    3.72 -goal thy "(UN x. B) = B";
    3.73 -by (Blast_tac 1);
    3.74 -qed "UN1_constant";
    3.75 -Addsimps[UN1_constant];
    3.76 -
    3.77 -goal thy "(INT x. B) = B";
    3.78 -by (Blast_tac 1);
    3.79 -qed "INT1_constant";
    3.80 -Addsimps[INT1_constant];
    3.81 +Addsimps[INT_constant];
    3.82  
    3.83  goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
    3.84  by (Blast_tac 1);
    3.85 @@ -646,38 +619,24 @@
    3.86  local
    3.87    fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
    3.88  in
    3.89 -val UN1_simps = map prover 
    3.90 -                ["(UN x. insert a (B x)) = insert a (UN x. B x)",
    3.91 -                 "(UN x. A x Int B)  = ((UN x. A x) Int B)",
    3.92 -                 "(UN x. A Int B x)  = (A Int (UN x. B x))",
    3.93 -                 "(UN x. A x Un B)   = ((UN x. A x) Un B)",
    3.94 -                 "(UN x. A Un B x)   = (A Un (UN x. B x))",
    3.95 -                 "(UN x. A x - B)    = ((UN x. A x) - B)",
    3.96 -                 "(UN x. A - B x)    = (A - (INT x. B x))"];
    3.97 -
    3.98 -val INT1_simps = map prover
    3.99 -                ["(INT x. insert a (B x)) = insert a (INT x. B x)",
   3.100 -                 "(INT x. A x Int B) = ((INT x. A x) Int B)",
   3.101 -                 "(INT x. A Int B x) = (A Int (INT x. B x))",
   3.102 -                 "(INT x. A x Un B)  = ((INT x. A x) Un B)",
   3.103 -                 "(INT x. A Un B x)  = (A Un (INT x. B x))",
   3.104 -                 "(INT x. A x - B)   = ((INT x. A x) - B)",
   3.105 -                 "(INT x. A - B x)   = (A - (UN x. B x))"];
   3.106 -
   3.107  val UN_simps = map prover 
   3.108 -                ["(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
   3.109 -                 "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
   3.110 -                 "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
   3.111 -                 "(UN x:C. A - B x)    = (A - (INT x:C. B x))"];
   3.112 +    ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
   3.113 +     "!!C. C ~= {} ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
   3.114 +     "!!C. C ~= {} ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
   3.115 +     "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
   3.116 +     "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
   3.117 +     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
   3.118 +     "(UN x:C. A - B x)    = (A - (INT x:C. B x))"];
   3.119  
   3.120  val INT_simps = map prover
   3.121 -                ["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
   3.122 -                 "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
   3.123 -                 "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))"];
   3.124 +    ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
   3.125 +     "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
   3.126 +     "!!C. C ~= {} ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
   3.127 +     "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
   3.128 +     "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
   3.129 +     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
   3.130 +     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))"];
   3.131  
   3.132 -(*The missing laws for bounded Unions and Intersections are conditional
   3.133 -  on the index set's being non-empty.  Thus they are probably NOT worth 
   3.134 -  adding as default rewrites.*)
   3.135  
   3.136  val ball_simps = map prover
   3.137      ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
   3.138 @@ -711,5 +670,4 @@
   3.139  
   3.140  end;
   3.141  
   3.142 -Addsimps (UN1_simps @ INT1_simps @ UN_simps @ INT_simps @ 
   3.143 -	  ball_simps @ bex_simps);
   3.144 +Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
     4.1 --- a/src/HOL/mono.ML	Wed Nov 05 13:29:47 1997 +0100
     4.2 +++ b/src/HOL/mono.ML	Wed Nov 05 13:32:07 1997 +0100
     4.3 @@ -28,23 +28,13 @@
     4.4  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
     4.5  qed "UN_mono";
     4.6  
     4.7 -val [prem] = goal Set.thy
     4.8 -    "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
     4.9 -by (blast_tac (claset() addIs [prem RS subsetD]) 1);
    4.10 -qed "UN1_mono";
    4.11 -
    4.12 +(*The last inclusion is POSITIVE! *)
    4.13  val prems = goal Set.thy
    4.14      "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
    4.15  \    (INT x:A. f(x)) <= (INT x:A. g(x))";
    4.16  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
    4.17  qed "INT_anti_mono";
    4.18  
    4.19 -(*The inclusion is POSITIVE! *)
    4.20 -val [prem] = goal Set.thy
    4.21 -    "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
    4.22 -by (blast_tac (claset() addIs [prem RS subsetD]) 1);
    4.23 -qed "INT1_mono";
    4.24 -
    4.25  goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
    4.26  by (Blast_tac 1);
    4.27  qed "insert_mono";
     5.1 --- a/src/HOL/subset.ML	Wed Nov 05 13:29:47 1997 +0100
     5.2 +++ b/src/HOL/subset.ML	Wed Nov 05 13:32:07 1997 +0100
     5.3 @@ -42,15 +42,6 @@
     5.4  by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
     5.5  qed "UN_least";
     5.6  
     5.7 -goal Set.thy "B(a) <= (UN x. B(x))";
     5.8 -by (REPEAT (ares_tac [UN1_I RS subsetI] 1));
     5.9 -qed "UN1_upper";
    5.10 -
    5.11 -val [prem] = goal Set.thy "[| !!x. B(x)<=C |] ==> (UN x. B(x)) <= C";
    5.12 -by (rtac subsetI 1);
    5.13 -by (REPEAT (eresolve_tac [asm_rl, UN1_E, prem RS subsetD] 1));
    5.14 -qed "UN1_least";
    5.15 -
    5.16  
    5.17  (*** Big Intersection -- greatest lower bound of a set ***)
    5.18  
    5.19 @@ -75,16 +66,6 @@
    5.20  by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
    5.21  qed "INT_greatest";
    5.22  
    5.23 -goal Set.thy "(INT x. B(x)) <= B(a)";
    5.24 -by (Blast_tac 1);
    5.25 -qed "INT1_lower";
    5.26 -
    5.27 -val [prem] = goal Set.thy
    5.28 -    "[| !!x. C<=B(x) |] ==> C <= (INT x. B(x))";
    5.29 -by (rtac (INT1_I RS subsetI) 1);
    5.30 -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
    5.31 -qed "INT1_greatest";
    5.32 -
    5.33  (*** Finite Union -- the least upper bound of 2 sets ***)
    5.34  
    5.35  goal Set.thy "A <= A Un B";