src/ZF/func.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     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 (simp_tac (FOL_ss addsimps prems addcongs [Sigma_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 apply_funtype below!*)
    88 goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
    89 by (rtac (fun_unique_Pair RS ex1E) 1);
    90 by (REPEAT (assume_tac 1));
    91 by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
    92 by (etac (apply_equality RS ssubst) 3);
    93 by (REPEAT (assume_tac 1));
    94 val apply_type = result();
    95 
    96 (*This version is acceptable to the simplifier*)
    97 goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
    98 by (REPEAT (ares_tac [apply_type] 1));
    99 val apply_funtype = result();
   100 
   101 goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
   102 by (rtac (fun_unique_Pair RS ex1E) 1);
   103 by (resolve_tac [apply_equality RS ssubst] 3);
   104 by (REPEAT (assume_tac 1));
   105 val apply_Pair = result();
   106 
   107 val [major] = goal ZF.thy
   108     "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
   109 by (rtac (major RS PiE) 1);
   110 by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 
   111 			    major RSN (2,apply_equality)]) 1);
   112 val apply_iff = result();
   113 
   114 (*Refining one Pi type to another*)
   115 val prems = goal ZF.thy
   116     "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
   117 by (rtac (subsetI RS PiI) 1);
   118 by (eresolve_tac (prems RL [memberPiE]) 1);
   119 by (etac ssubst 1);
   120 by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1));
   121 val Pi_type = result();
   122 
   123 
   124 (** Elimination of membership in a function **)
   125 
   126 goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
   127 by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
   128 val domain_type = result();
   129 
   130 goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
   131 by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
   132 by (assume_tac 1);
   133 val range_type = result();
   134 
   135 val prems = goal ZF.thy
   136     "[| <a,b>: f;  f: Pi(A,B);       \
   137 \       [| a:A;  b:B(a);  f`a = b |] ==> P  \
   138 \    |] ==> P";
   139 by (cut_facts_tac prems 1);
   140 by (resolve_tac prems 1);
   141 by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
   142 val Pair_mem_PiE = result();
   143 
   144 (*** Lambda Abstraction ***)
   145 
   146 goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
   147 by (etac RepFunI 1);
   148 val lamI = result();
   149 
   150 val major::prems = goalw ZF.thy [lam_def]
   151     "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
   152 \    |] ==>  P";  
   153 by (rtac (major RS RepFunE) 1);
   154 by (REPEAT (ares_tac prems 1));
   155 val lamE = result();
   156 
   157 goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
   158 by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
   159 val lamD = result();
   160 
   161 val prems = goalw ZF.thy [lam_def]
   162     "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
   163 by (fast_tac (ZF_cs addIs (PiI::prems)) 1);
   164 val lam_type = result();
   165 
   166 goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
   167 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
   168 val lam_funtype = result();
   169 
   170 goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
   171 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
   172 val beta = result();
   173 
   174 (*congruence rule for lambda abstraction*)
   175 val prems = goalw ZF.thy [lam_def] 
   176     "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
   177 by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
   178 val lam_cong = result();
   179 
   180 val [major] = goal ZF.thy
   181     "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
   182 by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
   183 by (rtac ballI 1);
   184 by (rtac (beta RS ssubst) 1);
   185 by (assume_tac 1);
   186 by (etac (major RS theI) 1);
   187 val lam_theI = result();
   188 
   189 
   190 (** Extensionality **)
   191 
   192 (*Semi-extensionality!*)
   193 val prems = goal ZF.thy
   194     "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
   195 \       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
   196 by (rtac subsetI 1);
   197 by (eresolve_tac (prems RL [memberPiE]) 1);
   198 by (etac ssubst 1);
   199 by (resolve_tac (prems RL [ssubst]) 1);
   200 by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
   201 val fun_subset = result();
   202 
   203 val prems = goal ZF.thy
   204     "[| f : Pi(A,B);  g: Pi(A,D);  \
   205 \       !!x. x:A ==> f`x = g`x       |] ==> f=g";
   206 by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
   207 		      [subset_refl,equalityI,fun_subset]) 1));
   208 val fun_extension = result();
   209 
   210 goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
   211 by (rtac fun_extension 1);
   212 by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
   213 val eta = result();
   214 
   215 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
   216 val prems = goal ZF.thy
   217     "[| f: Pi(A,B);        \
   218 \       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
   219 \    |] ==> P";
   220 by (resolve_tac prems 1);
   221 by (rtac (eta RS sym) 2);
   222 by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
   223 val Pi_lamE = result();
   224 
   225 
   226 (*** properties of "restrict" ***)
   227 
   228 goalw ZF.thy [restrict_def,lam_def]
   229     "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
   230 by (fast_tac (ZF_cs addIs [apply_Pair]) 1);
   231 val restrict_subset = result();
   232 
   233 val prems = goalw ZF.thy [restrict_def]
   234     "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
   235 by (rtac lam_type 1);
   236 by (eresolve_tac prems 1);
   237 val restrict_type = result();
   238 
   239 val [pi,subs] = goal ZF.thy 
   240     "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
   241 by (rtac (pi RS apply_type RS restrict_type) 1);
   242 by (etac (subs RS subsetD) 1);
   243 val restrict_type2 = result();
   244 
   245 goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
   246 by (etac beta 1);
   247 val restrict = result();
   248 
   249 (*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
   250 val prems = goalw ZF.thy [restrict_def]
   251     "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
   252 by (REPEAT (ares_tac (prems@[lam_cong]) 1));
   253 val restrict_eqI = result();
   254 
   255 goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C";
   256 by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1
   257      ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1));
   258 val domain_restrict = result();
   259 
   260 val [prem] = goalw ZF.thy [restrict_def]
   261     "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
   262 by (rtac (refl RS lam_cong) 1);
   263 be (prem RS subsetD RS beta) 1;	(*easier than calling simp_tac*)
   264 val restrict_lam_eq = result();
   265 
   266 
   267 
   268 (*** Unions of functions ***)
   269 
   270 (** The Union of a set of COMPATIBLE functions is a function **)
   271 val [ex_prem,disj_prem] = goal ZF.thy
   272     "[| ALL x:S. EX C D. x:C->D; \
   273 \       !!x y. [| x:S;  y:S |] ==> x<=y | y<=x  |] ==>  \
   274 \    Union(S) : domain(Union(S)) -> range(Union(S))";
   275 val premE = ex_prem RS bspec RS exE;
   276 by (REPEAT (eresolve_tac [exE,PiE,premE] 1 
   277      ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1));
   278 by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1 
   279      ORELSE ares_tac [allI,impI,ex1I,UnionI] 1));
   280 by (res_inst_tac [ ("x1","B") ] premE 1);
   281 by (res_inst_tac [ ("x1","Ba") ] premE 2);
   282 by (REPEAT (eresolve_tac [asm_rl,exE] 1));
   283 by (eresolve_tac [disj_prem RS disjE] 1);
   284 by (DEPTH_SOLVE (set_mp_tac 1
   285 		 ORELSE eresolve_tac [asm_rl, apply_equality2] 1));
   286 val fun_Union = result();
   287 
   288 
   289 (** The Union of 2 disjoint functions is a function **)
   290 
   291 val prems = goal ZF.thy
   292     "[| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
   293 \    (f Un g) : (A Un C) -> (B Un D)";
   294      (*Contradiction if A Int C = 0, a:A, a:B*)
   295 val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
   296 by (cut_facts_tac prems 1);
   297 by (rtac PiI 1);
   298 (*solve subgoal 2 first!!*)
   299 by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
   300        INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
   301 by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
   302 val fun_disjoint_Un = result();
   303 
   304 goal ZF.thy
   305     "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   306 \             (f Un g)`a = f`a";
   307 by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,
   308 		      fun_disjoint_Un] 1));
   309 val fun_disjoint_apply1 = result();
   310 
   311 goal ZF.thy
   312     "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   313 \             (f Un g)`c = g`c";
   314 by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,
   315 		      fun_disjoint_Un] 1));
   316 val fun_disjoint_apply2 = result();
   317 
   318 (** Domain and range of a function/relation **)
   319 
   320 val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";
   321 by (rtac equalityI 1);
   322 by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);
   323 by (rtac (major RS PiE) 1);
   324 by (fast_tac ZF_cs 1);
   325 val domain_of_fun = result();
   326 
   327 val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
   328 by (rtac (major RS Pi_type) 1);
   329 by (etac (major RS apply_Pair RS rangeI) 1);
   330 val range_of_fun = result();
   331 
   332 (*** Extensions of functions ***)
   333 
   334 (*Singleton function -- in the underlying form of singletons*)
   335 goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) -> Upair(b,b)";
   336 by (fast_tac (ZF_cs addIs [PiI]) 1);
   337 val fun_single_lemma = result();
   338 
   339 goalw ZF.thy [cons_def]
   340     "!!f A B. [| f: A->B;  ~c:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
   341 by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
   342 by (assume_tac 1);
   343 by (rtac equals0I 1);
   344 by (fast_tac ZF_cs 1);
   345 val fun_extend = result();
   346 
   347 goal ZF.thy "!!f A B. [| f: A->B;  a:A;  ~ c:A |] ==> cons(<c,b>,f)`a = f`a";
   348 by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
   349 by (rtac fun_extend 3);
   350 by (REPEAT (assume_tac 1));
   351 val fun_extend_apply1 = result();
   352 
   353 goal ZF.thy "!!f A B. [| f: A->B;  ~ c:A |] ==> cons(<c,b>,f)`c = b";
   354 by (rtac (consI1 RS apply_equality) 1);
   355 by (rtac fun_extend 1);
   356 by (REPEAT (assume_tac 1));
   357 val fun_extend_apply2 = result();
   358 
   359 (*The empty function*)
   360 goal ZF.thy "0: 0->A";
   361 by (fast_tac (ZF_cs addIs [PiI]) 1);
   362 val fun_empty = result();
   363 
   364 (*The singleton function*)
   365 goal ZF.thy "{<a,b>} : {a} -> cons(b,C)";
   366 by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
   367 val fun_single = result();
   368