0

1 
(* Title: ZF/subset


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Derived rules involving subsets


7 
Union and Intersection as lattice operations


8 
*)


9 


10 
(*** cons ***)


11 


12 
val cons_subsetI = prove_goal ZF.thy "[ a:C; B<=C ] ==> cons(a,B) <= C"


13 
(fn prems=>


14 
[ (cut_facts_tac prems 1),


15 
(REPEAT (ares_tac [subsetI] 1


16 
ORELSE eresolve_tac [consE,ssubst,subsetD] 1)) ]);


17 


18 
val subset_consI = prove_goal ZF.thy "B <= cons(a,B)"


19 
(fn _=> [ (rtac subsetI 1), (etac consI2 1) ]);


20 


21 
(*Useful for rewriting!*)


22 
val cons_subset_iff = prove_goal ZF.thy "cons(a,B)<=C <> a:C & B<=C"


23 
(fn _=> [ (fast_tac upair_cs 1) ]);


24 


25 
(*A safe special case of subset elimination, adding no new variables


26 
[ cons(a,B) <= C; [ a : C; B <= C ] ==> R ] ==> R *)


27 
val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE);


28 


29 
val subset_empty_iff = prove_goal ZF.thy "A<=0 <> A=0"


30 
(fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);


31 


32 
val subset_cons_iff = prove_goal ZF.thy


33 
"C<=cons(a,B) <> C<=B  (a:C & C{a} <= B)"


34 
(fn _=> [ (fast_tac upair_cs 1) ]);


35 


36 
(*** succ ***)


37 


38 
val subset_succI = prove_goal ZF.thy "i <= succ(i)"


39 
(fn _=> [ (rtac subsetI 1), (etac succI2 1) ]);


40 


41 
(*But if j is an ordinal or is transitive, then i:j implies i<=j!


42 
See ordinal/Ord_succ_subsetI*)


43 
val succ_subsetI = prove_goalw ZF.thy [succ_def]


44 
"[ i:j; i<=j ] ==> succ(i)<=j"


45 
(fn prems=>


46 
[ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]);


47 


48 
val succ_subsetE = prove_goalw ZF.thy [succ_def]


49 
"[ succ(i) <= j; [ i:j; i<=j ] ==> P \


50 
\ ] ==> P"


51 
(fn major::prems=>


52 
[ (rtac (major RS cons_subsetE) 1),


53 
(REPEAT (ares_tac prems 1)) ]);


54 


55 
(*** singletons ***)


56 


57 
val singleton_subsetI = prove_goal ZF.thy


58 
"a:C ==> {a} <= C"


59 
(fn prems=>


60 
[ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]);


61 


62 
val singleton_subsetD = prove_goal ZF.thy


63 
"{a} <= C ==> a:C"


64 
(fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]);


65 


66 
(*** Big Union  least upper bound of a set ***)


67 


68 
val Union_subset_iff = prove_goal ZF.thy "Union(A) <= C <> (ALL x:A. x <= C)"


69 
(fn _ => [ fast_tac upair_cs 1 ]);


70 


71 
val Union_upper = prove_goal ZF.thy


72 
"B:A ==> B <= Union(A)"


73 
(fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]);


74 


75 
val Union_least = prove_goal ZF.thy


76 
"[ !!x. x:A ==> x<=C ] ==> Union(A) <= C"


77 
(fn [prem]=>


78 
[ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),


79 
(etac prem 1) ]);


80 


81 
(*** Union of a family of sets ***)


82 


83 
goal ZF.thy "A <= (UN i:I. B(i)) <> A = (UN i:I. A Int B(i))";


84 
by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1);


85 
val subset_UN_iff_eq = result();


86 


87 
val UN_subset_iff = prove_goal ZF.thy


88 
"(UN x:A.B(x)) <= C <> (ALL x:A. B(x) <= C)"


89 
(fn _ => [ fast_tac upair_cs 1 ]);


90 


91 
val UN_upper = prove_goal ZF.thy


92 
"!!x A. x:A ==> B(x) <= (UN x:A.B(x))"


93 
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]);


94 


95 
val UN_least = prove_goal ZF.thy


96 
"[ !!x. x:A ==> B(x)<=C ] ==> (UN x:A.B(x)) <= C"


97 
(fn [prem]=>


98 
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),


99 
(etac prem 1) ]);


100 


101 


102 
(*** Big Intersection  greatest lower bound of a nonempty set ***)


103 


104 
val Inter_subset_iff = prove_goal ZF.thy


105 
"!!a A. a: A ==> C <= Inter(A) <> (ALL x:A. C <= x)"


106 
(fn _ => [ fast_tac upair_cs 1 ]);


107 


108 
val Inter_lower = prove_goal ZF.thy "B:A ==> Inter(A) <= B"


109 
(fn prems=>


110 
[ (REPEAT (resolve_tac (prems@[subsetI]) 1


111 
ORELSE etac InterD 1)) ]);


112 


113 
val Inter_greatest = prove_goal ZF.thy


114 
"[ a:A; !!x. x:A ==> C<=x ] ==> C <= Inter(A)"


115 
(fn [prem1,prem2]=>


116 
[ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),


117 
(etac prem2 1) ]);


118 


119 
(*** Intersection of a family of sets ***)


120 


121 
val INT_lower = prove_goal ZF.thy


122 
"x:A ==> (INT x:A.B(x)) <= B(x)"


123 
(fn [prem] =>


124 
[ rtac (prem RS RepFunI RS Inter_lower) 1 ]);


125 


126 
val INT_greatest = prove_goal ZF.thy


127 
"[ a:A; !!x. x:A ==> C<=B(x) ] ==> C <= (INT x:A.B(x))"


128 
(fn [nonempty,prem] =>


129 
[ rtac (nonempty RS RepFunI RS Inter_greatest) 1,


130 
REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);


131 


132 


133 
(*** Finite Union  the least upper bound of 2 sets ***)


134 


135 
val Un_subset_iff = prove_goal ZF.thy "A Un B <= C <> A <= C & B <= C"


136 
(fn _ => [ fast_tac upair_cs 1 ]);


137 


138 
val Un_upper1 = prove_goal ZF.thy "A <= A Un B"


139 
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]);


140 


141 
val Un_upper2 = prove_goal ZF.thy "B <= A Un B"


142 
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]);


143 


144 
val Un_least = prove_goal ZF.thy "!!A B C. [ A<=C; B<=C ] ==> A Un B <= C"


145 
(fn _ =>


146 
[ (rtac (Un_subset_iff RS iffD2) 1),


147 
(REPEAT (ares_tac [conjI] 1)) ]);


148 


149 
(*** Finite Intersection  the greatest lower bound of 2 sets *)


150 


151 
val Int_subset_iff = prove_goal ZF.thy "C <= A Int B <> C <= A & C <= B"


152 
(fn _ => [ fast_tac upair_cs 1 ]);


153 


154 
val Int_lower1 = prove_goal ZF.thy "A Int B <= A"


155 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);


156 


157 
val Int_lower2 = prove_goal ZF.thy "A Int B <= B"


158 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);


159 


160 
val Int_greatest = prove_goal ZF.thy


161 
"!!A B C. [ C<=A; C<=B ] ==> C <= A Int B"


162 
(fn prems=>


163 
[ (rtac (Int_subset_iff RS iffD2) 1),


164 
(REPEAT (ares_tac [conjI] 1)) ]);


165 


166 
(*** Set difference *)


167 


168 
val Diff_subset = prove_goal ZF.thy "AB <= A"


169 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);


170 


171 
val Diff_contains = prove_goal ZF.thy


172 
"[ C<=A; C Int B = 0 ] ==> C <= AB"


173 
(fn prems=>


174 
[ (cut_facts_tac prems 1),


175 
(rtac subsetI 1),


176 
(REPEAT (ares_tac [DiffI,IntI,notI] 1


177 
ORELSE eresolve_tac [subsetD,equals0D] 1)) ]);


178 


179 
(** Collect **)


180 


181 
val Collect_subset = prove_goal ZF.thy "Collect(A,P) <= A"


182 
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]);


183 


184 
(** RepFun **)


185 


186 
val prems = goal ZF.thy "[ !!x. x:A ==> f(x): B ] ==> {f(x). x:A} <= B";


187 
by (rtac subsetI 1);


188 
by (etac RepFunE 1);


189 
by (etac ssubst 1);


190 
by (eresolve_tac prems 1);


191 
val RepFun_subset = result();

689

192 


193 
(*A more powerful claset for subset reasoning*)


194 
val subset_cs = subset0_cs


195 
addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,


196 
Inter_greatest,Int_greatest,RepFun_subset]


197 
addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]


198 
addIs [Union_upper,Inter_lower]


199 
addSEs [cons_subsetE];


200 
