1 (* Title: HOL/Hilbert_Choice.thy
3 Author: Lawrence C Paulson
4 Copyright 2001 University of Cambridge
7 header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
9 theory Hilbert_Choice = NatArith
10 files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
13 Eps :: "('a => bool) => 'a"
17 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<epsilon>_./ _)" [0, 10] 10)
20 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10)
23 "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10)
26 "SOME x. P" == "Eps (%x. P)"
29 someI: "P (x::'a) ==> P (SOME x. P x)"
33 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
34 by (blast intro: someI)
38 inv :: "('a => 'b) => ('b => 'a)"
39 "inv(f::'a=>'b) == % y. @x. f(x)=y"
41 Inv :: "['a set, 'a => 'b] => ('b => 'a)"
42 "Inv A f == (% x. (@ y. y : A & f y = x))"
45 use "Hilbert_Choice_lemmas.ML"
48 (** Least value operator **)
51 LeastM :: "['a => 'b::ord, 'a => bool] => 'a"
52 "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
55 "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
58 "LEAST x WRT m. P" == "LeastM m (%x. P)"
61 "[| P x; !!y. P y ==> m x <= m y;
62 !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
64 apply (unfold LeastM_def)
65 apply (rule someI2_ex)
70 lemma LeastM_equality:
71 "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) =
76 apply (blast intro!: order_antisym)
79 lemma wf_linord_ex_has_least:
80 "[|wf r; ALL x y. ((x,y):r^+) = ((y,x)~:r^*); P k|] \
81 \ ==> EX x. P x & (!y. P y --> (m x,m y):r^*)"
82 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
83 apply (drule_tac x = "m`Collect P" in spec)
87 (* successor of obsolete nonempty_has_least *)
88 lemma ex_has_least_nat:
89 "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
90 apply (simp only: pred_nat_trancl_eq_le [symmetric])
91 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
92 apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
96 lemma LeastM_nat_lemma:
97 "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
98 apply (unfold LeastM_def)
100 apply (erule ex_has_least_nat)
103 lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
105 lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
106 apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
112 (** Greatest value operator **)
115 GreatestM :: "['a => 'b::ord, 'a => bool] => 'a"
116 "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
118 Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10)
119 "Greatest == GreatestM (%x. x)"
122 "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
123 ("GREATEST _ WRT _. _" [0,4,10]10)
126 "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
130 !!y. P y ==> m y <= m x;
131 !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
132 ==> Q (GreatestM m P)";
133 apply (unfold GreatestM_def)
134 apply (rule someI2_ex)
139 lemma GreatestM_equality:
140 "[| P k; !!x. P x ==> m x <= m k |]
141 ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
142 apply (rule_tac m=m in GreatestMI2)
145 apply (blast intro!: order_antisym)
148 lemma Greatest_equality:
149 "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
150 apply (unfold Greatest_def)
151 apply (erule GreatestM_equality)
155 lemma ex_has_greatest_nat_lemma:
156 "[|P k; ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]
157 ==> EX y. P y & ~ (m y < m k + n)"
158 apply (induct_tac "n")
161 apply (force simp add: le_Suc_eq)
164 lemma ex_has_greatest_nat: "[|P k; ! y. P y --> m y < b|]
165 ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
167 apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
168 apply (subgoal_tac [3] "m k <= b")
172 lemma GreatestM_nat_lemma:
173 "[|P k; ! y. P y --> m y < b|]
174 ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
175 apply (unfold GreatestM_def)
176 apply (rule someI_ex)
177 apply (erule ex_has_greatest_nat)
181 lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
183 lemma GreatestM_nat_le: "[|P x; ! y. P y --> m y < b|]
184 ==> (m x::nat) <= m (GreatestM m P)"
185 apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
188 (** Specialization to GREATEST **)
191 "[|P (k::nat); ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
193 apply (unfold Greatest_def)
194 apply (rule GreatestM_natI)
199 "[|P x; ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
200 apply (unfold Greatest_def)
201 apply (rule GreatestM_nat_le)
206 use "meson_lemmas.ML"