Re: [isabelle] Subtyping
-----BEGIN PGP SIGNED MESSAGE-----
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"
> inst_parent_type :: "(A,B) sum" and
> inst_child_type :: A
> 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
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
> Any clarification on this will be much appreciated!
I hope this has helped.
-----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