%%% A most naive version of translation from natural deductions
%%% into a proof in the Hilbert-style system and vice versa.
%%% Expresses the equivalence of the two systems.
%%% Author: Frank Pfenning

% abs implements bracket abstraction which amounts to
% the computational content of the deduction theorem.

abs : (|- A -> |- B) -> |- A => B -> type.
% mode +{A} +{B} +{D} -{F} abs D F.

aID	  : abs ([x] x) (MP (MP S K) K).
aONE	  : abs ([x] ONE) (MP K ONE).
aPAIR	  : abs ([x] PAIR) (MP K PAIR).
aLEFT	  : abs ([x] LEFT) (MP K LEFT).
aRIGHT	  : abs ([x] RIGHT) (MP K RIGHT).
aK	  : abs ([x] K) (MP K K).
aS	  : abs ([x] S) (MP K S).
aMP	  : abs ([x] MP (P x) (Q x)) (MP (MP S P') Q')
	      <- abs P P' <- abs Q Q'.

% comb does the translation from natural deduction to Hilbert deductions,
% appealing to the deduction theorem in case of implies-introduction
% which requires hypothetical reasoning.

comb : ! A -> |- A -> type.
% mode comb +D -F.

ctrue     : comb trueI ONE.
candI     : comb (andI P Q) (MP (MP PAIR P') Q') <- comb P P' <- comb Q Q'.
candEL    : comb (andEL P)  (MP LEFT P')	 <- comb P P'.
candER    : comb (andER P)  (MP RIGHT P')	 <- comb P P'.
cimpliesI : comb (impliesI PP) Q
            <- ({x}{y} comb x y
	                -> ({B:o} abs ([z:|- B] y) (MP K y))
		        -> comb (PP x) (PP' y))
	    <- abs PP' Q.
cimpliesE : comb (impliesE P Q) (MP P' Q')
	    <- comb P P'
	    <- comb Q Q'.

% Now the translation from Hilbert deduction into natural deductions.
% This simply gives the definition of the (proof) combinators as lambda-terms.

combdefn : |- A -> ! A -> type.
%mode  combdefn +D -F.

cdK     : combdefn K (impliesI [p] impliesI [q] p).
cdS	: combdefn S (impliesI [p] impliesI [q] impliesI [r]
		         (impliesE (impliesE p r) (impliesE q r))).
cdONE   : combdefn ONE trueI.
cdPAIR  : combdefn PAIR (impliesI [p] impliesI [q] andI p q).
cdLEFT  : combdefn LEFT (impliesI [p] andEL p).
cdRIGHT : combdefn RIGHT (impliesI [p] andER p).
cdMP    : combdefn (MP P Q) (impliesE P' Q')
	     <- combdefn P P'
	     <- combdefn Q Q'.


%%% Decidability proof for theorem  HD -> ND
%terminates D (combdefn D _).