src/ZF/Perm.thy
 author wenzelm Fri Sep 16 21:28:09 2016 +0200 (2016-09-16) changeset 63901 4ce989e962e0 parent 60770 240563fbf41d child 67399 eab6ce8368fa permissions -rw-r--r--
more symbols;
 wenzelm@32960 ` 1` ```(* Title: ZF/Perm.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 3` ``` Copyright 1991 University of Cambridge ``` clasohm@0 ` 4` clasohm@0 ` 5` ```The theory underlying permutation groups ``` clasohm@0 ` 6` ``` -- Composition of relations, the identity relation ``` clasohm@0 ` 7` ``` -- Injections, surjections, bijections ``` clasohm@0 ` 8` ``` -- Lemmas for the Schroeder-Bernstein Theorem ``` clasohm@0 ` 9` ```*) ``` clasohm@0 ` 10` wenzelm@60770 ` 11` ```section\Injections, Surjections, Bijections, Composition\ ``` paulson@13356 ` 12` haftmann@16417 ` 13` ```theory Perm imports func begin ``` clasohm@0 ` 14` wenzelm@24893 ` 15` ```definition ``` paulson@13176 ` 16` ``` (*composition of relations and functions; NOT Suppes's relative product*) ``` wenzelm@24893 ` 17` ``` comp :: "[i,i]=>i" (infixr "O" 60) where ``` paulson@46821 ` 18` ``` "r O s == {xz \ domain(s)*range(r) . ``` paulson@46820 ` 19` ``` \x y z. xz= & :s & :r}" ``` paulson@13176 ` 20` wenzelm@24893 ` 21` ```definition ``` paulson@1806 ` 22` ``` (*the identity function for A*) ``` wenzelm@24893 ` 23` ``` id :: "i=>i" where ``` paulson@46820 ` 24` ``` "id(A) == (\x\A. x)" ``` clasohm@0 ` 25` wenzelm@24893 ` 26` ```definition ``` paulson@1806 ` 27` ``` (*one-to-one functions from A to B*) ``` wenzelm@24893 ` 28` ``` inj :: "[i,i]=>i" where ``` paulson@46953 ` 29` ``` "inj(A,B) == { f \ A->B. \w\A. \x\A. f`w=f`x \ w=x}" ``` clasohm@0 ` 30` wenzelm@24893 ` 31` ```definition ``` paulson@1806 ` 32` ``` (*onto functions from A to B*) ``` wenzelm@24893 ` 33` ``` surj :: "[i,i]=>i" where ``` paulson@46953 ` 34` ``` "surj(A,B) == { f \ A->B . \y\B. \x\A. f`x=y}" ``` clasohm@0 ` 35` wenzelm@24893 ` 36` ```definition ``` paulson@1806 ` 37` ``` (*one-to-one and onto functions*) ``` wenzelm@24893 ` 38` ``` bij :: "[i,i]=>i" where ``` paulson@46820 ` 39` ``` "bij(A,B) == inj(A,B) \ surj(A,B)" ``` paulson@13176 ` 40` paulson@13176 ` 41` wenzelm@60770 ` 42` ```subsection\Surjective Function Space\ ``` paulson@13176 ` 43` paulson@46953 ` 44` ```lemma surj_is_fun: "f \ surj(A,B) ==> f \ A->B" ``` paulson@13176 ` 45` ```apply (unfold surj_def) ``` paulson@13176 ` 46` ```apply (erule CollectD1) ``` paulson@13176 ` 47` ```done ``` paulson@13176 ` 48` paulson@46953 ` 49` ```lemma fun_is_surj: "f \ Pi(A,B) ==> f \ surj(A,range(f))" ``` paulson@13176 ` 50` ```apply (unfold surj_def) ``` paulson@13176 ` 51` ```apply (blast intro: apply_equality range_of_fun domain_type) ``` paulson@13176 ` 52` ```done ``` paulson@13176 ` 53` paulson@46953 ` 54` ```lemma surj_range: "f \ surj(A,B) ==> range(f)=B" ``` paulson@13176 ` 55` ```apply (unfold surj_def) ``` paulson@13176 ` 56` ```apply (best intro: apply_Pair elim: range_type) ``` paulson@13176 ` 57` ```done ``` paulson@13176 ` 58` wenzelm@60770 ` 59` ```text\A function with a right inverse is a surjection\ ``` paulson@13176 ` 60` paulson@46821 ` 61` ```lemma f_imp_surjective: ``` paulson@46953 ` 62` ``` "[| f \ A->B; !!y. y \ B ==> d(y): A; !!y. y \ B ==> f`d(y) = y |] ``` paulson@46953 ` 63` ``` ==> f \ surj(A,B)" ``` paulson@41160 ` 64` ``` by (simp add: surj_def, blast) ``` paulson@13176 ` 65` paulson@46821 ` 66` ```lemma lam_surjective: ``` paulson@46953 ` 67` ``` "[| !!x. x \ A ==> c(x): B; ``` paulson@46953 ` 68` ``` !!y. y \ B ==> d(y): A; ``` paulson@46953 ` 69` ``` !!y. y \ B ==> c(d(y)) = y ``` paulson@46820 ` 70` ``` |] ==> (\x\A. c(x)) \ surj(A,B)" ``` paulson@46821 ` 71` ```apply (rule_tac d = d in f_imp_surjective) ``` paulson@13176 ` 72` ```apply (simp_all add: lam_type) ``` paulson@13176 ` 73` ```done ``` paulson@13176 ` 74` wenzelm@60770 ` 75` ```text\Cantor's theorem revisited\ ``` paulson@46820 ` 76` ```lemma cantor_surj: "f \ surj(A,Pow(A))" ``` paulson@13180 ` 77` ```apply (unfold surj_def, safe) ``` paulson@13176 ` 78` ```apply (cut_tac cantor) ``` paulson@46821 ` 79` ```apply (best del: subsetI) ``` paulson@13176 ` 80` ```done ``` paulson@13176 ` 81` paulson@13176 ` 82` wenzelm@60770 ` 83` ```subsection\Injective Function Space\ ``` paulson@13176 ` 84` paulson@46953 ` 85` ```lemma inj_is_fun: "f \ inj(A,B) ==> f \ A->B" ``` paulson@13176 ` 86` ```apply (unfold inj_def) ``` paulson@13176 ` 87` ```apply (erule CollectD1) ``` paulson@13176 ` 88` ```done ``` paulson@13176 ` 89` wenzelm@60770 ` 90` ```text\Good for dealing with sets of pairs, but a bit ugly in use [used in AC]\ ``` paulson@46821 ` 91` ```lemma inj_equality: ``` paulson@46953 ` 92` ``` "[| :f; :f; f \ inj(A,B) |] ==> a=c" ``` paulson@13176 ` 93` ```apply (unfold inj_def) ``` paulson@13176 ` 94` ```apply (blast dest: Pair_mem_PiD) ``` paulson@13176 ` 95` ```done ``` paulson@13176 ` 96` paulson@46953 ` 97` ```lemma inj_apply_equality: "[| f \ inj(A,B); f`a=f`b; a \ A; b \ A |] ==> a=b" ``` paulson@13180 ` 98` ```by (unfold inj_def, blast) ``` paulson@13176 ` 99` wenzelm@60770 ` 100` ```text\A function with a left inverse is an injection\ ``` paulson@13176 ` 101` paulson@46953 ` 102` ```lemma f_imp_injective: "[| f \ A->B; \x\A. d(f`x)=x |] ==> f \ inj(A,B)" ``` paulson@13176 ` 103` ```apply (simp (no_asm_simp) add: inj_def) ``` paulson@13176 ` 104` ```apply (blast intro: subst_context [THEN box_equals]) ``` paulson@13176 ` 105` ```done ``` paulson@13176 ` 106` paulson@46821 ` 107` ```lemma lam_injective: ``` paulson@46953 ` 108` ``` "[| !!x. x \ A ==> c(x): B; ``` paulson@46953 ` 109` ``` !!x. x \ A ==> d(c(x)) = x |] ``` paulson@46820 ` 110` ``` ==> (\x\A. c(x)) \ inj(A,B)" ``` paulson@13784 ` 111` ```apply (rule_tac d = d in f_imp_injective) ``` paulson@13176 ` 112` ```apply (simp_all add: lam_type) ``` paulson@13176 ` 113` ```done ``` paulson@13176 ` 114` wenzelm@60770 ` 115` ```subsection\Bijections\ ``` paulson@13176 ` 116` paulson@46953 ` 117` ```lemma bij_is_inj: "f \ bij(A,B) ==> f \ inj(A,B)" ``` paulson@13176 ` 118` ```apply (unfold bij_def) ``` paulson@13176 ` 119` ```apply (erule IntD1) ``` paulson@13176 ` 120` ```done ``` paulson@13176 ` 121` paulson@46953 ` 122` ```lemma bij_is_surj: "f \ bij(A,B) ==> f \ surj(A,B)" ``` paulson@13176 ` 123` ```apply (unfold bij_def) ``` paulson@13176 ` 124` ```apply (erule IntD2) ``` paulson@13176 ` 125` ```done ``` paulson@13176 ` 126` paulson@46953 ` 127` ```lemma bij_is_fun: "f \ bij(A,B) ==> f \ A->B" ``` paulson@46953 ` 128` ``` by (rule bij_is_inj [THEN inj_is_fun]) ``` paulson@13176 ` 129` paulson@46821 ` 130` ```lemma lam_bijective: ``` paulson@46953 ` 131` ``` "[| !!x. x \ A ==> c(x): B; ``` paulson@46953 ` 132` ``` !!y. y \ B ==> d(y): A; ``` paulson@46953 ` 133` ``` !!x. x \ A ==> d(c(x)) = x; ``` paulson@46953 ` 134` ``` !!y. y \ B ==> c(d(y)) = y ``` paulson@46820 ` 135` ``` |] ==> (\x\A. c(x)) \ bij(A,B)" ``` paulson@13176 ` 136` ```apply (unfold bij_def) ``` paulson@13180 ` 137` ```apply (blast intro!: lam_injective lam_surjective) ``` paulson@13176 ` 138` ```done ``` paulson@13176 ` 139` wenzelm@63901 ` 140` ```lemma RepFun_bijective: "(\y\x. \!y'. f(y') = f(y)) ``` paulson@46953 ` 141` ``` ==> (\z\{f(y). y \ x}. THE y. f(y) = z) \ bij({f(y). y \ x}, x)" ``` paulson@13784 ` 142` ```apply (rule_tac d = f in lam_bijective) ``` paulson@13176 ` 143` ```apply (auto simp add: the_equality2) ``` paulson@13176 ` 144` ```done ``` paulson@13176 ` 145` paulson@13176 ` 146` wenzelm@60770 ` 147` ```subsection\Identity Function\ ``` paulson@13176 ` 148` paulson@46953 ` 149` ```lemma idI [intro!]: "a \ A ==> \ id(A)" ``` paulson@13176 ` 150` ```apply (unfold id_def) ``` paulson@13176 ` 151` ```apply (erule lamI) ``` paulson@13176 ` 152` ```done ``` paulson@13176 ` 153` paulson@46953 ` 154` ```lemma idE [elim!]: "[| p \ id(A); !!x.[| x \ A; p= |] ==> P |] ==> P" ``` paulson@13180 ` 155` ```by (simp add: id_def lam_def, blast) ``` paulson@13176 ` 156` paulson@46820 ` 157` ```lemma id_type: "id(A) \ A->A" ``` paulson@13176 ` 158` ```apply (unfold id_def) ``` paulson@13180 ` 159` ```apply (rule lam_type, assumption) ``` paulson@13176 ` 160` ```done ``` paulson@13176 ` 161` paulson@46953 ` 162` ```lemma id_conv [simp]: "x \ A ==> id(A)`x = x" ``` paulson@13176 ` 163` ```apply (unfold id_def) ``` paulson@13176 ` 164` ```apply (simp (no_asm_simp)) ``` paulson@13176 ` 165` ```done ``` paulson@13176 ` 166` paulson@46820 ` 167` ```lemma id_mono: "A<=B ==> id(A) \ id(B)" ``` paulson@13176 ` 168` ```apply (unfold id_def) ``` paulson@13176 ` 169` ```apply (erule lam_mono) ``` paulson@13176 ` 170` ```done ``` paulson@13176 ` 171` paulson@13176 ` 172` ```lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)" ``` paulson@13176 ` 173` ```apply (simp add: inj_def id_def) ``` paulson@46821 ` 174` ```apply (blast intro: lam_type) ``` paulson@13176 ` 175` ```done ``` paulson@13176 ` 176` wenzelm@45602 ` 177` ```lemmas id_inj = subset_refl [THEN id_subset_inj] ``` paulson@13176 ` 178` paulson@13176 ` 179` ```lemma id_surj: "id(A): surj(A,A)" ``` paulson@13176 ` 180` ```apply (unfold id_def surj_def) ``` paulson@13176 ` 181` ```apply (simp (no_asm_simp)) ``` paulson@13176 ` 182` ```done ``` paulson@13176 ` 183` paulson@13176 ` 184` ```lemma id_bij: "id(A): bij(A,A)" ``` paulson@13176 ` 185` ```apply (unfold bij_def) ``` paulson@13176 ` 186` ```apply (blast intro: id_inj id_surj) ``` paulson@13176 ` 187` ```done ``` paulson@13176 ` 188` paulson@46821 ` 189` ```lemma subset_iff_id: "A \ B \ id(A) \ A->B" ``` paulson@13176 ` 190` ```apply (unfold id_def) ``` paulson@13180 ` 191` ```apply (force intro!: lam_type dest: apply_type) ``` paulson@13176 ` 192` ```done ``` paulson@13176 ` 193` wenzelm@60770 ` 194` ```text\@{term id} as the identity relation\ ``` paulson@46821 ` 195` ```lemma id_iff [simp]: " \ id(A) \ x=y & y \ A" ``` paulson@14060 ` 196` ```by auto ``` paulson@13176 ` 197` paulson@14060 ` 198` wenzelm@60770 ` 199` ```subsection\Converse of a Function\ ``` paulson@13176 ` 200` paulson@46953 ` 201` ```lemma inj_converse_fun: "f \ inj(A,B) ==> converse(f) \ range(f)->A" ``` paulson@13176 ` 202` ```apply (unfold inj_def) ``` paulson@13176 ` 203` ```apply (simp (no_asm_simp) add: Pi_iff function_def) ``` paulson@13176 ` 204` ```apply (erule CollectE) ``` paulson@13176 ` 205` ```apply (simp (no_asm_simp) add: apply_iff) ``` paulson@13176 ` 206` ```apply (blast dest: fun_is_rel) ``` paulson@13176 ` 207` ```done ``` paulson@13176 ` 208` wenzelm@60770 ` 209` ```text\Equations for converse(f)\ ``` paulson@13176 ` 210` wenzelm@60770 ` 211` ```text\The premises are equivalent to saying that f is injective...\ ``` paulson@13176 ` 212` ```lemma left_inverse_lemma: ``` paulson@46953 ` 213` ``` "[| f \ A->B; converse(f): C->A; a \ A |] ==> converse(f)`(f`a) = a" ``` paulson@13176 ` 214` ```by (blast intro: apply_Pair apply_equality converseI) ``` paulson@13176 ` 215` paulson@46953 ` 216` ```lemma left_inverse [simp]: "[| f \ inj(A,B); a \ A |] ==> converse(f)`(f`a) = a" ``` paulson@13180 ` 217` ```by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) ``` paulson@13176 ` 218` paulson@14883 ` 219` ```lemma left_inverse_eq: ``` paulson@14883 ` 220` ``` "[|f \ inj(A,B); f ` x = y; x \ A|] ==> converse(f) ` y = x" ``` paulson@14883 ` 221` ```by auto ``` paulson@14883 ` 222` wenzelm@45602 ` 223` ```lemmas left_inverse_bij = bij_is_inj [THEN left_inverse] ``` paulson@13176 ` 224` paulson@13176 ` 225` ```lemma right_inverse_lemma: ``` paulson@46953 ` 226` ``` "[| f \ A->B; converse(f): C->A; b \ C |] ==> f`(converse(f)`b) = b" ``` paulson@46821 ` 227` ```by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) ``` paulson@13176 ` 228` paulson@46953 ` 229` ```(*Should the premises be f \ surj(A,B), b \ B for symmetry with left_inverse? ``` paulson@13176 ` 230` ``` No: they would not imply that converse(f) was a function! *) ``` paulson@13176 ` 231` ```lemma right_inverse [simp]: ``` paulson@46953 ` 232` ``` "[| f \ inj(A,B); b \ range(f) |] ==> f`(converse(f)`b) = b" ``` paulson@13176 ` 233` ```by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun) ``` paulson@13176 ` 234` paulson@46953 ` 235` ```lemma right_inverse_bij: "[| f \ bij(A,B); b \ B |] ==> f`(converse(f)`b) = b" ``` paulson@13180 ` 236` ```by (force simp add: bij_def surj_range) ``` paulson@13176 ` 237` wenzelm@60770 ` 238` ```subsection\Converses of Injections, Surjections, Bijections\ ``` paulson@13176 ` 239` paulson@46953 ` 240` ```lemma inj_converse_inj: "f \ inj(A,B) ==> converse(f): inj(range(f), A)" ``` paulson@13176 ` 241` ```apply (rule f_imp_injective) ``` paulson@46821 ` 242` ```apply (erule inj_converse_fun, clarify) ``` paulson@13180 ` 243` ```apply (rule right_inverse) ``` paulson@13176 ` 244` ``` apply assumption ``` paulson@46821 ` 245` ```apply blast ``` paulson@13176 ` 246` ```done ``` paulson@13176 ` 247` paulson@46953 ` 248` ```lemma inj_converse_surj: "f \ inj(A,B) ==> converse(f): surj(range(f), A)" ``` paulson@46821 ` 249` ```by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun ``` paulson@13176 ` 250` ``` range_of_fun [THEN apply_type]) ``` paulson@13176 ` 251` wenzelm@60770 ` 252` ```text\Adding this as an intro! rule seems to cause looping\ ``` paulson@46953 ` 253` ```lemma bij_converse_bij [TC]: "f \ bij(A,B) ==> converse(f): bij(B,A)" ``` paulson@13176 ` 254` ```apply (unfold bij_def) ``` paulson@13176 ` 255` ```apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj) ``` paulson@13176 ` 256` ```done ``` paulson@13176 ` 257` paulson@13176 ` 258` paulson@13176 ` 259` wenzelm@60770 ` 260` ```subsection\Composition of Two Relations\ ``` paulson@13176 ` 261` wenzelm@60770 ` 262` ```text\The inductive definition package could derive these theorems for @{term"r O s"}\ ``` paulson@13176 ` 263` paulson@46820 ` 264` ```lemma compI [intro]: "[| :s; :r |] ==> \ r O s" ``` paulson@13180 ` 265` ```by (unfold comp_def, blast) ``` paulson@13176 ` 266` paulson@46821 ` 267` ```lemma compE [elim!]: ``` paulson@46821 ` 268` ``` "[| xz \ r O s; ``` paulson@13176 ` 269` ``` !!x y z. [| xz=; :s; :r |] ==> P |] ``` paulson@13176 ` 270` ``` ==> P" ``` paulson@13180 ` 271` ```by (unfold comp_def, blast) ``` paulson@13176 ` 272` paulson@46821 ` 273` ```lemma compEpair: ``` paulson@46821 ` 274` ``` "[| \ r O s; ``` paulson@13176 ` 275` ``` !!y. [| :s; :r |] ==> P |] ``` paulson@13176 ` 276` ``` ==> P" ``` paulson@46821 ` 277` ```by (erule compE, simp) ``` paulson@13176 ` 278` paulson@13176 ` 279` ```lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" ``` paulson@13180 ` 280` ```by blast ``` paulson@13176 ` 281` paulson@13176 ` 282` wenzelm@60770 ` 283` ```subsection\Domain and Range -- see Suppes, Section 3.1\ ``` paulson@13176 ` 284` wenzelm@60770 ` 285` ```text\Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327\ ``` paulson@46820 ` 286` ```lemma range_comp: "range(r O s) \ range(r)" ``` paulson@13180 ` 287` ```by blast ``` paulson@13176 ` 288` paulson@46820 ` 289` ```lemma range_comp_eq: "domain(r) \ range(s) ==> range(r O s) = range(r)" ``` paulson@13180 ` 290` ```by (rule range_comp [THEN equalityI], blast) ``` paulson@13176 ` 291` paulson@46820 ` 292` ```lemma domain_comp: "domain(r O s) \ domain(s)" ``` paulson@13180 ` 293` ```by blast ``` paulson@13176 ` 294` paulson@46820 ` 295` ```lemma domain_comp_eq: "range(s) \ domain(r) ==> domain(r O s) = domain(s)" ``` paulson@13180 ` 296` ```by (rule domain_comp [THEN equalityI], blast) ``` paulson@13176 ` 297` paulson@13176 ` 298` ```lemma image_comp: "(r O s)``A = r``(s``A)" ``` paulson@13180 ` 299` ```by blast ``` paulson@13176 ` 300` paulson@46953 ` 301` ```lemma inj_inj_range: "f \ inj(A,B) ==> f \ inj(A,range(f))" ``` paulson@41160 ` 302` ``` by (auto simp add: inj_def Pi_iff function_def) ``` paulson@41160 ` 303` paulson@46953 ` 304` ```lemma inj_bij_range: "f \ inj(A,B) ==> f \ bij(A,range(f))" ``` paulson@46821 ` 305` ``` by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) ``` paulson@41160 ` 306` paulson@13176 ` 307` wenzelm@60770 ` 308` ```subsection\Other Results\ ``` paulson@13176 ` 309` paulson@46820 ` 310` ```lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') \ (r O s)" ``` paulson@13180 ` 311` ```by blast ``` paulson@13176 ` 312` wenzelm@60770 ` 313` ```text\composition preserves relations\ ``` paulson@46820 ` 314` ```lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) \ A*C" ``` paulson@13180 ` 315` ```by blast ``` paulson@13176 ` 316` wenzelm@60770 ` 317` ```text\associative law for composition\ ``` paulson@13176 ` 318` ```lemma comp_assoc: "(r O s) O t = r O (s O t)" ``` paulson@13180 ` 319` ```by blast ``` paulson@13176 ` 320` paulson@13176 ` 321` ```(*left identity of composition; provable inclusions are ``` paulson@46821 ` 322` ``` id(A) O r \ r ``` paulson@46820 ` 323` ``` and [| r<=A*B; B<=C |] ==> r \ id(C) O r *) ``` paulson@13176 ` 324` ```lemma left_comp_id: "r<=A*B ==> id(B) O r = r" ``` paulson@13180 ` 325` ```by blast ``` paulson@13176 ` 326` paulson@13176 ` 327` ```(*right identity of composition; provable inclusions are ``` paulson@46820 ` 328` ``` r O id(A) \ r ``` paulson@46820 ` 329` ``` and [| r<=A*B; A<=C |] ==> r \ r O id(C) *) ``` paulson@13176 ` 330` ```lemma right_comp_id: "r<=A*B ==> r O id(A) = r" ``` paulson@13180 ` 331` ```by blast ``` paulson@13176 ` 332` paulson@13176 ` 333` wenzelm@60770 ` 334` ```subsection\Composition Preserves Functions, Injections, and Surjections\ ``` paulson@13176 ` 335` paulson@13180 ` 336` ```lemma comp_function: "[| function(g); function(f) |] ==> function(f O g)" ``` paulson@13180 ` 337` ```by (unfold function_def, blast) ``` paulson@13176 ` 338` wenzelm@60770 ` 339` ```text\Don't think the premises can be weakened much\ ``` paulson@46953 ` 340` ```lemma comp_fun: "[| g \ A->B; f \ B->C |] ==> (f O g) \ A->C" ``` paulson@13176 ` 341` ```apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) ``` paulson@46821 ` 342` ```apply (subst range_rel_subset [THEN domain_comp_eq], auto) ``` paulson@13176 ` 343` ```done ``` paulson@13176 ` 344` paulson@46953 ` 345` ```(*Thanks to the new definition of "apply", the premise f \ B->C is gone!*) ``` paulson@13176 ` 346` ```lemma comp_fun_apply [simp]: ``` paulson@46953 ` 347` ``` "[| g \ A->B; a \ A |] ==> (f O g)`a = f`(g`a)" ``` paulson@46821 ` 348` ```apply (frule apply_Pair, assumption) ``` paulson@13176 ` 349` ```apply (simp add: apply_def image_comp) ``` paulson@46821 ` 350` ```apply (blast dest: apply_equality) ``` paulson@13176 ` 351` ```done ``` paulson@13176 ` 352` wenzelm@60770 ` 353` ```text\Simplifies compositions of lambda-abstractions\ ``` paulson@46821 ` 354` ```lemma comp_lam: ``` paulson@46953 ` 355` ``` "[| !!x. x \ A ==> b(x): B |] ``` paulson@46820 ` 356` ``` ==> (\y\B. c(y)) O (\x\A. b(x)) = (\x\A. c(b(x)))" ``` paulson@46821 ` 357` ```apply (subgoal_tac "(\x\A. b(x)) \ A -> B") ``` paulson@13176 ` 358` ``` apply (rule fun_extension) ``` paulson@13176 ` 359` ``` apply (blast intro: comp_fun lam_funtype) ``` paulson@13176 ` 360` ``` apply (rule lam_funtype) ``` paulson@46821 ` 361` ``` apply simp ``` paulson@46821 ` 362` ```apply (simp add: lam_type) ``` paulson@13176 ` 363` ```done ``` paulson@13176 ` 364` paulson@13176 ` 365` ```lemma comp_inj: ``` paulson@46953 ` 366` ``` "[| g \ inj(A,B); f \ inj(B,C) |] ==> (f O g) \ inj(A,C)" ``` paulson@46821 ` 367` ```apply (frule inj_is_fun [of g]) ``` paulson@46821 ` 368` ```apply (frule inj_is_fun [of f]) ``` paulson@13176 ` 369` ```apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective) ``` paulson@46821 ` 370` ``` apply (blast intro: comp_fun, simp) ``` paulson@13176 ` 371` ```done ``` paulson@13176 ` 372` paulson@46821 ` 373` ```lemma comp_surj: ``` paulson@46953 ` 374` ``` "[| g \ surj(A,B); f \ surj(B,C) |] ==> (f O g) \ surj(A,C)" ``` paulson@13176 ` 375` ```apply (unfold surj_def) ``` paulson@13176 ` 376` ```apply (blast intro!: comp_fun comp_fun_apply) ``` paulson@13176 ` 377` ```done ``` paulson@13176 ` 378` paulson@46821 ` 379` ```lemma comp_bij: ``` paulson@46953 ` 380` ``` "[| g \ bij(A,B); f \ bij(B,C) |] ==> (f O g) \ bij(A,C)" ``` paulson@13176 ` 381` ```apply (unfold bij_def) ``` paulson@13176 ` 382` ```apply (blast intro: comp_inj comp_surj) ``` paulson@13176 ` 383` ```done ``` paulson@13176 ` 384` paulson@13176 ` 385` wenzelm@60770 ` 386` ```subsection\Dual Properties of @{term inj} and @{term surj}\ ``` paulson@13356 ` 387` wenzelm@60770 ` 388` ```text\Useful for proofs from ``` paulson@46821 ` 389` ``` D Pastre. Automatic theorem proving in set theory. ``` wenzelm@60770 ` 390` ``` Artificial Intelligence, 10:1--27, 1978.\ ``` paulson@13176 ` 391` paulson@46821 ` 392` ```lemma comp_mem_injD1: ``` paulson@46953 ` 393` ``` "[| (f O g): inj(A,C); g \ A->B; f \ B->C |] ==> g \ inj(A,B)" ``` paulson@46821 ` 394` ```by (unfold inj_def, force) ``` paulson@13176 ` 395` paulson@46821 ` 396` ```lemma comp_mem_injD2: ``` paulson@46953 ` 397` ``` "[| (f O g): inj(A,C); g \ surj(A,B); f \ B->C |] ==> f \ inj(B,C)" ``` paulson@13180 ` 398` ```apply (unfold inj_def surj_def, safe) ``` paulson@13784 ` 399` ```apply (rule_tac x1 = x in bspec [THEN bexE]) ``` paulson@13784 ` 400` ```apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe) ``` paulson@13176 ` 401` ```apply (rule_tac t = "op ` (g) " in subst_context) ``` paulson@13176 ` 402` ```apply (erule asm_rl bspec [THEN bspec, THEN mp])+ ``` paulson@13176 ` 403` ```apply (simp (no_asm_simp)) ``` paulson@13176 ` 404` ```done ``` paulson@13176 ` 405` paulson@46821 ` 406` ```lemma comp_mem_surjD1: ``` paulson@46953 ` 407` ``` "[| (f O g): surj(A,C); g \ A->B; f \ B->C |] ==> f \ surj(B,C)" ``` paulson@13176 ` 408` ```apply (unfold surj_def) ``` paulson@13176 ` 409` ```apply (blast intro!: comp_fun_apply [symmetric] apply_funtype) ``` paulson@13176 ` 410` ```done ``` paulson@13176 ` 411` paulson@13176 ` 412` paulson@46821 ` 413` ```lemma comp_mem_surjD2: ``` paulson@46953 ` 414` ``` "[| (f O g): surj(A,C); g \ A->B; f \ inj(B,C) |] ==> g \ surj(A,B)" ``` paulson@13180 ` 415` ```apply (unfold inj_def surj_def, safe) ``` paulson@46821 ` 416` ```apply (drule_tac x = "f`y" in bspec, auto) ``` paulson@13176 ` 417` ```apply (blast intro: apply_funtype) ``` paulson@13176 ` 418` ```done ``` paulson@13176 ` 419` wenzelm@60770 ` 420` ```subsubsection\Inverses of Composition\ ``` paulson@13176 ` 421` wenzelm@60770 ` 422` ```text\left inverse of composition; one inclusion is ``` wenzelm@60770 ` 423` ``` @{term "f \ A->B ==> id(A) \ converse(f) O f"}\ ``` paulson@46953 ` 424` ```lemma left_comp_inverse: "f \ inj(A,B) ==> converse(f) O f = id(A)" ``` paulson@46821 ` 425` ```apply (unfold inj_def, clarify) ``` paulson@46821 ` 426` ```apply (rule equalityI) ``` paulson@46821 ` 427` ``` apply (auto simp add: apply_iff, blast) ``` paulson@13176 ` 428` ```done ``` paulson@13176 ` 429` wenzelm@60770 ` 430` ```text\right inverse of composition; one inclusion is ``` wenzelm@60770 ` 431` ``` @{term "f \ A->B ==> f O converse(f) \ id(B)"}\ ``` paulson@46821 ` 432` ```lemma right_comp_inverse: ``` paulson@46953 ` 433` ``` "f \ surj(A,B) ==> f O converse(f) = id(B)" ``` paulson@46821 ` 434` ```apply (simp add: surj_def, clarify) ``` paulson@13176 ` 435` ```apply (rule equalityI) ``` paulson@13176 ` 436` ```apply (best elim: domain_type range_type dest: apply_equality2) ``` paulson@13176 ` 437` ```apply (blast intro: apply_Pair) ``` paulson@13176 ` 438` ```done ``` paulson@13176 ` 439` paulson@13176 ` 440` wenzelm@60770 ` 441` ```subsubsection\Proving that a Function is a Bijection\ ``` paulson@13176 ` 442` paulson@46821 ` 443` ```lemma comp_eq_id_iff: ``` paulson@46953 ` 444` ``` "[| f \ A->B; g \ B->A |] ==> f O g = id(B) \ (\y\B. f`(g`y)=y)" ``` paulson@13180 ` 445` ```apply (unfold id_def, safe) ``` paulson@13176 ` 446` ``` apply (drule_tac t = "%h. h`y " in subst_context) ``` paulson@13176 ` 447` ``` apply simp ``` paulson@13176 ` 448` ```apply (rule fun_extension) ``` paulson@13176 ` 449` ``` apply (blast intro: comp_fun lam_type) ``` paulson@13176 ` 450` ``` apply auto ``` paulson@13176 ` 451` ```done ``` paulson@13176 ` 452` paulson@46821 ` 453` ```lemma fg_imp_bijective: ``` paulson@46953 ` 454` ``` "[| f \ A->B; g \ B->A; f O g = id(B); g O f = id(A) |] ==> f \ bij(A,B)" ``` paulson@13176 ` 455` ```apply (unfold bij_def) ``` paulson@13176 ` 456` ```apply (simp add: comp_eq_id_iff) ``` paulson@13180 ` 457` ```apply (blast intro: f_imp_injective f_imp_surjective apply_funtype) ``` paulson@13176 ` 458` ```done ``` paulson@13176 ` 459` paulson@46953 ` 460` ```lemma nilpotent_imp_bijective: "[| f \ A->A; f O f = id(A) |] ==> f \ bij(A,A)" ``` paulson@13180 ` 461` ```by (blast intro: fg_imp_bijective) ``` paulson@13176 ` 462` paulson@13180 ` 463` ```lemma invertible_imp_bijective: ``` paulson@46953 ` 464` ``` "[| converse(f): B->A; f \ A->B |] ==> f \ bij(A,B)" ``` paulson@46821 ` 465` ```by (simp add: fg_imp_bijective comp_eq_id_iff ``` paulson@13180 ` 466` ``` left_inverse_lemma right_inverse_lemma) ``` paulson@13176 ` 467` wenzelm@60770 ` 468` ```subsubsection\Unions of Functions\ ``` paulson@13356 ` 469` wenzelm@60770 ` 470` ```text\See similar theorems in func.thy\ ``` paulson@13176 ` 471` wenzelm@60770 ` 472` ```text\Theorem by KG, proof by LCP\ ``` paulson@13176 ` 473` ```lemma inj_disjoint_Un: ``` paulson@46953 ` 474` ``` "[| f \ inj(A,B); g \ inj(C,D); B \ D = 0 |] ``` paulson@46953 ` 475` ``` ==> (\a\A \ C. if a \ A then f`a else g`a) \ inj(A \ C, B \ D)" ``` paulson@46953 ` 476` ```apply (rule_tac d = "%z. if z \ B then converse (f) `z else converse (g) `z" ``` paulson@13180 ` 477` ``` in lam_injective) ``` paulson@13176 ` 478` ```apply (auto simp add: inj_is_fun [THEN apply_type]) ``` paulson@13176 ` 479` ```done ``` paulson@13176 ` 480` paulson@46821 ` 481` ```lemma surj_disjoint_Un: ``` paulson@46953 ` 482` ``` "[| f \ surj(A,B); g \ surj(C,D); A \ C = 0 |] ``` paulson@46820 ` 483` ``` ==> (f \ g) \ surj(A \ C, B \ D)" ``` paulson@46821 ` 484` ```apply (simp add: surj_def fun_disjoint_Un) ``` paulson@46821 ` 485` ```apply (blast dest!: domain_of_fun ``` wenzelm@32960 ` 486` ``` intro!: fun_disjoint_apply1 fun_disjoint_apply2) ``` paulson@13176 ` 487` ```done ``` paulson@13176 ` 488` wenzelm@60770 ` 489` ```text\A simple, high-level proof; the version for injections follows from it, ``` wenzelm@60770 ` 490` ``` using @{term "f \ inj(A,B) \ f \ bij(A,range(f))"}\ ``` paulson@13176 ` 491` ```lemma bij_disjoint_Un: ``` paulson@46953 ` 492` ``` "[| f \ bij(A,B); g \ bij(C,D); A \ C = 0; B \ D = 0 |] ``` paulson@46820 ` 493` ``` ==> (f \ g) \ bij(A \ C, B \ D)" ``` paulson@13176 ` 494` ```apply (rule invertible_imp_bijective) ``` paulson@13176 ` 495` ```apply (subst converse_Un) ``` paulson@13176 ` 496` ```apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij) ``` paulson@13176 ` 497` ```done ``` paulson@13176 ` 498` paulson@13176 ` 499` wenzelm@60770 ` 500` ```subsubsection\Restrictions as Surjections and Bijections\ ``` paulson@13176 ` 501` paulson@13176 ` 502` ```lemma surj_image: ``` paulson@46953 ` 503` ``` "f \ Pi(A,B) ==> f \ surj(A, f``A)" ``` paulson@46821 ` 504` ```apply (simp add: surj_def) ``` paulson@46821 ` 505` ```apply (blast intro: apply_equality apply_Pair Pi_type) ``` paulson@13176 ` 506` ```done ``` paulson@13176 ` 507` paulson@47101 ` 508` ```lemma surj_image_eq: "f \ surj(A, B) ==> f``A = B" ``` paulson@47101 ` 509` ``` by (auto simp add: surj_def image_fun) (blast dest: apply_type) ``` paulson@47101 ` 510` paulson@46820 ` 511` ```lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \ B)" ``` paulson@13180 ` 512` ```by (auto simp add: restrict_def) ``` paulson@13176 ` 513` paulson@46821 ` 514` ```lemma restrict_inj: ``` paulson@46953 ` 515` ``` "[| f \ inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)" ``` paulson@13176 ` 516` ```apply (unfold inj_def) ``` paulson@46821 ` 517` ```apply (safe elim!: restrict_type2, auto) ``` paulson@13176 ` 518` ```done ``` paulson@13176 ` 519` paulson@46953 ` 520` ```lemma restrict_surj: "[| f \ Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)" ``` paulson@13176 ` 521` ```apply (insert restrict_type2 [THEN surj_image]) ``` paulson@46821 ` 522` ```apply (simp add: restrict_image) ``` paulson@13176 ` 523` ```done ``` paulson@13176 ` 524` paulson@46821 ` 525` ```lemma restrict_bij: ``` paulson@46953 ` 526` ``` "[| f \ inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)" ``` paulson@13180 ` 527` ```apply (simp add: inj_def bij_def) ``` paulson@13180 ` 528` ```apply (blast intro: restrict_surj surj_is_fun) ``` paulson@13176 ` 529` ```done ``` paulson@13176 ` 530` paulson@13176 ` 531` wenzelm@60770 ` 532` ```subsubsection\Lemmas for Ramsey's Theorem\ ``` paulson@13176 ` 533` paulson@46953 ` 534` ```lemma inj_weaken_type: "[| f \ inj(A,B); B<=D |] ==> f \ inj(A,D)" ``` paulson@13176 ` 535` ```apply (unfold inj_def) ``` paulson@13176 ` 536` ```apply (blast intro: fun_weaken_type) ``` paulson@13176 ` 537` ```done ``` paulson@13176 ` 538` paulson@13176 ` 539` ```lemma inj_succ_restrict: ``` paulson@46953 ` 540` ``` "[| f \ inj(succ(m), A) |] ==> restrict(f,m) \ inj(m, A-{f`m})" ``` paulson@13269 ` 541` ```apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast) ``` paulson@13176 ` 542` ```apply (unfold inj_def) ``` paulson@13176 ` 543` ```apply (fast elim: range_type mem_irrefl dest: apply_equality) ``` paulson@13176 ` 544` ```done ``` paulson@13176 ` 545` paulson@13176 ` 546` paulson@46821 ` 547` ```lemma inj_extend: ``` paulson@46953 ` 548` ``` "[| f \ inj(A,B); a\A; b\B |] ``` paulson@46820 ` 549` ``` ==> cons(,f) \ inj(cons(a,A), cons(b,B))" ``` paulson@13176 ` 550` ```apply (unfold inj_def) ``` paulson@13176 ` 551` ```apply (force intro: apply_type simp add: fun_extend) ``` paulson@13176 ` 552` ```done ``` paulson@13176 ` 553` clasohm@0 ` 554` ```end ```