conversion of Perm to Isar. Strengthening of comp_fun_apply
authorpaulson
Fri May 24 13:15:37 2002 +0200 (2002-05-24)
changeset 13176312bd350579b
parent 13175 81082cfa5618
child 13177 ba734cc2887d
conversion of Perm to Isar. Strengthening of comp_fun_apply
src/ZF/Induct/Multiset.ML
src/ZF/IsaMakefile
src/ZF/Order.thy
src/ZF/Perm.ML
src/ZF/Perm.thy
src/ZF/UNITY/Constrains.ML
src/ZF/UNITY/UNITY.ML
src/ZF/ex/Limit.thy
src/ZF/func.thy
     1.1 --- a/src/ZF/Induct/Multiset.ML	Thu May 23 17:05:21 2002 +0200
     1.2 +++ b/src/ZF/Induct/Multiset.ML	Fri May 24 13:15:37 2002 +0200
     1.3 @@ -696,9 +696,7 @@
     1.4  by (rtac fun_extension 1 THEN rtac lam_type 1);
     1.5  by (ALLGOALS(Asm_full_simp_tac));
     1.6  by (auto_tac (claset(), simpset()  
     1.7 -        addsimps [multiset_fun_iff,
     1.8 -                 fun_extend_apply1,
     1.9 -                 fun_extend_apply2]));
    1.10 +        addsimps [multiset_fun_iff, fun_extend_apply]));
    1.11  by (dres_inst_tac [("c", "a"), ("b", "1")] fun_extend3 1);
    1.12  by (stac Un_commute 3);
    1.13  by (auto_tac (claset(), simpset() addsimps [cons_eq]));
     2.1 --- a/src/ZF/IsaMakefile	Thu May 23 17:05:21 2002 +0200
     2.2 +++ b/src/ZF/IsaMakefile	Fri May 24 13:15:37 2002 +0200
     2.3 @@ -38,7 +38,7 @@
     2.4    Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
     2.5    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     2.6    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
     2.7 -  OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy	\
     2.8 +  OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
     2.9    QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
    2.10    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    2.11    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
     3.1 --- a/src/ZF/Order.thy	Thu May 23 17:05:21 2002 +0200
     3.2 +++ b/src/ZF/Order.thy	Fri May 24 13:15:37 2002 +0200
     3.3 @@ -436,8 +436,7 @@
     3.4  apply (blast intro!: bij_converse_bij
     3.5               intro: bij_is_fun apply_funtype)+
     3.6  apply (erule notE)
     3.7 -apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
     3.8 -                 comp_fun_apply [of _ A B _ A])
     3.9 +apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B])
    3.10  done
    3.11  
    3.12  
     4.1 --- a/src/ZF/Perm.ML	Thu May 23 17:05:21 2002 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,545 +0,0 @@
     4.4 -(*  Title:      ZF/Perm.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1991  University of Cambridge
     4.8 -
     4.9 -The theory underlying permutation groups
    4.10 -  -- Composition of relations, the identity relation
    4.11 -  -- Injections, surjections, bijections
    4.12 -  -- Lemmas for the Schroeder-Bernstein Theorem
    4.13 -*)
    4.14 -
    4.15 -(** Surjective function space **)
    4.16 -
    4.17 -Goalw [surj_def] "f: surj(A,B) ==> f: A->B";
    4.18 -by (etac CollectD1 1);
    4.19 -qed "surj_is_fun";
    4.20 -
    4.21 -Goalw [surj_def] "f : Pi(A,B) ==> f: surj(A,range(f))";
    4.22 -by (blast_tac (claset() addIs [apply_equality, range_of_fun, domain_type]) 1);
    4.23 -qed "fun_is_surj";
    4.24 -
    4.25 -Goalw [surj_def] "f: surj(A,B) ==> range(f)=B";
    4.26 -by (best_tac (claset() addIs [apply_Pair] addEs [range_type]) 1);
    4.27 -qed "surj_range";
    4.28 -
    4.29 -(** A function with a right inverse is a surjection **)
    4.30 -
    4.31 -val prems = Goalw [surj_def]
    4.32 -    "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y \
    4.33 -\    |] ==> f: surj(A,B)";
    4.34 -by (blast_tac (claset() addIs prems) 1);
    4.35 -qed "f_imp_surjective";
    4.36 -
    4.37 -val prems = Goal
    4.38 -    "[| !!x. x:A ==> c(x): B;           \
    4.39 -\       !!y. y:B ==> d(y): A;           \
    4.40 -\       !!y. y:B ==> c(d(y)) = y        \
    4.41 -\    |] ==> (lam x:A. c(x)) : surj(A,B)";
    4.42 -by (res_inst_tac [("d", "d")] f_imp_surjective 1);
    4.43 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems) ));
    4.44 -qed "lam_surjective";
    4.45 -
    4.46 -(*Cantor's theorem revisited*)
    4.47 -Goalw [surj_def] "f ~: surj(A,Pow(A))";
    4.48 -by Safe_tac;
    4.49 -by (cut_facts_tac [cantor] 1);
    4.50 -by (fast_tac subset_cs 1);
    4.51 -qed "cantor_surj";
    4.52 -
    4.53 -
    4.54 -(** Injective function space **)
    4.55 -
    4.56 -Goalw [inj_def] "f: inj(A,B) ==> f: A->B";
    4.57 -by (etac CollectD1 1);
    4.58 -qed "inj_is_fun";
    4.59 -
    4.60 -(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
    4.61 -Goalw [inj_def]
    4.62 -    "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
    4.63 -by (blast_tac (claset() addDs [Pair_mem_PiD]) 1);
    4.64 -qed "inj_equality";
    4.65 -
    4.66 -Goalw [inj_def] "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
    4.67 -by (Blast_tac 1);
    4.68 -qed "inj_apply_equality";
    4.69 -
    4.70 -(** A function with a left inverse is an injection **)
    4.71 -
    4.72 -Goal "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
    4.73 -by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
    4.74 -by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
    4.75 -bind_thm ("f_imp_injective", ballI RSN (2,result()));
    4.76 -
    4.77 -val prems = Goal
    4.78 -    "[| !!x. x:A ==> c(x): B;           \
    4.79 -\       !!x. x:A ==> d(c(x)) = x        \
    4.80 -\    |] ==> (lam x:A. c(x)) : inj(A,B)";
    4.81 -by (res_inst_tac [("d", "d")] f_imp_injective 1);
    4.82 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems)));
    4.83 -qed "lam_injective";
    4.84 -
    4.85 -(** Bijections **)
    4.86 -
    4.87 -Goalw [bij_def] "f: bij(A,B) ==> f: inj(A,B)";
    4.88 -by (etac IntD1 1);
    4.89 -qed "bij_is_inj";
    4.90 -
    4.91 -Goalw [bij_def] "f: bij(A,B) ==> f: surj(A,B)";
    4.92 -by (etac IntD2 1);
    4.93 -qed "bij_is_surj";
    4.94 -
    4.95 -(* f: bij(A,B) ==> f: A->B *)
    4.96 -bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
    4.97 -
    4.98 -val prems = Goalw [bij_def]
    4.99 -    "[| !!x. x:A ==> c(x): B;           \
   4.100 -\       !!y. y:B ==> d(y): A;           \
   4.101 -\       !!x. x:A ==> d(c(x)) = x;       \
   4.102 -\       !!y. y:B ==> c(d(y)) = y        \
   4.103 -\    |] ==> (lam x:A. c(x)) : bij(A,B)";
   4.104 -by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
   4.105 -qed "lam_bijective";
   4.106 -
   4.107 -Goal "(ALL y : x. EX! y'. f(y') = f(y))  \
   4.108 -\     ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)";
   4.109 -by (res_inst_tac [("d","f")] lam_bijective 1);
   4.110 -by (auto_tac (claset(),
   4.111 -	      simpset() addsimps [the_equality2]));
   4.112 -qed "RepFun_bijective";
   4.113 -
   4.114 -
   4.115 -(** Identity function **)
   4.116 -
   4.117 -Goalw [id_def] "a:A ==> <a,a> : id(A)";  
   4.118 -by (etac lamI 1);
   4.119 -qed "idI";
   4.120 -
   4.121 -val major::prems = Goalw [id_def]
   4.122 -    "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P  \
   4.123 -\    |] ==>  P";  
   4.124 -by (rtac (major RS lamE) 1);
   4.125 -by (REPEAT (ares_tac prems 1));
   4.126 -qed "idE";
   4.127 -
   4.128 -Goalw [id_def] "id(A) : A->A";  
   4.129 -by (rtac lam_type 1);
   4.130 -by (assume_tac 1);
   4.131 -qed "id_type";
   4.132 -
   4.133 -Goalw [id_def] "x:A ==> id(A)`x = x";
   4.134 -by (Asm_simp_tac 1);
   4.135 -qed "id_conv";
   4.136 -
   4.137 -Addsimps [id_conv];
   4.138 -
   4.139 -Goalw [id_def] "A<=B ==> id(A) <= id(B)";
   4.140 -by (etac lam_mono 1);
   4.141 -qed "id_mono";
   4.142 -
   4.143 -Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
   4.144 -by (REPEAT (ares_tac [CollectI,lam_type] 1));
   4.145 -by (etac subsetD 1 THEN assume_tac 1);
   4.146 -by (Simp_tac 1);
   4.147 -qed "id_subset_inj";
   4.148 -
   4.149 -bind_thm ("id_inj", subset_refl RS id_subset_inj);
   4.150 -
   4.151 -Goalw [id_def,surj_def] "id(A): surj(A,A)";
   4.152 -by (Asm_simp_tac 1);
   4.153 -qed "id_surj";
   4.154 -
   4.155 -Goalw [bij_def] "id(A): bij(A,A)";
   4.156 -by (blast_tac (claset() addIs [id_inj, id_surj]) 1);
   4.157 -qed "id_bij";
   4.158 -
   4.159 -Goalw [id_def] "A <= B <-> id(A) : A->B";
   4.160 -by (fast_tac (claset() addSIs [lam_type] addDs [apply_type] 
   4.161 -                      addss (simpset())) 1);
   4.162 -qed "subset_iff_id";
   4.163 -
   4.164 -
   4.165 -(*** Converse of a function ***)
   4.166 -
   4.167 -Goalw [inj_def] "f: inj(A,B) ==> converse(f) : range(f)->A";
   4.168 -by (asm_simp_tac (simpset() addsimps [Pi_iff, function_def]) 1);
   4.169 -by (etac CollectE 1);
   4.170 -by (asm_simp_tac (simpset() addsimps [apply_iff]) 1);
   4.171 -by (blast_tac (claset() addDs [fun_is_rel]) 1);
   4.172 -qed "inj_converse_fun";
   4.173 -
   4.174 -(** Equations for converse(f) **)
   4.175 -
   4.176 -(*The premises are equivalent to saying that f is injective...*) 
   4.177 -Goal "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
   4.178 -by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
   4.179 -qed "left_inverse_lemma";
   4.180 -
   4.181 -Goal "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
   4.182 -by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
   4.183 -			       inj_is_fun]) 1);
   4.184 -qed "left_inverse";
   4.185 -
   4.186 -bind_thm ("left_inverse_bij", bij_is_inj RS left_inverse);
   4.187 -
   4.188 -Goal "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
   4.189 -by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
   4.190 -by (REPEAT (assume_tac 1));
   4.191 -qed "right_inverse_lemma";
   4.192 -
   4.193 -(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
   4.194 -  No: they would not imply that converse(f) was a function! *)
   4.195 -Goal "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
   4.196 -by (rtac right_inverse_lemma 1);
   4.197 -by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
   4.198 -qed "right_inverse";
   4.199 -
   4.200 -Addsimps [left_inverse, right_inverse];
   4.201 -
   4.202 -
   4.203 -Goal "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
   4.204 -by (force_tac (claset(), simpset() addsimps [bij_def, surj_range]) 1);
   4.205 -qed "right_inverse_bij";
   4.206 -
   4.207 -(** Converses of injections, surjections, bijections **)
   4.208 -
   4.209 -Goal "f: inj(A,B) ==> converse(f): inj(range(f), A)";
   4.210 -by (rtac f_imp_injective 1);
   4.211 -by (etac inj_converse_fun 1);
   4.212 -by (rtac right_inverse 1);
   4.213 -by (REPEAT (assume_tac 1));
   4.214 -qed "inj_converse_inj";
   4.215 -
   4.216 -Goal "f: inj(A,B) ==> converse(f): surj(range(f), A)";
   4.217 -by (blast_tac (claset() addIs [f_imp_surjective, inj_converse_fun, 
   4.218 -			       left_inverse,
   4.219 -			       inj_is_fun, range_of_fun RS apply_type]) 1);
   4.220 -qed "inj_converse_surj";
   4.221 -
   4.222 -Goalw [bij_def] "f: bij(A,B) ==> converse(f): bij(B,A)";
   4.223 -by (fast_tac (claset() addEs [surj_range RS subst, inj_converse_inj,
   4.224 -			      inj_converse_surj]) 1);
   4.225 -qed "bij_converse_bij";
   4.226 -(*Adding this as an SI seems to cause looping*)
   4.227 -
   4.228 -AddTCs [bij_converse_bij];
   4.229 -
   4.230 -
   4.231 -(** Composition of two relations **)
   4.232 -
   4.233 -(*The inductive definition package could derive these theorems for (r O s)*)
   4.234 -
   4.235 -Goalw [comp_def] "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
   4.236 -by (Blast_tac 1);
   4.237 -qed "compI";
   4.238 -
   4.239 -val prems = Goalw [comp_def]
   4.240 -    "[| xz : r O s;  \
   4.241 -\       !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
   4.242 -\    |] ==> P";
   4.243 -by (cut_facts_tac prems 1);
   4.244 -by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
   4.245 -qed "compE";
   4.246 -
   4.247 -bind_thm ("compEpair", 
   4.248 -    rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
   4.249 -                    THEN prune_params_tac)
   4.250 -        (inst "xz" "<a,c>" compE));
   4.251 -
   4.252 -AddSIs [idI];
   4.253 -AddIs  [compI];
   4.254 -AddSEs [compE,idE];
   4.255 -
   4.256 -Goal "converse(R O S) = converse(S) O converse(R)";
   4.257 -by (Blast_tac 1);
   4.258 -qed "converse_comp";
   4.259 -
   4.260 -
   4.261 -(** Domain and Range -- see Suppes, section 3.1 **)
   4.262 -
   4.263 -(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
   4.264 -Goal "range(r O s) <= range(r)";
   4.265 -by (Blast_tac 1);
   4.266 -qed "range_comp";
   4.267 -
   4.268 -Goal "domain(r) <= range(s) ==> range(r O s) = range(r)";
   4.269 -by (rtac (range_comp RS equalityI) 1);
   4.270 -by (Blast_tac 1);
   4.271 -qed "range_comp_eq";
   4.272 -
   4.273 -Goal "domain(r O s) <= domain(s)";
   4.274 -by (Blast_tac 1);
   4.275 -qed "domain_comp";
   4.276 -
   4.277 -Goal "range(s) <= domain(r) ==> domain(r O s) = domain(s)";
   4.278 -by (rtac (domain_comp RS equalityI) 1);
   4.279 -by (Blast_tac 1);
   4.280 -qed "domain_comp_eq";
   4.281 -
   4.282 -Goal "(r O s)``A = r``(s``A)";
   4.283 -by (Blast_tac 1);
   4.284 -qed "image_comp";
   4.285 -
   4.286 -
   4.287 -(** Other results **)
   4.288 -
   4.289 -Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
   4.290 -by (Blast_tac 1);
   4.291 -qed "comp_mono";
   4.292 -
   4.293 -(*composition preserves relations*)
   4.294 -Goal "[| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C";
   4.295 -by (Blast_tac 1);
   4.296 -qed "comp_rel";
   4.297 -
   4.298 -(*associative law for composition*)
   4.299 -Goal "(r O s) O t = r O (s O t)";
   4.300 -by (Blast_tac 1);
   4.301 -qed "comp_assoc";
   4.302 -
   4.303 -(*left identity of composition; provable inclusions are
   4.304 -        id(A) O r <= r       
   4.305 -  and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
   4.306 -Goal "r<=A*B ==> id(B) O r = r";
   4.307 -by (Blast_tac 1);
   4.308 -qed "left_comp_id";
   4.309 -
   4.310 -(*right identity of composition; provable inclusions are
   4.311 -        r O id(A) <= r
   4.312 -  and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
   4.313 -Goal "r<=A*B ==> r O id(A) = r";
   4.314 -by (Blast_tac 1);
   4.315 -qed "right_comp_id";
   4.316 -
   4.317 -
   4.318 -(** Composition preserves functions, injections, and surjections **)
   4.319 -
   4.320 -Goalw [function_def]
   4.321 -    "[| function(g);  function(f) |] ==> function(f O g)";
   4.322 -by (Blast_tac 1);
   4.323 -qed "comp_function";
   4.324 -
   4.325 -Goal "[| g: A->B;  f: B->C |] ==> (f O g) : A->C";
   4.326 -by (asm_full_simp_tac
   4.327 -    (simpset() addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
   4.328 -           setloop etac conjE) 1);
   4.329 -by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
   4.330 -by (Blast_tac 1);
   4.331 -qed "comp_fun";
   4.332 -
   4.333 -Goal "[| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
   4.334 -by (REPEAT (ares_tac [comp_fun,apply_equality,compI,
   4.335 -                      apply_Pair,apply_type] 1));
   4.336 -qed "comp_fun_apply";
   4.337 -
   4.338 -Addsimps [comp_fun_apply];
   4.339 -
   4.340 -(*Simplifies compositions of lambda-abstractions*)
   4.341 -val [prem] = Goal
   4.342 -    "[| !!x. x:A ==> b(x): B    \
   4.343 -\    |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
   4.344 -by (rtac fun_extension 1);
   4.345 -by (rtac comp_fun 1);
   4.346 -by (rtac lam_funtype 2);
   4.347 -by (typecheck_tac (tcset() addTCs [prem]));
   4.348 -by (asm_simp_tac (simpset() addsimps [prem]
   4.349 -                   setSolver (mk_solver ""
   4.350 -                   (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
   4.351 -qed "comp_lam";
   4.352 -
   4.353 -Goal "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
   4.354 -by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
   4.355 -    f_imp_injective 1);
   4.356 -by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
   4.357 -by (asm_simp_tac (simpset()  
   4.358 -		  setSolver (mk_solver ""
   4.359 -		  (type_solver_tac (tcset() addTCs [inj_is_fun])))) 1);
   4.360 -qed "comp_inj";
   4.361 -
   4.362 -Goalw [surj_def]
   4.363 -    "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
   4.364 -by (blast_tac (claset() addSIs [comp_fun,comp_fun_apply]) 1);
   4.365 -qed "comp_surj";
   4.366 -
   4.367 -Goalw [bij_def]
   4.368 -    "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
   4.369 -by (blast_tac (claset() addIs [comp_inj,comp_surj]) 1);
   4.370 -qed "comp_bij";
   4.371 -
   4.372 -
   4.373 -(** Dual properties of inj and surj -- useful for proofs from
   4.374 -    D Pastre.  Automatic theorem proving in set theory. 
   4.375 -    Artificial Intelligence, 10:1--27, 1978. **)
   4.376 -
   4.377 -Goalw [inj_def]
   4.378 -    "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
   4.379 -by Safe_tac;
   4.380 -by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   4.381 -by (asm_simp_tac (simpset() ) 1);
   4.382 -qed "comp_mem_injD1";
   4.383 -
   4.384 -Goalw [inj_def,surj_def]
   4.385 -    "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
   4.386 -by Safe_tac;
   4.387 -by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
   4.388 -by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
   4.389 -by (REPEAT (assume_tac 1));
   4.390 -by Safe_tac;
   4.391 -by (res_inst_tac [("t", "op `(g)")] subst_context 1);
   4.392 -by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   4.393 -by (asm_simp_tac (simpset() ) 1);
   4.394 -qed "comp_mem_injD2";
   4.395 -
   4.396 -Goalw [surj_def]
   4.397 -    "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
   4.398 -by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
   4.399 -qed "comp_mem_surjD1";
   4.400 -
   4.401 -Goal "[| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
   4.402 -by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
   4.403 -qed "comp_fun_applyD";
   4.404 -
   4.405 -Goalw [inj_def,surj_def]
   4.406 -    "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
   4.407 -by Safe_tac;
   4.408 -by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
   4.409 -by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
   4.410 -by (blast_tac (claset() addSIs [apply_funtype]) 1);
   4.411 -qed "comp_mem_surjD2";
   4.412 -
   4.413 -
   4.414 -(** inverses of composition **)
   4.415 -
   4.416 -(*left inverse of composition; one inclusion is
   4.417 -        f: A->B ==> id(A) <= converse(f) O f *)
   4.418 -Goalw [inj_def] "f: inj(A,B) ==> converse(f) O f = id(A)";
   4.419 -by (fast_tac (claset() addIs [apply_Pair] 
   4.420 -                      addEs [domain_type]
   4.421 -               addss (simpset() addsimps [apply_iff])) 1);
   4.422 -qed "left_comp_inverse";
   4.423 -
   4.424 -(*right inverse of composition; one inclusion is
   4.425 -                f: A->B ==> f O converse(f) <= id(B) 
   4.426 -*)
   4.427 -val [prem] = goalw (the_context ()) [surj_def]
   4.428 -    "f: surj(A,B) ==> f O converse(f) = id(B)";
   4.429 -val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
   4.430 -by (cut_facts_tac [prem] 1);
   4.431 -by (rtac equalityI 1);
   4.432 -by (best_tac (claset() addEs [domain_type, range_type, make_elim appfD]) 1);
   4.433 -by (blast_tac (claset() addIs [apply_Pair]) 1);
   4.434 -qed "right_comp_inverse";
   4.435 -
   4.436 -(** Proving that a function is a bijection **)
   4.437 -
   4.438 -Goalw [id_def]
   4.439 -    "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
   4.440 -by Safe_tac;
   4.441 -by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
   4.442 -by (Asm_full_simp_tac 1);
   4.443 -by (rtac fun_extension 1);
   4.444 -by (REPEAT (ares_tac [comp_fun, lam_type] 1));
   4.445 -by Auto_tac;
   4.446 -qed "comp_eq_id_iff";
   4.447 -
   4.448 -Goalw [bij_def]
   4.449 -    "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f : bij(A,B)";
   4.450 -by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff]) 1);
   4.451 -by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1
   4.452 -       ORELSE eresolve_tac [bspec, apply_type] 1));
   4.453 -qed "fg_imp_bijective";
   4.454 -
   4.455 -Goal "[| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)";
   4.456 -by (REPEAT (ares_tac [fg_imp_bijective] 1));
   4.457 -qed "nilpotent_imp_bijective";
   4.458 -
   4.459 -Goal "[| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
   4.460 -by (asm_simp_tac (simpset() addsimps [fg_imp_bijective, comp_eq_id_iff, 
   4.461 -                                  left_inverse_lemma, right_inverse_lemma]) 1);
   4.462 -qed "invertible_imp_bijective";
   4.463 -
   4.464 -(** Unions of functions -- cf similar theorems on func.ML **)
   4.465 -
   4.466 -(*Theorem by KG, proof by LCP*)
   4.467 -Goal "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] \
   4.468 -\     ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)";
   4.469 -by (res_inst_tac [("d","%z. if z:B then converse(f)`z else converse(g)`z")]
   4.470 -        lam_injective 1);
   4.471 -by (auto_tac (claset(),
   4.472 -	      simpset() addsimps [inj_is_fun RS apply_type]));
   4.473 -by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
   4.474 -qed "inj_disjoint_Un";
   4.475 -
   4.476 -Goalw [surj_def]
   4.477 -    "[| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |]  \
   4.478 -\    ==> (f Un g) : surj(A Un C, B Un D)";
   4.479 -by (blast_tac (claset() addIs [fun_disjoint_apply1, fun_disjoint_apply2,
   4.480 -			      fun_disjoint_Un, trans]) 1);
   4.481 -qed "surj_disjoint_Un";
   4.482 -
   4.483 -(*A simple, high-level proof; the version for injections follows from it,
   4.484 -  using  f:inj(A,B) <-> f:bij(A,range(f))  *)
   4.485 -Goal "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] \
   4.486 -\     ==> (f Un g) : bij(A Un C, B Un D)";
   4.487 -by (rtac invertible_imp_bijective 1);
   4.488 -by (stac converse_Un 1);
   4.489 -by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
   4.490 -qed "bij_disjoint_Un";
   4.491 -
   4.492 -
   4.493 -(** Restrictions as surjections and bijections *)
   4.494 -
   4.495 -val prems = goalw (the_context ()) [surj_def]
   4.496 -    "f: Pi(A,B) ==> f: surj(A, f``A)";
   4.497 -val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
   4.498 -by (fast_tac (claset() addIs rls) 1);
   4.499 -qed "surj_image";
   4.500 -
   4.501 -Goal "restrict(f,A) `` B = f `` (A Int B)";
   4.502 -by (auto_tac (claset(), simpset() addsimps [restrict_def])); 
   4.503 -qed "restrict_image";
   4.504 -Addsimps [restrict_image];
   4.505 -
   4.506 -Goalw [inj_def]
   4.507 -    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
   4.508 -by (safe_tac (claset() addSEs [restrict_type2]));
   4.509 -by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
   4.510 -                          box_equals, restrict] 1));
   4.511 -qed "restrict_inj";
   4.512 -
   4.513 -Goal "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"; 
   4.514 -by (rtac (simplify (simpset() addsimps [restrict_image])
   4.515 -          (restrict_type2 RS surj_image)) 1);
   4.516 -by (REPEAT (assume_tac 1));
   4.517 -qed "restrict_surj";
   4.518 -
   4.519 -Goalw [inj_def,bij_def]
   4.520 -    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
   4.521 -by (blast_tac (claset() addSIs [restrict, restrict_surj]
   4.522 -		       addIs [box_equals, surj_is_fun]) 1);
   4.523 -qed "restrict_bij";
   4.524 -
   4.525 -
   4.526 -(*** Lemmas for Ramsey's Theorem ***)
   4.527 -
   4.528 -Goalw [inj_def] "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)";
   4.529 -by (blast_tac (claset() addIs [fun_weaken_type]) 1);
   4.530 -qed "inj_weaken_type";
   4.531 -
   4.532 -Goal "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
   4.533 -by (rtac (restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
   4.534 -by (assume_tac 1);
   4.535 -by (Blast_tac 1);
   4.536 -by (rewtac inj_def);
   4.537 -by (fast_tac (claset() addEs [range_type, mem_irrefl] 
   4.538 -	               addDs [apply_equality]) 1);
   4.539 -qed "inj_succ_restrict";
   4.540 -
   4.541 -Goalw [inj_def]
   4.542 -    "[| f: inj(A,B);  a~:A;  b~:B |] \
   4.543 -\    ==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
   4.544 -by (force_tac (claset() addIs [apply_type],
   4.545 -               simpset() addsimps [fun_extend, fun_extend_apply2,
   4.546 -						fun_extend_apply1]) 1);
   4.547 -qed "inj_extend";
   4.548 -
     5.1 --- a/src/ZF/Perm.thy	Thu May 23 17:05:21 2002 +0200
     5.2 +++ b/src/ZF/Perm.thy	Fri May 24 13:15:37 2002 +0200
     5.3 @@ -9,30 +9,662 @@
     5.4    -- Lemmas for the Schroeder-Bernstein Theorem
     5.5  *)
     5.6  
     5.7 -Perm = mono + func +
     5.8 -consts
     5.9 -  O     :: [i,i]=>i      (infixr 60)
    5.10 -
    5.11 -defs
    5.12 -  (*composition of relations and functions; NOT Suppes's relative product*)
    5.13 -  comp_def    "r O s == {xz : domain(s)*range(r) . 
    5.14 -                              EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    5.15 +theory Perm = mono + func:
    5.16  
    5.17  constdefs
    5.18 +
    5.19 +  (*composition of relations and functions; NOT Suppes's relative product*)
    5.20 +  comp     :: "[i,i]=>i"      (infixr "O" 60)
    5.21 +    "r O s == {xz : domain(s)*range(r) . 
    5.22 +               EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    5.23 +
    5.24    (*the identity function for A*)
    5.25 -  id    :: i=>i
    5.26 -  "id(A) == (lam x:A. x)"
    5.27 +  id    :: "i=>i"
    5.28 +    "id(A) == (lam x:A. x)"
    5.29  
    5.30    (*one-to-one functions from A to B*)
    5.31 -  inj   :: [i,i]=>i
    5.32 -  "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
    5.33 +  inj   :: "[i,i]=>i"
    5.34 +    "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
    5.35  
    5.36    (*onto functions from A to B*)
    5.37 -  surj  :: [i,i]=>i
    5.38 -  "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
    5.39 +  surj  :: "[i,i]=>i"
    5.40 +    "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
    5.41  
    5.42    (*one-to-one and onto functions*)
    5.43 -  bij   :: [i,i]=>i
    5.44 -  "bij(A,B) == inj(A,B) Int surj(A,B)"
    5.45 +  bij   :: "[i,i]=>i"
    5.46 +    "bij(A,B) == inj(A,B) Int surj(A,B)"
    5.47 +
    5.48 +
    5.49 +(** Surjective function space **)
    5.50 +
    5.51 +lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
    5.52 +apply (unfold surj_def)
    5.53 +apply (erule CollectD1)
    5.54 +done
    5.55 +
    5.56 +lemma fun_is_surj: "f : Pi(A,B) ==> f: surj(A,range(f))"
    5.57 +apply (unfold surj_def)
    5.58 +apply (blast intro: apply_equality range_of_fun domain_type)
    5.59 +done
    5.60 +
    5.61 +lemma surj_range: "f: surj(A,B) ==> range(f)=B"
    5.62 +apply (unfold surj_def)
    5.63 +apply (best intro: apply_Pair elim: range_type)
    5.64 +done
    5.65 +
    5.66 +(** A function with a right inverse is a surjection **)
    5.67 +
    5.68 +lemma f_imp_surjective: 
    5.69 +    "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y |]
    5.70 +     ==> f: surj(A,B)"
    5.71 +apply (simp add: surj_def) 
    5.72 +apply (blast)
    5.73 +done
    5.74 +
    5.75 +lemma lam_surjective: 
    5.76 +    "[| !!x. x:A ==> c(x): B;            
    5.77 +        !!y. y:B ==> d(y): A;            
    5.78 +        !!y. y:B ==> c(d(y)) = y         
    5.79 +     |] ==> (lam x:A. c(x)) : surj(A,B)"
    5.80 +apply (rule_tac d = "d" in f_imp_surjective) 
    5.81 +apply (simp_all add: lam_type)
    5.82 +done
    5.83 +
    5.84 +(*Cantor's theorem revisited*)
    5.85 +lemma cantor_surj: "f ~: surj(A,Pow(A))"
    5.86 +apply (unfold surj_def)
    5.87 +apply safe
    5.88 +apply (cut_tac cantor)
    5.89 +apply (best del: subsetI) 
    5.90 +done
    5.91 +
    5.92 +
    5.93 +(** Injective function space **)
    5.94 +
    5.95 +lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
    5.96 +apply (unfold inj_def)
    5.97 +apply (erule CollectD1)
    5.98 +done
    5.99 +
   5.100 +(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
   5.101 +lemma inj_equality: 
   5.102 +    "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
   5.103 +apply (unfold inj_def)
   5.104 +apply (blast dest: Pair_mem_PiD)
   5.105 +done
   5.106 +
   5.107 +lemma inj_apply_equality: "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b"
   5.108 +apply (unfold inj_def)
   5.109 +apply blast
   5.110 +done
   5.111 +
   5.112 +(** A function with a left inverse is an injection **)
   5.113 +
   5.114 +lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"
   5.115 +apply (simp (no_asm_simp) add: inj_def)
   5.116 +apply (blast intro: subst_context [THEN box_equals])
   5.117 +done
   5.118 +
   5.119 +lemma lam_injective: 
   5.120 +    "[| !!x. x:A ==> c(x): B;            
   5.121 +        !!x. x:A ==> d(c(x)) = x |]
   5.122 +     ==> (lam x:A. c(x)) : inj(A,B)"
   5.123 +apply (rule_tac d = "d" in f_imp_injective)
   5.124 +apply (simp_all add: lam_type)
   5.125 +done
   5.126 +
   5.127 +(** Bijections **)
   5.128 +
   5.129 +lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
   5.130 +apply (unfold bij_def)
   5.131 +apply (erule IntD1)
   5.132 +done
   5.133 +
   5.134 +lemma bij_is_surj: "f: bij(A,B) ==> f: surj(A,B)"
   5.135 +apply (unfold bij_def)
   5.136 +apply (erule IntD2)
   5.137 +done
   5.138 +
   5.139 +(* f: bij(A,B) ==> f: A->B *)
   5.140 +lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard]
   5.141 +
   5.142 +lemma lam_bijective: 
   5.143 +    "[| !!x. x:A ==> c(x): B;            
   5.144 +        !!y. y:B ==> d(y): A;            
   5.145 +        !!x. x:A ==> d(c(x)) = x;        
   5.146 +        !!y. y:B ==> c(d(y)) = y         
   5.147 +     |] ==> (lam x:A. c(x)) : bij(A,B)"
   5.148 +apply (unfold bij_def)
   5.149 +apply (blast intro!: lam_injective lam_surjective);
   5.150 +done
   5.151 +
   5.152 +lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))   
   5.153 +      ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
   5.154 +apply (rule_tac d = "f" in lam_bijective)
   5.155 +apply (auto simp add: the_equality2)
   5.156 +done
   5.157 +
   5.158 +
   5.159 +(** Identity function **)
   5.160 +
   5.161 +lemma idI [intro!]: "a:A ==> <a,a> : id(A)"
   5.162 +apply (unfold id_def)
   5.163 +apply (erule lamI)
   5.164 +done
   5.165 +
   5.166 +lemma idE [elim!]: "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P |] ==>  P"
   5.167 +apply (simp add: id_def lam_def) 
   5.168 +apply (blast intro: elim:); 
   5.169 +done
   5.170 +
   5.171 +lemma id_type: "id(A) : A->A"
   5.172 +apply (unfold id_def)
   5.173 +apply (rule lam_type)
   5.174 +apply assumption
   5.175 +done
   5.176 +
   5.177 +lemma id_conv [simp]: "x:A ==> id(A)`x = x"
   5.178 +apply (unfold id_def)
   5.179 +apply (simp (no_asm_simp))
   5.180 +done
   5.181 +
   5.182 +lemma id_mono: "A<=B ==> id(A) <= id(B)"
   5.183 +apply (unfold id_def)
   5.184 +apply (erule lam_mono)
   5.185 +done
   5.186 +
   5.187 +lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
   5.188 +apply (simp add: inj_def id_def)
   5.189 +apply (blast intro: lam_type) 
   5.190 +done
   5.191 +
   5.192 +lemmas id_inj = subset_refl [THEN id_subset_inj, standard]
   5.193 +
   5.194 +lemma id_surj: "id(A): surj(A,A)"
   5.195 +apply (unfold id_def surj_def)
   5.196 +apply (simp (no_asm_simp))
   5.197 +done
   5.198 +
   5.199 +lemma id_bij: "id(A): bij(A,A)"
   5.200 +apply (unfold bij_def)
   5.201 +apply (blast intro: id_inj id_surj)
   5.202 +done
   5.203 +
   5.204 +lemma subset_iff_id: "A <= B <-> id(A) : A->B"
   5.205 +apply (unfold id_def)
   5.206 +apply (force intro!: lam_type dest: apply_type);
   5.207 +done
   5.208 +
   5.209 +
   5.210 +(*** Converse of a function ***)
   5.211 +
   5.212 +lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A"
   5.213 +apply (unfold inj_def)
   5.214 +apply (simp (no_asm_simp) add: Pi_iff function_def)
   5.215 +apply (erule CollectE)
   5.216 +apply (simp (no_asm_simp) add: apply_iff)
   5.217 +apply (blast dest: fun_is_rel)
   5.218 +done
   5.219 +
   5.220 +(** Equations for converse(f) **)
   5.221 +
   5.222 +(*The premises are equivalent to saying that f is injective...*) 
   5.223 +lemma left_inverse_lemma:
   5.224 +     "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a"
   5.225 +by (blast intro: apply_Pair apply_equality converseI)
   5.226 +
   5.227 +lemma left_inverse [simp]: "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a"
   5.228 +apply (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)
   5.229 +done
   5.230 +
   5.231 +lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard]
   5.232 +
   5.233 +lemma right_inverse_lemma:
   5.234 +     "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
   5.235 +apply (rule apply_Pair [THEN converseD [THEN apply_equality]])
   5.236 +apply (auto ); 
   5.237 +done
   5.238 +
   5.239 +(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
   5.240 +  No: they would not imply that converse(f) was a function! *)
   5.241 +lemma right_inverse [simp]:
   5.242 +     "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b"
   5.243 +by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
   5.244 +
   5.245 +lemma right_inverse_bij: "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b"
   5.246 +apply (force simp add: bij_def surj_range)
   5.247 +done
   5.248 +
   5.249 +(** Converses of injections, surjections, bijections **)
   5.250 +
   5.251 +lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
   5.252 +apply (rule f_imp_injective)
   5.253 +apply (erule inj_converse_fun)
   5.254 +apply (clarify ); 
   5.255 +apply (rule right_inverse);
   5.256 + apply assumption
   5.257 +apply (blast intro: elim:); 
   5.258 +done
   5.259 +
   5.260 +lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
   5.261 +by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun 
   5.262 +                 range_of_fun [THEN apply_type])
   5.263 +
   5.264 +(*Adding this as an intro! rule seems to cause looping*)
   5.265 +lemma bij_converse_bij [TC]: "f: bij(A,B) ==> converse(f): bij(B,A)"
   5.266 +apply (unfold bij_def)
   5.267 +apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
   5.268 +done
   5.269 +
   5.270 +
   5.271 +
   5.272 +(** Composition of two relations **)
   5.273 +
   5.274 +(*The inductive definition package could derive these theorems for (r O s)*)
   5.275 +
   5.276 +lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
   5.277 +apply (unfold comp_def)
   5.278 +apply blast
   5.279 +done
   5.280 +
   5.281 +lemma compE [elim!]: 
   5.282 +    "[| xz : r O s;   
   5.283 +        !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
   5.284 +     ==> P"
   5.285 +apply (unfold comp_def)
   5.286 +apply blast
   5.287 +done
   5.288 +
   5.289 +lemma compEpair: 
   5.290 +    "[| <a,c> : r O s;   
   5.291 +        !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
   5.292 +     ==> P"
   5.293 +apply (erule compE)
   5.294 +apply (simp add: );  
   5.295 +done
   5.296 +
   5.297 +lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
   5.298 +apply blast
   5.299 +done
   5.300 +
   5.301 +
   5.302 +(** Domain and Range -- see Suppes, section 3.1 **)
   5.303 +
   5.304 +(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
   5.305 +lemma range_comp: "range(r O s) <= range(r)"
   5.306 +apply blast
   5.307 +done
   5.308 +
   5.309 +lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)"
   5.310 +apply (rule range_comp [THEN equalityI])
   5.311 +apply blast
   5.312 +done
   5.313 +
   5.314 +lemma domain_comp: "domain(r O s) <= domain(s)"
   5.315 +apply blast
   5.316 +done
   5.317 +
   5.318 +lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)"
   5.319 +apply (rule domain_comp [THEN equalityI])
   5.320 +apply blast
   5.321 +done
   5.322 +
   5.323 +lemma image_comp: "(r O s)``A = r``(s``A)"
   5.324 +apply blast
   5.325 +done
   5.326 +
   5.327 +
   5.328 +(** Other results **)
   5.329 +
   5.330 +lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
   5.331 +apply blast
   5.332 +done
   5.333 +
   5.334 +(*composition preserves relations*)
   5.335 +lemma comp_rel: "[| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C"
   5.336 +apply blast
   5.337 +done
   5.338 +
   5.339 +(*associative law for composition*)
   5.340 +lemma comp_assoc: "(r O s) O t = r O (s O t)"
   5.341 +apply blast
   5.342 +done
   5.343 +
   5.344 +(*left identity of composition; provable inclusions are
   5.345 +        id(A) O r <= r       
   5.346 +  and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
   5.347 +lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
   5.348 +apply blast
   5.349 +done
   5.350 +
   5.351 +(*right identity of composition; provable inclusions are
   5.352 +        r O id(A) <= r
   5.353 +  and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
   5.354 +lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
   5.355 +apply blast
   5.356 +done
   5.357 +
   5.358 +
   5.359 +(** Composition preserves functions, injections, and surjections **)
   5.360 +
   5.361 +lemma comp_function: 
   5.362 +    "[| function(g);  function(f) |] ==> function(f O g)"
   5.363 +apply (unfold function_def)
   5.364 +apply blast
   5.365 +done
   5.366 +
   5.367 +(*Don't think the premises can be weakened much*)
   5.368 +lemma comp_fun: "[| g: A->B;  f: B->C |] ==> (f O g) : A->C"
   5.369 +apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
   5.370 +apply (subst range_rel_subset [THEN domain_comp_eq]);
   5.371 +apply (auto ); 
   5.372 +done
   5.373 +
   5.374 +(*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
   5.375 +lemma comp_fun_apply [simp]:
   5.376 +     "[| g: A->B;  a:A |] ==> (f O g)`a = f`(g`a)"
   5.377 +apply (frule apply_Pair, assumption) 
   5.378 +apply (simp add: apply_def image_comp)
   5.379 +apply (blast dest: apply_equality) 
   5.380 +done
   5.381 +
   5.382 +(*Simplifies compositions of lambda-abstractions*)
   5.383 +lemma comp_lam: 
   5.384 +    "[| !!x. x:A ==> b(x): B |]
   5.385 +     ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"
   5.386 +apply (subgoal_tac "(lam x:A. b(x)) : A -> B") 
   5.387 + apply (rule fun_extension)
   5.388 +   apply (blast intro: comp_fun lam_funtype)
   5.389 +  apply (rule lam_funtype)
   5.390 + apply (simp add: ); 
   5.391 +apply (simp add: lam_type); 
   5.392 +done
   5.393 +
   5.394 +lemma comp_inj:
   5.395 +     "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)"
   5.396 +apply (frule inj_is_fun [of g]) 
   5.397 +apply (frule inj_is_fun [of f]) 
   5.398 +apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
   5.399 + apply (blast intro: comp_fun);
   5.400 +apply (simp add: );  
   5.401 +done
   5.402 +
   5.403 +lemma comp_surj: 
   5.404 +    "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)"
   5.405 +apply (unfold surj_def)
   5.406 +apply (blast intro!: comp_fun comp_fun_apply)
   5.407 +done
   5.408 +
   5.409 +lemma comp_bij: 
   5.410 +    "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)"
   5.411 +apply (unfold bij_def)
   5.412 +apply (blast intro: comp_inj comp_surj)
   5.413 +done
   5.414 +
   5.415 +
   5.416 +(** Dual properties of inj and surj -- useful for proofs from
   5.417 +    D Pastre.  Automatic theorem proving in set theory. 
   5.418 +    Artificial Intelligence, 10:1--27, 1978. **)
   5.419 +
   5.420 +lemma comp_mem_injD1: 
   5.421 +    "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
   5.422 +apply (unfold inj_def)
   5.423 +apply (force ); 
   5.424 +done
   5.425 +
   5.426 +lemma comp_mem_injD2: 
   5.427 +    "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
   5.428 +apply (unfold inj_def surj_def)
   5.429 +apply safe
   5.430 +apply (rule_tac x1 = "x" in bspec [THEN bexE])
   5.431 +apply (erule_tac [3] x1 = "w" in bspec [THEN bexE])
   5.432 +apply assumption+
   5.433 +apply safe
   5.434 +apply (rule_tac t = "op ` (g) " in subst_context)
   5.435 +apply (erule asm_rl bspec [THEN bspec, THEN mp])+
   5.436 +apply (simp (no_asm_simp))
   5.437 +done
   5.438 +
   5.439 +lemma comp_mem_surjD1: 
   5.440 +    "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)"
   5.441 +apply (unfold surj_def)
   5.442 +apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
   5.443 +done
   5.444 +
   5.445 +
   5.446 +lemma comp_mem_surjD2: 
   5.447 +    "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)"
   5.448 +apply (unfold inj_def surj_def)
   5.449 +apply safe
   5.450 +apply (drule_tac x = "f`y" in bspec);
   5.451 +apply (auto );  
   5.452 +apply (blast intro: apply_funtype)
   5.453 +done
   5.454 +
   5.455 +(** inverses of composition **)
   5.456 +
   5.457 +(*left inverse of composition; one inclusion is
   5.458 +        f: A->B ==> id(A) <= converse(f) O f *)
   5.459 +lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
   5.460 +apply (unfold inj_def)
   5.461 +apply (clarify ); 
   5.462 +apply (rule equalityI) 
   5.463 + apply (auto simp add: apply_iff)
   5.464 +apply (blast intro: elim:);  
   5.465 +done
   5.466 +
   5.467 +(*right inverse of composition; one inclusion is
   5.468 +                f: A->B ==> f O converse(f) <= id(B) 
   5.469 +*)
   5.470 +lemma right_comp_inverse: 
   5.471 +    "f: surj(A,B) ==> f O converse(f) = id(B)"
   5.472 +apply (simp add: surj_def) 
   5.473 +apply (clarify ); 
   5.474 +apply (rule equalityI)
   5.475 +apply (best elim: domain_type range_type dest: apply_equality2)
   5.476 +apply (blast intro: apply_Pair)
   5.477 +done
   5.478 +
   5.479 +
   5.480 +(** Proving that a function is a bijection **)
   5.481 +
   5.482 +lemma comp_eq_id_iff: 
   5.483 +    "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"
   5.484 +apply (unfold id_def)
   5.485 +apply safe
   5.486 + apply (drule_tac t = "%h. h`y " in subst_context)
   5.487 + apply simp
   5.488 +apply (rule fun_extension)
   5.489 +  apply (blast intro: comp_fun lam_type)
   5.490 + apply auto
   5.491 +done
   5.492 +
   5.493 +lemma fg_imp_bijective: 
   5.494 +    "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f : bij(A,B)"
   5.495 +apply (unfold bij_def)
   5.496 +apply (simp add: comp_eq_id_iff)
   5.497 +apply (blast intro: f_imp_injective f_imp_surjective apply_funtype);
   5.498 +done
   5.499 +
   5.500 +lemma nilpotent_imp_bijective: "[| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)"
   5.501 +apply (blast intro: fg_imp_bijective)
   5.502 +done
   5.503 +
   5.504 +lemma invertible_imp_bijective: "[| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)"
   5.505 +apply (simp (no_asm_simp) add: fg_imp_bijective comp_eq_id_iff left_inverse_lemma right_inverse_lemma)
   5.506 +done
   5.507 +
   5.508 +(** Unions of functions -- cf similar theorems on func.ML **)
   5.509 +
   5.510 +(*Theorem by KG, proof by LCP*)
   5.511 +lemma inj_disjoint_Un:
   5.512 +     "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |]  
   5.513 +      ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)"
   5.514 +apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" in lam_injective)
   5.515 +apply (auto simp add: inj_is_fun [THEN apply_type])
   5.516 +apply (blast intro: inj_is_fun [THEN apply_type])
   5.517 +done
   5.518 +
   5.519 +lemma surj_disjoint_Un: 
   5.520 +    "[| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |]   
   5.521 +     ==> (f Un g) : surj(A Un C, B Un D)"
   5.522 +apply (unfold surj_def)
   5.523 +apply (blast intro: fun_disjoint_apply1 fun_disjoint_apply2 fun_disjoint_Un trans)
   5.524 +done
   5.525 +
   5.526 +(*A simple, high-level proof; the version for injections follows from it,
   5.527 +  using  f:inj(A,B) <-> f:bij(A,range(f))  *)
   5.528 +lemma bij_disjoint_Un:
   5.529 +     "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |]  
   5.530 +      ==> (f Un g) : bij(A Un C, B Un D)"
   5.531 +apply (rule invertible_imp_bijective)
   5.532 +apply (subst converse_Un)
   5.533 +apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
   5.534 +done
   5.535 +
   5.536 +
   5.537 +(** Restrictions as surjections and bijections *)
   5.538 +
   5.539 +lemma surj_image:
   5.540 +    "f: Pi(A,B) ==> f: surj(A, f``A)"
   5.541 +apply (simp add: surj_def); 
   5.542 +apply (blast intro: apply_equality apply_Pair Pi_type); 
   5.543 +done
   5.544 +
   5.545 +lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)"
   5.546 +apply (auto simp add: restrict_def)
   5.547 +done
   5.548 +
   5.549 +lemma restrict_inj: 
   5.550 +    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
   5.551 +apply (unfold inj_def)
   5.552 +apply (safe elim!: restrict_type2); 
   5.553 +apply (auto ); 
   5.554 +done
   5.555 +
   5.556 +lemma restrict_surj: "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
   5.557 +apply (insert restrict_type2 [THEN surj_image])
   5.558 +apply (simp add: restrict_image); 
   5.559 +done
   5.560 +
   5.561 +lemma restrict_bij: 
   5.562 +    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
   5.563 +apply (unfold inj_def bij_def)
   5.564 +apply (blast intro!: restrict restrict_surj intro: box_equals surj_is_fun)
   5.565 +done
   5.566 +
   5.567 +
   5.568 +(*** Lemmas for Ramsey's Theorem ***)
   5.569 +
   5.570 +lemma inj_weaken_type: "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)"
   5.571 +apply (unfold inj_def)
   5.572 +apply (blast intro: fun_weaken_type)
   5.573 +done
   5.574 +
   5.575 +lemma inj_succ_restrict:
   5.576 +     "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
   5.577 +apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type])
   5.578 +apply assumption
   5.579 +apply blast
   5.580 +apply (unfold inj_def)
   5.581 +apply (fast elim: range_type mem_irrefl dest: apply_equality)
   5.582 +done
   5.583 +
   5.584 +
   5.585 +lemma inj_extend: 
   5.586 +    "[| f: inj(A,B);  a~:A;  b~:B |]  
   5.587 +     ==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))"
   5.588 +apply (unfold inj_def)
   5.589 +apply (force intro: apply_type  simp add: fun_extend)
   5.590 +done
   5.591 +
   5.592 +
   5.593 +ML
   5.594 +{*
   5.595 +val comp_def = thm "comp_def";
   5.596 +val id_def = thm "id_def";
   5.597 +val inj_def = thm "inj_def";
   5.598 +val surj_def = thm "surj_def";
   5.599 +val bij_def = thm "bij_def";
   5.600 +
   5.601 +val surj_is_fun = thm "surj_is_fun";
   5.602 +val fun_is_surj = thm "fun_is_surj";
   5.603 +val surj_range = thm "surj_range";
   5.604 +val f_imp_surjective = thm "f_imp_surjective";
   5.605 +val lam_surjective = thm "lam_surjective";
   5.606 +val cantor_surj = thm "cantor_surj";
   5.607 +val inj_is_fun = thm "inj_is_fun";
   5.608 +val inj_equality = thm "inj_equality";
   5.609 +val inj_apply_equality = thm "inj_apply_equality";
   5.610 +val f_imp_injective = thm "f_imp_injective";
   5.611 +val lam_injective = thm "lam_injective";
   5.612 +val bij_is_inj = thm "bij_is_inj";
   5.613 +val bij_is_surj = thm "bij_is_surj";
   5.614 +val bij_is_fun = thm "bij_is_fun";
   5.615 +val lam_bijective = thm "lam_bijective";
   5.616 +val RepFun_bijective = thm "RepFun_bijective";
   5.617 +val idI = thm "idI";
   5.618 +val idE = thm "idE";
   5.619 +val id_type = thm "id_type";
   5.620 +val id_conv = thm "id_conv";
   5.621 +val id_mono = thm "id_mono";
   5.622 +val id_subset_inj = thm "id_subset_inj";
   5.623 +val id_inj = thm "id_inj";
   5.624 +val id_surj = thm "id_surj";
   5.625 +val id_bij = thm "id_bij";
   5.626 +val subset_iff_id = thm "subset_iff_id";
   5.627 +val inj_converse_fun = thm "inj_converse_fun";
   5.628 +val left_inverse_lemma = thm "left_inverse_lemma";
   5.629 +val left_inverse = thm "left_inverse";
   5.630 +val left_inverse_bij = thm "left_inverse_bij";
   5.631 +val right_inverse_lemma = thm "right_inverse_lemma";
   5.632 +val right_inverse = thm "right_inverse";
   5.633 +val right_inverse_bij = thm "right_inverse_bij";
   5.634 +val inj_converse_inj = thm "inj_converse_inj";
   5.635 +val inj_converse_surj = thm "inj_converse_surj";
   5.636 +val bij_converse_bij = thm "bij_converse_bij";
   5.637 +val compI = thm "compI";
   5.638 +val compE = thm "compE";
   5.639 +val compEpair = thm "compEpair";
   5.640 +val converse_comp = thm "converse_comp";
   5.641 +val range_comp = thm "range_comp";
   5.642 +val range_comp_eq = thm "range_comp_eq";
   5.643 +val domain_comp = thm "domain_comp";
   5.644 +val domain_comp_eq = thm "domain_comp_eq";
   5.645 +val image_comp = thm "image_comp";
   5.646 +val comp_mono = thm "comp_mono";
   5.647 +val comp_rel = thm "comp_rel";
   5.648 +val comp_assoc = thm "comp_assoc";
   5.649 +val left_comp_id = thm "left_comp_id";
   5.650 +val right_comp_id = thm "right_comp_id";
   5.651 +val comp_function = thm "comp_function";
   5.652 +val comp_fun = thm "comp_fun";
   5.653 +val comp_fun_apply = thm "comp_fun_apply";
   5.654 +val comp_lam = thm "comp_lam";
   5.655 +val comp_inj = thm "comp_inj";
   5.656 +val comp_surj = thm "comp_surj";
   5.657 +val comp_bij = thm "comp_bij";
   5.658 +val comp_mem_injD1 = thm "comp_mem_injD1";
   5.659 +val comp_mem_injD2 = thm "comp_mem_injD2";
   5.660 +val comp_mem_surjD1 = thm "comp_mem_surjD1";
   5.661 +val comp_mem_surjD2 = thm "comp_mem_surjD2";
   5.662 +val left_comp_inverse = thm "left_comp_inverse";
   5.663 +val right_comp_inverse = thm "right_comp_inverse";
   5.664 +val comp_eq_id_iff = thm "comp_eq_id_iff";
   5.665 +val fg_imp_bijective = thm "fg_imp_bijective";
   5.666 +val nilpotent_imp_bijective = thm "nilpotent_imp_bijective";
   5.667 +val invertible_imp_bijective = thm "invertible_imp_bijective";
   5.668 +val inj_disjoint_Un = thm "inj_disjoint_Un";
   5.669 +val surj_disjoint_Un = thm "surj_disjoint_Un";
   5.670 +val bij_disjoint_Un = thm "bij_disjoint_Un";
   5.671 +val surj_image = thm "surj_image";
   5.672 +val restrict_image = thm "restrict_image";
   5.673 +val restrict_inj = thm "restrict_inj";
   5.674 +val restrict_surj = thm "restrict_surj";
   5.675 +val restrict_bij = thm "restrict_bij";
   5.676 +val inj_weaken_type = thm "inj_weaken_type";
   5.677 +val inj_succ_restrict = thm "inj_succ_restrict";
   5.678 +val inj_extend = thm "inj_extend";
   5.679 +*}
   5.680  
   5.681  end
     6.1 --- a/src/ZF/UNITY/Constrains.ML	Thu May 23 17:05:21 2002 +0200
     6.2 +++ b/src/ZF/UNITY/Constrains.ML	Fri May 24 13:15:37 2002 +0200
     6.3 @@ -470,6 +470,7 @@
     6.4  by (cut_inst_tac [("F", "xa")] Acts_type 1);
     6.5  by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
     6.6  by Auto_tac;
     6.7 +by (rename_tac "xa xc xd act xe xf" 1);
     6.8  by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); 
     6.9  by (dres_inst_tac [("x", "f`xf")] bspec 1);
    6.10  by Auto_tac;
     7.1 --- a/src/ZF/UNITY/UNITY.ML	Thu May 23 17:05:21 2002 +0200
     7.2 +++ b/src/ZF/UNITY/UNITY.ML	Fri May 24 13:15:37 2002 +0200
     7.3 @@ -722,6 +722,7 @@
     7.4  by (cut_inst_tac [("F", "xa")] Acts_type 1);
     7.5  by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
     7.6  by Auto_tac;
     7.7 +by (rename_tac "xa xc xd act xe xf" 1);
     7.8  by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); 
     7.9  by (dres_inst_tac [("x", "f`xf")] bspec 1);
    7.10  by Auto_tac;
     8.1 --- a/src/ZF/ex/Limit.thy	Thu May 23 17:05:21 2002 +0200
     8.2 +++ b/src/ZF/ex/Limit.thy	Fri May 24 13:15:37 2002 +0200
     8.3 @@ -772,21 +772,20 @@
     8.4      "cpo(D) ==> id(set(D)) \<in> cont(D,D)"
     8.5  by (simp add: id_type contI cpo_lub [THEN islub_in] chain_fun [THEN eta])
     8.6  
     8.7 -
     8.8 -lemmas comp_cont_apply =  cont_fun [THEN comp_fun_apply, OF _ cont_fun];
     8.9 +lemmas comp_cont_apply =  cont_fun [THEN comp_fun_apply]
    8.10  
    8.11  lemma comp_pres_cont [TC]:
    8.12      "[| f \<in> cont(D',E); g \<in> cont(D,D'); cpo(D)|] ==> f O g \<in> cont(D,E)"
    8.13  apply (rule contI)
    8.14  apply (rule_tac [2] comp_cont_apply [THEN ssubst])
    8.15 -apply (rule_tac [5] comp_cont_apply [THEN ssubst])
    8.16 -apply (rule_tac [8] cont_mono)
    8.17 -apply (rule_tac [9] cont_mono) (* 15 subgoals *)
    8.18 +apply (rule_tac [4] comp_cont_apply [THEN ssubst])
    8.19 +apply (rule_tac [6] cont_mono)
    8.20 +apply (rule_tac [7] cont_mono) (* 13 subgoals *)
    8.21  apply typecheck (* proves all but the lub case *)
    8.22  apply (subst comp_cont_apply)
    8.23 -apply (rule_tac [4] cont_lub [THEN ssubst])
    8.24 -apply (rule_tac [6] cont_lub [THEN ssubst])
    8.25 -prefer 8 apply (simp add: comp_cont_apply chain_in)
    8.26 +apply (rule_tac [3] cont_lub [THEN ssubst])
    8.27 +apply (rule_tac [5] cont_lub [THEN ssubst])
    8.28 +prefer 7 apply (simp add: comp_cont_apply chain_in)
    8.29  apply (auto intro: cpo_lub [THEN islub_in] cont_chain)
    8.30  done
    8.31  
    8.32 @@ -797,8 +796,8 @@
    8.33       ==> rel(cf(D,E),f O g,f' O g')"
    8.34  apply (rule rel_cfI) 
    8.35  apply (subst comp_cont_apply)
    8.36 -apply (rule_tac [4] comp_cont_apply [THEN ssubst])
    8.37 -apply (rule_tac [7] cpo_trans)
    8.38 +apply (rule_tac [3] comp_cont_apply [THEN ssubst])
    8.39 +apply (rule_tac [5] cpo_trans)
    8.40  apply (assumption | rule rel_cf cont_mono cont_map comp_pres_cont)+
    8.41  done
    8.42  
    8.43 @@ -810,10 +809,10 @@
    8.44  apply simp
    8.45  apply (rule rel_cfI)
    8.46  apply (rule comp_cont_apply [THEN ssubst])
    8.47 -apply (rule_tac [4] comp_cont_apply [THEN ssubst])
    8.48 -apply (rule_tac [7] cpo_trans)
    8.49 -apply (rule_tac [8] rel_cf)
    8.50 -apply (rule_tac [10] cont_mono) 
    8.51 +apply (rule_tac [3] comp_cont_apply [THEN ssubst])
    8.52 +apply (rule_tac [5] cpo_trans)
    8.53 +apply (rule_tac [6] rel_cf)
    8.54 +apply (rule_tac [8] cont_mono) 
    8.55  apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont] 
    8.56                      cont_map chain_rel rel_cf)+
    8.57  done
    8.58 @@ -826,8 +825,7 @@
    8.59  apply (assumption | 
    8.60         rule comp_fun cf_cont [THEN cont_fun]  cpo_lub [THEN islub_in]  
    8.61              cpo_cf chain_cf_comp)+
    8.62 -apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply,
    8.63 -                           OF _ _ chain_in [THEN cf_cont]])
    8.64 +apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply])
    8.65  apply (subst comp_cont_apply)
    8.66  apply (assumption | rule cpo_lub [THEN islub_in, THEN cf_cont]  cpo_cf)+
    8.67  apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub] 
    8.68 @@ -1790,15 +1788,15 @@
    8.69  apply (assumption | rule e_less_cont [THEN cont_fun]  apply_type Dinf_prod)+
    8.70  apply (rule_tac x1 = x and n1 = xa in Dinf_eq [THEN subst])
    8.71  apply (rule_tac [3] comp_fun_apply [THEN subst])
    8.72 -apply (rename_tac [6] y)
    8.73 -apply (rule_tac [6] P = 
    8.74 +apply (rename_tac [5] y)
    8.75 +apply (rule_tac [5] P = 
    8.76           "%z. rel(DD`succ(y), 
    8.77                    (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
    8.78                    z)"
    8.79         in id_conv [THEN subst])
    8.80 -apply (rule_tac [7] rel_cf)
    8.81 +apply (rule_tac [6] rel_cf)
    8.82  (* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
    8.83 -(* solves 11 of 12 subgoals *)
    8.84 +(* solves 10 of 11 subgoals *)
    8.85  apply (assumption |
    8.86         rule Dinf_prod [THEN apply_type] cont_fun Rp_cont e_less_cont
    8.87              emb_cont emb_chain_emb emb_chain_cpo apply_type embRp_rel
    8.88 @@ -1825,7 +1823,7 @@
    8.89  apply (drule mp, assumption)
    8.90  apply (subst e_gr_le)
    8.91  apply (rule_tac [4] comp_fun_apply [THEN ssubst])
    8.92 -apply (rule_tac [7] Dinf_eq [THEN ssubst])
    8.93 +apply (rule_tac [6] Dinf_eq [THEN ssubst])
    8.94  apply (assumption | 
    8.95         rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont 
    8.96              apply_type Dinf_prod nat_succI)+
    8.97 @@ -1871,8 +1869,8 @@
    8.98  apply (rule fun_extension)
    8.99  apply (rule_tac [3] id_conv [THEN ssubst])
   8.100  apply (rule_tac [4] comp_fun_apply [THEN ssubst])
   8.101 -apply (rule_tac [7] beta [THEN ssubst])
   8.102 -apply (rule_tac [8] rho_emb_id [THEN ssubst])
   8.103 +apply (rule_tac [6] beta [THEN ssubst])
   8.104 +apply (rule_tac [7] rho_emb_id [THEN ssubst])
   8.105  apply (assumption | 
   8.106         rule comp_fun id_type lam_type rho_emb_fun Dinf_prod [THEN apply_type]
   8.107              apply_type refl)+
   8.108 @@ -1880,10 +1878,10 @@
   8.109  apply (rule rel_cfI) (* ------------------>>>Yields type cond, not in HOL *)
   8.110  apply (subst id_conv)
   8.111  apply (rule_tac [2] comp_fun_apply [THEN ssubst])
   8.112 -apply (rule_tac [5] beta [THEN ssubst])
   8.113 -apply (rule_tac [6] rho_emb_apply1 [THEN ssubst])
   8.114 -apply (rule_tac [7] rel_DinfI) 
   8.115 -apply (rule_tac [7] beta [THEN ssubst])
   8.116 +apply (rule_tac [4] beta [THEN ssubst])
   8.117 +apply (rule_tac [5] rho_emb_apply1 [THEN ssubst])
   8.118 +apply (rule_tac [6] rel_DinfI) 
   8.119 +apply (rule_tac [6] beta [THEN ssubst])
   8.120  (* Dinf_prod bad with lam_type *)
   8.121  apply (assumption |
   8.122         rule eps1 lam_type rho_emb_fun eps_fun
   8.123 @@ -1928,11 +1926,11 @@
   8.124  apply (assumption | rule emb_rho_emb)+
   8.125  apply (rule fun_extension) (* Manual instantiation in HOL. *)
   8.126  apply (rule_tac [3] comp_fun_apply [THEN ssubst])
   8.127 -apply (rule_tac [6] fun_extension) (*Next, clean up and instantiate unknowns *)
   8.128 +apply (rule_tac [5] fun_extension) (*Next, clean up and instantiate unknowns *)
   8.129  apply (assumption | rule comp_fun rho_emb_fun eps_fun Dinf_prod apply_type)+
   8.130  apply (simp add: rho_emb_apply2 eps_fun [THEN apply_type])
   8.131  apply (rule comp_fun_apply [THEN subst])
   8.132 -apply (rule_tac [4] eps_split_left [THEN subst])
   8.133 +apply (rule_tac [3] eps_split_left [THEN subst])
   8.134  apply (auto intro: eps_fun)
   8.135  done
   8.136  
     9.1 --- a/src/ZF/func.thy	Thu May 23 17:05:21 2002 +0200
     9.2 +++ b/src/ZF/func.thy	Fri May 24 13:15:37 2002 +0200
     9.3 @@ -57,9 +57,7 @@
     9.4  
     9.5  (*Applying a function outside its domain yields 0*)
     9.6  lemma apply_0: "a ~: domain(f) ==> f`a = 0"
     9.7 -apply (unfold apply_def)
     9.8 -apply (blast intro: elim:); 
     9.9 -done
    9.10 +by (unfold apply_def, blast)
    9.11  
    9.12  lemma Pi_memberD: "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>"
    9.13  apply (frule fun_is_rel)
    9.14 @@ -67,12 +65,9 @@
    9.15  done
    9.16  
    9.17  lemma function_apply_Pair: "[| function(f);  a : domain(f)|] ==> <a,f`a>: f"
    9.18 -apply (simp add: function_def)
    9.19 -apply (clarify ); 
    9.20 -apply (subgoal_tac "f`a = y") 
    9.21 -apply (blast intro: elim:); 
    9.22 -apply (simp add: apply_def); 
    9.23 -apply (blast intro: elim:); 
    9.24 +apply (simp add: function_def, clarify) 
    9.25 +apply (subgoal_tac "f`a = y", blast) 
    9.26 +apply (simp add: apply_def, blast) 
    9.27  done
    9.28  
    9.29  lemma apply_Pair: "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f"
    9.30 @@ -141,7 +136,7 @@
    9.31  by (simp add: lam_def Pi_def function_def, blast)
    9.32  
    9.33  lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}"
    9.34 -by (blast intro: lam_type);
    9.35 +by (blast intro: lam_type)
    9.36  
    9.37  lemma function_lam: "function (lam x:A. b(x))"
    9.38  by (simp add: function_def lam_def) 
    9.39 @@ -150,14 +145,10 @@
    9.40  by (simp add: relation_def lam_def) 
    9.41  
    9.42  lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)"
    9.43 -apply (simp add: apply_def lam_def) 
    9.44 -apply (blast intro: elim:); 
    9.45 -done
    9.46 +by (simp add: apply_def lam_def, blast)
    9.47  
    9.48  lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
    9.49 -apply (simp add: apply_def lam_def) 
    9.50 -apply (blast intro: elim:); 
    9.51 -done
    9.52 +by (simp add: apply_def lam_def, blast)
    9.53  
    9.54  lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
    9.55  by (simp add: lam_def)
    9.56 @@ -173,7 +164,7 @@
    9.57  lemma lam_theI:
    9.58      "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
    9.59  apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI)
    9.60 -apply (simp add: ); 
    9.61 +apply simp 
    9.62  apply (blast intro: theI)
    9.63  done
    9.64  
    9.65 @@ -273,9 +264,7 @@
    9.66  by (simp add: Pi_iff function_def restrict_def, blast)
    9.67  
    9.68  lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
    9.69 -apply (simp add: apply_def restrict_def)
    9.70 -apply (blast intro: elim:); 
    9.71 -done
    9.72 +by (simp add: apply_def restrict_def, blast)
    9.73  
    9.74  lemma restrict_empty [simp]: "restrict(f,0) = 0"
    9.75  apply (unfold restrict_def)
    9.76 @@ -395,14 +384,14 @@
    9.77       "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"
    9.78  by (blast intro: fun_extend [THEN fun_weaken_type])
    9.79  
    9.80 -lemma fun_extend_apply1: "[| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a"
    9.81 -apply (rule apply_Pair [THEN consI2, THEN apply_equality])
    9.82 -apply (rule_tac [3] fun_extend, assumption+)
    9.83 -done
    9.84 +lemma extend_apply:
    9.85 +     "c ~: domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
    9.86 +by (auto simp add: apply_def) 
    9.87  
    9.88 -lemma fun_extend_apply2: "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b"
    9.89 -apply (rule consI1 [THEN apply_equality])
    9.90 -apply (rule fun_extend, assumption+)
    9.91 +lemma fun_extend_apply [simp]:
    9.92 +     "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)" 
    9.93 +apply (rule extend_apply) 
    9.94 +apply (simp add: Pi_def, blast) 
    9.95  done
    9.96  
    9.97  lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
    9.98 @@ -423,8 +412,7 @@
    9.99  apply (rule fun_extension) 
   9.100    apply assumption
   9.101   apply (blast intro: fun_extend) 
   9.102 -apply (erule consE)
   9.103 -apply (simp_all add: restrict fun_extend_apply1 fun_extend_apply2)
   9.104 +apply (erule consE, simp_all)
   9.105  done
   9.106  
   9.107  ML
   9.108 @@ -497,8 +485,7 @@
   9.109  val range_of_fun = thm "range_of_fun";
   9.110  val fun_extend = thm "fun_extend";
   9.111  val fun_extend3 = thm "fun_extend3";
   9.112 -val fun_extend_apply1 = thm "fun_extend_apply1";
   9.113 -val fun_extend_apply2 = thm "fun_extend_apply2";
   9.114 +val fun_extend_apply = thm "fun_extend_apply";
   9.115  val singleton_apply = thm "singleton_apply";
   9.116  val cons_fun_eq = thm "cons_fun_eq";
   9.117  *}