*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] Subtyping*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 24 Aug 2011 15:27:43 +0100*Cc*: isabelle-users at cl.cam.ac.uk, "Tim \(McKenzie\) Makarios" <tjm1983 at gmail.com>*In-reply-to*: <4E54BA54.7090600@gmail.com>*References*: <CAP0k5J7vOgpcrUqVy5s4gAsQf1zAtr4gH-wiXjj=Ge7bBHYVfQ@mail.gmail.com> <4E546478.7030708@gmail.com> <CAP0k5J6RHg1OwtJNOrjz-fh4dL7HcY3x6AsDJnnv_qBQusUuFA@mail.gmail.com> <4E54BA54.7090600@gmail.com>

Thanks for the reply. I've just tested datatype 'a + 'b = Inl 'a | Inr 'b but it complains about *** Outer syntax error: name declaration expected, *** but keyword + was found It works if I instead have datatype ('a, 'b) sum = Inl 'a | Inr 'b Should this produce the same effect? Using your is_Inl function, how should I then test that if a constant is of the type A, then is_Inl returns True? is_Inl takes an input of type 'a + 'b (or ('a,'b) sum, in my case), so how do I supply a constant of type A? Thanks John On Wed, Aug 24, 2011 at 9:46 AM, Christian Sternagel <c.sternagel at gmail.com> wrote: > Hi there, > > I would refrain from going into the "implementation" level of the sum type > (Abs_sum, Inl_rep) and just use pattern matching. > > The type A + B represents a type that incorporates values of type A /and/ > values of type B. Since we are in a strongly typed setting we need a new > type for this, which is essentially an algebraic datatype definable by (also > the internal construction is different, I think) > > datatype 'a + 'b = Inl 'a | Inr 'b > > here the Inl and Inr are the left and right injections. To extract values > you can just use pattern matching. > > fun is_Inl where > is_Inl (Inl _) = True" > | is_Inl (Inr _) = False" > > Hope this helps. > > cheers > > chris > > On 08/24/2011 05:32 AM, John Munroe wrote: >>> >>> On 24/08/11 11:03, John Munroe wrote: >>>> >>>> Hi, >>>> >>>> I'm trying to define a function 'f' such that when the input is of >>>> type 'A' it gives true, but when it's of type 'B' it gives false: >>>> Would I need to make A and B subtypes of some parent type, say, 'P', >>>> and that 'f' is of type "P => bool"? I can't seem to find much >>>> documentation on subtyping. >>> >>> It sounds like you might want to use a sum type, so that the type "'p" >>> is "'a + 'b". There was a discussion about this quite recently on this >>> very list, starting here: http://tinyurl.com/3jzx3ny >>> >>> Then you could have something like "f p = \<exists> a. p = Inl a" (but I >>> haven't tested this). >> >> Thanks for that. I'm not certain if I properly understand "f p = >> \<exists> a. p = Inl a". So, for my example, is the type of f "A + B >> => bool"? This is what I have: >> >> typedecl A >> typedecl B >> >> axiomatization >> f :: "A + B => bool" >> where >> ax1 : "f p = (EX a. p = Inl a)" >> >> consts a :: "A + 'b" >> >> lemma "f a = True" >> apply (simp add: ax1) >> ?? >> >> I can't seem to find out what Inl actually does. It's defined in >> Sum_Type to be "Inl = Abs_sum \<circ> Inl_Rep", but I can't seem to >> find where Abs_sum is defined. >> >> Thanks >> >> John >> >>> >>> Tim >>> <>< >>> -----BEGIN PGP SIGNATURE----- >>> Version: GnuPG v1.4.10 (GNU/Linux) >>> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ >>> >>> iEYEARECAAYFAk5UZHMACgkQ/cBxZIxl6rmwnACfdWxXr+HPTl/8EOuAg0Y6j1Ai >>> 378An1HvQucFMwMdkCUv4a+PtWuAXzbO >>> =Z7Ie >>> -----END PGP SIGNATURE----- >>> >> >> > >

**Follow-Ups**:**Re: [isabelle] Subtyping***From:*John Munroe

**References**:**[isabelle] Subtyping***From:*John Munroe

**Re: [isabelle] Subtyping***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Subtyping***From:*John Munroe

- Previous by Date: Re: [isabelle] Subtyping
- Next by Date: Re: [isabelle] Subtyping
- Previous by Thread: Re: [isabelle] Subtyping
- Next by Thread: Re: [isabelle] Subtyping
- Cl-isabelle-users August 2011 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