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_defn 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_compose: "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_inj_onI: 287 fixes A :: "'a::order set" 288 assumes ne: "\<And>x y. \<lbrakk>x < y; x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> f x \<noteq> f y" and lin: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> x\<le>y \<or> y\<le>x" 289 shows "inj_on f A" 290proof (rule inj_onI) 291 fix x y 292 assume eq: "f x = f y" and "x\<in>A" "y\<in>A" 293 then show "x = y" 294 using lin [of x y] ne by (force simp: dual_order.order_iff_strict) 295qed 296 297lemma linorder_injI: 298 assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y" 299 shows "inj f" 300 \<comment> \<open>Courtesy of Stephan Merz\<close> 301using assms by (auto intro: linorder_inj_onI linear) 302 303lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)" 304 unfolding Pow_def inj_on_def by blast 305 306lemma bij_betw_image_Pow: "bij_betw f A B \<Longrightarrow> bij_betw (image f) (Pow A) (Pow B)" 307 by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj) 308 309lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)" 310 by auto 311 312lemma surjI: 313 assumes "\<And>x. g (f x) = x" 314 shows "surj g" 315 using assms [symmetric] by auto 316 317lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x" 318 by (simp add: surj_def) 319 320lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C" 321 by (simp add: surj_def) blast 322 323lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)" 324 using image_comp [of g f UNIV] by simp 325 326lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B" 327 unfolding bij_betw_def by clarify 328 329lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B" 330 unfolding bij_betw_def by clarify 331 332lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f" 333 unfolding bij_betw_def by auto 334 335lemma bij_betw_empty1: "bij_betw f {} A \<Longrightarrow> A = {}" 336 unfolding bij_betw_def by blast 337 338lemma bij_betw_empty2: "bij_betw f A {} \<Longrightarrow> A = {}" 339 unfolding bij_betw_def by blast 340 341lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)" 342 unfolding bij_betw_def by simp 343 344lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B" 345 unfolding bij_betw_def by auto 346 347lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f" 348 by (rule bij_betw_def) 349 350lemma bijI: "inj f \<Longrightarrow> surj f \<Longrightarrow> bij f" 351 by (rule bij_betw_imageI) 352 353lemma bij_is_inj: "bij f \<Longrightarrow> inj f" 354 by (simp add: bij_def) 355 356lemma bij_is_surj: "bij f \<Longrightarrow> surj f" 357 by (simp add: bij_def) 358 359lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A" 360 by (simp add: bij_betw_def) 361 362lemma bij_betw_trans: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g \<circ> f) A C" 363 by (auto simp add:bij_betw_def comp_inj_on) 364 365lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g \<circ> f)" 366 by (rule bij_betw_trans) 367 368lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''" 369 by (auto simp add: bij_betw_def inj_on_def) 370 371lemma bij_betw_comp_iff2: 372 assumes bij: "bij_betw f' A' A''" 373 and img: "f ` A \<le> A'" 374 shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''" 375 using assms 376proof (auto simp add: bij_betw_comp_iff) 377 assume *: "bij_betw (f' \<circ> f) A A''" 378 then show "bij_betw f A A'" 379 using img 380 proof (auto simp add: bij_betw_def) 381 assume "inj_on (f' \<circ> f) A" 382 then show "inj_on f A" 383 using inj_on_imageI2 by blast 384 next 385 fix a' 386 assume **: "a' \<in> A'" 387 with bij have "f' a' \<in> A''" 388 unfolding bij_betw_def by auto 389 with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'" 390 unfolding bij_betw_def by force 391 with img have "f a \<in> A'" by auto 392 with bij ** 1 have "f a = a'" 393 unfolding bij_betw_def inj_on_def by auto 394 with 1 show "a' \<in> f ` A" by auto 395 qed 396qed 397 398lemma bij_betw_inv: 399 assumes "bij_betw f A B" 400 shows "\<exists>g. bij_betw g B A" 401proof - 402 have i: "inj_on f A" and s: "f ` A = B" 403 using assms by (auto simp: bij_betw_def) 404 let ?P = "\<lambda>b a. a \<in> A \<and> f a = b" 405 let ?g = "\<lambda>b. The (?P b)" 406 have g: "?g b = a" if P: "?P b a" for a b 407 proof - 408 from that s have ex1: "\<exists>a. ?P b a" by blast 409 then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i]) 410 then show ?thesis 411 using the1_equality[OF uex1, OF P] P by simp 412 qed 413 have "inj_on ?g B" 414 proof (rule inj_onI) 415 fix x y 416 assume "x \<in> B" "y \<in> B" "?g x = ?g y" 417 from s \<open>x \<in> B\<close> obtain a1 where a1: "?P x a1" by blast 418 from s \<open>y \<in> B\<close> obtain a2 where a2: "?P y a2" by blast 419 from g [OF a1] a1 g [OF a2] a2 \<open>?g x = ?g y\<close> show "x = y" by simp 420 qed 421 moreover have "?g ` B = A" 422 proof (auto simp: image_def) 423 fix b 424 assume "b \<in> B" 425 with s obtain a where P: "?P b a" by blast 426 with g[OF P] show "?g b \<in> A" by auto 427 next 428 fix a 429 assume "a \<in> A" 430 with s obtain b where P: "?P b a" by blast 431 with s have "b \<in> B" by blast 432 with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast 433 qed 434 ultimately show ?thesis 435 by (auto simp: bij_betw_def) 436qed 437 438lemma bij_betw_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'" 439 unfolding bij_betw_def inj_on_def by safe force+ (* somewhat slow *) 440 441lemma bij_betw_id[intro, simp]: "bij_betw id A A" 442 unfolding bij_betw_def id_def by auto 443 444lemma bij_betw_id_iff: "bij_betw id A B \<longleftrightarrow> A = B" 445 by (auto simp add: bij_betw_def) 446 447lemma bij_betw_combine: 448 "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)" 449 unfolding bij_betw_def inj_on_Un image_Un by auto 450 451lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'" 452 by (auto simp add: bij_betw_def inj_on_def) 453 454lemma bij_pointE: 455 assumes "bij f" 456 obtains x where "y = f x" and "\<And>x'. y = f x' \<Longrightarrow> x' = x" 457proof - 458 from assms have "inj f" by (rule bij_is_inj) 459 moreover from assms have "surj f" by (rule bij_is_surj) 460 then have "y \<in> range f" by simp 461 ultimately have "\<exists>!x. y = f x" by (simp add: range_ex1_eq) 462 with that show thesis by blast 463qed 464 465lemma surj_image_vimage_eq: "surj f \<Longrightarrow> f ` (f -` A) = A" 466 by simp 467 468lemma surj_vimage_empty: 469 assumes "surj f" 470 shows "f -` A = {} \<longleftrightarrow> A = {}" 471 using surj_image_vimage_eq [OF \<open>surj f\<close>, of A] 472 by (intro iffI) fastforce+ 473 474lemma inj_vimage_image_eq: "inj f \<Longrightarrow> f -` (f ` A) = A" 475 unfolding inj_def by blast 476 477lemma vimage_subsetD: "surj f \<Longrightarrow> f -` B \<subseteq> A \<Longrightarrow> B \<subseteq> f ` A" 478 by (blast intro: sym) 479 480lemma vimage_subsetI: "inj f \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> f -` B \<subseteq> A" 481 unfolding inj_def by blast 482 483lemma vimage_subset_eq: "bij f \<Longrightarrow> f -` B \<subseteq> A \<longleftrightarrow> B \<subseteq> f ` A" 484 unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD) 485 486lemma 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" 487 by (fastforce simp: inj_on_def) 488 489lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B" 490 by (erule inj_on_image_eq_iff) simp_all 491 492lemma 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" 493 unfolding inj_on_def by blast 494 495lemma 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" 496 unfolding inj_on_def by blast 497 498lemma image_Int: "inj f \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B" 499 unfolding inj_def by blast 500 501lemma image_set_diff: "inj f \<Longrightarrow> f ` (A - B) = f ` A - f ` B" 502 unfolding inj_def by blast 503 504lemma 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" 505 by (auto simp: inj_on_def) 506 507(*FIXME DELETE*) 508lemma 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" 509 by (blast dest: inj_onD) 510 511lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A" 512 by (blast dest: injD) 513 514lemma inj_image_subset_iff: "inj f \<Longrightarrow> f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B" 515 by (blast dest: injD) 516 517lemma inj_image_eq_iff: "inj f \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B" 518 by (blast dest: injD) 519 520lemma surj_Compl_image_subset: "surj f \<Longrightarrow> - (f ` A) \<subseteq> f ` (- A)" 521 by auto 522 523lemma inj_image_Compl_subset: "inj f \<Longrightarrow> f ` (- A) \<subseteq> - (f ` A)" 524 by (auto simp: inj_def) 525 526lemma bij_image_Compl_eq: "bij f \<Longrightarrow> f ` (- A) = - (f ` A)" 527 by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI) 528 529lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}" 530 \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close> 531 by (simp add: inj_def) (blast intro: the_equality [symmetric]) 532 533lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}" 534 by (auto simp add: inj_on_def intro: the_equality [symmetric]) 535 536lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A" 537 by (auto intro!: inj_onI) 538 539lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A" 540 by (auto intro!: inj_onI dest: strict_mono_eq) 541 542lemma bij_betw_byWitness: 543 assumes left: "\<forall>a \<in> A. f' (f a) = a" 544 and right: "\<forall>a' \<in> A'. f (f' a') = a'" 545 and "f ` A \<subseteq> A'" 546 and img2: "f' ` A' \<subseteq> A" 547 shows "bij_betw f A A'" 548 using assms 549 unfolding bij_betw_def inj_on_def 550proof safe 551 fix a b 552 assume "a \<in> A" "b \<in> A" 553 with left have "a = f' (f a) \<and> b = f' (f b)" by simp 554 moreover assume "f a = f b" 555 ultimately show "a = b" by simp 556next 557 fix a' assume *: "a' \<in> A'" 558 with img2 have "f' a' \<in> A" by blast 559 moreover from * right have "a' = f (f' a')" by simp 560 ultimately show "a' \<in> f ` A" by blast 561qed 562 563corollary notIn_Un_bij_betw: 564 assumes "b \<notin> A" 565 and "f b \<notin> A'" 566 and "bij_betw f A A'" 567 shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})" 568proof - 569 have "bij_betw f {b} {f b}" 570 unfolding bij_betw_def inj_on_def by simp 571 with assms show ?thesis 572 using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast 573qed 574 575lemma notIn_Un_bij_betw3: 576 assumes "b \<notin> A" 577 and "f b \<notin> A'" 578 shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})" 579proof 580 assume "bij_betw f A A'" 581 then show "bij_betw f (A \<union> {b}) (A' \<union> {f b})" 582 using assms notIn_Un_bij_betw [of b A f A'] by blast 583next 584 assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})" 585 have "f ` A = A'" 586 proof auto 587 fix a 588 assume **: "a \<in> A" 589 then have "f a \<in> A' \<union> {f b}" 590 using * unfolding bij_betw_def by blast 591 moreover 592 have False if "f a = f b" 593 proof - 594 have "a = b" 595 using * ** that unfolding bij_betw_def inj_on_def by blast 596 with \<open>b \<notin> A\<close> ** show ?thesis by blast 597 qed 598 ultimately show "f a \<in> A'" by blast 599 next 600 fix a' 601 assume **: "a' \<in> A'" 602 then have "a' \<in> f ` (A \<union> {b})" 603 using * by (auto simp add: bij_betw_def) 604 then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast 605 moreover 606 have False if "a = b" using 1 ** \<open>f b \<notin> A'\<close> that by blast 607 ultimately have "a \<in> A" by blast 608 with 1 show "a' \<in> f ` A" by blast 609 qed 610 then show "bij_betw f A A'" 611 using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast 612qed 613 614text \<open>Important examples\<close> 615 616context cancel_semigroup_add 617begin 618 619lemma inj_on_add [simp]: 620 "inj_on ((+) a) A" 621 by (rule inj_onI) simp 622 623lemma inj_add_left: 624 \<open>inj ((+) a)\<close> 625 by simp 626 627lemma inj_on_add' [simp]: 628 "inj_on (\<lambda>b. b + a) A" 629 by (rule inj_onI) simp 630 631lemma bij_betw_add [simp]: 632 "bij_betw ((+) a) A B \<longleftrightarrow> (+) a ` A = B" 633 by (simp add: bij_betw_def) 634 635end 636 637context ab_group_add 638begin 639 640lemma surj_plus [simp]: 641 "surj ((+) a)" 642 by (auto intro!: range_eqI [of b "(+) a" "b - a" for b]) (simp add: algebra_simps) 643 644lemma inj_diff_right [simp]: 645 \<open>inj (\<lambda>b. b - a)\<close> 646proof - 647 have \<open>inj ((+) (- a))\<close> 648 by (fact inj_add_left) 649 also have \<open>(+) (- a) = (\<lambda>b. b - a)\<close> 650 by (simp add: fun_eq_iff) 651 finally show ?thesis . 652qed 653 654lemma surj_diff_right [simp]: 655 "surj (\<lambda>x. x - a)" 656 using surj_plus [of "- a"] by (simp cong: image_cong_simp) 657 658lemma translation_Compl: 659 "(+) a ` (- t) = - ((+) a ` t)" 660proof (rule set_eqI) 661 fix b 662 show "b \<in> (+) a ` (- t) \<longleftrightarrow> b \<in> - (+) a ` t" 663 by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"]) 664qed 665 666lemma translation_subtract_Compl: 667 "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)" 668 using translation_Compl [of "- a" t] by (simp cong: image_cong_simp) 669 670lemma translation_diff: 671 "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)" 672 by auto 673 674lemma translation_subtract_diff: 675 "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)" 676 using translation_diff [of "- a"] by (simp cong: image_cong_simp) 677 678lemma translation_Int: 679 "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)" 680 by auto 681 682lemma translation_subtract_Int: 683 "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)" 684 using translation_Int [of " -a"] by (simp cong: image_cong_simp) 685 686end 687 688 689subsection \<open>Function Updating\<close> 690 691definition fun_upd :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" 692 where "fun_upd f a b = (\<lambda>x. if x = a then b else f x)" 693 694nonterminal updbinds and updbind 695 696syntax 697 "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" ("(2_ :=/ _)") 698 "" :: "updbind \<Rightarrow> updbinds" ("_") 699 "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _") 700 "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" ("_/'((_)')" [1000, 0] 900) 701 702translations 703 "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs" 704 "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y" 705 706(* Hint: to define the sum of two functions (or maps), use case_sum. 707 A nice infix syntax could be defined by 708notation 709 case_sum (infixr "'(+')"80) 710*) 711 712lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y" 713 unfolding fun_upd_def 714 apply safe 715 apply (erule subst) 716 apply (rule_tac [2] ext) 717 apply auto 718 done 719 720lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f" 721 by (simp only: fun_upd_idem_iff) 722 723lemma fun_upd_triv [iff]: "f(x := f x) = f" 724 by (simp only: fun_upd_idem) 725 726lemma fun_upd_apply [simp]: "(f(x := y)) z = (if z = x then y else f z)" 727 by (simp add: fun_upd_def) 728 729(* fun_upd_apply supersedes these two, but they are useful 730 if fun_upd_apply is intentionally removed from the simpset *) 731lemma fun_upd_same: "(f(x := y)) x = y" 732 by simp 733 734lemma fun_upd_other: "z \<noteq> x \<Longrightarrow> (f(x := y)) z = f z" 735 by simp 736 737lemma fun_upd_upd [simp]: "f(x := y, x := z) = f(x := z)" 738 by (simp add: fun_eq_iff) 739 740lemma fun_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a := b))(c := d) = (m(c := d))(a := b)" 741 by (rule ext) auto 742 743lemma inj_on_fun_updI: "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A" 744 by (auto simp: inj_on_def) 745 746lemma fun_upd_image: "f(x := y) ` A = (if x \<in> A then insert y (f ` (A - {x})) else f ` A)" 747 by auto 748 749lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)" 750 by auto 751 752lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z" 753 by (simp add: fun_eq_iff split: if_split_asm) 754 755 756subsection \<open>\<open>override_on\<close>\<close> 757 758definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" 759 where "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)" 760 761lemma override_on_emptyset[simp]: "override_on f g {} = f" 762 by (simp add: override_on_def) 763 764lemma override_on_apply_notin[simp]: "a \<notin> A \<Longrightarrow> (override_on f g A) a = f a" 765 by (simp add: override_on_def) 766 767lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a" 768 by (simp add: override_on_def) 769 770lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)" 771 by (simp add: override_on_def fun_eq_iff) 772 773lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)" 774 by (simp add: override_on_def fun_eq_iff) 775 776 777subsection \<open>\<open>swap\<close>\<close> 778 779definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" 780 where "swap a b f = f (a := f b, b:= f a)" 781 782lemma swap_apply [simp]: 783 "swap a b f a = f b" 784 "swap a b f b = f a" 785 "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c" 786 by (simp_all add: swap_def) 787 788lemma swap_self [simp]: "swap a a f = f" 789 by (simp add: swap_def) 790 791lemma swap_commute: "swap a b f = swap b a f" 792 by (simp add: fun_upd_def swap_def fun_eq_iff) 793 794lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" 795 by (rule ext) (simp add: fun_upd_def swap_def) 796 797lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id" 798 by (rule ext) simp 799 800lemma swap_triple: 801 assumes "a \<noteq> c" and "b \<noteq> c" 802 shows "swap a b (swap b c (swap a b f)) = swap a c f" 803 using assms by (simp add: fun_eq_iff swap_def) 804 805lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)" 806 by (rule ext) (simp add: fun_upd_def swap_def) 807 808lemma swap_image_eq [simp]: 809 assumes "a \<in> A" "b \<in> A" 810 shows "swap a b f ` A = f ` A" 811proof - 812 have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A" 813 using assms by (auto simp: image_iff swap_def) 814 then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" . 815 with subset[of f] show ?thesis by auto 816qed 817 818lemma 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" 819 by (auto simp add: inj_on_def swap_def) 820 821lemma inj_on_swap_iff [simp]: 822 assumes A: "a \<in> A" "b \<in> A" 823 shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A" 824proof 825 assume "inj_on (swap a b f) A" 826 with A have "inj_on (swap a b (swap a b f)) A" 827 by (iprover intro: inj_on_imp_inj_on_swap) 828 then show "inj_on f A" by simp 829next 830 assume "inj_on f A" 831 with A show "inj_on (swap a b f) A" 832 by (iprover intro: inj_on_imp_inj_on_swap) 833qed 834 835lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)" 836 by simp 837 838lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f" 839 by simp 840 841lemma 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" 842 by (auto simp: bij_betw_def) 843 844lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f" 845 by simp 846 847hide_const (open) swap 848 849 850subsection \<open>Inversion of injective functions\<close> 851 852definition the_inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" 853 where "the_inv_into A f = (\<lambda>x. THE y. y \<in> A \<and> f y = x)" 854 855lemma the_inv_into_f_f: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x" 856 unfolding the_inv_into_def inj_on_def by blast 857 858lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A \<Longrightarrow> f (the_inv_into A f y) = y" 859 apply (simp add: the_inv_into_def) 860 apply (rule the1I2) 861 apply (blast dest: inj_onD) 862 apply blast 863 done 864 865lemma 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" 866 apply (simp add: the_inv_into_def) 867 apply (rule the1I2) 868 apply (blast dest: inj_onD) 869 apply blast 870 done 871 872lemma the_inv_into_onto [simp]: "inj_on f A \<Longrightarrow> the_inv_into A f ` (f ` A) = A" 873 by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric]) 874 875lemma 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" 876 apply (erule subst) 877 apply (erule the_inv_into_f_f) 878 apply assumption 879 done 880 881lemma the_inv_into_comp: 882 "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow> 883 the_inv_into A (f \<circ> g) x = (the_inv_into A g \<circ> the_inv_into (g ` A) f) x" 884 apply (rule the_inv_into_f_eq) 885 apply (fast intro: comp_inj_on) 886 apply (simp add: f_the_inv_into_f the_inv_into_into) 887 apply (simp add: the_inv_into_into) 888 done 889 890lemma inj_on_the_inv_into: "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)" 891 by (auto intro: inj_onI simp: the_inv_into_f_f) 892 893lemma bij_betw_the_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A" 894 by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into) 895 896abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" 897 where "the_inv f \<equiv> the_inv_into UNIV f" 898 899lemma the_inv_f_f: "the_inv f (f x) = x" if "inj f" 900 using that UNIV_I by (rule the_inv_into_f_f) 901 902 903subsection \<open>Cantor's Paradox\<close> 904 905theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A" 906proof 907 assume "\<exists>f. f ` A = Pow A" 908 then obtain f where f: "f ` A = Pow A" .. 909 let ?X = "{a \<in> A. a \<notin> f a}" 910 have "?X \<in> Pow A" by blast 911 then have "?X \<in> f ` A" by (simp only: f) 912 then obtain x where "x \<in> A" and "f x = ?X" by blast 913 then show False by blast 914qed 915 916subsection \<open>Monotonic functions over a set\<close> 917 918definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s" 919 920lemma mono_onI: 921 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A" 922 unfolding mono_on_def by simp 923 924lemma mono_onD: 925 "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s" 926 unfolding mono_on_def by simp 927 928lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A" 929 unfolding mono_def mono_on_def by auto 930 931lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B" 932 unfolding mono_on_def by auto 933 934definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s" 935 936lemma strict_mono_onI: 937 "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A" 938 unfolding strict_mono_on_def by simp 939 940lemma strict_mono_onD: 941 "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s" 942 unfolding strict_mono_on_def by simp 943 944lemma mono_on_greaterD: 945 assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)" 946 shows "x > y" 947proof (rule ccontr) 948 assume "\<not>x > y" 949 hence "x \<le> y" by (simp add: not_less) 950 from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD) 951 with assms(4) show False by simp 952qed 953 954lemma strict_mono_inv: 955 fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)" 956 assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x" 957 shows "strict_mono g" 958proof 959 fix x y :: 'b assume "x < y" 960 from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast 961 with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less) 962 with inv show "g x < g y" by simp 963qed 964 965lemma strict_mono_on_imp_inj_on: 966 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A" 967 shows "inj_on f A" 968proof (rule inj_onI) 969 fix x y assume "x \<in> A" "y \<in> A" "f x = f y" 970 thus "x = y" 971 by (cases x y rule: linorder_cases) 972 (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 973qed 974 975lemma strict_mono_on_leD: 976 assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y" 977 shows "f x \<le> f y" 978proof (insert le_less_linear[of y x], elim disjE) 979 assume "x < y" 980 with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all 981 thus ?thesis by (rule less_imp_le) 982qed (insert assms, simp) 983 984lemma strict_mono_on_eqD: 985 fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)" 986 assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A" 987 shows "y = x" 988 using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) 989 990lemma strict_mono_on_imp_mono_on: 991 "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A" 992 by (rule mono_onI, rule strict_mono_on_leD) 993 994 995subsection \<open>Setup\<close> 996 997subsubsection \<open>Proof tools\<close> 998 999text \<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> 1000 1001simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ => 1002 let 1003 fun gen_fun_upd NONE T _ _ = NONE 1004 | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y) 1005 fun dest_fun_T1 (Type (_, T :: Ts)) = T 1006 fun find_double (t as Const (\<^const_name>\<open>fun_upd\<close>,T) $ f $ x $ y) = 1007 let 1008 fun find (Const (\<^const_name>\<open>fun_upd\<close>,T) $ g $ v $ w) = 1009 if v aconv x then SOME g else gen_fun_upd (find g) T v w 1010 | find t = NONE 1011 in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end 1012 1013 val ss = simpset_of \<^context> 1014 1015 fun proc ctxt ct = 1016 let 1017 val t = Thm.term_of ct 1018 in 1019 (case find_double t of 1020 (T, NONE) => NONE 1021 | (T, SOME rhs) => 1022 SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs)) 1023 (fn _ => 1024 resolve_tac ctxt [eq_reflection] 1 THEN 1025 resolve_tac ctxt @{thms ext} 1 THEN 1026 simp_tac (put_simpset ss ctxt) 1))) 1027 end 1028 in proc end 1029\<close> 1030 1031 1032subsubsection \<open>Functorial structure of types\<close> 1033 1034ML_file \<open>Tools/functor.ML\<close> 1035 1036functor map_fun: map_fun 1037 by (simp_all add: fun_eq_iff) 1038 1039functor vimage 1040 by (simp_all add: fun_eq_iff vimage_comp) 1041 1042 1043text \<open>Legacy theorem names\<close> 1044 1045lemmas o_def = comp_def 1046lemmas o_apply = comp_apply 1047lemmas o_assoc = comp_assoc [symmetric] 1048lemmas id_o = id_comp 1049lemmas o_id = comp_id 1050lemmas o_eq_dest = comp_eq_dest 1051lemmas o_eq_elim = comp_eq_elim 1052lemmas o_eq_dest_lhs = comp_eq_dest_lhs 1053lemmas o_eq_id_dest = comp_eq_id_dest 1054 1055end 1056