src/HOL/Fun.thy
 author traytel Mon Nov 25 10:14:29 2013 +0100 (2013-11-25) changeset 54578 9387251b6a46 parent 54147 97a8ff4e4ac9 child 55019 0d5e831175de permissions -rw-r--r--
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
 clasohm@1475 ` 1` ```(* Title: HOL/Fun.thy ``` clasohm@1475 ` 2` ``` Author: Tobias Nipkow, Cambridge University Computer Laboratory ``` clasohm@923 ` 3` ``` Copyright 1994 University of Cambridge ``` huffman@18154 ` 4` ```*) ``` clasohm@923 ` 5` huffman@18154 ` 6` ```header {* Notions about functions *} ``` clasohm@923 ` 7` paulson@15510 ` 8` ```theory Fun ``` haftmann@44860 ` 9` ```imports Complete_Lattices ``` wenzelm@46950 ` 10` ```keywords "enriched_type" :: thy_goal ``` nipkow@15131 ` 11` ```begin ``` nipkow@2912 ` 12` haftmann@26147 ` 13` ```lemma apply_inverse: ``` haftmann@26357 ` 14` ``` "f x = u \ (\x. P x \ g (f x) = x) \ P x \ x = g u" ``` haftmann@26147 ` 15` ``` by auto ``` nipkow@2912 ` 16` wenzelm@12258 ` 17` haftmann@26147 ` 18` ```subsection {* The Identity Function @{text id} *} ``` paulson@6171 ` 19` haftmann@44277 ` 20` ```definition id :: "'a \ 'a" where ``` haftmann@22744 ` 21` ``` "id = (\x. x)" ``` nipkow@13910 ` 22` haftmann@26147 ` 23` ```lemma id_apply [simp]: "id x = x" ``` haftmann@26147 ` 24` ``` by (simp add: id_def) ``` haftmann@26147 ` 25` huffman@47579 ` 26` ```lemma image_id [simp]: "image id = id" ``` huffman@47579 ` 27` ``` by (simp add: id_def fun_eq_iff) ``` haftmann@26147 ` 28` huffman@47579 ` 29` ```lemma vimage_id [simp]: "vimage id = id" ``` huffman@47579 ` 30` ``` by (simp add: id_def fun_eq_iff) ``` haftmann@26147 ` 31` haftmann@52435 ` 32` ```code_printing ``` haftmann@52435 ` 33` ``` constant id \ (Haskell) "id" ``` haftmann@52435 ` 34` haftmann@26147 ` 35` haftmann@26147 ` 36` ```subsection {* The Composition Operator @{text "f \ g"} *} ``` haftmann@26147 ` 37` haftmann@44277 ` 38` ```definition comp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" (infixl "o" 55) where ``` haftmann@22744 ` 39` ``` "f o g = (\x. f (g x))" ``` oheimb@11123 ` 40` wenzelm@21210 ` 41` ```notation (xsymbols) ``` wenzelm@19656 ` 42` ``` comp (infixl "\" 55) ``` wenzelm@19656 ` 43` wenzelm@21210 ` 44` ```notation (HTML output) ``` wenzelm@19656 ` 45` ``` comp (infixl "\" 55) ``` wenzelm@19656 ` 46` haftmann@49739 ` 47` ```lemma comp_apply [simp]: "(f o g) x = f (g x)" ``` haftmann@49739 ` 48` ``` by (simp add: comp_def) ``` paulson@13585 ` 49` haftmann@49739 ` 50` ```lemma comp_assoc: "(f o g) o h = f o (g o h)" ``` haftmann@49739 ` 51` ``` by (simp add: fun_eq_iff) ``` paulson@13585 ` 52` haftmann@49739 ` 53` ```lemma id_comp [simp]: "id o g = g" ``` haftmann@49739 ` 54` ``` by (simp add: fun_eq_iff) ``` paulson@13585 ` 55` haftmann@49739 ` 56` ```lemma comp_id [simp]: "f o id = f" ``` haftmann@49739 ` 57` ``` by (simp add: fun_eq_iff) ``` haftmann@49739 ` 58` haftmann@49739 ` 59` ```lemma comp_eq_dest: ``` haftmann@34150 ` 60` ``` "a o b = c o d \ a (b v) = c (d v)" ``` haftmann@49739 ` 61` ``` by (simp add: fun_eq_iff) ``` haftmann@34150 ` 62` haftmann@49739 ` 63` ```lemma comp_eq_elim: ``` haftmann@34150 ` 64` ``` "a o b = c o d \ ((\v. a (b v) = c (d v)) \ R) \ R" ``` haftmann@49739 ` 65` ``` by (simp add: fun_eq_iff) ``` haftmann@34150 ` 66` haftmann@49739 ` 67` ```lemma image_comp: ``` haftmann@49739 ` 68` ``` "(f o g) ` r = f ` (g ` r)" ``` paulson@33044 ` 69` ``` by auto ``` paulson@33044 ` 70` haftmann@49739 ` 71` ```lemma vimage_comp: ``` haftmann@49739 ` 72` ``` "(g \ f) -` x = f -` (g -` x)" ``` haftmann@49739 ` 73` ``` by auto ``` haftmann@49739 ` 74` haftmann@49739 ` 75` ```lemma INF_comp: ``` haftmann@49739 ` 76` ``` "INFI A (g \ f) = INFI (f ` A) g" ``` haftmann@49739 ` 77` ``` by (simp add: INF_def image_comp) ``` haftmann@49739 ` 78` haftmann@49739 ` 79` ```lemma SUP_comp: ``` haftmann@49739 ` 80` ``` "SUPR A (g \ f) = SUPR (f ` A) g" ``` haftmann@49739 ` 81` ``` by (simp add: SUP_def image_comp) ``` paulson@13585 ` 82` haftmann@52435 ` 83` ```code_printing ``` haftmann@52435 ` 84` ``` constant comp \ (SML) infixl 5 "o" and (Haskell) infixr 9 "." ``` haftmann@52435 ` 85` paulson@13585 ` 86` haftmann@26588 ` 87` ```subsection {* The Forward Composition Operator @{text fcomp} *} ``` haftmann@26357 ` 88` haftmann@44277 ` 89` ```definition fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl "\>" 60) where ``` haftmann@37751 ` 90` ``` "f \> g = (\x. g (f x))" ``` haftmann@26357 ` 91` haftmann@37751 ` 92` ```lemma fcomp_apply [simp]: "(f \> g) x = g (f x)" ``` haftmann@26357 ` 93` ``` by (simp add: fcomp_def) ``` haftmann@26357 ` 94` haftmann@37751 ` 95` ```lemma fcomp_assoc: "(f \> g) \> h = f \> (g \> h)" ``` haftmann@26357 ` 96` ``` by (simp add: fcomp_def) ``` haftmann@26357 ` 97` haftmann@37751 ` 98` ```lemma id_fcomp [simp]: "id \> g = g" ``` haftmann@26357 ` 99` ``` by (simp add: fcomp_def) ``` haftmann@26357 ` 100` haftmann@37751 ` 101` ```lemma fcomp_id [simp]: "f \> id = f" ``` haftmann@26357 ` 102` ``` by (simp add: fcomp_def) ``` haftmann@26357 ` 103` haftmann@52435 ` 104` ```code_printing ``` haftmann@52435 ` 105` ``` constant fcomp \ (Eval) infixl 1 "#>" ``` haftmann@31202 ` 106` haftmann@37751 ` 107` ```no_notation fcomp (infixl "\>" 60) ``` haftmann@26588 ` 108` haftmann@26357 ` 109` haftmann@40602 ` 110` ```subsection {* Mapping functions *} ``` haftmann@40602 ` 111` haftmann@40602 ` 112` ```definition map_fun :: "('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" where ``` haftmann@40602 ` 113` ``` "map_fun f g h = g \ h \ f" ``` haftmann@40602 ` 114` haftmann@40602 ` 115` ```lemma map_fun_apply [simp]: ``` haftmann@40602 ` 116` ``` "map_fun f g h x = g (h (f x))" ``` haftmann@40602 ` 117` ``` by (simp add: map_fun_def) ``` haftmann@40602 ` 118` haftmann@40602 ` 119` hoelzl@40702 ` 120` ```subsection {* Injectivity and Bijectivity *} ``` hoelzl@39076 ` 121` hoelzl@39076 ` 122` ```definition inj_on :: "('a \ 'b) \ 'a set \ bool" where -- "injective" ``` hoelzl@39076 ` 123` ``` "inj_on f A \ (\x\A. \y\A. f x = f y \ x = y)" ``` haftmann@26147 ` 124` hoelzl@39076 ` 125` ```definition bij_betw :: "('a \ 'b) \ 'a set \ 'b set \ bool" where -- "bijective" ``` hoelzl@39076 ` 126` ``` "bij_betw f A B \ inj_on f A \ f ` A = B" ``` haftmann@26147 ` 127` hoelzl@40702 ` 128` ```text{*A common special case: functions injective, surjective or bijective over ``` hoelzl@40702 ` 129` ```the entire domain type.*} ``` haftmann@26147 ` 130` haftmann@26147 ` 131` ```abbreviation ``` hoelzl@39076 ` 132` ``` "inj f \ inj_on f UNIV" ``` haftmann@26147 ` 133` hoelzl@40702 ` 134` ```abbreviation surj :: "('a \ 'b) \ bool" where -- "surjective" ``` hoelzl@40702 ` 135` ``` "surj f \ (range f = UNIV)" ``` paulson@13585 ` 136` hoelzl@39076 ` 137` ```abbreviation ``` hoelzl@39076 ` 138` ``` "bij f \ bij_betw f UNIV UNIV" ``` haftmann@26147 ` 139` nipkow@43705 ` 140` ```text{* The negated case: *} ``` nipkow@43705 ` 141` ```translations ``` nipkow@43705 ` 142` ```"\ CONST surj f" <= "CONST range f \ CONST UNIV" ``` nipkow@43705 ` 143` haftmann@26147 ` 144` ```lemma injI: ``` haftmann@26147 ` 145` ``` assumes "\x y. f x = f y \ x = y" ``` haftmann@26147 ` 146` ``` shows "inj f" ``` haftmann@26147 ` 147` ``` using assms unfolding inj_on_def by auto ``` paulson@13585 ` 148` berghofe@13637 ` 149` ```theorem range_ex1_eq: "inj f \ b : range f = (EX! x. b = f x)" ``` berghofe@13637 ` 150` ``` by (unfold inj_on_def, blast) ``` berghofe@13637 ` 151` paulson@13585 ` 152` ```lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y" ``` paulson@13585 ` 153` ```by (simp add: inj_on_def) ``` paulson@13585 ` 154` nipkow@32988 ` 155` ```lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)" ``` paulson@13585 ` 156` ```by (force simp add: inj_on_def) ``` paulson@13585 ` 157` hoelzl@40703 ` 158` ```lemma inj_on_cong: ``` hoelzl@40703 ` 159` ``` "(\ a. a : A \ f a = g a) \ inj_on f A = inj_on g A" ``` hoelzl@40703 ` 160` ```unfolding inj_on_def by auto ``` hoelzl@40703 ` 161` hoelzl@40703 ` 162` ```lemma inj_on_strict_subset: ``` hoelzl@40703 ` 163` ``` "\ inj_on f B; A < B \ \ f`A < f`B" ``` hoelzl@40703 ` 164` ```unfolding inj_on_def unfolding image_def by blast ``` hoelzl@40703 ` 165` haftmann@38620 ` 166` ```lemma inj_comp: ``` haftmann@38620 ` 167` ``` "inj f \ inj g \ inj (f \ g)" ``` haftmann@38620 ` 168` ``` by (simp add: inj_on_def) ``` haftmann@38620 ` 169` haftmann@38620 ` 170` ```lemma inj_fun: "inj f \ inj (\x y. f x)" ``` nipkow@39302 ` 171` ``` by (simp add: inj_on_def fun_eq_iff) ``` haftmann@38620 ` 172` nipkow@32988 ` 173` ```lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)" ``` nipkow@32988 ` 174` ```by (simp add: inj_on_eq_iff) ``` nipkow@32988 ` 175` haftmann@26147 ` 176` ```lemma inj_on_id[simp]: "inj_on id A" ``` hoelzl@39076 ` 177` ``` by (simp add: inj_on_def) ``` paulson@13585 ` 178` haftmann@26147 ` 179` ```lemma inj_on_id2[simp]: "inj_on (%x. x) A" ``` hoelzl@39076 ` 180` ```by (simp add: inj_on_def) ``` haftmann@26147 ` 181` bulwahn@46586 ` 182` ```lemma inj_on_Int: "inj_on f A \ inj_on f B \ inj_on f (A \ B)" ``` hoelzl@40703 ` 183` ```unfolding inj_on_def by blast ``` hoelzl@40703 ` 184` hoelzl@40703 ` 185` ```lemma inj_on_INTER: ``` hoelzl@40703 ` 186` ``` "\I \ {}; \ i. i \ I \ inj_on f (A i)\ \ inj_on f (\ i \ I. A i)" ``` hoelzl@40703 ` 187` ```unfolding inj_on_def by blast ``` hoelzl@40703 ` 188` hoelzl@40703 ` 189` ```lemma inj_on_Inter: ``` hoelzl@40703 ` 190` ``` "\S \ {}; \ A. A \ S \ inj_on f A\ \ inj_on f (Inter S)" ``` hoelzl@40703 ` 191` ```unfolding inj_on_def by blast ``` hoelzl@40703 ` 192` hoelzl@40703 ` 193` ```lemma inj_on_UNION_chain: ``` hoelzl@40703 ` 194` ``` assumes CH: "\ i j. \i \ I; j \ I\ \ A i \ A j \ A j \ A i" and ``` hoelzl@40703 ` 195` ``` INJ: "\ i. i \ I \ inj_on f (A i)" ``` hoelzl@40703 ` 196` ``` shows "inj_on f (\ i \ I. A i)" ``` haftmann@49905 ` 197` ```proof - ``` haftmann@49905 ` 198` ``` { ``` haftmann@49905 ` 199` ``` fix i j x y ``` haftmann@49905 ` 200` ``` assume *: "i \ I" "j \ I" and **: "x \ A i" "y \ A j" ``` haftmann@49905 ` 201` ``` and ***: "f x = f y" ``` haftmann@49905 ` 202` ``` have "x = y" ``` haftmann@49905 ` 203` ``` proof - ``` haftmann@49905 ` 204` ``` { ``` haftmann@49905 ` 205` ``` assume "A i \ A j" ``` haftmann@49905 ` 206` ``` with ** have "x \ A j" by auto ``` haftmann@49905 ` 207` ``` with INJ * ** *** have ?thesis ``` haftmann@49905 ` 208` ``` by(auto simp add: inj_on_def) ``` haftmann@49905 ` 209` ``` } ``` haftmann@49905 ` 210` ``` moreover ``` haftmann@49905 ` 211` ``` { ``` haftmann@49905 ` 212` ``` assume "A j \ A i" ``` haftmann@49905 ` 213` ``` with ** have "y \ A i" by auto ``` haftmann@49905 ` 214` ``` with INJ * ** *** have ?thesis ``` haftmann@49905 ` 215` ``` by(auto simp add: inj_on_def) ``` haftmann@49905 ` 216` ``` } ``` haftmann@49905 ` 217` ``` ultimately show ?thesis using CH * by blast ``` haftmann@49905 ` 218` ``` qed ``` haftmann@49905 ` 219` ``` } ``` haftmann@49905 ` 220` ``` then show ?thesis by (unfold inj_on_def UNION_eq) auto ``` hoelzl@40703 ` 221` ```qed ``` hoelzl@40703 ` 222` hoelzl@40702 ` 223` ```lemma surj_id: "surj id" ``` hoelzl@40702 ` 224` ```by simp ``` haftmann@26147 ` 225` hoelzl@39101 ` 226` ```lemma bij_id[simp]: "bij id" ``` hoelzl@39076 ` 227` ```by (simp add: bij_betw_def) ``` paulson@13585 ` 228` paulson@13585 ` 229` ```lemma inj_onI: ``` paulson@13585 ` 230` ``` "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A" ``` paulson@13585 ` 231` ```by (simp add: inj_on_def) ``` paulson@13585 ` 232` paulson@13585 ` 233` ```lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A" ``` paulson@13585 ` 234` ```by (auto dest: arg_cong [of concl: g] simp add: inj_on_def) ``` paulson@13585 ` 235` paulson@13585 ` 236` ```lemma inj_onD: "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y" ``` paulson@13585 ` 237` ```by (unfold inj_on_def, blast) ``` paulson@13585 ` 238` paulson@13585 ` 239` ```lemma inj_on_iff: "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)" ``` paulson@13585 ` 240` ```by (blast dest!: inj_onD) ``` paulson@13585 ` 241` paulson@13585 ` 242` ```lemma comp_inj_on: ``` paulson@13585 ` 243` ``` "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A" ``` paulson@13585 ` 244` ```by (simp add: comp_def inj_on_def) ``` paulson@13585 ` 245` nipkow@15303 ` 246` ```lemma inj_on_imageI: "inj_on (g o f) A \ inj_on g (f ` A)" ``` nipkow@15303 ` 247` ```apply(simp add:inj_on_def image_def) ``` nipkow@15303 ` 248` ```apply blast ``` nipkow@15303 ` 249` ```done ``` nipkow@15303 ` 250` nipkow@15439 ` 251` ```lemma inj_on_image_iff: "\ ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y); ``` nipkow@15439 ` 252` ``` inj_on f A \ \ inj_on g (f ` A) = inj_on g A" ``` nipkow@15439 ` 253` ```apply(unfold inj_on_def) ``` nipkow@15439 ` 254` ```apply blast ``` nipkow@15439 ` 255` ```done ``` nipkow@15439 ` 256` paulson@13585 ` 257` ```lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)" ``` paulson@13585 ` 258` ```by (unfold inj_on_def, blast) ``` wenzelm@12258 ` 259` paulson@13585 ` 260` ```lemma inj_singleton: "inj (%s. {s})" ``` paulson@13585 ` 261` ```by (simp add: inj_on_def) ``` paulson@13585 ` 262` nipkow@15111 ` 263` ```lemma inj_on_empty[iff]: "inj_on f {}" ``` nipkow@15111 ` 264` ```by(simp add: inj_on_def) ``` nipkow@15111 ` 265` nipkow@15303 ` 266` ```lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A" ``` paulson@13585 ` 267` ```by (unfold inj_on_def, blast) ``` paulson@13585 ` 268` nipkow@15111 ` 269` ```lemma inj_on_Un: ``` nipkow@15111 ` 270` ``` "inj_on f (A Un B) = ``` nipkow@15111 ` 271` ``` (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})" ``` nipkow@15111 ` 272` ```apply(unfold inj_on_def) ``` nipkow@15111 ` 273` ```apply (blast intro:sym) ``` nipkow@15111 ` 274` ```done ``` nipkow@15111 ` 275` nipkow@15111 ` 276` ```lemma inj_on_insert[iff]: ``` nipkow@15111 ` 277` ``` "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))" ``` nipkow@15111 ` 278` ```apply(unfold inj_on_def) ``` nipkow@15111 ` 279` ```apply (blast intro:sym) ``` nipkow@15111 ` 280` ```done ``` nipkow@15111 ` 281` nipkow@15111 ` 282` ```lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)" ``` nipkow@15111 ` 283` ```apply(unfold inj_on_def) ``` nipkow@15111 ` 284` ```apply (blast) ``` nipkow@15111 ` 285` ```done ``` nipkow@15111 ` 286` hoelzl@40703 ` 287` ```lemma comp_inj_on_iff: ``` hoelzl@40703 ` 288` ``` "inj_on f A \ inj_on f' (f ` A) \ inj_on (f' o f) A" ``` hoelzl@40703 ` 289` ```by(auto simp add: comp_inj_on inj_on_def) ``` hoelzl@40703 ` 290` hoelzl@40703 ` 291` ```lemma inj_on_imageI2: ``` hoelzl@40703 ` 292` ``` "inj_on (f' o f) A \ inj_on f A" ``` hoelzl@40703 ` 293` ```by(auto simp add: comp_inj_on inj_on_def) ``` hoelzl@40703 ` 294` haftmann@51598 ` 295` ```lemma inj_img_insertE: ``` haftmann@51598 ` 296` ``` assumes "inj_on f A" ``` haftmann@51598 ` 297` ``` assumes "x \ B" and "insert x B = f ` A" ``` haftmann@51598 ` 298` ``` obtains x' A' where "x' \ A'" and "A = insert x' A'" ``` haftmann@51598 ` 299` ``` and "x = f x'" and "B = f ` A'" ``` haftmann@51598 ` 300` ```proof - ``` haftmann@51598 ` 301` ``` from assms have "x \ f ` A" by auto ``` haftmann@51598 ` 302` ``` then obtain x' where *: "x' \ A" "x = f x'" by auto ``` haftmann@51598 ` 303` ``` then have "A = insert x' (A - {x'})" by auto ``` haftmann@51598 ` 304` ``` with assms * have "B = f ` (A - {x'})" ``` haftmann@51598 ` 305` ``` by (auto dest: inj_on_contraD) ``` haftmann@51598 ` 306` ``` have "x' \ A - {x'}" by simp ``` haftmann@51598 ` 307` ``` from `x' \ A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})` ``` haftmann@51598 ` 308` ``` show ?thesis .. ``` haftmann@51598 ` 309` ```qed ``` haftmann@51598 ` 310` traytel@54578 ` 311` ```lemma linorder_injI: ``` traytel@54578 ` 312` ``` assumes hyp: "\x y. x < (y::'a::linorder) \ f x \ f y" ``` traytel@54578 ` 313` ``` shows "inj f" ``` traytel@54578 ` 314` ``` -- {* Courtesy of Stephan Merz *} ``` traytel@54578 ` 315` ```proof (rule inj_onI) ``` traytel@54578 ` 316` ``` fix x y ``` traytel@54578 ` 317` ``` assume f_eq: "f x = f y" ``` traytel@54578 ` 318` ``` show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq) ``` traytel@54578 ` 319` ```qed ``` traytel@54578 ` 320` hoelzl@40702 ` 321` ```lemma surj_def: "surj f \ (\y. \x. y = f x)" ``` hoelzl@40702 ` 322` ``` by auto ``` hoelzl@39076 ` 323` hoelzl@40702 ` 324` ```lemma surjI: assumes *: "\ x. g (f x) = x" shows "surj g" ``` hoelzl@40702 ` 325` ``` using *[symmetric] by auto ``` paulson@13585 ` 326` hoelzl@39076 ` 327` ```lemma surjD: "surj f \ \x. y = f x" ``` hoelzl@39076 ` 328` ``` by (simp add: surj_def) ``` paulson@13585 ` 329` hoelzl@39076 ` 330` ```lemma surjE: "surj f \ (\x. y = f x \ C) \ C" ``` hoelzl@39076 ` 331` ``` by (simp add: surj_def, blast) ``` paulson@13585 ` 332` paulson@13585 ` 333` ```lemma comp_surj: "[| surj f; surj g |] ==> surj (g o f)" ``` paulson@13585 ` 334` ```apply (simp add: comp_def surj_def, clarify) ``` paulson@13585 ` 335` ```apply (drule_tac x = y in spec, clarify) ``` paulson@13585 ` 336` ```apply (drule_tac x = x in spec, blast) ``` paulson@13585 ` 337` ```done ``` paulson@13585 ` 338` hoelzl@39074 ` 339` ```lemma bij_betw_imp_surj: "bij_betw f A UNIV \ surj f" ``` hoelzl@40702 ` 340` ``` unfolding bij_betw_def by auto ``` hoelzl@39074 ` 341` hoelzl@40703 ` 342` ```lemma bij_betw_empty1: ``` hoelzl@40703 ` 343` ``` assumes "bij_betw f {} A" ``` hoelzl@40703 ` 344` ``` shows "A = {}" ``` hoelzl@40703 ` 345` ```using assms unfolding bij_betw_def by blast ``` hoelzl@40703 ` 346` hoelzl@40703 ` 347` ```lemma bij_betw_empty2: ``` hoelzl@40703 ` 348` ``` assumes "bij_betw f A {}" ``` hoelzl@40703 ` 349` ``` shows "A = {}" ``` hoelzl@40703 ` 350` ```using assms unfolding bij_betw_def by blast ``` hoelzl@40703 ` 351` hoelzl@40703 ` 352` ```lemma inj_on_imp_bij_betw: ``` hoelzl@40703 ` 353` ``` "inj_on f A \ bij_betw f A (f ` A)" ``` hoelzl@40703 ` 354` ```unfolding bij_betw_def by simp ``` hoelzl@40703 ` 355` hoelzl@39076 ` 356` ```lemma bij_def: "bij f \ inj f \ surj f" ``` hoelzl@40702 ` 357` ``` unfolding bij_betw_def .. ``` hoelzl@39074 ` 358` paulson@13585 ` 359` ```lemma bijI: "[| inj f; surj f |] ==> bij f" ``` paulson@13585 ` 360` ```by (simp add: bij_def) ``` paulson@13585 ` 361` paulson@13585 ` 362` ```lemma bij_is_inj: "bij f ==> inj f" ``` paulson@13585 ` 363` ```by (simp add: bij_def) ``` paulson@13585 ` 364` paulson@13585 ` 365` ```lemma bij_is_surj: "bij f ==> surj f" ``` paulson@13585 ` 366` ```by (simp add: bij_def) ``` paulson@13585 ` 367` nipkow@26105 ` 368` ```lemma bij_betw_imp_inj_on: "bij_betw f A B \ inj_on f A" ``` nipkow@26105 ` 369` ```by (simp add: bij_betw_def) ``` nipkow@26105 ` 370` nipkow@31438 ` 371` ```lemma bij_betw_trans: ``` nipkow@31438 ` 372` ``` "bij_betw f A B \ bij_betw g B C \ bij_betw (g o f) A C" ``` nipkow@31438 ` 373` ```by(auto simp add:bij_betw_def comp_inj_on) ``` nipkow@31438 ` 374` hoelzl@40702 ` 375` ```lemma bij_comp: "bij f \ bij g \ bij (g o f)" ``` hoelzl@40702 ` 376` ``` by (rule bij_betw_trans) ``` hoelzl@40702 ` 377` hoelzl@40703 ` 378` ```lemma bij_betw_comp_iff: ``` hoelzl@40703 ` 379` ``` "bij_betw f A A' \ bij_betw f' A' A'' \ bij_betw (f' o f) A A''" ``` hoelzl@40703 ` 380` ```by(auto simp add: bij_betw_def inj_on_def) ``` hoelzl@40703 ` 381` hoelzl@40703 ` 382` ```lemma bij_betw_comp_iff2: ``` hoelzl@40703 ` 383` ``` assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \ A'" ``` hoelzl@40703 ` 384` ``` shows "bij_betw f A A' \ bij_betw (f' o f) A A''" ``` hoelzl@40703 ` 385` ```using assms ``` hoelzl@40703 ` 386` ```proof(auto simp add: bij_betw_comp_iff) ``` hoelzl@40703 ` 387` ``` assume *: "bij_betw (f' \ f) A A''" ``` hoelzl@40703 ` 388` ``` thus "bij_betw f A A'" ``` hoelzl@40703 ` 389` ``` using IM ``` hoelzl@40703 ` 390` ``` proof(auto simp add: bij_betw_def) ``` hoelzl@40703 ` 391` ``` assume "inj_on (f' \ f) A" ``` hoelzl@40703 ` 392` ``` thus "inj_on f A" using inj_on_imageI2 by blast ``` hoelzl@40703 ` 393` ``` next ``` hoelzl@40703 ` 394` ``` fix a' assume **: "a' \ A'" ``` hoelzl@40703 ` 395` ``` hence "f' a' \ A''" using BIJ unfolding bij_betw_def by auto ``` hoelzl@40703 ` 396` ``` then obtain a where 1: "a \ A \ f'(f a) = f' a'" using * ``` hoelzl@40703 ` 397` ``` unfolding bij_betw_def by force ``` hoelzl@40703 ` 398` ``` hence "f a \ A'" using IM by auto ``` hoelzl@40703 ` 399` ``` hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto ``` hoelzl@40703 ` 400` ``` thus "a' \ f ` A" using 1 by auto ``` hoelzl@40703 ` 401` ``` qed ``` hoelzl@40703 ` 402` ```qed ``` hoelzl@40703 ` 403` nipkow@26105 ` 404` ```lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A" ``` nipkow@26105 ` 405` ```proof - ``` nipkow@26105 ` 406` ``` have i: "inj_on f A" and s: "f ` A = B" ``` nipkow@26105 ` 407` ``` using assms by(auto simp:bij_betw_def) ``` nipkow@26105 ` 408` ``` let ?P = "%b a. a:A \ f a = b" let ?g = "%b. The (?P b)" ``` nipkow@26105 ` 409` ``` { fix a b assume P: "?P b a" ``` nipkow@26105 ` 410` ``` hence ex1: "\a. ?P b a" using s unfolding image_def by blast ``` nipkow@26105 ` 411` ``` hence uex1: "\!a. ?P b a" by(blast dest:inj_onD[OF i]) ``` nipkow@26105 ` 412` ``` hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp ``` nipkow@26105 ` 413` ``` } note g = this ``` nipkow@26105 ` 414` ``` have "inj_on ?g B" ``` nipkow@26105 ` 415` ``` proof(rule inj_onI) ``` nipkow@26105 ` 416` ``` fix x y assume "x:B" "y:B" "?g x = ?g y" ``` nipkow@26105 ` 417` ``` from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast ``` nipkow@26105 ` 418` ``` from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast ``` nipkow@26105 ` 419` ``` from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp ``` nipkow@26105 ` 420` ``` qed ``` nipkow@26105 ` 421` ``` moreover have "?g ` B = A" ``` nipkow@26105 ` 422` ``` proof(auto simp:image_def) ``` nipkow@26105 ` 423` ``` fix b assume "b:B" ``` nipkow@26105 ` 424` ``` with s obtain a where P: "?P b a" unfolding image_def by blast ``` nipkow@26105 ` 425` ``` thus "?g b \ A" using g[OF P] by auto ``` nipkow@26105 ` 426` ``` next ``` nipkow@26105 ` 427` ``` fix a assume "a:A" ``` nipkow@26105 ` 428` ``` then obtain b where P: "?P b a" using s unfolding image_def by blast ``` nipkow@26105 ` 429` ``` then have "b:B" using s unfolding image_def by blast ``` nipkow@26105 ` 430` ``` with g[OF P] show "\b\B. a = ?g b" by blast ``` nipkow@26105 ` 431` ``` qed ``` nipkow@26105 ` 432` ``` ultimately show ?thesis by(auto simp:bij_betw_def) ``` nipkow@26105 ` 433` ```qed ``` nipkow@26105 ` 434` hoelzl@40703 ` 435` ```lemma bij_betw_cong: ``` hoelzl@40703 ` 436` ``` "(\ a. a \ A \ f a = g a) \ bij_betw f A A' = bij_betw g A A'" ``` hoelzl@40703 ` 437` ```unfolding bij_betw_def inj_on_def by force ``` hoelzl@40703 ` 438` hoelzl@40703 ` 439` ```lemma bij_betw_id[intro, simp]: ``` hoelzl@40703 ` 440` ``` "bij_betw id A A" ``` hoelzl@40703 ` 441` ```unfolding bij_betw_def id_def by auto ``` hoelzl@40703 ` 442` hoelzl@40703 ` 443` ```lemma bij_betw_id_iff: ``` hoelzl@40703 ` 444` ``` "bij_betw id A B \ A = B" ``` hoelzl@40703 ` 445` ```by(auto simp add: bij_betw_def) ``` hoelzl@40703 ` 446` hoelzl@39075 ` 447` ```lemma bij_betw_combine: ``` hoelzl@39075 ` 448` ``` assumes "bij_betw f A B" "bij_betw f C D" "B \ D = {}" ``` hoelzl@39075 ` 449` ``` shows "bij_betw f (A \ C) (B \ D)" ``` hoelzl@39075 ` 450` ``` using assms unfolding bij_betw_def inj_on_Un image_Un by auto ``` hoelzl@39075 ` 451` hoelzl@40703 ` 452` ```lemma bij_betw_UNION_chain: ``` hoelzl@40703 ` 453` ``` assumes CH: "\ i j. \i \ I; j \ I\ \ A i \ A j \ A j \ A i" and ``` hoelzl@40703 ` 454` ``` BIJ: "\ i. i \ I \ bij_betw f (A i) (A' i)" ``` hoelzl@40703 ` 455` ``` shows "bij_betw f (\ i \ I. A i) (\ i \ I. A' i)" ``` haftmann@49905 ` 456` ```proof (unfold bij_betw_def, auto) ``` hoelzl@40703 ` 457` ``` have "\ i. i \ I \ inj_on f (A i)" ``` hoelzl@40703 ` 458` ``` using BIJ bij_betw_def[of f] by auto ``` hoelzl@40703 ` 459` ``` thus "inj_on f (\ i \ I. A i)" ``` hoelzl@40703 ` 460` ``` using CH inj_on_UNION_chain[of I A f] by auto ``` hoelzl@40703 ` 461` ```next ``` hoelzl@40703 ` 462` ``` fix i x ``` hoelzl@40703 ` 463` ``` assume *: "i \ I" "x \ A i" ``` hoelzl@40703 ` 464` ``` hence "f x \ A' i" using BIJ bij_betw_def[of f] by auto ``` hoelzl@40703 ` 465` ``` thus "\j \ I. f x \ A' j" using * by blast ``` hoelzl@40703 ` 466` ```next ``` hoelzl@40703 ` 467` ``` fix i x' ``` hoelzl@40703 ` 468` ``` assume *: "i \ I" "x' \ A' i" ``` hoelzl@40703 ` 469` ``` hence "\x \ A i. x' = f x" using BIJ bij_betw_def[of f] by blast ``` haftmann@49905 ` 470` ``` then have "\j \ I. \x \ A j. x' = f x" ``` haftmann@49905 ` 471` ``` using * by blast ``` haftmann@49905 ` 472` ``` then show "x' \ f ` (\x\I. A x)" by (simp add: image_def) ``` hoelzl@40703 ` 473` ```qed ``` hoelzl@40703 ` 474` hoelzl@40703 ` 475` ```lemma bij_betw_subset: ``` hoelzl@40703 ` 476` ``` assumes BIJ: "bij_betw f A A'" and ``` hoelzl@40703 ` 477` ``` SUB: "B \ A" and IM: "f ` B = B'" ``` hoelzl@40703 ` 478` ``` shows "bij_betw f B B'" ``` hoelzl@40703 ` 479` ```using assms ``` hoelzl@40703 ` 480` ```by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def) ``` hoelzl@40703 ` 481` paulson@13585 ` 482` ```lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A" ``` hoelzl@40702 ` 483` ```by simp ``` paulson@13585 ` 484` hoelzl@42903 ` 485` ```lemma surj_vimage_empty: ``` hoelzl@42903 ` 486` ``` assumes "surj f" shows "f -` A = {} \ A = {}" ``` hoelzl@42903 ` 487` ``` using surj_image_vimage_eq[OF `surj f`, of A] ``` nipkow@44890 ` 488` ``` by (intro iffI) fastforce+ ``` hoelzl@42903 ` 489` paulson@13585 ` 490` ```lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A" ``` paulson@13585 ` 491` ```by (simp add: inj_on_def, blast) ``` paulson@13585 ` 492` paulson@13585 ` 493` ```lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A" ``` hoelzl@40702 ` 494` ```by (blast intro: sym) ``` paulson@13585 ` 495` paulson@13585 ` 496` ```lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A" ``` paulson@13585 ` 497` ```by (unfold inj_on_def, blast) ``` paulson@13585 ` 498` paulson@13585 ` 499` ```lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)" ``` paulson@13585 ` 500` ```apply (unfold bij_def) ``` paulson@13585 ` 501` ```apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD) ``` paulson@13585 ` 502` ```done ``` paulson@13585 ` 503` Andreas@53927 ` 504` ```lemma inj_on_image_eq_iff: "\ inj_on f C; A \ C; B \ C \ \ f ` A = f ` B \ A = B" ``` Andreas@53927 ` 505` ```by(fastforce simp add: inj_on_def) ``` Andreas@53927 ` 506` nipkow@31438 ` 507` ```lemma inj_on_Un_image_eq_iff: "inj_on f (A \ B) \ f ` A = f ` B \ A = B" ``` Andreas@53927 ` 508` ```by(erule inj_on_image_eq_iff) simp_all ``` nipkow@31438 ` 509` paulson@13585 ` 510` ```lemma inj_on_image_Int: ``` paulson@13585 ` 511` ``` "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B" ``` paulson@13585 ` 512` ```apply (simp add: inj_on_def, blast) ``` paulson@13585 ` 513` ```done ``` paulson@13585 ` 514` paulson@13585 ` 515` ```lemma inj_on_image_set_diff: ``` paulson@13585 ` 516` ``` "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B" ``` paulson@13585 ` 517` ```apply (simp add: inj_on_def, blast) ``` paulson@13585 ` 518` ```done ``` paulson@13585 ` 519` paulson@13585 ` 520` ```lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B" ``` paulson@13585 ` 521` ```by (simp add: inj_on_def, blast) ``` paulson@13585 ` 522` paulson@13585 ` 523` ```lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B" ``` paulson@13585 ` 524` ```by (simp add: inj_on_def, blast) ``` paulson@13585 ` 525` paulson@13585 ` 526` ```lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)" ``` paulson@13585 ` 527` ```by (blast dest: injD) ``` paulson@13585 ` 528` paulson@13585 ` 529` ```lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)" ``` paulson@13585 ` 530` ```by (simp add: inj_on_def, blast) ``` paulson@13585 ` 531` paulson@13585 ` 532` ```lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)" ``` paulson@13585 ` 533` ```by (blast dest: injD) ``` paulson@13585 ` 534` paulson@13585 ` 535` ```(*injectivity's required. Left-to-right inclusion holds even if A is empty*) ``` paulson@13585 ` 536` ```lemma image_INT: ``` paulson@13585 ` 537` ``` "[| inj_on f C; ALL x:A. B x <= C; j:A |] ``` paulson@13585 ` 538` ``` ==> f ` (INTER A B) = (INT x:A. f ` B x)" ``` paulson@13585 ` 539` ```apply (simp add: inj_on_def, blast) ``` paulson@13585 ` 540` ```done ``` paulson@13585 ` 541` paulson@13585 ` 542` ```(*Compare with image_INT: no use of inj_on, and if f is surjective then ``` paulson@13585 ` 543` ``` it doesn't matter whether A is empty*) ``` paulson@13585 ` 544` ```lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)" ``` paulson@13585 ` 545` ```apply (simp add: bij_def) ``` paulson@13585 ` 546` ```apply (simp add: inj_on_def surj_def, blast) ``` paulson@13585 ` 547` ```done ``` paulson@13585 ` 548` paulson@13585 ` 549` ```lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)" ``` hoelzl@40702 ` 550` ```by auto ``` paulson@13585 ` 551` paulson@13585 ` 552` ```lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)" ``` paulson@13585 ` 553` ```by (auto simp add: inj_on_def) ``` paulson@5852 ` 554` paulson@13585 ` 555` ```lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)" ``` paulson@13585 ` 556` ```apply (simp add: bij_def) ``` paulson@13585 ` 557` ```apply (rule equalityI) ``` paulson@13585 ` 558` ```apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset) ``` paulson@13585 ` 559` ```done ``` paulson@13585 ` 560` haftmann@41657 ` 561` ```lemma inj_vimage_singleton: "inj f \ f -` {a} \ {THE x. f x = a}" ``` haftmann@41657 ` 562` ``` -- {* The inverse image of a singleton under an injective function ``` haftmann@41657 ` 563` ``` is included in a singleton. *} ``` haftmann@41657 ` 564` ``` apply (auto simp add: inj_on_def) ``` haftmann@41657 ` 565` ``` apply (blast intro: the_equality [symmetric]) ``` haftmann@41657 ` 566` ``` done ``` haftmann@41657 ` 567` hoelzl@43991 ` 568` ```lemma inj_on_vimage_singleton: ``` hoelzl@43991 ` 569` ``` "inj_on f A \ f -` {a} \ A \ {THE x. x \ A \ f x = a}" ``` hoelzl@43991 ` 570` ``` by (auto simp add: inj_on_def intro: the_equality [symmetric]) ``` hoelzl@43991 ` 571` hoelzl@35584 ` 572` ```lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A" ``` hoelzl@35580 ` 573` ``` by (auto intro!: inj_onI) ``` paulson@13585 ` 574` hoelzl@35584 ` 575` ```lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \ inj_on f A" ``` hoelzl@35584 ` 576` ``` by (auto intro!: inj_onI dest: strict_mono_eq) ``` hoelzl@35584 ` 577` haftmann@41657 ` 578` paulson@13585 ` 579` ```subsection{*Function Updating*} ``` paulson@13585 ` 580` haftmann@44277 ` 581` ```definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where ``` haftmann@26147 ` 582` ``` "fun_upd f a b == % x. if x=a then b else f x" ``` haftmann@26147 ` 583` wenzelm@41229 ` 584` ```nonterminal updbinds and updbind ``` wenzelm@41229 ` 585` haftmann@26147 ` 586` ```syntax ``` haftmann@26147 ` 587` ``` "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)") ``` haftmann@26147 ` 588` ``` "" :: "updbind => updbinds" ("_") ``` haftmann@26147 ` 589` ``` "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _") ``` wenzelm@35115 ` 590` ``` "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000, 0] 900) ``` haftmann@26147 ` 591` haftmann@26147 ` 592` ```translations ``` wenzelm@35115 ` 593` ``` "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" ``` wenzelm@35115 ` 594` ``` "f(x:=y)" == "CONST fun_upd f x y" ``` haftmann@26147 ` 595` haftmann@26147 ` 596` ```(* Hint: to define the sum of two functions (or maps), use sum_case. ``` haftmann@26147 ` 597` ``` A nice infix syntax could be defined (in Datatype.thy or below) by ``` wenzelm@35115 ` 598` ```notation ``` wenzelm@35115 ` 599` ``` sum_case (infixr "'(+')"80) ``` haftmann@26147 ` 600` ```*) ``` haftmann@26147 ` 601` paulson@13585 ` 602` ```lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)" ``` paulson@13585 ` 603` ```apply (simp add: fun_upd_def, safe) ``` paulson@13585 ` 604` ```apply (erule subst) ``` paulson@13585 ` 605` ```apply (rule_tac [2] ext, auto) ``` paulson@13585 ` 606` ```done ``` paulson@13585 ` 607` wenzelm@45603 ` 608` ```lemma fun_upd_idem: "f x = y ==> f(x:=y) = f" ``` wenzelm@45603 ` 609` ``` by (simp only: fun_upd_idem_iff) ``` paulson@13585 ` 610` wenzelm@45603 ` 611` ```lemma fun_upd_triv [iff]: "f(x := f x) = f" ``` wenzelm@45603 ` 612` ``` by (simp only: fun_upd_idem) ``` paulson@13585 ` 613` paulson@13585 ` 614` ```lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)" ``` paulson@17084 ` 615` ```by (simp add: fun_upd_def) ``` paulson@13585 ` 616` paulson@13585 ` 617` ```(* fun_upd_apply supersedes these two, but they are useful ``` paulson@13585 ` 618` ``` if fun_upd_apply is intentionally removed from the simpset *) ``` paulson@13585 ` 619` ```lemma fun_upd_same: "(f(x:=y)) x = y" ``` paulson@13585 ` 620` ```by simp ``` paulson@13585 ` 621` paulson@13585 ` 622` ```lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z" ``` paulson@13585 ` 623` ```by simp ``` paulson@13585 ` 624` paulson@13585 ` 625` ```lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)" ``` nipkow@39302 ` 626` ```by (simp add: fun_eq_iff) ``` paulson@13585 ` 627` paulson@13585 ` 628` ```lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)" ``` paulson@13585 ` 629` ```by (rule ext, auto) ``` paulson@13585 ` 630` nipkow@15303 ` 631` ```lemma inj_on_fun_updI: "\ inj_on f A; y \ f`A \ \ inj_on (f(x:=y)) A" ``` nipkow@44890 ` 632` ```by (fastforce simp:inj_on_def image_def) ``` nipkow@15303 ` 633` paulson@15510 ` 634` ```lemma fun_upd_image: ``` paulson@15510 ` 635` ``` "f(x:=y) ` A = (if x \ A then insert y (f ` (A-{x})) else f ` A)" ``` paulson@15510 ` 636` ```by auto ``` paulson@15510 ` 637` nipkow@31080 ` 638` ```lemma fun_upd_comp: "f \ (g(x := y)) = (f \ g)(x := f y)" ``` huffman@44921 ` 639` ``` by auto ``` nipkow@31080 ` 640` nipkow@44744 ` 641` ```lemma UNION_fun_upd: ``` nipkow@44744 ` 642` ``` "UNION J (A(i:=B)) = (UNION (J-{i}) A \ (if i\J then B else {}))" ``` nipkow@44744 ` 643` ```by (auto split: if_splits) ``` nipkow@44744 ` 644` haftmann@26147 ` 645` haftmann@26147 ` 646` ```subsection {* @{text override_on} *} ``` haftmann@26147 ` 647` haftmann@44277 ` 648` ```definition override_on :: "('a \ 'b) \ ('a \ 'b) \ 'a set \ 'a \ 'b" where ``` haftmann@26147 ` 649` ``` "override_on f g A = (\a. if a \ A then g a else f a)" ``` nipkow@13910 ` 650` nipkow@15691 ` 651` ```lemma override_on_emptyset[simp]: "override_on f g {} = f" ``` nipkow@15691 ` 652` ```by(simp add:override_on_def) ``` nipkow@13910 ` 653` nipkow@15691 ` 654` ```lemma override_on_apply_notin[simp]: "a ~: A ==> (override_on f g A) a = f a" ``` nipkow@15691 ` 655` ```by(simp add:override_on_def) ``` nipkow@13910 ` 656` nipkow@15691 ` 657` ```lemma override_on_apply_in[simp]: "a : A ==> (override_on f g A) a = g a" ``` nipkow@15691 ` 658` ```by(simp add:override_on_def) ``` nipkow@13910 ` 659` haftmann@26147 ` 660` haftmann@26147 ` 661` ```subsection {* @{text swap} *} ``` paulson@15510 ` 662` haftmann@44277 ` 663` ```definition swap :: "'a \ 'a \ ('a \ 'b) \ ('a \ 'b)" where ``` haftmann@22744 ` 664` ``` "swap a b f = f (a := f b, b:= f a)" ``` paulson@15510 ` 665` huffman@34101 ` 666` ```lemma swap_self [simp]: "swap a a f = f" ``` nipkow@15691 ` 667` ```by (simp add: swap_def) ``` paulson@15510 ` 668` paulson@15510 ` 669` ```lemma swap_commute: "swap a b f = swap b a f" ``` paulson@15510 ` 670` ```by (rule ext, simp add: fun_upd_def swap_def) ``` paulson@15510 ` 671` paulson@15510 ` 672` ```lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" ``` paulson@15510 ` 673` ```by (rule ext, simp add: fun_upd_def swap_def) ``` paulson@15510 ` 674` huffman@34145 ` 675` ```lemma swap_triple: ``` huffman@34145 ` 676` ``` assumes "a \ c" and "b \ c" ``` huffman@34145 ` 677` ``` shows "swap a b (swap b c (swap a b f)) = swap a c f" ``` nipkow@39302 ` 678` ``` using assms by (simp add: fun_eq_iff swap_def) ``` huffman@34145 ` 679` huffman@34101 ` 680` ```lemma comp_swap: "f \ swap a b g = swap a b (f \ g)" ``` huffman@34101 ` 681` ```by (rule ext, simp add: fun_upd_def swap_def) ``` huffman@34101 ` 682` hoelzl@39076 ` 683` ```lemma swap_image_eq [simp]: ``` hoelzl@39076 ` 684` ``` assumes "a \ A" "b \ A" shows "swap a b f ` A = f ` A" ``` hoelzl@39076 ` 685` ```proof - ``` hoelzl@39076 ` 686` ``` have subset: "\f. swap a b f ` A \ f ` A" ``` hoelzl@39076 ` 687` ``` using assms by (auto simp: image_iff swap_def) ``` hoelzl@39076 ` 688` ``` then have "swap a b (swap a b f) ` A \ (swap a b f) ` A" . ``` hoelzl@39076 ` 689` ``` with subset[of f] show ?thesis by auto ``` hoelzl@39076 ` 690` ```qed ``` hoelzl@39076 ` 691` paulson@15510 ` 692` ```lemma inj_on_imp_inj_on_swap: ``` hoelzl@39076 ` 693` ``` "\inj_on f A; a \ A; b \ A\ \ inj_on (swap a b f) A" ``` hoelzl@39076 ` 694` ``` by (simp add: inj_on_def swap_def, blast) ``` paulson@15510 ` 695` paulson@15510 ` 696` ```lemma inj_on_swap_iff [simp]: ``` hoelzl@39076 ` 697` ``` assumes A: "a \ A" "b \ A" shows "inj_on (swap a b f) A \ inj_on f A" ``` hoelzl@39075 ` 698` ```proof ``` paulson@15510 ` 699` ``` assume "inj_on (swap a b f) A" ``` hoelzl@39075 ` 700` ``` with A have "inj_on (swap a b (swap a b f)) A" ``` hoelzl@39075 ` 701` ``` by (iprover intro: inj_on_imp_inj_on_swap) ``` hoelzl@39075 ` 702` ``` thus "inj_on f A" by simp ``` paulson@15510 ` 703` ```next ``` paulson@15510 ` 704` ``` assume "inj_on f A" ``` krauss@34209 ` 705` ``` with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap) ``` paulson@15510 ` 706` ```qed ``` paulson@15510 ` 707` hoelzl@39076 ` 708` ```lemma surj_imp_surj_swap: "surj f \ surj (swap a b f)" ``` hoelzl@40702 ` 709` ``` by simp ``` paulson@15510 ` 710` hoelzl@39076 ` 711` ```lemma surj_swap_iff [simp]: "surj (swap a b f) \ surj f" ``` hoelzl@40702 ` 712` ``` by simp ``` haftmann@21547 ` 713` hoelzl@39076 ` 714` ```lemma bij_betw_swap_iff [simp]: ``` hoelzl@39076 ` 715` ``` "\ x \ A; y \ A \ \ bij_betw (swap x y f) A B \ bij_betw f A B" ``` hoelzl@39076 ` 716` ``` by (auto simp: bij_betw_def) ``` hoelzl@39076 ` 717` hoelzl@39076 ` 718` ```lemma bij_swap_iff [simp]: "bij (swap a b f) \ bij f" ``` hoelzl@39076 ` 719` ``` by simp ``` hoelzl@39075 ` 720` wenzelm@36176 ` 721` ```hide_const (open) swap ``` haftmann@21547 ` 722` haftmann@31949 ` 723` ```subsection {* Inversion of injective functions *} ``` haftmann@31949 ` 724` nipkow@33057 ` 725` ```definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where ``` haftmann@44277 ` 726` ``` "the_inv_into A f == %x. THE y. y : A & f y = x" ``` nipkow@32961 ` 727` nipkow@33057 ` 728` ```lemma the_inv_into_f_f: ``` nipkow@33057 ` 729` ``` "[| inj_on f A; x : A |] ==> the_inv_into A f (f x) = x" ``` nipkow@33057 ` 730` ```apply (simp add: the_inv_into_def inj_on_def) ``` krauss@34209 ` 731` ```apply blast ``` nipkow@32961 ` 732` ```done ``` nipkow@32961 ` 733` nipkow@33057 ` 734` ```lemma f_the_inv_into_f: ``` nipkow@33057 ` 735` ``` "inj_on f A ==> y : f`A ==> f (the_inv_into A f y) = y" ``` nipkow@33057 ` 736` ```apply (simp add: the_inv_into_def) ``` nipkow@32961 ` 737` ```apply (rule the1I2) ``` nipkow@32961 ` 738` ``` apply(blast dest: inj_onD) ``` nipkow@32961 ` 739` ```apply blast ``` nipkow@32961 ` 740` ```done ``` nipkow@32961 ` 741` nipkow@33057 ` 742` ```lemma the_inv_into_into: ``` nipkow@33057 ` 743` ``` "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B" ``` nipkow@33057 ` 744` ```apply (simp add: the_inv_into_def) ``` nipkow@32961 ` 745` ```apply (rule the1I2) ``` nipkow@32961 ` 746` ``` apply(blast dest: inj_onD) ``` nipkow@32961 ` 747` ```apply blast ``` nipkow@32961 ` 748` ```done ``` nipkow@32961 ` 749` nipkow@33057 ` 750` ```lemma the_inv_into_onto[simp]: ``` nipkow@33057 ` 751` ``` "inj_on f A ==> the_inv_into A f ` (f ` A) = A" ``` nipkow@33057 ` 752` ```by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric]) ``` nipkow@32961 ` 753` nipkow@33057 ` 754` ```lemma the_inv_into_f_eq: ``` nipkow@33057 ` 755` ``` "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x" ``` nipkow@32961 ` 756` ``` apply (erule subst) ``` nipkow@33057 ` 757` ``` apply (erule the_inv_into_f_f, assumption) ``` nipkow@32961 ` 758` ``` done ``` nipkow@32961 ` 759` nipkow@33057 ` 760` ```lemma the_inv_into_comp: ``` nipkow@32961 ` 761` ``` "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==> ``` nipkow@33057 ` 762` ``` the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x" ``` nipkow@33057 ` 763` ```apply (rule the_inv_into_f_eq) ``` nipkow@32961 ` 764` ``` apply (fast intro: comp_inj_on) ``` nipkow@33057 ` 765` ``` apply (simp add: f_the_inv_into_f the_inv_into_into) ``` nipkow@33057 ` 766` ```apply (simp add: the_inv_into_into) ``` nipkow@32961 ` 767` ```done ``` nipkow@32961 ` 768` nipkow@33057 ` 769` ```lemma inj_on_the_inv_into: ``` nipkow@33057 ` 770` ``` "inj_on f A \ inj_on (the_inv_into A f) (f ` A)" ``` nipkow@33057 ` 771` ```by (auto intro: inj_onI simp: image_def the_inv_into_f_f) ``` nipkow@32961 ` 772` nipkow@33057 ` 773` ```lemma bij_betw_the_inv_into: ``` nipkow@33057 ` 774` ``` "bij_betw f A B \ bij_betw (the_inv_into A f) B A" ``` nipkow@33057 ` 775` ```by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into) ``` nipkow@32961 ` 776` berghofe@32998 ` 777` ```abbreviation the_inv :: "('a \ 'b) \ ('b \ 'a)" where ``` nipkow@33057 ` 778` ``` "the_inv f \ the_inv_into UNIV f" ``` berghofe@32998 ` 779` berghofe@32998 ` 780` ```lemma the_inv_f_f: ``` berghofe@32998 ` 781` ``` assumes "inj f" ``` berghofe@32998 ` 782` ``` shows "the_inv f (f x) = x" using assms UNIV_I ``` nipkow@33057 ` 783` ``` by (rule the_inv_into_f_f) ``` berghofe@32998 ` 784` haftmann@44277 ` 785` hoelzl@40703 ` 786` ```subsection {* Cantor's Paradox *} ``` hoelzl@40703 ` 787` blanchet@54147 ` 788` ```lemma Cantors_paradox: ``` hoelzl@40703 ` 789` ``` "\(\f. f ` A = Pow A)" ``` hoelzl@40703 ` 790` ```proof clarify ``` hoelzl@40703 ` 791` ``` fix f assume "f ` A = Pow A" hence *: "Pow A \ f ` A" by blast ``` hoelzl@40703 ` 792` ``` let ?X = "{a \ A. a \ f a}" ``` hoelzl@40703 ` 793` ``` have "?X \ Pow A" unfolding Pow_def by auto ``` hoelzl@40703 ` 794` ``` with * obtain x where "x \ A \ f x = ?X" by blast ``` hoelzl@40703 ` 795` ``` thus False by best ``` hoelzl@40703 ` 796` ```qed ``` haftmann@31949 ` 797` haftmann@40969 ` 798` ```subsection {* Setup *} ``` haftmann@40969 ` 799` haftmann@40969 ` 800` ```subsubsection {* Proof tools *} ``` haftmann@22845 ` 801` haftmann@22845 ` 802` ```text {* simplifies terms of the form ``` haftmann@22845 ` 803` ``` f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} ``` haftmann@22845 ` 804` wenzelm@24017 ` 805` ```simproc_setup fun_upd2 ("f(v := w, x := y)") = {* fn _ => ``` haftmann@22845 ` 806` ```let ``` haftmann@22845 ` 807` ``` fun gen_fun_upd NONE T _ _ = NONE ``` wenzelm@24017 ` 808` ``` | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) \$ f \$ x \$ y) ``` haftmann@22845 ` 809` ``` fun dest_fun_T1 (Type (_, T :: Ts)) = T ``` haftmann@22845 ` 810` ``` fun find_double (t as Const (@{const_name fun_upd},T) \$ f \$ x \$ y) = ``` haftmann@22845 ` 811` ``` let ``` haftmann@22845 ` 812` ``` fun find (Const (@{const_name fun_upd},T) \$ g \$ v \$ w) = ``` haftmann@22845 ` 813` ``` if v aconv x then SOME g else gen_fun_upd (find g) T v w ``` haftmann@22845 ` 814` ``` | find t = NONE ``` haftmann@22845 ` 815` ``` in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end ``` wenzelm@24017 ` 816` wenzelm@51717 ` 817` ``` val ss = simpset_of @{context} ``` wenzelm@51717 ` 818` wenzelm@51717 ` 819` ``` fun proc ctxt ct = ``` wenzelm@24017 ` 820` ``` let ``` wenzelm@24017 ` 821` ``` val t = Thm.term_of ct ``` wenzelm@24017 ` 822` ``` in ``` wenzelm@24017 ` 823` ``` case find_double t of ``` wenzelm@24017 ` 824` ``` (T, NONE) => NONE ``` wenzelm@24017 ` 825` ``` | (T, SOME rhs) => ``` wenzelm@27330 ` 826` ``` SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs)) ``` wenzelm@24017 ` 827` ``` (fn _ => ``` wenzelm@24017 ` 828` ``` rtac eq_reflection 1 THEN ``` wenzelm@24017 ` 829` ``` rtac ext 1 THEN ``` wenzelm@51717 ` 830` ``` simp_tac (put_simpset ss ctxt) 1)) ``` wenzelm@24017 ` 831` ``` end ``` wenzelm@24017 ` 832` ```in proc end ``` haftmann@22845 ` 833` ```*} ``` haftmann@22845 ` 834` haftmann@22845 ` 835` haftmann@40969 ` 836` ```subsubsection {* Functorial structure of types *} ``` haftmann@40969 ` 837` wenzelm@48891 ` 838` ```ML_file "Tools/enriched_type.ML" ``` haftmann@40969 ` 839` haftmann@47488 ` 840` ```enriched_type map_fun: map_fun ``` haftmann@47488 ` 841` ``` by (simp_all add: fun_eq_iff) ``` haftmann@47488 ` 842` haftmann@47488 ` 843` ```enriched_type vimage ``` haftmann@49739 ` 844` ``` by (simp_all add: fun_eq_iff vimage_comp) ``` haftmann@49739 ` 845` haftmann@49739 ` 846` ```text {* Legacy theorem names *} ``` haftmann@49739 ` 847` haftmann@49739 ` 848` ```lemmas o_def = comp_def ``` haftmann@49739 ` 849` ```lemmas o_apply = comp_apply ``` haftmann@49739 ` 850` ```lemmas o_assoc = comp_assoc [symmetric] ``` haftmann@49739 ` 851` ```lemmas id_o = id_comp ``` haftmann@49739 ` 852` ```lemmas o_id = comp_id ``` haftmann@49739 ` 853` ```lemmas o_eq_dest = comp_eq_dest ``` haftmann@49739 ` 854` ```lemmas o_eq_elim = comp_eq_elim ``` haftmann@49739 ` 855` ```lemmas image_compose = image_comp ``` haftmann@49739 ` 856` ```lemmas vimage_compose = vimage_comp ``` haftmann@47488 ` 857` nipkow@2912 ` 858` ```end ``` haftmann@47488 ` 859`