1(*---------------------------------------------------------------------------* 2 * Some first order logic examples, using John Harrison's implementation * 3 * of MESON. There are many more such examples in src/meson/test.sml. * 4 *---------------------------------------------------------------------------*) 5 6(*---------------------------------------------------------------------------* 7 * Invokes MESON and supplies some statistics as well. * 8 *---------------------------------------------------------------------------*) 9 10fun Prove tm = 11 Lib.with_flag(mesonLib.chatting, 1) 12 (Count.apply Tactical.prove) 13 (tm,mesonLib.MESON_TAC[]); 14 15 16val LOS = Term 17 `(!x y z. P x y /\ P y z ==> P x z) /\ 18 (!x y z. Q x y /\ Q y z ==> Q x z) /\ 19 (!x y. P x y ==> P y x) /\ 20 (!x y. P x y \/ Q x y) 21 ==> (!x y. P x y) \/ (!x y. Q x y)`; 22 23Prove LOS;; 24 25 26val CAT001_3 = Term 27`(!X. equal(X,X)) /\ 28 (!Y X. equal(X,Y) ==> equal(Y,X)) /\ 29 (!Y X Z. equal(X,Y) /\ equal(Y,Z) ==> equal(X,Z)) /\ 30 (!Y X. equivalent(X,Y) ==> there_exists(X)) /\ 31 (!X Y. equivalent(X,Y) ==> equal(X,Y)) /\ 32 (!X Y. there_exists(X) /\ equal(X,Y) ==> equivalent(X,Y)) /\ 33 (!X. there_exists(domain(X)) ==> there_exists(X)) /\ 34 (!X. there_exists(codomain(X)) ==> there_exists(X)) /\ 35 (!Y X. there_exists(compose(X,Y)) ==> there_exists(domain(X))) /\ 36 (!X Y. there_exists(compose(X,Y)) ==> equal(domain(X),codomain(Y))) /\ 37 (!X Y. there_exists(domain(X)) /\ equal(domain(X),codomain(Y)) ==> 38 there_exists(compose(X,Y))) /\ 39 (!X Y Z. equal(compose(X,compose(Y,Z)),compose(compose(X,Y),Z))) /\ 40 (!X. equal(compose(X,domain(X)),X)) /\ 41 (!X. equal(compose(codomain(X),X),X)) /\ 42 (!X Y. equivalent(X,Y) ==> there_exists(Y)) /\ 43 (!X Y. there_exists X /\ there_exists Y /\ equal(X,Y) ==> equivalent(X,Y)) /\ 44 (!Y X. there_exists(compose(X,Y)) ==> there_exists(codomain(X))) /\ 45 (!X Y. there_exists(f1(X,Y)) \/ equal(X,Y)) /\ 46 (!X Y. equal(X,f1(X,Y)) \/ equal(Y,f1(X,Y)) \/ equal(X,Y)) /\ 47 (!X Y. equal(X,f1(X,Y)) /\ equal(Y,f1(X,Y)) ==> equal(X,Y)) /\ 48 (!X Y. equal(X,Y) /\ there_exists(X) ==> there_exists(Y)) /\ 49 (!X Y Z. equal(X,Y) /\ equivalent(X,Z) ==> equivalent(Y,Z)) /\ 50 (!X Z Y. equal(X,Y) /\ equivalent(Z,X) ==> equivalent(Z,Y)) /\ 51 (!X Y. equal(X,Y) ==> equal(domain(X),domain(Y))) /\ 52 (!X Y. equal(X,Y) ==> equal(codomain(X),codomain(Y))) /\ 53 (!X Y Z. equal(X,Y) ==> equal(compose(X,Z),compose(Y,Z))) /\ 54 (!X Z Y. equal(X,Y) ==> equal(compose(Z,X),compose(Z,Y))) /\ 55 (!A B C. equal(A,B) ==> equal(f1(A,C),f1(B,C))) /\ 56 (!D F' E. equal(D,E) ==> equal(f1(F',D),f1(F',E))) /\ 57 (there_exists(compose(a,b))) /\ 58 (!Y X Z. equal(compose(compose(a,b),X),Y) /\ 59 equal(compose(compose(a,b),Z),Y) ==> equal(X,Z)) /\ 60 (there_exists(compose(b,h))) /\ 61 (equal(compose(b,h),compose(b,g))) /\ 62 (~equal(h,g)) 63 ==> 64 F`; 65 66Prove CAT001_3; 67 68 69val CAT005_1 = Term 70`(!X. equal(X,X)) /\ 71 (!Y X. equal(X,Y) ==> equal(Y,X)) /\ 72 (!Y X Z. equal(X,Y) /\ equal(Y,Z) ==> equal(X,Z)) /\ 73 (!X Y. defined(X,Y) ==> product(X,Y,compose(X,Y))) /\ 74 (!Z X Y. product(X,Y,Z) ==> defined(X,Y)) /\ 75 (!X Xy Y Z. product(X,Y,Xy) /\ defined(Xy,Z) ==> defined(Y,Z)) /\ 76 (!Y Xy Z X Yz. product(X,Y,Xy) /\ product(Y,Z,Yz) /\ 77 defined(Xy,Z) ==> defined(X,Yz)) /\ 78 (!Xy Y Z X Yz Xyz. product(X,Y,Xy) /\ product(Xy,Z,Xyz) /\ 79 product(Y,Z,Yz) ==> product(X,Yz,Xyz)) /\ 80 (!Z Yz X Y. product(Y,Z,Yz) /\ defined(X,Yz) ==> defined(X,Y)) /\ 81 (!Y X Yz Xy Z. product(Y,Z,Yz) /\ product(X,Y,Xy) /\ 82 defined(X,Yz) ==> defined(Xy,Z)) /\ 83 (!Yz X Y Xy Z Xyz. product(Y,Z,Yz) /\ product(X,Yz,Xyz) /\ 84 product(X,Y,Xy) ==> product(Xy,Z,Xyz)) /\ 85 (!Y X Z. defined(X,Y) /\ defined(Y,Z) /\ identity_map(Y) ==> defined(X,Z)) /\ 86 (!X. identity_map(domain(X))) /\ 87 (!X. identity_map(codomain(X))) /\ 88 (!X. defined(X,domain(X))) /\ 89 (!X. defined(codomain(X),X)) /\ 90 (!X. product(X,domain(X),X)) /\ 91 (!X. product(codomain(X),X,X)) /\ 92 (!X Y. defined(X,Y) /\ identity_map(X) ==> product(X,Y,Y)) /\ 93 (!Y X. defined(X,Y) /\ identity_map(Y) ==> product(X,Y,X)) /\ 94 (!X Y Z W. product(X,Y,Z) /\ product(X,Y,W) ==> equal(Z,W)) /\ 95 (!X Y Z W. equal(X,Y) /\ product(X,Z,W) ==> product(Y,Z,W)) /\ 96 (!X Z Y W. equal(X,Y) /\ product(Z,X,W) ==> product(Z,Y,W)) /\ 97 (!X Z W Y. equal(X,Y) /\ product(Z,W,X) ==> product(Z,W,Y)) /\ 98 (!X Y. equal(X,Y) ==> equal(domain(X),domain(Y))) /\ 99 (!X Y. equal(X,Y) ==> equal(codomain(X),codomain(Y))) /\ 100 (!X Y. equal(X,Y) /\ identity_map(X) ==> identity_map(Y)) /\ 101 (!X Y Z. equal(X,Y) /\ defined(X,Z) ==> defined(Y,Z)) /\ 102 (!X Z Y. equal(X,Y) /\ defined(Z,X) ==> defined(Z,Y)) /\ 103 (!X Z Y. equal(X,Y) ==> equal(compose(Z,X),compose(Z,Y))) /\ 104 (!X Y Z. equal(X,Y) ==> equal(compose(X,Z),compose(Y,Z))) /\ 105 (defined(a,d)) /\ 106 (identity_map(d)) /\ 107 (~equal(domain(a),d)) 108 ==> 109 F`; 110 111 112Prove CAT005_1; (* Takes a while *) 113