Re: [isabelle] Subtyping
(sorry for multiple copies)
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.
On 08/24/2011 05:32 AM, John Munroe wrote:
On 24/08/11 11:03, John Munroe wrote:
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:
f :: "A + B => bool"
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.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and