src/HOL/Fun.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6301 08245f5a436d
child 6829 50459a995aa3
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
    37 Addsimps [id_apply];
    38 
    39 
    40 section "o";
    41 
    42 qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
    43  (K [rtac refl 1]);
    44 Addsimps [o_apply];
    45 
    46 qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    47   (K [rtac ext 1, rtac refl 1]);
    48 
    49 qed_goalw "id_o" thy [id_def] "id o g = g"
    50  (K [rtac ext 1, Simp_tac 1]);
    51 Addsimps [id_o];
    52 
    53 qed_goalw "o_id" thy [id_def] "f o id = f"
    54  (K [rtac ext 1, Simp_tac 1]);
    55 Addsimps [o_id];
    56 
    57 Goalw [o_def] "(f o g)``r = f``(g``r)";
    58 by (Blast_tac 1);
    59 qed "image_compose";
    60 
    61 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
    62 by (Blast_tac 1);
    63 qed "UNION_o";
    64 
    65 
    66 section "inj";
    67 (**NB: inj now just translates to inj_on**)
    68 
    69 (*** inj(f): f is a one-to-one function ***)
    70 
    71 (*for Tools/datatype_rep_proofs*)
    72 val [prem] = Goalw [inj_on_def]
    73     "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
    74 by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
    75 qed "datatype_injI";
    76 
    77 Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    78 by (Blast_tac 1);
    79 qed "injD";
    80 
    81 (*Useful with the simplifier*)
    82 Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
    83 by (rtac iffI 1);
    84 by (etac arg_cong 2);
    85 by (etac injD 1);
    86 by (assume_tac 1);
    87 qed "inj_eq";
    88 
    89 Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
    90 by (etac injD 1);
    91 by (rtac selectI 1);
    92 by (rtac refl 1);
    93 qed "inj_select";
    94 
    95 (*A one-to-one function has an inverse (given using select).*)
    96 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
    97 by (etac inj_select 1);
    98 qed "inv_f_f";
    99 
   100 Addsimps [inv_f_f];
   101 
   102 (* Useful??? *)
   103 val [oneone,minor] = Goal
   104     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
   105 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
   106 by (rtac (rangeI RS minor) 1);
   107 qed "inj_transfer";
   108 
   109 
   110 (*** inj_on f A: f is one-to-one over A ***)
   111 
   112 val prems = Goalw [inj_on_def]
   113     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
   114 by (blast_tac (claset() addIs prems) 1);
   115 qed "inj_onI";
   116 val injI = inj_onI;                  (*for compatibility*)
   117 
   118 val [major] = Goal 
   119     "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
   120 by (rtac inj_onI 1);
   121 by (etac (apply_inverse RS trans) 1);
   122 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   123 qed "inj_on_inverseI";
   124 val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
   125 
   126 Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   127 by (Blast_tac 1);
   128 qed "inj_onD";
   129 
   130 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   131 by (blast_tac (claset() addSDs [inj_onD]) 1);
   132 qed "inj_on_iff";
   133 
   134 Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   135 by (Blast_tac 1);
   136 qed "inj_on_contraD";
   137 
   138 Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   139 by (Blast_tac 1);
   140 qed "subset_inj_on";
   141 
   142 
   143 (** surj **)
   144 
   145 val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
   146 by (blast_tac (claset() addIs [prem RS sym]) 1);
   147 qed "surjI";
   148 
   149 Goalw [surj_def] "surj f ==> range f = UNIV";
   150 by Auto_tac;
   151 qed "surj_range";
   152 
   153 Goalw [surj_def] "surj f ==> EX x. y = f x";
   154 by (Blast_tac 1);
   155 qed "surjD";
   156 
   157 
   158 (*** Lemmas about injective functions and inv ***)
   159 
   160 Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
   161 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
   162 qed "comp_inj_on";
   163 
   164 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
   165 by (fast_tac (claset() addIs [selectI]) 1);
   166 qed "f_inv_f";
   167 
   168 Goal "surj f ==> f(inv f y) = y";
   169 by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
   170 qed "surj_f_inv_f";
   171 
   172 Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
   173 by (rtac (arg_cong RS box_equals) 1);
   174 by (REPEAT (ares_tac [f_inv_f] 1));
   175 qed "inv_injective";
   176 
   177 Goal "A <= range(f) ==> inj_on (inv f) A";
   178 by (fast_tac (claset() addIs [inj_onI] 
   179                        addEs [inv_injective, injD]) 1);
   180 qed "inj_on_inv";
   181 
   182 Goal "surj f ==> inj (inv f)";
   183 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
   184 qed "surj_imp_inj_inv";
   185 
   186 Goal "f``(A Int B) <= f``A Int f``B";
   187 by (Blast_tac 1);
   188 qed "image_Int_subset";
   189 
   190 Goal "f``A - f``B <= f``(A - B)";
   191 by (Blast_tac 1);
   192 qed "image_diff_subset";
   193 
   194 Goalw [inj_on_def]
   195    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
   196 by (Blast_tac 1);
   197 qed "inj_on_image_Int";
   198 
   199 Goalw [inj_on_def]
   200    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   201 by (Blast_tac 1);
   202 qed "inj_on_image_set_diff";
   203 
   204 Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
   205 by (Blast_tac 1);
   206 qed "image_Int";
   207 
   208 Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
   209 by (Blast_tac 1);
   210 qed "image_set_diff";
   211 
   212 Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
   213 by Auto_tac;
   214 qed "inv_image_comp";
   215 
   216 Goal "inj f ==> (f a : f``A) = (a : A)";
   217 by (blast_tac (claset() addDs [injD]) 1);
   218 qed "inj_image_mem_iff";
   219 
   220 Goal "inj f ==> (f``A = f``B) = (A = B)";
   221 by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
   222 qed "inj_image_eq_iff";
   223 
   224 val set_cs = claset() delrules [equalityI];
   225 
   226 
   227 section "fun_upd";
   228 
   229 Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   230 by Safe_tac;
   231 by (etac subst 1);
   232 by (rtac ext 2);
   233 by Auto_tac;
   234 qed "fun_upd_idem_iff";
   235 
   236 (* f x = y ==> f(x:=y) = f *)
   237 bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   238 
   239 (* f(x := f x) = f *)
   240 AddIffs [refl RS fun_upd_idem];
   241 
   242 Goal "(f(x:=y))z = (if z=x then y else f z)";
   243 by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   244 qed "fun_upd_apply";
   245 Addsimps [fun_upd_apply];
   246 
   247 qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
   248 	(K [Simp_tac 1]);
   249 qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
   250 	(K [Asm_simp_tac 1]);
   251 (*Addsimps [fun_upd_same, fun_upd_other];*)
   252 
   253 Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
   254 by (rtac ext 1);
   255 by (Auto_tac);
   256 qed "fun_upd_twist";
   257 
   258 
   259 (*** -> and Pi, by Florian Kammueller and LCP ***)
   260 
   261 val prems = Goalw [Pi_def]
   262 "[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
   263 \    ==> f: Pi A B";
   264 by (auto_tac (claset(), simpset() addsimps prems));
   265 qed "Pi_I";
   266 
   267 val prems = Goal 
   268 "[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
   269 by (blast_tac (claset() addIs Pi_I::prems) 1);
   270 qed "funcsetI";
   271 
   272 Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
   273 by Auto_tac;
   274 qed "Pi_mem";
   275 
   276 Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
   277 by Auto_tac;
   278 qed "funcset_mem";
   279 
   280 Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
   281 by Auto_tac;
   282 qed "apply_arb";
   283 
   284 Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
   285 by (rtac ext 1);
   286 by Auto_tac;
   287 val Pi_extensionality = ballI RSN (3, result());
   288 
   289 (*** compose ***)
   290 
   291 Goalw [Pi_def, compose_def, restrict_def]
   292      "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
   293 by Auto_tac;
   294 qed "funcset_compose";
   295 
   296 Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
   297 \     ==> compose A h (compose A g f) = compose A (compose B h g) f";
   298 by (res_inst_tac [("A","A")] Pi_extensionality 1);
   299 by (blast_tac (claset() addIs [funcset_compose]) 1);
   300 by (blast_tac (claset() addIs [funcset_compose]) 1);
   301 by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
   302 by Auto_tac;
   303 qed "compose_assoc";
   304 
   305 Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
   306 by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   307 qed "compose_eq";
   308 
   309 Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
   310 \     ==> compose A g f `` A = C";
   311 by (auto_tac (claset(),
   312 	      simpset() addsimps [image_def, compose_eq]));
   313 qed "surj_compose";
   314 
   315 
   316 Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
   317 \     ==> inj_on (compose A g f) A";
   318 by (auto_tac (claset(),
   319 	      simpset() addsimps [inj_on_def, compose_eq]));
   320 qed "inj_on_compose";
   321 
   322 
   323 (*** restrict / lam ***)
   324 Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
   325 by (auto_tac (claset(),
   326 	      simpset() addsimps [restrict_def, Pi_def]));
   327 qed "restrict_in_funcset";
   328 
   329 val prems = Goalw [restrict_def, Pi_def]
   330      "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
   331 by (asm_simp_tac (simpset() addsimps prems) 1);
   332 qed "restrictI";
   333 
   334 
   335 Goal "x: A ==> (lam y: A. f y) x = f x";
   336 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   337 qed "restrict_apply1";
   338 
   339 Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
   340 by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
   341 qed "restrict_apply1_mem";
   342 
   343 Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
   344 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   345 qed "restrict_apply2";
   346 
   347 
   348 val prems = Goal
   349     "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
   350 by (rtac ext 1);
   351 by (auto_tac (claset(),
   352 	      simpset() addsimps prems@[restrict_def, Pi_def]));
   353 qed "restrict_ext";
   354 
   355 
   356 (*** Inverse ***)
   357 
   358 Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
   359 by (Blast_tac 1);
   360 qed "surj_image";
   361 
   362 Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
   363 \                ==> (lam x: B. (Inv A f) x) : B funcset A";
   364 by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
   365 qed "Inv_funcset";
   366 
   367 
   368 Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
   369 \     ==> (lam y: B. (Inv A f) y) (f x) = x";
   370 by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
   371 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   372 by (rtac selectI2 1);
   373 by Auto_tac;
   374 qed "Inv_f_f";
   375 
   376 Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
   377 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
   378 by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
   379 by (fast_tac (claset() addIs [selectI2]) 1);
   380 qed "f_Inv_f";
   381 
   382 Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
   383 \     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   384 by (rtac Pi_extensionality 1);
   385 by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
   386 by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
   387 by (asm_simp_tac
   388     (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
   389 qed "compose_Inv_id";
   390 
   391 
   392 (*** Pi and Applyall ***)
   393 
   394 Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   395 by Auto_tac;
   396 qed "Pi_eq_empty";
   397 
   398 Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   399 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   400 qed "Pi_total1";
   401 
   402 Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
   403 by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
   404 by (rename_tac "g z" 1);
   405 by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
   406 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
   407 qed "Applyall_beta";
   408 
   409 Goal "Pi {} B = { (%x. @ y. True) }";
   410 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   411 qed "Pi_empty";
   412 
   413 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
   414 by (auto_tac (claset(),
   415 	      simpset() addsimps [impOfSubs major]));
   416 qed "Pi_mono";