| < Free Open Study > |
|
If Г, and , where , then for some C <: D.
Proof: By induction on the derivation of Г, . The intuitions are exactly the same as for the lambda-calculus with subtyping; details vary a little, of course. The most interesting cases are the last two.
Case T-VAR: | t = x | x:D Î Г |
If , then the result is trivial since . On the other hand, if x = xi and D = Bi, then, since , letting C = Ai finishes the case.
Case T-FIELD: | t = t0.fi | Г, |
| D = Ci |
By the induction hypothesis, there is some C0 such that and C0 <: D0. It is easy to check that for some . Therefore, by T-FIELD, .
Case T-INVK: |
|
By the induction hypothesis, there are some C0 and such that:
By Lemma A.13, . Moreover, by the transitivity of <:. Therefore, by T-INVK, .
Case T-NEW: |
|
By the induction hypothesis, for some with . We have by the transitivity of <:. Therefore, by T-NEW, .
Case T-UCAST: | t = (D)t0 | Г, | C <: D |
By the induction hypothesis, there is some E such that and E <: C. We have E <: D by the transitivity of <:, which yields by T-UCAST.
Case T-DCAST: | t = (D)t0 | Г, | D <: C | D ≠ C |
By the induction hypothesis, there is some E such that and E <: C. If E <: D or D <: E, then by T-UCAST or T-DCAST, respectively. On the other hand, if both D ≮: E and E ≮: D, then (with a stupid warning) by T-SCAST.
Case T-SCAST: | t = (D)t0 | Г, | D ≮: C | C ≮: D |
By the induction hypothesis, there is some E such that and E <: C. This means that E ≮ D. (To see this, note that each class in FJ has just one super class. It follows that, if both E <: C and E <: D, then either C <: D or D <: C.) So (with a stupid warning), by T-SCAST.
| < Free Open Study > |
|