# HG changeset patch # User paulson # Date 1022238937 -7200 # Node ID 312bd350579bf7958a7615f5be7f33ce40d4f75c # Parent 81082cfa561872c6b5770a0458f8aae0053e1e53 conversion of Perm to Isar. Strengthening of comp_fun_apply diff -r 81082cfa5618 -r 312bd350579b src/ZF/Induct/Multiset.ML --- 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])); diff -r 81082cfa5618 -r 312bd350579b src/ZF/IsaMakefile --- 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 \ diff -r 81082cfa5618 -r 312bd350579b src/ZF/Order.thy --- 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 diff -r 81082cfa5618 -r 312bd350579b src/ZF/Perm.ML --- 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] - "[| :f; :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 ==> : id(A)"; -by (etac lamI 1); -qed "idI"; - -val major::prems = Goalw [id_def] - "[| p: id(A); !!x.[| x:A; p= |] ==> 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] "[| :s; :r |] ==> : r O s"; -by (Blast_tac 1); -qed "compI"; - -val prems = Goalw [comp_def] - "[| xz : r O s; \ -\ !!x y z. [| xz=; :s; :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" "" 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(,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"; - diff -r 81082cfa5618 -r 312bd350579b src/ZF/Perm.thy --- 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= & :s & :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= & :s & :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: + "[| :f; :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 ==> : id(A)" +apply (unfold id_def) +apply (erule lamI) +done + +lemma idE [elim!]: "[| p: id(A); !!x.[| x:A; p= |] ==> 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]: "[| :s; :r |] ==> : r O s" +apply (unfold comp_def) +apply blast +done + +lemma compE [elim!]: + "[| xz : r O s; + !!x y z. [| xz=; :s; :r |] ==> P |] + ==> P" +apply (unfold comp_def) +apply blast +done + +lemma compEpair: + "[| : r O s; + !!y. [| :s; :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(,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 diff -r 81082cfa5618 -r 312bd350579b src/ZF/UNITY/Constrains.ML --- 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; diff -r 81082cfa5618 -r 312bd350579b src/ZF/UNITY/UNITY.ML --- 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; diff -r 81082cfa5618 -r 312bd350579b src/ZF/ex/Limit.thy --- 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)) \ 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 \ cont(D',E); g \ cont(D,D'); cpo(D)|] ==> f O g \ 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 diff -r 81082cfa5618 -r 312bd350579b src/ZF/func.thy --- 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 = " apply (frule fun_is_rel) @@ -67,12 +65,9 @@ done lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> : 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 |] ==> : 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(,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(,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(,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(,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(,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"; *}