% File: hol-1.0.elf

% The HOL-Nuprl connection.
% A formalziation of HOL.
% Author: Carsten Schuermann, Mark-Oliver Stehr.

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


tp : type.				%name tp (A B).

--> : tp -> tp -> tp.			%infix right 10 -->.

o  : tp.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Terms
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


tm : tp -> type.			%name tm (H G) (x y P Q R).

=>: tm (o --> o --> o).

== : tm (A --> A --> o).

@ : tm (A --> B) -> tm A -> tm B.	%infix left 15 @.

\ : (tm A -> tm B) -> tm (A --> B).  

==> = [H:tm o] [G:tm o] => @ H @ G.	%infix right 13 ==>.

=== = [H:tm A] [G:tm A] == @ H @ G.	%infix left 14 ===.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Derivability
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


|-    : tm o -> type.			%prefix 10 |-. 
                                        %name |- D u.

mp    : |- H -> |- H ==> G -> |- G.

disch : (|- H -> |- G) -> |- H ==> G.

refl  : |- H === H. 

beta  : |- (\ H) @ G === (H G).

sub   : {G:tm A -> tm o} |- H1 === H2 -> |- G H1 -> |- G H2.

abs   : |- \ H === \ G 
	 <- ({x} |- H x === G x).


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Booleans
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

bool  = o.

true  : tm bool = (\ [x : tm bool] x) === (\ [x: tm bool] x).
all|  : tm ((A --> bool) --> bool)
      = \ [P:tm (A --> bool)] P === \ [x] true.
all   = [P] all| @ P.
false : tm bool = all (\ [P] P).
neg   : tm (bool --> bool) = \ [P:tm bool] P ==> false.
/|\   : tm (bool --> bool --> bool)
      = \ [P:tm bool] \ [Q:tm bool] all (\ [R:tm bool] (P ==> Q ==> R) ==> R).	
/\    = [P] [Q] /|\ @ P @ Q.		%infix right 12 /\.
\|/   : tm (bool --> bool --> bool)	
      = \ [P:tm bool] \ [Q:tm bool] all (\ [R:tm bool] (P ==> R) ==> (Q ==> R) ==> R).	
\/    = [P] [Q] \|/ @ P @ Q.		%infix right 11 \/.
the|  : tm ((A --> bool) --> A).
the   = [P] the| @ P.
ex|   : tm ((A --> bool) --> bool)
      = \ [P:tm (A --> bool)] P @ (the (\ [x] P @ x)).
ex    = [P] ex| @ P.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Axioms 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

cases-ax   : |- all (\ [x:tm bool] x === true \/ x === false).
antisym-ax : |- all (\ [x:tm bool] 
                           all (\ [y:tm bool] 
                                  (x ==> y) ==> (y ==> x) ==> x === y)).
eta-ax     : |- (\ [x] F @ x) === F.
select-ax  : |- all (\ [P]  all (\ [x] P @ x ==>  P @ (the P))).