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