Structure real_algebraTheory

signature real_algebraTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Reals_def : thm
    val real_add_monoid_def : thm
    val real_mul_monoid_def : thm
  
  (*  Theorems  *)
    val GBAG_Reals_prod_BAG_OF_SET : thm
    val GBAG_Reals_sum_BAG_IMAGE_BAG_OF_SET : thm
    val Inv_Reals : thm
    val Reals_sum_inv : thm
    val RingReals : thm
    val Unit_Reals : thm
    val real_add_group : thm
    val real_add_monoid : thm
    val real_add_monoid_simps : thm
    val real_mul_group : thm
    val real_mul_monoid : thm
    val real_mul_monoid_simps : thm
    val ring_divides_Reals : thm
    val ring_prime_Reals : thm
(*
   [real_sigma] Parent theory of "real_algebra"
   
   [ring] Parent theory of "real_algebra"
   
   [Reals_def]  Definition
      
      ⊢ Reals =
        <|carrier := 𝕌(:real); sum := real_add_monoid;
          prod := real_mul_monoid|>
   
   [real_add_monoid_def]  Definition
      
      ⊢ real_add_monoid = <|carrier := 𝕌(:real); id := 0; op := $+ |>
   
   [real_mul_monoid_def]  Definition
      
      ⊢ real_mul_monoid = <|carrier := 𝕌(:real); id := 1; op := $* |>
   
   [GBAG_Reals_prod_BAG_OF_SET]  Theorem
      
      ⊢ ∀f s.
          FINITE s ⇒
          GBAG Reals.prod (BAG_IMAGE f (BAG_OF_SET s)) = product s f
   
   [GBAG_Reals_sum_BAG_IMAGE_BAG_OF_SET]  Theorem
      
      ⊢ ∀f s.
          FINITE s ⇒
          GBAG Reals.sum (BAG_IMAGE f (BAG_OF_SET s)) = SIGMA f s
   
   [Inv_Reals]  Theorem
      
      ⊢ r ≠ 0 ⇒ Inv Reals r = r⁻¹
   
   [Reals_sum_inv]  Theorem
      
      ⊢ Reals.sum.inv = numeric_negate
   
   [RingReals]  Theorem
      
      ⊢ Ring Reals
   
   [Unit_Reals]  Theorem
      
      ⊢ Unit Reals r ⇔ r ≠ 0
   
   [real_add_group]  Theorem
      
      ⊢ AbelianGroup real_add_monoid
   
   [real_add_monoid]  Theorem
      
      ⊢ AbelianMonoid real_add_monoid
   
   [real_add_monoid_simps]  Theorem
      
      ⊢ real_add_monoid.carrier = 𝕌(:real) ∧ real_add_monoid.op = $+ ∧
        real_add_monoid.id = 0
   
   [real_mul_group]  Theorem
      
      ⊢ AbelianGroup (real_mul_monoid excluding 0)
   
   [real_mul_monoid]  Theorem
      
      ⊢ AbelianMonoid real_mul_monoid
   
   [real_mul_monoid_simps]  Theorem
      
      ⊢ real_mul_monoid.carrier = 𝕌(:real) ∧ real_mul_monoid.op = $* ∧
        real_mul_monoid.id = 1
   
   [ring_divides_Reals]  Theorem
      
      ⊢ ring_divides Reals p q ⇔ p = 0 ⇒ q = 0
   
   [ring_prime_Reals]  Theorem
      
      ⊢ ring_prime Reals p
   
   
*)
end

HOL 4, Trindemossen-2