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