author  paulson 
Thu, 15 Sep 2005 17:44:53 +0200  
changeset 17420  bdcffa8d8665 
parent 16796  140f1e0ea846 
child 17702  ea88ddeafabe 
permissions  rwrr 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

1 
(* Title: HOL/Hilbert_Choice.thy 
14760  2 
ID: $Id$ 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

4 
Copyright 2001 University of Cambridge 
12023  5 
*) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

6 

14760  7 
header {* Hilbert's EpsilonOperator and the Axiom of Choice *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

8 

15131  9 
theory Hilbert_Choice 
15140  10 
imports NatArith 
16417  11 
uses ("Tools/meson.ML") ("Tools/specification_package.ML") 
15131  12 
begin 
12298  13 

14 
subsection {* Hilbert's epsilon *} 

15 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

16 
consts 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

17 
Eps :: "('a => bool) => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

18 

14872
3f2144aebd76
improved symbolic syntax of Eps: \<some> for mode "epsilon";
wenzelm
parents:
14760
diff
changeset

19 
syntax (epsilon) 
3f2144aebd76
improved symbolic syntax of Eps: \<some> for mode "epsilon";
wenzelm
parents:
14760
diff
changeset

20 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

21 
syntax (HOL) 
12298  22 
"_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

23 
syntax 
12298  24 
"_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

25 
translations 
13764  26 
"SOME x. P" == "Eps (%x. P)" 
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

27 

f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

28 
print_translation {* 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

29 
(* to avoid etacontraction of body *) 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

30 
[("Eps", fn [Abs abs] => 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

31 
let val (x,t) = atomic_abs_tr' abs 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

32 
in Syntax.const "_Eps" $ x $ t end)] 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13585
diff
changeset

33 
*} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

34 

12298  35 
axioms 
36 
someI: "P (x::'a) ==> P (SOME x. P x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

37 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

38 

12298  39 
constdefs 
40 
inv :: "('a => 'b) => ('b => 'a)" 

41 
"inv(f :: 'a => 'b) == %y. SOME x. f x = y" 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

42 

12298  43 
Inv :: "'a set => ('a => 'b) => ('b => 'a)" 
14760  44 
"Inv A f == %x. SOME y. y \<in> A & f y = x" 
45 

46 

47 
subsection {*Hilbert's Epsilonoperator*} 

48 

49 
text{*Easier to apply than @{text someI} if the witness comes from an 

50 
existential formula*} 

51 
lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)" 

52 
apply (erule exE) 

53 
apply (erule someI) 

54 
done 

55 

56 
text{*Easier to apply than @{text someI} because the conclusion has only one 

57 
occurrence of @{term P}.*} 

58 
lemma someI2: "[ P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)" 

59 
by (blast intro: someI) 

60 

61 
text{*Easier to apply than @{text someI2} if the witness comes from an 

62 
existential formula*} 

63 
lemma someI2_ex: "[ \<exists>a. P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)" 

64 
by (blast intro: someI2) 

65 

66 
lemma some_equality [intro]: 

67 
"[ P a; !!x. P x ==> x=a ] ==> (SOME x. P x) = a" 

68 
by (blast intro: someI2) 

69 

70 
lemma some1_equality: "[ EX!x. P x; P a ] ==> (SOME x. P x) = a" 

71 
by (blast intro: some_equality) 

72 

73 
lemma some_eq_ex: "P (SOME x. P x) = (\<exists>x. P x)" 

74 
by (blast intro: someI) 

75 

76 
lemma some_eq_trivial [simp]: "(SOME y. y=x) = x" 

77 
apply (rule some_equality) 

78 
apply (rule refl, assumption) 

79 
done 

80 

81 
lemma some_sym_eq_trivial [simp]: "(SOME y. x=y) = x" 

82 
apply (rule some_equality) 

83 
apply (rule refl) 

84 
apply (erule sym) 

85 
done 

86 

87 

88 
subsection{*Axiom of Choice, Proved Using the Description Operator*} 

89 

90 
text{*Used in @{text "Tools/meson.ML"}*} 

91 
lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)" 

92 
by (fast elim: someI) 

93 

94 
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)" 

95 
by (fast elim: someI) 

96 

97 

98 
subsection {*Function Inverse*} 

99 

100 
lemma inv_id [simp]: "inv id = id" 

101 
by (simp add: inv_def id_def) 

102 

103 
text{*A onetoone function has an inverse.*} 

104 
lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x" 

105 
by (simp add: inv_def inj_eq) 

106 

107 
lemma inv_f_eq: "[ inj f; f x = y ] ==> inv f y = x" 

108 
apply (erule subst) 

109 
apply (erule inv_f_f) 

110 
done 

111 

112 
lemma inj_imp_inv_eq: "[ inj f; \<forall>x. f(g x) = x ] ==> inv f = g" 

113 
by (blast intro: ext inv_f_eq) 

114 

115 
text{*But is it useful?*} 

116 
lemma inj_transfer: 

117 
assumes injf: "inj f" and minor: "!!y. y \<in> range(f) ==> P(inv f y)" 

118 
shows "P x" 

119 
proof  

120 
have "f x \<in> range f" by auto 

121 
hence "P(inv f (f x))" by (rule minor) 

122 
thus "P x" by (simp add: inv_f_f [OF injf]) 

123 
qed 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

124 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

125 

14760  126 
lemma inj_iff: "(inj f) = (inv f o f = id)" 
127 
apply (simp add: o_def expand_fun_eq) 

128 
apply (blast intro: inj_on_inverseI inv_f_f) 

129 
done 

130 

131 
lemma inj_imp_surj_inv: "inj f ==> surj (inv f)" 

132 
by (blast intro: surjI inv_f_f) 

133 

134 
lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y" 

135 
apply (simp add: inv_def) 

136 
apply (fast intro: someI) 

137 
done 

138 

139 
lemma surj_f_inv_f: "surj f ==> f(inv f y) = y" 

140 
by (simp add: f_inv_f surj_range) 

141 

142 
lemma inv_injective: 

143 
assumes eq: "inv f x = inv f y" 

144 
and x: "x: range f" 

145 
and y: "y: range f" 

146 
shows "x=y" 

147 
proof  

148 
have "f (inv f x) = f (inv f y)" using eq by simp 

149 
thus ?thesis by (simp add: f_inv_f x y) 

150 
qed 

151 

152 
lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A" 

153 
by (fast intro: inj_onI elim: inv_injective injD) 

154 

155 
lemma surj_imp_inj_inv: "surj f ==> inj (inv f)" 

156 
by (simp add: inj_on_inv surj_range) 

157 

158 
lemma surj_iff: "(surj f) = (f o inv f = id)" 

159 
apply (simp add: o_def expand_fun_eq) 

160 
apply (blast intro: surjI surj_f_inv_f) 

161 
done 

162 

163 
lemma surj_imp_inv_eq: "[ surj f; \<forall>x. g(f x) = x ] ==> inv f = g" 

164 
apply (rule ext) 

165 
apply (drule_tac x = "inv f x" in spec) 

166 
apply (simp add: surj_f_inv_f) 

167 
done 

168 

169 
lemma bij_imp_bij_inv: "bij f ==> bij (inv f)" 

170 
by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv) 

12372  171 

14760  172 
lemma inv_equality: "[ !!x. g (f x) = x; !!y. f (g y) = y ] ==> inv f = g" 
173 
apply (rule ext) 

174 
apply (auto simp add: inv_def) 

175 
done 

176 

177 
lemma inv_inv_eq: "bij f ==> inv (inv f) = f" 

178 
apply (rule inv_equality) 

179 
apply (auto simp add: bij_def surj_f_inv_f) 

180 
done 

181 

182 
(** bij(inv f) implies little about f. Consider f::bool=>bool such that 

183 
f(True)=f(False)=True. Then it's consistent with axiom someI that 

184 
inv f could be any function at all, including the identity function. 

185 
If inv f=id then inv f is a bijection, but inj f, surj(f) and 

186 
inv(inv f)=f all fail. 

187 
**) 

188 

189 
lemma o_inv_distrib: "[ bij f; bij g ] ==> inv (f o g) = inv g o inv f" 

190 
apply (rule inv_equality) 

191 
apply (auto simp add: bij_def surj_f_inv_f) 

192 
done 

193 

194 

195 
lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A" 

196 
by (simp add: image_eq_UN surj_f_inv_f) 

197 

198 
lemma image_inv_f_f: "inj f ==> (inv f) ` (f ` A) = A" 

199 
by (simp add: image_eq_UN) 

200 

201 
lemma inv_image_comp: "inj f ==> inv f ` (f`X) = X" 

202 
by (auto simp add: image_def) 

203 

204 
lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}" 

205 
apply auto 

206 
apply (force simp add: bij_is_inj) 

207 
apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric]) 

208 
done 

209 

210 
lemma bij_vimage_eq_inv_image: "bij f ==> f ` A = inv f ` A" 

211 
apply (auto simp add: bij_is_surj [THEN surj_f_inv_f]) 

212 
apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric]) 

213 
done 

214 

215 

216 
subsection {*Inverse of a PIfunction (restricted domain)*} 

217 

218 
lemma Inv_f_f: "[ inj_on f A; x \<in> A ] ==> Inv A f (f x) = x" 

219 
apply (simp add: Inv_def inj_on_def) 

220 
apply (blast intro: someI2) 

221 
done 

222 

223 
lemma f_Inv_f: "y \<in> f`A ==> f (Inv A f y) = y" 

224 
apply (simp add: Inv_def) 

13585  225 
apply (fast intro: someI2) 
226 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

227 

14760  228 
lemma Inv_injective: 
229 
assumes eq: "Inv A f x = Inv A f y" 

230 
and x: "x: f`A" 

231 
and y: "y: f`A" 

232 
shows "x=y" 

233 
proof  

234 
have "f (Inv A f x) = f (Inv A f y)" using eq by simp 

235 
thus ?thesis by (simp add: f_Inv_f x y) 

236 
qed 

237 

238 
lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B" 

239 
apply (rule inj_onI) 

240 
apply (blast intro: inj_onI dest: Inv_injective injD) 

241 
done 

242 

243 
lemma Inv_mem: "[ f ` A = B; x \<in> B ] ==> Inv A f x \<in> A" 

244 
apply (simp add: Inv_def) 

245 
apply (fast intro: someI2) 

246 
done 

247 

248 
lemma Inv_f_eq: "[ inj_on f A; f x = y; x \<in> A ] ==> Inv A f y = x" 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

249 
apply (erule subst) 
14760  250 
apply (erule Inv_f_f, assumption) 
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

251 
done 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

252 

dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

253 
lemma Inv_comp: 
14760  254 
"[ inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A ] ==> 
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

255 
Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x" 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

256 
apply simp 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

257 
apply (rule Inv_f_eq) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

258 
apply (fast intro: comp_inj_on) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

259 
apply (simp add: f_Inv_f Inv_mem) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

260 
apply (simp add: Inv_mem) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

261 
done 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14208
diff
changeset

262 

14760  263 

264 
subsection {*Other Consequences of Hilbert's Epsilon*} 

265 

266 
text {*Hilbert's Epsilon and the @{term split} Operator*} 

267 

268 
text{*Looping simprule*} 

269 
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))" 

270 
by (simp add: split_Pair_apply) 

271 

272 
lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))" 

273 
by (simp add: split_def) 

274 

275 
lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)" 

276 
by blast 

277 

278 

279 
text{*A relation is wellfounded iff it has no infinite descending chain*} 

280 
lemma wf_iff_no_infinite_down_chain: 

281 
"wf r = (~(\<exists>f. \<forall>i. (f(Suc i),f i) \<in> r))" 

282 
apply (simp only: wf_eq_minimal) 

283 
apply (rule iffI) 

284 
apply (rule notI) 

285 
apply (erule exE) 

286 
apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast) 

287 
apply (erule contrapos_np, simp, clarify) 

288 
apply (subgoal_tac "\<forall>n. nat_rec x (%i y. @z. z:Q & (z,y) :r) n \<in> Q") 

289 
apply (rule_tac x = "nat_rec x (%i y. @z. z:Q & (z,y) :r)" in exI) 

290 
apply (rule allI, simp) 

291 
apply (rule someI2_ex, blast, blast) 

292 
apply (rule allI) 

293 
apply (induct_tac "n", simp_all) 

294 
apply (rule someI2_ex, blast+) 

295 
done 

296 

297 
text{*A dynamicallyscoped fact for TFL *} 

12298  298 
lemma tfl_some: "\<forall>P x. P x > P (Eps P)" 
299 
by (blast intro: someI) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

300 

12298  301 

302 
subsection {* Least value operator *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

303 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

304 
constdefs 
12298  305 
LeastM :: "['a => 'b::ord, 'a => bool] => 'a" 
14760  306 
"LeastM m P == SOME x. P x & (\<forall>y. P y > m x <= m y)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

307 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

308 
syntax 
12298  309 
"_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0, 4, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

310 
translations 
12298  311 
"LEAST x WRT m. P" == "LeastM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

312 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

313 
lemma LeastMI2: 
12298  314 
"P x ==> (!!y. P y ==> m x <= m y) 
315 
==> (!!x. P x ==> \<forall>y. P y > m x \<le> m y ==> Q x) 

316 
==> Q (LeastM m P)" 

14760  317 
apply (simp add: LeastM_def) 
14208  318 
apply (rule someI2_ex, blast, blast) 
12298  319 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

320 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

321 
lemma LeastM_equality: 
12298  322 
"P k ==> (!!x. P x ==> m k <= m x) 
323 
==> m (LEAST x WRT m. P x) = (m k::'a::order)" 

14208  324 
apply (rule LeastMI2, assumption, blast) 
12298  325 
apply (blast intro!: order_antisym) 
326 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

327 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

328 
lemma wf_linord_ex_has_least: 
14760  329 
"wf r ==> \<forall>x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k 
330 
==> \<exists>x. P x & (!y. P y > (m x,m y):r^*)" 

12298  331 
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 
14208  332 
apply (drule_tac x = "m`Collect P" in spec, force) 
12298  333 
done 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

334 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

335 
lemma ex_has_least_nat: 
14760  336 
"P k ==> \<exists>x. P x & (\<forall>y. P y > m x <= (m y::nat))" 
12298  337 
apply (simp only: pred_nat_trancl_eq_le [symmetric]) 
338 
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 

16796  339 
apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption) 
12298  340 
done 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

341 

12298  342 
lemma LeastM_nat_lemma: 
14760  343 
"P k ==> P (LeastM m P) & (\<forall>y. P y > m (LeastM m P) <= (m y::nat))" 
344 
apply (simp add: LeastM_def) 

12298  345 
apply (rule someI_ex) 
346 
apply (erule ex_has_least_nat) 

347 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

348 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

349 
lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard] 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

350 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

351 
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" 
14208  352 
by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption) 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

353 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

354 

12298  355 
subsection {* Greatest value operator *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

356 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

357 
constdefs 
12298  358 
GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" 
14760  359 
"GreatestM m P == SOME x. P x & (\<forall>y. P y > m y <= m x)" 
12298  360 

361 
Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) 

362 
"Greatest == GreatestM (%x. x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

363 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

364 
syntax 
12298  365 
"_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" 
366 
("GREATEST _ WRT _. _" [0, 4, 10] 10) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

367 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

368 
translations 
12298  369 
"GREATEST x WRT m. P" == "GreatestM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

370 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

371 
lemma GreatestMI2: 
12298  372 
"P x ==> (!!y. P y ==> m y <= m x) 
373 
==> (!!x. P x ==> \<forall>y. P y > m y \<le> m x ==> Q x) 

374 
==> Q (GreatestM m P)" 

14760  375 
apply (simp add: GreatestM_def) 
14208  376 
apply (rule someI2_ex, blast, blast) 
12298  377 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

378 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

379 
lemma GreatestM_equality: 
12298  380 
"P k ==> (!!x. P x ==> m x <= m k) 
381 
==> m (GREATEST x WRT m. P x) = (m k::'a::order)" 

14208  382 
apply (rule_tac m = m in GreatestMI2, assumption, blast) 
12298  383 
apply (blast intro!: order_antisym) 
384 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

385 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

386 
lemma Greatest_equality: 
12298  387 
"P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k" 
14760  388 
apply (simp add: Greatest_def) 
14208  389 
apply (erule GreatestM_equality, blast) 
12298  390 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

391 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

392 
lemma ex_has_greatest_nat_lemma: 
14760  393 
"P k ==> \<forall>x. P x > (\<exists>y. P y & ~ ((m y::nat) <= m x)) 
394 
==> \<exists>y. P y & ~ (m y < m k + n)" 

15251  395 
apply (induct n, force) 
12298  396 
apply (force simp add: le_Suc_eq) 
397 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

398 

12298  399 
lemma ex_has_greatest_nat: 
14760  400 
"P k ==> \<forall>y. P y > m y < b 
401 
==> \<exists>x. P x & (\<forall>y. P y > (m y::nat) <= m x)" 

12298  402 
apply (rule ccontr) 
403 
apply (cut_tac P = P and n = "b  m k" in ex_has_greatest_nat_lemma) 

14208  404 
apply (subgoal_tac [3] "m k <= b", auto) 
12298  405 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

406 

12298  407 
lemma GreatestM_nat_lemma: 
14760  408 
"P k ==> \<forall>y. P y > m y < b 
409 
==> P (GreatestM m P) & (\<forall>y. P y > (m y::nat) <= m (GreatestM m P))" 

410 
apply (simp add: GreatestM_def) 

12298  411 
apply (rule someI_ex) 
14208  412 
apply (erule ex_has_greatest_nat, assumption) 
12298  413 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

414 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

415 
lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

416 

12298  417 
lemma GreatestM_nat_le: 
14760  418 
"P x ==> \<forall>y. P y > m y < b 
12298  419 
==> (m x::nat) <= m (GreatestM m P)" 
420 
apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 

421 
done 

422 

423 

424 
text {* \medskip Specialization to @{text GREATEST}. *} 

425 

14760  426 
lemma GreatestI: "P (k::nat) ==> \<forall>y. P y > y < b ==> P (GREATEST x. P x)" 
427 
apply (simp add: Greatest_def) 

14208  428 
apply (rule GreatestM_natI, auto) 
12298  429 
done 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

430 

12298  431 
lemma Greatest_le: 
14760  432 
"P x ==> \<forall>y. P y > y < b ==> (x::nat) <= (GREATEST x. P x)" 
433 
apply (simp add: Greatest_def) 

14208  434 
apply (rule GreatestM_nat_le, auto) 
12298  435 
done 
436 

437 

438 
subsection {* The Meson proof procedure *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

439 

12298  440 
subsubsection {* Negation Normal Form *} 
441 

442 
text {* de Morgan laws *} 

443 

444 
lemma meson_not_conjD: "~(P&Q) ==> ~P  ~Q" 

445 
and meson_not_disjD: "~(PQ) ==> ~P & ~Q" 

446 
and meson_not_notD: "~~P ==> P" 

14760  447 
and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)" 
448 
and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)" 

12298  449 
by fast+ 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

450 

12298  451 
text {* Removal of @{text ">"} and @{text "<>"} (positive and 
452 
negative occurrences) *} 

453 

454 
lemma meson_imp_to_disjD: "P>Q ==> ~P  Q" 

455 
and meson_not_impD: "~(P>Q) ==> P & ~Q" 

456 
and meson_iff_to_disjD: "P=Q ==> (~P  Q) & (~Q  P)" 

457 
and meson_not_iffD: "~(P=Q) ==> (P  Q) & (~P  ~Q)" 

458 
 {* Much more efficient than @{prop "(P & ~Q)  (Q & ~P)"} for computing CNF *} 

459 
by fast+ 

460 

461 

462 
subsubsection {* Pulling out the existential quantifiers *} 

463 

464 
text {* Conjunction *} 

465 

14760  466 
lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q" 
467 
and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)" 

12298  468 
by fast+ 
469 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

470 

12298  471 
text {* Disjunction *} 
472 

14760  473 
lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x))  (\<exists>x. Q(x)) ==> \<exists>x. P(x)  Q(x)" 
12298  474 
 {* DO NOT USE with forallSkolemization: makes fewer schematic variables!! *} 
475 
 {* With exSkolemization, makes fewer Skolem constants *} 

14760  476 
and meson_disj_exD1: "!!P Q. (\<exists>x. P(x))  Q ==> \<exists>x. P(x)  Q" 
477 
and meson_disj_exD2: "!!P Q. P  (\<exists>x. Q(x)) ==> \<exists>x. P  Q(x)" 

12298  478 
by fast+ 
479 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

480 

12298  481 
subsubsection {* Generating clauses for the Meson Proof Procedure *} 
482 

483 
text {* Disjunctions *} 

484 

485 
lemma meson_disj_assoc: "(PQ)R ==> P(QR)" 

486 
and meson_disj_comm: "PQ ==> QP" 

487 
and meson_disj_FalseD1: "FalseP ==> P" 

488 
and meson_disj_FalseD2: "PFalse ==> P" 

489 
by fast+ 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

490 

14760  491 

492 
subsection{*Lemmas for Meson, the Model Elimination Procedure*} 

493 

494 

495 
text{* Generation of contrapositives *} 

496 

497 
text{*Inserts negated disjunct after removing the negation; P is a literal. 

498 
Model elimination requires assuming the negation of every attempted subgoal, 

499 
hence the negated disjuncts.*} 

500 
lemma make_neg_rule: "~PQ ==> ((~P==>P) ==> Q)" 

501 
by blast 

502 

503 
text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} 

504 
lemma make_refined_neg_rule: "~PQ ==> (P ==> Q)" 

505 
by blast 

506 

507 
text{*@{term P} should be a literal*} 

508 
lemma make_pos_rule: "PQ ==> ((P==>~P) ==> Q)" 

509 
by blast 

510 

511 
text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't 

512 
insert new assumptions, for ordinary resolution.*} 

513 

514 
lemmas make_neg_rule' = make_refined_neg_rule 

515 

516 
lemma make_pos_rule': "[PQ; ~P] ==> Q" 

517 
by blast 

518 

519 
text{* Generation of a goal clause  put away the final literal *} 

520 

521 
lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" 

522 
by blast 

523 

524 
lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" 

525 
by blast 

526 

527 

528 
subsubsection{* Lemmas for Forward Proof*} 

529 

530 
text{*There is a similarity to congruence rules*} 

531 

532 
(*NOTE: could handle conjunctions (faster?) by 

533 
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) 

534 
lemma conj_forward: "[ P'&Q'; P' ==> P; Q' ==> Q ] ==> P&Q" 

535 
by blast 

536 

537 
lemma disj_forward: "[ P'Q'; P' ==> P; Q' ==> Q ] ==> PQ" 

538 
by blast 

539 

540 
(*Version of @{text disj_forward} for removal of duplicate literals*) 

541 
lemma disj_forward2: 

542 
"[ P'Q'; P' ==> P; [ Q'; P==>False ] ==> Q ] ==> PQ" 

543 
apply blast 

544 
done 

545 

546 
lemma all_forward: "[ \<forall>x. P'(x); !!x. P'(x) ==> P(x) ] ==> \<forall>x. P(x)" 

547 
by blast 

548 

549 
lemma ex_forward: "[ \<exists>x. P'(x); !!x. P'(x) ==> P(x) ] ==> \<exists>x. P(x)" 

550 
by blast 

551 

17420  552 

553 
text{*Many of these bindings are used by the ATP linkup, and not just by 

554 
legacy proof scripts.*} 

14760  555 
ML 
556 
{* 

557 
val inv_def = thm "inv_def"; 

558 
val Inv_def = thm "Inv_def"; 

559 

560 
val someI = thm "someI"; 

561 
val someI_ex = thm "someI_ex"; 

562 
val someI2 = thm "someI2"; 

563 
val someI2_ex = thm "someI2_ex"; 

564 
val some_equality = thm "some_equality"; 

565 
val some1_equality = thm "some1_equality"; 

566 
val some_eq_ex = thm "some_eq_ex"; 

567 
val some_eq_trivial = thm "some_eq_trivial"; 

568 
val some_sym_eq_trivial = thm "some_sym_eq_trivial"; 

569 
val choice = thm "choice"; 

570 
val bchoice = thm "bchoice"; 

571 
val inv_id = thm "inv_id"; 

572 
val inv_f_f = thm "inv_f_f"; 

573 
val inv_f_eq = thm "inv_f_eq"; 

574 
val inj_imp_inv_eq = thm "inj_imp_inv_eq"; 

575 
val inj_transfer = thm "inj_transfer"; 

576 
val inj_iff = thm "inj_iff"; 

577 
val inj_imp_surj_inv = thm "inj_imp_surj_inv"; 

578 
val f_inv_f = thm "f_inv_f"; 

579 
val surj_f_inv_f = thm "surj_f_inv_f"; 

580 
val inv_injective = thm "inv_injective"; 

581 
val inj_on_inv = thm "inj_on_inv"; 

582 
val surj_imp_inj_inv = thm "surj_imp_inj_inv"; 

583 
val surj_iff = thm "surj_iff"; 

584 
val surj_imp_inv_eq = thm "surj_imp_inv_eq"; 

585 
val bij_imp_bij_inv = thm "bij_imp_bij_inv"; 

586 
val inv_equality = thm "inv_equality"; 

587 
val inv_inv_eq = thm "inv_inv_eq"; 

588 
val o_inv_distrib = thm "o_inv_distrib"; 

589 
val image_surj_f_inv_f = thm "image_surj_f_inv_f"; 

590 
val image_inv_f_f = thm "image_inv_f_f"; 

591 
val inv_image_comp = thm "inv_image_comp"; 

592 
val bij_image_Collect_eq = thm "bij_image_Collect_eq"; 

593 
val bij_vimage_eq_inv_image = thm "bij_vimage_eq_inv_image"; 

594 
val Inv_f_f = thm "Inv_f_f"; 

595 
val f_Inv_f = thm "f_Inv_f"; 

596 
val Inv_injective = thm "Inv_injective"; 

597 
val inj_on_Inv = thm "inj_on_Inv"; 

598 
val split_paired_Eps = thm "split_paired_Eps"; 

599 
val Eps_split = thm "Eps_split"; 

600 
val Eps_split_eq = thm "Eps_split_eq"; 

601 
val wf_iff_no_infinite_down_chain = thm "wf_iff_no_infinite_down_chain"; 

602 
val Inv_mem = thm "Inv_mem"; 

603 
val Inv_f_eq = thm "Inv_f_eq"; 

604 
val Inv_comp = thm "Inv_comp"; 

605 
val tfl_some = thm "tfl_some"; 

606 
val make_neg_rule = thm "make_neg_rule"; 

607 
val make_refined_neg_rule = thm "make_refined_neg_rule"; 

608 
val make_pos_rule = thm "make_pos_rule"; 

609 
val make_neg_rule' = thm "make_neg_rule'"; 

610 
val make_pos_rule' = thm "make_pos_rule'"; 

611 
val make_neg_goal = thm "make_neg_goal"; 

612 
val make_pos_goal = thm "make_pos_goal"; 

613 
val conj_forward = thm "conj_forward"; 

614 
val disj_forward = thm "disj_forward"; 

615 
val disj_forward2 = thm "disj_forward2"; 

616 
val all_forward = thm "all_forward"; 

617 
val ex_forward = thm "ex_forward"; 

618 
*} 

619 

620 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

621 
use "Tools/meson.ML" 
16563  622 
setup Meson.skolemize_setup 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

623 

14115  624 
use "Tools/specification_package.ML" 
625 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

626 
end 