# Re: [isabelle] Parameterized Types?

```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?

One possibility would be to prove some theorems with type_definition
predicates as assumptions. In the Isabelle sources, HOLCF/Pcpodef.thy
contains several examples of this, such as:

theorem typedef_cpo:
fixes Abs :: "'a::cpo => 'b::po"
assumes type: "type_definition Rep Abs A"
and less: "op << == %x y. Rep x << Rep y"
shows "OFCLASS('b, cpo_class)"

Assumption "type" basically says that type 'b is defined as a predicate
subtype of 'a, and is isomorphic to the set A::'a set. An instantiation of
the type_definition predicate is what gets axiomatized whenever you use the
"typedef" command; take a look at HOL/Typedef.thy to see how it is defined.
Assumption "less" says that the overloaded "<<" relation on type 'b is
defined in terms of "<<" on type 'a, and finally "adm" places some
restrictions on the set A. The conclusion is exactly the proposition you
would get as a subgoal if you tried to prove that 'b is an instance of class
"cpo".

> 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?

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

```

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