13 (writeln s; prove_goal thy s |
13 (writeln s; prove_goal thy s |
14 (fn prems => [ (cut_facts_tac prems 1), |
14 (fn prems => [ (cut_facts_tac prems 1), |
15 (fast_tac (!claset addSIs [equalityI]) 1) ])); |
15 (fast_tac (!claset addSIs [equalityI]) 1) ])); |
16 |
16 |
17 (*Are all these really suitable?*) |
17 (*Are all these really suitable?*) |
18 Addsimps (map prove_fun |
18 val ball_simps = map prove_fun |
19 ["(ALL x:0.P(x)) <-> True", |
19 ["(ALL x:0.P(x)) <-> True", |
20 "(EX x:0.P(x)) <-> False", |
20 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
21 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
21 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))", |
22 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))", |
22 "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
23 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))", |
23 "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", |
24 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))", |
24 "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"]; |
25 "(ALL x: RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
25 |
26 "(EX x: RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))"]); |
26 val bex_simps = map prove_fun |
|
27 ["(EX x:0.P(x)) <-> False", |
|
28 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))", |
|
29 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))", |
|
30 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
|
31 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
|
32 "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"]; |
|
33 |
|
34 Addsimps (ball_simps @ bex_simps); |
27 |
35 |
28 Addsimps (map prove_fun |
36 Addsimps (map prove_fun |
29 ["{x:0. P(x)} = 0", |
37 ["{x:0. P(x)} = 0", |
30 "{x:A. False} = 0", |
38 "{x:A. False} = 0", |
31 "{x:A. True} = A", |
39 "{x:A. True} = A", |