Re: [isabelle] Subtyping



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.