On Mon 3/20/2006 2:09 PM, Brian Huffman wrote:
 On Sunday 19 March 2006 21:55, Robert Lamar wrote:
 > I am attempting to develop a theory of rings which features quotients. So
 > far, I have defined rings through axiomatic classes and ideals through a
 > predicate constant. There are several approaches to defining the quotient
 > ring which present themselves, but the next step would be to prove that the
 > quotient is an instance of the ring class. Is there a straightforward way
 > to do this without specifying a particular ideal?

 In your case, you could prove the following theorem:
 theorem typedef_ring:
 fixes Abs :: "'a::ring => 'b::{zero,plus,times}"
 assumes type: "type_definition Rep Abs A"
 and zero: "0 == Abs 0"
 and plus: "op + == %x y. Abs (Rep x + Rep y)"
 and times: "op * == %x y. Abs (Rep x * Rep y)"
 and ideal: "is_ideal A"
 shows "OFCLASS('b, ring_class)"

 You wouldn't get a parameterized type, but you would be able to define new
 types one at a time using typedef, and then prove that each new type is in
 the ring class using theorem typedef_ring.

  Brian

Thank you very much for this suggestion. The approach you suggest makes sense to me, and I have set out to prove this result. Although it is tedious at times, I am making progress. There are a couple of snags I have hit, though, and would appreciate input.
My only question for the moment arises from my attempt to prove a lemma, that the sum of two elements of a quotient is in the quotient. I am unable to get past a certain step, which I isolate in the following lemma:
lemma "EX s. S = coset I s ==> EX s. S = {i + s  i. i \<in> I}"
proof 
assume "EX s. S = coset I s"
from this coset_def [of I s] show "EX s. S = {i + s  i. i \<in> I}"
by simp
qed
I have defined
constdefs
coset :: "[('a::ring) set, 'a] => 'a set"
"coset I a == {i + a  i. i \<in> I}"
and would like to think that it is a straightforward matter of substitution. However, I know that section 5.11 of the tutorial makes it clear that reasoning about existential operators can be very tricky. Am I missing something crucial?
Robert Lamar