[Hol-checkins] CVS: hol98/src/real realScript.sml,1.16,1.17 realSimps.sml,1.2,1.3

[Joe H. <je...@us...>]

Update of /cvsroot/hol/hol98/src/real
In directory sc8-pr-cvs1:/tmp/cvs-serv603/real

Modified Files:
	realScript.sml realSimps.sml 
Log Message:
As predicted, I need a few more simplifying rewrites.


Index: realScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/real/realScript.sml,v
retrieving revision 1.16
retrieving revision 1.17
diff -b -C2 -d -r1.16 -r1.17
*** realScript.sml	2 Dec 2002 05:41:07 -0000	1.16
--- realScript.sml	3 Dec 2002 00:28:39 -0000	1.17
***************
*** 2647,2652 ****
     THEN numLib.ARITH_TAC);
  
! val REAL_DIV_CANCEL2 = store_thm
!   ("REAL_DIV_CANCEL2",
     ``!x y z : real. ~(x = 0) ==> ((y / x) / (z / x) = y / z)``,
     RW_TAC boolSimps.bool_ss [real_div]
--- 2647,2652 ----
     THEN numLib.ARITH_TAC);
  
! val REAL_DIV_DENOM_CANCEL = store_thm
!   ("REAL_DIV_DENOM_CANCEL",
     ``!x y z : real. ~(x = 0) ==> ((y / x) / (z / x) = y / z)``,
     RW_TAC boolSimps.bool_ss [real_div]
***************
*** 2661,2676 ****
     THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]);
  
! val REAL_DIV2_CANCEL2 = save_thm
!   ("REAL_DIV2_CANCEL2",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_CANCEL2));
  
! val REAL_DIV3_CANCEL2 = save_thm
!   ("REAL_DIV3_CANCEL2",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_CANCEL2));
  
! val REAL_DIV_MUL_CANCEL = store_thm
!   ("REAL_DIV_MUL_CANCEL",
     ``!x y z : real. ~(x = 0) ==> ((y / x) * (x / z) = y / z)``,
     RW_TAC boolSimps.bool_ss [real_div]
--- 2661,2676 ----
     THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]);
  
! val REAL_DIV_DENOM_CANCEL2 = save_thm
!   ("REAL_DIV_DENOM_CANCEL2",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_DENOM_CANCEL));
  
! val REAL_DIV_DENOM_CANCEL3 = save_thm
!   ("REAL_DIV_DENOM_CANCEL3",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_DENOM_CANCEL));
  
! val REAL_DIV_INNER_CANCEL = store_thm
!   ("REAL_DIV_INNER_CANCEL",
     ``!x y z : real. ~(x = 0) ==> ((y / x) * (x / z) = y / z)``,
     RW_TAC boolSimps.bool_ss [real_div]
***************
*** 2680,2692 ****
     THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]);
  
! val REAL_DIV2_MUL_CANCEL = save_thm
!   ("REAL_DIV2_MUL_CANCEL",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_MUL_CANCEL));
  
! val REAL_DIV3_MUL_CANCEL = save_thm
!   ("REAL_DIV3_MUL_CANCEL",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_MUL_CANCEL));
  
  val REAL_HALF_BETWEEN = store_thm
--- 2680,2721 ----
     THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]);
  
! val REAL_DIV_INNER_CANCEL2 = save_thm
!   ("REAL_DIV_INNER_CANCEL2",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_INNER_CANCEL));
  
! val REAL_DIV_INNER_CANCEL3 = save_thm
!   ("REAL_DIV_INNER_CANCEL3",
     SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_INNER_CANCEL));
! 
! val REAL_DIV_OUTER_CANCEL = store_thm
!   ("REAL_DIV_OUTER_CANCEL",
!    ``!x y z : real. ~(x = 0) ==> ((x / y) * (z / x) = z / y)``,
!    RW_TAC boolSimps.bool_ss [real_div]
!    THEN (KNOW_TAC ``!a b c d : real. a * b * (c * d) = (a * d) * (c * b)``
!          THEN1 metisLib.METIS_TAC [REAL_MUL_SYM, REAL_MUL_ASSOC])
!    THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
!    THEN RW_TAC boolSimps.bool_ss [REAL_MUL_RINV, REAL_MUL_LID]);
! 
! val REAL_DIV_OUTER_CANCEL2 = save_thm
!   ("REAL_DIV_OUTER_CANCEL2",
!    SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_OUTER_CANCEL));
! 
! val REAL_DIV_OUTER_CANCEL3 = save_thm
!   ("REAL_DIV_OUTER_CANCEL3",
!    SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_OUTER_CANCEL));
! 
! val REAL_DIV_REFL2 = save_thm
!   ("REAL_DIV_REFL2",
!    SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ]
!    (Q.SPEC `2` REAL_DIV_REFL));
! 
! val REAL_DIV_REFL3 = save_thm
!   ("REAL_DIV_REFL3",
!    SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ]
!    (Q.SPEC `3` REAL_DIV_REFL));
  
  val REAL_HALF_BETWEEN = store_thm

Index: realSimps.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/real/realSimps.sml,v
retrieving revision 1.2
retrieving revision 1.3
diff -b -C2 -d -r1.2 -r1.3
*** realSimps.sml	2 Dec 2002 05:41:07 -0000	1.2
--- realSimps.sml	3 Dec 2002 00:28:40 -0000	1.3
***************
*** 23,31 ****
              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_DIV2_CANCEL2,
!             REAL_DIV3_CANCEL2, REAL_OVER1, REAL_THIRDS_BETWEEN,
!             REAL_DIV_ADD, REAL_DIV2_MUL_CANCEL, REAL_DIV3_MUL_CANCEL, 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]};
  
  val real_ss = simpLib.++ (arith_ss, real_SS);
--- 23,33 ----
              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]};
  
  val real_ss = simpLib.++ (arith_ss, real_SS);