(def-language field-language
    (base-types kk)
    (constants
      (o_kk kk)
      (i_kk kk)
      (-_kk (kk kk))
      (+_kk (kk kk kk))
      (*_kk (kk kk kk))
      (inv (kk kk))))

(def-theory fields 
    (component-theories h-o-real-arithmetic)
    (language field-language)
    (distinct-constants (i_kk o_kk))
    (axioms
      (associative-law-for-multiplication-for-fields
        "forall(z,y,x:kk,(x *_kk y) *_kk z=x *_kk (y *_kk z))")
      (left-distributive-law-for-fields
        "forall(z,y,x:kk,x *_kk (y +_kk z)=x *_kk y +_kk x *_kk z)")
      (multiplicative-identity-for-fields
        "forall(x:kk,i_kk  *_kk x = x)" rewrite)
      (additive-identity-for-fields
        "forall(x:kk,x +_kk o_kk = x)" rewrite)
      (additive-inverse-for-fields
        "forall(x:kk,x +_kk (-_kk x) = o_kk)" rewrite)
      (commutative-law-for-multiplication-for-fields
        "forall(y,x:kk,x *_kk y=y *_kk x)")
      (associative-law-for-addition-for-fields
        "forall(z,y,x:kk,(x +_kk y) +_kk z=x +_kk (y +_kk z))")
      (commutative-law-for-addition-for-fields
        "forall(y,x:kk,x +_kk y=y +_kk x)")
      (multiplicative-inverse-for-fields
        "forall(x:kk,not(x = o_kk) implies x *_kk inv(x)=i_kk)" )))

(def-theorem field-zero-is-not-field-one 
    "not(o_kk = i_kk)"
    (theory fields)
    (proof
      (
        simplify
        )))

(def-theorem ()
    "total_q(+_kk,[kk,kk,kk])"
    (theory fields)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (assume-theorem commutative-law-for-addition-for-fields)
        )))

(def-theorem ()
    "total_q(*_kk,[kk,kk,kk])"
    (theory fields)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (assume-theorem commutative-law-for-multiplication-for-fields)
        )))

(def-theorem ()
    "total_q(-_kk,[kk,kk])"
    (theory fields)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (assume-theorem additive-inverse-for-fields)
        )))
									    

(def-translation fields-to-rr 
    (source fields)
    (target h-o-real-arithmetic)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs
      (kk rr))
    (constant-pairs
      (o_kk 0)
      (i_kk 1)
      (-_kk -)
      (+_kk +)
      (*_kk *)
      (inv "lambda(x:rr,1/x)"))
  (theory-interpretation-check using-simplification))