Re: [isabelle] Subtyping



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