*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Parameterized Types?*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Mon, 20 Mar 2006 11:09:14 -0800*In-reply-to*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E18@beta.ad.stetson.edu>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E18@beta.ad.stetson.edu>*User-agent*: KMail/1.8

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

**References**:**[isabelle] Parameterized Types?***From:*Robert Lamar

- Previous by Date: Re: [isabelle] Parameterized Types?
- Next by Date: Re: [isabelle] thm_deps
- Previous by Thread: Re: [isabelle] Parameterized Types?
- 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