author  wenzelm 
Sat, 20 Jan 2007 14:09:11 +0100  
changeset 22128  cdd92316dd31 
parent 21674  8a6bf9d7c751 
child 22147  f4ed4d940d44 
permissions  rwrr 
21163  1 
(* Title: HOL/simpdata.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1991 University of Cambridge 

5 

6 
Instantiation of the generic simplifier for HOL. 

7 
*) 

8 

9 
(** tools setup **) 

10 

11 
structure Quantifier1 = Quantifier1Fun 

12 
(struct 

13 
(*abstract syntax*) 

14 
fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t) 

15 
 dest_eq _ = NONE; 

16 
fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t) 

17 
 dest_conj _ = NONE; 

18 
fun dest_imp ((c as Const("op >",_)) $ s $ t) = SOME (c, s, t) 

19 
 dest_imp _ = NONE; 

20 
val conj = HOLogic.conj 

21 
val imp = HOLogic.imp 

22 
(*rules*) 

21551  23 
val iff_reflection = thm "eq_reflection" 
24 
val iffI = thm "iffI" 

25 
val iff_trans = thm "trans" 

26 
val conjI= thm "conjI" 

27 
val conjE= thm "conjE" 

28 
val impI = thm "impI" 

29 
val mp = thm "mp" 

21163  30 
val uncurry = thm "uncurry" 
21551  31 
val exI = thm "exI" 
32 
val exE = thm "exE" 

21163  33 
val iff_allI = thm "iff_allI" 
34 
val iff_exI = thm "iff_exI" 

35 
val all_comm = thm "all_comm" 

36 
val ex_comm = thm "ex_comm" 

37 
end); 

38 

21551  39 
structure Simpdata = 
21163  40 
struct 
41 

21551  42 
local 
43 
val eq_reflection = thm "eq_reflection" 

44 
in fun mk_meta_eq r = r RS eq_reflection end; 

21163  45 
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; 
46 

21551  47 
local 
48 
val Eq_FalseI = thm "Eq_FalseI" 

49 
val Eq_TrueI = thm "Eq_TrueI" 

50 
in fun mk_eq th = case concl_of th 

21163  51 
(*expects Trueprop if not == *) 
21551  52 
of Const ("==",_) $ _ $ _ => th 
53 
 _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th 

54 
 _ $ (Const ("Not", _) $ _) => th RS Eq_FalseI 

55 
 _ => th RS Eq_TrueI 

56 
end; 

21163  57 

21551  58 
local 
59 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" 

60 
val Eq_TrueI = thm "Eq_TrueI" 

61 
in fun mk_eq_True r = 

21163  62 
SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; 
21551  63 
end; 
21163  64 

65 
(* Produce theorems of the form 

66 
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) 

67 
*) 

21551  68 
local 
69 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" 

70 
val simp_implies_def = thm "simp_implies_def" 

71 
in fun lift_meta_eq_to_obj_eq i st = 

21163  72 
let 
73 
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q 

74 
 count_imp _ = 0; 

75 
val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i  1))) 

76 
in if j = 0 then meta_eq_to_obj_eq 

77 
else 

78 
let 

79 
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); 

80 
fun mk_simp_implies Q = foldr (fn (R, S) => 

81 
Const ("HOL.simp_implies", propT > propT > propT) $ R $ S) Q Ps 

82 
val aT = TFree ("'a", HOLogic.typeS); 

83 
val x = Free ("x", aT); 

84 
val y = Free ("y", aT) 

85 
in Goal.prove_global (Thm.theory_of_thm st) [] 

86 
[mk_simp_implies (Logic.mk_equals (x, y))] 

87 
(mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) 

88 
(fn prems => EVERY 

89 
[rewrite_goals_tac [simp_implies_def], 

90 
REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) 

91 
end 

92 
end; 

21551  93 
end; 
21163  94 

95 
(*Congruence rules for = (instead of ==)*) 

96 
fun mk_meta_cong rl = zero_var_indexes 

97 
(let val rl' = Seq.hd (TRYALL (fn i => fn st => 

98 
rtac (lift_meta_eq_to_obj_eq i st) i st) rl) 

99 
in mk_meta_eq rl' handle THM _ => 

100 
if can Logic.dest_equals (concl_of rl') then rl' 

101 
else error "Conclusion of congruence rules must be =equality" 

102 
end); 

103 

104 
fun mk_atomize pairs = 

105 
let 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

106 
fun atoms thm = 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

107 
let 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

108 
fun res th = map (fn rl => th RS rl); (*exception THM*) 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

109 
fun res_fixed rls = 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

110 
if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

111 
else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm]; 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

112 
in 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

113 
case concl_of thm 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

114 
of Const ("Trueprop", _) $ p => (case head_of p 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

115 
of Const (a, _) => (case AList.lookup (op =) pairs a 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

116 
of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

117 
 NONE => [thm]) 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

118 
 _ => [thm]) 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

119 
 _ => [thm] 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

120 
end; 
21163  121 
in atoms end; 
122 

123 
fun mksimps pairs = 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

124 
map_filter (try mk_eq) o mk_atomize pairs o gen_all; 
21163  125 

21551  126 
local 
127 
val simp_impliesI = thm "simp_impliesI" 

128 
val TrueI = thm "TrueI" 

129 
val FalseE = thm "FalseE" 

130 
val refl = thm "refl" 

131 
in fun unsafe_solver_tac prems = 

21163  132 
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' 
133 
FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE]; 

21551  134 
end; 
21163  135 
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; 
136 

137 
(*No premature instantiation of variables during simplification*) 

21551  138 
local 
139 
val simp_impliesI = thm "simp_impliesI" 

140 
val TrueI = thm "TrueI" 

141 
val FalseE = thm "FalseE" 

142 
val refl = thm "refl" 

143 
in fun safe_solver_tac prems = 

21163  144 
(fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' 
145 
FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems), 

146 
eq_assume_tac, ematch_tac [FalseE]]; 

21551  147 
end; 
21163  148 
val safe_solver = mk_solver "HOL safe" safe_solver_tac; 
149 

150 
structure SplitterData = 

151 
struct 

152 
structure Simplifier = Simplifier 

21551  153 
val mk_eq = mk_eq 
154 
val meta_eq_to_iff = thm "meta_eq_to_obj_eq" 

155 
val iffD = thm "iffD2" 

156 
val disjE = thm "disjE" 

157 
val conjE = thm "conjE" 

158 
val exE = thm "exE" 

159 
val contrapos = thm "contrapos_nn" 

160 
val contrapos2 = thm "contrapos_pp" 

161 
val notnotD = thm "notnotD" 

21163  162 
end; 
163 

164 
structure Splitter = SplitterFun(SplitterData); 

165 

21674  166 
val split_tac = Splitter.split_tac; 
167 
val split_inside_tac = Splitter.split_inside_tac; 

168 

169 
val op addsplits = Splitter.addsplits; 

170 
val op delsplits = Splitter.delsplits; 

171 
val Addsplits = Splitter.Addsplits; 

172 
val Delsplits = Splitter.Delsplits; 

173 

174 

21163  175 
(* integration of simplifier with classical reasoner *) 
176 

177 
structure Clasimp = ClasimpFun 

178 
(structure Simplifier = Simplifier and Splitter = Splitter 

179 
and Classical = Classical and Blast = Blast 

22128  180 
val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE"); 
21674  181 
open Clasimp; 
21163  182 

22128  183 
val _ = ML_Context.value_antiq "clasimpset" 
184 
(Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())")); 

185 

21163  186 
val mksimps_pairs = 
21551  187 
[("op >", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]), 
188 
("All", [thm "spec"]), ("True", []), ("False", []), 

189 
("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])]; 

21163  190 

21674  191 
val HOL_basic_ss = 
21163  192 
Simplifier.theory_context (the_context ()) empty_ss 
193 
setsubgoaler asm_simp_tac 

194 
setSSolver safe_solver 

195 
setSolver unsafe_solver 

196 
setmksimps (mksimps mksimps_pairs) 

197 
setmkeqTrue mk_eq_True 

198 
setmkcong mk_meta_cong; 

199 

21674  200 
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); 
21163  201 

202 
fun unfold_tac ths = 

21674  203 
let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths 
21163  204 
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; 
205 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

206 

26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

207 

21163  208 
(** simprocs **) 
209 

210 
(* simproc for proving "(y = x) == False" from premise "~(x = y)" *) 

211 

212 
val use_neq_simproc = ref true; 

213 

214 
local 

215 
val thy = the_context (); 

21551  216 
val neq_to_EQ_False = thm "not_sym" RS thm "Eq_FalseI"; 
21163  217 
fun neq_prover sg ss (eq $ lhs $ rhs) = 
218 
let 

219 
fun test thm = (case #prop (rep_thm thm) of 

220 
_ $ (Not $ (eq' $ l' $ r')) => 

221 
Not = HOLogic.Not andalso eq' = eq andalso 

222 
r' aconv lhs andalso l' aconv rhs 

223 
 _ => false) 

224 
in if !use_neq_simproc then case find_first test (prems_of_ss ss) 

225 
of NONE => NONE 

226 
 SOME thm => SOME (thm RS neq_to_EQ_False) 

227 
else NONE 

228 
end 

229 
in 

230 

231 
val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover; 

232 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

233 
end; 
21163  234 

235 

236 
(* simproc for Let *) 

237 

238 
val use_let_simproc = ref true; 

239 

240 
local 

241 
val thy = the_context (); 

242 
val Let_folded = thm "Let_folded"; 

243 
val Let_unfold = thm "Let_unfold"; 

21551  244 
val Let_def = thm "Let_def"; 
21163  245 
val (f_Let_unfold, x_Let_unfold) = 
246 
let val [(_$(f$x)$_)] = prems_of Let_unfold 

247 
in (cterm_of thy f, cterm_of thy x) end 

248 
val (f_Let_folded, x_Let_folded) = 

249 
let val [(_$(f$x)$_)] = prems_of Let_folded 

250 
in (cterm_of thy f, cterm_of thy x) end; 

251 
val g_Let_folded = 

252 
let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end; 

253 
in 

254 

255 
val let_simproc = 

256 
Simplifier.simproc thy "let_simp" ["Let x f"] 

257 
(fn sg => fn ss => fn t => 

258 
let val ctxt = Simplifier.the_context ss; 

259 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

260 
in Option.map (hd o Variable.export ctxt' ctxt o single) 

261 
(case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) 

262 
if not (!use_let_simproc) then NONE 

263 
else if is_Free x orelse is_Bound x orelse is_Const x 

21551  264 
then SOME Let_def 
21163  265 
else 
266 
let 

267 
val n = case f of (Abs (x,_,_)) => x  _ => "x"; 

268 
val cx = cterm_of sg x; 

269 
val {T=xT,...} = rep_cterm cx; 

270 
val cf = cterm_of sg f; 

271 
val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); 

272 
val (_$_$g) = prop_of fx_g; 

273 
val g' = abstract_over (x,g); 

274 
in (if (g aconv g') 

275 
then 

276 
let 

277 
val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold; 

278 
in SOME (rl OF [fx_g]) end 

279 
else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) 

280 
else let 

281 
val abs_g'= Abs (n,xT,g'); 

282 
val g'x = abs_g'$x; 

283 
val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x)); 

284 
val rl = cterm_instantiate 

285 
[(f_Let_folded,cterm_of sg f),(x_Let_folded,cx), 

286 
(g_Let_folded,cterm_of sg abs_g')] 

287 
Let_folded; 

288 
in SOME (rl OF [transitive fx_g g_g'x]) 

289 
end) 

290 
end 

291 
 _ => NONE) 

292 
end) 

293 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

294 
end; 
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

295 

21163  296 

297 
(* generic refutation procedure *) 

298 

299 
(* parameters: 

300 

301 
test: term > bool 

302 
tests if a term is at all relevant to the refutation proof; 

303 
if not, then it can be discarded. Can improve performance, 

304 
esp. if disjunctions can be discarded (no case distinction needed!). 

305 

306 
prep_tac: int > tactic 

307 
A preparation tactic to be applied to the goal once all relevant premises 

308 
have been moved to the conclusion. 

309 

310 
ref_tac: int > tactic 

311 
the actual refutation tactic. Should be able to deal with goals 

312 
[ A1; ...; An ] ==> False 

313 
where the Ai are atomic, i.e. no toplevel &,  or EX 

314 
*) 

315 

316 
local 

21551  317 
val conjE = thm "conjE" 
318 
val exE = thm "exE" 

319 
val disjE = thm "disjE" 

320 
val notE = thm "notE" 

321 
val rev_mp = thm "rev_mp" 

322 
val ccontr = thm "ccontr" 

21163  323 
val nnf_simpset = 
324 
empty_ss setmkeqTrue mk_eq_True 

325 
setmksimps (mksimps mksimps_pairs) 

326 
addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj", 

327 
thm "not_all", thm "not_ex", thm "not_not"]; 

328 
fun prem_nnf_tac i st = 

329 
full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; 

330 
in 

331 
fun refute_tac test prep_tac ref_tac = 

332 
let val refute_prems_tac = 

333 
REPEAT_DETERM 

334 
(eresolve_tac [conjE, exE] 1 ORELSE 

335 
filter_prems_tac test 1 ORELSE 

336 
etac disjE 1) THEN 

337 
((etac notE 1 THEN eq_assume_tac 1) ORELSE 

338 
ref_tac 1); 

339 
in EVERY'[TRY o filter_prems_tac test, 

340 
REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, 

341 
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] 

342 
end; 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

343 
end; 
21163  344 

345 
val defALL_regroup = 

346 
Simplifier.simproc (the_context ()) 

347 
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; 

348 

349 
val defEX_regroup = 

350 
Simplifier.simproc (the_context ()) 

351 
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; 

352 

353 

21674  354 
val simpset_simprocs = HOL_basic_ss 
21163  355 
addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc] 
356 

21313
26fc3a45547c
mk_atomize: careful matching against rules admits overloading;
wenzelm
parents:
21163
diff
changeset

357 
end; 
21551  358 

359 
structure Splitter = Simpdata.Splitter; 

360 
structure Clasimp = Simpdata.Clasimp; 