src/HOL/Fun.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7536 5c094aec523d
child 7876 1b3b683c092e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Fun
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Lemmas about functions.
     7 *)
     8 
     9 
    10 Goal "(f = g) = (! x. f(x)=g(x))";
    11 by (rtac iffI 1);
    12 by (Asm_simp_tac 1);
    13 by (rtac ext 1 THEN Asm_simp_tac 1);
    14 qed "expand_fun_eq";
    15 
    16 val prems = Goal
    17     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    18 by (rtac (arg_cong RS box_equals) 1);
    19 by (REPEAT (resolve_tac (prems@[refl]) 1));
    20 qed "apply_inverse";
    21 
    22 
    23 (** "Axiom" of Choice, proved using the description operator **)
    24 
    25 Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    26 by (fast_tac (claset() addEs [selectI]) 1);
    27 qed "choice";
    28 
    29 Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    30 by (fast_tac (claset() addEs [selectI]) 1);
    31 qed "bchoice";
    32 
    33 
    34 section "id";
    35 
    36 Goalw [id_def] "id x = x";
    37 by (rtac refl 1);
    38 qed "id_apply";
    39 Addsimps [id_apply];
    40 
    41 
    42 section "o";
    43 
    44 Goalw [o_def] "(f o g) x = f (g x)";
    45 by (rtac refl 1);
    46 qed "o_apply";
    47 Addsimps [o_apply];
    48 
    49 Goalw [o_def] "f o (g o h) = f o g o h";
    50 by (rtac ext 1);
    51 by (rtac refl 1);
    52 qed "o_assoc";
    53 
    54 Goalw [id_def] "id o g = g";
    55 by (rtac ext 1);
    56 by (Simp_tac 1);
    57 qed "id_o";
    58 Addsimps [id_o];
    59 
    60 Goalw [id_def] "f o id = f";
    61 by (rtac ext 1);
    62 by (Simp_tac 1);
    63 qed "o_id";
    64 Addsimps [o_id];
    65 
    66 Goalw [o_def] "(f o g)``r = f``(g``r)";
    67 by (Blast_tac 1);
    68 qed "image_compose";
    69 
    70 Goal "f``g``A = (UN x:A. {f (g x)})";
    71 by (Blast_tac 1);
    72 qed "image_image_eq_UN";
    73 
    74 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
    75 by (Blast_tac 1);
    76 qed "UN_o";
    77 
    78 (** lemma for proving injectivity of representation functions for **)
    79 (** datatypes involving function types                            **)
    80 
    81 Goalw [o_def]
    82   "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
    83 by (rtac ext 1);
    84 by (etac allE 1);
    85 by (etac allE 1);
    86 by (etac mp 1);
    87 by (etac fun_cong 1);
    88 qed "inj_fun_lemma";
    89 
    90 
    91 section "inj";
    92 (**NB: inj now just translates to inj_on**)
    93 
    94 (*** inj(f): f is a one-to-one function ***)
    95 
    96 (*for Tools/datatype_rep_proofs*)
    97 val [prem] = Goalw [inj_on_def]
    98     "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
    99 by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
   100 qed "datatype_injI";
   101 
   102 Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
   103 by (Blast_tac 1);
   104 qed "injD";
   105 
   106 (*Useful with the simplifier*)
   107 Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
   108 by (rtac iffI 1);
   109 by (etac arg_cong 2);
   110 by (etac injD 1);
   111 by (assume_tac 1);
   112 qed "inj_eq";
   113 
   114 Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
   115 by (etac injD 1);
   116 by (rtac selectI 1);
   117 by (rtac refl 1);
   118 qed "inj_select";
   119 
   120 (*A one-to-one function has an inverse (given using select).*)
   121 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
   122 by (etac inj_select 1);
   123 qed "inv_f_f";
   124 Addsimps [inv_f_f];
   125 
   126 Goal "[| inj(f);  f x = y |] ==> inv f y = x";
   127 by (etac subst 1);
   128 by (etac inv_f_f 1);
   129 qed "inv_f_eq";
   130 
   131 (* Useful??? *)
   132 val [oneone,minor] = Goal
   133     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
   134 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
   135 by (rtac (rangeI RS minor) 1);
   136 qed "inj_transfer";
   137 
   138 Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
   139 by (rtac ext 1);
   140 by (etac injD 1);
   141 by (etac fun_cong 1);
   142 qed "inj_o";
   143 
   144 (*** inj_on f A: f is one-to-one over A ***)
   145 
   146 val prems = Goalw [inj_on_def]
   147     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
   148 by (blast_tac (claset() addIs prems) 1);
   149 qed "inj_onI";
   150 val injI = inj_onI;                  (*for compatibility*)
   151 
   152 val [major] = Goal 
   153     "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
   154 by (rtac inj_onI 1);
   155 by (etac (apply_inverse RS trans) 1);
   156 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   157 qed "inj_on_inverseI";
   158 val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
   159 
   160 Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   161 by (Blast_tac 1);
   162 qed "inj_onD";
   163 
   164 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   165 by (blast_tac (claset() addSDs [inj_onD]) 1);
   166 qed "inj_on_iff";
   167 
   168 Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   169 by (Blast_tac 1);
   170 qed "inj_on_contraD";
   171 
   172 Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   173 by (Blast_tac 1);
   174 qed "subset_inj_on";
   175 
   176 
   177 (** surj **)
   178 
   179 val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
   180 by (blast_tac (claset() addIs [prem RS sym]) 1);
   181 qed "surjI";
   182 
   183 Goalw [surj_def] "surj f ==> range f = UNIV";
   184 by Auto_tac;
   185 qed "surj_range";
   186 
   187 Goalw [surj_def] "surj f ==> EX x. y = f x";
   188 by (Blast_tac 1);
   189 qed "surjD";
   190 
   191 
   192 (** Bijections **)
   193 
   194 Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
   195 by (Blast_tac 1);
   196 qed "bijI";
   197 
   198 Goalw [bij_def] "bij f ==> inj f";
   199 by (Blast_tac 1);
   200 qed "bij_is_inj";
   201 
   202 Goalw [bij_def] "bij f ==> surj f";
   203 by (Blast_tac 1);
   204 qed "bij_is_surj";
   205 
   206 
   207 (*** Lemmas about injective functions and inv ***)
   208 
   209 Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
   210 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
   211 qed "comp_inj_on";
   212 
   213 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
   214 by (fast_tac (claset() addIs [selectI]) 1);
   215 qed "f_inv_f";
   216 
   217 Goal "surj f ==> f(inv f y) = y";
   218 by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
   219 qed "surj_f_inv_f";
   220 
   221 Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
   222 by (rtac (arg_cong RS box_equals) 1);
   223 by (REPEAT (ares_tac [f_inv_f] 1));
   224 qed "inv_injective";
   225 
   226 Goal "A <= range(f) ==> inj_on (inv f) A";
   227 by (fast_tac (claset() addIs [inj_onI] 
   228                        addEs [inv_injective, injD]) 1);
   229 qed "inj_on_inv";
   230 
   231 Goal "surj f ==> inj (inv f)";
   232 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
   233 qed "surj_imp_inj_inv";
   234 
   235 (** We seem to need both the id-forms and the (%x. x) forms; the latter can
   236     arise by rewriting, while id may be used explicitly. **)
   237 
   238 Goal "(%x. x) `` Y = Y";
   239 by (Blast_tac 1);
   240 qed "image_ident";
   241 
   242 Goalw [id_def] "id `` Y = Y";
   243 by (Blast_tac 1);
   244 qed "image_id";
   245 Addsimps [image_ident, image_id];
   246 
   247 Goal "(%x. x) -`` Y = Y";
   248 by (Blast_tac 1);
   249 qed "vimage_ident";
   250 
   251 Goalw [id_def] "id -`` A = A";
   252 by Auto_tac;
   253 qed "vimage_id";
   254 Addsimps [vimage_ident, vimage_id];
   255 
   256 Goal "f``(A Int B) <= f``A Int f``B";
   257 by (Blast_tac 1);
   258 qed "image_Int_subset";
   259 
   260 Goal "f``A - f``B <= f``(A - B)";
   261 by (Blast_tac 1);
   262 qed "image_diff_subset";
   263 
   264 Goalw [inj_on_def]
   265    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
   266 by (Blast_tac 1);
   267 qed "inj_on_image_Int";
   268 
   269 Goalw [inj_on_def]
   270    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   271 by (Blast_tac 1);
   272 qed "inj_on_image_set_diff";
   273 
   274 Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
   275 by (Blast_tac 1);
   276 qed "image_Int";
   277 
   278 Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
   279 by (Blast_tac 1);
   280 qed "image_set_diff";
   281 
   282 Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
   283 by Auto_tac;
   284 qed "inv_image_comp";
   285 
   286 Goal "inj f ==> (f a : f``A) = (a : A)";
   287 by (blast_tac (claset() addDs [injD]) 1);
   288 qed "inj_image_mem_iff";
   289 
   290 Goal "inj f ==> (f``A = f``B) = (A = B)";
   291 by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
   292 qed "inj_image_eq_iff";
   293 
   294 Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
   295 by (Blast_tac 1);
   296 qed "image_UN";
   297 
   298 (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   299 Goalw [inj_on_def]
   300    "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
   301 \   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
   302 by (Blast_tac 1);
   303 qed "image_INT";
   304 
   305 val set_cs = claset() delrules [equalityI];
   306 
   307 
   308 section "fun_upd";
   309 
   310 Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   311 by Safe_tac;
   312 by (etac subst 1);
   313 by (rtac ext 2);
   314 by Auto_tac;
   315 qed "fun_upd_idem_iff";
   316 
   317 (* f x = y ==> f(x:=y) = f *)
   318 bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   319 
   320 (* f(x := f x) = f *)
   321 AddIffs [refl RS fun_upd_idem];
   322 
   323 Goal "(f(x:=y))z = (if z=x then y else f z)";
   324 by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   325 qed "fun_upd_apply";
   326 Addsimps [fun_upd_apply];
   327 
   328 (*fun_upd_apply supersedes these two*)
   329 Goal "(f(x:=y)) x = y";
   330 by (Simp_tac 1);
   331 qed "fun_upd_same";
   332 
   333 Goal "z~=x ==> (f(x:=y)) z = f z";
   334 by (Asm_simp_tac 1);
   335 qed "fun_upd_other";
   336 
   337 Goal "f(x:=y,x:=z) = f(x:=z)";
   338 by (rtac ext 1);
   339 by (Simp_tac 1);
   340 qed "fun_upd_upd";
   341 Addsimps [fun_upd_upd];
   342 
   343 Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
   344 by (rtac ext 1);
   345 by Auto_tac;
   346 qed "fun_upd_twist";
   347 
   348 
   349 (*** -> and Pi, by Florian Kammueller and LCP ***)
   350 
   351 val prems = Goalw [Pi_def]
   352 "[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
   353 \    ==> f: Pi A B";
   354 by (auto_tac (claset(), simpset() addsimps prems));
   355 qed "Pi_I";
   356 
   357 val prems = Goal 
   358 "[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
   359 by (blast_tac (claset() addIs Pi_I::prems) 1);
   360 qed "funcsetI";
   361 
   362 Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
   363 by Auto_tac;
   364 qed "Pi_mem";
   365 
   366 Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
   367 by Auto_tac;
   368 qed "funcset_mem";
   369 
   370 Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
   371 by Auto_tac;
   372 qed "apply_arb";
   373 
   374 Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
   375 by (rtac ext 1);
   376 by Auto_tac;
   377 val Pi_extensionality = ballI RSN (3, result());
   378 
   379 (*** compose ***)
   380 
   381 Goalw [Pi_def, compose_def, restrict_def]
   382      "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
   383 by Auto_tac;
   384 qed "funcset_compose";
   385 
   386 Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
   387 \     ==> compose A h (compose A g f) = compose A (compose B h g) f";
   388 by (res_inst_tac [("A","A")] Pi_extensionality 1);
   389 by (blast_tac (claset() addIs [funcset_compose]) 1);
   390 by (blast_tac (claset() addIs [funcset_compose]) 1);
   391 by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
   392 by Auto_tac;
   393 qed "compose_assoc";
   394 
   395 Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
   396 by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   397 qed "compose_eq";
   398 
   399 Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
   400 \     ==> compose A g f `` A = C";
   401 by (auto_tac (claset(),
   402 	      simpset() addsimps [image_def, compose_eq]));
   403 qed "surj_compose";
   404 
   405 
   406 Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
   407 \     ==> inj_on (compose A g f) A";
   408 by (auto_tac (claset(),
   409 	      simpset() addsimps [inj_on_def, compose_eq]));
   410 qed "inj_on_compose";
   411 
   412 
   413 (*** restrict / lam ***)
   414 Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
   415 by (auto_tac (claset(),
   416 	      simpset() addsimps [restrict_def, Pi_def]));
   417 qed "restrict_in_funcset";
   418 
   419 val prems = Goalw [restrict_def, Pi_def]
   420      "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
   421 by (asm_simp_tac (simpset() addsimps prems) 1);
   422 qed "restrictI";
   423 
   424 
   425 Goal "x: A ==> (lam y: A. f y) x = f x";
   426 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   427 qed "restrict_apply1";
   428 
   429 Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
   430 by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
   431 qed "restrict_apply1_mem";
   432 
   433 Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
   434 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   435 qed "restrict_apply2";
   436 
   437 
   438 val prems = Goal
   439     "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
   440 by (rtac ext 1);
   441 by (auto_tac (claset(),
   442 	      simpset() addsimps prems@[restrict_def, Pi_def]));
   443 qed "restrict_ext";
   444 
   445 
   446 (*** Inverse ***)
   447 
   448 Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
   449 by (Blast_tac 1);
   450 qed "surj_image";
   451 
   452 Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
   453 \                ==> (lam x: B. (Inv A f) x) : B funcset A";
   454 by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
   455 qed "Inv_funcset";
   456 
   457 
   458 Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
   459 \     ==> (lam y: B. (Inv A f) y) (f x) = x";
   460 by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
   461 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   462 by (rtac selectI2 1);
   463 by Auto_tac;
   464 qed "Inv_f_f";
   465 
   466 Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
   467 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
   468 by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
   469 by (fast_tac (claset() addIs [selectI2]) 1);
   470 qed "f_Inv_f";
   471 
   472 Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
   473 \     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   474 by (rtac Pi_extensionality 1);
   475 by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
   476 by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
   477 by (asm_simp_tac
   478     (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
   479 qed "compose_Inv_id";
   480 
   481 
   482 (*** Pi and Applyall ***)
   483 
   484 Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   485 by Auto_tac;
   486 qed "Pi_eq_empty";
   487 
   488 Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   489 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   490 qed "Pi_total1";
   491 
   492 Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
   493 by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
   494 by (rename_tac "g z" 1);
   495 by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
   496 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
   497 qed "Applyall_beta";
   498 
   499 Goal "Pi {} B = { (%x. @ y. True) }";
   500 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   501 qed "Pi_empty";
   502 
   503 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
   504 by (auto_tac (claset(),
   505 	      simpset() addsimps [impOfSubs major]));
   506 qed "Pi_mono";