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"
    and adm: "adm (%x. x : A)"
  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 

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