Up Next
B.1 Basic properties

In the following lemmas, we let D range over any right hand side of a judgment, except for the chemical judgment.
Lemma 2  [Useless variable]   For any judgment of the form A |- D, and any name x that is not free in D we have:
A |- D Û A + A' |- D
where A' is either x : s or x: s, x : " X. B.

Lemma 3  [Renaming of type variables]   Let h be a substitution on type variables. We have:
A |- D Þ h(A) |- h(D)
We say that a type scheme " X . t is more general than " X'. t' if t' is of the form h (t) for some substitution h replacing type and row variables by types and rows, respectively. This notion is also lifted to set of assumptions as follows: A' is more general than A if A and A' have the same domain and for each u in their domain, A'(u) is more general than A(u).
Lemma 4  [Generalization]   If A |- D and A' is more general than A, then A' |- D.

Lemma 5  [Substitution of a name in a term]   If A + x : t |- D and A |- u : t then A |- D {u/x}. Similarly, if A + x : [mi : ti i Î I], x : (l : tll Î S) |- D and A |- y : t, (A |- y.mi : ti) i Î I, and (A |- y.l : tl)l Î S then A |- D{x ¬ y}.

Lemma 6  [Substitution of a class name in a term]   Let A + c : " X . z(r)BW,V |- D and A + B |- C :: z(r)BW,V and X Í Gen (r, B, A). Then A |- D {c ¬ C}.


Up Next