Re: [isabelle] Subtyping

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.

Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla -


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