Menu
▾
▴
[Hol-checkins] CVS: hol98/src/real realScript.sml,1.20,1.21 realSimps.sml,1.4,1.5
|
From: Joe H. <je...@us...> - 2002-12-16 01:17:09
|
Update of /cvsroot/hol/hol98/src/real
In directory sc8-pr-cvs1:/tmp/cvs-serv19892
Modified Files:
realScript.sml realSimps.sml
Log Message:
A really useful theorem about supremums: for any 0 < e, you can
always gets within e of the supremum.
Index: realScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/real/realScript.sml,v
retrieving revision 1.20
retrieving revision 1.21
diff -b -C2 -d -r1.20 -r1.21
*** realScript.sml 6 Dec 2002 05:13:22 -0000 1.20
--- realScript.sml 16 Dec 2002 01:17:06 -0000 1.21
***************
*** 2543,2546 ****
--- 2543,2554 ----
THEN PROVE_TAC [REAL_DOWN]);
+ val REAL_BIGNUM = store_thm
+ ("REAL_BIGNUM",
+ ``!r : real. ?n : num. r < &n``,
+ GEN_TAC
+ THEN MP_TAC (Q.SPEC `1` REAL_ARCH)
+ THEN REWRITE_TAC [REAL_LT_01, REAL_MUL_RID]
+ THEN PROVE_TAC []);
+
(* ------------------------------------------------------------------------- *)
(* Define a constant for extracting "the positive part" of real numbers. *)
***************
*** 2596,2607 ****
val REAL_LE_MIN = store_thm
("REAL_LE_MIN",
! ``!x y z. z <= x /\ z <= y ==> z <= min x y``,
! RW_TAC boolSimps.bool_ss [min_def]);
val REAL_MIN_LE = store_thm
("REAL_MIN_LE",
! ``!x y. min x y <= x /\ min x y <= y``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_REFL]
! THEN PROVE_TAC [REAL_LE_TOTAL]);
val REAL_MIN_ALT = store_thm
--- 2604,2626 ----
val REAL_LE_MIN = store_thm
("REAL_LE_MIN",
! ``!z x y. z <= min x y = z <= x /\ z <= y``,
! RW_TAC boolSimps.bool_ss [min_def]
! THEN PROVE_TAC [REAL_LE_TRANS, REAL_LE_TOTAL]);
val REAL_MIN_LE = store_thm
("REAL_MIN_LE",
! ``!z x y. min x y <= z = x <= z \/ y <= z``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_REFL]
! THEN PROVE_TAC [REAL_LE_TOTAL, REAL_LE_TRANS]);
!
! val REAL_MIN_LE1 = store_thm
! ("REAL_MIN_LE1",
! ``!x y. min x y <= x``,
! RW_TAC boolSimps.bool_ss [REAL_MIN_LE, REAL_LE_REFL]);
!
! val REAL_MIN_LE2 = store_thm
! ("REAL_MIN_LE2",
! ``!x y. min x y <= y``,
! RW_TAC boolSimps.bool_ss [REAL_MIN_LE, REAL_LE_REFL]);
val REAL_MIN_ALT = store_thm
***************
*** 2613,2617 ****
val REAL_MIN_LE_LIN = store_thm
("REAL_MIN_LE_LIN",
! ``!x y z. 0 <= z /\ z <= 1 ==> min x y <= z * x + (1 - z) * y``,
RW_TAC boolSimps.bool_ss []
THEN MP_TAC (Q.SPECL [`x`, `y`] REAL_LE_TOTAL)
--- 2632,2636 ----
val REAL_MIN_LE_LIN = store_thm
("REAL_MIN_LE_LIN",
! ``!z x y. 0 <= z /\ z <= 1 ==> min x y <= z * x + (1 - z) * y``,
RW_TAC boolSimps.bool_ss []
THEN MP_TAC (Q.SPECL [`x`, `y`] REAL_LE_TOTAL)
***************
*** 2638,2649 ****
val REAL_MIN_ADD = store_thm
("REAL_MIN_ADD",
! ``!x y z. min (x + z) (y + z) = min x y + z``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_RADD]);
val REAL_MIN_SUB = store_thm
("REAL_MIN_SUB",
! ``!x y z. min (x - z) (y - z) = min x y - z``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]);
(* ------------------------------------------------------------------------- *)
(* Define the minimum of two real numbers *)
--- 2657,2674 ----
val REAL_MIN_ADD = store_thm
("REAL_MIN_ADD",
! ``!z x y. min (x + z) (y + z) = min x y + z``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_RADD]);
val REAL_MIN_SUB = store_thm
("REAL_MIN_SUB",
! ``!z x y. min (x - z) (y - z) = min x y - z``,
RW_TAC boolSimps.bool_ss [min_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]);
+ val REAL_IMP_MIN_LE2 = store_thm
+ ("REAL_IMP_MIN_LE2",
+ ``!x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> min x1 x2 <= min y1 y2``,
+ RW_TAC boolSimps.bool_ss [REAL_LE_MIN]
+ THEN RW_TAC boolSimps.bool_ss [REAL_MIN_LE]);
+
(* ------------------------------------------------------------------------- *)
(* Define the minimum of two real numbers *)
***************
*** 2659,2670 ****
val REAL_LE_MAX = store_thm
("REAL_LE_MAX",
! ``!x y. x <= max x y /\ y <= max x y``,
! RW_TAC boolSimps.bool_ss [max_def, REAL_LE_REFL]
! THEN PROVE_TAC [REAL_LE_TOTAL]);
val REAL_MAX_LE = store_thm
("REAL_MAX_LE",
! ``!x y z. z <= x /\ z <= y ==> z <= max x y``,
! RW_TAC boolSimps.bool_ss [max_def]);
val REAL_MAX_ALT = store_thm
--- 2684,2706 ----
val REAL_LE_MAX = store_thm
("REAL_LE_MAX",
! ``!z x y. z <= max x y = z <= x \/ z <= y``,
! RW_TAC boolSimps.bool_ss [max_def]
! THEN PROVE_TAC [REAL_LE_TOTAL, REAL_LE_TRANS]);
!
! val REAL_LE_MAX1 = store_thm
! ("REAL_LE_MAX1",
! ``!x y. x <= max x y``,
! RW_TAC boolSimps.bool_ss [REAL_LE_MAX, REAL_LE_REFL]);
!
! val REAL_LE_MAX2 = store_thm
! ("REAL_LE_MAX2",
! ``!x y. y <= max x y``,
! RW_TAC boolSimps.bool_ss [REAL_LE_MAX, REAL_LE_REFL]);
val REAL_MAX_LE = store_thm
("REAL_MAX_LE",
! ``!z x y. max x y <= z = x <= z /\ y <= z``,
! RW_TAC boolSimps.bool_ss [max_def]
! THEN PROVE_TAC [REAL_LE_TRANS, REAL_LE_TOTAL]);
val REAL_MAX_ALT = store_thm
***************
*** 2694,2700 ****
val REAL_LIN_LE_MAX = store_thm
("REAL_LIN_LE_MAX",
! ``!x y z. 0 <= z /\ z <= 1 ==> z * x + (1 - z) * y <= max x y``,
RW_TAC boolSimps.bool_ss []
! THEN MP_TAC (Q.SPECL [`~x`, `~y`, `z`] REAL_MIN_LE_LIN)
THEN RW_TAC boolSimps.bool_ss
[REAL_MIN_MAX, REAL_NEGNEG, REAL_MUL_RNEG, GSYM REAL_NEG_ADD,
--- 2730,2736 ----
val REAL_LIN_LE_MAX = store_thm
("REAL_LIN_LE_MAX",
! ``!z x y. 0 <= z /\ z <= 1 ==> z * x + (1 - z) * y <= max x y``,
RW_TAC boolSimps.bool_ss []
! THEN MP_TAC (Q.SPECL [`z`, `~x`, `~y`] REAL_MIN_LE_LIN)
THEN RW_TAC boolSimps.bool_ss
[REAL_MIN_MAX, REAL_NEGNEG, REAL_MUL_RNEG, GSYM REAL_NEG_ADD,
***************
*** 2703,2714 ****
val REAL_MAX_ADD = store_thm
("REAL_MAX_ADD",
! ``!x y z. max (x + z) (y + z) = max x y + z``,
RW_TAC boolSimps.bool_ss [max_def, REAL_LE_RADD]);
val REAL_MAX_SUB = store_thm
("REAL_MAX_SUB",
! ``!x y z. max (x - z) (y - z) = max x y - z``,
RW_TAC boolSimps.bool_ss [max_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]);
(* ------------------------------------------------------------------------- *)
(* More theorems about sup, and corresponding theorems about an inf operator *)
--- 2739,2756 ----
val REAL_MAX_ADD = store_thm
("REAL_MAX_ADD",
! ``!z x y. max (x + z) (y + z) = max x y + z``,
RW_TAC boolSimps.bool_ss [max_def, REAL_LE_RADD]);
val REAL_MAX_SUB = store_thm
("REAL_MAX_SUB",
! ``!z x y. max (x - z) (y - z) = max x y - z``,
RW_TAC boolSimps.bool_ss [max_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]);
+ val REAL_IMP_MAX_LE2 = store_thm
+ ("REAL_IMP_MAX_LE2",
+ ``!x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> max x1 x2 <= max y1 y2``,
+ RW_TAC boolSimps.bool_ss [REAL_MAX_LE]
+ THEN RW_TAC boolSimps.bool_ss [REAL_LE_MAX]);
+
(* ------------------------------------------------------------------------- *)
(* More theorems about sup, and corresponding theorems about an inf operator *)
***************
*** 2838,2841 ****
--- 2880,2951 ----
THEN (CONJ_TAC THEN1 PROVE_TAC [])
THEN RW_TAC boolSimps.bool_ss [REAL_LT_ADDR]);
+
+ val SUP_EPSILON = store_thm
+ ("SUP_EPSILON",
+ ``!p e.
+ 0 < e /\ (?x. p x) /\ (?z. !x. p x ==> x <= z) ==>
+ ?x. p x /\ sup p <= x + e``,
+ REPEAT GEN_TAC
+ THEN REPEAT DISCH_TAC
+ THEN REWRITE_TAC [GSYM REAL_NOT_LT]
+ THEN MP_TAC (Q.SPEC `p` REAL_SUP_LE)
+ THEN ASM_REWRITE_TAC []
+ THEN DISCH_THEN (fn th => REWRITE_TAC [GSYM th])
+ THEN POP_ASSUM MP_TAC
+ THEN RW_TAC boolSimps.bool_ss [GSYM IMP_DISJ_THM, REAL_NOT_LT]
+ THEN (SUFF_TAC
+ ``?n : num.
+ ?x : real. p x /\ z - &(SUC n) * e <= x /\ x <= z - & n * e /\
+ !y. p y ==> y <= z - &n * e``
+ THEN1 (RW_TAC boolSimps.bool_ss []
+ THEN Q.EXISTS_TAC `x'`
+ THEN RW_TAC boolSimps.bool_ss []
+ THEN Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x''`)
+ THEN RW_TAC boolSimps.bool_ss []
+ THEN MATCH_MP_TAC REAL_LE_TRANS
+ THEN Q.EXISTS_TAC `z - &n * e`
+ THEN RW_TAC boolSimps.bool_ss []
+ THEN (SUFF_TAC ``(z:real) - &n * e = z - &(SUC n) * e + 1 * e``
+ THEN1 RW_TAC boolSimps.bool_ss
+ [REAL_MUL_LID, REAL_LE_RADD])
+ THEN RW_TAC boolSimps.bool_ss
+ [real_sub, GSYM REAL_ADD_ASSOC, REAL_EQ_LADD]
+ THEN ONCE_REWRITE_TAC [GSYM REAL_EQ_NEG]
+ THEN RW_TAC boolSimps.bool_ss
+ [REAL_NEGNEG, REAL_NEG_ADD, GSYM REAL_MUL_LNEG,
+ GSYM REAL_ADD_RDISTRIB, REAL_EQ_RMUL]
+ THEN DISJ2_TAC
+ THEN RW_TAC boolSimps.bool_ss
+ [REAL_EQ_SUB_LADD, GSYM real_sub, REAL_ADD, REAL_INJ,
+ arithmeticTheory.ADD1]))
+ THEN (KNOW_TAC ``?n : num. ?x : real. p x /\ z - &(SUC n) * e <= x``
+ THEN1 (MP_TAC (Q.SPEC `(z - x) / e` REAL_BIGNUM)
+ THEN STRIP_TAC
+ THEN Q.EXISTS_TAC `n`
+ THEN Q.EXISTS_TAC `x`
+ THEN RW_TAC boolSimps.bool_ss [REAL_LE_SUB_RADD]
+ THEN ONCE_REWRITE_TAC [REAL_ADD_SYM]
+ THEN REWRITE_TAC [GSYM REAL_LE_SUB_RADD]
+ THEN (KNOW_TAC ``((z - x) / e) * e = (z:real) - x``
+ THEN1 (MATCH_MP_TAC REAL_DIV_RMUL
+ THEN PROVE_TAC [REAL_LT_LE]))
+ THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th])
+ THEN RW_TAC boolSimps.bool_ss [REAL_LE_RMUL]
+ THEN MATCH_MP_TAC REAL_LE_TRANS
+ THEN Q.EXISTS_TAC `&n`
+ THEN REWRITE_TAC [REAL_LE]
+ THEN PROVE_TAC
+ [arithmeticTheory.LESS_EQ_SUC_REFL, REAL_LT_LE]))
+ THEN DISCH_THEN (MP_TAC o HO_MATCH_MP LEAST_EXISTS_IMP)
+ THEN Q.SPEC_TAC (`$LEAST (\n. ?x. p x /\ z - & (SUC n) * e <= x)`, `m`)
+ THEN RW_TAC boolSimps.bool_ss [GSYM IMP_DISJ_THM]
+ THEN Q.EXISTS_TAC `m`
+ THEN Q.EXISTS_TAC `x'`
+ THEN ASM_REWRITE_TAC []
+ THEN (Cases_on `m`
+ THEN1 RW_TAC boolSimps.bool_ss [REAL_MUL_LZERO, REAL_SUB_RZERO])
+ THEN POP_ASSUM (MP_TAC o Q.SPEC `n`)
+ THEN RW_TAC boolSimps.bool_ss [prim_recTheory.LESS_SUC_REFL, GSYM real_lt]
+ THEN PROVE_TAC [REAL_LT_LE]);
(* ------------------------------------------------------------------------- *)
Index: realSimps.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/real/realSimps.sml,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** realSimps.sml 3 Dec 2002 07:07:33 -0000 1.4
--- realSimps.sml 16 Dec 2002 01:17:06 -0000 1.5
***************
*** 18,37 ****
dprocs = [],
filter = NONE,
! rewrs = [REAL_ADD_LID, REAL_ADD_RID, REAL_MUL_LID, REAL_MUL_RID,
! REAL_MUL_LZERO, REAL_MUL_RZERO, REAL_NEGNEG, REAL_LE_NEG2,
! REAL_LE_REFL, REAL_SUB_REFL, REAL_SUB_RZERO, REAL_LE_01,
! REAL_SUB_ADD2, REAL_MUL_SUB2_CANCEL, REAL_NEG_HALF,
! REAL_LE_SUB_CANCEL2, REAL_LT_HALF1, REAL_HALF_BETWEEN, REAL_LT_01,
! REAL_MUL_SUB1_CANCEL, REAL_NEG_THIRD, REAL_DIV_DENOM_CANCEL2,
! REAL_DIV_DENOM_CANCEL3, REAL_OVER1, REAL_THIRDS_BETWEEN,
! REAL_DIV_ADD, REAL_DIV_INNER_CANCEL2, REAL_DIV_INNER_CANCEL3,
! REAL_INJ, REAL_ADD, REAL_LE, REAL_LT, REAL_MUL, REAL_LT_INV_EQ,
! REAL_POS_POS, REAL_POS_INFLATE, REAL_MIN_REFL, REAL_MIN_LE,
! REAL_DIV_OUTER_CANCEL2, REAL_DIV_OUTER_CANCEL3, REAL_DIV_REFL2,
! REAL_DIV_REFL3, REAL_MAX_REFL, REAL_LE_MAX, REAL_ADD_SUB,
! REAL_SUB_ADD, REAL_ADD_SUB_ALT, REAL_POS_EQ_ZERO,
! REAL_POS_LE_ZERO, REAL_MIN_ADD, REAL_MIN_SUB, REAL_MAX_ADD,
! REAL_MAX_SUB, REAL_LE_RADD, REAL_SUB_RNEG, REAL_NEG_SUB,
! REAL_SUB_SUB2]};
val real_ss = simpLib.++ (arith_ss, real_SS);
--- 18,58 ----
dprocs = [],
filter = NONE,
! rewrs = [(* addition *)
! REAL_ADD_LID, REAL_ADD_RID,
! (* subtraction *)
! REAL_SUB_REFL, REAL_SUB_RZERO,
! (* multiplication *)
! REAL_MUL_LID, REAL_MUL_RID, REAL_MUL_LZERO, REAL_MUL_RZERO,
! (* division *)
! REAL_OVER1, REAL_DIV_ADD,
! (* less than or equal *)
! REAL_LE_REFL, REAL_LE_01, REAL_LE_RADD,
! (* less than *)
! REAL_LT_01, REAL_LT_INV_EQ,
! (* pushing out negations *)
! REAL_NEGNEG, REAL_LE_NEG2, REAL_SUB_RNEG, REAL_NEG_SUB,
! REAL_MUL_RNEG, REAL_MUL_LNEG,
! (* cancellations *)
! REAL_SUB_ADD2, REAL_MUL_SUB1_CANCEL, REAL_MUL_SUB2_CANCEL,
! REAL_LE_SUB_CANCEL2, REAL_ADD_SUB, REAL_SUB_ADD, REAL_ADD_SUB_ALT,
! REAL_SUB_SUB2,
! (* halves *)
! REAL_LT_HALF1, REAL_HALF_BETWEEN, REAL_NEG_HALF,
! REAL_DIV_DENOM_CANCEL2, REAL_DIV_INNER_CANCEL2,
! REAL_DIV_OUTER_CANCEL2, REAL_DIV_REFL2,
! (* thirds *)
! REAL_NEG_THIRD, REAL_DIV_DENOM_CANCEL3, REAL_THIRDS_BETWEEN,
! REAL_DIV_INNER_CANCEL3, REAL_DIV_OUTER_CANCEL3, REAL_DIV_REFL3,
! (* injections to the naturals *)
! REAL_INJ, REAL_ADD, REAL_LE, REAL_LT, REAL_MUL,
! (* pos *)
! REAL_POS_EQ_ZERO, REAL_POS_POS, REAL_POS_INFLATE,
! REAL_POS_LE_ZERO,
! (* min *)
! REAL_MIN_REFL, REAL_MIN_LE1, REAL_MIN_LE2, REAL_MIN_ADD,
! REAL_MIN_SUB,
! (* max *)
! REAL_MAX_REFL, REAL_LE_MAX1, REAL_LE_MAX2, REAL_MAX_ADD,
! REAL_MAX_SUB]};
val real_ss = simpLib.++ (arith_ss, real_SS);
|