Theory Real_Ring_Definition

section ‹The Real Ring definition›

theory Real_Ring_Definition

imports 
  "HOL-Algebra.Module" 
  "HOL-Algebra.RingHom" 
  HOL.Real 
  "HOL-Computational_Algebra.Formal_Power_Series"
begin


text ‹Defining real ring for examples on Noetherian Rings.›
definition                       
  REAL :: "real ring"
  where "REAL = ⦇carrier = UNIV, monoid.mult = (*), one = 1, zero = 0, add = (+)⦈"

lemma REAL_ring:‹ring REAL›
  apply(rule ringI)
     apply(rule abelian_groupI)
  by (auto simp:REAL_def monoidI ab_group_add_class.ab_left_minus distrib_right distrib_left
      intro: exI[of _ "- x" for x])

lemma REAL_cring:‹cring REAL›
  unfolding cring_def apply(safe) 
   apply (simp add: REAL_ring)
  apply(rule comm_monoidI)
  by(auto simp:REAL_def)

lemma REAL_field: ‹field REAL›
  unfolding field_def domain_def field_axioms_def
  apply(safe)
      apply(simp add:REAL_cring)
  unfolding domain_axioms_def 
  by(auto simp:REAL_def Units_def mult.commute nonzero_divide_eq_eq)
    (metis mult.commute nonzero_divide_eq_eq)

end