src/HOL/Hilbert_Choice.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (23 months ago) changeset 66831 29ea2b900a05 parent 65955 0616ba637b14 child 67613 ce654b0e6d69 permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Hilbert_Choice.thy
2     Author:     Lawrence C Paulson, Tobias Nipkow
3     Copyright   2001  University of Cambridge
4 *)
6 section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
8 theory Hilbert_Choice
9   imports Wellfounded
10   keywords "specification" :: thy_goal
11 begin
13 subsection \<open>Hilbert's epsilon\<close>
15 axiomatization Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
16   where someI: "P x \<Longrightarrow> P (Eps P)"
18 syntax (epsilon)
19   "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3\<some>_./ _)" [0, 10] 10)
20 syntax (input)
21   "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3@ _./ _)" [0, 10] 10)
22 syntax
23   "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
24 translations
25   "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
27 print_translation \<open>
28   [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
29       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
30       in Syntax.const @{syntax_const "_Eps"} \$ x \$ t end)]
31 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
33 definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
34 "inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
36 lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
39 abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
40 "inv \<equiv> inv_into UNIV"
43 subsection \<open>Hilbert's Epsilon-operator\<close>
45 text \<open>
46   Easier to apply than \<open>someI\<close> if the witness comes from an
47   existential formula.
48 \<close>
49 lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
50   apply (erule exE)
51   apply (erule someI)
52   done
54 text \<open>
55   Easier to apply than \<open>someI\<close> because the conclusion has only one
56   occurrence of @{term P}.
57 \<close>
58 lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
59   by (blast intro: someI)
61 text \<open>
62   Easier to apply than \<open>someI2\<close> if the witness comes from an
63   existential formula.
64 \<close>
65 lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
66   by (blast intro: someI2)
68 lemma someI2_bex: "\<exists>a\<in>A. P a \<Longrightarrow> (\<And>x. x \<in> A \<and> P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. x \<in> A \<and> P x)"
69   by (blast intro: someI2)
71 lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a"
72   by (blast intro: someI2)
74 lemma some1_equality: "\<exists>!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
75   by blast
77 lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)"
78   by (blast intro: someI)
80 lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
81   unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
83 lemma some_eq_trivial [simp]: "(SOME y. y = x) = x"
84   by (rule some_equality) (rule refl)
86 lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
87   apply (rule some_equality)
88    apply (rule refl)
89   apply (erule sym)
90   done
93 subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>
95 lemma choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
96   by (fast elim: someI)
98 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
99   by (fast elim: someI)
101 lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
102   by (fast elim: someI)
104 lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))"
105   by (fast elim: someI)
107 lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
108   by (fast elim: someI)
110 lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
111   by (fast elim: someI)
113 lemma dependent_nat_choice:
114   assumes 1: "\<exists>x. P 0 x"
115     and 2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
116   shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
117 proof (intro exI allI conjI)
118   fix n
119   define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
120   then have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
121     using someI_ex[OF 1] someI_ex[OF 2] by simp_all
122   then show "P n (f n)" "Q n (f n) (f (Suc n))"
123     by (induct n) auto
124 qed
127 subsection \<open>Function Inverse\<close>
129 lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
132 lemma inv_into_into: "x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A"
133   by (simp add: inv_into_def) (fast intro: someI2)
135 lemma inv_identity [simp]: "inv (\<lambda>a. a) = (\<lambda>a. a)"
138 lemma inv_id [simp]: "inv id = id"
141 lemma inv_into_f_f [simp]: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> inv_into A f (f x) = x"
142   by (simp add: inv_into_def inj_on_def) (blast intro: someI2)
144 lemma inv_f_f: "inj f \<Longrightarrow> inv f (f x) = x"
145   by simp
147 lemma f_inv_into_f: "y : f`A \<Longrightarrow> f (inv_into A f y) = y"
148   by (simp add: inv_into_def) (fast intro: someI2)
150 lemma inv_into_f_eq: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> f x = y \<Longrightarrow> inv_into A f y = x"
151   by (erule subst) (fast intro: inv_into_f_f)
153 lemma inv_f_eq: "inj f \<Longrightarrow> f x = y \<Longrightarrow> inv f y = x"
156 lemma inj_imp_inv_eq: "inj f \<Longrightarrow> \<forall>x. f (g x) = x \<Longrightarrow> inv f = g"
157   by (blast intro: inv_into_f_eq)
159 text \<open>But is it useful?\<close>
160 lemma inj_transfer:
161   assumes inj: "inj f"
162     and minor: "\<And>y. y \<in> range f \<Longrightarrow> P (inv f y)"
163   shows "P x"
164 proof -
165   have "f x \<in> range f" by auto
166   then have "P(inv f (f x))" by (rule minor)
167   then show "P x" by (simp add: inv_into_f_f [OF inj])
168 qed
170 lemma inj_iff: "inj f \<longleftrightarrow> inv f \<circ> f = id"
171   by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f)
173 lemma inv_o_cancel[simp]: "inj f \<Longrightarrow> inv f \<circ> f = id"
176 lemma o_inv_o_cancel[simp]: "inj f \<Longrightarrow> g \<circ> inv f \<circ> f = g"
179 lemma inv_into_image_cancel[simp]: "inj_on f A \<Longrightarrow> S \<subseteq> A \<Longrightarrow> inv_into A f ` f ` S = S"
180   by (fastforce simp: image_def)
182 lemma inj_imp_surj_inv: "inj f \<Longrightarrow> surj (inv f)"
183   by (blast intro!: surjI inv_into_f_f)
185 lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
188 lemma inv_into_injective:
189   assumes eq: "inv_into A f x = inv_into A f y"
190     and x: "x \<in> f`A"
191     and y: "y \<in> f`A"
192   shows "x = y"
193 proof -
194   from eq have "f (inv_into A f x) = f (inv_into A f y)"
195     by simp
196   with x y show ?thesis
198 qed
200 lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B"
201   by (blast intro: inj_onI dest: inv_into_injective injD)
203 lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A"
204   by (auto simp add: bij_betw_def inj_on_inv_into)
206 lemma surj_imp_inj_inv: "surj f \<Longrightarrow> inj (inv f)"
209 lemma surj_iff: "surj f \<longleftrightarrow> f \<circ> inv f = id"
210   by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
212 lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
213   by (simp add: o_def surj_iff fun_eq_iff)
215 lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g"
216   apply (rule ext)
217   apply (drule_tac x = "inv f x" in spec)
219   done
221 lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)"
222   by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
224 lemma inv_equality: "(\<And>x. g (f x) = x) \<Longrightarrow> (\<And>y. f (g y) = y) \<Longrightarrow> inv f = g"
225   by (rule ext) (auto simp add: inv_into_def)
227 lemma inv_inv_eq: "bij f \<Longrightarrow> inv (inv f) = f"
228   by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
230 text \<open>
231   \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such
232   that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close>
233   that \<open>inv f\<close> could be any function at all, including the identity function.
234   If \<open>inv f = id\<close> then \<open>inv f\<close> is a bijection, but \<open>inj f\<close>, \<open>surj f\<close> and \<open>inv
235   (inv f) = f\<close> all fail.
236 \<close>
238 lemma inv_into_comp:
239   "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
240     inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
241   apply (rule inv_into_f_eq)
242     apply (fast intro: comp_inj_on)
244   apply (simp add: f_inv_into_f inv_into_into)
245   done
247 lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
248   by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
250 lemma image_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
251   by (simp add: surj_f_inv_f image_comp comp_def)
253 lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
254   by simp
256 lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
257   apply auto
258    apply (force simp add: bij_is_inj)
259   apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
260   done
262 lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A"
263   apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
264   apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
265   done
267 lemma finite_fun_UNIVD1:
268   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
269     and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
270   shows "finite (UNIV :: 'a set)"
271 proof -
272   let ?UNIV_b = "UNIV :: 'b set"
273   from fin have "finite ?UNIV_b"
274     by (rule finite_fun_UNIVD2)
275   with card have "card ?UNIV_b \<ge> Suc (Suc 0)"
276     by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff)
277   then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))"
278     by simp
279   then obtain b1 b2 :: 'b where b1b2: "b1 \<noteq> b2"
280     by (auto simp: card_Suc_eq)
281   from fin have fin': "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
282     by (rule finite_imageI)
283   have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
284   proof (rule UNIV_eq_I)
285     fix x :: 'a
286     from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
288     then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
289       by blast
290   qed
291   with fin' show ?thesis
292     by simp
293 qed
295 text \<open>
296   Every infinite set contains a countable subset. More precisely we
297   show that a set \<open>S\<close> is infinite if and only if there exists an
298   injective function from the naturals into \<open>S\<close>.
300   The ``only if'' direction is harder because it requires the
301   construction of a sequence of pairwise different elements of an
302   infinite set \<open>S\<close>. The idea is to construct a sequence of
303   non-empty and infinite subsets of \<open>S\<close> obtained by successively
304   removing elements of \<open>S\<close>.
305 \<close>
307 lemma infinite_countable_subset:
308   assumes inf: "\<not> finite S"
309   shows "\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S"
310   \<comment> \<open>Courtesy of Stephan Merz\<close>
311 proof -
312   define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
313   define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
314   have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
315     by (induct n) (auto simp: Sseq_def inf)
316   then have **: "\<And>n. pick n \<in> Sseq n"
317     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
318   with * have "range pick \<subseteq> S" by auto
319   moreover have "pick n \<noteq> pick (n + Suc m)" for m n
320   proof -
321     have "pick n \<notin> Sseq (n + Suc m)"
322       by (induct m) (auto simp add: Sseq_def pick_def)
323     with ** show ?thesis by auto
324   qed
325   then have "inj pick"
327   ultimately show ?thesis by blast
328 qed
330 lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S)"
331   \<comment> \<open>Courtesy of Stephan Merz\<close>
332   using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
334 lemma image_inv_into_cancel:
335   assumes surj: "f`A = A'"
336     and sub: "B' \<subseteq> A'"
337   shows "f `((inv_into A f)`B') = B'"
338   using assms
339 proof (auto simp: f_inv_into_f)
340   let ?f' = "inv_into A f"
341   fix a'
342   assume *: "a' \<in> B'"
343   with sub have "a' \<in> A'" by auto
344   with surj have "a' = f (?f' a')"
345     by (auto simp: f_inv_into_f)
346   with * show "a' \<in> f ` (?f' ` B')" by blast
347 qed
349 lemma inv_into_inv_into_eq:
350   assumes "bij_betw f A A'"
351     and a: "a \<in> A"
352   shows "inv_into A' (inv_into A f) a = f a"
353 proof -
354   let ?f' = "inv_into A f"
355   let ?f'' = "inv_into A' ?f'"
356   from assms have *: "bij_betw ?f' A' A"
357     by (auto simp: bij_betw_inv_into)
358   with a obtain a' where a': "a' \<in> A'" "?f' a' = a"
359     unfolding bij_betw_def by force
360   with a * have "?f'' a = a'"
361     by (auto simp: f_inv_into_f bij_betw_def)
362   moreover from assms a' have "f a = a'"
363     by (auto simp: bij_betw_def)
364   ultimately show "?f'' a = f a" by simp
365 qed
367 lemma inj_on_iff_surj:
368   assumes "A \<noteq> {}"
369   shows "(\<exists>f. inj_on f A \<and> f ` A \<subseteq> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
370 proof safe
371   fix f
372   assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'"
373   let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"
374   let ?csi = "\<lambda>a. a \<in> A"
375   let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
376   have "?g ` A' = A"
377   proof
378     show "?g ` A' \<subseteq> A"
379     proof clarify
380       fix a'
381       assume *: "a' \<in> A'"
382       show "?g a' \<in> A"
383       proof (cases "a' \<in> f ` A")
384         case True
385         then obtain a where "?phi a' a" by blast
386         then have "?phi a' (SOME a. ?phi a' a)"
387           using someI[of "?phi a'" a] by blast
388         with True show ?thesis by auto
389       next
390         case False
391         with assms have "?csi (SOME a. ?csi a)"
392           using someI_ex[of ?csi] by blast
393         with False show ?thesis by auto
394       qed
395     qed
396   next
397     show "A \<subseteq> ?g ` A'"
398     proof -
399       have "?g (f a) = a \<and> f a \<in> A'" if a: "a \<in> A" for a
400       proof -
401         let ?b = "SOME aa. ?phi (f a) aa"
402         from a have "?phi (f a) a" by auto
403         then have *: "?phi (f a) ?b"
404           using someI[of "?phi(f a)" a] by blast
405         then have "?g (f a) = ?b" using a by auto
406         moreover from inj * a have "a = ?b"
407           by (auto simp add: inj_on_def)
408         ultimately have "?g(f a) = a" by simp
409         with incl a show ?thesis by auto
410       qed
411       then show ?thesis by force
412     qed
413   qed
414   then show "\<exists>g. g ` A' = A" by blast
415 next
416   fix g
417   let ?f = "inv_into A' g"
418   have "inj_on ?f (g ` A')"
419     by (auto simp: inj_on_inv_into)
420   moreover have "?f (g a') \<in> A'" if a': "a' \<in> A'" for a'
421   proof -
422     let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
423     from a' have "?phi a'" by auto
424     then have "?phi (SOME b'. ?phi b')"
425       using someI[of ?phi] by blast
426     then show ?thesis by (auto simp: inv_into_def)
427   qed
428   ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'"
429     by auto
430 qed
432 lemma Ex_inj_on_UNION_Sigma:
433   "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i))"
434 proof
435   let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i"
436   let ?sm = "\<lambda>a. SOME i. ?phi a i"
437   let ?f = "\<lambda>a. (?sm a, a)"
438   have "inj_on ?f (\<Union>i \<in> I. A i)"
439     by (auto simp: inj_on_def)
440   moreover
441   have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a
442     using that someI[of "?phi a" i] by auto
443   then have "?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
444     by auto
445   ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
446     by auto
447 qed
449 lemma inv_unique_comp:
450   assumes fg: "f \<circ> g = id"
451     and gf: "g \<circ> f = id"
452   shows "inv f = g"
453   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
456 subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
458 text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>
460 text \<open>Looping simprule!\<close>
461 lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))"
462   by simp
464 lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
467 lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \<and> y = y') = (x, y)"
468   by blast
471 text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
472 lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> r)"
473   (is "_ \<longleftrightarrow> \<not> ?ex")
474 proof
475   assume "wf r"
476   show "\<not> ?ex"
477   proof
478     assume ?ex
479     then obtain f where f: "(f (Suc i), f i) \<in> r" for i
480       by blast
481     from \<open>wf r\<close> have minimal: "x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" for x Q
482       by (auto simp: wf_eq_minimal)
483     let ?Q = "{w. \<exists>i. w = f i}"
484     fix n
485     have "f n \<in> ?Q" by blast
486     from minimal [OF this] obtain j where "(y, f j) \<in> r \<Longrightarrow> y \<notin> ?Q" for y by blast
487     with this [OF \<open>(f (Suc j), f j) \<in> r\<close>] have "f (Suc j) \<notin> ?Q" by simp
488     then show False by blast
489   qed
490 next
491   assume "\<not> ?ex"
492   then show "wf r"
493   proof (rule contrapos_np)
494     assume "\<not> wf r"
495     then obtain Q x where x: "x \<in> Q" and rec: "z \<in> Q \<Longrightarrow> \<exists>y. (y, z) \<in> r \<and> y \<in> Q" for z
496       by (auto simp add: wf_eq_minimal)
497     obtain descend :: "nat \<Rightarrow> 'a"
498       where descend_0: "descend 0 = x"
499         and descend_Suc: "descend (Suc n) = (SOME y. y \<in> Q \<and> (y, descend n) \<in> r)" for n
500       by (rule that [of "rec_nat x (\<lambda>_ rec. (SOME y. y \<in> Q \<and> (y, rec) \<in> r))"]) simp_all
501     have descend_Q: "descend n \<in> Q" for n
502     proof (induct n)
503       case 0
504       with x show ?case by (simp only: descend_0)
505     next
506       case Suc
507       then show ?case by (simp only: descend_Suc) (rule someI2_ex; use rec in blast)
508     qed
509     have "(descend (Suc i), descend i) \<in> r" for i
510       by (simp only: descend_Suc) (rule someI2_ex; use descend_Q rec in blast)
511     then show "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r" by blast
512   qed
513 qed
515 lemma wf_no_infinite_down_chainE:
516   assumes "wf r"
517   obtains k where "(f (Suc k), f k) \<notin> r"
518   using assms wf_iff_no_infinite_down_chain[of r] by blast
521 text \<open>A dynamically-scoped fact for TFL\<close>
522 lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
523   by (blast intro: someI)
526 subsection \<open>An aside: bounded accessible part\<close>
528 text \<open>Finite monotone eventually stable sequences\<close>
530 lemma finite_mono_remains_stable_implies_strict_prefix:
531   fixes f :: "nat \<Rightarrow> 'a::order"
532   assumes S: "finite (range f)" "mono f"
533     and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
534   shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
535   using assms
536 proof -
537   have "\<exists>n. f n = f (Suc n)"
538   proof (rule ccontr)
539     assume "\<not> ?thesis"
540     then have "\<And>n. f n \<noteq> f (Suc n)" by auto
541     with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)"
542       by (auto simp: le_less mono_iff_le_Suc)
543     with lift_Suc_mono_less_iff[of f] have *: "\<And>n m. n < m \<Longrightarrow> f n < f m"
544       by auto
545     have "inj f"
546     proof (intro injI)
547       fix x y
548       assume "f x = f y"
549       then show "x = y"
550         by (cases x y rule: linorder_cases) (auto dest: *)
551     qed
552     with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
553       by (rule finite_imageD)
554     then show False by simp
555   qed
556   then obtain n where n: "f n = f (Suc n)" ..
557   define N where "N = (LEAST n. f n = f (Suc n))"
558   have N: "f N = f (Suc N)"
559     unfolding N_def using n by (rule LeastI)
560   show ?thesis
561   proof (intro exI[of _ N] conjI allI impI)
562     fix n
563     assume "N \<le> n"
564     then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
565     proof (induct rule: dec_induct)
566       case base
567       then show ?case by simp
568     next
569       case (step n)
570       then show ?case
571         using eq [rule_format, of "n - 1"] N
572         by (cases n) (auto simp add: le_Suc_eq)
573     qed
574     from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
575   next
576     fix n m :: nat
577     assume "m < n" "n \<le> N"
578     then show "f m < f n"
579     proof (induct rule: less_Suc_induct)
580       case (1 i)
581       then have "i < N" by simp
582       then have "f i \<noteq> f (Suc i)"
583         unfolding N_def by (rule not_less_Least)
584       with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
585     next
586       case 2
587       then show ?case by simp
588     qed
589   qed
590 qed
592 lemma finite_mono_strict_prefix_implies_finite_fixpoint:
593   fixes f :: "nat \<Rightarrow> 'a set"
594   assumes S: "\<And>i. f i \<subseteq> S" "finite S"
595     and ex: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
596   shows "f (card S) = (\<Union>n. f n)"
597 proof -
598   from ex obtain N where inj: "\<And>n m. n \<le> N \<Longrightarrow> m \<le> N \<Longrightarrow> m < n \<Longrightarrow> f m \<subset> f n"
599     and eq: "\<forall>n\<ge>N. f N = f n"
600     by atomize auto
601   have "i \<le> N \<Longrightarrow> i \<le> card (f i)" for i
602   proof (induct i)
603     case 0
604     then show ?case by simp
605   next
606     case (Suc i)
607     with inj [of "Suc i" i] have "(f i) \<subset> (f (Suc i))" by auto
608     moreover have "finite (f (Suc i))" using S by (rule finite_subset)
609     ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
610     with Suc inj show ?case by auto
611   qed
612   then have "N \<le> card (f N)" by simp
613   also have "\<dots> \<le> card S" using S by (intro card_mono)
614   finally have "f (card S) = f N" using eq by auto
615   then show ?thesis
616     using eq inj [of N]
617     apply auto
618     apply (case_tac "n < N")
619      apply (auto simp: not_less)
620     done
621 qed
624 subsection \<open>More on injections, bijections, and inverses\<close>
626 locale bijection =
627   fixes f :: "'a \<Rightarrow> 'a"
628   assumes bij: "bij f"
629 begin
631 lemma bij_inv: "bij (inv f)"
632   using bij by (rule bij_imp_bij_inv)
634 lemma surj [simp]: "surj f"
635   using bij by (rule bij_is_surj)
637 lemma inj: "inj f"
638   using bij by (rule bij_is_inj)
640 lemma surj_inv [simp]: "surj (inv f)"
641   using inj by (rule inj_imp_surj_inv)
643 lemma inj_inv: "inj (inv f)"
644   using surj by (rule surj_imp_inj_inv)
646 lemma eqI: "f a = f b \<Longrightarrow> a = b"
647   using inj by (rule injD)
649 lemma eq_iff [simp]: "f a = f b \<longleftrightarrow> a = b"
650   by (auto intro: eqI)
652 lemma eq_invI: "inv f a = inv f b \<Longrightarrow> a = b"
653   using inj_inv by (rule injD)
655 lemma eq_inv_iff [simp]: "inv f a = inv f b \<longleftrightarrow> a = b"
656   by (auto intro: eq_invI)
658 lemma inv_left [simp]: "inv f (f a) = a"
659   using inj by (simp add: inv_f_eq)
661 lemma inv_comp_left [simp]: "inv f \<circ> f = id"
664 lemma inv_right [simp]: "f (inv f a) = a"
665   using surj by (simp add: surj_f_inv_f)
667 lemma inv_comp_right [simp]: "f \<circ> inv f = id"
670 lemma inv_left_eq_iff [simp]: "inv f a = b \<longleftrightarrow> f b = a"
671   by auto
673 lemma inv_right_eq_iff [simp]: "b = inv f a \<longleftrightarrow> f b = a"
674   by auto
676 end
678 lemma infinite_imp_bij_betw:
679   assumes infinite: "\<not> finite A"
680   shows "\<exists>h. bij_betw h A (A - {a})"
681 proof (cases "a \<in> A")
682   case False
683   then have "A - {a} = A" by blast
684   then show ?thesis
685     using bij_betw_id[of A] by auto
686 next
687   case True
688   with infinite have "\<not> finite (A - {a})" by auto
689   with infinite_iff_countable_subset[of "A - {a}"]
690   obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast
691   define g where "g n = (if n = 0 then a else f (Suc n))" for n
692   define A' where "A' = g ` UNIV"
693   have *: "\<forall>y. f y \<noteq> a" using 2 by blast
694   have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV"
695     apply (auto simp add: True g_def [abs_def])
696      apply (unfold inj_on_def)
697      apply (intro ballI impI)
698      apply (case_tac "x = 0")
699       apply (auto simp add: 2)
700   proof -
701     fix y
702     assume "a = (if y = 0 then a else f (Suc y))"
703     then show "y = 0" by (cases "y = 0") (use * in auto)
704   next
705     fix x y
706     assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
707     with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def)
708   next
709     fix n
710     from 2 show "f (Suc n) \<in> A" by blast
711   qed
712   then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A"
713     using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
714   then have 5: "bij_betw (inv g) A' UNIV"
715     by (auto simp add: bij_betw_inv_into)
716   from 3 obtain n where n: "g n = a" by auto
717   have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
718     by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
719   define v where "v m = (if m < n then m else Suc m)" for m
720   have 7: "bij_betw v UNIV (UNIV - {n})"
721   proof (unfold bij_betw_def inj_on_def, intro conjI, clarify)
722     fix m1 m2
723     assume "v m1 = v m2"
724     then show "m1 = m2"
725       apply (cases "m1 < n")
726        apply (cases "m2 < n")
727         apply (auto simp: inj_on_def v_def [abs_def])
728       apply (cases "m2 < n")
729        apply auto
730       done
731   next
732     show "v ` UNIV = UNIV - {n}"
733     proof (auto simp: v_def [abs_def])
734       fix m
735       assume "m \<noteq> n"
736       assume *: "m \<notin> Suc ` {m'. \<not> m' < n}"
737       have False if "n \<le> m"
738       proof -
739         from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto
740         from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" ..
741         with ** have "n \<le> m'" by auto
742         with m' * show ?thesis by auto
743       qed
744       then show "m < n" by force
745     qed
746   qed
747   define h' where "h' = g \<circ> v \<circ> (inv g)"
748   with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
749     by (auto simp add: bij_betw_trans)
750   define h where "h b = (if b \<in> A' then h' b else b)" for b
751   then have "\<forall>b \<in> A'. h b = h' b" by simp
752   with 8 have "bij_betw h  A' (A' - {a})"
753     using bij_betw_cong[of A' h] by auto
754   moreover
755   have "\<forall>b \<in> A - A'. h b = b" by (auto simp: h_def)
756   then have "bij_betw h  (A - A') (A - A')"
757     using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
758   moreover
759   from 4 have "(A' \<inter> (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
760     ((A' - {a}) \<inter> (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
761     by blast
762   ultimately have "bij_betw h A (A - {a})"
763     using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
764   then show ?thesis by blast
765 qed
767 lemma infinite_imp_bij_betw2:
768   assumes "\<not> finite A"
769   shows "\<exists>h. bij_betw h A (A \<union> {a})"
770 proof (cases "a \<in> A")
771   case True
772   then have "A \<union> {a} = A" by blast
773   then show ?thesis using bij_betw_id[of A] by auto
774 next
775   case False
776   let ?A' = "A \<union> {a}"
777   from False have "A = ?A' - {a}" by blast
778   moreover from assms have "\<not> finite ?A'" by auto
779   ultimately obtain f where "bij_betw f ?A' A"
780     using infinite_imp_bij_betw[of ?A' a] by auto
781   then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into)
782   then show ?thesis by auto
783 qed
785 lemma bij_betw_inv_into_left: "bij_betw f A A' \<Longrightarrow> a \<in> A \<Longrightarrow> inv_into A f (f a) = a"
786   unfolding bij_betw_def by clarify (rule inv_into_f_f)
788 lemma bij_betw_inv_into_right: "bij_betw f A A' \<Longrightarrow> a' \<in> A' \<Longrightarrow> f (inv_into A f a') = a'"
789   unfolding bij_betw_def using f_inv_into_f by force
791 lemma bij_betw_inv_into_subset:
792   "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw (inv_into A f) B' B"
793   by (auto simp: bij_betw_def intro: inj_on_inv_into)
796 subsection \<open>Specification package -- Hilbertized version\<close>
798 lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
799   by (simp only: someI_ex)
801 ML_file "Tools/choice_specification.ML"
803 end