(* August 19, 1997 (as part of general overhaul) *)

(* utilities for manipulating type labels plus definitions of
type constructors.  Subtyping requires the axiom of choice, so is deferred
to the file tableau2.mk2 *)

script "structural";  (* basic structural tactics *)

(* a parameter theorem ?thm is expected to be of the form
?x + ?y = t1: (t2:?x)+t3:?y *)

(* remove type label on right *)

start "?x^+?y";
ri "((RIGHT@LEFT@TYPES)** $?thm)*>?thm";
prove "TREMLEFT@?thm";

(* remove type label on left *)

start "?x^+?y";
ri "((RIGHT@RIGHT@TYPES)** $?thm)*>?thm";
prove "TREMRIGHT@?thm";

(* remove type labels on both sides *)

start "?x^+?y";
ri "((RIGHT@(RIGHT@TYPES)**(LEFT@TYPES))** $?thm)*>?thm";
prove "TREMBOTH@?thm";

(* remove type label at top *)

(* changed June 26th to prevent unintended side-effects *)

start "?t:?x";
ri "RIGHT@?thm"; ri "TYPES"; rri "?thm";
prove "TREMTOP@?thm";

(* add type label on left *)

start "?x";
ri "((RIGHT@LEFT@ $TYPES)** $?thm)*>?thm"; rri "?thm";
prove "TADDLEFT@?thm";


(* add type label on right *)

start "?x";
ri "((RIGHT@RIGHT@ $TYPES)** $?thm)*>?thm"; rri "?thm";
prove "TADDRIGHT@?thm";

(* add type labels on both sides *)

start "?x";
ri "((RIGHT@(RIGHT@ $TYPES)**(LEFT@ $TYPES))** $?thm)*>?thm"; rri "?thm";
prove "TADDBOTH@?thm";

(* add type label at top *)

start "?x";
ri "(($TYPES)**RIGHT@ $?thm)*>?thm";
prove "TADDTOP@?thm";

(* axioms for type constructors (June 19, 1997) *)

declaretypedinfix ~1 ~1 "->>";

axiom "ARROWTYPE" "(?t1 ->> ?t2):?f" "[?t2:?f@?t1:?1]";

declareinfix "<*>";

axiom "PRODTYPE" "(?t1 <*> ?t2):?x" "(?t1:P1@?x),?t2:P2@?x";

declareinfix "<+>";

axiom "UNIONTYPE" "(?t1 <+> ?t2):?x" "(?x=?t1:?x)||(?t1:?x),?t2:?x";

axiom "POINTTYPE" "[?x]:?y" "?x";

(*

(* This is not a satisfactory definition, because it puts the same error
object in every subtype of type ?t; the official definition will appear
after the axiom of choice in quantifiers.mk2 *)

declareinfix "|/";

declareconstant "error";

axiom "SUBTYPE"  "(?t |/ ?P):?x" "(?P@?t:?x)||(?t:?x),?t:error";

*)

(*

CONSTRUCTBOOL:

([true] <+> [false]) : ?x = 

bool : ?x

["BOOLDEF","CASEINTRO","EQUATION","POINTTYPE","REFLEX","UNIONTYPE"]

*)

s "([true]<+>[false]):?x";
ri "UNIONTYPE"; ex();
dlls "POINTTYPE";
ri "POINTTYPE"; ex();
top();
dlls "POINTTYPE";
ri "POINTTYPE"; ex();
top();
dlls "POINTTYPE";
ri "POINTTYPE"; ex();
top();
rri "EQUATION"; ex();
ri "EQSYMM"; ex();
rri "BOOLDEF"; ex();
p "CONSTRUCTBOOL";







quit();