7085

1 
(* Title: HOL/ex/Tarski


2 
ID: $Id$


3 
Author: Florian Kammueller, Cambridge University Computer Laboratory


4 
Copyright 1999 University of Cambridge


5 


6 
Minimal version of lattice theory plus the full theorem of Tarski:


7 
The fixedpoints of a complete lattice themselves form a complete lattice.


8 


9 
Illustrates firstclass theories, using the Sigma representation of structures


10 
*)


11 


12 


13 
(* abbreviate commonly used tactic application *)


14 


15 
fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));


16 


17 
(* Partial Order *)


18 
Open_locale "PO";


19 


20 
val simp_PO = simplify (simpset() addsimps [PartialOrder_def]) (thm "cl_po");


21 
Addsimps [simp_PO, thm "cl_po"];


22 


23 
val PO_simp = [thm "A_def", thm "r_def"];


24 


25 
Goal "refl A r";


26 
by (simp_tac (simpset() addsimps PO_simp) 1);


27 
qed "PartialOrderE1";


28 


29 
Goal "antisym r";


30 
by (simp_tac (simpset() addsimps PO_simp) 1);


31 
qed "PartialOrderE2";


32 


33 
Goal "trans r";


34 
by (simp_tac (simpset() addsimps PO_simp) 1);


35 
qed "PartialOrderE3";


36 


37 
Goal "[ refl A r; x: A] ==> (x, x): r";


38 
by (afs [refl_def] 1);


39 
qed "reflE";


40 
(* Interesting: A and r don't get bound because the proof doesn't use


41 
locale rules


42 
val reflE = "[ refl ?A ?r; ?x : ?A ] ==> (?x, ?x) : ?r" *)


43 


44 
Goal "[ antisym r; (a, b): r; (b, a): r ] ==> a = b";


45 
by (afs [antisym_def] 1);


46 
qed "antisymE";


47 


48 
Goalw [trans_def] "[ trans r; (a, b): r; (b, c): r] ==> (a,c): r";


49 
by (Fast_tac 1);


50 
qed "transE";


51 


52 
Goal "[ monotone f A r; x: A; y: A; (x, y): r ] ==> (f x, f y): r";


53 
by (afs [monotone_def] 1);


54 
qed "monotoneE";


55 


56 
Goal "S <= A ==> ( pset = S, order = induced S r ): PartialOrder";


57 
by (simp_tac (simpset() addsimps [PartialOrder_def]) 1);


58 
by (Step_tac 1);


59 
(* refl *)


60 
by (afs [refl_def,induced_def] 1);


61 
by (rtac conjI 1);


62 
by (Fast_tac 1);


63 
by (rtac ballI 1);


64 
by (rtac reflE 1);


65 
by (rtac PartialOrderE1 1);


66 
by (Fast_tac 1);


67 
(* antisym *)


68 
by (afs [antisym_def,induced_def] 1);


69 
by (Step_tac 1);


70 
by (rtac antisymE 1);


71 
by (assume_tac 2);


72 
by (assume_tac 2);


73 
by (rtac PartialOrderE2 1);


74 
(* trans *)


75 
by (afs [trans_def,induced_def] 1);


76 
by (Step_tac 1);


77 
by (rtac transE 1);


78 
by (assume_tac 2);


79 
by (assume_tac 2);


80 
by (rtac PartialOrderE3 1);


81 
qed "po_subset_po";


82 


83 
Goal "[ (x, y): induced S r; S <= A ] ==> (x, y): r";


84 
by (afs [induced_def] 1);


85 
qed "indE";


86 


87 
Goal "[ (x, y): r; x: S; y: S ] ==> (x, y): induced S r";


88 
by (afs [induced_def] 1);


89 
qed "indI";


90 


91 
(* with locales *)


92 
Open_locale "CL";


93 


94 
Delsimps [simp_PO, thm "cl_po"];


95 


96 
val simp_CL = simplify (simpset() addsimps [CompleteLattice_def])


97 
(thm "cl_co");


98 
Addsimps [simp_CL, thm "cl_co"];


99 


100 
Goalw [Ex_def] "(EX L. islub S cl L) = islub S cl (lub S cl)";


101 
by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def]) 1);


102 
qed "islub_lub";


103 


104 
Goalw [Ex_def] "(EX G. isglb S cl G) = isglb S cl (glb S cl)";


105 
by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def]) 1);


106 
qed "isglb_glb";


107 


108 
Goal "isglb S cl = islub S (dual cl)";


109 
by (afs [islub_def,isglb_def,dual_def,converse_def] 1);


110 
qed "isglb_dual_islub";


111 


112 
Goal "islub S cl = isglb S (dual cl)";


113 
by (afs [islub_def,isglb_def,dual_def,converse_def] 1);


114 
qed "islub_dual_isglb";


115 


116 
Goal "dual cl : PartialOrder";


117 
by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1);


118 
by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1);


119 
qed "dualPO";


120 


121 
Goal "! S. (S <= A >( ? L. islub S ( pset = A, order = r) L)) \


122 
\ ==> ! S. (S <= A > (? G. isglb S ( pset = A, order = r) G))";


123 
by (Step_tac 1);


124 
by (res_inst_tac


125 
[("x"," lub {y. y: A & (! k: S. (y, k): r)}(pset = A, order = r)")]


126 
exI 1);


127 
by (dres_inst_tac [("x","{y. y: A & (! k: S. (y,k): r)}")] spec 1);


128 
by (dtac mp 1);


129 
by (Fast_tac 1);


130 
by (afs [islub_lub, isglb_def] 1);


131 
by (afs [islub_def] 1);


132 
by (Blast_tac 1);


133 
qed "Rdual";


134 


135 
Goal "lub S cl = glb S (dual cl)";


136 
by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);


137 
qed "lub_dual_glb";


138 


139 
Goal "glb S cl = lub S (dual cl)";


140 
by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);


141 
qed "glb_dual_lub";


142 


143 
Goal "CompleteLattice <= PartialOrder";


144 
by (simp_tac (simpset() addsimps [PartialOrder_def, CompleteLattice_def]) 1);


145 
by (Fast_tac 1);


146 
qed "CL_subset_PO";


147 


148 
val CompleteLatticeE1 = CL_subset_PO RS subsetD;


149 


150 
Goal "! S. S <= A > (? L. islub S cl L)";


151 
by (simp_tac (simpset() addsimps PO_simp) 1);


152 
qed "CompleteLatticeE2";


153 


154 
Goal "! S. S <= A > (? G. isglb S cl G)";


155 
by (simp_tac (simpset() addsimps PO_simp) 1);


156 
qed "CompleteLatticeE3";


157 


158 
Addsimps [CompleteLatticeE1 RS (export simp_PO)];


159 


160 
Goal "refl A r";


161 
by (simp_tac (simpset() addsimps PO_simp) 1);


162 
qed "CompleteLatticeE11";


163 


164 
Goal "antisym r";


165 
by (simp_tac (simpset() addsimps PO_simp) 1);


166 
qed "CompleteLatticeE12";


167 


168 
Goal "trans r";


169 
by (afs (PO_simp) 1);


170 
qed "CompleteLatticeE13";


171 


172 
Goal "[ po : PartialOrder; (! S. S <= po.<A> > (? L. islub S po L));\


173 
\ (! S. S <= po.<A> > (? G. isglb S po G))] ==> po: CompleteLattice";


174 
by (afs [CompleteLattice_def] 1);


175 
qed "CompleteLatticeI";


176 


177 
Goal "dual cl : CompleteLattice";


178 
by (simp_tac (simpset() addsimps [CompleteLattice_def,dual_def]) 1);


179 
by (fold_goals_tac [dual_def]);


180 
by (simp_tac (simpset() addsimps [islub_dual_isglb RS sym,


181 
isglb_dual_islub RS sym,


182 
export dualPO]) 1);


183 
qed "CL_dualCL";


184 


185 
Goal "(dual cl.<A>) = cl.<A>";


186 
by (simp_tac (simpset() addsimps [dual_def]) 1);


187 
qed "dualA_iff";


188 


189 
Goal "((x, y): (dual cl.<r>)) = ((y, x): cl.<r>)";


190 
by (simp_tac (simpset() addsimps [dual_def]) 1);


191 
qed "dualr_iff";


192 


193 
Goal "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)";


194 
by (afs [monotone_def,dualA_iff,dualr_iff] 1);


195 
qed "monotone_dual";


196 


197 
Goal "[ x: A; y: A] ==> interval r x y = interval (dual cl.<r>) y x";


198 
by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1);


199 
by (fold_goals_tac [thm "r_def"]);


200 
by (Fast_tac 1);


201 
qed "interval_dual";


202 


203 
Goal "[ trans r; interval r a b ~= {} ] ==> (a, b): r";


204 
by (afs [interval_def] 1);


205 
by (rewtac trans_def);


206 
by (Blast_tac 1);


207 
qed "interval_not_empty";


208 


209 
Goal "x: interval r a b ==> (a, x): r";


210 
by (afs [interval_def] 1);


211 
qed "intervalE1";


212 


213 
Goal "[ a: A; b: A; interval r a b ~= {} ] ==> a: interval r a b";


214 
by (simp_tac (simpset() addsimps [interval_def]) 1);


215 
by (afs [PartialOrderE3,interval_not_empty] 1);


216 
by (afs [PartialOrderE1 RS reflE] 1);


217 
qed "left_in_interval";


218 


219 
Goal "[ a: A; b: A; interval r a b ~= {} ] ==> b: interval r a b";


220 
by (simp_tac (simpset() addsimps [interval_def]) 1);


221 
by (afs [PartialOrderE3,interval_not_empty] 1);


222 
by (afs [PartialOrderE1 RS reflE] 1);


223 
qed "right_in_interval";


224 


225 
Goal "[ ( pset = A, order = r ) : PartialOrder;\


226 
\ ! S. S <= A > (? L. islub S ( pset = A, order = r ) L) ] \


227 
\ ==> ( pset = A, order = r ) : CompleteLattice";


228 
by (afs [CompleteLatticeI, Rdual] 1);


229 
qed "CompleteLatticeI_simp";


230 


231 
(* sublattice *)


232 
Goal "S <<= cl ==> S <= A";


233 
by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1);


234 
qed "sublatticeE1";


235 


236 
Goal "S <<= cl ==> ( pset = S, order = induced S r ) : CompleteLattice";


237 
by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1);


238 
qed "sublatticeE2";


239 


240 
Goal "[ S <= A; ( pset = S, order = induced S r ) : CompleteLattice ] ==> S <<= cl";


241 
by (afs ([sublattice_def] @ PO_simp) 1);


242 
qed "sublatticeI";


243 


244 
(* lub *)


245 
Goal "[ S <= A; islub S cl x; islub S cl L] ==> x = L";


246 
by (rtac antisymE 1);


247 
by (rtac CompleteLatticeE12 1);


248 
by (rewtac islub_def);


249 
by (rotate_tac ~1 1);


250 
by (etac conjE 1);


251 
by (dtac conjunct2 1);


252 
by (dtac conjunct1 1);


253 
by (dtac conjunct2 1);


254 
by (rotate_tac ~1 1);


255 
by (dres_inst_tac [("x","L")] bspec 1);


256 
by (assume_tac 1);


257 
by (fold_goals_tac [thm "r_def"]);


258 
by (etac mp 1);


259 
by (assume_tac 1);


260 
(* (L, x) : (cl .<r>) *)


261 
by (rotate_tac ~1 1);


262 
by (etac conjE 1);


263 
by (rotate_tac ~1 1);


264 
by (dtac conjunct2 1);


265 
by (dtac bspec 1);


266 
by (etac conjunct1 1);


267 
by (etac mp 1);


268 
by (etac (conjunct2 RS conjunct1) 1);


269 
qed "lub_unique";


270 


271 
Goal "[ S <= A ] ==> ! x: S. (x,lub S cl): r";


272 
by (rtac exE 1);


273 
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);


274 
by (assume_tac 1);


275 
by (rewrite_goals_tac [lub_def,least_def]);

9969

276 
by (stac some_equality 1);

7085

277 
by (rtac conjI 1);


278 
by (afs [islub_def] 2);


279 
by (etac conjunct2 2);


280 
by (afs [islub_def] 1);


281 
by (rtac lub_unique 1);


282 
by (afs [thm "A_def"] 1);


283 
by (afs [islub_def] 1);


284 
by (assume_tac 1);


285 
by (afs [islub_def,thm "r_def"] 1);


286 
qed "lubE1";


287 


288 
Goal "[ S <= A; L: A; ! x: S. (x,L): r ] ==> (lub S cl, L): r";


289 
by (rtac exE 1);


290 
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);


291 
by (assume_tac 1);


292 
by (rewrite_goals_tac [lub_def,least_def]);

9969

293 
by (stac some_equality 1);

7085

294 
by (rtac conjI 1);


295 
by (afs [islub_def] 2);


296 
by (etac conjunct2 2);


297 
by (afs [islub_def] 1);


298 
by (rtac lub_unique 1);


299 
by (afs [thm "A_def"] 1);


300 
by (afs [islub_def] 1);


301 
by (assume_tac 1);


302 
by (afs [islub_def] 1);


303 
by (dtac conjunct2 1);


304 
by (dtac conjunct2 1);


305 
by (rotate_tac 3 1);


306 
by (dtac bspec 1);


307 
by (fold_goals_tac [thm "r_def"]);


308 
by (etac mp 2);


309 
by (afs [thm "A_def"] 1);


310 
by (assume_tac 1);


311 
qed "lubE2";


312 


313 
Goal "[ S <= A ] ==> lub S cl : A";


314 
by (rtac exE 1);


315 
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);


316 
by (assume_tac 1);


317 
by (rewrite_goals_tac [lub_def,least_def]);

9969

318 
by (stac some_equality 1);

7085

319 
by (afs [islub_def] 1);


320 
by (afs [islub_def, thm "A_def"] 2);


321 
by (rtac lub_unique 1);


322 
by (afs [thm "A_def"] 1);


323 
by (afs [islub_def] 1);


324 
by (assume_tac 1);


325 
qed "lub_in_lattice";


326 


327 
Goal "[ S <= A; L: A; ! x: S. (x,L): r;\


328 
\ ! z: A. (! y: S. (y,z): r) > (L,z): r ] ==> L = lub S cl";


329 
by (rtac lub_unique 1);


330 
by (assume_tac 1);


331 
by (afs ([islub_def] @ PO_simp) 1);


332 
by (rewtac islub_def);


333 
by (rtac conjI 1);


334 
by (fold_goals_tac PO_simp);


335 
by (rtac lub_in_lattice 1);


336 
by (assume_tac 1);


337 
by (afs [lubE1, lubE2] 1);


338 
qed "lubI";


339 


340 
Goal "[ S <= A; islub S cl L ] ==> L = lub S cl";


341 
by (afs ([lubI, islub_def] @ PO_simp) 1);


342 
qed "lubIa";


343 


344 
Goal "islub S cl L ==> L : A";


345 
by (afs [islub_def, thm "A_def"] 1);


346 
qed "islub_in_lattice";


347 


348 
Goal "islub S cl L ==> ! y: S. (y, L): r";


349 
by (afs [islub_def, thm "r_def"] 1);


350 
qed "islubE1";


351 


352 
Goal "[ islub S cl L; \


353 
\ z: A; ! y: S. (y, z): r] ==> (L, z): r";


354 
by (afs ([islub_def] @ PO_simp) 1);


355 
qed "islubE2";


356 


357 
Goal "[ S <= A ] ==> ? L. islub S cl L";


358 
by (afs [thm "A_def"] 1);


359 
qed "islubE";


360 


361 
Goal "[ L: A; ! y: S. (y, L): r; \


362 
\ (!z: A. (! y: S. (y, z):r) > (L, z): r)] ==> islub S cl L";


363 
by (afs ([islub_def] @ PO_simp) 1);


364 
qed "islubI";


365 


366 
(* glb *)


367 
Goal "S <= A ==> glb S cl : A";


368 
by (stac glb_dual_lub 1);


369 
by (afs [thm "A_def"] 1);


370 
by (rtac (dualA_iff RS subst) 1);


371 
by (rtac (export lub_in_lattice) 1);


372 
by (rtac CL_dualCL 1);


373 
by (afs [dualA_iff] 1);


374 
qed "glb_in_lattice";


375 


376 
Goal "S <= A ==> ! x: S. (glb S cl, x): r";


377 
by (stac glb_dual_lub 1);


378 
by (rtac ballI 1);


379 
by (afs [thm "r_def"] 1);


380 
by (rtac (dualr_iff RS subst) 1);


381 
by (rtac (export lubE1 RS bspec) 1);


382 
by (rtac CL_dualCL 1);


383 
by (afs [dualA_iff, thm "A_def"] 1);


384 
by (assume_tac 1);


385 
qed "glbE1";


386 


387 
(* Reduce the sublattice property by using substructural properties! *)


388 
(* abandoned see Tarski_4.ML *)


389 


390 
Open_locale "CLF";


391 


392 
val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl");


393 
Addsimps [simp_CLF, thm "f_cl"];


394 


395 
Goal "f : A funcset A";


396 
by (simp_tac (simpset() addsimps [thm "A_def"]) 1);


397 
qed "CLF_E1";


398 


399 
Goal "monotone f A r";


400 
by (simp_tac (simpset() addsimps PO_simp) 1);


401 
qed "CLF_E2";


402 


403 
Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}";


404 
by (afs [CLF_def, CL_dualCL, monotone_dual] 1);


405 
by (afs [dualA_iff] 1);


406 
qed "CLF_dual";


407 


408 
(* fixed points *)


409 
Goal "P <= A";


410 
by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);


411 
by (Fast_tac 1);


412 
qed "fixfE1";


413 


414 
Goal "x: P ==> f x = x";


415 
by (afs [thm "P_def", fix_def] 1);


416 
qed "fixfE2";


417 


418 
Goal "[ A <= B; x: fix (lam y: A. f y) A ] ==> x: fix f B";


419 
by (forward_tac [export fixfE2] 1);


420 
by (dtac ((export fixfE1) RS subsetD) 1);


421 
by (afs [fix_def] 1);


422 
by (rtac conjI 1);


423 
by (Fast_tac 1);


424 
by (res_inst_tac [("P","% y. f x = y")] subst 1);


425 
by (assume_tac 1);


426 
by (rtac sym 1);


427 
by (etac restrict_apply1 1);


428 
qed "fixf_subset";


429 


430 
(* lemmas for Tarski, lub *)


431 
Goal "H = {x. (x, f x) : r & x : A} ==> (lub H cl, f (lub H cl)) : r";


432 
by (rtac lubE2 1);


433 
by (Fast_tac 1);


434 
by (rtac (CLF_E1 RS funcset_mem) 1);


435 
by (rtac lub_in_lattice 1);


436 
by (Fast_tac 1);


437 
(* ! x:H. (x, f (lub H r)) : r *)


438 
by (rtac ballI 1);


439 
by (rtac transE 1);


440 
by (rtac CompleteLatticeE13 1);


441 
(* instantiates (x, ???z): cl.<r> to (x, f x), because of the def of H *)


442 
by (Fast_tac 1);


443 
(* so it remains to show (f x, f (lub H cl)) : r *)


444 
by (res_inst_tac [("f","f")] monotoneE 1);


445 
by (rtac CLF_E2 1);


446 
by (Fast_tac 1);


447 
by (rtac lub_in_lattice 1);


448 
by (Fast_tac 1);


449 
by (rtac (lubE1 RS bspec) 1);


450 
by (Fast_tac 1);


451 
by (assume_tac 1);


452 
qed "lubH_le_flubH";


453 


454 
Goal "[ H = {x. (x, f x) : r & x : A} ] ==> (f (lub H cl), lub H cl) : r";


455 
by (rtac (lubE1 RS bspec) 1);


456 
by (Fast_tac 1);


457 
by (res_inst_tac [("t","H")] ssubst 1);


458 
by (assume_tac 1);


459 
by (rtac CollectI 1);


460 
by (rtac conjI 1);


461 
by (rtac (CLF_E1 RS funcset_mem) 2);


462 
by (rtac lub_in_lattice 2);


463 
by (Fast_tac 2);


464 
by (res_inst_tac [("f","f")] monotoneE 1);


465 
by (rtac CLF_E2 1);


466 
by (afs [lubH_le_flubH] 3);


467 
by (rtac (CLF_E1 RS funcset_mem) 2);


468 
by (rtac lub_in_lattice 2);


469 
by (Fast_tac 2);


470 
by (rtac lub_in_lattice 1);


471 
by (Fast_tac 1);


472 
qed "flubH_le_lubH";


473 


474 
Goal "H = {x. (x, f x): r & x : A} ==> lub H cl : P";


475 
by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);


476 
by (rtac conjI 1);


477 
by (rtac lub_in_lattice 1);


478 
by (Fast_tac 1);


479 
by (rtac antisymE 1);


480 
by (rtac CompleteLatticeE12 1);


481 
by (afs [flubH_le_lubH] 1);


482 
by (afs [lubH_le_flubH] 1);


483 
qed "lubH_is_fixp";


484 


485 
Goal "[ H = {x. (x, f x) : r & x : A}; x: P ] ==> x: H";


486 
by (etac ssubst 1);


487 
by (Simp_tac 1);


488 
by (rtac conjI 1);

7499

489 
by (ftac fixfE2 1);

7085

490 
by (etac ssubst 1);


491 
by (rtac reflE 1);


492 
by (rtac CompleteLatticeE11 1);


493 
by (etac (fixfE1 RS subsetD) 1);


494 
by (etac (fixfE1 RS subsetD) 1);


495 
qed "fix_in_H";


496 


497 
Goal "H = {x. (x, f x) : r & x : A} ==> ! x: P. (x, lub H cl) : r";


498 
by (rtac ballI 1);


499 
by (rtac (lubE1 RS bspec) 1);


500 
by (Fast_tac 1);


501 
by (rtac fix_in_H 1);


502 
by (REPEAT (atac 1));


503 
qed "fixf_le_lubH";


504 


505 
Goal "H = {x. (x, f x) : r & x : A} ==> ! L. (! y: P. (y,L): r) > (lub H cl, L): r";


506 
by (rtac allI 1);


507 
by (rtac impI 1);


508 
by (etac bspec 1);


509 
by (rtac lubH_is_fixp 1);


510 
by (assume_tac 1);


511 
qed "lubH_least_fixf";


512 


513 
(* Tarski fixpoint theorem 1, first part *)


514 
Goal "lub P cl = lub {x. (x, f x) : r & x : A} cl";


515 
by (rtac sym 1);


516 
by (rtac lubI 1);


517 
by (rtac fixfE1 1);


518 
by (rtac lub_in_lattice 1);


519 
by (Fast_tac 1);


520 
by (afs [fixf_le_lubH] 1);


521 
by (afs [lubH_least_fixf] 1);


522 
qed "T_thm_1_lub";


523 


524 
(* Tarski for glb *)


525 
Goal "H = {x. (f x, x): r & x : A} ==> glb H cl : P";


526 
by (full_simp_tac


527 
(simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);


528 
by (rtac (dualA_iff RS subst) 1);


529 
by (rtac (CL_dualCL RS (export lubH_is_fixp)) 1);


530 
by (rtac (thm "f_cl" RS CLF_dual) 1);


531 
by (afs [dualr_iff, dualA_iff] 1);


532 
qed "glbH_is_fixp";


533 


534 
Goal "glb P cl = glb {x. (f x, x): r & x : A} cl";


535 
by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);


536 
by (rtac (dualA_iff RS subst) 1);


537 
by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1);


538 
by (rtac (thm "f_cl" RS CLF_dual) 1);


539 
by (afs [dualr_iff] 1);


540 
qed "T_thm_1_glb";


541 


542 
(* interval *)

8703

543 
Goal "refl A r ==> r <= A <*> A";

7085

544 
by (afs [refl_def] 1);


545 
qed "reflE1";


546 


547 
Goal "(x, y): r ==> x: A";


548 
by (rtac SigmaD1 1);


549 
by (rtac (reflE1 RS subsetD) 1);


550 
by (rtac CompleteLatticeE11 1);


551 
by (assume_tac 1);


552 
qed "rel_imp_elem";


553 


554 
Goal "[ a: A; b: A ] ==> interval r a b <= A";


555 
by (simp_tac (simpset() addsimps [interval_def]) 1);


556 
by (rtac subsetI 1);


557 
by (rtac rel_imp_elem 1);


558 
by (dtac CollectD 1);


559 
by (etac conjunct2 1);


560 
qed "interval_subset";


561 


562 
Goal "[ (a, x): r; (x, b): r ] ==> x: interval r a b";


563 
by (afs [interval_def] 1);


564 
qed "intervalI";


565 


566 
Goalw [interval_def] "[ S <= interval r a b; x: S ] ==> (a, x): r";


567 
by (Fast_tac 1);


568 
qed "interval_lemma1";


569 


570 
Goalw [interval_def] "[ S <= interval r a b; x: S ] ==> (x, b): r";


571 
by (Fast_tac 1);


572 
qed "interval_lemma2";


573 


574 
Goal "[ S <= A; S ~= {};\


575 
\ ! x: S. (a,x): r; ! y: S. (y, L): r ] ==> (a,L): r";


576 
by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);


577 
qed "a_less_lub";


578 


579 
Goal "[ S <= A; S ~= {};\


580 
\ ! x: S. (x,b): r; ! y: S. (G, y): r ] ==> (G,b): r";


581 
by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);


582 
qed "glb_less_b";


583 


584 
Goal "[ a : A; b : A; S <= interval r a b ]==> S <= A";


585 
by (afs [interval_subset RSN(2, subset_trans)] 1);


586 
qed "S_intv_cl";


587 


588 
Goal "[ a : A; b: A; S <= interval r a b; \


589 
\ S ~= {}; islub S cl L; interval r a b ~= {} ] ==> L : interval r a b";


590 
by (rtac intervalI 1);


591 
by (rtac a_less_lub 1);


592 
by (assume_tac 2);


593 
by (afs [S_intv_cl] 1);


594 
by (rtac ballI 1);


595 
by (afs [interval_lemma1] 1);


596 
by (afs [islubE1] 1);


597 
(* (L, b) : r *)


598 
by (rtac islubE2 1);


599 
by (assume_tac 1);


600 
by (assume_tac 1);


601 
by (rtac ballI 1);


602 
by (afs [interval_lemma2] 1);


603 
qed "L_in_interval";


604 


605 
Goal "[ a : A; b : A; interval r a b ~= {}; S <= interval r a b; isglb S cl G; \


606 
\ S ~= {} ] ==> G : interval r a b";


607 
by (afs [interval_dual] 1);


608 
by (rtac (export L_in_interval) 1);


609 
by (rtac dualPO 1);


610 
by (afs [dualA_iff, thm "A_def"] 1);


611 
by (afs [dualA_iff, thm "A_def"] 1);


612 
by (assume_tac 1);


613 
by (afs [isglb_dual_islub] 1);


614 
by (afs [isglb_dual_islub] 1);


615 
by (assume_tac 1);


616 
qed "G_in_interval";


617 


618 
Goal "[ a: A; b: A; interval r a b ~= {} ]\


619 
\ ==> ( pset = interval r a b, order = induced (interval r a b) r ) : PartialOrder";


620 
by (rtac po_subset_po 1);


621 
by (afs [interval_subset] 1);


622 
qed "intervalPO";


623 


624 
Goal "[ a : A; b : A;\


625 
\ interval r a b ~= {} ] ==> ! S. S <= interval r a b >\


626 
\ (? L. islub S ( pset = interval r a b, order = induced (interval r a b) r ) L)";


627 
by (strip_tac 1);


628 
by (forward_tac [S_intv_cl RS islubE] 1);


629 
by (assume_tac 2);


630 
by (assume_tac 1);


631 
by (etac exE 1);


632 
(* define the lub for the interval as: *)


633 
by (res_inst_tac [("x","if S = {} then a else L")] exI 1);


634 
by (rtac (export islubI) 1);


635 
(* (if S = {} then a else L) : interval r a b *)


636 
by (asm_full_simp_tac


637 
(simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1);


638 
by (afs [left_in_interval] 1);


639 
(* lub prop 1 *)


640 
by (case_tac "S = {}" 1);


641 
(* S = {}, y: S = False => everything *)


642 
by (Fast_tac 1);


643 
(* S ~= {} *)


644 
by (Asm_full_simp_tac 1);


645 
(* ! y:S. (y, L) : induced (interval r a b) r *)


646 
by (rtac ballI 1);


647 
by (afs [induced_def, L_in_interval] 1);


648 
by (rtac conjI 1);


649 
by (rtac subsetD 1);


650 
by (afs [S_intv_cl] 1);


651 
by (assume_tac 1);


652 
by (afs [islubE1] 1);


653 
(* ! z:interval r a b. (! y:S. (y, z) : induced (interval r a b) r >


654 
(if S = {} then a else L, z) : induced (interval r a b) r *)


655 
by (rtac ballI 1);


656 
by (rtac impI 1);


657 
by (case_tac "S = {}" 1);


658 
(* S = {} *)


659 
by (Asm_full_simp_tac 1);


660 
by (afs [induced_def, interval_def] 1);


661 
by (rtac conjI 1);


662 
by (rtac reflE 1);


663 
by (rtac CompleteLatticeE11 1);


664 
by (assume_tac 1);


665 
by (rtac interval_not_empty 1);


666 
by (rtac CompleteLatticeE13 1);


667 
by (afs [interval_def] 1);


668 
(* S ~= {} *)


669 
by (Asm_full_simp_tac 1);


670 
by (afs [induced_def, L_in_interval] 1);


671 
by (rtac islubE2 1);


672 
by (assume_tac 1);


673 
by (rtac subsetD 1);


674 
by (assume_tac 2);


675 
by (afs [S_intv_cl] 1);


676 
by (Fast_tac 1);


677 
qed "intv_CL_lub";


678 


679 
val intv_CL_glb = intv_CL_lub RS Rdual;


680 


681 
Goal "[ a: A; b: A; interval r a b ~= {} ]\


682 
\ ==> interval r a b <<= cl";


683 
by (rtac sublatticeI 1);


684 
by (afs [interval_subset] 1);


685 
by (rtac CompleteLatticeI 1);


686 
by (afs [intervalPO] 1);


687 
by (afs [intv_CL_lub] 1);


688 
by (afs [intv_CL_glb] 1);


689 
qed "interval_is_sublattice";


690 


691 
val interv_is_compl_latt = interval_is_sublattice RS sublatticeE2;


692 


693 
(* Top and Bottom *)


694 
Goal "Top cl = Bot (dual cl)";


695 
by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);


696 
qed "Top_dual_Bot";


697 


698 
Goal "Bot cl = Top (dual cl)";


699 
by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);


700 
qed "Bot_dual_Top";


701 


702 
Goal "Bot cl: A";


703 
by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);

9969

704 
by (rtac someI2 1);

7085

705 
by (fold_goals_tac [thm "A_def"]);


706 
by (etac conjunct1 2);


707 
by (rtac conjI 1);


708 
by (rtac glb_in_lattice 1);


709 
by (rtac subset_refl 1);


710 
by (fold_goals_tac [thm "r_def"]);


711 
by (afs [glbE1] 1);


712 
qed "Bot_in_lattice";


713 


714 
Goal "Top cl: A";


715 
by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1);


716 
by (rtac (dualA_iff RS subst) 1);


717 
by (afs [export Bot_in_lattice,CL_dualCL] 1);


718 
qed "Top_in_lattice";


719 


720 
Goal "x: A ==> (x, Top cl): r";


721 
by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);

9969

722 
by (rtac someI2 1);

7085

723 
by (fold_goals_tac [thm "r_def", thm "A_def"]);


724 
by (Fast_tac 2);


725 
by (rtac conjI 1);


726 
by (rtac lubE1 2);


727 
by (afs [lub_in_lattice] 1);


728 
by (rtac subset_refl 1);


729 
qed "Top_prop";


730 


731 
Goal "x: A ==> (Bot cl, x): r";


732 
by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1);


733 
by (rtac (dualr_iff RS subst) 1);


734 
by (rtac (export Top_prop) 1);


735 
by (rtac CL_dualCL 1);


736 
by (afs [dualA_iff, thm "A_def"] 1);


737 
qed "Bot_prop";


738 


739 
Goal "x: A ==> interval r x (Top cl) ~= {}";


740 
by (rtac notI 1);


741 
by (dres_inst_tac [("a","Top cl")] equals0D 1);


742 
by (afs [interval_def] 1);


743 
by (afs [refl_def,Top_in_lattice,Top_prop] 1);


744 
qed "Top_intv_not_empty";


745 


746 
Goal "x: A ==> interval r (Bot cl) x ~= {}";


747 
by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1);


748 
by (stac interval_dual 1);


749 
by (assume_tac 2);


750 
by (afs [thm "A_def"] 1);


751 
by (rtac (dualA_iff RS subst) 1);


752 
by (rtac (export Top_in_lattice) 1);


753 
by (rtac CL_dualCL 1);


754 
by (afs [export Top_intv_not_empty,CL_dualCL,dualA_iff, thm "A_def"] 1);


755 
qed "Bot_intv_not_empty";


756 


757 
(* fixed points form a partial order *)


758 
Goal "( pset = P, order = induced P r) : PartialOrder";


759 
by (rtac po_subset_po 1);


760 
by (rtac fixfE1 1);


761 
qed "fixf_po";


762 


763 
Open_locale "Tarski";


764 


765 
Goal "Y <= A";


766 
by (rtac (fixfE1 RSN(2,subset_trans)) 1);


767 
by (rtac (thm "Y_ss") 1);


768 
qed "Y_subset_A";


769 


770 
Goal "lub Y cl : A";


771 
by (afs [Y_subset_A RS lub_in_lattice] 1);


772 
qed "lubY_in_A";


773 


774 
Goal "(lub Y cl, f (lub Y cl)): r";


775 
by (rtac lubE2 1);


776 
by (rtac Y_subset_A 1);


777 
by (rtac (CLF_E1 RS funcset_mem) 1);


778 
by (rtac lubY_in_A 1);


779 
(* Y <= P ==> f x = x *)


780 
by (rtac ballI 1);


781 
by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1);


782 
by (etac (thm "Y_ss" RS subsetD) 1);


783 
(* reduce (f x, f (lub Y cl)) : r to (x, lub Y cl): r by monotonicity *)


784 
by (res_inst_tac [("f","f")] monotoneE 1);


785 
by (rtac CLF_E2 1);


786 
by (afs [Y_subset_A RS subsetD] 1);


787 
by (rtac lubY_in_A 1);


788 
by (afs [lubE1, Y_subset_A] 1);


789 
qed "lubY_le_flubY";


790 


791 
Goalw [thm "intY1_def"] "intY1 <= A";


792 
by (rtac interval_subset 1);


793 
by (rtac lubY_in_A 1);


794 
by (rtac Top_in_lattice 1);


795 
qed "intY1_subset";


796 


797 
val intY1_elem = intY1_subset RS subsetD;


798 


799 
Goal "(lam x: intY1. f x): intY1 funcset intY1";


800 
by (rtac restrictI 1);


801 
by (afs [thm "intY1_def", interval_def] 1);


802 
by (rtac conjI 1);


803 
by (rtac transE 1);


804 
by (rtac CompleteLatticeE13 1);


805 
by (rtac lubY_le_flubY 1);


806 
(* (f (lub Y cl), f x) : r *)


807 
by (res_inst_tac [("f","f")]monotoneE 1);


808 
by (rtac CLF_E2 1);


809 
by (rtac lubY_in_A 1);


810 
by (afs [thm "intY1_def",interval_def, intY1_elem] 1);


811 
by (afs [thm "intY1_def", interval_def] 1);


812 
(* (f x, Top cl) : r *)


813 
by (rtac Top_prop 1);


814 
by (rtac (CLF_E1 RS funcset_mem) 1);


815 
by (afs [thm "intY1_def",interval_def, intY1_elem] 1);


816 
qed "intY1_func";


817 


818 
Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";


819 
by (simp_tac (simpset() addsimps [monotone_def]) 1);


820 
by (Clarify_tac 1);


821 
by (simp_tac (simpset() addsimps [induced_def]) 1);


822 
by (afs [intY1_func RS funcset_mem] 1);


823 
by (afs [restrict_apply1] 1);


824 
by (res_inst_tac [("f","f")] monotoneE 1);


825 
by (rtac CLF_E2 1);


826 
by (etac (intY1_subset RS subsetD) 2);


827 
by (etac (intY1_subset RS subsetD) 1);


828 
by (afs [induced_def] 1);


829 
qed "intY1_mono";


830 


831 
Goalw [thm "intY1_def"]


832 
"( pset = intY1, order = induced intY1 r ): CompleteLattice";


833 
by (rtac interv_is_compl_latt 1);


834 
by (rtac lubY_in_A 1);


835 
by (rtac Top_in_lattice 1);


836 
by (rtac Top_intv_not_empty 1);


837 
by (rtac lubY_in_A 1);


838 
qed "intY1_is_cl";


839 


840 
Goalw [thm "P_def"] "v : P";


841 
by (res_inst_tac [("A","intY1")] fixf_subset 1);


842 
by (rtac intY1_subset 1);


843 
by (rewrite_goals_tac [thm "v_def"]);


844 
by (rtac (simplify (simpset()) (intY1_is_cl RS export glbH_is_fixp)) 1);


845 
by (afs [CLF_def, intY1_is_cl, intY1_func, intY1_mono] 1);


846 
by (Simp_tac 1);


847 
qed "v_in_P";


848 


849 
Goalw [thm "intY1_def"]


850 
"[ z : P; ! y:Y. (y, z) : induced P r ] ==> z : intY1";


851 
by (rtac intervalI 1);


852 
by (etac (fixfE1 RS subsetD RS Top_prop) 2);


853 
by (rtac lubE2 1);


854 
by (rtac Y_subset_A 1);


855 
by (fast_tac (claset() addSEs [fixfE1 RS subsetD]) 1);


856 
by (rtac ballI 1);


857 
by (dtac bspec 1);


858 
by (assume_tac 1);


859 
by (afs [induced_def] 1);


860 
qed "z_in_interval";


861 


862 
Goal "[ z : P; ! y:Y. (y, z) : induced P r ]\


863 
\ ==> ((lam x: intY1. f x) z, z) : induced intY1 r";


864 
by (afs [induced_def,intY1_func RS funcset_mem, z_in_interval] 1);


865 
by (rtac (z_in_interval RS restrict_apply1 RS ssubst) 1);


866 
by (assume_tac 1);


867 
by (afs [induced_def] 1);


868 
by (afs [fixfE2] 1);


869 
by (rtac reflE 1);


870 
by (rtac CompleteLatticeE11 1);


871 
by (etac (fixfE1 RS subsetD) 1);


872 
qed "f'z_in_int_rel";


873 


874 
Goal "? L. islub Y ( pset = P, order = induced P r ) L";


875 
by (res_inst_tac [("x","v")] exI 1);


876 
by (simp_tac (simpset() addsimps [islub_def]) 1);


877 
(* v : P *)


878 
by (afs [v_in_P] 1);


879 
by (rtac conjI 1);


880 
(* v is lub *)


881 
(* 1. ! y:Y. (y, v) : induced P r *)


882 
by (rtac ballI 1);


883 
by (afs [induced_def, subsetD, v_in_P] 1);


884 
by (rtac conjI 1);


885 
by (etac (thm "Y_ss" RS subsetD) 1);


886 
by (res_inst_tac [("b","lub Y cl")] transE 1);


887 
by (rtac CompleteLatticeE13 1);


888 
by (rtac (lubE1 RS bspec) 1);


889 
by (rtac Y_subset_A 1);


890 
by (assume_tac 1);


891 
by (res_inst_tac [("b","Top cl")] intervalE1 1);


892 
by (afs [thm "v_def"] 1);


893 
by (fold_goals_tac [thm "intY1_def"]);


894 
by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1);


895 
by (Simp_tac 1);


896 
by (rtac subsetI 1);


897 
by (dtac CollectD 1);


898 
by (etac conjunct2 1);


899 
(* v is LEAST ub *)


900 
by (Clarify_tac 1);


901 
by (rtac indI 1);


902 
by (afs [v_in_P] 2);


903 
by (assume_tac 2);


904 
by (rewrite_goals_tac [thm "v_def"]);


905 
by (rtac indE 1);


906 
by (rtac intY1_subset 2);


907 
by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1);


908 
by (Simp_tac 1);


909 
by (rtac subsetI 1);


910 
by (dtac CollectD 1);


911 
by (etac conjunct2 1);


912 
by (afs [f'z_in_int_rel, z_in_interval] 1);


913 
qed "tarski_full_lemma";


914 
val Tarski_full_lemma = Export tarski_full_lemma;


915 


916 
Close_locale "Tarski";


917 


918 
Goal "( pset = P, order = induced P r) : CompleteLattice";


919 
by (rtac CompleteLatticeI_simp 1);


920 
by (afs [fixf_po] 1);


921 
by (Clarify_tac 1);


922 
by (etac Tarski_full_lemma 1);


923 
qed "Tarski_full";


924 


925 


926 
Close_locale "CLF";


927 
Close_locale "CL";


928 
Close_locale "PO";


929 


930 


931 
