Received: by 10.114.210.2 with SMTP id i2mr2979416wag.21.1204930521249;
        Fri, 07 Mar 2008 14:55:21 -0800 (PST)
Return-Path: <andrew.ga...@gmail.com>
Received: from wf-out-1314.google.com (wf-out-1314.google.com [209.85.200.175])
        by mx.google.com with ESMTP id v36si15411359wah.3.2008.03.07.14.55.20;
        Fri, 07 Mar 2008 14:55:21 -0800 (PST)
Received-SPF: pass (google.com: domain of andrew.ga...@gmail.com designates 209.85.200.175 as permitted sender) client-ip=209.85.200.175;
Authentication-Results: mx.google.com; spf=pass (google.com: domain of andrew.ga...@gmail.com designates 209.85.200.175 as permitted sender) smtp.mail=andrew.ga...@gmail.com; dkim=pass (test mode) header...@gmail.com
Received: by wf-out-1314.google.com with SMTP id 23so1159848wfg.29
        for <abella-theorem-prover@googlegroups.com>; Fri, 07 Mar 2008 14:55:20 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:received:received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references;
        bh=CJ0/V5XTAzsRwURfUWndyAffdwpX8yJXUlhAlI0GeXg=;
        b=Ftei+ugxq7uiCWIINzjWawUyttVNQybFlLV27KSuS98X3PaC7G0UTv3DKmbQBk1onGeqPhC5IP3vaGd32hUqqvPhmwpUTxxYWPcnKyXx30ES6nao0UCLtGy8YAHEVPgE8iNdesBINheDX/vZY/xLqmTysTC6q7wILP0cnWISjEg=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references;
        b=wdNPrjSQq7/1QGZwzq0iV5pKTML1YNrsWGz1bl0YGKqL6ojAW50C74M9p3pxznzg+WQ1XhgSJtyU2t4rASYFMFTmbKee1LEl7S2nPSOpIJyoxMjnZ0iIw+sJmzKGHCY1RHzDhGnE0EhcaTyJODCcrcsVU8lTH24UxTMWGXrumXo=
Received: by 10.142.86.7 with SMTP id j7mr1171722wfb.78.1204930520181;
        Fri, 07 Mar 2008 14:55:20 -0800 (PST)
Received: by 10.142.132.1 with HTTP; Fri, 7 Mar 2008 14:55:20 -0800 (PST)
Message-ID: <ff170bdf0803071455g35459d2fk3ea85622dcc84f1b@mail.gmail.com>
Date: Fri, 7 Mar 2008 16:55:20 -0600
From: "Andrew Gacek" <andrew.ga...@gmail.com>
To: abella-theorem-prover@googlegroups.com
Subject: Re: [Abella] lifting specifications?
In-Reply-To: <18385.48846.402977.154...@locatelli.inf.ed.ac.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
References: <18385.48846.402977.154...@locatelli.inf.ed.ac.uk>

Hi Randy,

>  The .mod file:
>
>   trm (app M N) :- trm M, trm N.
>   trm (abs R) :- pi x\ trm x => trm (R x).
>
>  And we have
>
>   Define ctxs nil nil nil.
>   Define nabla x, ctxs (trm x :: L) (pr1 x x :: K)
>                                     (cd1 x x :: notabs x :: J)
>       := ctxs L K J.
>
>  Can I lift "trm" to contexts, like
>
>   Theorem trm_app: forall L K J M N,
>    ctxs L K J -> {L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.

I don't have Abella handy, but I think the following should work.

Theorem trm_app: forall L M N,
  {L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.
intros. search.


>  I don't see how to prove this.  In your example poplmark-1a.thm I see
>  you define something similar:
>
>   Define cty L top.
>   Define cty L X := exists U, member (bound X U) L.
>   Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2.
>   Define cty L (all T1 T2) :=
>     cty L T1 /\ nabla x, cty (bound x T1 :: L) (T2 x).
>
>  What is going on here?

Here I'm defining a predicate which recognizes closed types. I could
have defined this in the specification logic with

cty top.
cty (arrow T1 T2) :- cty T1, cty T2.
cty (all T1 T2) :- cty T1, pi x\ cty x => cty (T2 x).

But the definition I used in poplmark-1a is a little more convenient
since it generates contexts like (bound x T :: ...) rather than (cty x
:: ...). And this former style of contexts matches that of the sub
judgment. In summary, I could define cty in the specification logic,
but reasoning would take a little more work.

-Andrew