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