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