src/ZF/func.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
     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 Zermelo-Fraenkel 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 (*Semi-extensionality!*)
   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