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
```