0

1 
(* Title: ZF/domrange


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Converse, domain, range of a relation or function


7 
*)


8 


9 
(*** converse ***)


10 


11 
val converseI = prove_goalw ZF.thy [converse_def]


12 
"!!a b r. <a,b>:r ==> <b,a>:converse(r)"


13 
(fn _ => [ (fast_tac pair_cs 1) ]);


14 


15 
val converseD = prove_goalw ZF.thy [converse_def]


16 
"!!a b r. <a,b> : converse(r) ==> <b,a> : r"


17 
(fn _ => [ (fast_tac pair_cs 1) ]);


18 


19 
val converseE = prove_goalw ZF.thy [converse_def]


20 
"[ yx : converse(r); \


21 
\ !!x y. [ yx=<y,x>; <x,y>:r ] ==> P \


22 
\ ] ==> P"


23 
(fn [major,minor]=>


24 
[ (rtac (major RS ReplaceE) 1),


25 
(REPEAT (eresolve_tac [exE, conjE, minor] 1)),


26 
(hyp_subst_tac 1),


27 
(assume_tac 1) ]);


28 


29 
val converse_cs = pair_cs addSIs [converseI]


30 
addSEs [converseD,converseE];


31 


32 
val converse_of_converse = prove_goal ZF.thy


33 
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"


34 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);


35 


36 
val converse_type = prove_goal ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"


37 
(fn _ => [ (fast_tac converse_cs 1) ]);


38 


39 
val converse_of_prod = prove_goal ZF.thy "converse(A*B) = B*A"


40 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);


41 


42 
val converse_empty = prove_goal ZF.thy "converse(0) = 0"


43 
(fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);


44 


45 
(*** domain ***)


46 


47 
val domain_iff = prove_goalw ZF.thy [domain_def]


48 
"a: domain(r) <> (EX y. <a,y>: r)"


49 
(fn _=> [ (fast_tac pair_cs 1) ]);


50 


51 
val domainI = prove_goal ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"


52 
(fn _ => [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);


53 


54 
val domainE = prove_goal ZF.thy


55 
"[ a : domain(r); !!y. <a,y>: r ==> P ] ==> P"


56 
(fn prems=>


57 
[ (rtac (domain_iff RS iffD1 RS exE) 1),


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


59 


60 
val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"


61 
(fn _ =>


62 
[ (REPEAT (eresolve_tac [domainE,SigmaE2] 1


63 
ORELSE ares_tac [domainI,equalityI,subsetI,SigmaI] 1)) ]);


64 


65 
val domain_empty = prove_goal ZF.thy "domain(0) = 0"


66 
(fn _ =>


67 
[ (REPEAT (eresolve_tac [domainE,emptyE] 1


68 
ORELSE ares_tac [equalityI,subsetI] 1)) ]);


69 


70 
val domain_subset = prove_goal ZF.thy "domain(Sigma(A,B)) <= A"


71 
(fn _ =>


72 
[ (rtac subsetI 1),


73 
(etac domainE 1),


74 
(etac SigmaD1 1) ]);


75 


76 


77 
(*** range ***)


78 


79 
val rangeI = prove_goalw ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"


80 
(fn _ => [ (etac (converseI RS domainI) 1) ]);


81 


82 
val rangeE = prove_goalw ZF.thy [range_def]


83 
"[ b : range(r); !!x. <x,b>: r ==> P ] ==> P"


84 
(fn major::prems=>


85 
[ (rtac (major RS domainE) 1),


86 
(resolve_tac prems 1),


87 
(etac converseD 1) ]);


88 


89 
val range_of_prod = prove_goalw ZF.thy [range_def]


90 
"!!a A B. a:A ==> range(A*B) = B"


91 
(fn _ =>


92 
[ (rtac (converse_of_prod RS ssubst) 1),


93 
(etac domain_of_prod 1) ]);


94 


95 
val range_empty = prove_goalw ZF.thy [range_def] "range(0) = 0"


96 
(fn _ =>


97 
[ (rtac (converse_empty RS ssubst) 1),


98 
(rtac domain_empty 1) ]);


99 


100 
val range_subset = prove_goalw ZF.thy [range_def] "range(A*B) <= B"


101 
(fn _ =>


102 
[ (rtac (converse_of_prod RS ssubst) 1),


103 
(rtac domain_subset 1) ]);


104 


105 


106 
(*** field ***)


107 


108 
val fieldI1 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> a : field(r)"


109 
(fn [prem]=>


110 
[ (rtac (prem RS domainI RS UnI1) 1) ]);


111 


112 
val fieldI2 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> b : field(r)"


113 
(fn [prem]=>


114 
[ (rtac (prem RS rangeI RS UnI2) 1) ]);


115 


116 
val fieldCI = prove_goalw ZF.thy [field_def]


117 
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"


118 
(fn [prem]=>


119 
[ (rtac (prem RS domainI RS UnCI) 1),


120 
(swap_res_tac [rangeI] 1),


121 
(etac notnotD 1) ]);


122 


123 
val fieldE = prove_goalw ZF.thy [field_def]


124 
"[ a : field(r); \


125 
\ !!x. <a,x>: r ==> P; \


126 
\ !!x. <x,a>: r ==> P ] ==> P"


127 
(fn major::prems=>


128 
[ (rtac (major RS UnE) 1),


129 
(REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);


130 


131 
val field_of_prod = prove_goal ZF.thy "field(A*A) = A"


132 
(fn _ =>


133 
[ (fast_tac (pair_cs addIs [fieldCI,equalityI] addSEs [fieldE]) 1) ]);


134 


135 
val field_subset = prove_goal ZF.thy "field(A*B) <= A Un B"


136 
(fn _ => [ (fast_tac (pair_cs addIs [fieldCI] addSEs [fieldE]) 1) ]);


137 


138 
val domain_subset_field = prove_goalw ZF.thy [field_def]


139 
"domain(r) <= field(r)"


140 
(fn _ => [ (rtac Un_upper1 1) ]);


141 


142 
val range_subset_field = prove_goalw ZF.thy [field_def]


143 
"range(r) <= field(r)"


144 
(fn _ => [ (rtac Un_upper2 1) ]);


145 


146 
val domain_times_range = prove_goal ZF.thy


147 
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"


148 
(fn _ => [ (fast_tac (pair_cs addIs [domainI,rangeI]) 1) ]);


149 


150 
val field_times_field = prove_goal ZF.thy


151 
"!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"


152 
(fn _ => [ (fast_tac (pair_cs addIs [fieldI1,fieldI2]) 1) ]);


153 


154 


155 
(*** Image of a set under a function/relation ***)


156 


157 
val image_iff = prove_goalw ZF.thy [image_def]


158 
"b : r``A <> (EX x:A. <x,b>:r)"


159 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);


160 


161 
val image_singleton_iff = prove_goal ZF.thy


162 
"b : r``{a} <> <a,b>:r"


163 
(fn _ => [ rtac (image_iff RS iff_trans) 1,


164 
fast_tac pair_cs 1 ]);


165 


166 
val imageI = prove_goalw ZF.thy [image_def]


167 
"!!a b r. [ <a,b>: r; a:A ] ==> b : r``A"


168 
(fn _ => [ (REPEAT (ares_tac [CollectI,rangeI,bexI] 1)) ]);


169 


170 
val imageE = prove_goalw ZF.thy [image_def]


171 
"[ b: r``A; !!x.[ <x,b>: r; x:A ] ==> P ] ==> P"


172 
(fn major::prems=>


173 
[ (rtac (major RS CollectE) 1),


174 
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);


175 


176 
val image_subset = prove_goal ZF.thy


177 
"!!A B r. [ r <= A*B; C<=A ] ==> r``C <= B"


178 
(fn _ =>


179 
[ (rtac subsetI 1),


180 
(REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);


181 


182 


183 
(*** Inverse image of a set under a function/relation ***)


184 


185 
val vimage_iff = prove_goalw ZF.thy [vimage_def,image_def,converse_def]


186 
"a : r``B <> (EX y:B. <a,y>:r)"


187 
(fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);


188 


189 
val vimage_singleton_iff = prove_goal ZF.thy


190 
"a : r``{b} <> <a,b>:r"


191 
(fn _ => [ rtac (vimage_iff RS iff_trans) 1,


192 
fast_tac pair_cs 1 ]);


193 


194 
val vimageI = prove_goalw ZF.thy [vimage_def]


195 
"!!A B r. [ <a,b>: r; b:B ] ==> a : r``B"


196 
(fn _ => [ (REPEAT (ares_tac [converseI RS imageI] 1)) ]);


197 


198 
val vimageE = prove_goalw ZF.thy [vimage_def]


199 
"[ a: r``B; !!x.[ <a,x>: r; x:B ] ==> P ] ==> P"


200 
(fn major::prems=>


201 
[ (rtac (major RS imageE) 1),


202 
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);


203 


204 
val vimage_subset = prove_goalw ZF.thy [vimage_def]


205 
"!!A B r. [ r <= A*B; C<=B ] ==> r``C <= A"


206 
(fn _ => [ (REPEAT (ares_tac [converse_type RS image_subset] 1)) ]);


207 


208 


209 
(** Theoremproving for ZF set theory **)


210 


211 
val ZF_cs = pair_cs


212 
addSIs [converseI]


213 
addIs [imageI, vimageI, domainI, rangeI, fieldCI]


214 
addSEs [imageE, vimageE, domainE, rangeE, fieldE, converseD, converseE];


215 


216 
val eq_cs = ZF_cs addSIs [equalityI];


217 


218 
(** The Union of a set of relations is a relation  Lemma for fun_Union **)


219 
goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==> \


220 
\ Union(S) <= domain(Union(S)) * range(Union(S))";


221 
by (fast_tac ZF_cs 1);


222 
val rel_Union = result();


223 


224 
(** The Union of 2 relations is a relation (Lemma for fun_Un) **)


225 
val rel_Un = prove_goal ZF.thy


226 
"!!r s. [ r <= A*B; s <= C*D ] ==> (r Un s) <= (A Un C) * (B Un D)"


227 
(fn _ => [ (fast_tac ZF_cs 1) ]);


228 


229 
