src/HOL/Fun.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10832 e33b47e4246d
child 11395 2eeaa1077b73
permissions -rw-r--r--
improved theory reference in comment
     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 Goal "(f = g) = (! x. f(x)=g(x))";
    10 by (rtac iffI 1);
    11 by (Asm_simp_tac 1);
    12 by (rtac ext 1 THEN Asm_simp_tac 1);
    13 qed "expand_fun_eq";
    14 
    15 val prems = Goal
    16     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    17 by (rtac (arg_cong RS box_equals) 1);
    18 by (REPEAT (resolve_tac (prems@[refl]) 1));
    19 qed "apply_inverse";
    20 
    21 
    22 (** "Axiom" of Choice, proved using the description operator **)
    23 
    24 (*"choice" is now proved in Tools/meson.ML*)
    25 
    26 Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    27 by (fast_tac (claset() addEs [someI]) 1);
    28 qed "bchoice";
    29 
    30 
    31 section "id";
    32 
    33 Goalw [id_def] "id x = x";
    34 by (rtac refl 1);
    35 qed "id_apply";
    36 Addsimps [id_apply];
    37 
    38 Goal "inv id = id";
    39 by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
    40 qed "inv_id";
    41 Addsimps [inv_id];
    42 
    43 
    44 section "o";
    45 
    46 Goalw [o_def] "(f o g) x = f (g x)";
    47 by (rtac refl 1);
    48 qed "o_apply";
    49 Addsimps [o_apply];
    50 
    51 Goalw [o_def] "f o (g o h) = f o g o h";
    52 by (rtac ext 1);
    53 by (rtac refl 1);
    54 qed "o_assoc";
    55 
    56 Goalw [id_def] "id o g = g";
    57 by (rtac ext 1);
    58 by (Simp_tac 1);
    59 qed "id_o";
    60 Addsimps [id_o];
    61 
    62 Goalw [id_def] "f o id = f";
    63 by (rtac ext 1);
    64 by (Simp_tac 1);
    65 qed "o_id";
    66 Addsimps [o_id];
    67 
    68 Goalw [o_def] "(f o g)`r = f`(g`r)";
    69 by (Blast_tac 1);
    70 qed "image_compose";
    71 
    72 Goal "f`A = (UN x:A. {f x})";
    73 by (Blast_tac 1);
    74 qed "image_eq_UN";
    75 
    76 Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
    77 by (Blast_tac 1);
    78 qed "UN_o";
    79 
    80 (** lemma for proving injectivity of representation functions for **)
    81 (** datatypes involving function types                            **)
    82 
    83 Goalw [o_def]
    84   "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
    85 by (rtac ext 1);
    86 by (etac allE 1);
    87 by (etac allE 1);
    88 by (etac mp 1);
    89 by (etac fun_cong 1);
    90 qed "inj_fun_lemma";
    91 
    92 
    93 section "inj";
    94 (**NB: inj now just translates to inj_on**)
    95 
    96 (*** inj(f): f is a one-to-one function ***)
    97 
    98 (*for Tools/datatype_rep_proofs*)
    99 val [prem] = Goalw [inj_on_def]
   100     "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
   101 by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
   102 qed "datatype_injI";
   103 
   104 Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
   105 by (Blast_tac 1);
   106 qed "injD";
   107 
   108 (*Useful with the simplifier*)
   109 Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
   110 by (rtac iffI 1);
   111 by (etac arg_cong 2);
   112 by (etac injD 1);
   113 by (assume_tac 1);
   114 qed "inj_eq";
   115 
   116 (*A one-to-one function has an inverse (given using select).*)
   117 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
   118 by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
   119 qed "inv_f_f";
   120 Addsimps [inv_f_f];
   121 
   122 Goal "[| inj(f);  f x = y |] ==> inv f y = x";
   123 by (etac subst 1);
   124 by (etac inv_f_f 1);
   125 qed "inv_f_eq";
   126 
   127 Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
   128 by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
   129 qed "inj_imp_inv_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 bind_thm ("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 bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
   159 
   160 Goal "(inj f) = (inv f o f = id)";
   161 by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
   162 by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
   163 qed "inj_iff";
   164 
   165 Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   166 by (Blast_tac 1);
   167 qed "inj_onD";
   168 
   169 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   170 by (blast_tac (claset() addSDs [inj_onD]) 1);
   171 qed "inj_on_iff";
   172 
   173 Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   174 by (Blast_tac 1);
   175 qed "inj_on_contraD";
   176 
   177 Goal "inj (%s. {s})";
   178 by (rtac injI 1);
   179 by (etac singleton_inject 1);
   180 qed "inj_singleton";
   181 
   182 Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   183 by (Blast_tac 1);
   184 qed "subset_inj_on";
   185 
   186 
   187 (** surj **)
   188 
   189 val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
   190 by (blast_tac (claset() addIs [prem RS sym]) 1);
   191 qed "surjI";
   192 
   193 Goalw [surj_def] "surj f ==> range f = UNIV";
   194 by Auto_tac;
   195 qed "surj_range";
   196 
   197 Goalw [surj_def] "surj f ==> EX x. y = f x";
   198 by (Blast_tac 1);
   199 qed "surjD";
   200 
   201 Goal "inj f ==> surj (inv f)";
   202 by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
   203 qed "inj_imp_surj_inv";
   204 
   205 
   206 (*** Lemmas about injective functions and inv ***)
   207 
   208 Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
   209 by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
   210 qed "comp_inj_on";
   211 
   212 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
   213 by (fast_tac (claset() addIs [someI]) 1);
   214 qed "f_inv_f";
   215 
   216 Goal "surj f ==> f(inv f y) = y";
   217 by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
   218 qed "surj_f_inv_f";
   219 
   220 Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
   221 by (rtac (arg_cong RS box_equals) 1);
   222 by (REPEAT (ares_tac [f_inv_f] 1));
   223 qed "inv_injective";
   224 
   225 Goal "A <= range(f) ==> inj_on (inv f) A";
   226 by (fast_tac (claset() addIs [inj_onI] 
   227                        addEs [inv_injective, injD]) 1);
   228 qed "inj_on_inv";
   229 
   230 Goal "surj f ==> inj (inv f)";
   231 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
   232 qed "surj_imp_inj_inv";
   233 
   234 Goal "(surj f) = (f o inv f = id)";
   235 by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
   236 by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
   237 qed "surj_iff";
   238 
   239 Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
   240 by (rtac ext 1);
   241 by (dres_inst_tac [("x","inv f x")] spec 1); 
   242 by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
   243 qed "surj_imp_inv_eq";
   244 
   245 
   246 (** Bijections **)
   247 
   248 Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
   249 by (Blast_tac 1);
   250 qed "bijI";
   251 
   252 Goalw [bij_def] "bij f ==> inj f";
   253 by (Blast_tac 1);
   254 qed "bij_is_inj";
   255 
   256 Goalw [bij_def] "bij f ==> surj f";
   257 by (Blast_tac 1);
   258 qed "bij_is_surj";
   259 
   260 Goalw [bij_def] "bij f ==> bij (inv f)";
   261 by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
   262 qed "bij_imp_bij_inv";
   263 
   264 val prems = 
   265 Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
   266 by (rtac ext 1);
   267 by (auto_tac (claset(), simpset() addsimps prems));
   268 qed "inv_equality";
   269 
   270 Goalw [bij_def] "bij f ==> inv (inv f) = f";
   271 by (rtac inv_equality 1);
   272 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
   273 qed "inv_inv_eq";
   274 
   275 (** bij(inv f) implies little about f.  Consider f::bool=>bool such that
   276     f(True)=f(False)=True.  Then it's consistent with axiom someI that
   277     inv(f) could be any function at all, including the identity function.
   278     If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
   279     inv(inv(f))=f all fail.
   280 **)
   281 
   282 Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
   283 by (rtac (inv_equality) 1);
   284 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
   285 qed "o_inv_distrib";
   286 
   287 
   288 (** We seem to need both the id-forms and the (%x. x) forms; the latter can
   289     arise by rewriting, while id may be used explicitly. **)
   290 
   291 Goal "(%x. x) ` Y = Y";
   292 by (Blast_tac 1);
   293 qed "image_ident";
   294 
   295 Goalw [id_def] "id ` Y = Y";
   296 by (Blast_tac 1);
   297 qed "image_id";
   298 Addsimps [image_ident, image_id];
   299 
   300 Goal "(%x. x) -` Y = Y";
   301 by (Blast_tac 1);
   302 qed "vimage_ident";
   303 
   304 Goalw [id_def] "id -` A = A";
   305 by Auto_tac;
   306 qed "vimage_id";
   307 Addsimps [vimage_ident, vimage_id];
   308 
   309 Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
   310 by (blast_tac (claset() addIs [sym]) 1);
   311 qed "vimage_image_eq";
   312 
   313 Goal "f ` (f -` A) <= A";
   314 by (Blast_tac 1);
   315 qed "image_vimage_subset";
   316 
   317 Goal "f ` (f -` A) = A Int range f";
   318 by (Blast_tac 1);
   319 qed "image_vimage_eq";
   320 Addsimps [image_vimage_eq];
   321 
   322 Goal "surj f ==> f ` (f -` A) = A";
   323 by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
   324 qed "surj_image_vimage_eq";
   325 
   326 Goal "surj f ==> f ` (inv f ` A) = A";
   327 by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
   328 qed "image_surj_f_inv_f";
   329 
   330 Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
   331 by (Blast_tac 1);
   332 qed "inj_vimage_image_eq";
   333 
   334 Goal "inj f ==> (inv f) ` (f ` A) = A";
   335 by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
   336 qed "image_inv_f_f";
   337 
   338 Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
   339 by (blast_tac (claset() addIs [sym]) 1);
   340 qed "vimage_subsetD";
   341 
   342 Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
   343 by (Blast_tac 1);
   344 qed "vimage_subsetI";
   345 
   346 Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
   347 by (blast_tac (claset() delrules [subsetI]
   348 			addIs [vimage_subsetI, vimage_subsetD]) 1);
   349 qed "vimage_subset_eq";
   350 
   351 Goal "f`(A Int B) <= f`A Int f`B";
   352 by (Blast_tac 1);
   353 qed "image_Int_subset";
   354 
   355 Goal "f`A - f`B <= f`(A - B)";
   356 by (Blast_tac 1);
   357 qed "image_diff_subset";
   358 
   359 Goalw [inj_on_def]
   360    "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B";
   361 by (Blast_tac 1);
   362 qed "inj_on_image_Int";
   363 
   364 Goalw [inj_on_def]
   365    "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B";
   366 by (Blast_tac 1);
   367 qed "inj_on_image_set_diff";
   368 
   369 Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
   370 by (Blast_tac 1);
   371 qed "image_Int";
   372 
   373 Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
   374 by (Blast_tac 1);
   375 qed "image_set_diff";
   376 
   377 Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
   378 by Auto_tac;
   379 qed "inv_image_comp";
   380 
   381 Goal "inj f ==> (f a : f`A) = (a : A)";
   382 by (blast_tac (claset() addDs [injD]) 1);
   383 qed "inj_image_mem_iff";
   384 
   385 Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
   386 by (Blast_tac 1);
   387 qed "inj_image_subset_iff";
   388 
   389 Goal "inj f ==> (f`A = f`B) = (A = B)";
   390 by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
   391 qed "inj_image_eq_iff";
   392 
   393 Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
   394 by (Blast_tac 1);
   395 qed "image_UN";
   396 
   397 (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   398 Goalw [inj_on_def]
   399    "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
   400 \   ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   401 by (Blast_tac 1);
   402 qed "image_INT";
   403 
   404 (*Compare with image_INT: no use of inj_on, and if f is surjective then
   405   it doesn't matter whether A is empty*)
   406 Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   407 by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
   408 	       simpset()) 1);
   409 qed "bij_image_INT";
   410 
   411 Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
   412 by Auto_tac;
   413 by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
   414 by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
   415 qed "bij_image_Collect_eq";
   416 
   417 Goal "bij f ==> f -` A = inv f ` A";
   418 by Safe_tac;
   419 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
   420 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
   421 qed "bij_vimage_eq_inv_image";
   422 
   423 Goal "surj f ==> -(f`A) <= f`(-A)";
   424 by (auto_tac (claset(), simpset() addsimps [surj_def]));  
   425 qed "surj_Compl_image_subset";
   426 
   427 Goal "inj f ==> f`(-A) <= -(f`A)";
   428 by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
   429 qed "inj_image_Compl_subset";
   430 
   431 Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
   432 by (rtac equalityI 1); 
   433 by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
   434                                                 surj_Compl_image_subset]))); 
   435 qed "bij_image_Compl_eq";
   436 
   437 val set_cs = claset() delrules [equalityI];
   438 
   439 
   440 section "fun_upd";
   441 
   442 Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   443 by Safe_tac;
   444 by (etac subst 1);
   445 by (rtac ext 2);
   446 by Auto_tac;
   447 qed "fun_upd_idem_iff";
   448 
   449 (* f x = y ==> f(x:=y) = f *)
   450 bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   451 
   452 (* f(x := f x) = f *)
   453 AddIffs [refl RS fun_upd_idem];
   454 
   455 Goal "(f(x:=y))z = (if z=x then y else f z)";
   456 by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   457 qed "fun_upd_apply";
   458 Addsimps [fun_upd_apply];
   459 
   460 (* fun_upd_apply supersedes these two,   but they are useful 
   461    if fun_upd_apply is intentionally removed from the simpset *)
   462 Goal "(f(x:=y)) x = y";
   463 by (Simp_tac 1);
   464 qed "fun_upd_same";
   465 
   466 Goal "z~=x ==> (f(x:=y)) z = f z";
   467 by (Asm_simp_tac 1);
   468 qed "fun_upd_other";
   469 
   470 Goal "f(x:=y,x:=z) = f(x:=z)";
   471 by (rtac ext 1);
   472 by (Simp_tac 1);
   473 qed "fun_upd_upd";
   474 Addsimps [fun_upd_upd];
   475 
   476 (* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
   477 local 
   478   fun gen_fun_upd  None    T _ _ = None
   479   |   gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
   480   fun dest_fun_T1 (Type (_,T::Ts)) = T
   481   fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let
   482       fun find         (Const ("Fun.fun_upd",T) $ g $ v $ w) = 
   483           if v aconv x then Some g else gen_fun_upd (find g) T v w
   484       |   find t = None
   485       in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
   486   val ss = simpset ();
   487   val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
   488                           simp_tac ss 1]
   489   fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
   490 in 
   491   val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
   492    [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
   493    (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
   494        Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
   495 end;
   496 Addsimprocs[fun_upd2_simproc];
   497 
   498 Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
   499 by (rtac ext 1);
   500 by Auto_tac;
   501 qed "fun_upd_twist";
   502 
   503 
   504 (*** -> and Pi, by Florian Kammueller and LCP ***)
   505 
   506 val prems = Goalw [Pi_def]
   507 "[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
   508 \    ==> f: Pi A B";
   509 by (auto_tac (claset(), simpset() addsimps prems));
   510 qed "Pi_I";
   511 
   512 val prems = Goal 
   513 "[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
   514 by (blast_tac (claset() addIs Pi_I::prems) 1);
   515 qed "funcsetI";
   516 
   517 Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
   518 by Auto_tac;
   519 qed "Pi_mem";
   520 
   521 Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
   522 by Auto_tac;
   523 qed "funcset_mem";
   524 
   525 Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
   526 by Auto_tac;
   527 qed "apply_arb";
   528 
   529 Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
   530 by (rtac ext 1);
   531 by Auto_tac;
   532 bind_thm ("Pi_extensionality", ballI RSN (3, result()));
   533 
   534 
   535 (*** compose ***)
   536 
   537 Goalw [Pi_def, compose_def, restrict_def]
   538      "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
   539 by Auto_tac;
   540 qed "funcset_compose";
   541 
   542 Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
   543 \     ==> compose A h (compose A g f) = compose A (compose B h g) f";
   544 by (res_inst_tac [("A","A")] Pi_extensionality 1);
   545 by (blast_tac (claset() addIs [funcset_compose]) 1);
   546 by (blast_tac (claset() addIs [funcset_compose]) 1);
   547 by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
   548 by Auto_tac;
   549 qed "compose_assoc";
   550 
   551 Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
   552 by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   553 qed "compose_eq";
   554 
   555 Goal "[| f : A funcset B; f ` A = B; g: B funcset C; g ` B = C |]\
   556 \     ==> compose A g f ` A = C";
   557 by (auto_tac (claset(),
   558 	      simpset() addsimps [image_def, compose_eq]));
   559 qed "surj_compose";
   560 
   561 Goal "[| f : A funcset B; g: B funcset C; f ` A = B; inj_on f A; inj_on g B |]\
   562 \     ==> inj_on (compose A g f) A";
   563 by (auto_tac (claset(),
   564 	      simpset() addsimps [inj_on_def, compose_eq]));
   565 qed "inj_on_compose";
   566 
   567 
   568 (*** restrict / lam ***)
   569 
   570 Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
   571 by (auto_tac (claset(),
   572 	      simpset() addsimps [restrict_def, Pi_def]));
   573 qed "restrict_in_funcset";
   574 
   575 val prems = Goalw [restrict_def, Pi_def]
   576      "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
   577 by (asm_simp_tac (simpset() addsimps prems) 1);
   578 qed "restrictI";
   579 
   580 Goal "x: A ==> (lam y: A. f y) x = f x";
   581 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   582 qed "restrict_apply1";
   583 
   584 Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
   585 by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
   586 qed "restrict_apply1_mem";
   587 
   588 Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
   589 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   590 qed "restrict_apply2";
   591 
   592 val prems = Goal
   593     "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
   594 by (rtac ext 1);
   595 by (auto_tac (claset(),
   596 	      simpset() addsimps prems@[restrict_def, Pi_def]));
   597 qed "restrict_ext";
   598 
   599 Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
   600 by Auto_tac;
   601 qed "inj_on_restrict_eq";
   602 
   603 
   604 (*** Inverse ***)
   605 
   606 Goal "[|f ` A = B;  x: B |] ==> ? y: A. f y = x";
   607 by (Blast_tac 1);
   608 qed "surj_image";
   609 
   610 Goalw [Inv_def] "[| f ` A = B; f : A funcset B |] \
   611 \                ==> (lam x: B. (Inv A f) x) : B funcset A";
   612 by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
   613 qed "Inv_funcset";
   614 
   615 
   616 Goal "[| f: A funcset B;  inj_on f A;  f ` A = B;  x: A |] \
   617 \     ==> (lam y: B. (Inv A f) y) (f x) = x";
   618 by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
   619 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   620 by (rtac someI2 1);
   621 by Auto_tac;
   622 qed "Inv_f_f";
   623 
   624 Goal "[| f: A funcset B;  f ` A = B;  x: B |] \
   625 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
   626 by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
   627 by (fast_tac (claset() addIs [someI2]) 1);
   628 qed "f_Inv_f";
   629 
   630 Goal "[| f: A funcset B;  inj_on f A;  f ` A = B |]\
   631 \     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   632 by (rtac Pi_extensionality 1);
   633 by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
   634 by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
   635 by (asm_simp_tac
   636     (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
   637 qed "compose_Inv_id";
   638 
   639 
   640 (*** Pi ***)
   641 
   642 Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   643 by Auto_tac;
   644 qed "Pi_eq_empty";
   645 
   646 Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   647 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   648 qed "Pi_total1";
   649 
   650 Goal "Pi {} B = { %x. @y. True }";
   651 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   652 qed "Pi_empty";
   653 
   654 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
   655 by (auto_tac (claset(),
   656 	      simpset() addsimps [impOfSubs major]));
   657 qed "Pi_mono";