HOL/ex/Tarski: new example by Florian Kammueller
authorpaulson
Mon Jul 26 16:30:50 1999 +0200 (1999-07-26)
changeset 7085e5a5f8d23f26
parent 7084 4af4f4d8035c
child 7086 f9aa63a5a8b6
HOL/ex/Tarski: new example by Florian Kammueller
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
src/HOL/ex/Tarski.ML
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Jul 26 16:29:59 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jul 26 16:30:50 1999 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4  
     1.5  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
     1.6    $(SRC)/Provers/Arith/cancel_sums.ML		\
     1.7 +  $(SRC)/Provers/Arith/assoc_fold.ML		\
     1.8 +  $(SRC)/Provers/Arith/combine_coeff.ML		\
     1.9    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    1.10    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.11    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    1.12 @@ -321,7 +323,8 @@
    1.13    ex/mesontest.ML ex/set.ML ex/Group.ML ex/Group.thy ex/IntRing.ML \
    1.14    ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
    1.15    ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
    1.16 -  ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
    1.17 +  ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
    1.18 +  ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
    1.19    ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
    1.20    ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
    1.21  	@$(ISATOOL) usedir $(OUT)/HOL ex
     2.1 --- a/src/HOL/ex/ROOT.ML	Mon Jul 26 16:29:59 1999 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Mon Jul 26 16:30:50 1999 +0200
     2.3 @@ -29,6 +29,7 @@
     2.4  
     2.5  time_use     "set.ML";
     2.6  time_use_thy "MT";
     2.7 +time_use_thy "Tarski";
     2.8  
     2.9  time_use_thy "StringEx";
    2.10  time_use_thy "BinEx";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Tarski.ML	Mon Jul 26 16:30:50 1999 +0200
     3.3 @@ -0,0 +1,931 @@
     3.4 +(*  Title:      HOL/ex/Tarski
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Kammueller, Cambridge University Computer Laboratory
     3.7 +    Copyright   1999  University of Cambridge
     3.8 +
     3.9 +Minimal version of lattice theory plus the full theorem of Tarski:
    3.10 +   The fixedpoints of a complete lattice themselves form a complete lattice.
    3.11 +
    3.12 +Illustrates first-class theories, using the Sigma representation of structures
    3.13 +*)
    3.14 +
    3.15 +
    3.16 +(* abbreviate commonly used tactic application *)
    3.17 +
    3.18 +fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
    3.19 +
    3.20 +(* Partial Order *)
    3.21 +Open_locale "PO";
    3.22 +
    3.23 +val simp_PO = simplify (simpset() addsimps [PartialOrder_def]) (thm "cl_po");
    3.24 +Addsimps [simp_PO, thm "cl_po"];
    3.25 +
    3.26 +val PO_simp = [thm "A_def", thm "r_def"];
    3.27 +
    3.28 +Goal "refl A r";
    3.29 +by (simp_tac (simpset() addsimps PO_simp) 1);
    3.30 +qed "PartialOrderE1";
    3.31 +
    3.32 +Goal "antisym r";
    3.33 +by (simp_tac (simpset() addsimps PO_simp) 1);
    3.34 +qed "PartialOrderE2";
    3.35 +
    3.36 +Goal "trans r";
    3.37 +by (simp_tac (simpset() addsimps PO_simp) 1);
    3.38 +qed "PartialOrderE3";
    3.39 +
    3.40 +Goal "[| refl A r; x: A|] ==> (x, x): r";
    3.41 +by (afs [refl_def] 1);
    3.42 +qed "reflE";
    3.43 +(* Interesting: A and r don't get bound because the proof doesn't use
    3.44 +   locale rules 
    3.45 +val reflE = "[| refl ?A ?r; ?x : ?A |] ==> (?x, ?x) : ?r" *)
    3.46 +
    3.47 +Goal "[| antisym r; (a, b): r; (b, a): r |] ==> a = b";
    3.48 +by (afs [antisym_def] 1);
    3.49 +qed "antisymE";
    3.50 +
    3.51 +Goalw [trans_def] "[| trans r; (a, b): r; (b, c): r|] ==> (a,c): r";
    3.52 +by (Fast_tac 1);
    3.53 +qed "transE";
    3.54 +
    3.55 +Goal "[| monotone f A r;  x: A; y: A; (x, y): r |] ==> (f x, f y): r";
    3.56 +by (afs [monotone_def] 1);
    3.57 +qed "monotoneE";
    3.58 +
    3.59 +Goal "S <= A ==> (| pset = S, order = induced S r |): PartialOrder";
    3.60 +by (simp_tac (simpset() addsimps [PartialOrder_def]) 1);
    3.61 +by (Step_tac 1);
    3.62 +(* refl *)
    3.63 +by (afs [refl_def,induced_def] 1);
    3.64 +by (rtac conjI 1);
    3.65 +by (Fast_tac 1);
    3.66 +by (rtac ballI 1);
    3.67 +by (rtac reflE 1);
    3.68 +by (rtac PartialOrderE1 1);
    3.69 +by (Fast_tac 1);
    3.70 +(* antisym *)
    3.71 +by (afs [antisym_def,induced_def] 1);
    3.72 +by (Step_tac 1);
    3.73 +by (rtac antisymE 1);
    3.74 +by (assume_tac 2);
    3.75 +by (assume_tac 2);
    3.76 +by (rtac PartialOrderE2 1);
    3.77 +(* trans *)
    3.78 +by (afs [trans_def,induced_def] 1);
    3.79 +by (Step_tac 1);
    3.80 +by (rtac transE 1);
    3.81 +by (assume_tac 2);
    3.82 +by (assume_tac 2);
    3.83 +by (rtac PartialOrderE3 1);
    3.84 +qed "po_subset_po";
    3.85 +
    3.86 +Goal "[| (x, y): induced S r; S <= A |] ==> (x, y): r";
    3.87 +by (afs [induced_def] 1);
    3.88 +qed "indE";
    3.89 +
    3.90 +Goal "[| (x, y): r; x: S; y: S |] ==> (x, y): induced S r";
    3.91 +by (afs [induced_def] 1);
    3.92 +qed "indI";
    3.93 +
    3.94 +(* with locales *)
    3.95 +Open_locale "CL";
    3.96 +
    3.97 +Delsimps [simp_PO, thm "cl_po"];
    3.98 +
    3.99 +val simp_CL = simplify (simpset() addsimps [CompleteLattice_def]) 
   3.100 +                       (thm "cl_co");
   3.101 +Addsimps [simp_CL, thm "cl_co"];
   3.102 +
   3.103 +Goalw [Ex_def] "(EX L. islub S cl L) = islub S cl (lub S cl)";
   3.104 +by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def]) 1);
   3.105 +qed "islub_lub";
   3.106 +
   3.107 +Goalw [Ex_def] "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
   3.108 +by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def]) 1);
   3.109 +qed "isglb_glb";
   3.110 +
   3.111 +Goal "isglb S cl = islub S (dual cl)";
   3.112 +by (afs [islub_def,isglb_def,dual_def,converse_def] 1);
   3.113 +qed "isglb_dual_islub";
   3.114 +
   3.115 +Goal "islub S cl = isglb S (dual cl)";
   3.116 +by (afs [islub_def,isglb_def,dual_def,converse_def] 1);
   3.117 +qed "islub_dual_isglb";
   3.118 +
   3.119 +Goal "dual cl : PartialOrder";
   3.120 +by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1);
   3.121 +by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1);
   3.122 +qed "dualPO";
   3.123 +
   3.124 +Goal "! S. (S <= A -->( ? L. islub S (| pset = A, order = r|) L)) \
   3.125 +\     ==> ! S. (S <= A --> (? G. isglb S (| pset = A, order = r|) G))";
   3.126 +by (Step_tac 1);
   3.127 +by (res_inst_tac
   3.128 +    [("x"," lub {y. y: A & (! k: S. (y, k): r)}(|pset = A, order = r|)")] 
   3.129 +    exI 1);
   3.130 +by (dres_inst_tac [("x","{y. y: A & (! k: S. (y,k): r)}")] spec 1);
   3.131 +by (dtac mp 1);
   3.132 +by (Fast_tac 1);
   3.133 +by (afs [islub_lub, isglb_def] 1);
   3.134 +by (afs [islub_def] 1);
   3.135 +by (Blast_tac 1);
   3.136 +qed "Rdual";
   3.137 +
   3.138 +Goal "lub S cl = glb S (dual cl)";
   3.139 +by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);
   3.140 +qed "lub_dual_glb";
   3.141 +
   3.142 +Goal "glb S cl = lub S (dual cl)";
   3.143 +by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);
   3.144 +qed "glb_dual_lub";
   3.145 +
   3.146 +Goal "CompleteLattice <= PartialOrder";
   3.147 +by (simp_tac (simpset() addsimps [PartialOrder_def, CompleteLattice_def]) 1);
   3.148 +by (Fast_tac 1);
   3.149 +qed "CL_subset_PO";
   3.150 +
   3.151 +val CompleteLatticeE1 = CL_subset_PO RS subsetD;
   3.152 +
   3.153 +Goal "! S.  S <= A --> (? L. islub S cl L)";
   3.154 +by (simp_tac (simpset() addsimps PO_simp) 1);
   3.155 +qed "CompleteLatticeE2";
   3.156 +
   3.157 +Goal "! S.  S <= A --> (? G. isglb S cl G)";
   3.158 +by (simp_tac (simpset() addsimps PO_simp) 1);
   3.159 +qed "CompleteLatticeE3";
   3.160 +
   3.161 +Addsimps [CompleteLatticeE1 RS (export simp_PO)];
   3.162 +
   3.163 +Goal "refl A r";
   3.164 +by (simp_tac (simpset() addsimps PO_simp) 1);
   3.165 +qed "CompleteLatticeE11";
   3.166 +
   3.167 +Goal "antisym r";
   3.168 +by (simp_tac (simpset() addsimps PO_simp) 1);
   3.169 +qed "CompleteLatticeE12";
   3.170 +
   3.171 +Goal "trans r";
   3.172 +by (afs (PO_simp) 1);
   3.173 +qed "CompleteLatticeE13";
   3.174 +
   3.175 +Goal "[| po : PartialOrder; (! S. S <= po.<A> --> (? L. islub S po L));\
   3.176 +\  (! S. S <= po.<A> --> (? G. isglb S po G))|] ==> po: CompleteLattice";
   3.177 +by (afs [CompleteLattice_def] 1);
   3.178 +qed "CompleteLatticeI";
   3.179 +
   3.180 +Goal "dual cl : CompleteLattice";
   3.181 +by (simp_tac (simpset() addsimps [CompleteLattice_def,dual_def]) 1);
   3.182 +by (fold_goals_tac [dual_def]);
   3.183 +by (simp_tac (simpset() addsimps [islub_dual_isglb RS sym,
   3.184 +				  isglb_dual_islub RS sym,
   3.185 +				  export dualPO]) 1);
   3.186 +qed "CL_dualCL";
   3.187 +
   3.188 +Goal "(dual cl.<A>) = cl.<A>";
   3.189 +by (simp_tac (simpset() addsimps [dual_def]) 1);
   3.190 +qed "dualA_iff";
   3.191 +
   3.192 +Goal "((x, y): (dual cl.<r>)) = ((y, x): cl.<r>)";
   3.193 +by (simp_tac (simpset() addsimps [dual_def]) 1);
   3.194 +qed "dualr_iff";
   3.195 +
   3.196 +Goal "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)";
   3.197 +by (afs [monotone_def,dualA_iff,dualr_iff] 1);
   3.198 +qed "monotone_dual";
   3.199 +
   3.200 +Goal "[| x: A; y: A|] ==> interval r x y = interval (dual cl.<r>) y x";
   3.201 +by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1);
   3.202 +by (fold_goals_tac [thm "r_def"]);
   3.203 +by (Fast_tac 1);
   3.204 +qed "interval_dual";
   3.205 +
   3.206 +Goal "[| trans r; interval r a b ~= {} |] ==> (a, b): r";
   3.207 +by (afs [interval_def] 1);
   3.208 +by (rewtac trans_def);
   3.209 +by (Blast_tac 1);
   3.210 +qed "interval_not_empty";
   3.211 +
   3.212 +Goal "x: interval r a b ==> (a, x): r";
   3.213 +by (afs [interval_def] 1);
   3.214 +qed "intervalE1";
   3.215 +
   3.216 +Goal "[| a: A; b: A; interval r a b ~= {} |] ==> a: interval r a b";
   3.217 +by (simp_tac (simpset() addsimps [interval_def]) 1);
   3.218 +by (afs [PartialOrderE3,interval_not_empty] 1);
   3.219 +by (afs [PartialOrderE1 RS reflE] 1);
   3.220 +qed "left_in_interval";
   3.221 +
   3.222 +Goal "[| a: A; b: A; interval r a b ~= {} |] ==> b: interval r a b";
   3.223 +by (simp_tac (simpset() addsimps [interval_def]) 1);
   3.224 +by (afs [PartialOrderE3,interval_not_empty] 1);
   3.225 +by (afs [PartialOrderE1 RS reflE] 1);
   3.226 +qed "right_in_interval";
   3.227 +
   3.228 +Goal "[| (| pset = A, order = r |) : PartialOrder;\
   3.229 +\        ! S. S <= A --> (? L. islub S (| pset = A, order = r |)  L) |] \
   3.230 +\   ==> (| pset = A, order = r |) : CompleteLattice";
   3.231 +by (afs [CompleteLatticeI, Rdual] 1);
   3.232 +qed "CompleteLatticeI_simp";
   3.233 +
   3.234 +(* sublattice *)
   3.235 +Goal "S <<= cl ==> S <= A";
   3.236 +by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1);
   3.237 +qed "sublatticeE1";
   3.238 +
   3.239 +Goal "S <<= cl  ==> (| pset = S, order = induced S r |) : CompleteLattice";
   3.240 +by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1);
   3.241 +qed "sublatticeE2";
   3.242 +
   3.243 +Goal "[| S <= A; (| pset = S, order = induced S r |) : CompleteLattice |] ==> S <<= cl";
   3.244 +by (afs ([sublattice_def] @ PO_simp) 1);
   3.245 +qed "sublatticeI";
   3.246 +
   3.247 +(* lub *)
   3.248 +Goal "[| S <= A; islub S cl x; islub S cl L|] ==> x = L";
   3.249 +by (rtac antisymE 1); 
   3.250 +by (rtac CompleteLatticeE12 1);
   3.251 +by (rewtac islub_def);
   3.252 +by (rotate_tac ~1 1);
   3.253 +by (etac conjE 1);
   3.254 +by (dtac conjunct2 1);
   3.255 +by (dtac conjunct1 1);
   3.256 +by (dtac conjunct2 1);
   3.257 +by (rotate_tac ~1 1);
   3.258 +by (dres_inst_tac [("x","L")] bspec 1);
   3.259 +by (assume_tac 1);
   3.260 +by (fold_goals_tac [thm "r_def"]);
   3.261 +by (etac mp 1);
   3.262 +by (assume_tac 1);
   3.263 +(* (L, x) : (cl .<r>) *)
   3.264 +by (rotate_tac ~1 1);
   3.265 +by (etac conjE 1);
   3.266 +by (rotate_tac ~1 1);
   3.267 +by (dtac conjunct2 1);
   3.268 +by (dtac bspec 1);
   3.269 +by (etac conjunct1 1);
   3.270 +by (etac mp 1);
   3.271 +by (etac (conjunct2 RS conjunct1) 1);
   3.272 +qed "lub_unique";
   3.273 +
   3.274 +Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r";
   3.275 +by (rtac exE 1);
   3.276 +by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
   3.277 +by (assume_tac 1);
   3.278 +by (rewrite_goals_tac [lub_def,least_def]);
   3.279 +by (stac select_equality 1);
   3.280 +by (rtac conjI 1);
   3.281 +by (afs [islub_def] 2);
   3.282 +by (etac conjunct2 2);
   3.283 +by (afs [islub_def] 1);
   3.284 +by (rtac lub_unique 1);
   3.285 +by (afs [thm "A_def"] 1);
   3.286 +by (afs [islub_def] 1);
   3.287 +by (assume_tac 1);
   3.288 +by (afs [islub_def,thm "r_def"] 1);
   3.289 +qed "lubE1";
   3.290 +
   3.291 +Goal "[| S <= A; L: A; ! x: S. (x,L): r |] ==> (lub S cl, L): r";
   3.292 +by (rtac exE 1);
   3.293 +by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
   3.294 +by (assume_tac 1);
   3.295 +by (rewrite_goals_tac [lub_def,least_def]);
   3.296 +by (stac select_equality 1);
   3.297 +by (rtac conjI 1);
   3.298 +by (afs [islub_def] 2);
   3.299 +by (etac conjunct2 2);
   3.300 +by (afs [islub_def] 1);
   3.301 +by (rtac lub_unique 1);
   3.302 +by (afs [thm "A_def"] 1);
   3.303 +by (afs [islub_def] 1);
   3.304 +by (assume_tac 1);
   3.305 +by (afs [islub_def] 1);
   3.306 +by (dtac conjunct2 1);
   3.307 +by (dtac conjunct2 1);
   3.308 +by (rotate_tac 3 1);
   3.309 +by (dtac bspec 1);
   3.310 +by (fold_goals_tac [thm "r_def"]);
   3.311 +by (etac mp 2);
   3.312 +by (afs [thm "A_def"] 1);
   3.313 +by (assume_tac 1);
   3.314 +qed "lubE2";
   3.315 +
   3.316 +Goal "[| S <= A |] ==> lub S cl : A";  
   3.317 +by (rtac exE 1);
   3.318 +by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
   3.319 +by (assume_tac 1);
   3.320 +by (rewrite_goals_tac [lub_def,least_def]);
   3.321 +by (stac select_equality 1);
   3.322 +by (afs [islub_def] 1);
   3.323 +by (afs [islub_def, thm "A_def"] 2);
   3.324 +by (rtac lub_unique 1);
   3.325 +by (afs [thm "A_def"] 1);
   3.326 +by (afs [islub_def] 1);
   3.327 +by (assume_tac 1);
   3.328 +qed "lub_in_lattice";
   3.329 +
   3.330 +Goal "[| S <= A; L: A; ! x: S. (x,L): r;\
   3.331 +\ ! z: A. (! y: S. (y,z): r) --> (L,z): r |] ==> L = lub S cl";
   3.332 +by (rtac lub_unique 1);
   3.333 +by (assume_tac 1);
   3.334 +by (afs ([islub_def] @ PO_simp) 1);
   3.335 +by (rewtac islub_def);
   3.336 +by (rtac conjI 1);
   3.337 +by (fold_goals_tac PO_simp);
   3.338 +by (rtac lub_in_lattice 1);
   3.339 +by (assume_tac 1);
   3.340 +by (afs [lubE1, lubE2] 1);
   3.341 +qed "lubI";
   3.342 +
   3.343 +Goal "[| S <= A; islub S cl L |] ==> L = lub S cl";
   3.344 +by (afs ([lubI, islub_def] @ PO_simp) 1);
   3.345 +qed "lubIa";
   3.346 +
   3.347 +Goal "islub S cl L ==> L : A";
   3.348 +by (afs [islub_def, thm "A_def"] 1);
   3.349 +qed "islub_in_lattice";
   3.350 +
   3.351 +Goal "islub S cl L ==> ! y: S. (y, L): r";
   3.352 +by (afs [islub_def, thm "r_def"] 1);
   3.353 +qed "islubE1";
   3.354 +
   3.355 +Goal "[| islub S cl L; \
   3.356 +\      z: A; ! y: S. (y, z): r|] ==> (L, z): r";
   3.357 +by (afs ([islub_def] @ PO_simp) 1);
   3.358 +qed "islubE2";
   3.359 +
   3.360 +Goal "[| S <= A |] ==> ? L. islub S cl L";
   3.361 +by (afs [thm "A_def"] 1);
   3.362 +qed "islubE";
   3.363 +
   3.364 +Goal "[| L: A; ! y: S. (y, L): r; \
   3.365 +\     (!z: A. (! y: S. (y, z):r) --> (L, z): r)|] ==> islub S cl L";
   3.366 +by (afs ([islub_def] @ PO_simp) 1);
   3.367 +qed "islubI";
   3.368 +
   3.369 +(* glb *)
   3.370 +Goal "S <= A ==> glb S cl : A";  
   3.371 +by (stac glb_dual_lub 1);
   3.372 +by (afs [thm "A_def"] 1);
   3.373 +by (rtac (dualA_iff RS subst) 1);
   3.374 +by (rtac (export lub_in_lattice) 1);
   3.375 +by (rtac CL_dualCL 1);
   3.376 +by (afs [dualA_iff] 1);
   3.377 +qed "glb_in_lattice";
   3.378 +
   3.379 +Goal "S <= A ==> ! x: S. (glb S cl, x): r";
   3.380 +by (stac glb_dual_lub 1);
   3.381 +by (rtac ballI 1);
   3.382 +by (afs [thm "r_def"] 1);
   3.383 +by (rtac (dualr_iff RS subst) 1);
   3.384 +by (rtac (export lubE1 RS bspec) 1);
   3.385 +by (rtac CL_dualCL 1);
   3.386 +by (afs [dualA_iff, thm "A_def"] 1);
   3.387 +by (assume_tac 1);
   3.388 +qed "glbE1";
   3.389 +
   3.390 +(* Reduce the sublattice property by using substructural properties! *)
   3.391 +(* abandoned see Tarski_4.ML *)
   3.392 +
   3.393 +Open_locale "CLF";
   3.394 +
   3.395 +val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl");
   3.396 +Addsimps [simp_CLF, thm "f_cl"];
   3.397 +
   3.398 +Goal "f : A funcset A";
   3.399 +by (simp_tac (simpset() addsimps [thm "A_def"]) 1);
   3.400 +qed "CLF_E1";
   3.401 +
   3.402 +Goal "monotone f A r";
   3.403 +by (simp_tac (simpset() addsimps PO_simp) 1);
   3.404 +qed "CLF_E2";
   3.405 +
   3.406 +Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}";
   3.407 +by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
   3.408 +by (afs [dualA_iff] 1);
   3.409 +qed "CLF_dual";
   3.410 +
   3.411 +(* fixed points *)
   3.412 +Goal "P <= A";
   3.413 +by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);
   3.414 +by (Fast_tac 1);
   3.415 +qed "fixfE1";
   3.416 +
   3.417 +Goal "x: P ==> f x = x";
   3.418 +by (afs [thm "P_def", fix_def] 1);
   3.419 +qed "fixfE2";
   3.420 +
   3.421 +Goal "[| A <= B; x: fix (lam y: A. f y) A |] ==> x: fix f B";
   3.422 +by (forward_tac [export fixfE2] 1);
   3.423 +by (dtac ((export fixfE1) RS subsetD) 1);
   3.424 +by (afs [fix_def] 1);
   3.425 +by (rtac conjI 1);
   3.426 +by (Fast_tac 1);
   3.427 +by (res_inst_tac [("P","% y. f x = y")] subst 1);
   3.428 +by (assume_tac 1);
   3.429 +by (rtac sym 1);
   3.430 +by (etac restrict_apply1 1);
   3.431 +qed "fixf_subset";
   3.432 +
   3.433 +(* lemmas for Tarski, lub *)
   3.434 +Goal "H = {x. (x, f x) : r & x : A} ==> (lub H cl, f (lub H cl)) : r";
   3.435 +by (rtac lubE2 1);
   3.436 +by (Fast_tac 1);
   3.437 +by (rtac (CLF_E1 RS funcset_mem) 1);
   3.438 +by (rtac lub_in_lattice 1);
   3.439 +by (Fast_tac 1);
   3.440 +(* ! x:H. (x, f (lub H r)) : r *)
   3.441 +by (rtac ballI 1);
   3.442 +by (rtac transE 1);
   3.443 +by (rtac CompleteLatticeE13 1);
   3.444 +(* instantiates (x, ???z): cl.<r> to (x, f x), because of the def of H *)
   3.445 +by (Fast_tac 1);
   3.446 +(* so it remains to show (f x, f (lub H cl)) : r *)
   3.447 +by (res_inst_tac [("f","f")] monotoneE 1);
   3.448 +by (rtac CLF_E2 1);
   3.449 +by (Fast_tac 1);
   3.450 +by (rtac lub_in_lattice 1);
   3.451 +by (Fast_tac 1);
   3.452 +by (rtac (lubE1 RS bspec) 1);
   3.453 +by (Fast_tac 1);
   3.454 +by (assume_tac 1);
   3.455 +qed "lubH_le_flubH";
   3.456 +
   3.457 +Goal "[|  H = {x. (x, f x) : r & x : A} |] ==> (f (lub H cl), lub H cl) : r";
   3.458 +by (rtac (lubE1 RS bspec) 1);
   3.459 +by (Fast_tac 1);
   3.460 +by (res_inst_tac [("t","H")] ssubst 1);
   3.461 +by (assume_tac 1);
   3.462 +by (rtac CollectI 1);
   3.463 +by (rtac conjI 1);
   3.464 +by (rtac (CLF_E1 RS funcset_mem) 2);
   3.465 +by (rtac lub_in_lattice 2);
   3.466 +by (Fast_tac 2);
   3.467 +by (res_inst_tac [("f","f")] monotoneE 1);
   3.468 +by (rtac CLF_E2 1);
   3.469 +by (afs [lubH_le_flubH] 3);
   3.470 +by (rtac (CLF_E1 RS funcset_mem) 2);
   3.471 +by (rtac lub_in_lattice 2);
   3.472 +by (Fast_tac 2);
   3.473 +by (rtac lub_in_lattice 1);
   3.474 +by (Fast_tac 1);
   3.475 +qed "flubH_le_lubH";
   3.476 +
   3.477 +Goal "H = {x. (x, f x): r & x : A} ==> lub H cl : P";
   3.478 +by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);
   3.479 +by (rtac conjI 1);
   3.480 +by (rtac lub_in_lattice 1);
   3.481 +by (Fast_tac 1);
   3.482 +by (rtac antisymE 1);
   3.483 +by (rtac CompleteLatticeE12 1);
   3.484 +by (afs [flubH_le_lubH] 1);
   3.485 +by (afs [lubH_le_flubH] 1);
   3.486 +qed "lubH_is_fixp";
   3.487 +
   3.488 +Goal "[| H = {x. (x, f x) : r & x : A};  x: P |] ==> x: H";
   3.489 +by (etac ssubst 1);
   3.490 +by (Simp_tac 1);
   3.491 +by (rtac conjI 1);
   3.492 +by (forward_tac [fixfE2] 1);
   3.493 +by (etac ssubst 1);
   3.494 +by (rtac reflE 1);
   3.495 +by (rtac CompleteLatticeE11 1);
   3.496 +by (etac (fixfE1 RS subsetD) 1);
   3.497 +by (etac (fixfE1 RS subsetD) 1);
   3.498 +qed "fix_in_H";
   3.499 +
   3.500 +Goal "H = {x. (x, f x) : r & x : A} ==> ! x: P. (x, lub H cl) : r";
   3.501 +by (rtac ballI 1);
   3.502 +by (rtac (lubE1 RS bspec) 1);
   3.503 +by (Fast_tac 1);
   3.504 +by (rtac fix_in_H 1);
   3.505 +by (REPEAT (atac 1));
   3.506 +qed "fixf_le_lubH";
   3.507 +
   3.508 +Goal "H = {x. (x, f x) : r & x : A} ==> ! L. (! y: P. (y,L): r) --> (lub H cl, L): r";
   3.509 +by (rtac allI 1);
   3.510 +by (rtac impI 1);
   3.511 +by (etac bspec 1);
   3.512 +by (rtac lubH_is_fixp 1);
   3.513 +by (assume_tac 1);
   3.514 +qed "lubH_least_fixf";
   3.515 +
   3.516 +(* Tarski fixpoint theorem 1, first part *)
   3.517 +Goal "lub P cl = lub {x. (x, f x) : r & x : A} cl";
   3.518 +by (rtac sym 1);
   3.519 +by (rtac lubI 1);
   3.520 +by (rtac fixfE1 1);
   3.521 +by (rtac lub_in_lattice 1);
   3.522 +by (Fast_tac 1);
   3.523 +by (afs [fixf_le_lubH] 1);
   3.524 +by (afs [lubH_least_fixf] 1);
   3.525 +qed "T_thm_1_lub";
   3.526 +
   3.527 +(* Tarski for glb *)
   3.528 +Goal "H = {x. (f x, x): r & x : A} ==> glb H cl : P";
   3.529 +by (full_simp_tac 
   3.530 +    (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
   3.531 +by (rtac (dualA_iff RS subst) 1);
   3.532 +by (rtac (CL_dualCL RS (export lubH_is_fixp)) 1);
   3.533 +by (rtac (thm "f_cl" RS CLF_dual) 1);
   3.534 +by (afs [dualr_iff, dualA_iff] 1);
   3.535 +qed "glbH_is_fixp";
   3.536 +
   3.537 +Goal "glb P cl = glb {x. (f x, x): r & x : A} cl";
   3.538 +by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
   3.539 +by (rtac (dualA_iff RS subst) 1);
   3.540 +by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1);
   3.541 +by (rtac (thm "f_cl" RS CLF_dual) 1);
   3.542 +by (afs [dualr_iff] 1);
   3.543 +qed "T_thm_1_glb";
   3.544 +
   3.545 +(* interval *)
   3.546 +Goal "refl A r ==> r <= A Times A";
   3.547 +by (afs [refl_def] 1);
   3.548 +qed "reflE1";
   3.549 +
   3.550 +Goal "(x, y): r ==> x: A";
   3.551 +by (rtac SigmaD1 1);
   3.552 +by (rtac (reflE1 RS subsetD) 1);
   3.553 +by (rtac CompleteLatticeE11 1);
   3.554 +by (assume_tac 1);
   3.555 +qed "rel_imp_elem";
   3.556 +
   3.557 +Goal "[| a: A; b: A |] ==> interval r a b <= A";
   3.558 +by (simp_tac (simpset() addsimps [interval_def]) 1);
   3.559 +by (rtac subsetI 1);
   3.560 +by (rtac rel_imp_elem 1);
   3.561 +by (dtac CollectD 1);
   3.562 +by (etac conjunct2 1);
   3.563 +qed "interval_subset";
   3.564 +
   3.565 +Goal "[| (a, x): r; (x, b): r |] ==> x: interval r a b";
   3.566 +by (afs [interval_def] 1);
   3.567 +qed "intervalI";
   3.568 +
   3.569 +Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (a, x): r";
   3.570 +by (Fast_tac 1);
   3.571 +qed "interval_lemma1";
   3.572 +
   3.573 +Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (x, b): r";
   3.574 +by (Fast_tac 1);
   3.575 +qed "interval_lemma2";
   3.576 +
   3.577 +Goal "[| S <= A; S ~= {};\
   3.578 +\        ! x: S. (a,x): r; ! y: S. (y, L): r |] ==> (a,L): r";
   3.579 +by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
   3.580 +qed "a_less_lub";
   3.581 +
   3.582 +Goal "[| S <= A; S ~= {};\
   3.583 +\        ! x: S. (x,b): r; ! y: S. (G, y): r |] ==> (G,b): r";
   3.584 +by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
   3.585 +qed "glb_less_b";
   3.586 +
   3.587 +Goal "[| a : A; b : A; S <= interval r a b |]==> S <= A";
   3.588 +by (afs [interval_subset RSN(2, subset_trans)] 1);
   3.589 +qed "S_intv_cl";
   3.590 +
   3.591 +Goal "[| a : A; b: A; S <= interval r a b; \
   3.592 +\      S ~= {}; islub S cl L; interval r a b ~= {} |] ==> L : interval r a b";
   3.593 +by (rtac intervalI 1);
   3.594 +by (rtac a_less_lub 1);
   3.595 +by (assume_tac 2);
   3.596 +by (afs [S_intv_cl] 1);
   3.597 +by (rtac ballI 1);
   3.598 +by (afs [interval_lemma1] 1);
   3.599 +by (afs [islubE1] 1);
   3.600 +(* (L, b) : r *)
   3.601 +by (rtac islubE2 1);
   3.602 +by (assume_tac 1);
   3.603 +by (assume_tac 1);
   3.604 +by (rtac ballI 1);
   3.605 +by (afs [interval_lemma2] 1);
   3.606 +qed "L_in_interval";
   3.607 +
   3.608 +Goal "[| a : A; b : A; interval r a b ~= {}; S <= interval r a b; isglb S cl G; \
   3.609 +\      S ~= {} |]   ==> G : interval r a b";
   3.610 +by (afs [interval_dual] 1);
   3.611 +by (rtac (export L_in_interval) 1);
   3.612 +by (rtac dualPO 1);
   3.613 +by (afs [dualA_iff, thm "A_def"] 1);
   3.614 +by (afs [dualA_iff, thm "A_def"] 1);
   3.615 +by (assume_tac 1);
   3.616 +by (afs [isglb_dual_islub] 1);
   3.617 +by (afs [isglb_dual_islub] 1);
   3.618 +by (assume_tac 1);
   3.619 +qed "G_in_interval";
   3.620 +
   3.621 +Goal "[| a: A; b: A; interval r a b ~= {} |]\
   3.622 +\  ==> (| pset = interval r a b, order = induced (interval r a b) r |) : PartialOrder";
   3.623 +by (rtac po_subset_po 1);
   3.624 +by (afs [interval_subset] 1);
   3.625 +qed "intervalPO";
   3.626 +
   3.627 +Goal "[| a : A; b : A;\
   3.628 +\   interval r a b ~= {} |] ==> ! S. S <= interval r a b -->\
   3.629 +\         (? L. islub S (| pset = interval r a b, order = induced (interval r a b) r |)  L)";
   3.630 +by (strip_tac 1);
   3.631 +by (forward_tac [S_intv_cl RS islubE] 1);
   3.632 +by (assume_tac 2);
   3.633 +by (assume_tac 1);
   3.634 +by (etac exE 1);
   3.635 +(* define the lub for the interval as: *)
   3.636 +by (res_inst_tac [("x","if S = {} then a else L")] exI 1);
   3.637 +by (rtac (export islubI) 1);
   3.638 +(* (if S = {} then a else L) : interval r a b *)
   3.639 +by (asm_full_simp_tac
   3.640 +    (simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1);
   3.641 +by (afs [left_in_interval] 1);
   3.642 +(* lub prop 1 *)
   3.643 +by (case_tac "S = {}" 1);
   3.644 +(* S = {}, y: S = False => everything *)
   3.645 +by (Fast_tac 1);
   3.646 +(* S ~= {} *)
   3.647 +by (Asm_full_simp_tac 1);
   3.648 +(* ! y:S. (y, L) : induced (interval r a b) r *)
   3.649 +by (rtac ballI 1);
   3.650 +by (afs [induced_def, L_in_interval] 1);
   3.651 +by (rtac conjI 1);
   3.652 +by (rtac subsetD 1);
   3.653 +by (afs [S_intv_cl] 1);
   3.654 +by (assume_tac 1);
   3.655 +by (afs [islubE1] 1);
   3.656 +(* ! z:interval r a b. (! y:S. (y, z) : induced (interval r a b) r -->
   3.657 +      (if S = {} then a else L, z) : induced (interval r a b) r *)
   3.658 +by (rtac ballI 1);
   3.659 +by (rtac impI 1);
   3.660 +by (case_tac "S = {}" 1);
   3.661 +(* S = {} *)
   3.662 +by (Asm_full_simp_tac 1);
   3.663 +by (afs [induced_def, interval_def] 1);
   3.664 +by (rtac conjI 1);
   3.665 +by (rtac reflE 1);
   3.666 +by (rtac CompleteLatticeE11 1);
   3.667 +by (assume_tac 1);
   3.668 +by (rtac interval_not_empty 1);
   3.669 +by (rtac CompleteLatticeE13 1);
   3.670 +by (afs [interval_def] 1);
   3.671 +(* S ~= {} *)
   3.672 +by (Asm_full_simp_tac 1);
   3.673 +by (afs [induced_def, L_in_interval] 1);
   3.674 +by (rtac islubE2 1);
   3.675 +by (assume_tac 1);
   3.676 +by (rtac subsetD 1);
   3.677 +by (assume_tac 2);
   3.678 +by (afs [S_intv_cl] 1);
   3.679 +by (Fast_tac 1);
   3.680 +qed "intv_CL_lub";
   3.681 +
   3.682 +val intv_CL_glb = intv_CL_lub RS Rdual;
   3.683 +
   3.684 +Goal "[| a: A; b: A; interval r a b ~= {} |]\
   3.685 +\       ==> interval r a b <<= cl";
   3.686 +by (rtac sublatticeI 1);
   3.687 +by (afs [interval_subset] 1);
   3.688 +by (rtac CompleteLatticeI 1);
   3.689 +by (afs [intervalPO] 1);
   3.690 +by (afs [intv_CL_lub] 1);
   3.691 +by (afs [intv_CL_glb] 1);
   3.692 +qed "interval_is_sublattice";
   3.693 +
   3.694 +val interv_is_compl_latt = interval_is_sublattice RS sublatticeE2;
   3.695 +
   3.696 +(* Top and Bottom *)
   3.697 +Goal "Top cl = Bot (dual cl)";
   3.698 +by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);
   3.699 +qed "Top_dual_Bot";
   3.700 +
   3.701 +Goal "Bot cl = Top (dual cl)";
   3.702 +by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);
   3.703 +qed "Bot_dual_Top";
   3.704 +
   3.705 +Goal "Bot cl: A";
   3.706 +by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);
   3.707 +by (rtac selectI2 1);
   3.708 +by (fold_goals_tac [thm "A_def"]);
   3.709 +by (etac conjunct1 2);
   3.710 +by (rtac conjI 1);
   3.711 +by (rtac glb_in_lattice 1);
   3.712 +by (rtac subset_refl 1);
   3.713 +by (fold_goals_tac [thm "r_def"]);
   3.714 +by (afs [glbE1] 1);
   3.715 +qed "Bot_in_lattice";
   3.716 +
   3.717 +Goal "Top cl: A";
   3.718 +by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1);
   3.719 +by (rtac (dualA_iff RS subst) 1);
   3.720 +by (afs [export Bot_in_lattice,CL_dualCL] 1);
   3.721 +qed "Top_in_lattice";
   3.722 +
   3.723 +Goal "x: A ==> (x, Top cl): r";
   3.724 +by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);
   3.725 +by (rtac selectI2 1);
   3.726 +by (fold_goals_tac [thm "r_def", thm "A_def"]);
   3.727 +by (Fast_tac 2);
   3.728 +by (rtac conjI 1);
   3.729 +by (rtac lubE1 2);
   3.730 +by (afs [lub_in_lattice] 1);
   3.731 +by (rtac subset_refl 1);
   3.732 +qed "Top_prop";
   3.733 +
   3.734 +Goal "x: A ==> (Bot cl, x): r";
   3.735 +by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1);
   3.736 +by (rtac (dualr_iff RS subst) 1);
   3.737 +by (rtac (export Top_prop) 1);
   3.738 +by (rtac CL_dualCL 1);
   3.739 +by (afs [dualA_iff, thm "A_def"] 1);
   3.740 +qed "Bot_prop";
   3.741 +
   3.742 +Goal "x: A  ==> interval r x (Top cl) ~= {}";
   3.743 +by (rtac notI 1);
   3.744 +by (dres_inst_tac [("a","Top cl")] equals0D 1);
   3.745 +by (afs [interval_def] 1);
   3.746 +by (afs [refl_def,Top_in_lattice,Top_prop] 1);
   3.747 +qed "Top_intv_not_empty";
   3.748 +
   3.749 +Goal "x: A ==> interval r (Bot cl) x ~= {}";
   3.750 +by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1);
   3.751 +by (stac interval_dual 1);
   3.752 +by (assume_tac 2);
   3.753 +by (afs [thm "A_def"] 1);
   3.754 +by (rtac (dualA_iff RS subst) 1);
   3.755 +by (rtac (export Top_in_lattice) 1);
   3.756 +by (rtac CL_dualCL 1);
   3.757 +by (afs [export Top_intv_not_empty,CL_dualCL,dualA_iff, thm "A_def"] 1);
   3.758 +qed "Bot_intv_not_empty";
   3.759 +
   3.760 +(* fixed points form a partial order *)
   3.761 +Goal "(| pset = P, order = induced P r|) : PartialOrder";
   3.762 +by (rtac po_subset_po 1);
   3.763 +by (rtac fixfE1 1);
   3.764 +qed "fixf_po";
   3.765 +
   3.766 +Open_locale "Tarski";
   3.767 +
   3.768 +Goal "Y <= A";
   3.769 +by (rtac (fixfE1 RSN(2,subset_trans)) 1);
   3.770 +by (rtac (thm "Y_ss") 1);
   3.771 +qed "Y_subset_A";
   3.772 +
   3.773 +Goal "lub Y cl : A";
   3.774 +by (afs [Y_subset_A RS lub_in_lattice] 1);
   3.775 +qed "lubY_in_A";
   3.776 +
   3.777 +Goal "(lub Y cl, f (lub Y cl)): r";
   3.778 +by (rtac lubE2 1);
   3.779 +by (rtac Y_subset_A 1);
   3.780 +by (rtac (CLF_E1 RS funcset_mem) 1);
   3.781 +by (rtac lubY_in_A 1);
   3.782 +(* Y <= P ==> f x = x *)
   3.783 +by (rtac ballI 1);
   3.784 +by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1);
   3.785 +by (etac (thm "Y_ss" RS subsetD) 1);
   3.786 +(* reduce (f x, f (lub Y cl)) : r to (x, lub Y cl): r by monotonicity *)
   3.787 +by (res_inst_tac [("f","f")] monotoneE 1);
   3.788 +by (rtac CLF_E2 1);
   3.789 +by (afs [Y_subset_A RS subsetD] 1);
   3.790 +by (rtac lubY_in_A 1);
   3.791 +by (afs [lubE1, Y_subset_A] 1);
   3.792 +qed "lubY_le_flubY";
   3.793 +
   3.794 +Goalw [thm "intY1_def"] "intY1 <= A";
   3.795 +by (rtac interval_subset 1);
   3.796 +by (rtac lubY_in_A 1);
   3.797 +by (rtac Top_in_lattice 1);
   3.798 +qed "intY1_subset";
   3.799 +
   3.800 +val intY1_elem = intY1_subset RS subsetD;
   3.801 +
   3.802 +Goal "(lam x: intY1. f x): intY1 funcset intY1";
   3.803 +by (rtac restrictI 1);
   3.804 +by (afs [thm "intY1_def", interval_def] 1);
   3.805 +by (rtac conjI 1);
   3.806 +by (rtac transE 1);
   3.807 +by (rtac CompleteLatticeE13 1);
   3.808 +by (rtac lubY_le_flubY 1);
   3.809 +(* (f (lub Y cl), f x) : r *)
   3.810 +by (res_inst_tac [("f","f")]monotoneE 1);
   3.811 +by (rtac CLF_E2 1);
   3.812 +by (rtac lubY_in_A 1);
   3.813 +by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
   3.814 +by (afs [thm "intY1_def", interval_def] 1);
   3.815 +(* (f x, Top cl) : r *)
   3.816 +by (rtac Top_prop 1);
   3.817 +by (rtac (CLF_E1 RS funcset_mem) 1);
   3.818 +by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
   3.819 +qed "intY1_func";
   3.820 +
   3.821 +Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";
   3.822 +by (simp_tac (simpset() addsimps [monotone_def]) 1);
   3.823 +by (Clarify_tac 1);
   3.824 +by (simp_tac (simpset() addsimps [induced_def]) 1);
   3.825 +by (afs [intY1_func RS funcset_mem] 1);
   3.826 +by (afs [restrict_apply1] 1);
   3.827 +by (res_inst_tac [("f","f")] monotoneE 1);
   3.828 +by (rtac CLF_E2 1);
   3.829 +by (etac (intY1_subset RS subsetD) 2);
   3.830 +by (etac (intY1_subset RS subsetD) 1);
   3.831 +by (afs [induced_def] 1);
   3.832 +qed "intY1_mono";
   3.833 +
   3.834 +Goalw [thm "intY1_def"]
   3.835 +    "(| pset = intY1, order = induced intY1 r |): CompleteLattice";
   3.836 +by (rtac interv_is_compl_latt 1);
   3.837 +by (rtac lubY_in_A 1);
   3.838 +by (rtac Top_in_lattice 1);
   3.839 +by (rtac Top_intv_not_empty 1);
   3.840 +by (rtac lubY_in_A 1);
   3.841 +qed "intY1_is_cl";
   3.842 +
   3.843 +Goalw  [thm "P_def"] "v : P";
   3.844 +by (res_inst_tac [("A","intY1")] fixf_subset 1);
   3.845 +by (rtac intY1_subset 1);
   3.846 +by (rewrite_goals_tac [thm "v_def"]);
   3.847 +by (rtac (simplify (simpset()) (intY1_is_cl RS export glbH_is_fixp)) 1);
   3.848 +by (afs [CLF_def, intY1_is_cl, intY1_func, intY1_mono] 1);
   3.849 +by (Simp_tac 1);
   3.850 +qed "v_in_P";
   3.851 +
   3.852 +Goalw [thm "intY1_def"]
   3.853 +     "[| z : P; ! y:Y. (y, z) : induced P r |] ==> z : intY1";
   3.854 +by (rtac intervalI 1);
   3.855 +by (etac (fixfE1 RS subsetD RS Top_prop) 2);
   3.856 +by (rtac lubE2 1);
   3.857 +by (rtac Y_subset_A 1);
   3.858 +by (fast_tac (claset() addSEs [fixfE1 RS subsetD]) 1);
   3.859 +by (rtac ballI 1);
   3.860 +by (dtac bspec 1);
   3.861 +by (assume_tac 1);
   3.862 +by (afs [induced_def] 1);
   3.863 +qed "z_in_interval";
   3.864 +
   3.865 +Goal "[| z : P; ! y:Y. (y, z) : induced P r |]\
   3.866 +\     ==> ((lam x: intY1. f x) z, z) : induced intY1 r";
   3.867 +by (afs [induced_def,intY1_func RS funcset_mem, z_in_interval] 1);
   3.868 +by (rtac (z_in_interval RS restrict_apply1 RS ssubst) 1);
   3.869 +by (assume_tac 1);
   3.870 +by (afs [induced_def] 1);
   3.871 +by (afs [fixfE2] 1);
   3.872 +by (rtac reflE 1);
   3.873 +by (rtac CompleteLatticeE11 1);
   3.874 +by (etac (fixfE1 RS subsetD) 1);
   3.875 +qed "f'z_in_int_rel";
   3.876 +
   3.877 +Goal "? L. islub Y (| pset = P, order = induced P r |) L";
   3.878 +by (res_inst_tac [("x","v")] exI 1);
   3.879 +by (simp_tac (simpset() addsimps [islub_def]) 1);
   3.880 +(* v : P *)
   3.881 +by (afs [v_in_P] 1);
   3.882 +by (rtac conjI 1);
   3.883 +(* v is lub *)
   3.884 +(*  1. ! y:Y. (y, v) : induced P r *)
   3.885 +by (rtac ballI 1);
   3.886 +by (afs [induced_def, subsetD, v_in_P] 1);
   3.887 +by (rtac conjI 1);
   3.888 +by (etac (thm "Y_ss" RS subsetD) 1);
   3.889 +by (res_inst_tac [("b","lub Y cl")] transE 1);
   3.890 +by (rtac CompleteLatticeE13 1);
   3.891 +by (rtac (lubE1 RS bspec) 1);
   3.892 +by (rtac Y_subset_A 1);
   3.893 +by (assume_tac 1);
   3.894 +by (res_inst_tac [("b","Top cl")] intervalE1 1);
   3.895 +by (afs [thm "v_def"] 1);
   3.896 +by (fold_goals_tac [thm "intY1_def"]);
   3.897 +by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1);
   3.898 +by (Simp_tac 1);
   3.899 +by (rtac subsetI 1);
   3.900 +by (dtac CollectD 1);
   3.901 +by (etac conjunct2 1);
   3.902 +(* v is LEAST ub *)
   3.903 +by (Clarify_tac 1);
   3.904 +by (rtac indI 1);
   3.905 +by (afs [v_in_P] 2);
   3.906 +by (assume_tac 2);
   3.907 +by (rewrite_goals_tac [thm "v_def"]);
   3.908 +by (rtac indE 1);
   3.909 +by (rtac intY1_subset 2);
   3.910 +by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1);
   3.911 +by (Simp_tac 1);
   3.912 +by (rtac subsetI 1);
   3.913 +by (dtac CollectD 1);
   3.914 +by (etac conjunct2 1);
   3.915 +by (afs [f'z_in_int_rel, z_in_interval] 1);
   3.916 +qed "tarski_full_lemma";
   3.917 +val Tarski_full_lemma = Export tarski_full_lemma;
   3.918 +
   3.919 +Close_locale "Tarski";
   3.920 +
   3.921 +Goal "(| pset = P, order = induced P r|) : CompleteLattice";
   3.922 +by (rtac CompleteLatticeI_simp 1);
   3.923 +by (afs [fixf_po] 1);
   3.924 +by (Clarify_tac 1);
   3.925 +by (etac Tarski_full_lemma 1);
   3.926 +qed "Tarski_full";
   3.927 +
   3.928 +
   3.929 +Close_locale "CLF";
   3.930 +Close_locale "CL";
   3.931 +Close_locale "PO";
   3.932 +
   3.933 +
   3.934 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/Tarski.thy	Mon Jul 26 16:30:50 1999 +0200
     4.3 @@ -0,0 +1,141 @@
     4.4 +(*  Title:      HOL/ex/Tarski
     4.5 +    ID:         $Id$
     4.6 +    Author:     Florian Kammueller, Cambridge University Computer Laboratory
     4.7 +    Copyright   1999  University of Cambridge
     4.8 +
     4.9 +Minimal version of lattice theory plus the full theorem of Tarski:
    4.10 +   The fixedpoints of a complete lattice themselves form a complete lattice.
    4.11 +
    4.12 +Illustrates first-class theories, using the Sigma representation of structures
    4.13 +*)
    4.14 +
    4.15 +Tarski = Main + 
    4.16 +
    4.17 +
    4.18 +record 'a potype = 
    4.19 +  pset  :: "'a set"
    4.20 +  order :: "('a * 'a) set"
    4.21 +
    4.22 +syntax
    4.23 +  "@pset" :: "'a potype => 'a set"             ("_ .<A>"  [90] 90)
    4.24 +  "@order" :: "'a potype => ('a *'a)set"       ("_ .<r>"  [90] 90) 
    4.25 +
    4.26 +translations
    4.27 +  "po.<A>" == "pset po"
    4.28 +  "po.<r>" == "order po"
    4.29 +
    4.30 +constdefs
    4.31 +  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
    4.32 +    "monotone f A r == ! x: A. ! y: A. (x, y): r --> ((f x), (f y)) : r"
    4.33 +
    4.34 +  least :: "['a => bool, 'a potype] => 'a"
    4.35 +   "least P po == @ x. x: po.<A> & P x &
    4.36 +                       (! y: po.<A>. P y --> (x,y): po.<r>)"
    4.37 +
    4.38 +  greatest :: "['a => bool, 'a potype] => 'a"
    4.39 +   "greatest P po == @ x. x: po.<A> & P x &
    4.40 +                          (! y: po.<A>. P y --> (y,x): po.<r>)"
    4.41 +
    4.42 +  lub  :: "['a set, 'a potype] => 'a"
    4.43 +   "lub S po == least (%x. ! y: S. (y,x): po.<r>) po"
    4.44 +
    4.45 +  glb  :: "['a set, 'a potype] => 'a"
    4.46 +   "glb S po == greatest (%x. ! y: S. (x,y): po.<r>) po"
    4.47 +
    4.48 +  islub :: "['a set, 'a potype, 'a] => bool"
    4.49 +   "islub S po == %L. (L: po.<A> & (! y: S. (y,L): po.<r>) &
    4.50 +                      (! z:po.<A>. (! y: S. (y,z): po.<r>) --> (L,z): po.<r>))"
    4.51 +
    4.52 +  isglb :: "['a set, 'a potype, 'a] => bool"
    4.53 +   "isglb S po == %G. (G: po.<A> & (! y: S. (G,y): po.<r>) &
    4.54 +                     (! z: po.<A>. (! y: S. (z,y): po.<r>) --> (z,G): po.<r>))"
    4.55 +
    4.56 +  fix    :: "[('a => 'a), 'a set] => 'a set"
    4.57 +   "fix f A  == {x. x: A & f x = x}"
    4.58 +
    4.59 +  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
    4.60 +   "interval r a b == {x. (a,x): r & (x,b): r}"
    4.61 +
    4.62 +
    4.63 +constdefs
    4.64 +  Bot :: "'a potype => 'a"
    4.65 +   "Bot po == least (%x. True) po"
    4.66 +
    4.67 +  Top :: "'a potype => 'a"
    4.68 +   "Top po == greatest (%x. True) po"
    4.69 +
    4.70 +  PartialOrder :: "('a potype) set"
    4.71 +   "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
    4.72 +		        trans (P.<r>)}"
    4.73 +
    4.74 +  CompleteLattice :: "('a potype) set"
    4.75 +   "CompleteLattice == {cl. cl: PartialOrder & 
    4.76 +			(! S. S <= cl.<A> --> (? L. islub S cl L)) &
    4.77 +			(! S. S <= cl.<A> --> (? G. isglb S cl G))}"
    4.78 +
    4.79 +  CLF :: "('a potype * ('a => 'a)) set"
    4.80 +   "CLF == SIGMA cl: CompleteLattice.
    4.81 +             {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
    4.82 +  
    4.83 +  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
    4.84 +   "induced A r == {(a,b). a : A & b: A & (a,b): r}"
    4.85 +
    4.86 +
    4.87 +
    4.88 +
    4.89 +constdefs
    4.90 +  sublattice :: "('a potype * 'a set)set"
    4.91 +   "sublattice == 
    4.92 +      SIGMA cl: CompleteLattice.
    4.93 +          {S. S <= cl.<A> &
    4.94 +	   (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
    4.95 +
    4.96 +syntax
    4.97 +  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
    4.98 +
    4.99 +translations
   4.100 +  "S <<= cl" == "S : sublattice ^^ {cl}"
   4.101 +
   4.102 +constdefs
   4.103 +  dual :: "'a potype => 'a potype"
   4.104 +   "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
   4.105 +
   4.106 +locale PO = 
   4.107 +fixes 
   4.108 +  cl :: "'a potype"
   4.109 +  A  :: "'a set"
   4.110 +  r  :: "('a * 'a) set"
   4.111 +assumes 
   4.112 +  cl_po  "cl : PartialOrder"
   4.113 +defines
   4.114 +  A_def "A == cl.<A>"
   4.115 +  r_def "r == cl.<r>"
   4.116 +
   4.117 +locale CL = PO +
   4.118 +fixes 
   4.119 +assumes 
   4.120 +  cl_co  "cl : CompleteLattice"
   4.121 +
   4.122 +locale CLF = CL +
   4.123 +fixes
   4.124 +  f :: "'a => 'a"
   4.125 +  P :: "'a set"
   4.126 +assumes 
   4.127 +  f_cl "f : CLF ^^{cl}"
   4.128 +defines
   4.129 +  P_def "P == fix f A"
   4.130 +
   4.131 +
   4.132 +locale Tarski = CLF + 
   4.133 +fixes
   4.134 +  Y :: "'a set"
   4.135 +  intY1 :: "'a set"
   4.136 +  v     :: "'a"
   4.137 +assumes
   4.138 +  Y_ss "Y <= P"
   4.139 +defines
   4.140 +  intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
   4.141 +  v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
   4.142 +	          (| pset=intY1, order=induced intY1 r|)"
   4.143 +
   4.144 +end
   4.145 \ No newline at end of file