*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Parameterized Types?*From*: "Robert Lamar" <rlamar at stetson.edu>*Date*: Mon, 20 Mar 2006 00:55:33 -0500*Thread-index*: AcZL4ucdm1gs7apGSV2iWPnaGdAwiQ==*Thread-topic*: Parameterized Types?

Title:

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? My goal, as I imagine it, is to define a type which is parameterized, essentially, by subsets of "UNIV::('a::ring set)" (or more specifically, by subsets which satisfy my is_ideal predicate). Is this possible? Is there a different (better) way to approach this problem?

Thanks,

Robert Lamar

Stetson University

**Follow-Ups**:**Re: [isabelle] Parameterized Types?***From:*Clemens Ballarin

**Re: [isabelle] Parameterized Types?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] mutual recdefs
- Next by Date: Re: [isabelle] Parameterized Types?
- Previous by Thread: Re: [isabelle] How to unify the premises with my rule?
- Next by Thread: Re: [isabelle] Parameterized Types?
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list