%%% Refinement rules for natural deduction
%%% It can also be viewed as a single-conclusion sequent calculus.
%%% These rules are not operational.
%%%
%%% Author: Frank Pfenning

hyp  : o -> type.  % Hypotheses (left)
conc : o -> type.  % Conclusion (right)
%name hyp H
%name conc R

axiom : (hyp A -> conc A).

cut : conc A
       -> (hyp A -> conc C)
       -> conc C.

% Conjunction
andr  : conc A
	 -> conc B
	 -> conc (A and B).

andl1 : (hyp A -> conc C)
	 -> (hyp (A and B) -> conc C).

andl2 : (hyp B -> conc C)
	 -> (hyp (A and B) -> conc C).

% Implication
impr  : (hyp A -> conc B)
	 -> conc (A imp B).

impl  : conc A
	 -> (hyp B -> conc C)
	 -> (hyp (A imp B) -> conc C).

% Disjunction
orr1  : conc A
	 -> conc (A or B).

orr2  : conc B
	 -> conc (A or B).

orl   : (hyp A -> conc C)
	 -> (hyp B -> conc C)
	 -> (hyp (A or B) -> conc C).

% Truth
truer : conc (true).
% no truel

% Falsehood
% no falser
falsel : (hyp (false) -> conc C).

% Negation
notr   : ({p:o} hyp A -> conc p)
	  -> conc (not A).

notl   : conc A
	  -> ({C:o} hyp (not A) -> conc C).

% Universal Quantification
forallr : ({a:i} conc (A a))
	   -> conc (forall A). 

foralll : {T:i} (hyp (A T) -> conc C)
	   -> (hyp (forall A) -> conc C).

% Existential Quantification
existsr : {T:i} conc (A T)
	   -> conc (exists A).

existsl : ({a:i} hyp (A a) -> conc C)
	   -> (hyp (exists A) -> conc C).