src/HOL/Fun.ML
changeset 13585 db4005b40cc6
parent 13584 3736cf381e15
child 13586 0f339348df0e
     1.1 --- a/src/HOL/Fun.ML	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,507 +0,0 @@
     1.4 -(*  Title:      HOL/Fun
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 -
     1.9 -Lemmas about functions.
    1.10 -*)
    1.11 -
    1.12 -Goal "(f = g) = (! x. f(x)=g(x))";
    1.13 -by (rtac iffI 1);
    1.14 -by (Asm_simp_tac 1);
    1.15 -by (rtac ext 1 THEN Asm_simp_tac 1);
    1.16 -qed "expand_fun_eq";
    1.17 -
    1.18 -val prems = Goal
    1.19 -    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    1.20 -by (rtac (arg_cong RS box_equals) 1);
    1.21 -by (REPEAT (resolve_tac (prems@[refl]) 1));
    1.22 -qed "apply_inverse";
    1.23 -
    1.24 -
    1.25 -section "id";
    1.26 -
    1.27 -Goalw [id_def] "id x = x";
    1.28 -by (rtac refl 1);
    1.29 -qed "id_apply";
    1.30 -Addsimps [id_apply];
    1.31 -
    1.32 -
    1.33 -section "o";
    1.34 -
    1.35 -Goalw [o_def] "(f o g) x = f (g x)";
    1.36 -by (rtac refl 1);
    1.37 -qed "o_apply";
    1.38 -Addsimps [o_apply];
    1.39 -
    1.40 -Goalw [o_def] "f o (g o h) = f o g o h";
    1.41 -by (rtac ext 1);
    1.42 -by (rtac refl 1);
    1.43 -qed "o_assoc";
    1.44 -
    1.45 -Goalw [id_def] "id o g = g";
    1.46 -by (rtac ext 1);
    1.47 -by (Simp_tac 1);
    1.48 -qed "id_o";
    1.49 -Addsimps [id_o];
    1.50 -
    1.51 -Goalw [id_def] "f o id = f";
    1.52 -by (rtac ext 1);
    1.53 -by (Simp_tac 1);
    1.54 -qed "o_id";
    1.55 -Addsimps [o_id];
    1.56 -
    1.57 -Goalw [o_def] "(f o g)`r = f`(g`r)";
    1.58 -by (Blast_tac 1);
    1.59 -qed "image_compose";
    1.60 -
    1.61 -Goal "f`A = (UN x:A. {f x})";
    1.62 -by (Blast_tac 1);
    1.63 -qed "image_eq_UN";
    1.64 -
    1.65 -Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
    1.66 -by (Blast_tac 1);
    1.67 -qed "UN_o";
    1.68 -
    1.69 -(** lemma for proving injectivity of representation functions for **)
    1.70 -(** datatypes involving function types                            **)
    1.71 -
    1.72 -Goalw [o_def]
    1.73 -  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
    1.74 -by (rtac ext 1);
    1.75 -by (etac allE 1);
    1.76 -by (etac allE 1);
    1.77 -by (etac mp 1);
    1.78 -by (etac fun_cong 1);
    1.79 -qed "inj_fun_lemma";
    1.80 -
    1.81 -
    1.82 -section "inj";
    1.83 -(**NB: inj now just translates to inj_on**)
    1.84 -
    1.85 -(*** inj(f): f is a one-to-one function ***)
    1.86 -
    1.87 -(*for Tools/datatype_rep_proofs*)
    1.88 -val [prem] = Goalw [inj_on_def]
    1.89 -    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
    1.90 -by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
    1.91 -qed "datatype_injI";
    1.92 -
    1.93 -Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    1.94 -by (Blast_tac 1);
    1.95 -qed "injD";
    1.96 -
    1.97 -(*Useful with the simplifier*)
    1.98 -Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
    1.99 -by (rtac iffI 1);
   1.100 -by (etac arg_cong 2);
   1.101 -by (etac injD 1);
   1.102 -by (assume_tac 1);
   1.103 -qed "inj_eq";
   1.104 -
   1.105 -Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
   1.106 -by (rtac ext 1);
   1.107 -by (etac injD 1);
   1.108 -by (etac fun_cong 1);
   1.109 -qed "inj_o";
   1.110 -
   1.111 -(*** inj_on f A: f is one-to-one over A ***)
   1.112 -
   1.113 -val prems = Goalw [inj_on_def]
   1.114 -    "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A";
   1.115 -by (blast_tac (claset() addIs prems) 1);
   1.116 -qed "inj_onI";
   1.117 -bind_thm ("injI", inj_onI);                  (*for compatibility*)
   1.118 -
   1.119 -val [major] = Goal 
   1.120 -    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
   1.121 -by (rtac inj_onI 1);
   1.122 -by (etac (apply_inverse RS trans) 1);
   1.123 -by (REPEAT (eresolve_tac [asm_rl,major] 1));
   1.124 -qed "inj_on_inverseI";
   1.125 -bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
   1.126 -
   1.127 -Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   1.128 -by (Blast_tac 1);
   1.129 -qed "inj_onD";
   1.130 -
   1.131 -Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   1.132 -by (blast_tac (claset() addSDs [inj_onD]) 1);
   1.133 -qed "inj_on_iff";
   1.134 -
   1.135 -Goalw [o_def, inj_on_def]
   1.136 -     "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
   1.137 -by (Blast_tac 1);
   1.138 -qed "comp_inj_on";
   1.139 -
   1.140 -Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   1.141 -by (Blast_tac 1);
   1.142 -qed "inj_on_contraD";
   1.143 -
   1.144 -Goal "inj (%s. {s})";
   1.145 -by (rtac injI 1);
   1.146 -by (etac singleton_inject 1);
   1.147 -qed "inj_singleton";
   1.148 -
   1.149 -Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   1.150 -by (Blast_tac 1);
   1.151 -qed "subset_inj_on";
   1.152 -
   1.153 -
   1.154 -(** surj **)
   1.155 -
   1.156 -val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
   1.157 -by (blast_tac (claset() addIs [prem RS sym]) 1);
   1.158 -qed "surjI";
   1.159 -
   1.160 -Goalw [surj_def] "surj f ==> range f = UNIV";
   1.161 -by Auto_tac;
   1.162 -qed "surj_range";
   1.163 -
   1.164 -Goalw [surj_def] "surj f ==> EX x. y = f x";
   1.165 -by (Blast_tac 1);
   1.166 -qed "surjD";
   1.167 -
   1.168 -val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C";
   1.169 -by (cut_facts_tac [p1 RS surjD] 1);
   1.170 -by (etac exE 1);
   1.171 -by (rtac p2 1);
   1.172 -by (atac 1);
   1.173 -qed "surjE";
   1.174 -
   1.175 -Goalw [o_def, surj_def] "[| surj f;  surj g |] ==> surj (g o f)";
   1.176 -by (Clarify_tac 1); 
   1.177 -by (dres_inst_tac [("x","y")] spec 1); 
   1.178 -by (Clarify_tac 1); 
   1.179 -by (dres_inst_tac [("x","x")] spec 1); 
   1.180 -by (Blast_tac 1); 
   1.181 -qed "comp_surj";
   1.182 -
   1.183 -
   1.184 -(** Bijections **)
   1.185 -
   1.186 -Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
   1.187 -by (Blast_tac 1);
   1.188 -qed "bijI";
   1.189 -
   1.190 -Goalw [bij_def] "bij f ==> inj f";
   1.191 -by (Blast_tac 1);
   1.192 -qed "bij_is_inj";
   1.193 -
   1.194 -Goalw [bij_def] "bij f ==> surj f";
   1.195 -by (Blast_tac 1);
   1.196 -qed "bij_is_surj";
   1.197 -
   1.198 -
   1.199 -(** We seem to need both the id-forms and the (%x. x) forms; the latter can
   1.200 -    arise by rewriting, while id may be used explicitly. **)
   1.201 -
   1.202 -Goal "(%x. x) ` Y = Y";
   1.203 -by (Blast_tac 1);
   1.204 -qed "image_ident";
   1.205 -
   1.206 -Goalw [id_def] "id ` Y = Y";
   1.207 -by (Blast_tac 1);
   1.208 -qed "image_id";
   1.209 -Addsimps [image_ident, image_id];
   1.210 -
   1.211 -Goal "(%x. x) -` Y = Y";
   1.212 -by (Blast_tac 1);
   1.213 -qed "vimage_ident";
   1.214 -
   1.215 -Goalw [id_def] "id -` A = A";
   1.216 -by Auto_tac;
   1.217 -qed "vimage_id";
   1.218 -Addsimps [vimage_ident, vimage_id];
   1.219 -
   1.220 -Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
   1.221 -by (blast_tac (claset() addIs [sym]) 1);
   1.222 -qed "vimage_image_eq";
   1.223 -
   1.224 -Goal "f ` (f -` A) <= A";
   1.225 -by (Blast_tac 1);
   1.226 -qed "image_vimage_subset";
   1.227 -
   1.228 -Goal "f ` (f -` A) = A Int range f";
   1.229 -by (Blast_tac 1);
   1.230 -qed "image_vimage_eq";
   1.231 -Addsimps [image_vimage_eq];
   1.232 -
   1.233 -Goal "surj f ==> f ` (f -` A) = A";
   1.234 -by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
   1.235 -qed "surj_image_vimage_eq";
   1.236 -
   1.237 -Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
   1.238 -by (Blast_tac 1);
   1.239 -qed "inj_vimage_image_eq";
   1.240 -
   1.241 -Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
   1.242 -by (blast_tac (claset() addIs [sym]) 1);
   1.243 -qed "vimage_subsetD";
   1.244 -
   1.245 -Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
   1.246 -by (Blast_tac 1);
   1.247 -qed "vimage_subsetI";
   1.248 -
   1.249 -Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
   1.250 -by (blast_tac (claset() delrules [subsetI]
   1.251 -			addIs [vimage_subsetI, vimage_subsetD]) 1);
   1.252 -qed "vimage_subset_eq";
   1.253 -
   1.254 -Goal "f`(A Int B) <= f`A Int f`B";
   1.255 -by (Blast_tac 1);
   1.256 -qed "image_Int_subset";
   1.257 -
   1.258 -Goal "f`A - f`B <= f`(A - B)";
   1.259 -by (Blast_tac 1);
   1.260 -qed "image_diff_subset";
   1.261 -
   1.262 -Goalw [inj_on_def]
   1.263 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B";
   1.264 -by (Blast_tac 1);
   1.265 -qed "inj_on_image_Int";
   1.266 -
   1.267 -Goalw [inj_on_def]
   1.268 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B";
   1.269 -by (Blast_tac 1);
   1.270 -qed "inj_on_image_set_diff";
   1.271 -
   1.272 -Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
   1.273 -by (Blast_tac 1);
   1.274 -qed "image_Int";
   1.275 -
   1.276 -Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
   1.277 -by (Blast_tac 1);
   1.278 -qed "image_set_diff";
   1.279 -
   1.280 -Goal "inj f ==> (f a : f`A) = (a : A)";
   1.281 -by (blast_tac (claset() addDs [injD]) 1);
   1.282 -qed "inj_image_mem_iff";
   1.283 -
   1.284 -Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
   1.285 -by (Blast_tac 1);
   1.286 -qed "inj_image_subset_iff";
   1.287 -
   1.288 -Goal "inj f ==> (f`A = f`B) = (A = B)";
   1.289 -by (blast_tac (claset() addDs [injD]) 1);
   1.290 -qed "inj_image_eq_iff";
   1.291 -
   1.292 -Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
   1.293 -by (Blast_tac 1);
   1.294 -qed "image_UN";
   1.295 -
   1.296 -(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   1.297 -Goalw [inj_on_def]
   1.298 -   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
   1.299 -\   ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   1.300 -by (Blast_tac 1);
   1.301 -qed "image_INT";
   1.302 -
   1.303 -(*Compare with image_INT: no use of inj_on, and if f is surjective then
   1.304 -  it doesn't matter whether A is empty*)
   1.305 -Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   1.306 -by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
   1.307 -by (Blast_tac 1);  
   1.308 -qed "bij_image_INT";
   1.309 -
   1.310 -Goal "surj f ==> -(f`A) <= f`(-A)";
   1.311 -by (auto_tac (claset(), simpset() addsimps [surj_def]));  
   1.312 -qed "surj_Compl_image_subset";
   1.313 -
   1.314 -Goal "inj f ==> f`(-A) <= -(f`A)";
   1.315 -by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
   1.316 -qed "inj_image_Compl_subset";
   1.317 -
   1.318 -Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
   1.319 -by (rtac equalityI 1); 
   1.320 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
   1.321 -                                                surj_Compl_image_subset]))); 
   1.322 -qed "bij_image_Compl_eq";
   1.323 -
   1.324 -val set_cs = claset() delrules [equalityI];
   1.325 -
   1.326 -
   1.327 -section "fun_upd";
   1.328 -
   1.329 -Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   1.330 -by Safe_tac;
   1.331 -by (etac subst 1);
   1.332 -by (rtac ext 2);
   1.333 -by Auto_tac;
   1.334 -qed "fun_upd_idem_iff";
   1.335 -
   1.336 -(* f x = y ==> f(x:=y) = f *)
   1.337 -bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   1.338 -
   1.339 -(* f(x := f x) = f *)
   1.340 -AddIffs [refl RS fun_upd_idem];
   1.341 -
   1.342 -Goal "(f(x:=y))z = (if z=x then y else f z)";
   1.343 -by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   1.344 -qed "fun_upd_apply";
   1.345 -Addsimps [fun_upd_apply];
   1.346 -
   1.347 -(* fun_upd_apply supersedes these two,   but they are useful 
   1.348 -   if fun_upd_apply is intentionally removed from the simpset *)
   1.349 -Goal "(f(x:=y)) x = y";
   1.350 -by (Simp_tac 1);
   1.351 -qed "fun_upd_same";
   1.352 -
   1.353 -Goal "z~=x ==> (f(x:=y)) z = f z";
   1.354 -by (Asm_simp_tac 1);
   1.355 -qed "fun_upd_other";
   1.356 -
   1.357 -Goal "f(x:=y,x:=z) = f(x:=z)";
   1.358 -by (rtac ext 1);
   1.359 -by (Simp_tac 1);
   1.360 -qed "fun_upd_upd";
   1.361 -Addsimps [fun_upd_upd];
   1.362 -
   1.363 -(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
   1.364 -local 
   1.365 -  fun gen_fun_upd None T _ _ = None
   1.366 -    | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y);
   1.367 -  fun dest_fun_T1 (Type (_, T :: Ts)) = T;
   1.368 -  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
   1.369 -    let
   1.370 -      fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
   1.371 -            if v aconv x then Some g else gen_fun_upd (find g) T v w
   1.372 -        | find t = None;
   1.373 -    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end;
   1.374 -
   1.375 -  val ss = simpset ();
   1.376 -  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1);
   1.377 -in 
   1.378 -  val fun_upd2_simproc =
   1.379 -    Simplifier.simproc (Theory.sign_of (the_context ()))
   1.380 -      "fun_upd2" ["f(v := w, x := y)"]
   1.381 -      (fn sg => fn _ => fn t =>
   1.382 -        case find_double t of (T, None) => None
   1.383 -        | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover));
   1.384 -end;
   1.385 -Addsimprocs[fun_upd2_simproc];
   1.386 -
   1.387 -Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
   1.388 -by (rtac ext 1);
   1.389 -by Auto_tac;
   1.390 -qed "fun_upd_twist";
   1.391 -
   1.392 -
   1.393 -(*** -> and Pi, by Florian Kammueller and LCP ***)
   1.394 -
   1.395 -val prems = Goalw [Pi_def]
   1.396 -"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = arbitrary|] \
   1.397 -\    ==> f: Pi A B";
   1.398 -by (auto_tac (claset(), simpset() addsimps prems));
   1.399 -qed "Pi_I";
   1.400 -
   1.401 -val prems = Goal 
   1.402 -"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = arbitrary|] ==> f: A funcset B";
   1.403 -by (blast_tac (claset() addIs Pi_I::prems) 1);
   1.404 -qed "funcsetI";
   1.405 -
   1.406 -Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
   1.407 -by Auto_tac;
   1.408 -qed "Pi_mem";
   1.409 -
   1.410 -Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
   1.411 -by Auto_tac;
   1.412 -qed "funcset_mem";
   1.413 -
   1.414 -Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
   1.415 -by Auto_tac;
   1.416 -qed "apply_arb";
   1.417 -
   1.418 -Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
   1.419 -by (rtac ext 1);
   1.420 -by Auto_tac;
   1.421 -bind_thm ("Pi_extensionality", ballI RSN (3, result()));
   1.422 -
   1.423 -
   1.424 -(*** compose ***)
   1.425 -
   1.426 -Goalw [Pi_def, compose_def, restrict_def]
   1.427 -     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
   1.428 -by Auto_tac;
   1.429 -qed "funcset_compose";
   1.430 -
   1.431 -Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
   1.432 -\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
   1.433 -by (res_inst_tac [("A","A")] Pi_extensionality 1);
   1.434 -by (blast_tac (claset() addIs [funcset_compose]) 1);
   1.435 -by (blast_tac (claset() addIs [funcset_compose]) 1);
   1.436 -by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
   1.437 -by Auto_tac;
   1.438 -qed "compose_assoc";
   1.439 -
   1.440 -Goal "x : A ==> compose A g f x = g(f(x))";
   1.441 -by (asm_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   1.442 -qed "compose_eq";
   1.443 -
   1.444 -Goal "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C";
   1.445 -by (auto_tac (claset(), simpset() addsimps [image_def, compose_eq]));
   1.446 -qed "surj_compose";
   1.447 -
   1.448 -Goal "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A";
   1.449 -by (auto_tac (claset(), simpset() addsimps [inj_on_def, compose_eq]));
   1.450 -qed "inj_on_compose";
   1.451 -
   1.452 -
   1.453 -(*** restrict / bounded abstraction ***)
   1.454 -
   1.455 -Goal "f`A <= B ==> (%x:A. f x) : A funcset B";
   1.456 -by (auto_tac (claset(),
   1.457 -	      simpset() addsimps [restrict_def, Pi_def]));
   1.458 -qed "restrict_in_funcset";
   1.459 -
   1.460 -val prems = Goalw [restrict_def, Pi_def]
   1.461 -     "(!!x. x: A ==> f x: B x) ==> (%x:A. f x) : Pi A B";
   1.462 -by (asm_simp_tac (simpset() addsimps prems) 1);
   1.463 -qed "restrictI";
   1.464 -
   1.465 -Goal "(%y:A. f y) x = (if x : A then f x else arbitrary)";
   1.466 -by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   1.467 -qed "restrict_apply";
   1.468 -Addsimps [restrict_apply];
   1.469 -
   1.470 -val prems = Goal
   1.471 -    "(!!x. x: A ==> f x = g x) ==> (%x:A. f x) = (%x:A. g x)";
   1.472 -by (rtac ext 1);
   1.473 -by (auto_tac (claset(),
   1.474 -	      simpset() addsimps prems@[restrict_def, Pi_def]));
   1.475 -qed "restrict_ext";
   1.476 -
   1.477 -Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
   1.478 -by Auto_tac;
   1.479 -qed "inj_on_restrict_eq";
   1.480 -
   1.481 -
   1.482 -Goal "f : A funcset B ==> compose A (%y:B. y) f = f";
   1.483 -by (rtac ext 1); 
   1.484 -by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   1.485 -qed "Id_compose";
   1.486 -
   1.487 -Goal "g : A funcset B ==> compose A g (%x:A. x) = g";
   1.488 -by (rtac ext 1); 
   1.489 -by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   1.490 -qed "compose_Id";
   1.491 -
   1.492 -
   1.493 -(*** Pi ***)
   1.494 -
   1.495 -Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   1.496 -by Auto_tac;
   1.497 -qed "Pi_eq_empty";
   1.498 -
   1.499 -Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   1.500 -by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   1.501 -qed "Pi_total1";
   1.502 -
   1.503 -Goal "Pi {} B = { %x. arbitrary }";
   1.504 -by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   1.505 -qed "Pi_empty";
   1.506 -
   1.507 -val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
   1.508 -by (auto_tac (claset(),
   1.509 -	      simpset() addsimps [impOfSubs major]));
   1.510 -qed "Pi_mono";