*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Subtyping*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Thu, 25 Aug 2011 12:52:20 +1200*Cc*: isabelle-users at cl.cam.ac.uk, Christian Sternagel <c.sternagel at gmail.com>*In-reply-to*: <CAP0k5J5o=28ugkz48jVYaUR9NjGktKXscXAjOKQyVpy0ennAXA@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> <CAP0k5J5o=28ugkz48jVYaUR9NjGktKXscXAjOKQyVpy0ennAXA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.18) Gecko/20110617 Thunderbird/3.1.11

-----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:*John Munroe

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

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