Re: [isabelle] Subtyping



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.