#use "hol.ml";; let SUBPRED = new_definition `SUBPRED X Y <=> (!x. X x ==> Y x)`;; let MINUS = new_definition `MINUS X Y x <=> X x /\ ~Y x`;; let MINUS_ANTIMON = MESON [SUBPRED;MINUS] `SUBPRED X Y ==> SUBPRED (MINUS AA Y) (MINUS AA X)`;; let IM = new_definition `IM f X y <=> (?x. X x /\ y = f x)`;; let IM_MON = MESON [SUBPRED;IM] `SUBPRED X Y ==> SUBPRED (IM f X) (IM f Y)`;; g `!Phi:(A->bool)->A->bool. (!U V. SUBPRED U V ==> SUBPRED (Phi U) (Phi V)) ==> ?Y. SUBPRED (Phi Y) Y /\ SUBPRED Y (Phi Y)`;; e(GEN_TAC);; e(DISCH_TAC);; e(EXISTS_TAC(`\u:A. !X. SUBPRED (Phi X) X ==> X u`));; e(ASM_MESON_TAC[SUBPRED]);; let KT = top_thm();; let INJFUN = new_definition `INJFUN (f:A->B) <=> (!x y. f x = f y ==> x = y)`;; let INJFUN = new_definition `INJFUN AA BB f <=> (!x. AA x ==> BB (f x)) /\ (!x y. AA x /\ AA y /\ f x = f y ==> x = y)`;; let EQPOT1 = new_definition `EQPOT1 AA BB R <=> (!x. AA x ==> (?y. BB y /\ R x y))`;; let EQPOT2 = new_definition `EQPOT2 AA BB R <=> (!y. BB y ==> (?x. AA x /\ R x y))`;; let EQPOT3 = new_definition `EQPOT3 AA BB R <=> (!x y z w. AA x /\ BB y /\ AA z /\ BB w /\ R x y /\ R z w ==> (x = z <=> y = w))`;; let EQPOT = new_definition `EQPOT AA BB <=> (?R. EQPOT1 AA BB R /\ EQPOT2 AA BB R /\ EQPOT3 AA BB R)`;; g `INJFUN (AA:A->bool) (BB:B->bool) f ==> INJFUN BB AA g ==> EQPOT AA BB`;; (*** Left to reader ***) let CBS = top_thm();; g `INJFUN (AA:A->bool) (BB:A->bool) f ==> SUBPRED BB AA ==> EQPOT AA BB`;; (*** Left to reader ***) let CBSCOR = top_thm();;