%sig FORMULA- = {
  o : type.
  i : type.
  false  : o. 
  imp    : o -> o -> o.   %infix right 10 imp.
  forall : (i -> o) -> o.	    
}.


%sig FORMULA = {
  %struct F : FORMULA- = {}.		 
  o = F.o.
  i = F.i. 
  not    : F.o -> F.o.        %prefix 12 not.
  false  = F.false.
  imp   = [p] [q] p F.imp q.    %infix right 10 imp.
  forall = F.forall.
}.



%sig ND = {
  % Natural deductions
  %struct F : FORMULA = {}.

  nd : F.o -> type.
  %name nd D u.

  impi    : (nd A -> nd B) -> nd (A F.imp B).
  impe    : nd (A F.imp B) -> nd A -> nd B.

  noti    : ({p:F.o} nd A -> nd p) -> nd (F.not A).
  note    : nd (F.not A) -> {C:F.o} nd A -> nd C.

  foralli : ({a:F.i} nd (A a)) -> nd (F.forall A).
  foralle : nd (F.forall A) -> {T:F.i} nd (A T).

  % block lnd : some {A:F.o} block {u:nd A}.
  % block lo : block {p:F.o}.
  % block li : block {a:F.i}.

  % worlds (lnd | lo | li) (nd A).

  % Example

  _ : nd (A F.imp (B F.imp A))
    = (impi [u:nd A] impi [v:nd B] u).   

  %abbrev     % why isn't this strict. BUG Fri Jan 23 12:49:57 2009 --cs
   dn : nd (A F.imp F.not F.not A)
     = (impi [u:nd A] noti [p:F.o] [w:nd (F.not A)] note w p u).


}.


%sig HIL = {
  % Hilbert deductions

  %struct F : FORMULA = {}.
  hil : F.o -> type.  % Hilbert deductions
  %name hil H u.
 
  k : hil (A F.imp (B F.imp A)).
  s : hil ((A F.imp (B F.imp C)) F.imp ((A F.imp B) F.imp (A F.imp C))).

  n1 : hil ((A F.imp (F.not B)) F.imp ((A F.imp B) F.imp (F.not A))).
  n2 : hil ((F.not A) F.imp (A F.imp B)).

  f1 : {T:F.i} hil ((F.forall [x:F.i] A x) F.imp (A T)).
  f2 : hil ((F.forall [x:F.i] (B F.imp A x)) F.imp (B F.imp F.forall [x:F.i] A x)).

  mp : hil (A F.imp B) -> hil A -> hil B.
  ug : ({a:F.i} hil (A a)) -> hil (F.forall [x:F.i] A x).

  % worlds (li) (hil A).

}.

% Local reductions

%sig REDEXP = {
  %struct F : FORMULA = {}.
  %struct ND : ND = {%struct F := F.}.
  ==>R : ND.nd A -> ND.nd A -> type.  %infix none 14 ==>R.
  %name ==>R R.

  redl_imp    : (ND.impe (ND.impi [u:ND.nd A] D u) E) ==>R (D E).
  redl_not    : (ND.note (ND.noti [p:F.o] [u:ND.nd A] D p u) C E) ==>R (D C E).
  redl_forall : (ND.foralle (ND.foralli [a:F.i] D a) T) ==>R (D T).

  % Local expansions

  ==>E : ND.nd A -> ND.nd A -> type.  %infix none 14 ==>E.
  %name ==>E E.

  expl_imp    : {D:ND.nd (A F.imp B)}  D ==>E (ND.impi [u:ND.nd A] ND.impe D u).
  expl_not    : {D:ND.nd (F.not A)}    D ==>E (ND.noti [p:F.o] [u:ND.nd A] ND.note D p u).
  expl_forall : {D:ND.nd (F.forall A)} D ==>E (ND.foralli [a:F.i] ND.foralle D a).

}.

% Translating Hilbert derivations to natural deductions

hilnd : hil A -> nd A -> type.

hnd_k : hilnd (k) (impi [u:nd A] impi [v:nd B] u).
hnd_s : hilnd (s) (impi [u:nd (A imp B imp C)]
		     impi [v:nd (A imp B)]
		     impi [w:nd A] impe (impe u w) (impe v w)).

hnd_n1 : hilnd (n1) (impi [u:nd (A imp (not B))]
			   impi [v:nd (A imp B)]
			   noti [p:o] [w:nd A]
			   note (impe u w) p (impe v w)).

hnd_n2 : hilnd (n2) (impi [u:nd (not A)]
			   impi [v:nd A] note u B v).

hnd_f1 :
  hilnd (f1 T) (impi [u:nd (forall [x:i] A x)] foralle u T).

hnd_f2 :
  hilnd (f2) (impi [u:nd (forall [x:i] (B imp A x))]
		     impi [v:nd B]
		     foralli [a:i] impe (foralle u a) v).

hnd_mp : hilnd (mp H1 H2) (impe D1 D2)
	  <- hilnd H1 D1
	  <- hilnd H2 D2.

hnd_ug : hilnd (ug H1) (foralli D1)
	    <- ({a:i} hilnd (H1 a) (D1 a)).

%mode hilnd +H -D.
%worlds (li) (hilnd H D).
%terminates H (hilnd H _).
%covers hilnd +H -D.
%total H (hilnd H _).

%solve id' : 
hilnd (mp (mp s k) k) (D:nd (A imp A)).

_ : nd (A imp A)
  = (impe
	(impe
	    (impi
		([u:nd (A imp (B imp A) imp A)]
		    impi
		       ([v:nd (A imp B imp A)]
			   impi ([w:nd A] impe (impe u w) (impe v w)))))
	    (impi ([u:nd A] impi ([v:nd (B imp A)] u))))
	(impi ([u:nd A] impi ([v:nd B] u)))).

%%% The deduction theorem for Hilbert derivations

ded : (hil A -> hil B) -> hil (A imp B) -> type.

ded_id : ded ([u:hil A] u) (mp (mp s k) (k : hil (A imp (A imp A)))).

ded_k  : ded ([u:hil A] k) (mp k k).
ded_s  : ded ([u:hil A] s) (mp k s).

ded_n1 : ded ([u:hil A] n1) (mp k n1).
ded_n2 : ded ([u:hil A] n2) (mp k n2).

ded_f1 : ded ([u:hil A] f1 T) (mp k (f1 T)).
ded_f2 : ded ([u:hil A] f2) (mp k f2).

ded_mp : ded ([u:hil A] mp (H1 u) (H2 u)) (mp (mp s H1') H2')
	  <- ded H1 H1'
	  <- ded H2 H2'.

ded_ug : ded ([u:hil A] ug (H1 u)) (mp f2 (ug H1'))
	  <- ({a:i} ded ([u:hil A] H1 u a) (H1' a)).

%block lded : some {A:o} block {u:nd A} {v:hil A}
	   {h:{C:o} ded ([w:hil C] v) (mp k v)}.

%mode ded +H -H'.
%worlds (li | lo | lded) (ded H H').
%terminates H (ded H _).
%covers ded +H -H'.
%total H (ded H _).

%%% Mapping natural deductions to Hilbert derivations.

ndhil : nd A -> hil A -> type.

ndh_impi : ndhil (impi D1) H1'
	    <- ({u:nd A1} {v:hil A1}
		  ({C:o} ded ([w:hil C] v) (mp k v))
		  -> ndhil u v
		  -> ndhil (D1 u) (H1 v))
	    <- ded H1 H1'.

ndh_impe : ndhil (impe D1 D2) (mp H1 H2)
	    <- ndhil D1 H1
	    <- ndhil D2 H2.

ndh_noti : ndhil (noti D1) (mp (mp n1 H1') H1'')
	    <- ({p:o} {u:nd A1} {v:hil A1}
		  ({C:o} ded ([w:hil C] v) (mp k v))
		  -> ndhil u v
		  -> ndhil (D1 p u) (H1 p v))
	    <- ded (H1 (not A1)) H1'
	    <- ded (H1 A1) H1''.

ndh_note : ndhil (note D1 C D2) (mp (mp n2 H1) H2)
	    <- ndhil D1 H1
	    <- ndhil D2 H2.

ndh_foralli : ndhil (foralli D1) (ug H1)
	       <- ({a:i} ndhil (D1 a) (H1 a)).

ndh_foralle : ndhil (foralle D1 T) (mp (f1 T) H1)
	       <- ndhil D1 H1.

%mode ndhil +D -H.
%block lndhil : some {A:o} block {u:nd A} {v:hil A}
	   {h:{C:o} ded ([w:hil C] v) (mp k v)}
	   {nh:ndhil u v}.
%worlds (li | lo | lndhil) (ndhil D H).
%terminates D (ndhil D _).
%covers ndhil +D -H.
%total D (ndhil D _).