src/ZF/subset.ML
author lcp
Thu, 03 Nov 1994 12:30:55 +0100
changeset 689 bf95dada47ac
parent 0 a5a9c433f639
child 760 f0200e91b272
permissions -rw-r--r--
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/subset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Derived rules involving subsets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Union and Intersection as lattice operations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
(*** cons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
val cons_subsetI = prove_goal ZF.thy "[| a:C; B<=C |] ==> cons(a,B) <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
    (REPEAT (ares_tac [subsetI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
     ORELSE eresolve_tac  [consE,ssubst,subsetD] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
val subset_consI = prove_goal ZF.thy "B <= cons(a,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
 (fn _=> [ (rtac subsetI 1), (etac consI2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(*Useful for rewriting!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val cons_subset_iff = prove_goal ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 (fn _=> [ (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
(*A safe special case of subset elimination, adding no new variables 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val subset_empty_iff = prove_goal ZF.thy "A<=0 <-> A=0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
 (fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val subset_cons_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
 (fn _=> [ (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*** succ ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val subset_succI = prove_goal ZF.thy "i <= succ(i)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 (fn _=> [ (rtac subsetI 1), (etac succI2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(*But if j is an ordinal or is transitive, then i:j implies i<=j! 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  See ordinal/Ord_succ_subsetI*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val succ_subsetI = prove_goalw ZF.thy [succ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    "[| i:j;  i<=j |] ==> succ(i)<=j"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  [ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val succ_subsetE = prove_goalw ZF.thy [succ_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  [ (rtac (major RS cons_subsetE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*** singletons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val singleton_subsetI = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "a:C ==> {a} <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  [ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val singleton_subsetD = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    "{a} <= C  ==>  a:C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
 (fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*** Big Union -- least upper bound of a set  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val Union_subset_iff = prove_goal ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val Union_upper = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "B:A ==> B <= Union(A)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
 (fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val Union_least = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(*** Union of a family of sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val subset_UN_iff_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val UN_subset_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
     "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val UN_upper = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    "!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
 (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val UN_least = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
(*** Big Intersection -- greatest lower bound of a nonempty set ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val Inter_subset_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
     "!!a A. a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val Inter_lower = prove_goal ZF.thy "B:A ==> Inter(A) <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
  [ (REPEAT (resolve_tac (prems@[subsetI]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
     ORELSE etac InterD 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val Inter_greatest = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
    "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
 (fn [prem1,prem2]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    (etac prem2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*** Intersection of a family of sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val INT_lower = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    "x:A ==> (INT x:A.B(x)) <= B(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
 (fn [prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  [ rtac (prem RS RepFunI RS Inter_lower) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val INT_greatest = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A.B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 (fn [nonempty,prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
  [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*** Finite Union -- the least upper bound of 2 sets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val Un_subset_iff = prove_goal ZF.thy "A Un B <= C <-> A <= C & B <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Un_upper1 = prove_goal ZF.thy "A <= A Un B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val Un_upper2 = prove_goal ZF.thy "B <= A Un B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
val Un_least = prove_goal ZF.thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  [ (rtac (Un_subset_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    (REPEAT (ares_tac [conjI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
val Int_subset_iff = prove_goal ZF.thy "C <= A Int B <-> C <= A & C <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val Int_lower1 = prove_goal ZF.thy "A Int B <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
val Int_lower2 = prove_goal ZF.thy "A Int B <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
val Int_greatest = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
                             "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
  [ (rtac (Int_subset_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
    (REPEAT (ares_tac [conjI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*** Set difference *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
val Diff_subset = prove_goal ZF.thy "A-B <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
val Diff_contains = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
    "[| C<=A;  C Int B = 0 |] ==> C <= A-B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
    (rtac subsetI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
    (REPEAT (ares_tac [DiffI,IntI,notI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
     ORELSE eresolve_tac [subsetD,equals0D] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
(** Collect **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val Collect_subset = prove_goal ZF.thy "Collect(A,P) <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
(** RepFun **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
by (etac RepFunE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
val RepFun_subset = result();
689
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   192
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   193
(*A more powerful claset for subset reasoning*)
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   194
val subset_cs = subset0_cs 
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   195
  addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   196
	  Inter_greatest,Int_greatest,RepFun_subset]
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   197
  addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   198
  addIs  [Union_upper,Inter_lower]
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   199
  addSEs [cons_subsetE];
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   200