Re: [isabelle] Subtyping



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





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