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