Structure real_of_ratTheory

Source File Identifier index Theory binding index 
signature real_of_ratTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Q_SET : thm
    val real_of_rat_def : thm
  
  (*  Theorems  *)
    val ABS_SQUARE : thm
    val ADD_IN_QSET : thm
    val DIV_IN_QSET : thm
    val INT_BI_INDUCTION : thm
    val INT_FLOOR_ADD : thm
    val INT_FLOOR_MUL : thm
    val INT_FLOOR_REAL_OF_INT : thm
    val INV_IN_QSET : thm
    val IS_INT_ADD : thm
    val IS_INT_ADD2 : thm
    val IS_INT_MUL : thm
    val IS_INT_NUM : thm
    val IS_INT_REAL_OF_INT : thm
    val MUL_IN_QSET : thm
    val NUM_IN_QSET : thm
    val NUM_LT_NEG : thm
    val NUM_NEG : thm
    val NUM_OPP_SIGNS_COMPARE : thm
    val OPP_IN_QSET : thm
    val QSET_COUNTABLE : thm
    val Q_DENSE_IN_REAL : thm
    val Q_DENSE_IN_REAL_LEMMA : thm
    val RATND_ADD : thm
    val RATND_MUL : thm
    val RAT_DIV_LEMMA : thm
    val RAT_DIV_PROD : thm
    val RAT_OF_INT_SUB : thm
    val REAL_IS_INT_LT_LE : thm
    val REAL_LT_SUB_SWAP : thm
    val REAL_OF_RAT_0 : thm
    val REAL_OF_RAT_1 : thm
    val REAL_OF_RAT_ADD : thm
    val REAL_OF_RAT_DIV : thm
    val REAL_OF_RAT_INJ : thm
    val REAL_OF_RAT_LE : thm
    val REAL_OF_RAT_LT : thm
    val REAL_OF_RAT_MAX : thm
    val REAL_OF_RAT_MIN : thm
    val REAL_OF_RAT_MINV : thm
    val REAL_OF_RAT_MUL : thm
    val REAL_OF_RAT_NEG : thm
    val REAL_OF_RAT_NUM_CLAUSES : thm
    val REAL_OF_RAT_OF_INT : thm
    val REAL_OF_RAT_OF_NUM : thm
    val REAL_OF_RAT_SUB : thm
    val REAL_PYTH : thm
    val REAL_Q_DENSE : thm
    val REAL_RAT_DENSE : thm
    val SUB_IN_QSET : thm
    val countable_real_rat_set : thm
    val q_set_def : thm
    val real_rat_set : thm
    val real_rat_set_def : thm
  
  val real_of_rat_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [intreal] Parent theory of "real_of_rat"
   
   [rat] Parent theory of "real_of_rat"
   
   [Q_SET]  Definition
      
      ⊒ β„š = IMAGE real_of_rat π•Œ(:rat)
   
   [real_of_rat_def]  Definition
      
      ⊒ βˆ€q. real_of_rat q = real_of_int (RATN q) / &RATD q
   
   [ABS_SQUARE]  Theorem
      
      ⊒ βˆ€i. ABS i * ABS i = i * i
   
   [ADD_IN_QSET]  Theorem
      
      ⊒ βˆ€x y. x ∈ β„š ∧ y ∈ β„š β‡’ x + y ∈ β„š
   
   [DIV_IN_QSET]  Theorem
      
      ⊒ βˆ€x y. x ∈ β„š ∧ y ∈ β„š ∧ y β‰  0 β‡’ x / y ∈ β„š
   
   [INT_BI_INDUCTION]  Theorem
      
      ⊒ βˆ€P. P 0 ∧ (βˆ€x. P x ⇔ P (x + 1)) ⇔ βˆ€x. P x
   
   [INT_FLOOR_ADD]  Theorem
      
      ⊒ is_int x ∧ is_int y β‡’ ⌊xβŒ‹ + ⌊yβŒ‹ = ⌊x + yβŒ‹
   
   [INT_FLOOR_MUL]  Theorem
      
      ⊒ is_int x ∧ is_int y β‡’ ⌊xβŒ‹ * ⌊yβŒ‹ = ⌊x * yβŒ‹
   
   [INT_FLOOR_REAL_OF_INT]  Theorem
      
      ⊒ ⌊real_of_int iβŒ‹ = i
   
   [INV_IN_QSET]  Theorem
      
      ⊒ βˆ€x. x ∈ β„š ∧ x β‰  0 β‡’ 1 / x ∈ β„š
   
   [IS_INT_ADD]  Theorem
      
      ⊒ is_int x ∧ is_int y β‡’ is_int (x + y)
   
   [IS_INT_ADD2]  Theorem
      
      ⊒ is_int x ∧ is_int (x + y) β‡’ is_int y
   
   [IS_INT_MUL]  Theorem
      
      ⊒ is_int x ∧ is_int y β‡’ is_int (x * y)
   
   [IS_INT_NUM]  Theorem
      
      ⊒ is_int (&n)
   
   [IS_INT_REAL_OF_INT]  Theorem
      
      ⊒ is_int x ⇔ βˆƒi. x = real_of_int i
   
   [MUL_IN_QSET]  Theorem
      
      ⊒ βˆ€x y. x ∈ β„š ∧ y ∈ β„š β‡’ x * y ∈ β„š
   
   [NUM_IN_QSET]  Theorem
      
      ⊒ βˆ€n. &n ∈ β„š ∧ -&n ∈ β„š
   
   [NUM_LT_NEG]  Theorem
      
      ⊒ βˆ€i1 i2. i1 ≀ 0 ∧ i2 ≀ 0 β‡’ (Num i1 < Num i2 ⇔ i2 < i1)
   
   [NUM_NEG]  Theorem
      
      ⊒ Num (-i) = Num i
   
   [NUM_OPP_SIGNS_COMPARE]  Theorem
      
      ⊒ βˆ€i1 i2.
          i1 ≀ 0 ∧ 0 ≀ i2 β‡’
          (Num i1 < Num i2 ⇔ 0 < i1 + i2) ∧
          (Num i2 < Num i1 ⇔ i1 + i2 < 0) ∧ (Num i1 = Num i2 ⇔ i1 + i2 = 0)
   
   [OPP_IN_QSET]  Theorem
      
      ⊒ βˆ€x. x ∈ β„š β‡’ -x ∈ β„š
   
   [QSET_COUNTABLE]  Theorem
      
      ⊒ countable β„š
   
   [Q_DENSE_IN_REAL]  Theorem
      
      ⊒ βˆ€x y. x < y β‡’ βˆƒr. r ∈ β„š ∧ x < r ∧ r < y
   
   [Q_DENSE_IN_REAL_LEMMA]  Theorem
      
      ⊒ βˆ€x y. 0 ≀ x ∧ x < y β‡’ βˆƒr. r ∈ β„š ∧ x < r ∧ r < y
   
   [RATND_ADD]  Theorem
      
      ⊒ rat_of_int (RATN r1 * &RATD r2 + &RATD r1 * RATN r2) /
        &(RATD r1 * RATD r2) =
        r1 + r2
   
   [RATND_MUL]  Theorem
      
      ⊒ rat_of_int (RATN r1 * RATN r2) / &(RATD r1 * RATD r2) = r1 * r2
   
   [RAT_DIV_LEMMA]  Theorem
      
      ⊒ q1 β‰  0 ∧ q2 β‰  0 β‡’ (p1 / q1 = p2 / q2 ⇔ p1 * q2 = p2 * q1)
   
   [RAT_DIV_PROD]  Theorem
      
      ⊒ b β‰  0 ∧ d β‰  0 β‡’ a / b * (c / d) = a * c / (b * d)
   
   [RAT_OF_INT_SUB]  Theorem
      
      ⊒ rat_of_int a βˆ’ rat_of_int b = rat_of_int (a βˆ’ b)
   
   [REAL_IS_INT_LT_LE]  Theorem
      
      ⊒ is_int a ∧ is_int b β‡’ (a < b ⇔ a + 1 ≀ b)
   
   [REAL_LT_SUB_SWAP]  Theorem
      
      ⊒ a < b βˆ’ c ⇔ c < b βˆ’ a
   
   [REAL_OF_RAT_0]  Theorem
      
      ⊒ real_of_rat 0 = 0
   
   [REAL_OF_RAT_1]  Theorem
      
      ⊒ real_of_rat 1 = 1
   
   [REAL_OF_RAT_ADD]  Theorem
      
      ⊒ real_of_rat r1 + real_of_rat r2 = real_of_rat (r1 + r2)
   
   [REAL_OF_RAT_DIV]  Theorem
      
      ⊒ r2 β‰  0 β‡’ real_of_rat r1 / real_of_rat r2 = real_of_rat (r1 / r2)
   
   [REAL_OF_RAT_INJ]  Theorem
      
      ⊒ real_of_rat r1 = real_of_rat r2 ⇔ r1 = r2
   
   [REAL_OF_RAT_LE]  Theorem
      
      ⊒ real_of_rat r1 ≀ real_of_rat r2 ⇔ r1 ≀ r2
   
   [REAL_OF_RAT_LT]  Theorem
      
      ⊒ real_of_rat r1 < real_of_rat r2 ⇔ r1 < r2
   
   [REAL_OF_RAT_MAX]  Theorem
      
      ⊒ max (real_of_rat r) (real_of_rat q) = real_of_rat (rat_max r q)
   
   [REAL_OF_RAT_MIN]  Theorem
      
      ⊒ min (real_of_rat r) (real_of_rat q) = real_of_rat (rat_min r q)
   
   [REAL_OF_RAT_MINV]  Theorem
      
      ⊒ r β‰  0 β‡’ (real_of_rat r)⁻¹ = real_of_rat (rat_minv r)
   
   [REAL_OF_RAT_MUL]  Theorem
      
      ⊒ real_of_rat r1 * real_of_rat r2 = real_of_rat (r1 * r2)
   
   [REAL_OF_RAT_NEG]  Theorem
      
      ⊒ -real_of_rat r = real_of_rat (-r)
   
   [REAL_OF_RAT_NUM_CLAUSES]  Theorem
      
      ⊒ (real_of_rat q = &n ⇔ q = &n) ∧ (real_of_rat q = -&n ⇔ q = -&n) ∧
        (real_of_rat q < &n ⇔ q < &n) ∧ (real_of_rat q < -&n ⇔ q < -&n) ∧
        (real_of_rat q ≀ &n ⇔ q ≀ &n) ∧ (real_of_rat q ≀ -&n ⇔ q ≀ -&n) ∧
        (&n < real_of_rat q ⇔ &n < q) ∧ (-&n < real_of_rat q ⇔ -&n < q) ∧
        (&n ≀ real_of_rat q ⇔ &n ≀ q) ∧ (-&n ≀ real_of_rat q ⇔ -&n ≀ q)
   
   [REAL_OF_RAT_OF_INT]  Theorem
      
      ⊒ real_of_rat (rat_of_int i) = real_of_int i
   
   [REAL_OF_RAT_OF_NUM]  Theorem
      
      ⊒ real_of_rat (&n) = &n
   
   [REAL_OF_RAT_SUB]  Theorem
      
      ⊒ real_of_rat r1 βˆ’ real_of_rat r2 = real_of_rat (r1 βˆ’ r2)
   
   [REAL_PYTH]  Theorem
      
      ⊒ βˆ€r1. βˆƒx. is_int x ∧ r1 < x
   
   [REAL_Q_DENSE]  Theorem
      
      ⊒ βˆ€r1 r2. r1 < r2 β‡’ βˆƒq. r1 < real_of_rat q ∧ real_of_rat q < r2
   
   [REAL_RAT_DENSE]  Theorem
      
      ⊒ βˆ€x y. x < y β‡’ βˆƒr. r ∈ β„š ∧ x < r ∧ r < y
   
   [SUB_IN_QSET]  Theorem
      
      ⊒ βˆ€x y. x ∈ β„š ∧ y ∈ β„š β‡’ x βˆ’ y ∈ β„š
   
   [countable_real_rat_set]  Theorem
      
      ⊒ countable β„š
   
   [q_set_def]  Theorem
      
      ⊒ β„š =
        {x | βˆƒa b. x = &a / &b ∧ 0 < &b} βˆͺ
        {x | βˆƒa b. x = -(&a / &b) ∧ 0 < &b}
   
   [real_rat_set]  Theorem
      
      ⊒ β„š = {r | βˆƒq. r = real_of_rat q}
   
   [real_rat_set_def]  Theorem
      
      ⊒ β„š =
        {x | βˆƒa b. x = &a / &b ∧ 0 < &b} βˆͺ
        {x | βˆƒa b. x = -(&a / &b) ∧ 0 < &b}
   
   
*)
end
Source File Identifier index Theory binding index

HOL 4, Trindemossen-1