Move q_set (real_rat_set_def) theorems from real_sigma to real_of_rat…

… with duplicated proofs merged

src/integer/integerScript.sml

@@ -26,7 +26,7 @@ val _ = set_grammar_ancestry ["arithmetic", "pred_set"]
             "BasicProvers", "boolSimps", "pairSimps",
             "numSimps", "numLib", "metisLib"];
 *)
-open jrhUtils quotient liteLib
+open jrhUtils quotient liteLib pred_setTheory
      arithmeticTheory prim_recTheory numTheory
      simpLib numLib boolTheory liteLib metisLib BasicProvers;
 
@@ -1731,6 +1731,13 @@ QED
 val Num = new_definition("Num",
   Term `Num (i:int) = @n. if 0 <= i then i = &n else i = - &n`);
 
+Overload num_of_int[inferior] = “Num” (* from HOL Light *)
+
+(* NOTE: In HOL-Light, num_of_int is unspecified for negative integers:
+   |- !x. num_of_int x = (@n. &n = x) (int.ml, line 2056)
+ *)
+Theorem num_of_int = Num
+
 Theorem NUM_OF_INT[simp,compute]:
   !n. Num(&n) = n
 Proof
@@ -3127,7 +3134,6 @@ val INT_LE_MONO = store_thm(
   ASM_SIMP_TAC bool_ss [INT_LE_LT, INT_MUL_SIGN_CASES, INT_LT_GT] THEN
   PROVE_TAC [INT_ENTIRE, INT_LT_REFL]);
 
-open pred_setTheory
 val INFINITE_INT_UNIV = store_thm(
   "INFINITE_INT_UNIV",
   ``INFINITE univ(:int)``,
@@ -3508,6 +3514,16 @@ val LEAST_INT_DEF = new_definition ("LEAST_INT_DEF",
 
 val _ = set_fixity "LEAST_INT" Binder
 
+(* NOTE: Ported from HOL-Light *)
+Theorem FORALL_INT_CASES :
+    !(P :int -> bool). (!x. P x) <=> (!n. P (&n)) /\ (!n. P (-&n))
+Proof
+    rpt STRIP_TAC
+ >> EQ_TAC >> rw []
+ >> MP_TAC (Q.SPEC ‘x’ INT_NUM_CASES) >> rw [] (* 3 subgoals *)
+ >> rw []
+QED
+
 (*---------------------------------------------------------------------------*)
 (* Euclidean div and mod                                                     *)
 (*---------------------------------------------------------------------------*)

src/rational/intExtensionScript.sml

@@ -9,15 +9,7 @@
 
 open HolKernel boolLib Parse bossLib;
 
-(* interactive mode
-app load ["integerTheory","intLib",
-"ringLib", "pairTheory",
-        "integerRingTheory","integerRingLib",
-        "schneiderUtils"];
-*)
-open
-        arithmeticTheory pairTheory
-        integerTheory intLib
+open arithmeticTheory pairTheory integerTheory intLib
         EVAL_ringTheory EVAL_ringLib integerRingLib
         schneiderUtils;
 

src/rational/ratRingScript.sml

@@ -8,13 +8,7 @@
 
 open HolKernel boolLib Parse bossLib;
 
-(* interactive mode
-app load [
-        "integerTheory", "ratTheory", "ringLib", "schneiderUtils";
-*)
-
-open
-        integerTheory ratTheory EVAL_ringLib schneiderUtils;
+open integerTheory ratTheory EVAL_ringLib schneiderUtils;
 
 val _ = new_theory "ratRing";
 

src/rational/ratScript.sml

@@ -8,14 +8,15 @@
 
 open HolKernel boolLib Parse BasicProvers bossLib;
 
-open
-        arithmeticTheory
+open arithmeticTheory pred_setTheory
         integerTheory intLib
         intExtensionTheory intExtensionLib
         EVAL_ringLib integerRingLib
         fracTheory fracLib ratUtils
         quotient schneiderUtils;
 
+open gcdTheory dividesTheory primeFactorTheory;
+
 val arith_ss = old_arith_ss
 
 val _ = new_theory "rat";
@@ -3127,6 +3128,23 @@ Proof
   simp[RAT_MUL_NUM_CALCULATE] >> strip_tac >> irule nmr_dnm_unique >> simp[]
 QED
 
+(* This is another form of RATND_suff_eq using only natural numbers *)
+Theorem RATND_of_coprimes :
+    !p q. gcd p q = 1 /\ q <> 0 ==> RATN (&p / &q) = &p /\ RATD (&p / &q) = q
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ >> qabbrev_tac ‘n = int_of_num p’
+ >> ‘&p = rat_of_int n’ by rw [rat_of_int_def]
+ >> ‘gcd (Num n) q = 1’ by rw [Abbr ‘n’]
+ >> rw [RATND_suff_eq]
+QED
+
+Theorem RATND_of_coprimes' :
+    !p q. gcd p q = 1 /\ q <> 0 ==> RATN (-&p / &q) = -&p /\ RATD (-&p / &q) = q
+Proof
+    rw [GSYM RAT_DIV_AINV, RATND_of_coprimes]
+QED
+
 Definition div_gcd_def:
   div_gcd a b =
     let d = gcd (Num a) b in

src/real/realScript.sml

@@ -1102,6 +1102,26 @@ val REAL_DIV_MUL2 = store_thm("REAL_DIV_MUL2",
   IMP_SUBST_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[] THEN
   REWRITE_TAC[REAL_MUL_LID]);
 
+Theorem REAL_DIV_PROD:
+  !a b c (d :real). a / b * (c / d) = (a * c) / (b * d)
+Proof
+    rpt STRIP_TAC
+ >> simp[real_div,REAL_INV_MUL'] >> metis_tac[REAL_MUL_ASSOC,REAL_MUL_SYM]
+QED
+
+Theorem REAL_DIV_LT:
+  !a b c (d :real). 0 < b * d ==> (a / b < c / d <=> a * d < c * b)
+Proof
+  rw[real_div]
+  >> ‘b<>0 /\ d<>0’ by (CCONTR_TAC >> gs[])
+  >> ‘a * inv b <c * inv d <=> a * inv b * (b*d) < c * inv d * (b*d)’ by simp[REAL_LT_RMUL]
+  >> ‘a * inv b * (b*d) = a*d * (inv b * b)’ by metis_tac[REAL_MUL_ASSOC,REAL_MUL_SYM]
+  >> ‘_ = a*d’ by simp[REAL_MUL_RID,REAL_MUL_LINV]
+  >> ‘c * inv d * (b*d) = c*b * (inv d * d)’ by metis_tac[REAL_MUL_ASSOC,REAL_MUL_SYM]
+  >> ‘_ = c*b’ by simp[REAL_MUL_RID,REAL_MUL_LINV]
+  >> simp[]
+QED
+
 val REAL_MIDDLE1 = store_thm("REAL_MIDDLE1",
   “!a b. a <= b ==> a <= (a + b) / &2”,
   REPEAT GEN_TAC THEN DISCH_TAC THEN
@@ -4062,7 +4082,7 @@ val NUM_CEILING_LE = store_thm
    THEN numLib.LEAST_ELIM_TAC
    THEN METIS_TAC [NOT_LESS_EQUAL]);
 
-Theorem NUM_CEILING_UPPER_BOUND : (* was: util_probTheory.CLG_UBOUND *)
+Theorem NUM_CEILING_UPPER_BOUND :
     !x. 0 <= x ==> &(clg x) < x + 1
 Proof
     RW_TAC std_ss [NUM_CEILING_def]
@@ -4085,6 +4105,9 @@ Proof
  >> FULL_SIMP_TAC std_ss [REAL_LT_SUB_RADD]
 QED
 
+(* backward compatible name of NUM_CEILING_UPPER_BOUND *)
+Theorem CLG_UBOUND = NUM_CEILING_UPPER_BOUND
+
 (* ----------------------------------------------------------------------
     nonzerop : real -> real
 
@@ -5153,6 +5176,21 @@ Proof
   CONJ_TAC THEN MATCH_MP_TAC RAT_LEMMA4 THEN ASM_REWRITE_TAC[]
 QED
 
+Theorem RAT_LEMMA5_BETTER:
+  y1 <> 0:real /\ y2 <> 0 ==> (x1 / y1 = x2 / y2 <=> x1 * y2 = x2 * y1)
+Proof
+    rw[]
+ >> ‘y1*y2 <> 0’ by simp[] >> simp[real_div]
+ >> ‘x1 * inv y1 = x2 * inv y2 <=>
+     x1 * inv y1 * (y1 * y2) = x2 * inv y2 * (y1 * y2)’ by simp[REAL_EQ_RMUL]
+ >> ‘x1 * inv y1 * (y1 * y2) = x2 * inv y2 * (y1 * y2) <=>
+     x1 * y2 * (inv y1 * y1) = x2 * y1 * (inv y2 * y2)’ by
+    metis_tac[REAL_MUL_ASSOC, REAL_MUL_SYM]
+ >> ‘x1 * y2 * (inv y1 * y1) = x2 * y1 * (inv y2 * y2) <=>
+     x1 * y2 = x2 * y1’ by simp[REAL_MUL_LINV]
+ >> metis_tac[]
+QED
+
 (* The following common used HALF theorems were moved from seqTheory *)
 Theorem HALF_POS :
     0:real < 1/2