46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); |
46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); |
47 |
47 |
48 simpset_ref() := |
48 simpset_ref() := |
49 simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) |
49 simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) |
50 addcongs [if_weak_cong] |
50 addcongs [if_weak_cong] |
51 addsplits [split_if] |
|
52 setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); |
51 setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); |
53 |
52 |
54 |
|
55 (** Splitting IFs in the assumptions **) |
|
56 |
|
57 Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"; |
|
58 by (Simp_tac 1); |
|
59 qed "split_if_asm"; |
|
60 |
|
61 bind_thms ("if_splits", [split_if, split_if_asm]); |
|
62 |
|
63 |
|
64 (*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***) |
|
65 |
|
66 local |
|
67 (*For proving rewrite rules*) |
|
68 fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s |
|
69 (fn _ => [Simp_tac 1, |
|
70 ALLGOALS (blast_tac (claset() addSIs[equalityI]))])); |
|
71 |
|
72 in |
|
73 |
|
74 val ball_simps = map prover |
|
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)", |
|
78 "(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)))", |
|
80 "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)", |
|
81 "(ALL x:0.P(x)) <-> True", |
|
82 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))", |
|
83 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))", |
|
84 "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))", |
|
85 "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))", |
|
86 "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))", |
|
87 "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"]; |
|
88 |
|
89 val ball_conj_distrib = |
|
90 prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; |
|
91 |
|
92 val bex_simps = map prover |
|
93 ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)", |
|
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))", |
|
99 "(EX x:0.P(x)) <-> False", |
|
100 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))", |
|
101 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))", |
|
102 "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))", |
|
103 "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))", |
|
104 "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))", |
|
105 "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"]; |
|
106 |
|
107 val bex_disj_distrib = |
|
108 prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"; |
|
109 |
|
110 val Rep_simps = map prover |
|
111 ["{x. y:0, R(x,y)} = 0", (*Replace*) |
|
112 "{x:0. P(x)} = 0", (*Collect*) |
|
113 "{x:A. P} = (if P then A else 0)", |
|
114 "RepFun(0,f) = 0", (*RepFun*) |
|
115 "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", |
|
116 "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] |
|
117 |
|
118 val misc_simps = map prover |
|
119 ["0 Un A = A", "A Un 0 = A", |
|
120 "0 Int A = 0", "A Int 0 = 0", |
|
121 "0 - A = 0", "A - 0 = A", |
|
122 "Union(0) = 0", |
|
123 "Union(cons(b,A)) = b Un Union(A)", |
|
124 "Inter({b}) = b"] |
|
125 |
|
126 |
|
127 val UN_simps = map prover |
|
128 ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))", |
|
129 "(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)", |
|
130 "(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))", |
|
131 "(UN x:C. A(x) Int B) = ((UN x:C. A(x)) Int B)", |
|
132 "(UN x:C. A Int B(x)) = (A Int (UN x:C. B(x)))", |
|
133 "(UN x:C. A(x) - B) = ((UN x:C. A(x)) - B)", |
|
134 "(UN x:C. A - B(x)) = (if C=0 then 0 else A - (INT x:C. B(x)))", |
|
135 "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))", |
|
136 "(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))", |
|
137 "(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"]; |
|
138 |
|
139 val INT_simps = map prover |
|
140 ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B", |
|
141 "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))", |
|
142 "(INT x:C. A(x) - B) = (INT x:C. A(x)) - B", |
|
143 "(INT x:C. A - B(x)) = (if C=0 then 0 else A - (UN x:C. B(x)))", |
|
144 "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))", |
|
145 "(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)", |
|
146 "(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"]; |
|
147 |
|
148 (** The _extend_simps rules are oriented in the opposite direction, to |
|
149 pull UN and INT outwards. **) |
|
150 |
|
151 val UN_extend_simps = map prover |
|
152 ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))", |
|
153 "(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))", |
|
154 "A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))", |
|
155 "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)", |
|
156 "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))", |
|
157 "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)", |
|
158 "A - (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A - B(x)))", |
|
159 "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))", |
|
160 "(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))", |
|
161 "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"]; |
|
162 |
|
163 val INT_extend_simps = map prover |
|
164 ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)", |
|
165 "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))", |
|
166 "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)", |
|
167 "A - (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A - B(x)))", |
|
168 "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))", |
|
169 "(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))", |
|
170 "A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"]; |
|
171 |
|
172 end; |
|
173 |
|
174 bind_thms ("ball_simps", ball_simps); |
|
175 bind_thm ("ball_conj_distrib", ball_conj_distrib); |
|
176 bind_thms ("bex_simps", bex_simps); |
|
177 bind_thm ("bex_disj_distrib", bex_disj_distrib); |
|
178 bind_thms ("Rep_simps", Rep_simps); |
|
179 bind_thms ("misc_simps", misc_simps); |
|
180 |
|
181 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); |
|
182 |
|
183 bind_thms ("UN_simps", UN_simps); |
|
184 bind_thms ("INT_simps", INT_simps); |
|
185 |
|
186 Addsimps (UN_simps @ INT_simps); |
|
187 |
|
188 bind_thms ("UN_extend_simps", UN_extend_simps); |
|
189 bind_thms ("INT_extend_simps", INT_extend_simps); |
|
190 |
|
191 |
|
192 (** One-point rule for bounded quantifiers: see HOL/Set.ML **) |
|
193 |
|
194 Goal "(EX x:A. x=a) <-> (a:A)"; |
|
195 by (Blast_tac 1); |
|
196 qed "bex_triv_one_point1"; |
|
197 |
|
198 Goal "(EX x:A. a=x) <-> (a:A)"; |
|
199 by (Blast_tac 1); |
|
200 qed "bex_triv_one_point2"; |
|
201 |
|
202 Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"; |
|
203 by (Blast_tac 1); |
|
204 qed "bex_one_point1"; |
|
205 |
|
206 Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"; |
|
207 by (Blast_tac 1); |
|
208 qed "bex_one_point2"; |
|
209 |
|
210 Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"; |
|
211 by (Blast_tac 1); |
|
212 qed "ball_one_point1"; |
|
213 |
|
214 Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))"; |
|
215 by (Blast_tac 1); |
|
216 qed "ball_one_point2"; |
|
217 |
|
218 Addsimps [bex_triv_one_point1,bex_triv_one_point2, |
|
219 bex_one_point1,bex_one_point2, |
|
220 ball_one_point1,ball_one_point2]; |
|
221 |
53 |
222 |
54 |
223 local |
55 local |
224 |
56 |
225 val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac; |
57 val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac; |