(* Title : Lubs.ML
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Completeness of the reals. A few of the
definitions suggested by James Margetson
*)
open Lubs;
(*------------------------------------------------------------------------
Rules for *<= and <=*
------------------------------------------------------------------------*)
Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x";
by (assume_tac 1);
qed "setleI";
Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x";
by (Fast_tac 1);
qed "setleD";
Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S";
by (assume_tac 1);
qed "setgeI";
Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y";
by (Fast_tac 1);
qed "setgeD";
(*------------------------------------------------------------------------
Rules about leastP, ub and lub
------------------------------------------------------------------------*)
Goalw [leastP_def] "!!x. leastP P x ==> P x";
by (Step_tac 1);
qed "leastPD1";
Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P";
by (Step_tac 1);
qed "leastPD2";
Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y";
by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
qed "leastPD3";
Goalw [isLub_def,isUb_def,leastP_def]
"!!x. isLub R S x ==> S *<= x";
by (Step_tac 1);
qed "isLubD1";
Goalw [isLub_def,isUb_def,leastP_def]
"!!x. isLub R S x ==> x: R";
by (Step_tac 1);
qed "isLubD1a";
Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x";
by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
qed "isLub_isUb";
Goal "!!x. [| isLub R S x; y : S |] ==> y <= x";
by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
qed "isLubD2";
Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x";
by (assume_tac 1);
qed "isLubD3";
Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x";
by (assume_tac 1);
qed "isLubI1";
Goalw [isLub_def,leastP_def]
"!!x. [| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x";
by (Step_tac 1);
qed "isLubI2";
Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x";
by (fast_tac (claset() addDs [setleD]) 1);
qed "isUbD";
Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x";
by (Step_tac 1);
qed "isUbD2";
Goalw [isUb_def] "!!x. isUb R S x ==> x: R";
by (Step_tac 1);
qed "isUbD2a";
Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x";
by (Step_tac 1);
qed "isUbI";
Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y";
by (blast_tac (claset() addSIs [leastPD3]) 1);
qed "isLub_le_isUb";
Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S";
by (etac leastPD2 1);
qed "isLub_ubs";