Re: [Hol-info] Learning HOL: Commutative rings

[Clemens B. <bal...@in...>]

This might be a good occasion to draw attention to the algebraic library
in Isabelle/HOL.  The formalisation of rings is similar to HOL, but
Isabelle provides context mechanisms, called locales, that aim at making
their use easier.

The following theory file illustrates this ("cring" stands for
commutative ring).  As Michael pointed out, the explicit argument R
makes statements rather unreadable.  Locales provides better syntax (see
lemma bin2_1) and more automation.  There is also a normaliser for rings
that solves the goal automatically (see lemma bin2_2).

The algebra library can be viewed at
http://www4.in.tum.de/~isabelle/library/HOL/HOL-Algebra/index.html.

Clemens
--
theory RingDemo = CRing:

lemma bin2:
    "[| cring R; x \<in> carrier R; y \<in> carrier R |]
    ==> mult R (add R x y) (add R x y) =
       add R
        (add R (add R (mult R x x) (mult R x y)) (mult R x y))
        (mult R y y)"
  apply (simp add: cring.l_distr cring.r_distr abelian_monoid.a_ac
    comm_semigroup.m_comm magma.m_closed abelian_monoid.a_closed
    cring.axioms comm_semigroup.intro)
  done

lemma (in cring) bin2_1:
  "[| x \<in> carrier R; y \<in> carrier R |] ==>
  (x \<oplus> y) \<otimes> (x \<oplus> y) = x \<otimes> x \<oplus> x
\<otimes> y \<oplus> x \<otimes> y \<oplus> y \<otimes> y"
  apply (simp add: l_distr r_distr a_ac m_comm) 
    (* Fewer arguments to simp, because locales know relations
       between rings and their algebraic superstructures. *)
  done

lemma (in cring) bin2_2:
  "[| x \<in> carrier R; y \<in> carrier R |] ==>
  (x \<oplus> y) \<otimes> (x \<oplus> y) = x \<otimes> x \<oplus> x
\<otimes> y \<oplus> x \<otimes> y \<oplus> y \<otimes> y"
  apply algebra
  done

end
-- 
Dr. Clemens Ballarin
Institut fuer Informatik, TU Muenchen
Boltzmannstr. 3, 85748 Garching, Germany
Phone: +49-89-289-17326, Fax: +49-89-289-17307
http://www4.in.tum.de/~ballarin/