4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Rewriting for ZF set theory: specialized extraction of rewrites from theorems |
6 Rewriting for ZF set theory: specialized extraction of rewrites from theorems |
7 *) |
7 *) |
8 |
8 |
9 (** Rewriting **) |
9 (*** New version of mk_rew_rules ***) |
10 |
|
11 local |
|
12 (*For proving rewrite rules*) |
|
13 fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1])); |
|
14 |
|
15 in |
|
16 |
|
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", |
|
23 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", |
|
24 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))", |
|
25 "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
|
26 "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", |
|
27 "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))", |
|
28 "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"]; |
|
29 |
|
30 val ball_conj_distrib = |
|
31 prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
|
32 |
|
33 val bex_simps = map prover |
|
34 ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
|
35 "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", |
|
36 "(EX x:0.P(x)) <-> False", |
|
37 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", |
|
38 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", |
|
39 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
|
40 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
|
41 "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))", |
|
42 "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"]; |
|
43 |
|
44 val bex_disj_distrib = |
|
45 prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; |
|
46 |
|
47 val Rep_simps = map prover |
|
48 ["{x. y:0, R(x,y)} = 0", (*Replace*) |
|
49 "{x:0. P(x)} = 0", (*Collect*) |
|
50 "{x:A. False} = 0", |
|
51 "{x:A. True} = A", |
|
52 "RepFun(0,f) = 0", (*RepFun*) |
|
53 "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", |
|
54 "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] |
|
55 |
|
56 val misc_simps = map prover |
|
57 ["0 Un A = A", "A Un 0 = A", |
|
58 "0 Int A = 0", "A Int 0 = 0", |
|
59 "0 - A = 0", "A - 0 = A", |
|
60 "Union(0) = 0", |
|
61 "Union(cons(b,A)) = b Un Union(A)", |
|
62 "Inter({b}) = b"] |
|
63 |
|
64 end; |
|
65 |
|
66 bind_thms ("ball_simps", ball_simps); |
|
67 bind_thm ("ball_conj_distrib", ball_conj_distrib); |
|
68 bind_thms ("bex_simps", bex_simps); |
|
69 bind_thm ("bex_disj_distrib", bex_disj_distrib); |
|
70 bind_thms ("Rep_simps", Rep_simps); |
|
71 bind_thms ("misc_simps", misc_simps); |
|
72 |
|
73 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); |
|
74 |
|
75 |
|
76 (** New version of mk_rew_rules **) |
|
77 |
10 |
78 (*Should False yield False<->True, or should it solve goals some other way?*) |
11 (*Should False yield False<->True, or should it solve goals some other way?*) |
79 |
12 |
80 (*Analyse a theorem to atomic rewrite rules*) |
13 (*Analyse a theorem to atomic rewrite rules*) |
81 fun atomize (conn_pairs, mem_pairs) th = |
14 fun atomize (conn_pairs, mem_pairs) th = |
123 by (Simp_tac 1); |
56 by (Simp_tac 1); |
124 qed "split_if_asm"; |
57 qed "split_if_asm"; |
125 |
58 |
126 bind_thms ("if_splits", [split_if, split_if_asm]); |
59 bind_thms ("if_splits", [split_if, split_if_asm]); |
127 |
60 |
|
61 |
|
62 (*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***) |
|
63 |
|
64 local |
|
65 (*For proving rewrite rules*) |
|
66 fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s |
|
67 (fn _ => [Simp_tac 1, |
|
68 ALLGOALS (blast_tac (claset() addSIs[equalityI]))])); |
|
69 |
|
70 in |
|
71 |
|
72 val ball_simps = map prover |
|
73 ["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)", |
|
74 "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))", |
|
75 "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))", |
|
76 "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", |
|
77 "(ALL x:0.P(x)) <-> True", |
|
78 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", |
|
79 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))", |
|
80 "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
|
81 "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", |
|
82 "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))", |
|
83 "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"]; |
|
84 |
|
85 val ball_conj_distrib = |
|
86 prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
|
87 |
|
88 val bex_simps = map prover |
|
89 ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
|
90 "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))", |
|
91 "(EX x:0.P(x)) <-> False", |
|
92 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", |
|
93 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", |
|
94 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
|
95 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
|
96 "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))", |
|
97 "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"]; |
|
98 |
|
99 val bex_disj_distrib = |
|
100 prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; |
|
101 |
|
102 val Rep_simps = map prover |
|
103 ["{x. y:0, R(x,y)} = 0", (*Replace*) |
|
104 "{x:0. P(x)} = 0", (*Collect*) |
|
105 "{x:A. False} = 0", |
|
106 "{x:A. True} = A", |
|
107 "RepFun(0,f) = 0", (*RepFun*) |
|
108 "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", |
|
109 "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] |
|
110 |
|
111 val misc_simps = map prover |
|
112 ["0 Un A = A", "A Un 0 = A", |
|
113 "0 Int A = 0", "A Int 0 = 0", |
|
114 "0 - A = 0", "A - 0 = A", |
|
115 "Union(0) = 0", |
|
116 "Union(cons(b,A)) = b Un Union(A)", |
|
117 "Inter({b}) = b"] |
|
118 |
|
119 |
|
120 val UN_simps = map prover |
|
121 ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))", |
|
122 "(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)", |
|
123 "(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))", |
|
124 "(UN x:C. A(x) Int B) = ((UN x:C. A(x)) Int B)", |
|
125 "(UN x:C. A Int B(x)) = (A Int (UN x:C. B(x)))", |
|
126 "(UN x:C. A(x) - B) = ((UN x:C. A(x)) - B)", |
|
127 "(UN x:C. A - B(x)) = (if C=0 then 0 else A - (INT x:C. B(x)))", |
|
128 "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))", |
|
129 "(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))", |
|
130 "(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"]; |
|
131 |
|
132 val INT_simps = map prover |
|
133 ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B", |
|
134 "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))", |
|
135 "(INT x:C. A(x) - B) = (INT x:C. A(x)) - B", |
|
136 "(INT x:C. A - B(x)) = (if C=0 then 0 else A - (UN x:C. B(x)))", |
|
137 "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))", |
|
138 "(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)", |
|
139 "(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"]; |
|
140 |
|
141 (** The _extend_simps rules are oriented in the opposite direction, to |
|
142 pull UN and INT outwards. **) |
|
143 |
|
144 val UN_extend_simps = map prover |
|
145 ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))", |
|
146 "(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))", |
|
147 "A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))", |
|
148 "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)", |
|
149 "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))", |
|
150 "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)", |
|
151 "A - (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A - B(x)))", |
|
152 "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))", |
|
153 "(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))", |
|
154 "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"]; |
|
155 |
|
156 val INT_extend_simps = map prover |
|
157 ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)", |
|
158 "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))", |
|
159 "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)", |
|
160 "A - (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A - B(x)))", |
|
161 "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))", |
|
162 "(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))", |
|
163 "A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"]; |
|
164 |
|
165 end; |
|
166 |
|
167 bind_thms ("ball_simps", ball_simps); |
|
168 bind_thm ("ball_conj_distrib", ball_conj_distrib); |
|
169 bind_thms ("bex_simps", bex_simps); |
|
170 bind_thm ("bex_disj_distrib", bex_disj_distrib); |
|
171 bind_thms ("Rep_simps", Rep_simps); |
|
172 bind_thms ("misc_simps", misc_simps); |
|
173 |
|
174 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); |
|
175 |
|
176 bind_thms ("UN_simps", UN_simps); |
|
177 bind_thms ("INT_simps", INT_simps); |
|
178 |
|
179 Addsimps (UN_simps @ INT_simps); |
|
180 |
|
181 bind_thms ("UN_extend_simps", UN_extend_simps); |
|
182 bind_thms ("INT_extend_simps", INT_extend_simps); |
|
183 |
|
184 |
128 (** One-point rule for bounded quantifiers: see HOL/Set.ML **) |
185 (** One-point rule for bounded quantifiers: see HOL/Set.ML **) |
129 |
186 |
130 Goal "(EX x:A. x=a) <-> (a:A)"; |
187 Goal "(EX x:A. x=a) <-> (a:A)"; |
131 by (Blast_tac 1); |
188 by (Blast_tac 1); |
132 qed "bex_triv_one_point1"; |
189 qed "bex_triv_one_point1"; |