conversion of Perm to Isar. Strengthening of comp_fun_apply
--- a/src/ZF/Induct/Multiset.ML Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/Induct/Multiset.ML Fri May 24 13:15:37 2002 +0200
@@ -696,9 +696,7 @@
by (rtac fun_extension 1 THEN rtac lam_type 1);
by (ALLGOALS(Asm_full_simp_tac));
by (auto_tac (claset(), simpset()
- addsimps [multiset_fun_iff,
- fun_extend_apply1,
- fun_extend_apply2]));
+ addsimps [multiset_fun_iff, fun_extend_apply]));
by (dres_inst_tac [("c", "a"), ("b", "1")] fun_extend3 1);
by (stac Un_commute 3);
by (auto_tac (claset(), simpset() addsimps [cons_eq]));
--- a/src/ZF/IsaMakefile Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/IsaMakefile Fri May 24 13:15:37 2002 +0200
@@ -38,7 +38,7 @@
Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
- OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy \
+ OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \
QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
--- a/src/ZF/Order.thy Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/Order.thy Fri May 24 13:15:37 2002 +0200
@@ -436,8 +436,7 @@
apply (blast intro!: bij_converse_bij
intro: bij_is_fun apply_funtype)+
apply (erule notE)
-apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
- comp_fun_apply [of _ A B _ A])
+apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B])
done
--- a/src/ZF/Perm.ML Thu May 23 17:05:21 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,545 +0,0 @@
-(* Title: ZF/Perm.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-The theory underlying permutation groups
- -- Composition of relations, the identity relation
- -- Injections, surjections, bijections
- -- Lemmas for the Schroeder-Bernstein Theorem
-*)
-
-(** Surjective function space **)
-
-Goalw [surj_def] "f: surj(A,B) ==> f: A->B";
-by (etac CollectD1 1);
-qed "surj_is_fun";
-
-Goalw [surj_def] "f : Pi(A,B) ==> f: surj(A,range(f))";
-by (blast_tac (claset() addIs [apply_equality, range_of_fun, domain_type]) 1);
-qed "fun_is_surj";
-
-Goalw [surj_def] "f: surj(A,B) ==> range(f)=B";
-by (best_tac (claset() addIs [apply_Pair] addEs [range_type]) 1);
-qed "surj_range";
-
-(** A function with a right inverse is a surjection **)
-
-val prems = Goalw [surj_def]
- "[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \
-\ |] ==> f: surj(A,B)";
-by (blast_tac (claset() addIs prems) 1);
-qed "f_imp_surjective";
-
-val prems = Goal
- "[| !!x. x:A ==> c(x): B; \
-\ !!y. y:B ==> d(y): A; \
-\ !!y. y:B ==> c(d(y)) = y \
-\ |] ==> (lam x:A. c(x)) : surj(A,B)";
-by (res_inst_tac [("d", "d")] f_imp_surjective 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems) ));
-qed "lam_surjective";
-
-(*Cantor's theorem revisited*)
-Goalw [surj_def] "f ~: surj(A,Pow(A))";
-by Safe_tac;
-by (cut_facts_tac [cantor] 1);
-by (fast_tac subset_cs 1);
-qed "cantor_surj";
-
-
-(** Injective function space **)
-
-Goalw [inj_def] "f: inj(A,B) ==> f: A->B";
-by (etac CollectD1 1);
-qed "inj_is_fun";
-
-(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
-Goalw [inj_def]
- "[| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c";
-by (blast_tac (claset() addDs [Pair_mem_PiD]) 1);
-qed "inj_equality";
-
-Goalw [inj_def] "[| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b";
-by (Blast_tac 1);
-qed "inj_apply_equality";
-
-(** A function with a left inverse is an injection **)
-
-Goal "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
-by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
-by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
-bind_thm ("f_imp_injective", ballI RSN (2,result()));
-
-val prems = Goal
- "[| !!x. x:A ==> c(x): B; \
-\ !!x. x:A ==> d(c(x)) = x \
-\ |] ==> (lam x:A. c(x)) : inj(A,B)";
-by (res_inst_tac [("d", "d")] f_imp_injective 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems)));
-qed "lam_injective";
-
-(** Bijections **)
-
-Goalw [bij_def] "f: bij(A,B) ==> f: inj(A,B)";
-by (etac IntD1 1);
-qed "bij_is_inj";
-
-Goalw [bij_def] "f: bij(A,B) ==> f: surj(A,B)";
-by (etac IntD2 1);
-qed "bij_is_surj";
-
-(* f: bij(A,B) ==> f: A->B *)
-bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
-
-val prems = Goalw [bij_def]
- "[| !!x. x:A ==> c(x): B; \
-\ !!y. y:B ==> d(y): A; \
-\ !!x. x:A ==> d(c(x)) = x; \
-\ !!y. y:B ==> c(d(y)) = y \
-\ |] ==> (lam x:A. c(x)) : bij(A,B)";
-by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
-qed "lam_bijective";
-
-Goal "(ALL y : x. EX! y'. f(y') = f(y)) \
-\ ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)";
-by (res_inst_tac [("d","f")] lam_bijective 1);
-by (auto_tac (claset(),
- simpset() addsimps [the_equality2]));
-qed "RepFun_bijective";
-
-
-(** Identity function **)
-
-Goalw [id_def] "a:A ==> <a,a> : id(A)";
-by (etac lamI 1);
-qed "idI";
-
-val major::prems = Goalw [id_def]
- "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P \
-\ |] ==> P";
-by (rtac (major RS lamE) 1);
-by (REPEAT (ares_tac prems 1));
-qed "idE";
-
-Goalw [id_def] "id(A) : A->A";
-by (rtac lam_type 1);
-by (assume_tac 1);
-qed "id_type";
-
-Goalw [id_def] "x:A ==> id(A)`x = x";
-by (Asm_simp_tac 1);
-qed "id_conv";
-
-Addsimps [id_conv];
-
-Goalw [id_def] "A<=B ==> id(A) <= id(B)";
-by (etac lam_mono 1);
-qed "id_mono";
-
-Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
-by (REPEAT (ares_tac [CollectI,lam_type] 1));
-by (etac subsetD 1 THEN assume_tac 1);
-by (Simp_tac 1);
-qed "id_subset_inj";
-
-bind_thm ("id_inj", subset_refl RS id_subset_inj);
-
-Goalw [id_def,surj_def] "id(A): surj(A,A)";
-by (Asm_simp_tac 1);
-qed "id_surj";
-
-Goalw [bij_def] "id(A): bij(A,A)";
-by (blast_tac (claset() addIs [id_inj, id_surj]) 1);
-qed "id_bij";
-
-Goalw [id_def] "A <= B <-> id(A) : A->B";
-by (fast_tac (claset() addSIs [lam_type] addDs [apply_type]
- addss (simpset())) 1);
-qed "subset_iff_id";
-
-
-(*** Converse of a function ***)
-
-Goalw [inj_def] "f: inj(A,B) ==> converse(f) : range(f)->A";
-by (asm_simp_tac (simpset() addsimps [Pi_iff, function_def]) 1);
-by (etac CollectE 1);
-by (asm_simp_tac (simpset() addsimps [apply_iff]) 1);
-by (blast_tac (claset() addDs [fun_is_rel]) 1);
-qed "inj_converse_fun";
-
-(** Equations for converse(f) **)
-
-(*The premises are equivalent to saying that f is injective...*)
-Goal "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a";
-by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
-qed "left_inverse_lemma";
-
-Goal "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
-by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
- inj_is_fun]) 1);
-qed "left_inverse";
-
-bind_thm ("left_inverse_bij", bij_is_inj RS left_inverse);
-
-Goal "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
-by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
-by (REPEAT (assume_tac 1));
-qed "right_inverse_lemma";
-
-(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
- No: they would not imply that converse(f) was a function! *)
-Goal "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b";
-by (rtac right_inverse_lemma 1);
-by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
-qed "right_inverse";
-
-Addsimps [left_inverse, right_inverse];
-
-
-Goal "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b";
-by (force_tac (claset(), simpset() addsimps [bij_def, surj_range]) 1);
-qed "right_inverse_bij";
-
-(** Converses of injections, surjections, bijections **)
-
-Goal "f: inj(A,B) ==> converse(f): inj(range(f), A)";
-by (rtac f_imp_injective 1);
-by (etac inj_converse_fun 1);
-by (rtac right_inverse 1);
-by (REPEAT (assume_tac 1));
-qed "inj_converse_inj";
-
-Goal "f: inj(A,B) ==> converse(f): surj(range(f), A)";
-by (blast_tac (claset() addIs [f_imp_surjective, inj_converse_fun,
- left_inverse,
- inj_is_fun, range_of_fun RS apply_type]) 1);
-qed "inj_converse_surj";
-
-Goalw [bij_def] "f: bij(A,B) ==> converse(f): bij(B,A)";
-by (fast_tac (claset() addEs [surj_range RS subst, inj_converse_inj,
- inj_converse_surj]) 1);
-qed "bij_converse_bij";
-(*Adding this as an SI seems to cause looping*)
-
-AddTCs [bij_converse_bij];
-
-
-(** Composition of two relations **)
-
-(*The inductive definition package could derive these theorems for (r O s)*)
-
-Goalw [comp_def] "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
-by (Blast_tac 1);
-qed "compI";
-
-val prems = Goalw [comp_def]
- "[| xz : r O s; \
-\ !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac prems 1);
-by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
-qed "compE";
-
-bind_thm ("compEpair",
- rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
- THEN prune_params_tac)
- (inst "xz" "<a,c>" compE));
-
-AddSIs [idI];
-AddIs [compI];
-AddSEs [compE,idE];
-
-Goal "converse(R O S) = converse(S) O converse(R)";
-by (Blast_tac 1);
-qed "converse_comp";
-
-
-(** Domain and Range -- see Suppes, section 3.1 **)
-
-(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
-Goal "range(r O s) <= range(r)";
-by (Blast_tac 1);
-qed "range_comp";
-
-Goal "domain(r) <= range(s) ==> range(r O s) = range(r)";
-by (rtac (range_comp RS equalityI) 1);
-by (Blast_tac 1);
-qed "range_comp_eq";
-
-Goal "domain(r O s) <= domain(s)";
-by (Blast_tac 1);
-qed "domain_comp";
-
-Goal "range(s) <= domain(r) ==> domain(r O s) = domain(s)";
-by (rtac (domain_comp RS equalityI) 1);
-by (Blast_tac 1);
-qed "domain_comp_eq";
-
-Goal "(r O s)``A = r``(s``A)";
-by (Blast_tac 1);
-qed "image_comp";
-
-
-(** Other results **)
-
-Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (Blast_tac 1);
-qed "comp_mono";
-
-(*composition preserves relations*)
-Goal "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C";
-by (Blast_tac 1);
-qed "comp_rel";
-
-(*associative law for composition*)
-Goal "(r O s) O t = r O (s O t)";
-by (Blast_tac 1);
-qed "comp_assoc";
-
-(*left identity of composition; provable inclusions are
- id(A) O r <= r
- and [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
-Goal "r<=A*B ==> id(B) O r = r";
-by (Blast_tac 1);
-qed "left_comp_id";
-
-(*right identity of composition; provable inclusions are
- r O id(A) <= r
- and [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
-Goal "r<=A*B ==> r O id(A) = r";
-by (Blast_tac 1);
-qed "right_comp_id";
-
-
-(** Composition preserves functions, injections, and surjections **)
-
-Goalw [function_def]
- "[| function(g); function(f) |] ==> function(f O g)";
-by (Blast_tac 1);
-qed "comp_function";
-
-Goal "[| g: A->B; f: B->C |] ==> (f O g) : A->C";
-by (asm_full_simp_tac
- (simpset() addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
- setloop etac conjE) 1);
-by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
-by (Blast_tac 1);
-qed "comp_fun";
-
-Goal "[| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)";
-by (REPEAT (ares_tac [comp_fun,apply_equality,compI,
- apply_Pair,apply_type] 1));
-qed "comp_fun_apply";
-
-Addsimps [comp_fun_apply];
-
-(*Simplifies compositions of lambda-abstractions*)
-val [prem] = Goal
- "[| !!x. x:A ==> b(x): B \
-\ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
-by (rtac fun_extension 1);
-by (rtac comp_fun 1);
-by (rtac lam_funtype 2);
-by (typecheck_tac (tcset() addTCs [prem]));
-by (asm_simp_tac (simpset() addsimps [prem]
- setSolver (mk_solver ""
- (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
-qed "comp_lam";
-
-Goal "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)";
-by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
- f_imp_injective 1);
-by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
-by (asm_simp_tac (simpset()
- setSolver (mk_solver ""
- (type_solver_tac (tcset() addTCs [inj_is_fun])))) 1);
-qed "comp_inj";
-
-Goalw [surj_def]
- "[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)";
-by (blast_tac (claset() addSIs [comp_fun,comp_fun_apply]) 1);
-qed "comp_surj";
-
-Goalw [bij_def]
- "[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)";
-by (blast_tac (claset() addIs [comp_inj,comp_surj]) 1);
-qed "comp_bij";
-
-
-(** Dual properties of inj and surj -- useful for proofs from
- D Pastre. Automatic theorem proving in set theory.
- Artificial Intelligence, 10:1--27, 1978. **)
-
-Goalw [inj_def]
- "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
-by Safe_tac;
-by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (asm_simp_tac (simpset() ) 1);
-qed "comp_mem_injD1";
-
-Goalw [inj_def,surj_def]
- "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)";
-by Safe_tac;
-by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
-by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
-by (REPEAT (assume_tac 1));
-by Safe_tac;
-by (res_inst_tac [("t", "op `(g)")] subst_context 1);
-by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (asm_simp_tac (simpset() ) 1);
-qed "comp_mem_injD2";
-
-Goalw [surj_def]
- "[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)";
-by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
-qed "comp_mem_surjD1";
-
-Goal "[| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c";
-by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
-qed "comp_fun_applyD";
-
-Goalw [inj_def,surj_def]
- "[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)";
-by Safe_tac;
-by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
-by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
-by (blast_tac (claset() addSIs [apply_funtype]) 1);
-qed "comp_mem_surjD2";
-
-
-(** inverses of composition **)
-
-(*left inverse of composition; one inclusion is
- f: A->B ==> id(A) <= converse(f) O f *)
-Goalw [inj_def] "f: inj(A,B) ==> converse(f) O f = id(A)";
-by (fast_tac (claset() addIs [apply_Pair]
- addEs [domain_type]
- addss (simpset() addsimps [apply_iff])) 1);
-qed "left_comp_inverse";
-
-(*right inverse of composition; one inclusion is
- f: A->B ==> f O converse(f) <= id(B)
-*)
-val [prem] = goalw (the_context ()) [surj_def]
- "f: surj(A,B) ==> f O converse(f) = id(B)";
-val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
-by (cut_facts_tac [prem] 1);
-by (rtac equalityI 1);
-by (best_tac (claset() addEs [domain_type, range_type, make_elim appfD]) 1);
-by (blast_tac (claset() addIs [apply_Pair]) 1);
-qed "right_comp_inverse";
-
-(** Proving that a function is a bijection **)
-
-Goalw [id_def]
- "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
-by Safe_tac;
-by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
-by (Asm_full_simp_tac 1);
-by (rtac fun_extension 1);
-by (REPEAT (ares_tac [comp_fun, lam_type] 1));
-by Auto_tac;
-qed "comp_eq_id_iff";
-
-Goalw [bij_def]
- "[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f : bij(A,B)";
-by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff]) 1);
-by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1
- ORELSE eresolve_tac [bspec, apply_type] 1));
-qed "fg_imp_bijective";
-
-Goal "[| f: A->A; f O f = id(A) |] ==> f : bij(A,A)";
-by (REPEAT (ares_tac [fg_imp_bijective] 1));
-qed "nilpotent_imp_bijective";
-
-Goal "[| converse(f): B->A; f: A->B |] ==> f : bij(A,B)";
-by (asm_simp_tac (simpset() addsimps [fg_imp_bijective, comp_eq_id_iff,
- left_inverse_lemma, right_inverse_lemma]) 1);
-qed "invertible_imp_bijective";
-
-(** Unions of functions -- cf similar theorems on func.ML **)
-
-(*Theorem by KG, proof by LCP*)
-Goal "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] \
-\ ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)";
-by (res_inst_tac [("d","%z. if z:B then converse(f)`z else converse(g)`z")]
- lam_injective 1);
-by (auto_tac (claset(),
- simpset() addsimps [inj_is_fun RS apply_type]));
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
-qed "inj_disjoint_Un";
-
-Goalw [surj_def]
- "[| f: surj(A,B); g: surj(C,D); A Int C = 0 |] \
-\ ==> (f Un g) : surj(A Un C, B Un D)";
-by (blast_tac (claset() addIs [fun_disjoint_apply1, fun_disjoint_apply2,
- fun_disjoint_Un, trans]) 1);
-qed "surj_disjoint_Un";
-
-(*A simple, high-level proof; the version for injections follows from it,
- using f:inj(A,B) <-> f:bij(A,range(f)) *)
-Goal "[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] \
-\ ==> (f Un g) : bij(A Un C, B Un D)";
-by (rtac invertible_imp_bijective 1);
-by (stac converse_Un 1);
-by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
-qed "bij_disjoint_Un";
-
-
-(** Restrictions as surjections and bijections *)
-
-val prems = goalw (the_context ()) [surj_def]
- "f: Pi(A,B) ==> f: surj(A, f``A)";
-val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
-by (fast_tac (claset() addIs rls) 1);
-qed "surj_image";
-
-Goal "restrict(f,A) `` B = f `` (A Int B)";
-by (auto_tac (claset(), simpset() addsimps [restrict_def]));
-qed "restrict_image";
-Addsimps [restrict_image];
-
-Goalw [inj_def]
- "[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)";
-by (safe_tac (claset() addSEs [restrict_type2]));
-by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
- box_equals, restrict] 1));
-qed "restrict_inj";
-
-Goal "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)";
-by (rtac (simplify (simpset() addsimps [restrict_image])
- (restrict_type2 RS surj_image)) 1);
-by (REPEAT (assume_tac 1));
-qed "restrict_surj";
-
-Goalw [inj_def,bij_def]
- "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)";
-by (blast_tac (claset() addSIs [restrict, restrict_surj]
- addIs [box_equals, surj_is_fun]) 1);
-qed "restrict_bij";
-
-
-(*** Lemmas for Ramsey's Theorem ***)
-
-Goalw [inj_def] "[| f: inj(A,B); B<=D |] ==> f: inj(A,D)";
-by (blast_tac (claset() addIs [fun_weaken_type]) 1);
-qed "inj_weaken_type";
-
-Goal "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
-by (rtac (restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (rewtac inj_def);
-by (fast_tac (claset() addEs [range_type, mem_irrefl]
- addDs [apply_equality]) 1);
-qed "inj_succ_restrict";
-
-Goalw [inj_def]
- "[| f: inj(A,B); a~:A; b~:B |] \
-\ ==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
-by (force_tac (claset() addIs [apply_type],
- simpset() addsimps [fun_extend, fun_extend_apply2,
- fun_extend_apply1]) 1);
-qed "inj_extend";
-
--- a/src/ZF/Perm.thy Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/Perm.thy Fri May 24 13:15:37 2002 +0200
@@ -9,30 +9,662 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = mono + func +
-consts
- O :: [i,i]=>i (infixr 60)
-
-defs
- (*composition of relations and functions; NOT Suppes's relative product*)
- comp_def "r O s == {xz : domain(s)*range(r) .
- EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+theory Perm = mono + func:
constdefs
+
+ (*composition of relations and functions; NOT Suppes's relative product*)
+ comp :: "[i,i]=>i" (infixr "O" 60)
+ "r O s == {xz : domain(s)*range(r) .
+ EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+
(*the identity function for A*)
- id :: i=>i
- "id(A) == (lam x:A. x)"
+ id :: "i=>i"
+ "id(A) == (lam x:A. x)"
(*one-to-one functions from A to B*)
- inj :: [i,i]=>i
- "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
+ inj :: "[i,i]=>i"
+ "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
(*onto functions from A to B*)
- surj :: [i,i]=>i
- "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
+ surj :: "[i,i]=>i"
+ "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
(*one-to-one and onto functions*)
- bij :: [i,i]=>i
- "bij(A,B) == inj(A,B) Int surj(A,B)"
+ bij :: "[i,i]=>i"
+ "bij(A,B) == inj(A,B) Int surj(A,B)"
+
+
+(** Surjective function space **)
+
+lemma surj_is_fun: "f: surj(A,B) ==> f: A->B"
+apply (unfold surj_def)
+apply (erule CollectD1)
+done
+
+lemma fun_is_surj: "f : Pi(A,B) ==> f: surj(A,range(f))"
+apply (unfold surj_def)
+apply (blast intro: apply_equality range_of_fun domain_type)
+done
+
+lemma surj_range: "f: surj(A,B) ==> range(f)=B"
+apply (unfold surj_def)
+apply (best intro: apply_Pair elim: range_type)
+done
+
+(** A function with a right inverse is a surjection **)
+
+lemma f_imp_surjective:
+ "[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y |]
+ ==> f: surj(A,B)"
+apply (simp add: surj_def)
+apply (blast)
+done
+
+lemma lam_surjective:
+ "[| !!x. x:A ==> c(x): B;
+ !!y. y:B ==> d(y): A;
+ !!y. y:B ==> c(d(y)) = y
+ |] ==> (lam x:A. c(x)) : surj(A,B)"
+apply (rule_tac d = "d" in f_imp_surjective)
+apply (simp_all add: lam_type)
+done
+
+(*Cantor's theorem revisited*)
+lemma cantor_surj: "f ~: surj(A,Pow(A))"
+apply (unfold surj_def)
+apply safe
+apply (cut_tac cantor)
+apply (best del: subsetI)
+done
+
+
+(** Injective function space **)
+
+lemma inj_is_fun: "f: inj(A,B) ==> f: A->B"
+apply (unfold inj_def)
+apply (erule CollectD1)
+done
+
+(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
+lemma inj_equality:
+ "[| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c"
+apply (unfold inj_def)
+apply (blast dest: Pair_mem_PiD)
+done
+
+lemma inj_apply_equality: "[| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b"
+apply (unfold inj_def)
+apply blast
+done
+
+(** A function with a left inverse is an injection **)
+
+lemma f_imp_injective: "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"
+apply (simp (no_asm_simp) add: inj_def)
+apply (blast intro: subst_context [THEN box_equals])
+done
+
+lemma lam_injective:
+ "[| !!x. x:A ==> c(x): B;
+ !!x. x:A ==> d(c(x)) = x |]
+ ==> (lam x:A. c(x)) : inj(A,B)"
+apply (rule_tac d = "d" in f_imp_injective)
+apply (simp_all add: lam_type)
+done
+
+(** Bijections **)
+
+lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)"
+apply (unfold bij_def)
+apply (erule IntD1)
+done
+
+lemma bij_is_surj: "f: bij(A,B) ==> f: surj(A,B)"
+apply (unfold bij_def)
+apply (erule IntD2)
+done
+
+(* f: bij(A,B) ==> f: A->B *)
+lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard]
+
+lemma lam_bijective:
+ "[| !!x. x:A ==> c(x): B;
+ !!y. y:B ==> d(y): A;
+ !!x. x:A ==> d(c(x)) = x;
+ !!y. y:B ==> c(d(y)) = y
+ |] ==> (lam x:A. c(x)) : bij(A,B)"
+apply (unfold bij_def)
+apply (blast intro!: lam_injective lam_surjective);
+done
+
+lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))
+ ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
+apply (rule_tac d = "f" in lam_bijective)
+apply (auto simp add: the_equality2)
+done
+
+
+(** Identity function **)
+
+lemma idI [intro!]: "a:A ==> <a,a> : id(A)"
+apply (unfold id_def)
+apply (erule lamI)
+done
+
+lemma idE [elim!]: "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P |] ==> P"
+apply (simp add: id_def lam_def)
+apply (blast intro: elim:);
+done
+
+lemma id_type: "id(A) : A->A"
+apply (unfold id_def)
+apply (rule lam_type)
+apply assumption
+done
+
+lemma id_conv [simp]: "x:A ==> id(A)`x = x"
+apply (unfold id_def)
+apply (simp (no_asm_simp))
+done
+
+lemma id_mono: "A<=B ==> id(A) <= id(B)"
+apply (unfold id_def)
+apply (erule lam_mono)
+done
+
+lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
+apply (simp add: inj_def id_def)
+apply (blast intro: lam_type)
+done
+
+lemmas id_inj = subset_refl [THEN id_subset_inj, standard]
+
+lemma id_surj: "id(A): surj(A,A)"
+apply (unfold id_def surj_def)
+apply (simp (no_asm_simp))
+done
+
+lemma id_bij: "id(A): bij(A,A)"
+apply (unfold bij_def)
+apply (blast intro: id_inj id_surj)
+done
+
+lemma subset_iff_id: "A <= B <-> id(A) : A->B"
+apply (unfold id_def)
+apply (force intro!: lam_type dest: apply_type);
+done
+
+
+(*** Converse of a function ***)
+
+lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A"
+apply (unfold inj_def)
+apply (simp (no_asm_simp) add: Pi_iff function_def)
+apply (erule CollectE)
+apply (simp (no_asm_simp) add: apply_iff)
+apply (blast dest: fun_is_rel)
+done
+
+(** Equations for converse(f) **)
+
+(*The premises are equivalent to saying that f is injective...*)
+lemma left_inverse_lemma:
+ "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a"
+by (blast intro: apply_Pair apply_equality converseI)
+
+lemma left_inverse [simp]: "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"
+apply (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)
+done
+
+lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard]
+
+lemma right_inverse_lemma:
+ "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"
+apply (rule apply_Pair [THEN converseD [THEN apply_equality]])
+apply (auto );
+done
+
+(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
+ No: they would not imply that converse(f) was a function! *)
+lemma right_inverse [simp]:
+ "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"
+by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
+
+lemma right_inverse_bij: "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b"
+apply (force simp add: bij_def surj_range)
+done
+
+(** Converses of injections, surjections, bijections **)
+
+lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
+apply (rule f_imp_injective)
+apply (erule inj_converse_fun)
+apply (clarify );
+apply (rule right_inverse);
+ apply assumption
+apply (blast intro: elim:);
+done
+
+lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
+by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
+ range_of_fun [THEN apply_type])
+
+(*Adding this as an intro! rule seems to cause looping*)
+lemma bij_converse_bij [TC]: "f: bij(A,B) ==> converse(f): bij(B,A)"
+apply (unfold bij_def)
+apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
+done
+
+
+
+(** Composition of two relations **)
+
+(*The inductive definition package could derive these theorems for (r O s)*)
+
+lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
+apply (unfold comp_def)
+apply blast
+done
+
+lemma compE [elim!]:
+ "[| xz : r O s;
+ !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |]
+ ==> P"
+apply (unfold comp_def)
+apply blast
+done
+
+lemma compEpair:
+ "[| <a,c> : r O s;
+ !!y. [| <a,y>:s; <y,c>:r |] ==> P |]
+ ==> P"
+apply (erule compE)
+apply (simp add: );
+done
+
+lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
+apply blast
+done
+
+
+(** Domain and Range -- see Suppes, section 3.1 **)
+
+(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
+lemma range_comp: "range(r O s) <= range(r)"
+apply blast
+done
+
+lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)"
+apply (rule range_comp [THEN equalityI])
+apply blast
+done
+
+lemma domain_comp: "domain(r O s) <= domain(s)"
+apply blast
+done
+
+lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)"
+apply (rule domain_comp [THEN equalityI])
+apply blast
+done
+
+lemma image_comp: "(r O s)``A = r``(s``A)"
+apply blast
+done
+
+
+(** Other results **)
+
+lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
+apply blast
+done
+
+(*composition preserves relations*)
+lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C"
+apply blast
+done
+
+(*associative law for composition*)
+lemma comp_assoc: "(r O s) O t = r O (s O t)"
+apply blast
+done
+
+(*left identity of composition; provable inclusions are
+ id(A) O r <= r
+ and [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
+lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
+apply blast
+done
+
+(*right identity of composition; provable inclusions are
+ r O id(A) <= r
+ and [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
+lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
+apply blast
+done
+
+
+(** Composition preserves functions, injections, and surjections **)
+
+lemma comp_function:
+ "[| function(g); function(f) |] ==> function(f O g)"
+apply (unfold function_def)
+apply blast
+done
+
+(*Don't think the premises can be weakened much*)
+lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) : A->C"
+apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
+apply (subst range_rel_subset [THEN domain_comp_eq]);
+apply (auto );
+done
+
+(*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
+lemma comp_fun_apply [simp]:
+ "[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)"
+apply (frule apply_Pair, assumption)
+apply (simp add: apply_def image_comp)
+apply (blast dest: apply_equality)
+done
+
+(*Simplifies compositions of lambda-abstractions*)
+lemma comp_lam:
+ "[| !!x. x:A ==> b(x): B |]
+ ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"
+apply (subgoal_tac "(lam x:A. b(x)) : A -> B")
+ apply (rule fun_extension)
+ apply (blast intro: comp_fun lam_funtype)
+ apply (rule lam_funtype)
+ apply (simp add: );
+apply (simp add: lam_type);
+done
+
+lemma comp_inj:
+ "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)"
+apply (frule inj_is_fun [of g])
+apply (frule inj_is_fun [of f])
+apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
+ apply (blast intro: comp_fun);
+apply (simp add: );
+done
+
+lemma comp_surj:
+ "[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"
+apply (unfold surj_def)
+apply (blast intro!: comp_fun comp_fun_apply)
+done
+
+lemma comp_bij:
+ "[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)"
+apply (unfold bij_def)
+apply (blast intro: comp_inj comp_surj)
+done
+
+
+(** Dual properties of inj and surj -- useful for proofs from
+ D Pastre. Automatic theorem proving in set theory.
+ Artificial Intelligence, 10:1--27, 1978. **)
+
+lemma comp_mem_injD1:
+ "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"
+apply (unfold inj_def)
+apply (force );
+done
+
+lemma comp_mem_injD2:
+ "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"
+apply (unfold inj_def surj_def)
+apply safe
+apply (rule_tac x1 = "x" in bspec [THEN bexE])
+apply (erule_tac [3] x1 = "w" in bspec [THEN bexE])
+apply assumption+
+apply safe
+apply (rule_tac t = "op ` (g) " in subst_context)
+apply (erule asm_rl bspec [THEN bspec, THEN mp])+
+apply (simp (no_asm_simp))
+done
+
+lemma comp_mem_surjD1:
+ "[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"
+apply (unfold surj_def)
+apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
+done
+
+
+lemma comp_mem_surjD2:
+ "[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"
+apply (unfold inj_def surj_def)
+apply safe
+apply (drule_tac x = "f`y" in bspec);
+apply (auto );
+apply (blast intro: apply_funtype)
+done
+
+(** inverses of composition **)
+
+(*left inverse of composition; one inclusion is
+ f: A->B ==> id(A) <= converse(f) O f *)
+lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
+apply (unfold inj_def)
+apply (clarify );
+apply (rule equalityI)
+ apply (auto simp add: apply_iff)
+apply (blast intro: elim:);
+done
+
+(*right inverse of composition; one inclusion is
+ f: A->B ==> f O converse(f) <= id(B)
+*)
+lemma right_comp_inverse:
+ "f: surj(A,B) ==> f O converse(f) = id(B)"
+apply (simp add: surj_def)
+apply (clarify );
+apply (rule equalityI)
+apply (best elim: domain_type range_type dest: apply_equality2)
+apply (blast intro: apply_Pair)
+done
+
+
+(** Proving that a function is a bijection **)
+
+lemma comp_eq_id_iff:
+ "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"
+apply (unfold id_def)
+apply safe
+ apply (drule_tac t = "%h. h`y " in subst_context)
+ apply simp
+apply (rule fun_extension)
+ apply (blast intro: comp_fun lam_type)
+ apply auto
+done
+
+lemma fg_imp_bijective:
+ "[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f : bij(A,B)"
+apply (unfold bij_def)
+apply (simp add: comp_eq_id_iff)
+apply (blast intro: f_imp_injective f_imp_surjective apply_funtype);
+done
+
+lemma nilpotent_imp_bijective: "[| f: A->A; f O f = id(A) |] ==> f : bij(A,A)"
+apply (blast intro: fg_imp_bijective)
+done
+
+lemma invertible_imp_bijective: "[| converse(f): B->A; f: A->B |] ==> f : bij(A,B)"
+apply (simp (no_asm_simp) add: fg_imp_bijective comp_eq_id_iff left_inverse_lemma right_inverse_lemma)
+done
+
+(** Unions of functions -- cf similar theorems on func.ML **)
+
+(*Theorem by KG, proof by LCP*)
+lemma inj_disjoint_Un:
+ "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |]
+ ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)"
+apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" in lam_injective)
+apply (auto simp add: inj_is_fun [THEN apply_type])
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+lemma surj_disjoint_Un:
+ "[| f: surj(A,B); g: surj(C,D); A Int C = 0 |]
+ ==> (f Un g) : surj(A Un C, B Un D)"
+apply (unfold surj_def)
+apply (blast intro: fun_disjoint_apply1 fun_disjoint_apply2 fun_disjoint_Un trans)
+done
+
+(*A simple, high-level proof; the version for injections follows from it,
+ using f:inj(A,B) <-> f:bij(A,range(f)) *)
+lemma bij_disjoint_Un:
+ "[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |]
+ ==> (f Un g) : bij(A Un C, B Un D)"
+apply (rule invertible_imp_bijective)
+apply (subst converse_Un)
+apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
+done
+
+
+(** Restrictions as surjections and bijections *)
+
+lemma surj_image:
+ "f: Pi(A,B) ==> f: surj(A, f``A)"
+apply (simp add: surj_def);
+apply (blast intro: apply_equality apply_Pair Pi_type);
+done
+
+lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)"
+apply (auto simp add: restrict_def)
+done
+
+lemma restrict_inj:
+ "[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"
+apply (unfold inj_def)
+apply (safe elim!: restrict_type2);
+apply (auto );
+done
+
+lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"
+apply (insert restrict_type2 [THEN surj_image])
+apply (simp add: restrict_image);
+done
+
+lemma restrict_bij:
+ "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"
+apply (unfold inj_def bij_def)
+apply (blast intro!: restrict restrict_surj intro: box_equals surj_is_fun)
+done
+
+
+(*** Lemmas for Ramsey's Theorem ***)
+
+lemma inj_weaken_type: "[| f: inj(A,B); B<=D |] ==> f: inj(A,D)"
+apply (unfold inj_def)
+apply (blast intro: fun_weaken_type)
+done
+
+lemma inj_succ_restrict:
+ "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
+apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type])
+apply assumption
+apply blast
+apply (unfold inj_def)
+apply (fast elim: range_type mem_irrefl dest: apply_equality)
+done
+
+
+lemma inj_extend:
+ "[| f: inj(A,B); a~:A; b~:B |]
+ ==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))"
+apply (unfold inj_def)
+apply (force intro: apply_type simp add: fun_extend)
+done
+
+
+ML
+{*
+val comp_def = thm "comp_def";
+val id_def = thm "id_def";
+val inj_def = thm "inj_def";
+val surj_def = thm "surj_def";
+val bij_def = thm "bij_def";
+
+val surj_is_fun = thm "surj_is_fun";
+val fun_is_surj = thm "fun_is_surj";
+val surj_range = thm "surj_range";
+val f_imp_surjective = thm "f_imp_surjective";
+val lam_surjective = thm "lam_surjective";
+val cantor_surj = thm "cantor_surj";
+val inj_is_fun = thm "inj_is_fun";
+val inj_equality = thm "inj_equality";
+val inj_apply_equality = thm "inj_apply_equality";
+val f_imp_injective = thm "f_imp_injective";
+val lam_injective = thm "lam_injective";
+val bij_is_inj = thm "bij_is_inj";
+val bij_is_surj = thm "bij_is_surj";
+val bij_is_fun = thm "bij_is_fun";
+val lam_bijective = thm "lam_bijective";
+val RepFun_bijective = thm "RepFun_bijective";
+val idI = thm "idI";
+val idE = thm "idE";
+val id_type = thm "id_type";
+val id_conv = thm "id_conv";
+val id_mono = thm "id_mono";
+val id_subset_inj = thm "id_subset_inj";
+val id_inj = thm "id_inj";
+val id_surj = thm "id_surj";
+val id_bij = thm "id_bij";
+val subset_iff_id = thm "subset_iff_id";
+val inj_converse_fun = thm "inj_converse_fun";
+val left_inverse_lemma = thm "left_inverse_lemma";
+val left_inverse = thm "left_inverse";
+val left_inverse_bij = thm "left_inverse_bij";
+val right_inverse_lemma = thm "right_inverse_lemma";
+val right_inverse = thm "right_inverse";
+val right_inverse_bij = thm "right_inverse_bij";
+val inj_converse_inj = thm "inj_converse_inj";
+val inj_converse_surj = thm "inj_converse_surj";
+val bij_converse_bij = thm "bij_converse_bij";
+val compI = thm "compI";
+val compE = thm "compE";
+val compEpair = thm "compEpair";
+val converse_comp = thm "converse_comp";
+val range_comp = thm "range_comp";
+val range_comp_eq = thm "range_comp_eq";
+val domain_comp = thm "domain_comp";
+val domain_comp_eq = thm "domain_comp_eq";
+val image_comp = thm "image_comp";
+val comp_mono = thm "comp_mono";
+val comp_rel = thm "comp_rel";
+val comp_assoc = thm "comp_assoc";
+val left_comp_id = thm "left_comp_id";
+val right_comp_id = thm "right_comp_id";
+val comp_function = thm "comp_function";
+val comp_fun = thm "comp_fun";
+val comp_fun_apply = thm "comp_fun_apply";
+val comp_lam = thm "comp_lam";
+val comp_inj = thm "comp_inj";
+val comp_surj = thm "comp_surj";
+val comp_bij = thm "comp_bij";
+val comp_mem_injD1 = thm "comp_mem_injD1";
+val comp_mem_injD2 = thm "comp_mem_injD2";
+val comp_mem_surjD1 = thm "comp_mem_surjD1";
+val comp_mem_surjD2 = thm "comp_mem_surjD2";
+val left_comp_inverse = thm "left_comp_inverse";
+val right_comp_inverse = thm "right_comp_inverse";
+val comp_eq_id_iff = thm "comp_eq_id_iff";
+val fg_imp_bijective = thm "fg_imp_bijective";
+val nilpotent_imp_bijective = thm "nilpotent_imp_bijective";
+val invertible_imp_bijective = thm "invertible_imp_bijective";
+val inj_disjoint_Un = thm "inj_disjoint_Un";
+val surj_disjoint_Un = thm "surj_disjoint_Un";
+val bij_disjoint_Un = thm "bij_disjoint_Un";
+val surj_image = thm "surj_image";
+val restrict_image = thm "restrict_image";
+val restrict_inj = thm "restrict_inj";
+val restrict_surj = thm "restrict_surj";
+val restrict_bij = thm "restrict_bij";
+val inj_weaken_type = thm "inj_weaken_type";
+val inj_succ_restrict = thm "inj_succ_restrict";
+val inj_extend = thm "inj_extend";
+*}
end
--- a/src/ZF/UNITY/Constrains.ML Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/UNITY/Constrains.ML Fri May 24 13:15:37 2002 +0200
@@ -470,6 +470,7 @@
by (cut_inst_tac [("F", "xa")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
by Auto_tac;
+by (rename_tac "xa xc xd act xe xf" 1);
by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
by (dres_inst_tac [("x", "f`xf")] bspec 1);
by Auto_tac;
--- a/src/ZF/UNITY/UNITY.ML Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/UNITY/UNITY.ML Fri May 24 13:15:37 2002 +0200
@@ -722,6 +722,7 @@
by (cut_inst_tac [("F", "xa")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
by Auto_tac;
+by (rename_tac "xa xc xd act xe xf" 1);
by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1);
by (dres_inst_tac [("x", "f`xf")] bspec 1);
by Auto_tac;
--- a/src/ZF/ex/Limit.thy Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/ex/Limit.thy Fri May 24 13:15:37 2002 +0200
@@ -772,21 +772,20 @@
"cpo(D) ==> id(set(D)) \<in> cont(D,D)"
by (simp add: id_type contI cpo_lub [THEN islub_in] chain_fun [THEN eta])
-
-lemmas comp_cont_apply = cont_fun [THEN comp_fun_apply, OF _ cont_fun];
+lemmas comp_cont_apply = cont_fun [THEN comp_fun_apply]
lemma comp_pres_cont [TC]:
"[| f \<in> cont(D',E); g \<in> cont(D,D'); cpo(D)|] ==> f O g \<in> cont(D,E)"
apply (rule contI)
apply (rule_tac [2] comp_cont_apply [THEN ssubst])
-apply (rule_tac [5] comp_cont_apply [THEN ssubst])
-apply (rule_tac [8] cont_mono)
-apply (rule_tac [9] cont_mono) (* 15 subgoals *)
+apply (rule_tac [4] comp_cont_apply [THEN ssubst])
+apply (rule_tac [6] cont_mono)
+apply (rule_tac [7] cont_mono) (* 13 subgoals *)
apply typecheck (* proves all but the lub case *)
apply (subst comp_cont_apply)
-apply (rule_tac [4] cont_lub [THEN ssubst])
-apply (rule_tac [6] cont_lub [THEN ssubst])
-prefer 8 apply (simp add: comp_cont_apply chain_in)
+apply (rule_tac [3] cont_lub [THEN ssubst])
+apply (rule_tac [5] cont_lub [THEN ssubst])
+prefer 7 apply (simp add: comp_cont_apply chain_in)
apply (auto intro: cpo_lub [THEN islub_in] cont_chain)
done
@@ -797,8 +796,8 @@
==> rel(cf(D,E),f O g,f' O g')"
apply (rule rel_cfI)
apply (subst comp_cont_apply)
-apply (rule_tac [4] comp_cont_apply [THEN ssubst])
-apply (rule_tac [7] cpo_trans)
+apply (rule_tac [3] comp_cont_apply [THEN ssubst])
+apply (rule_tac [5] cpo_trans)
apply (assumption | rule rel_cf cont_mono cont_map comp_pres_cont)+
done
@@ -810,10 +809,10 @@
apply simp
apply (rule rel_cfI)
apply (rule comp_cont_apply [THEN ssubst])
-apply (rule_tac [4] comp_cont_apply [THEN ssubst])
-apply (rule_tac [7] cpo_trans)
-apply (rule_tac [8] rel_cf)
-apply (rule_tac [10] cont_mono)
+apply (rule_tac [3] comp_cont_apply [THEN ssubst])
+apply (rule_tac [5] cpo_trans)
+apply (rule_tac [6] rel_cf)
+apply (rule_tac [8] cont_mono)
apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont]
cont_map chain_rel rel_cf)+
done
@@ -826,8 +825,7 @@
apply (assumption |
rule comp_fun cf_cont [THEN cont_fun] cpo_lub [THEN islub_in]
cpo_cf chain_cf_comp)+
-apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply,
- OF _ _ chain_in [THEN cf_cont]])
+apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply])
apply (subst comp_cont_apply)
apply (assumption | rule cpo_lub [THEN islub_in, THEN cf_cont] cpo_cf)+
apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub]
@@ -1790,15 +1788,15 @@
apply (assumption | rule e_less_cont [THEN cont_fun] apply_type Dinf_prod)+
apply (rule_tac x1 = x and n1 = xa in Dinf_eq [THEN subst])
apply (rule_tac [3] comp_fun_apply [THEN subst])
-apply (rename_tac [6] y)
-apply (rule_tac [6] P =
+apply (rename_tac [5] y)
+apply (rule_tac [5] P =
"%z. rel(DD`succ(y),
(ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
z)"
in id_conv [THEN subst])
-apply (rule_tac [7] rel_cf)
+apply (rule_tac [6] rel_cf)
(* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
-(* solves 11 of 12 subgoals *)
+(* solves 10 of 11 subgoals *)
apply (assumption |
rule Dinf_prod [THEN apply_type] cont_fun Rp_cont e_less_cont
emb_cont emb_chain_emb emb_chain_cpo apply_type embRp_rel
@@ -1825,7 +1823,7 @@
apply (drule mp, assumption)
apply (subst e_gr_le)
apply (rule_tac [4] comp_fun_apply [THEN ssubst])
-apply (rule_tac [7] Dinf_eq [THEN ssubst])
+apply (rule_tac [6] Dinf_eq [THEN ssubst])
apply (assumption |
rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont
apply_type Dinf_prod nat_succI)+
@@ -1871,8 +1869,8 @@
apply (rule fun_extension)
apply (rule_tac [3] id_conv [THEN ssubst])
apply (rule_tac [4] comp_fun_apply [THEN ssubst])
-apply (rule_tac [7] beta [THEN ssubst])
-apply (rule_tac [8] rho_emb_id [THEN ssubst])
+apply (rule_tac [6] beta [THEN ssubst])
+apply (rule_tac [7] rho_emb_id [THEN ssubst])
apply (assumption |
rule comp_fun id_type lam_type rho_emb_fun Dinf_prod [THEN apply_type]
apply_type refl)+
@@ -1880,10 +1878,10 @@
apply (rule rel_cfI) (* ------------------>>>Yields type cond, not in HOL *)
apply (subst id_conv)
apply (rule_tac [2] comp_fun_apply [THEN ssubst])
-apply (rule_tac [5] beta [THEN ssubst])
-apply (rule_tac [6] rho_emb_apply1 [THEN ssubst])
-apply (rule_tac [7] rel_DinfI)
-apply (rule_tac [7] beta [THEN ssubst])
+apply (rule_tac [4] beta [THEN ssubst])
+apply (rule_tac [5] rho_emb_apply1 [THEN ssubst])
+apply (rule_tac [6] rel_DinfI)
+apply (rule_tac [6] beta [THEN ssubst])
(* Dinf_prod bad with lam_type *)
apply (assumption |
rule eps1 lam_type rho_emb_fun eps_fun
@@ -1928,11 +1926,11 @@
apply (assumption | rule emb_rho_emb)+
apply (rule fun_extension) (* Manual instantiation in HOL. *)
apply (rule_tac [3] comp_fun_apply [THEN ssubst])
-apply (rule_tac [6] fun_extension) (*Next, clean up and instantiate unknowns *)
+apply (rule_tac [5] fun_extension) (*Next, clean up and instantiate unknowns *)
apply (assumption | rule comp_fun rho_emb_fun eps_fun Dinf_prod apply_type)+
apply (simp add: rho_emb_apply2 eps_fun [THEN apply_type])
apply (rule comp_fun_apply [THEN subst])
-apply (rule_tac [4] eps_split_left [THEN subst])
+apply (rule_tac [3] eps_split_left [THEN subst])
apply (auto intro: eps_fun)
done
--- a/src/ZF/func.thy Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/func.thy Fri May 24 13:15:37 2002 +0200
@@ -57,9 +57,7 @@
(*Applying a function outside its domain yields 0*)
lemma apply_0: "a ~: domain(f) ==> f`a = 0"
-apply (unfold apply_def)
-apply (blast intro: elim:);
-done
+by (unfold apply_def, blast)
lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"
apply (frule fun_is_rel)
@@ -67,12 +65,9 @@
done
lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> <a,f`a>: f"
-apply (simp add: function_def)
-apply (clarify );
-apply (subgoal_tac "f`a = y")
-apply (blast intro: elim:);
-apply (simp add: apply_def);
-apply (blast intro: elim:);
+apply (simp add: function_def, clarify)
+apply (subgoal_tac "f`a = y", blast)
+apply (simp add: apply_def, blast)
done
lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"
@@ -141,7 +136,7 @@
by (simp add: lam_def Pi_def function_def, blast)
lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}"
-by (blast intro: lam_type);
+by (blast intro: lam_type)
lemma function_lam: "function (lam x:A. b(x))"
by (simp add: function_def lam_def)
@@ -150,14 +145,10 @@
by (simp add: relation_def lam_def)
lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)"
-apply (simp add: apply_def lam_def)
-apply (blast intro: elim:);
-done
+by (simp add: apply_def lam_def, blast)
lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
-apply (simp add: apply_def lam_def)
-apply (blast intro: elim:);
-done
+by (simp add: apply_def lam_def, blast)
lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
by (simp add: lam_def)
@@ -173,7 +164,7 @@
lemma lam_theI:
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI)
-apply (simp add: );
+apply simp
apply (blast intro: theI)
done
@@ -273,9 +264,7 @@
by (simp add: Pi_iff function_def restrict_def, blast)
lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
-apply (simp add: apply_def restrict_def)
-apply (blast intro: elim:);
-done
+by (simp add: apply_def restrict_def, blast)
lemma restrict_empty [simp]: "restrict(f,0) = 0"
apply (unfold restrict_def)
@@ -395,14 +384,14 @@
"[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"
by (blast intro: fun_extend [THEN fun_weaken_type])
-lemma fun_extend_apply1: "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"
-apply (rule apply_Pair [THEN consI2, THEN apply_equality])
-apply (rule_tac [3] fun_extend, assumption+)
-done
+lemma extend_apply:
+ "c ~: domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
+by (auto simp add: apply_def)
-lemma fun_extend_apply2: "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"
-apply (rule consI1 [THEN apply_equality])
-apply (rule fun_extend, assumption+)
+lemma fun_extend_apply [simp]:
+ "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
+apply (rule extend_apply)
+apply (simp add: Pi_def, blast)
done
lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
@@ -423,8 +412,7 @@
apply (rule fun_extension)
apply assumption
apply (blast intro: fun_extend)
-apply (erule consE)
-apply (simp_all add: restrict fun_extend_apply1 fun_extend_apply2)
+apply (erule consE, simp_all)
done
ML
@@ -497,8 +485,7 @@
val range_of_fun = thm "range_of_fun";
val fun_extend = thm "fun_extend";
val fun_extend3 = thm "fun_extend3";
-val fun_extend_apply1 = thm "fun_extend_apply1";
-val fun_extend_apply2 = thm "fun_extend_apply2";
+val fun_extend_apply = thm "fun_extend_apply";
val singleton_apply = thm "singleton_apply";
val cons_fun_eq = thm "cons_fun_eq";
*}