# HG changeset patch # User paulson # Date 1292414329 0 # Node ID be34449f6cba8701f4f89451d654fdbef5622480 # Parent df8c7dc30214daded172e409934a8e89b0639bd5 Added two theorems about the concept of range. Tidied up the comments. diff -r df8c7dc30214 -r be34449f6cba src/ZF/Perm.thy --- a/src/ZF/Perm.thy Wed Dec 01 15:38:05 2010 +0100 +++ b/src/ZF/Perm.thy Wed Dec 15 11:58:49 2010 +0000 @@ -39,9 +39,7 @@ "bij(A,B) == inj(A,B) Int surj(A,B)" -subsection{*Surjections*} - -(** Surjective function space **) +subsection{*Surjective Function Space*} lemma surj_is_fun: "f: surj(A,B) ==> f: A->B" apply (unfold surj_def) @@ -58,13 +56,12 @@ apply (best intro: apply_Pair elim: range_type) done -(** A function with a right inverse is a surjection **) +text{* 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, blast) -done + by (simp add: surj_def, blast) lemma lam_surjective: "[| !!x. x:A ==> c(x): B; @@ -75,7 +72,7 @@ apply (simp_all add: lam_type) done -(*Cantor's theorem revisited*) +text{*Cantor's theorem revisited*} lemma cantor_surj: "f ~: surj(A,Pow(A))" apply (unfold surj_def, safe) apply (cut_tac cantor) @@ -83,16 +80,14 @@ done -subsection{*Injections*} - -(** Injective function space **) +subsection{*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]*) +text{*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) @@ -102,8 +97,7 @@ lemma inj_apply_equality: "[| f:inj(A,B); f`a=f`b; a:A; b:A |] ==> a=b" by (unfold inj_def, blast) - -(** A function with a left inverse is an injection **) +text{* 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) @@ -130,7 +124,7 @@ apply (erule IntD2) done -(* f: bij(A,B) ==> f: A->B *) +text{* f: bij(A,B) ==> f: A->B *} lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard] lemma lam_bijective: @@ -202,7 +196,6 @@ by auto - subsection{*Converse of a Function*} lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A" @@ -213,7 +206,7 @@ apply (blast dest: fun_is_rel) done -(** Equations for converse(f) **) +text{* Equations for converse(f) *} text{*The premises are equivalent to saying that f is injective...*} lemma left_inverse_lemma: @@ -256,7 +249,7 @@ 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*) +text{*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) @@ -266,7 +259,7 @@ subsection{*Composition of Two Relations*} -(*The inductive definition package could derive these theorems for (r O s)*) +text{*The inductive definition package could derive these theorems for @term{r O s}*} lemma compI [intro]: "[| :s; :r |] ==> : r O s" by (unfold comp_def, blast) @@ -289,7 +282,7 @@ subsection{*Domain and Range -- see Suppes, Section 3.1*} -(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) +text{*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*} lemma range_comp: "range(r O s) <= range(r)" by blast @@ -305,17 +298,23 @@ lemma image_comp: "(r O s)``A = r``(s``A)" by blast +lemma inj_inj_range: "f: inj(A,B) ==> f : inj(A,range(f))" + by (auto simp add: inj_def Pi_iff function_def) + +lemma inj_bij_range: "f: inj(A,B) ==> f : bij(A,range(f))" + by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) + subsection{*Other Results*} lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" by blast -(*composition preserves relations*) +text{*composition preserves relations*} lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C" by blast -(*associative law for composition*) +text{*associative law for composition*} lemma comp_assoc: "(r O s) O t = r O (s O t)" by blast @@ -337,7 +336,7 @@ lemma comp_function: "[| function(g); function(f) |] ==> function(f O g)" by (unfold function_def, blast) -(*Don't think the premises can be weakened much*) +text{*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], auto) @@ -351,7 +350,7 @@ apply (blast dest: apply_equality) done -(*Simplifies compositions of lambda-abstractions*) +text{*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)))" @@ -420,16 +419,16 @@ subsubsection{*Inverses of Composition*} -(*left inverse of composition; one inclusion is - f: A->B ==> id(A) <= converse(f) O f *) +text{*left inverse of composition; one inclusion is + @term{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, clarify) apply (rule equalityI) apply (auto simp add: apply_iff, blast) done -(*right inverse of composition; one inclusion is - f: A->B ==> f O converse(f) <= id(B) *) +text{*right inverse of composition; one inclusion is + @term{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, clarify) @@ -470,7 +469,7 @@ text{*See similar theorems in func.thy*} -(*Theorem by KG, proof by LCP*) +text{*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)" @@ -487,8 +486,8 @@ intro!: fun_disjoint_apply1 fun_disjoint_apply2) done -(*A simple, high-level proof; the version for injections follows from it, - using f:inj(A,B) <-> f:bij(A,range(f)) *) +text{*A simple, high-level proof; the version for injections follows from it, + using @term{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)"