*To*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Subtyping*From*: John Munroe <munddr at gmail.com>*Date*: Thu, 25 Aug 2011 02:07:54 +0100*Cc*: isabelle-users at cl.cam.ac.uk, Christian Sternagel <c.sternagel at gmail.com>*In-reply-to*: <4E559CC4.1080703@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> <CAP0k5J5o=28ugkz48jVYaUR9NjGktKXscXAjOKQyVpy0ennAXA@mail.gmail.com> <4E559CC4.1080703@gmail.com>

Thanks so much. It surely has been helpful! One thing though: I can't define the datatype "'a + 'b" with datatype 'a + 'b = Inl 'a | Inr 'b It doesn't seem to like the '+' operator. Is using "datatype ('a,'b) sum" the only way? (I see that it doesn't have to be 'sum' but any arbitrary name seems to do.) Also, is the approach of using sum type more appropriate than overloading for my application? Would overloading allow the same effect to be produced, i.e. defining a function that gives True only if the input is of a particular type? Thanks again. John On Thu, Aug 25, 2011 at 1:52 AM, Tim (McKenzie) Makarios <tjm1983 at gmail.com> wrote: > -----BEGIN PGP SIGNED MESSAGE----- > Hash: SHA1 > > On 25/08/11 06:08, John Munroe wrote: >> 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? > > The lemma asserts that inst_parent_type is of the form "Inl a" for some > a. It is provable "by (simp add: ax1 [symmetric])". > >> 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. > > You don't need to assume anything. Whenever you've got an element a of > type 'a, you've got a corresponding element "Inl a" of type "'a + 'b"; > you don't need to assume this. > > Given any element c of type "'a + 'b", there is either > - - exactly one element a of type 'a such that "c = Inl a" or > - - exactly one element b of type 'b such that "c = Inr b" > but not both. is_Inl tells you whether or not it's the first of these > two possibilities. > >> Any clarification on this will be much appreciated! >> >> Thanks >> >> John > > I hope this has helped. > > Tim > <>< > -----BEGIN PGP SIGNATURE----- > Version: GnuPG v1.4.10 (GNU/Linux) > Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ > > iEYEARECAAYFAk5VnL4ACgkQ/cBxZIxl6rmpnACfZY9urcaOfhUhfzBxJJ9ip+B3 > Kv0AoNc9v9xGgMurYt6dez55S2rFCJIQ > =EjHt > -----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

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

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

- 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