Re: [isabelle] Parameterized Types?

Title: RE: [isabelle] Parameterized Types?

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

I have defined
    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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.