author  nipkow 
Sun, 22 Dec 2002 15:02:40 +0100  
changeset 13764  3e180bf68496 
parent 13763  f94b569cd610 
child 14115  65ec3f73d00b 
permissions  rwrr 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

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

2 
ID: $Id$ 
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 

12023  7 
header {* Hilbert's epsilonoperator and everything to do with the Axiom of Choice *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

8 

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

9 
theory Hilbert_Choice = NatArith 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

10 
files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"): 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

11 

12298  12 

13 
subsection {* Hilbert's epsilon *} 

14 

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

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

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

17 

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

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

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

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

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

26 

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

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

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

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

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

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

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

33 

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

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

36 

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

37 

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

40 
"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

41 

12298  42 
Inv :: "'a set => ('a => 'b) => ('b => 'a)" 
43 
"Inv A f == %x. SOME y. y : A & f y = x" 

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

44 

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

45 

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

46 
use "Hilbert_Choice_lemmas.ML" 
12372  47 
declare someI_ex [elim?]; 
48 

13585  49 
lemma Inv_mem: "[ f ` A = B; x \<in> B ] ==> Inv A f x \<in> A" 
50 
apply (unfold Inv_def) 

51 
apply (fast intro: someI2) 

52 
done 

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

53 

12298  54 
lemma tfl_some: "\<forall>P x. P x > P (Eps P)" 
55 
 {* dynamicallyscoped fact for TFL *} 

56 
by (blast intro: someI) 

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

57 

12298  58 

59 
subsection {* Least value operator *} 

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

60 

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

61 
constdefs 
12298  62 
LeastM :: "['a => 'b::ord, 'a => bool] => 'a" 
63 
"LeastM m P == SOME x. P x & (ALL y. P y > m x <= m y)" 

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

64 

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

65 
syntax 
12298  66 
"_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

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

69 

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

70 
lemma LeastMI2: 
12298  71 
"P x ==> (!!y. P y ==> m x <= m y) 
72 
==> (!!x. P x ==> \<forall>y. P y > m x \<le> m y ==> Q x) 

73 
==> Q (LeastM m P)" 

74 
apply (unfold LeastM_def) 

75 
apply (rule someI2_ex) 

76 
apply blast 

77 
apply blast 

78 
done 

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

79 

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

80 
lemma LeastM_equality: 
12298  81 
"P k ==> (!!x. P x ==> m k <= m x) 
82 
==> m (LEAST x WRT m. P x) = (m k::'a::order)" 

83 
apply (rule LeastMI2) 

84 
apply assumption 

85 
apply blast 

86 
apply (blast intro!: order_antisym) 

87 
done 

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

88 

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

89 
lemma wf_linord_ex_has_least: 
12298  90 
"wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k 
91 
==> EX x. P x & (!y. P y > (m x,m y):r^*)" 

92 
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 

93 
apply (drule_tac x = "m`Collect P" in spec) 

94 
apply force 

95 
done 

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

96 

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

97 
lemma ex_has_least_nat: 
12298  98 
"P k ==> EX x. P x & (ALL y. P y > m x <= (m y::nat))" 
99 
apply (simp only: pred_nat_trancl_eq_le [symmetric]) 

100 
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 

101 
apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le) 

102 
apply assumption 

103 
done 

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

104 

12298  105 
lemma LeastM_nat_lemma: 
106 
"P k ==> P (LeastM m P) & (ALL y. P y > m (LeastM m P) <= (m y::nat))" 

107 
apply (unfold LeastM_def) 

108 
apply (rule someI_ex) 

109 
apply (erule ex_has_least_nat) 

110 
done 

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

111 

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

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

113 

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

114 
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" 
12298  115 
apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) 
116 
apply assumption 

117 
apply assumption 

118 
done 

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

119 

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

120 

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

122 

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

123 
constdefs 
12298  124 
GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" 
125 
"GreatestM m P == SOME x. P x & (ALL y. P y > m y <= m x)" 

126 

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

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

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

129 

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

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

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

133 

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

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

136 

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

137 
lemma GreatestMI2: 
12298  138 
"P x ==> (!!y. P y ==> m y <= m x) 
139 
==> (!!x. P x ==> \<forall>y. P y > m y \<le> m x ==> Q x) 

140 
==> Q (GreatestM m P)" 

141 
apply (unfold GreatestM_def) 

142 
apply (rule someI2_ex) 

143 
apply blast 

144 
apply blast 

145 
done 

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

146 

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

147 
lemma GreatestM_equality: 
12298  148 
"P k ==> (!!x. P x ==> m x <= m k) 
149 
==> m (GREATEST x WRT m. P x) = (m k::'a::order)" 

150 
apply (rule_tac m = m in GreatestMI2) 

151 
apply assumption 

152 
apply blast 

153 
apply (blast intro!: order_antisym) 

154 
done 

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

155 

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

156 
lemma Greatest_equality: 
12298  157 
"P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k" 
158 
apply (unfold Greatest_def) 

159 
apply (erule GreatestM_equality) 

160 
apply blast 

161 
done 

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

162 

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

163 
lemma ex_has_greatest_nat_lemma: 
12298  164 
"P k ==> ALL x. P x > (EX y. P y & ~ ((m y::nat) <= m x)) 
165 
==> EX y. P y & ~ (m y < m k + n)" 

166 
apply (induct_tac n) 

167 
apply force 

168 
apply (force simp add: le_Suc_eq) 

169 
done 

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

170 

12298  171 
lemma ex_has_greatest_nat: 
172 
"P k ==> ALL y. P y > m y < b 

173 
==> EX x. P x & (ALL y. P y > (m y::nat) <= m x)" 

174 
apply (rule ccontr) 

175 
apply (cut_tac P = P and n = "b  m k" in ex_has_greatest_nat_lemma) 

176 
apply (subgoal_tac [3] "m k <= b") 

177 
apply auto 

178 
done 

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

179 

12298  180 
lemma GreatestM_nat_lemma: 
181 
"P k ==> ALL y. P y > m y < b 

182 
==> P (GreatestM m P) & (ALL y. P y > (m y::nat) <= m (GreatestM m P))" 

183 
apply (unfold GreatestM_def) 

184 
apply (rule someI_ex) 

185 
apply (erule ex_has_greatest_nat) 

186 
apply assumption 

187 
done 

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

188 

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

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

190 

12298  191 
lemma GreatestM_nat_le: 
192 
"P x ==> ALL y. P y > m y < b 

193 
==> (m x::nat) <= m (GreatestM m P)" 

194 
apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 

195 
done 

196 

197 

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

199 

200 
lemma GreatestI: "P (k::nat) ==> ALL y. P y > y < b ==> P (GREATEST x. P x)" 

201 
apply (unfold Greatest_def) 

202 
apply (rule GreatestM_natI) 

203 
apply auto 

204 
done 

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

205 

12298  206 
lemma Greatest_le: 
207 
"P x ==> ALL y. P y > y < b ==> (x::nat) <= (GREATEST x. P x)" 

208 
apply (unfold Greatest_def) 

209 
apply (rule GreatestM_nat_le) 

210 
apply auto 

211 
done 

212 

213 

214 
subsection {* The Meson proof procedure *} 

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

215 

12298  216 
subsubsection {* Negation Normal Form *} 
217 

218 
text {* de Morgan laws *} 

219 

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

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

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

223 
and meson_not_allD: "!!P. ~(ALL x. P(x)) ==> EX x. ~P(x)" 

224 
and meson_not_exD: "!!P. ~(EX x. P(x)) ==> ALL x. ~P(x)" 

225 
by fast+ 

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

226 

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

229 

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

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

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

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

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

235 
by fast+ 

236 

237 

238 
subsubsection {* Pulling out the existential quantifiers *} 

239 

240 
text {* Conjunction *} 

241 

242 
lemma meson_conj_exD1: "!!P Q. (EX x. P(x)) & Q ==> EX x. P(x) & Q" 

243 
and meson_conj_exD2: "!!P Q. P & (EX x. Q(x)) ==> EX x. P & Q(x)" 

244 
by fast+ 

245 

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

246 

12298  247 
text {* Disjunction *} 
248 

249 
lemma meson_disj_exD: "!!P Q. (EX x. P(x))  (EX x. Q(x)) ==> EX x. P(x)  Q(x)" 

250 
 {* DO NOT USE with forallSkolemization: makes fewer schematic variables!! *} 

251 
 {* With exSkolemization, makes fewer Skolem constants *} 

252 
and meson_disj_exD1: "!!P Q. (EX x. P(x))  Q ==> EX x. P(x)  Q" 

253 
and meson_disj_exD2: "!!P Q. P  (EX x. Q(x)) ==> EX x. P  Q(x)" 

254 
by fast+ 

255 

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

256 

12298  257 
subsubsection {* Generating clauses for the Meson Proof Procedure *} 
258 

259 
text {* Disjunctions *} 

260 

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

262 
and meson_disj_comm: "PQ ==> QP" 

263 
and meson_disj_FalseD1: "FalseP ==> P" 

264 
and meson_disj_FalseD2: "PFalse ==> P" 

265 
by fast+ 

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

266 

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

267 
use "meson_lemmas.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

268 
use "Tools/meson.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

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

270 

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

271 
end 