Executable Specification

[View stlc.sig] [View stlc.mod]
sig stlc.

kind	tm, ty		type.

type 	arr 		ty -> ty -> ty.
type    b               ty.

type	app		tm -> tm -> tm.
type 	abs		ty -> (tm -> tm) -> tm.

type    ty              ty -> o.
type    tm              tm -> o.

module stlc.

ty b.
ty (arr T1 T2) :- ty T1, ty T2.

tm (app M1 M2) :- tm M1, tm M2.
tm (abs T R) :- ty T, pi x\ tm x => tm (R x).


[View stlc.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "stlc".

%% The strengthening lemma in Section 5.1 and its proof
Theorem ty_indep_tm_simp : forall T, nabla x,
  {tm x |- ty (T x)} -> exists T', T = y\T' /\ {ty T'}.
induction on 1. intros. case H1. % Case: T x = b search. % Case: T x = arr (T1 x) (T2 x) apply IH to H2. apply IH to H3. search. % Case: context case H3. case H2. case H4.
Define name : tm -> prop by nabla x, name x. Define ctx : olist -> prop by ctx nil; nabla x, ctx (tm x :: L) := ctx L. Theorem ctx_mem : forall L E, ctx L -> member E L -> exists X, E = tm X /\ name X. %% The strengthening lemma in B.3 which is used in Section 5.3 Theorem ty_indep_tm : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} -> exists T', T = y\T' /\ {L |- ty T'}.