70 ALLGOALS (blast_tac (claset() addSIs[equalityI]))])); |
70 ALLGOALS (blast_tac (claset() addSIs[equalityI]))])); |
71 |
71 |
72 in |
72 in |
73 |
73 |
74 val ball_simps = map prover |
74 val ball_simps = map prover |
75 ["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", |
75 ["(ALL x:A. P(x) & Q) <-> (ALL x:A. P(x)) & (A=0 | Q)", |
|
76 "(ALL x:A. P & Q(x)) <-> (A=0 | P) & (ALL x:A. Q(x))", |
|
77 "(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", |
76 "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", |
78 "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", |
77 "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", |
79 "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", |
78 "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", |
80 "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", |
79 "(ALL x:0.P(x)) <-> True", |
81 "(ALL x:0.P(x)) <-> True", |
80 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", |
82 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", |
88 prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
90 prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
89 |
91 |
90 val bex_simps = map prover |
92 val bex_simps = map prover |
91 ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
93 ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
92 "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", |
94 "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", |
|
95 "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)", |
|
96 "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))", |
|
97 "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))", |
|
98 "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))", |
93 "(EX x:0.P(x)) <-> False", |
99 "(EX x:0.P(x)) <-> False", |
94 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", |
100 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", |
95 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", |
101 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", |
96 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
102 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
97 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
103 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |