author | paulson |
Fri, 06 Jun 1997 12:48:21 +0200 | |
changeset 3425 | fc4ca570d185 |
parent 2876 | 02c12d4c8b97 |
child 3840 | e0baea4d485a |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/simpdata |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
2469 | 6 |
Rewriting for ZF set theory: specialized extraction of rewrites from theorems |
0 | 7 |
*) |
8 |
||
2469 | 9 |
(** Rewriting **) |
0 | 10 |
|
3425 | 11 |
local |
12 |
(*For proving rewrite rules*) |
|
13 |
fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1])); |
|
14 |
||
15 |
in |
|
0 | 16 |
|
3425 | 17 |
val ball_simps = map prover |
18 |
["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", |
|
19 |
"(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", |
|
20 |
"(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", |
|
21 |
"(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", |
|
22 |
"(ALL x:0.P(x)) <-> True", |
|
2482
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
23 |
"(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
24 |
"(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
25 |
"(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
26 |
"(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
27 |
"(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"]; |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
28 |
|
3425 | 29 |
val ball_conj_distrib = |
30 |
prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
|
31 |
||
32 |
val bex_simps = map prover |
|
33 |
["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
|
34 |
"(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", |
|
35 |
"(EX x:0.P(x)) <-> False", |
|
2482
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
36 |
"(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
37 |
"(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
38 |
"(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
39 |
"(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
40 |
"(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"]; |
87383dd9f4b5
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
41 |
|
3425 | 42 |
val bex_disj_distrib = |
43 |
prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; |
|
44 |
||
45 |
val Rep_simps = map prover |
|
46 |
["{x:0. P(x)} = 0", |
|
47 |
"{x:A. False} = 0", |
|
48 |
"{x:A. True} = A", |
|
49 |
"RepFun(0,f) = 0", |
|
50 |
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", |
|
51 |
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] |
|
0 | 52 |
|
3425 | 53 |
val misc_simps = map prover |
54 |
["0 Un A = A", "A Un 0 = A", |
|
55 |
"0 Int A = 0", "A Int 0 = 0", |
|
56 |
"0-A = 0", "A-0 = A", |
|
57 |
"Union(0) = 0", |
|
58 |
"Union(cons(b,A)) = b Un Union(A)", |
|
59 |
"Inter({b}) = b"] |
|
0 | 60 |
|
3425 | 61 |
end; |
62 |
||
63 |
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); |
|
64 |
||
0 | 65 |
|
66 |
(** New version of mk_rew_rules **) |
|
67 |
||
68 |
(*Should False yield False<->True, or should it solve goals some other way?*) |
|
69 |
||
1036 | 70 |
(*Analyse a theorem to atomic rewrite rules*) |
71 |
fun atomize (conn_pairs, mem_pairs) th = |
|
72 |
let fun tryrules pairs t = |
|
1461 | 73 |
case head_of t of |
74 |
Const(a,_) => |
|
75 |
(case assoc(pairs,a) of |
|
76 |
Some rls => flat (map (atomize (conn_pairs, mem_pairs)) |
|
77 |
([th] RL rls)) |
|
78 |
| None => [th]) |
|
79 |
| _ => [th] |
|
1036 | 80 |
in case concl_of th of |
1461 | 81 |
Const("Trueprop",_) $ P => |
82 |
(case P of |
|
83 |
Const("op :",_) $ a $ b => tryrules mem_pairs b |
|
84 |
| Const("True",_) => [] |
|
85 |
| Const("False",_) => [] |
|
86 |
| A => tryrules conn_pairs A) |
|
1036 | 87 |
| _ => [th] |
88 |
end; |
|
89 |
||
0 | 90 |
(*Analyse a rigid formula*) |
1036 | 91 |
val ZF_conn_pairs = |
1461 | 92 |
[("Ball", [bspec]), |
93 |
("All", [spec]), |
|
94 |
("op -->", [mp]), |
|
95 |
("op &", [conjunct1,conjunct2])]; |
|
0 | 96 |
|
97 |
(*Analyse a:b, where b is rigid*) |
|
1036 | 98 |
val ZF_mem_pairs = |
1461 | 99 |
[("Collect", [CollectD1,CollectD2]), |
100 |
("op -", [DiffD1,DiffD2]), |
|
101 |
("op Int", [IntD1,IntD2])]; |
|
0 | 102 |
|
1036 | 103 |
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); |
104 |
||
2469 | 105 |
simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all); |
106 |
||
107 |
val ZF_ss = !simpset; |