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

OK. I suspect I'm doing something wrong here, but here's what I have: typedecl A typedecl B datatype ('a, 'b) sum = Inl 'a | Inr 'b fun is_Inl where is1: "is_Inl (Inl _) = True" | is2: "is_Inl (Inr _) = False" axiomatization inst_parent_type :: "(A,B) sum" and inst_child_type :: A where ax1: "Inl inst_child_type = inst_parent_type" lemma "is_Inl inst_parent_type" apply (simp add: is1 ax1) I'm guessing that the lemma tests whether the type of 'inst_parent_type', i.e. (A,B) sum, has a left injection, i.e. whether there exists an instance of the "left" child type. Axiom ax1 asserts that 'inst_child_type' is the left injection. So, should the lemma be provable? This approach is supposed to imitate subtyping, but it seems to require that an instance of the "parent type" to be constructed in order to do any reasoning about subtypes. If I'm right, then it's somewhat more restrictive because such an instance must be first assumed to exist. Any clarification on this will be much appreciated! Thanks John On Wed, Aug 24, 2011 at 3:27 PM, John Munroe <munddr at gmail.com> wrote: > 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:*Tim (McKenzie) Makarios

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

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

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

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

- Previous by Date: Re: [isabelle] Subtyping
- Next by Date: [isabelle] Overloading in locales
- 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