author  wenzelm 
Thu, 15 Nov 2001 18:21:38 +0100  
changeset 12209  09bc6f8456b9 
parent 12199  8213fd95acb5 
child 12484  7ad150f5fc10 
permissions  rwrr 
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 

12199  9 
(*** New version of mk_rew_rules ***) 
0  10 

11 
(*Should False yield False<>True, or should it solve goals some other way?*) 

12 

1036  13 
(*Analyse a theorem to atomic rewrite rules*) 
14 
fun atomize (conn_pairs, mem_pairs) th = 

15 
let fun tryrules pairs t = 

1461  16 
case head_of t of 
17 
Const(a,_) => 

18 
(case assoc(pairs,a) of 

19 
Some rls => flat (map (atomize (conn_pairs, mem_pairs)) 

20 
([th] RL rls)) 

21 
 None => [th]) 

22 
 _ => [th] 

1036  23 
in case concl_of th of 
1461  24 
Const("Trueprop",_) $ P => 
25 
(case P of 

26 
Const("op :",_) $ a $ b => tryrules mem_pairs b 

27 
 Const("True",_) => [] 

28 
 Const("False",_) => [] 

29 
 A => tryrules conn_pairs A) 

1036  30 
 _ => [th] 
31 
end; 

32 

0  33 
(*Analyse a rigid formula*) 
1036  34 
val ZF_conn_pairs = 
1461  35 
[("Ball", [bspec]), 
36 
("All", [spec]), 

37 
("op >", [mp]), 

38 
("op &", [conjunct1,conjunct2])]; 

0  39 

40 
(*Analyse a:b, where b is rigid*) 

1036  41 
val ZF_mem_pairs = 
1461  42 
[("Collect", [CollectD1,CollectD2]), 
43 
("op ", [DiffD1,DiffD2]), 

44 
("op Int", [IntD1,IntD2])]; 

0  45 

1036  46 
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); 
47 

12209
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

48 
simpset_ref() := 
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

49 
simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) 
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

50 
addcongs [if_weak_cong] 
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

51 
addsplits [split_if] 
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

52 
setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); 
09bc6f8456b9
type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm
parents:
12199
diff
changeset

53 

2469  54 

11323  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 

12199  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))  Q)", 

76 
"(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)))", 

78 
"(ALL x:A. P(x) > Q) <> ((EX x:A. P(x)) > Q)", 

79 
"(ALL x:0.P(x)) <> True", 

80 
"(ALL x:succ(i).P(x)) <> P(i) & (ALL x:i. P(x))", 

81 
"(ALL x:cons(a,B).P(x)) <> P(a) & (ALL x:B. P(x))", 

82 
"(ALL x:RepFun(A,f). P(x)) <> (ALL y:A. P(f(y)))", 

83 
"(ALL x:Union(A).P(x)) <> (ALL y:A. ALL x:y. P(x))", 

84 
"(ALL x:Collect(A,Q).P(x)) <> (ALL x:A. Q(x) > P(x))", 

85 
"(~(ALL x:A. P(x))) <> (EX x:A. ~P(x))"]; 

86 

87 
val ball_conj_distrib = 

88 
prover "(ALL x:A. P(x) & Q(x)) <> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"; 

89 

90 
val bex_simps = map prover 

91 
["(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)))", 

93 
"(EX x:0.P(x)) <> False", 

94 
"(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))", 

96 
"(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))", 

98 
"(EX x:Collect(A,Q).P(x)) <> (EX x:A. Q(x) & P(x))", 

99 
"(~(EX x:A. P(x))) <> (ALL x:A. ~P(x))"]; 

100 

101 
val bex_disj_distrib = 

102 
prover "(EX x:A. P(x)  Q(x)) <> ((EX x:A. P(x))  (EX x:A. Q(x)))"; 

103 

104 
val Rep_simps = map prover 

105 
["{x. y:0, R(x,y)} = 0", (*Replace*) 

106 
"{x:0. P(x)} = 0", (*Collect*) 

107 
"{x:A. False} = 0", 

108 
"{x:A. True} = A", 

109 
"RepFun(0,f) = 0", (*RepFun*) 

110 
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", 

111 
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] 

112 

113 
val misc_simps = map prover 

114 
["0 Un A = A", "A Un 0 = A", 

115 
"0 Int A = 0", "A Int 0 = 0", 

116 
"0  A = 0", "A  0 = A", 

117 
"Union(0) = 0", 

118 
"Union(cons(b,A)) = b Un Union(A)", 

119 
"Inter({b}) = b"] 

120 

121 

122 
val UN_simps = map prover 

123 
["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))", 

124 
"(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)", 

125 
"(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))", 

126 
"(UN x:C. A(x) Int B) = ((UN x:C. A(x)) Int B)", 

127 
"(UN x:C. A Int B(x)) = (A Int (UN x:C. B(x)))", 

128 
"(UN x:C. A(x)  B) = ((UN x:C. A(x))  B)", 

129 
"(UN x:C. A  B(x)) = (if C=0 then 0 else A  (INT x:C. B(x)))", 

130 
"(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))", 

131 
"(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))", 

132 
"(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"]; 

133 

134 
val INT_simps = map prover 

135 
["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B", 

136 
"(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))", 

137 
"(INT x:C. A(x)  B) = (INT x:C. A(x))  B", 

138 
"(INT x:C. A  B(x)) = (if C=0 then 0 else A  (UN x:C. B(x)))", 

139 
"(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))", 

140 
"(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)", 

141 
"(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"]; 

142 

143 
(** The _extend_simps rules are oriented in the opposite direction, to 

144 
pull UN and INT outwards. **) 

145 

146 
val UN_extend_simps = map prover 

147 
["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))", 

148 
"(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))", 

149 
"A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))", 

150 
"((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)", 

151 
"(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))", 

152 
"((UN x:C. A(x))  B) = (UN x:C. A(x)  B)", 

153 
"A  (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A  B(x)))", 

154 
"(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))", 

155 
"(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))", 

156 
"(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"]; 

157 

158 
val INT_extend_simps = map prover 

159 
["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)", 

160 
"A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))", 

161 
"(INT x:C. A(x))  B = (INT x:C. A(x)  B)", 

162 
"A  (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A  B(x)))", 

163 
"cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))", 

164 
"(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))", 

165 
"A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"]; 

166 

167 
end; 

168 

169 
bind_thms ("ball_simps", ball_simps); 

170 
bind_thm ("ball_conj_distrib", ball_conj_distrib); 

171 
bind_thms ("bex_simps", bex_simps); 

172 
bind_thm ("bex_disj_distrib", bex_disj_distrib); 

173 
bind_thms ("Rep_simps", Rep_simps); 

174 
bind_thms ("misc_simps", misc_simps); 

175 

176 
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps); 

177 

178 
bind_thms ("UN_simps", UN_simps); 

179 
bind_thms ("INT_simps", INT_simps); 

180 

181 
Addsimps (UN_simps @ INT_simps); 

182 

183 
bind_thms ("UN_extend_simps", UN_extend_simps); 

184 
bind_thms ("INT_extend_simps", INT_extend_simps); 

185 

186 

11233  187 
(** Onepoint rule for bounded quantifiers: see HOL/Set.ML **) 
188 

189 
Goal "(EX x:A. x=a) <> (a:A)"; 

190 
by (Blast_tac 1); 

191 
qed "bex_triv_one_point1"; 

192 

193 
Goal "(EX x:A. a=x) <> (a:A)"; 

194 
by (Blast_tac 1); 

195 
qed "bex_triv_one_point2"; 

196 

197 
Goal "(EX x:A. x=a & P(x)) <> (a:A & P(a))"; 

198 
by (Blast_tac 1); 

199 
qed "bex_one_point1"; 

200 

201 
Goal "(EX x:A. a=x & P(x)) <> (a:A & P(a))"; 

202 
by(Blast_tac 1); 

203 
qed "bex_one_point2"; 

204 

205 
Goal "(ALL x:A. x=a > P(x)) <> (a:A > P(a))"; 

206 
by (Blast_tac 1); 

207 
qed "ball_one_point1"; 

208 

209 
Goal "(ALL x:A. a=x > P(x)) <> (a:A > P(a))"; 

210 
by (Blast_tac 1); 

211 
qed "ball_one_point2"; 

212 

213 
Addsimps [bex_triv_one_point1,bex_triv_one_point2, 

214 
bex_one_point1,bex_one_point2, 

215 
ball_one_point1,ball_one_point2]; 

216 

12199  217 

11233  218 
let 
219 
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

220 
("EX x:A. P(x) & Q(x)",FOLogic.oT) 

221 

222 
val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN 

223 
Quantifier1.prove_one_point_ex_tac; 

224 

225 
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; 

226 

227 
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

228 
("ALL x:A. P(x) > Q(x)",FOLogic.oT) 

229 

230 
val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN 

231 
Quantifier1.prove_one_point_all_tac; 

232 

233 
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; 

234 

235 
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; 

236 
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; 

237 
in 

238 

239 
Addsimprocs [defBALL_regroup,defBEX_regroup] 

240 

241 
end; 

242 

12199  243 

4091  244 
val ZF_ss = simpset(); 