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