0

1 
(* Title: ZF/func


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Functions in ZermeloFraenkel Set Theory


7 
*)


8 


9 
(*** The Pi operator  dependent function space ***)


10 


11 
val prems = goalw ZF.thy [Pi_def]


12 
"[ f <= Sigma(A,B); !!x. x:A ==> EX! y. <x,y>: f ] ==> \


13 
\ f: Pi(A,B)";


14 
by (REPEAT (ares_tac (prems @ [CollectI,PowI,ballI,impI]) 1));


15 
val PiI = result();


16 


17 
(**Two "destruct" rules for Pi **)


18 


19 
val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";


20 
by (rtac (major RS CollectE) 1);


21 
by (etac PowD 1);


22 
val fun_is_rel = result();


23 


24 
val major::prems = goalw ZF.thy [Pi_def]


25 
"[ f: Pi(A,B); a:A ] ==> EX! y. <a,y>: f";


26 
by (rtac (major RS CollectE) 1);


27 
by (etac bspec 1);


28 
by (resolve_tac prems 1);


29 
val fun_unique_Pair = result();


30 


31 
val prems = goal ZF.thy


32 
"[ f: Pi(A,B); \


33 
\ [ f <= Sigma(A,B); ALL x:A. EX! y. <x,y>: f ] ==> P \


34 
\ ] ==> P";


35 
by (REPEAT (ares_tac (prems@[ballI,fun_is_rel,fun_unique_Pair]) 1));


36 
val PiE = result();


37 


38 
val prems = goalw ZF.thy [Pi_def]


39 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> Pi(A,B) = Pi(A',B')";


40 
by (prove_cong_tac (prems@[Collect_cong,Sigma_cong,ball_cong]) 1);


41 
val Pi_cong = result();


42 


43 
(*Weaking one function type to another*)


44 
goalw ZF.thy [Pi_def] "!!f. [ f: A>B; B<=D ] ==> f: A>D";


45 
by (safe_tac ZF_cs);


46 
by (set_mp_tac 1);


47 
by (fast_tac ZF_cs 1);


48 
val fun_weaken_type = result();


49 


50 
(*Empty function spaces*)


51 
goalw ZF.thy [Pi_def] "Pi(0,A) = {0}";


52 
by (fast_tac (ZF_cs addIs [equalityI]) 1);


53 
val Pi_empty1 = result();


54 


55 
goalw ZF.thy [Pi_def] "!!A a. a:A ==> A>0 = 0";


56 
by (fast_tac (ZF_cs addIs [equalityI]) 1);


57 
val Pi_empty2 = result();


58 


59 


60 
(*** Function Application ***)


61 


62 
goal ZF.thy "!!a b f. [ <a,b>: f; <a,c>: f; f: Pi(A,B) ] ==> b=c";


63 
by (etac PiE 1);


64 
by (etac (bspec RS ex1_equalsE) 1);


65 
by (etac (subsetD RS SigmaD1) 1);


66 
by (REPEAT (assume_tac 1));


67 
val apply_equality2 = result();


68 


69 
goalw ZF.thy [apply_def] "!!a b f. [ <a,b>: f; f: Pi(A,B) ] ==> f`a = b";


70 
by (rtac the_equality 1);


71 
by (rtac apply_equality2 2);


72 
by (REPEAT (assume_tac 1));


73 
val apply_equality = result();


74 


75 
val prems = goal ZF.thy


76 
"[ f: Pi(A,B); c: f; !!x. [ x:A; c = <x,f`x> ] ==> P \


77 
\ ] ==> P";


78 
by (cut_facts_tac prems 1);


79 
by (etac (fun_is_rel RS subsetD RS SigmaE) 1);


80 
by (REPEAT (ares_tac prems 1));


81 
by (hyp_subst_tac 1);


82 
by (etac (apply_equality RS ssubst) 1);


83 
by (resolve_tac prems 1);


84 
by (rtac refl 1);


85 
val memberPiE = result();


86 


87 
(*Conclusion is flexible  use res_inst_tac or else RS with a theorem


88 
of the form f:A>B *)


89 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> f`a : B(a)";


90 
by (rtac (fun_unique_Pair RS ex1E) 1);


91 
by (REPEAT (assume_tac 1));


92 
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);


93 
by (etac (apply_equality RS ssubst) 3);


94 
by (REPEAT (assume_tac 1));


95 
val apply_type = result();


96 


97 
goal ZF.thy "!!f. [ f: Pi(A,B); a:A ] ==> <a,f`a>: f";


98 
by (rtac (fun_unique_Pair RS ex1E) 1);


99 
by (resolve_tac [apply_equality RS ssubst] 3);


100 
by (REPEAT (assume_tac 1));


101 
val apply_Pair = result();


102 


103 
val [major] = goal ZF.thy


104 
"f: Pi(A,B) ==> <a,b>: f <> a:A & f`a = b";


105 
by (rtac (major RS PiE) 1);


106 
by (fast_tac (ZF_cs addSIs [major RS apply_Pair,


107 
major RSN (2,apply_equality)]) 1);


108 
val apply_iff = result();


109 


110 
(*Refining one Pi type to another*)


111 
val prems = goal ZF.thy


112 
"[ f: Pi(A,C); !!x. x:A ==> f`x : B(x) ] ==> f : Pi(A,B)";


113 
by (rtac (subsetI RS PiI) 1);


114 
by (eresolve_tac (prems RL [memberPiE]) 1);


115 
by (etac ssubst 1);


116 
by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1));


117 
val Pi_type = result();


118 


119 


120 
(** Elimination of membership in a function **)


121 


122 
goal ZF.thy "!!a A. [ <a,b> : f; f: Pi(A,B) ] ==> a : A";


123 
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));


124 
val domain_type = result();


125 


126 
goal ZF.thy "!!b B a. [ <a,b> : f; f: Pi(A,B) ] ==> b : B(a)";


127 
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);


128 
by (assume_tac 1);


129 
val range_type = result();


130 


131 
val prems = goal ZF.thy


132 
"[ <a,b>: f; f: Pi(A,B); \


133 
\ [ a:A; b:B(a); f`a = b ] ==> P \


134 
\ ] ==> P";


135 
by (cut_facts_tac prems 1);


136 
by (resolve_tac prems 1);


137 
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));


138 
val Pair_mem_PiE = result();


139 


140 
(*** Lambda Abstraction ***)


141 


142 
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";


143 
by (etac RepFunI 1);


144 
val lamI = result();


145 


146 
val major::prems = goalw ZF.thy [lam_def]


147 
"[ p: (lam x:A. b(x)); !!x.[ x:A; p=<x,b(x)> ] ==> P \


148 
\ ] ==> P";


149 
by (rtac (major RS RepFunE) 1);


150 
by (REPEAT (ares_tac prems 1));


151 
val lamE = result();


152 


153 
goal ZF.thy "!!a b c. [ <a,c>: (lam x:A. b(x)) ] ==> c = b(a)";


154 
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));


155 
val lamD = result();


156 


157 
val prems = goalw ZF.thy [lam_def]


158 
"[ !!x. x:A ==> b(x): B(x) ] ==> (lam x:A.b(x)) : Pi(A,B)";


159 
by (fast_tac (ZF_cs addIs (PiI::prems)) 1);


160 
val lam_type = result();


161 


162 
goal ZF.thy "(lam x:A.b(x)) : A > {b(x). x:A}";


163 
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));


164 
val lam_funtype = result();


165 


166 
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";


167 
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));


168 
val beta = result();


169 


170 
(*congruence rule for lambda abstraction*)


171 
val prems = goalw ZF.thy [lam_def]


172 
"[ A=A'; !!x. x:A' ==> b(x)=b'(x) ] ==> \


173 
\ (lam x:A.b(x)) = (lam x:A'.b'(x))";


174 
by (rtac RepFun_cong 1);


175 
by (res_inst_tac [("t","Pair")] subst_context2 2);


176 
by (REPEAT (ares_tac (prems@[refl]) 1));


177 
val lam_cong = result();


178 


179 
val [major] = goal ZF.thy


180 
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";


181 
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);


182 
by (rtac ballI 1);


183 
by (rtac (beta RS ssubst) 1);


184 
by (assume_tac 1);


185 
by (etac (major RS theI) 1);


186 
val lam_theI = result();


187 


188 


189 
(** Extensionality **)


190 


191 
(*Semiextensionality!*)


192 
val prems = goal ZF.thy


193 
"[ f : Pi(A,B); g: Pi(C,D); A<=C; \


194 
\ !!x. x:A ==> f`x = g`x ] ==> f<=g";


195 
by (rtac subsetI 1);


196 
by (eresolve_tac (prems RL [memberPiE]) 1);


197 
by (etac ssubst 1);


198 
by (resolve_tac (prems RL [ssubst]) 1);


199 
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));


200 
val fun_subset = result();


201 


202 
val prems = goal ZF.thy


203 
"[ f : Pi(A,B); g: Pi(A,D); \


204 
\ !!x. x:A ==> f`x = g`x ] ==> f=g";


205 
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @


206 
[subset_refl,equalityI,fun_subset]) 1));


207 
val fun_extension = result();


208 


209 
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";


210 
by (rtac fun_extension 1);


211 
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));


212 
val eta = result();


213 


214 
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)


215 
val prems = goal ZF.thy


216 
"[ f: Pi(A,B); \


217 
\ !!b. [ ALL x:A. b(x):B(x); f = (lam x:A.b(x)) ] ==> P \


218 
\ ] ==> P";


219 
by (resolve_tac prems 1);


220 
by (rtac (eta RS sym) 2);


221 
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));


222 
val Pi_lamE = result();


223 


224 


225 
(*** properties of "restrict" ***)


226 


227 
goalw ZF.thy [restrict_def,lam_def]


228 
"!!f A. [ f: Pi(C,B); A<=C ] ==> restrict(f,A) <= f";


229 
by (fast_tac (ZF_cs addIs [apply_Pair]) 1);


230 
val restrict_subset = result();


231 


232 
val prems = goalw ZF.thy [restrict_def]


233 
"[ !!x. x:A ==> f`x: B(x) ] ==> restrict(f,A) : Pi(A,B)";


234 
by (rtac lam_type 1);


235 
by (eresolve_tac prems 1);


236 
val restrict_type = result();


237 


238 
val [pi,subs] = goal ZF.thy


239 
"[ f: Pi(C,B); A<=C ] ==> restrict(f,A) : Pi(A,B)";


240 
by (rtac (pi RS apply_type RS restrict_type) 1);


241 
by (etac (subs RS subsetD) 1);


242 
val restrict_type2 = result();


243 


244 
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";


245 
by (etac beta 1);


246 
val restrict = result();


247 


248 
(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*)


249 
val prems = goalw ZF.thy [restrict_def]


250 
"[ A=B; !!x. x:B ==> f`x=g`x ] ==> restrict(f,A) = restrict(g,B)";


251 
by (REPEAT (ares_tac (prems@[lam_cong]) 1));


252 
val restrict_eqI = result();


253 


254 
goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C";


255 
by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1


256 
ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1));


257 
val domain_restrict = result();


258 


259 
val [prem] = goalw ZF.thy [restrict_def]


260 
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";


261 
by (rtac (refl RS lam_cong) 1);


262 
be (prem RS subsetD RS beta) 1; (*easier than calling SIMP_TAC*)


263 
val restrict_lam_eq = result();


264 


265 


266 


267 
(*** Unions of functions ***)


268 


269 
(** The Union of a set of COMPATIBLE functions is a function **)


270 
val [ex_prem,disj_prem] = goal ZF.thy


271 
"[ ALL x:S. EX C D. x:C>D; \


272 
\ !!x y. [ x:S; y:S ] ==> x<=y  y<=x ] ==> \


273 
\ Union(S) : domain(Union(S)) > range(Union(S))";


274 
val premE = ex_prem RS bspec RS exE;


275 
by (REPEAT (eresolve_tac [exE,PiE,premE] 1


276 
ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1));


277 
by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1


278 
ORELSE ares_tac [allI,impI,ex1I,UnionI] 1));


279 
by (res_inst_tac [ ("x1","B") ] premE 1);


280 
by (res_inst_tac [ ("x1","Ba") ] premE 2);


281 
by (REPEAT (eresolve_tac [asm_rl,exE] 1));


282 
by (eresolve_tac [disj_prem RS disjE] 1);


283 
by (DEPTH_SOLVE (set_mp_tac 1


284 
ORELSE eresolve_tac [asm_rl, apply_equality2] 1));


285 
val fun_Union = result();


286 


287 


288 
(** The Union of 2 disjoint functions is a function **)


289 


290 
val prems = goal ZF.thy


291 
"[ f: A>B; g: C>D; A Int C = 0 ] ==> \


292 
\ (f Un g) : (A Un C) > (B Un D)";


293 
(*Contradiction if A Int C = 0, a:A, a:B*)


294 
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));


295 
by (cut_facts_tac prems 1);


296 
by (rtac PiI 1);


297 
(*solve subgoal 2 first!!*)


298 
by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2


299 
INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));


300 
by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));


301 
val fun_disjoint_Un = result();


302 


303 
goal ZF.thy


304 
"!!f g a. [ a:A; f: A>B; g: C>D; A Int C = 0 ] ==> \


305 
\ (f Un g)`a = f`a";


306 
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,


307 
fun_disjoint_Un] 1));


308 
val fun_disjoint_apply1 = result();


309 


310 
goal ZF.thy


311 
"!!f g c. [ c:C; f: A>B; g: C>D; A Int C = 0 ] ==> \


312 
\ (f Un g)`c = g`c";


313 
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,


314 
fun_disjoint_Un] 1));


315 
val fun_disjoint_apply2 = result();


316 


317 
(** Domain and range of a function/relation **)


318 


319 
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";


320 
by (rtac equalityI 1);


321 
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);


322 
by (rtac (major RS PiE) 1);


323 
by (fast_tac ZF_cs 1);


324 
val domain_of_fun = result();


325 


326 
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A>range(f)";


327 
by (rtac (major RS Pi_type) 1);


328 
by (etac (major RS apply_Pair RS rangeI) 1);


329 
val range_of_fun = result();


330 


331 
(*** Extensions of functions ***)


332 


333 
(*Singleton function  in the underlying form of singletons*)


334 
goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) > Upair(b,b)";


335 
by (fast_tac (ZF_cs addIs [PiI]) 1);


336 
val fun_single_lemma = result();


337 


338 
goalw ZF.thy [cons_def]


339 
"!!f A B. [ f: A>B; ~c:A ] ==> cons(<c,b>,f) : cons(c,A) > cons(b,B)";


340 
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);


341 
by (assume_tac 1);


342 
by (rtac equals0I 1);


343 
by (fast_tac ZF_cs 1);


344 
val fun_extend = result();


345 


346 
goal ZF.thy "!!f A B. [ f: A>B; a:A; ~ c:A ] ==> cons(<c,b>,f)`a = f`a";


347 
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);


348 
by (rtac fun_extend 3);


349 
by (REPEAT (assume_tac 1));


350 
val fun_extend_apply1 = result();


351 


352 
goal ZF.thy "!!f A B. [ f: A>B; ~ c:A ] ==> cons(<c,b>,f)`c = b";


353 
by (rtac (consI1 RS apply_equality) 1);


354 
by (rtac fun_extend 1);


355 
by (REPEAT (assume_tac 1));


356 
val fun_extend_apply2 = result();


357 


358 
(*The empty function*)


359 
goal ZF.thy "0: 0>A";


360 
by (fast_tac (ZF_cs addIs [PiI]) 1);


361 
val fun_empty = result();


362 


363 
(*The singleton function*)


364 
goal ZF.thy "{<a,b>} : {a} > cons(b,C)";


365 
by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));


366 
val fun_single = result();


367 
