isabelle: src/HOL/Real/Lubs.ML@f130bcf29620 (annotated)

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title : Lubs.ML
7219 4e3f386c2e37 inserted Id: lines paulson parents: 5148 diff changeset	2	ID : $Id$
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright : 1998 University of Cambridge
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5	Description : Completeness of the reals. A few of the
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	definitions suggested by James Margetson
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	(*------------------------------------------------------------------------
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10	Rules for <= and <=
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	------------------------------------------------------------------------*)
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	12	Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	13	by (assume_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14	qed "setleI";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	15
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	16	Goalw [setle_def] "[\| S *<= x; y: S \|] ==> y <= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	17	by (Fast_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	18	qed "setleD";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	19
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	20	Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	21	by (assume_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	22	qed "setgeI";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	23
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	24	Goalw [setge_def] "[\| x <=* S; y: S \|] ==> x <= y";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	25	by (Fast_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	26	qed "setgeD";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	27
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	28	(*------------------------------------------------------------------------
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	29	Rules about leastP, ub and lub
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	30	------------------------------------------------------------------------*)
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	31	Goalw [leastP_def] "leastP P x ==> P x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	32	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	33	qed "leastPD1";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	34
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	35	Goalw [leastP_def] "leastP P x ==> x <=* Collect P";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	36	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	37	qed "leastPD2";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	38
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	39	Goal "[\| leastP P x; y: Collect P \|] ==> x <= y";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	40	by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	41	qed "leastPD3";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	42
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	43	Goalw [isLub_def,isUb_def,leastP_def]
5148 74919e8f221c More tidying and removal of "\!\!... from Goal commands paulson parents: 5143 diff changeset	44	"isLub R S x ==> S *<= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	45	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	46	qed "isLubD1";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	47
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	48	Goalw [isLub_def,isUb_def,leastP_def]
5148 74919e8f221c More tidying and removal of "\!\!... from Goal commands paulson parents: 5143 diff changeset	49	"isLub R S x ==> x: R";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	50	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	51	qed "isLubD1a";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	52
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	53	Goalw [isUb_def] "isLub R S x ==> isUb R S x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	54	by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	55	qed "isLub_isUb";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	56
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	57	Goal "[\| isLub R S x; y : S \|] ==> y <= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	58	by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	59	qed "isLubD2";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	60
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	61	Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	62	by (assume_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	63	qed "isLubD3";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	64
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	65	Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	66	by (assume_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	67	qed "isLubI1";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	68
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	69	Goalw [isLub_def,leastP_def]
5148 74919e8f221c More tidying and removal of "\!\!... from Goal commands paulson parents: 5143 diff changeset	70	"[\| isUb R S x; x <=* Collect (isUb R S) \|] ==> isLub R S x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	71	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	72	qed "isLubI2";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	73
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	74	Goalw [isUb_def] "[\| isUb R S x; y : S \|] ==> y <= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	75	by (fast_tac (claset() addDs [setleD]) 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	76	qed "isUbD";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	77
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	78	Goalw [isUb_def] "isUb R S x ==> S *<= x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	79	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	80	qed "isUbD2";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	81
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	82	Goalw [isUb_def] "isUb R S x ==> x: R";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	83	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	84	qed "isUbD2a";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	85
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	86	Goalw [isUb_def] "[\| S *<= x; x: R \|] ==> isUb R S x";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	87	by (Step_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	88	qed "isUbI";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	89
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	90	Goalw [isLub_def] "[\| isLub R S x; isUb R S y \|] ==> x <= y";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	91	by (blast_tac (claset() addSIs [leastPD3]) 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	92	qed "isLub_le_isUb";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	93
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5078 diff changeset	94	Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	95	by (etac leastPD2 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	96	qed "isLub_ubs";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	97
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	98
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	99
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	100

author	wenzelm
	Wed, 10 Jul 2002 14:47:48 +0200
changeset 13332	f130bcf29620
parent 7219	4e3f386c2e37
permissions	-rw-r--r--