author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47040  78e88d26f19d 
child 50705  0e943b33d907 
permissions  rwrr 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
38991
diff
changeset

1 
(* Title: HOL/Metis_Examples/Tarski.thy 
43197  2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
41144  3 
Author: Jasmin Blanchette, TU Muenchen 
23449  4 

43197  5 
Metis example featuring the full theorem of Tarski. 
23449  6 
*) 
7 

43197  8 
header {* Metis Example Featuring the Full Theorem of Tarski *} 
23449  9 

27368  10 
theory Tarski 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41144
diff
changeset

11 
imports Main "~~/src/HOL/Library/FuncSet" 
27368  12 
begin 
23449  13 

42103
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41413
diff
changeset

14 
declare [[metis_new_skolemizer]] 
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41413
diff
changeset

15 

23449  16 
(*Many of these higherorder problems appear to be impossible using the 
17 
current linkup. They often seem to need either higherorder unification 

18 
or explicit reasoning about connectives such as conjunction. The numerous 

19 
set comprehensions are to blame.*) 

20 

21 
record 'a potype = 

22 
pset :: "'a set" 

23 
order :: "('a * 'a) set" 

24 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

25 
definition monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" where 
23449  26 
"monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r > ((f x), (f y)) : r" 
27 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

28 
definition least :: "['a => bool, 'a potype] => 'a" where 
23449  29 
"least P po == @ x. x: pset po & P x & 
30 
(\<forall>y \<in> pset po. P y > (x,y): order po)" 

31 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

32 
definition greatest :: "['a => bool, 'a potype] => 'a" where 
23449  33 
"greatest P po == @ x. x: pset po & P x & 
34 
(\<forall>y \<in> pset po. P y > (y,x): order po)" 

35 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

36 
definition lub :: "['a set, 'a potype] => 'a" where 
23449  37 
"lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po" 
38 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

39 
definition glb :: "['a set, 'a potype] => 'a" where 
23449  40 
"glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po" 
41 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

42 
definition isLub :: "['a set, 'a potype, 'a] => bool" where 
23449  43 
"isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) & 
44 
(\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) > (L,z): order po))" 

45 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

46 
definition isGlb :: "['a set, 'a potype, 'a] => bool" where 
23449  47 
"isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) & 
48 
(\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) > (z,G): order po))" 

49 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

50 
definition "fix" :: "[('a => 'a), 'a set] => 'a set" where 
23449  51 
"fix f A == {x. x: A & f x = x}" 
52 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

53 
definition interval :: "[('a*'a) set,'a, 'a ] => 'a set" where 
23449  54 
"interval r a b == {x. (a,x): r & (x,b): r}" 
55 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

56 
definition Bot :: "'a potype => 'a" where 
23449  57 
"Bot po == least (%x. True) po" 
58 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

59 
definition Top :: "'a potype => 'a" where 
23449  60 
"Top po == greatest (%x. True) po" 
61 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

62 
definition PartialOrder :: "('a potype) set" where 
30198  63 
"PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) & 
23449  64 
trans (order P)}" 
65 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

66 
definition CompleteLattice :: "('a potype) set" where 
23449  67 
"CompleteLattice == {cl. cl: PartialOrder & 
68 
(\<forall>S. S \<subseteq> pset cl > (\<exists>L. isLub S cl L)) & 

69 
(\<forall>S. S \<subseteq> pset cl > (\<exists>G. isGlb S cl G))}" 

70 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

71 
definition induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where 
23449  72 
"induced A r == {(a,b). a : A & b: A & (a,b): r}" 
73 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

74 
definition sublattice :: "('a potype * 'a set)set" where 
23449  75 
"sublattice == 
76 
SIGMA cl: CompleteLattice. 

77 
{S. S \<subseteq> pset cl & 

78 
( pset = S, order = induced S (order cl) ): CompleteLattice }" 

79 

35054  80 
abbreviation 
81 
sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50) 

82 
where "S <<= cl \<equiv> S : sublattice `` {cl}" 

23449  83 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

84 
definition dual :: "'a potype => 'a potype" where 
23449  85 
"dual po == ( pset = pset po, order = converse (order po) )" 
86 

27681  87 
locale PO = 
23449  88 
fixes cl :: "'a potype" 
89 
and A :: "'a set" 

90 
and r :: "('a * 'a) set" 

91 
assumes cl_po: "cl : PartialOrder" 

92 
defines A_def: "A == pset cl" 

93 
and r_def: "r == order cl" 

94 

27681  95 
locale CL = PO + 
23449  96 
assumes cl_co: "cl : CompleteLattice" 
97 

27681  98 
definition CLF_set :: "('a potype * ('a => 'a)) set" where 
99 
"CLF_set = (SIGMA cl: CompleteLattice. 

100 
{f. f: pset cl > pset cl & monotone f (pset cl) (order cl)})" 

101 

102 
locale CLF = CL + 

23449  103 
fixes f :: "'a => 'a" 
104 
and P :: "'a set" 

27681  105 
assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF``{cl}"*) 
23449  106 
defines P_def: "P == fix f A" 
107 

27681  108 
locale Tarski = CLF + 
23449  109 
fixes Y :: "'a set" 
110 
and intY1 :: "'a set" 

111 
and v :: "'a" 

112 
assumes 

113 
Y_ss: "Y \<subseteq> P" 

114 
defines 

115 
intY1_def: "intY1 == interval r (lub Y cl) (Top cl)" 

116 
and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & 

117 
x: intY1} 

118 
( pset=intY1, order=induced intY1 r)" 

119 

120 
subsection {* Partial Order *} 

121 

30198  122 
lemma (in PO) PO_imp_refl_on: "refl_on A r" 
23449  123 
apply (insert cl_po) 
124 
apply (simp add: PartialOrder_def A_def r_def) 

125 
done 

126 

127 
lemma (in PO) PO_imp_sym: "antisym r" 

128 
apply (insert cl_po) 

129 
apply (simp add: PartialOrder_def r_def) 

130 
done 

131 

132 
lemma (in PO) PO_imp_trans: "trans r" 

133 
apply (insert cl_po) 

134 
apply (simp add: PartialOrder_def r_def) 

135 
done 

136 

137 
lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r" 

138 
apply (insert cl_po) 

30198  139 
apply (simp add: PartialOrder_def refl_on_def A_def r_def) 
23449  140 
done 
141 

142 
lemma (in PO) antisymE: "[ (a, b) \<in> r; (b, a) \<in> r ] ==> a = b" 

143 
apply (insert cl_po) 

144 
apply (simp add: PartialOrder_def antisym_def r_def) 

145 
done 

146 

147 
lemma (in PO) transE: "[ (a, b) \<in> r; (b, c) \<in> r] ==> (a,c) \<in> r" 

148 
apply (insert cl_po) 

149 
apply (simp add: PartialOrder_def r_def) 

150 
apply (unfold trans_def, fast) 

151 
done 

152 

153 
lemma (in PO) monotoneE: 

154 
"[ monotone f A r; x \<in> A; y \<in> A; (x, y) \<in> r ] ==> (f x, f y) \<in> r" 

155 
by (simp add: monotone_def) 

156 

157 
lemma (in PO) po_subset_po: 

158 
"S \<subseteq> A ==> ( pset = S, order = induced S r ) \<in> PartialOrder" 

159 
apply (simp (no_asm) add: PartialOrder_def) 

160 
apply auto 

161 
 {* refl *} 

30198  162 
apply (simp add: refl_on_def induced_def) 
23449  163 
apply (blast intro: reflE) 
164 
 {* antisym *} 

165 
apply (simp add: antisym_def induced_def) 

166 
apply (blast intro: antisymE) 

167 
 {* trans *} 

168 
apply (simp add: trans_def induced_def) 

169 
apply (blast intro: transE) 

170 
done 

171 

172 
lemma (in PO) indE: "[ (x, y) \<in> induced S r; S \<subseteq> A ] ==> (x, y) \<in> r" 

173 
by (simp add: add: induced_def) 

174 

175 
lemma (in PO) indI: "[ (x, y) \<in> r; x \<in> S; y \<in> S ] ==> (x, y) \<in> induced S r" 

176 
by (simp add: add: induced_def) 

177 

178 
lemma (in CL) CL_imp_ex_isLub: "S \<subseteq> A ==> \<exists>L. isLub S cl L" 

179 
apply (insert cl_co) 

180 
apply (simp add: CompleteLattice_def A_def) 

181 
done 

182 

183 
declare (in CL) cl_co [simp] 

184 

185 
lemma isLub_lub: "(\<exists>L. isLub S cl L) = isLub S cl (lub S cl)" 

186 
by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric]) 

187 

188 
lemma isGlb_glb: "(\<exists>G. isGlb S cl G) = isGlb S cl (glb S cl)" 

189 
by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric]) 

190 

191 
lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45970
diff
changeset

192 
by (simp add: isLub_def isGlb_def dual_def converse_unfold) 
23449  193 

194 
lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45970
diff
changeset

195 
by (simp add: isLub_def isGlb_def dual_def converse_unfold) 
23449  196 

197 
lemma (in PO) dualPO: "dual cl \<in> PartialOrder" 

198 
apply (insert cl_po) 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

199 
apply (simp add: PartialOrder_def dual_def) 
23449  200 
done 
201 

202 
lemma Rdual: 

203 
"\<forall>S. (S \<subseteq> A >( \<exists>L. isLub S ( pset = A, order = r) L)) 

204 
==> \<forall>S. (S \<subseteq> A > (\<exists>G. isGlb S ( pset = A, order = r) G))" 

205 
apply safe 

206 
apply (rule_tac x = "lub {y. y \<in> A & (\<forall>k \<in> S. (y, k) \<in> r)} 

207 
(pset = A, order = r) " in exI) 

208 
apply (drule_tac x = "{y. y \<in> A & (\<forall>k \<in> S. (y,k) \<in> r) }" in spec) 

209 
apply (drule mp, fast) 

210 
apply (simp add: isLub_lub isGlb_def) 

211 
apply (simp add: isLub_def, blast) 

212 
done 

213 

214 
lemma lub_dual_glb: "lub S cl = glb S (dual cl)" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45970
diff
changeset

215 
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold) 
23449  216 

217 
lemma glb_dual_lub: "glb S cl = lub S (dual cl)" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45970
diff
changeset

218 
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold) 
23449  219 

220 
lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder" 

221 
by (simp add: PartialOrder_def CompleteLattice_def, fast) 

222 

223 
lemmas CL_imp_PO = CL_subset_PO [THEN subsetD] 

224 

30198  225 
declare PO.PO_imp_refl_on [OF PO.intro [OF CL_imp_PO], simp] 
27681  226 
declare PO.PO_imp_sym [OF PO.intro [OF CL_imp_PO], simp] 
227 
declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp] 

23449  228 

30198  229 
lemma (in CL) CO_refl_on: "refl_on A r" 
230 
by (rule PO_imp_refl_on) 

23449  231 

232 
lemma (in CL) CO_antisym: "antisym r" 

233 
by (rule PO_imp_sym) 

234 

235 
lemma (in CL) CO_trans: "trans r" 

236 
by (rule PO_imp_trans) 

237 

238 
lemma CompleteLatticeI: 

239 
"[ po \<in> PartialOrder; (\<forall>S. S \<subseteq> pset po > (\<exists>L. isLub S po L)); 

240 
(\<forall>S. S \<subseteq> pset po > (\<exists>G. isGlb S po G))] 

241 
==> po \<in> CompleteLattice" 

242 
apply (unfold CompleteLattice_def, blast) 

243 
done 

244 

245 
lemma (in CL) CL_dualCL: "dual cl \<in> CompleteLattice" 

246 
apply (insert cl_co) 

247 
apply (simp add: CompleteLattice_def dual_def) 

248 
apply (fold dual_def) 

249 
apply (simp add: isLub_dual_isGlb [symmetric] isGlb_dual_isLub [symmetric] 

250 
dualPO) 

251 
done 

252 

253 
lemma (in PO) dualA_iff: "pset (dual cl) = pset cl" 

254 
by (simp add: dual_def) 

255 

256 
lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)" 

257 
by (simp add: dual_def) 

258 

259 
lemma (in PO) monotone_dual: 

43197  260 
"monotone f (pset cl) (order cl) 
23449  261 
==> monotone f (pset (dual cl)) (order(dual cl))" 
262 
by (simp add: monotone_def dualA_iff dualr_iff) 

263 

264 
lemma (in PO) interval_dual: 

265 
"[ x \<in> A; y \<in> A] ==> interval r x y = interval (order(dual cl)) y x" 

266 
apply (simp add: interval_def dualr_iff) 

267 
apply (fold r_def, fast) 

268 
done 

269 

270 
lemma (in PO) interval_not_empty: 

271 
"[ trans r; interval r a b \<noteq> {} ] ==> (a, b) \<in> r" 

272 
apply (simp add: interval_def) 

273 
apply (unfold trans_def, blast) 

274 
done 

275 

276 
lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r" 

277 
by (simp add: interval_def) 

278 

279 
lemma (in PO) left_in_interval: 

280 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {} ] ==> a \<in> interval r a b" 

281 
apply (simp (no_asm_simp) add: interval_def) 

282 
apply (simp add: PO_imp_trans interval_not_empty) 

283 
apply (simp add: reflE) 

284 
done 

285 

286 
lemma (in PO) right_in_interval: 

287 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {} ] ==> b \<in> interval r a b" 

288 
apply (simp (no_asm_simp) add: interval_def) 

289 
apply (simp add: PO_imp_trans interval_not_empty) 

290 
apply (simp add: reflE) 

291 
done 

292 

293 
subsection {* sublattice *} 

294 

295 
lemma (in PO) sublattice_imp_CL: 

296 
"S <<= cl ==> ( pset = S, order = induced S r ) \<in> CompleteLattice" 

297 
by (simp add: sublattice_def CompleteLattice_def A_def r_def) 

298 

299 
lemma (in CL) sublatticeI: 

300 
"[ S \<subseteq> A; ( pset = S, order = induced S r ) \<in> CompleteLattice ] 

301 
==> S <<= cl" 

302 
by (simp add: sublattice_def A_def r_def) 

303 

304 
subsection {* lub *} 

305 

306 
lemma (in CL) lub_unique: "[ S \<subseteq> A; isLub S cl x; isLub S cl L] ==> x = L" 

307 
apply (rule antisymE) 

308 
apply (auto simp add: isLub_def r_def) 

309 
done 

310 

311 
lemma (in CL) lub_upper: "[S \<subseteq> A; x \<in> S] ==> (x, lub S cl) \<in> r" 

312 
apply (rule CL_imp_ex_isLub [THEN exE], assumption) 

313 
apply (unfold lub_def least_def) 

314 
apply (rule some_equality [THEN ssubst]) 

315 
apply (simp add: isLub_def) 

316 
apply (simp add: lub_unique A_def isLub_def) 

317 
apply (simp add: isLub_def r_def) 

318 
done 

319 

320 
lemma (in CL) lub_least: 

321 
"[ S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r ] ==> (lub S cl, L) \<in> r" 

322 
apply (rule CL_imp_ex_isLub [THEN exE], assumption) 

323 
apply (unfold lub_def least_def) 

324 
apply (rule_tac s=x in some_equality [THEN ssubst]) 

325 
apply (simp add: isLub_def) 

326 
apply (simp add: lub_unique A_def isLub_def) 

327 
apply (simp add: isLub_def r_def A_def) 

328 
done 

329 

330 
lemma (in CL) lub_in_lattice: "S \<subseteq> A ==> lub S cl \<in> A" 

331 
apply (rule CL_imp_ex_isLub [THEN exE], assumption) 

332 
apply (unfold lub_def least_def) 

333 
apply (subst some_equality) 

334 
apply (simp add: isLub_def) 

335 
prefer 2 apply (simp add: isLub_def A_def) 

336 
apply (simp add: lub_unique A_def isLub_def) 

337 
done 

338 

339 
lemma (in CL) lubI: 

340 
"[ S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r; 

341 
\<forall>z \<in> A. (\<forall>y \<in> S. (y,z) \<in> r) > (L,z) \<in> r ] ==> L = lub S cl" 

342 
apply (rule lub_unique, assumption) 

343 
apply (simp add: isLub_def A_def r_def) 

344 
apply (unfold isLub_def) 

345 
apply (rule conjI) 

346 
apply (fold A_def r_def) 

347 
apply (rule lub_in_lattice, assumption) 

348 
apply (simp add: lub_upper lub_least) 

349 
done 

350 

351 
lemma (in CL) lubIa: "[ S \<subseteq> A; isLub S cl L ] ==> L = lub S cl" 

352 
by (simp add: lubI isLub_def A_def r_def) 

353 

354 
lemma (in CL) isLub_in_lattice: "isLub S cl L ==> L \<in> A" 

355 
by (simp add: isLub_def A_def) 

356 

357 
lemma (in CL) isLub_upper: "[isLub S cl L; y \<in> S] ==> (y, L) \<in> r" 

358 
by (simp add: isLub_def r_def) 

359 

360 
lemma (in CL) isLub_least: 

361 
"[ isLub S cl L; z \<in> A; \<forall>y \<in> S. (y, z) \<in> r] ==> (L, z) \<in> r" 

362 
by (simp add: isLub_def A_def r_def) 

363 

364 
lemma (in CL) isLubI: 

365 
"[ L \<in> A; \<forall>y \<in> S. (y, L) \<in> r; 

366 
(\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) > (L, z) \<in> r)] ==> isLub S cl L" 

367 
by (simp add: isLub_def A_def r_def) 

368 

369 
subsection {* glb *} 

370 

371 
lemma (in CL) glb_in_lattice: "S \<subseteq> A ==> glb S cl \<in> A" 

372 
apply (subst glb_dual_lub) 

373 
apply (simp add: A_def) 

374 
apply (rule dualA_iff [THEN subst]) 

375 
apply (rule CL.lub_in_lattice) 

27681  376 
apply (rule CL.intro) 
377 
apply (rule PO.intro) 

23449  378 
apply (rule dualPO) 
27681  379 
apply (rule CL_axioms.intro) 
23449  380 
apply (rule CL_dualCL) 
381 
apply (simp add: dualA_iff) 

382 
done 

383 

384 
lemma (in CL) glb_lower: "[S \<subseteq> A; x \<in> S] ==> (glb S cl, x) \<in> r" 

385 
apply (subst glb_dual_lub) 

386 
apply (simp add: r_def) 

387 
apply (rule dualr_iff [THEN subst]) 

388 
apply (rule CL.lub_upper) 

27681  389 
apply (rule CL.intro) 
390 
apply (rule PO.intro) 

23449  391 
apply (rule dualPO) 
27681  392 
apply (rule CL_axioms.intro) 
23449  393 
apply (rule CL_dualCL) 
394 
apply (simp add: dualA_iff A_def, assumption) 

395 
done 

396 

397 
text {* 

398 
Reduce the sublattice property by using substructural properties; 

399 
abandoned see @{text "Tarski_4.ML"}. 

400 
*} 

401 

402 
declare (in CLF) f_cl [simp] 

403 

404 
lemma (in CLF) [simp]: 

42762
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

405 
"f: pset cl > pset cl & monotone f (pset cl) (order cl)" 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

406 
proof  
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

407 
have "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> {R \<in> pset v \<rightarrow> pset v. monotone R (pset v) (order v)}" 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

408 
unfolding CLF_set_def using SigmaE2 by blast 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

409 
hence F1: "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> pset v \<rightarrow> pset v \<and> monotone u (pset v) (order v)" 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

410 
using CollectE by blast 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

411 
hence "Tarski.monotone f (pset cl) (order cl)" by (metis f_cl) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

412 
hence "(cl, f) \<in> CLF_set \<and> Tarski.monotone f (pset cl) (order cl)" 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

413 
by (metis f_cl) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

414 
thus "f \<in> pset cl \<rightarrow> pset cl \<and> Tarski.monotone f (pset cl) (order cl)" 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

415 
using F1 by metis 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

416 
qed 
23449  417 

418 
lemma (in CLF) f_in_funcset: "f \<in> A > A" 

419 
by (simp add: A_def) 

420 

421 
lemma (in CLF) monotone_f: "monotone f A r" 

422 
by (simp add: A_def r_def) 

423 

424 
(*never proved, 20070122*) 

45705  425 

27681  426 
declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] 
427 

42762
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

428 
lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" 
23449  429 
apply (simp del: dualA_iff) 
430 
apply (simp) 

43197  431 
done 
27681  432 

433 
declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del] 

23449  434 
dualA_iff[simp del] 
435 

436 
subsection {* fixed points *} 

437 

438 
lemma fix_subset: "fix f A \<subseteq> A" 

439 
by (simp add: fix_def, fast) 

440 

441 
lemma fix_imp_eq: "x \<in> fix f A ==> f x = x" 

442 
by (simp add: fix_def) 

443 

444 
lemma fixf_subset: 

445 
"[ A \<subseteq> B; x \<in> fix (%y: A. f y) A ] ==> x \<in> fix f B" 

446 
by (simp add: fix_def, auto) 

447 

448 
subsection {* lemmas for Tarski, lub *} 

449 

450 
(*never proved, 20070122*) 

45705  451 

452 
declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] 

453 

23449  454 
lemma (in CLF) lubH_le_flubH: 
455 
"H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r" 

456 
apply (rule lub_least, fast) 

457 
apply (rule f_in_funcset [THEN funcset_mem]) 

458 
apply (rule lub_in_lattice, fast) 

459 
 {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *} 

460 
apply (rule ballI) 

461 
(*never proved, 20070122*) 

462 
apply (rule transE) 

463 
 {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *} 

464 
 {* because of the def of @{text H} *} 

465 
apply fast 

466 
 {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *} 

467 
apply (rule_tac f = "f" in monotoneE) 

468 
apply (rule monotone_f, fast) 

469 
apply (rule lub_in_lattice, fast) 

470 
apply (rule lub_upper, fast) 

471 
apply assumption 

472 
done 

45705  473 

474 
declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] 

475 
funcset_mem[rule del] CL.lub_in_lattice[rule del] 

476 
PO.transE[rule del] PO.monotoneE[rule del] 

477 
CLF.monotone_f[rule del] CL.lub_upper[rule del] 

23449  478 

479 
(*never proved, 20070122*) 

45705  480 

481 
declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] 

482 
PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] 

483 
CLF.lubH_le_flubH[simp] 

484 

23449  485 
lemma (in CLF) flubH_le_lubH: 
486 
"[ H = {x. (x, f x) \<in> r & x \<in> A} ] ==> (f (lub H cl), lub H cl) \<in> r" 

487 
apply (rule lub_upper, fast) 

488 
apply (rule_tac t = "H" in ssubst, assumption) 

489 
apply (rule CollectI) 

47040  490 
by (metis (lifting) CO_refl_on lubH_le_flubH monotone_def monotone_f refl_onD1 refl_onD2) 
23449  491 

45705  492 
declare CLF.f_in_funcset[rule del] funcset_mem[rule del] 
493 
CL.lub_in_lattice[rule del] PO.monotoneE[rule del] 

494 
CLF.monotone_f[rule del] CL.lub_upper[rule del] 

495 
CLF.lubH_le_flubH[simp del] 

23449  496 

497 
(*never proved, 20070122*) 

45705  498 

37622  499 
(* Singlestep version fails. The conjecture clauses refer to local abstraction 
500 
functions (Frees). *) 

23449  501 
lemma (in CLF) lubH_is_fixp: 
502 
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" 

503 
apply (simp add: fix_def) 

504 
apply (rule conjI) 

36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

505 
proof  
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

506 
assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}" 
42762
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

507 
have F1: "\<forall>u v. v \<inter> u \<subseteq> u" by (metis Int_commute Int_lower1) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

508 
have "{R. (R, f R) \<in> r} \<inter> {R. R \<in> A} = H" using A1 by (metis Collect_conj_eq) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

509 
hence "H \<subseteq> {R. R \<in> A}" using F1 by metis 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

510 
hence "H \<subseteq> A" by (metis Collect_mem_eq) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

511 
hence "lub H cl \<in> A" by (metis lub_in_lattice) 
0b3c3cf28218
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents:
42103
diff
changeset

512 
thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" using A1 by metis 
36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

513 
next 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

514 
assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

515 
have F1: "\<forall>v. {R. R \<in> v} = v" by (metis Collect_mem_eq) 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

516 
have F2: "\<forall>w u. {R. R \<in> u \<and> R \<in> w} = u \<inter> w" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

517 
by (metis Collect_conj_eq Collect_mem_eq) 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

518 
have F3: "\<forall>x v. {R. v R \<in> x} = v ` x" by (metis vimage_def) 
36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

519 
hence F4: "A \<inter> (\<lambda>R. (R, f R)) ` r = H" using A1 by auto 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

520 
hence F5: "(f (lub H cl), lub H cl) \<in> r" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

521 
by (metis A1 flubH_le_lubH) 
36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

522 
have F6: "(lub H cl, f (lub H cl)) \<in> r" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

523 
by (metis A1 lubH_le_flubH) 
36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

524 
have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl" 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

525 
using F5 by (metis antisymE) 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

526 
hence "f (lub H cl) = lub H cl" using F6 by metis 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

527 
thus "H = {x. (x, f x) \<in> r \<and> x \<in> A} 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

528 
\<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

529 
lub {x. (x, f x) \<in> r \<and> x \<in> A} cl" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45705
diff
changeset

530 
by metis 
24827  531 
qed 
23449  532 

25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
24855
diff
changeset

533 
lemma (in CLF) (*lubH_is_fixp:*) 
23449  534 
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" 
535 
apply (simp add: fix_def) 

536 
apply (rule conjI) 

30198  537 
apply (metis CO_refl_on lubH_le_flubH refl_onD1) 
23449  538 
apply (metis antisymE flubH_le_lubH lubH_le_flubH) 
539 
done 

540 

541 
lemma (in CLF) fix_in_H: 

542 
"[ H = {x. (x, f x) \<in> r & x \<in> A}; x \<in> P ] ==> x \<in> H" 

30198  543 
by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on 
23449  544 
fix_subset [of f A, THEN subsetD]) 
545 

546 
lemma (in CLF) fixf_le_lubH: 

547 
"H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r" 

548 
apply (rule ballI) 

549 
apply (rule lub_upper, fast) 

550 
apply (rule fix_in_H) 

551 
apply (simp_all add: P_def) 

552 
done 

553 

554 
lemma (in CLF) lubH_least_fixf: 

555 
"H = {x. (x, f x) \<in> r & x \<in> A} 

556 
==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) > (lub H cl, L) \<in> r" 

557 
apply (metis P_def lubH_is_fixp) 

558 
done 

559 

560 
subsection {* Tarski fixpoint theorem 1, first part *} 

45705  561 

562 
declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] 

563 
CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] 

564 

23449  565 
lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl" 
566 
(*sledgehammer;*) 

567 
apply (rule sym) 

568 
apply (simp add: P_def) 

569 
apply (rule lubI) 

43197  570 
apply (metis P_def fix_subset) 
24827  571 
apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) 
47040  572 
apply (metis P_def fixf_le_lubH) 
573 
by (metis P_def lubH_least_fixf) 

23449  574 

45705  575 
declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] 
576 
CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] 

23449  577 

578 
(*never proved, 20070122*) 

45705  579 

580 
declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] 

581 
PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] 

582 

23449  583 
lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P" 
584 
 {* Tarski for glb *} 

585 
(*sledgehammer;*) 

586 
apply (simp add: glb_dual_lub P_def A_def r_def) 

587 
apply (rule dualA_iff [THEN subst]) 

588 
apply (rule CLF.lubH_is_fixp) 

27681  589 
apply (rule CLF.intro) 
590 
apply (rule CL.intro) 

591 
apply (rule PO.intro) 

23449  592 
apply (rule dualPO) 
27681  593 
apply (rule CL_axioms.intro) 
23449  594 
apply (rule CL_dualCL) 
27681  595 
apply (rule CLF_axioms.intro) 
23449  596 
apply (rule CLF_dual) 
597 
apply (simp add: dualr_iff dualA_iff) 

598 
done 

599 

45705  600 
declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] 
601 
PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] 

23449  602 

603 
(*never proved, 20070122*) 

45705  604 

23449  605 
lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl" 
606 
(*sledgehammer;*) 

607 
apply (simp add: glb_dual_lub P_def A_def r_def) 

608 
apply (rule dualA_iff [THEN subst]) 

609 
(*never proved, 20070122*) 

610 
(*sledgehammer;*) 

27681  611 
apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, 
612 
OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) 

23449  613 
done 
614 

615 
subsection {* interval *} 

616 

45705  617 
declare (in CLF) CO_refl_on[simp] refl_on_def [simp] 
23449  618 

619 
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A" 

30198  620 
by (metis CO_refl_on refl_onD1) 
45705  621 

622 
declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] 

23449  623 

45705  624 
declare (in CLF) rel_imp_elem[intro] 
625 
declare interval_def [simp] 

626 

23449  627 
lemma (in CLF) interval_subset: "[ a \<in> A; b \<in> A ] ==> interval r a b \<subseteq> A" 
30198  628 
by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) 
23449  629 

45705  630 
declare (in CLF) rel_imp_elem[rule del] 
631 
declare interval_def [simp del] 

23449  632 

633 
lemma (in CLF) intervalI: 

634 
"[ (a, x) \<in> r; (x, b) \<in> r ] ==> x \<in> interval r a b" 

635 
by (simp add: interval_def) 

636 

637 
lemma (in CLF) interval_lemma1: 

638 
"[ S \<subseteq> interval r a b; x \<in> S ] ==> (a, x) \<in> r" 

639 
by (unfold interval_def, fast) 

640 

641 
lemma (in CLF) interval_lemma2: 

642 
"[ S \<subseteq> interval r a b; x \<in> S ] ==> (x, b) \<in> r" 

643 
by (unfold interval_def, fast) 

644 

645 
lemma (in CLF) a_less_lub: 

646 
"[ S \<subseteq> A; S \<noteq> {}; 

647 
\<forall>x \<in> S. (a,x) \<in> r; \<forall>y \<in> S. (y, L) \<in> r ] ==> (a,L) \<in> r" 

648 
by (blast intro: transE) 

649 

650 
lemma (in CLF) glb_less_b: 

651 
"[ S \<subseteq> A; S \<noteq> {}; 

652 
\<forall>x \<in> S. (x,b) \<in> r; \<forall>y \<in> S. (G, y) \<in> r ] ==> (G,b) \<in> r" 

653 
by (blast intro: transE) 

654 

655 
lemma (in CLF) S_intv_cl: 

656 
"[ a \<in> A; b \<in> A; S \<subseteq> interval r a b ]==> S \<subseteq> A" 

657 
by (simp add: subset_trans [OF _ interval_subset]) 

658 

45705  659 

23449  660 
lemma (in CLF) L_in_interval: 
661 
"[ a \<in> A; b \<in> A; S \<subseteq> interval r a b; 

43197  662 
S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} ] ==> L \<in> interval r a b" 
23449  663 
(*WON'T TERMINATE 
664 
apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def) 

665 
*) 

666 
apply (rule intervalI) 

667 
apply (rule a_less_lub) 

668 
prefer 2 apply assumption 

669 
apply (simp add: S_intv_cl) 

670 
apply (rule ballI) 

671 
apply (simp add: interval_lemma1) 

672 
apply (simp add: isLub_upper) 

673 
 {* @{text "(L, b) \<in> r"} *} 

674 
apply (simp add: isLub_least interval_lemma2) 

675 
done 

676 

677 
(*never proved, 20070122*) 

45705  678 

23449  679 
lemma (in CLF) G_in_interval: 
680 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G; 

681 
S \<noteq> {} ] ==> G \<in> interval r a b" 

682 
apply (simp add: interval_dual) 

27681  683 
apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] 
23449  684 
dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) 
685 
done 

686 

45705  687 

23449  688 
lemma (in CLF) intervalPO: 
689 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {} ] 

690 
==> ( pset = interval r a b, order = induced (interval r a b) r ) 

691 
\<in> PartialOrder" 

36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

692 
proof  
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

693 
assume A1: "a \<in> A" 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

694 
assume "b \<in> A" 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

695 
hence "\<forall>u. u \<in> A \<longrightarrow> interval r u b \<subseteq> A" by (metis interval_subset) 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

696 
hence "interval r a b \<subseteq> A" using A1 by metis 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

697 
hence "interval r a b \<subseteq> A" by metis 
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

698 
thus ?thesis by (metis po_subset_po) 
23449  699 
qed 
700 

701 
lemma (in CLF) intv_CL_lub: 

702 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {} ] 

703 
==> \<forall>S. S \<subseteq> interval r a b > 

704 
(\<exists>L. isLub S ( pset = interval r a b, 

705 
order = induced (interval r a b) r ) L)" 

706 
apply (intro strip) 

707 
apply (frule S_intv_cl [THEN CL_imp_ex_isLub]) 

708 
prefer 2 apply assumption 

709 
apply assumption 

710 
apply (erule exE) 

711 
 {* define the lub for the interval as *} 

712 
apply (rule_tac x = "if S = {} then a else L" in exI) 

713 
apply (simp (no_asm_simp) add: isLub_def split del: split_if) 

714 
apply (intro impI conjI) 

715 
 {* @{text "(if S = {} then a else L) \<in> interval r a b"} *} 

716 
apply (simp add: CL_imp_PO L_in_interval) 

717 
apply (simp add: left_in_interval) 

718 
 {* lub prop 1 *} 

719 
apply (case_tac "S = {}") 

720 
 {* @{text "S = {}, y \<in> S = False => everything"} *} 

721 
apply fast 

722 
 {* @{text "S \<noteq> {}"} *} 

723 
apply simp 

724 
 {* @{text "\<forall>y:S. (y, L) \<in> induced (interval r a b) r"} *} 

725 
apply (rule ballI) 

726 
apply (simp add: induced_def L_in_interval) 

727 
apply (rule conjI) 

728 
apply (rule subsetD) 

729 
apply (simp add: S_intv_cl, assumption) 

730 
apply (simp add: isLub_upper) 

731 
 {* @{text "\<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r \<longrightarrow> (if S = {} then a else L, z) \<in> induced (interval r a b) r"} *} 

732 
apply (rule ballI) 

733 
apply (rule impI) 

734 
apply (case_tac "S = {}") 

735 
 {* @{text "S = {}"} *} 

736 
apply simp 

737 
apply (simp add: induced_def interval_def) 

738 
apply (rule conjI) 

739 
apply (rule reflE, assumption) 

740 
apply (rule interval_not_empty) 

741 
apply (rule CO_trans) 

742 
apply (simp add: interval_def) 

743 
 {* @{text "S \<noteq> {}"} *} 

744 
apply simp 

745 
apply (simp add: induced_def L_in_interval) 

746 
apply (rule isLub_least, assumption) 

747 
apply (rule subsetD) 

748 
prefer 2 apply assumption 

749 
apply (simp add: S_intv_cl, fast) 

750 
done 

751 

752 
lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] 

753 

754 
(*never proved, 20070122*) 

45705  755 

23449  756 
lemma (in CLF) interval_is_sublattice: 
757 
"[ a \<in> A; b \<in> A; interval r a b \<noteq> {} ] 

758 
==> interval r a b <<= cl" 

759 
(*sledgehammer *) 

760 
apply (rule sublatticeI) 

761 
apply (simp add: interval_subset) 

762 
(*never proved, 20070122*) 

763 
(*sledgehammer *) 

764 
apply (rule CompleteLatticeI) 

765 
apply (simp add: intervalPO) 

766 
apply (simp add: intv_CL_lub) 

767 
apply (simp add: intv_CL_glb) 

768 
done 

769 

770 
lemmas (in CLF) interv_is_compl_latt = 

771 
interval_is_sublattice [THEN sublattice_imp_CL] 

772 

773 
subsection {* Top and Bottom *} 

774 
lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)" 

775 
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) 

776 

777 
lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" 

778 
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) 

779 

45705  780 

23449  781 
lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A" 
782 
(*sledgehammer; *) 

783 
apply (simp add: Bot_def least_def) 

784 
apply (rule_tac a="glb A cl" in someI2) 

43197  785 
apply (simp_all add: glb_in_lattice glb_lower 
23449  786 
r_def [symmetric] A_def [symmetric]) 
787 
done 

788 

789 
(*first proved 20070125 after relaxing relevance*) 

45705  790 

23449  791 
lemma (in CLF) Top_in_lattice: "Top cl \<in> A" 
792 
(*sledgehammer;*) 

793 
apply (simp add: Top_dual_Bot A_def) 

794 
(*first proved 20070125 after relaxing relevance*) 

795 
(*sledgehammer*) 

796 
apply (rule dualA_iff [THEN subst]) 

27681  797 
apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual) 
23449  798 
done 
799 

800 
lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r" 

801 
apply (simp add: Top_def greatest_def) 

802 
apply (rule_tac a="lub A cl" in someI2) 

803 
apply (rule someI2) 

43197  804 
apply (simp_all add: lub_in_lattice lub_upper 
23449  805 
r_def [symmetric] A_def [symmetric]) 
806 
done 

807 

808 
(*never proved, 20070122*) 

45705  809 

23449  810 
lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r" 
43197  811 
(*sledgehammer*) 
23449  812 
apply (simp add: Bot_dual_Top r_def) 
813 
apply (rule dualr_iff [THEN subst]) 

27681  814 
apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] 
23449  815 
dualA_iff A_def dualPO CL_dualCL CLF_dual) 
816 
done 

817 

45705  818 

43197  819 
lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}" 
23449  820 
apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) 
821 
done 

822 

45705  823 

43197  824 
lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" 
23449  825 
apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) 
826 
done 

827 

828 
subsection {* fixed points form a partial order *} 

829 

830 
lemma (in CLF) fixf_po: "( pset = P, order = induced P r) \<in> PartialOrder" 

831 
by (simp add: P_def fix_subset po_subset_po) 

832 

833 
(*first proved 20070125 after relaxing relevance*) 

45705  834 

835 
declare (in Tarski) P_def[simp] Y_ss [simp] 

836 
declare fix_subset [intro] subset_trans [intro] 

837 

23449  838 
lemma (in Tarski) Y_subset_A: "Y \<subseteq> A" 
43197  839 
(*sledgehammer*) 
23449  840 
apply (rule subset_trans [OF _ fix_subset]) 
841 
apply (rule Y_ss [simplified P_def]) 

842 
done 

843 

45705  844 
declare (in Tarski) P_def[simp del] Y_ss [simp del] 
845 
declare fix_subset [rule del] subset_trans [rule del] 

23449  846 

847 
lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A" 

848 
by (rule Y_subset_A [THEN lub_in_lattice]) 

849 

850 
(*never proved, 20070122*) 

45705  851 

23449  852 
lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r" 
43197  853 
(*sledgehammer*) 
23449  854 
apply (rule lub_least) 
855 
apply (rule Y_subset_A) 

856 
apply (rule f_in_funcset [THEN funcset_mem]) 

857 
apply (rule lubY_in_A) 

858 
 {* @{text "Y \<subseteq> P ==> f x = x"} *} 

859 
apply (rule ballI) 

860 
(*sledgehammer *) 

861 
apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) 

862 
apply (erule Y_ss [simplified P_def, THEN subsetD]) 

863 
 {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *} 

864 
(*sledgehammer*) 

865 
apply (rule_tac f = "f" in monotoneE) 

866 
apply (rule monotone_f) 

867 
apply (simp add: Y_subset_A [THEN subsetD]) 

868 
apply (rule lubY_in_A) 

869 
apply (simp add: lub_upper Y_subset_A) 

870 
done 

871 

872 
(*first proved 20070125 after relaxing relevance*) 

45705  873 

23449  874 
lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A" 
43197  875 
(*sledgehammer*) 
23449  876 
apply (unfold intY1_def) 
877 
apply (rule interval_subset) 

878 
apply (rule lubY_in_A) 

879 
apply (rule Top_in_lattice) 

880 
done 

881 

882 
lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] 

883 

884 
(*never proved, 20070122*) 

45705  885 

23449  886 
lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1" 
43197  887 
(*sledgehammer*) 
23449  888 
apply (simp add: intY1_def interval_def) 
889 
apply (rule conjI) 

890 
apply (rule transE) 

891 
apply (rule lubY_le_flubY) 

892 
 {* @{text "(f (lub Y cl), f x) \<in> r"} *} 

893 
(*sledgehammer [has been proved before now...]*) 

894 
apply (rule_tac f=f in monotoneE) 

895 
apply (rule monotone_f) 

896 
apply (rule lubY_in_A) 

897 
apply (simp add: intY1_def interval_def intY1_elem) 

898 
apply (simp add: intY1_def interval_def) 

43197  899 
 {* @{text "(f x, Top cl) \<in> r"} *} 
23449  900 
apply (rule Top_prop) 
901 
apply (rule f_in_funcset [THEN funcset_mem]) 

902 
apply (simp add: intY1_def interval_def intY1_elem) 

903 
done 

904 

45705  905 

27368  906 
lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 > intY1" 
907 
apply (rule restrict_in_funcset) 

908 
apply (metis intY1_f_closed restrict_in_funcset) 

909 
done 

23449  910 

45705  911 

24855  912 
lemma (in Tarski) intY1_mono: 
23449  913 
"monotone (%x: intY1. f x) intY1 (induced intY1 r)" 
914 
(*sledgehammer *) 

915 
apply (auto simp add: monotone_def induced_def intY1_f_closed) 

916 
apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) 

917 
done 

918 

919 
(*proof requires relaxing relevance: 20070125*) 

45705  920 

23449  921 
lemma (in Tarski) intY1_is_cl: 
922 
"( pset = intY1, order = induced intY1 r ) \<in> CompleteLattice" 

43197  923 
(*sledgehammer*) 
23449  924 
apply (unfold intY1_def) 
925 
apply (rule interv_is_compl_latt) 

926 
apply (rule lubY_in_A) 

927 
apply (rule Top_in_lattice) 

928 
apply (rule Top_intv_not_empty) 

929 
apply (rule lubY_in_A) 

930 
done 

931 

932 
(*never proved, 20070122*) 

45705  933 

23449  934 
lemma (in Tarski) v_in_P: "v \<in> P" 
43197  935 
(*sledgehammer*) 
23449  936 
apply (unfold P_def) 
937 
apply (rule_tac A = "intY1" in fixf_subset) 

938 
apply (rule intY1_subset) 

27681  939 
apply (simp add: CLF.glbH_is_fixp [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified] 
940 
v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) 

23449  941 
done 
942 

45705  943 

23449  944 
lemma (in Tarski) z_in_interval: 
945 
"[ z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r ] ==> z \<in> intY1" 

946 
(*sledgehammer *) 

947 
apply (unfold intY1_def P_def) 

948 
apply (rule intervalI) 

949 
prefer 2 

950 
apply (erule fix_subset [THEN subsetD, THEN Top_prop]) 

951 
apply (rule lub_least) 

952 
apply (rule Y_subset_A) 

953 
apply (fast elim!: fix_subset [THEN subsetD]) 

954 
apply (simp add: induced_def) 

955 
done 

956 

45705  957 

23449  958 
lemma (in Tarski) f'z_in_int_rel: "[ z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r ] 
43197  959 
==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
26806  960 
apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) 
23449  961 
done 
962 

963 
(*never proved, 20070122*) 

45705  964 

23449  965 
lemma (in Tarski) tarski_full_lemma: 
966 
"\<exists>L. isLub Y ( pset = P, order = induced P r ) L" 

967 
apply (rule_tac x = "v" in exI) 

968 
apply (simp add: isLub_def) 

969 
 {* @{text "v \<in> P"} *} 

970 
apply (simp add: v_in_P) 

971 
apply (rule conjI) 

43197  972 
(*sledgehammer*) 
23449  973 
 {* @{text v} is lub *} 
974 
 {* @{text "1. \<forall>y:Y. (y, v) \<in> induced P r"} *} 

975 
apply (rule ballI) 

976 
apply (simp add: induced_def subsetD v_in_P) 

977 
apply (rule conjI) 

978 
apply (erule Y_ss [THEN subsetD]) 

979 
apply (rule_tac b = "lub Y cl" in transE) 

980 
apply (rule lub_upper) 

981 
apply (rule Y_subset_A, assumption) 

982 
apply (rule_tac b = "Top cl" in interval_imp_mem) 

983 
apply (simp add: v_def) 

984 
apply (fold intY1_def) 

27681  985 
apply (rule CL.glb_in_lattice [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) 
23449  986 
apply (simp add: CL_imp_PO intY1_is_cl, force) 
987 
 {* @{text v} is LEAST ub *} 

988 
apply clarify 

989 
apply (rule indI) 

990 
prefer 3 apply assumption 

991 
prefer 2 apply (simp add: v_in_P) 

992 
apply (unfold v_def) 

993 
(*never proved, 20070122*) 

43197  994 
(*sledgehammer*) 
23449  995 
apply (rule indE) 
996 
apply (rule_tac [2] intY1_subset) 

997 
(*never proved, 20070122*) 

43197  998 
(*sledgehammer*) 
27681  999 
apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) 
23449  1000 
apply (simp add: CL_imp_PO intY1_is_cl) 
1001 
apply force 

1002 
apply (simp add: induced_def intY1_f_closed z_in_interval) 

1003 
apply (simp add: P_def fix_imp_eq [of _ f A] reflE 

1004 
fix_subset [of f A, THEN subsetD]) 

1005 
done 

1006 

1007 
lemma CompleteLatticeI_simp: 

1008 
"[ ( pset = A, order = r ) \<in> PartialOrder; 

1009 
\<forall>S. S \<subseteq> A > (\<exists>L. isLub S ( pset = A, order = r ) L) ] 

1010 
==> ( pset = A, order = r ) \<in> CompleteLattice" 

1011 
by (simp add: CompleteLatticeI Rdual) 

1012 

45705  1013 
(*never proved, 20070122*) 
23449  1014 

45705  1015 
declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] 
1016 
Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] 

1017 
CompleteLatticeI_simp [intro] 

1018 

23449  1019 
theorem (in CLF) Tarski_full: 
1020 
"( pset = P, order = induced P r) \<in> CompleteLattice" 

43197  1021 
(*sledgehammer*) 
23449  1022 
apply (rule CompleteLatticeI_simp) 
1023 
apply (rule fixf_po, clarify) 

1024 
(*never proved, 20070122*) 

43197  1025 
(*sledgehammer*) 
23449  1026 
apply (simp add: P_def A_def r_def) 
27681  1027 
apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, 
1028 
OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) 

23449  1029 
done 
36554
2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

1030 

2673979cb54d
more neg_clausify proofs that get replaced by direct proofs
blanchet
parents:
35416
diff
changeset

1031 
declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del] 
23449  1032 
Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del] 
1033 
CompleteLatticeI_simp [rule del] 

1034 

1035 
end 