author  skalberg 
Sun, 04 Apr 2004 15:34:14 +0200  
changeset 14518  c3019a66180f 
parent 14516  a183dec876ab 
child 14620  1be590fd2422 
permissions  rwrr 
14516  1 
(* Title: Provers/shuffler.ML 
2 
ID: $Id$ 

3 
Author: Sebastian Skalberg, TU Muenchen 

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5 

6 
Package for proving two terms equal by normalizing (hence the 

7 
"shuffler" name). Uses the simplifier for the normalization. 

8 
*) 

9 

10 
signature Shuffler = 

11 
sig 

12 
val debug : bool ref 

13 

14 
val norm_term : theory > term > thm 

15 
val make_equal : theory > term > term > thm option 

16 
val set_prop : theory > term > (string * thm) list > (string * thm) option 

17 

18 
val find_potential: theory > term > (string * thm) list 

19 

20 
val gen_shuffle_tac: theory > bool > (string * thm) list > int > tactic 

21 

22 
val shuffle_tac: (string * thm) list > int > tactic 

23 
val search_tac : (string * thm) list > int > tactic 

24 

25 
val print_shuffles: theory > unit 

26 

27 
val add_shuffle_rule: thm > theory > theory 

28 
val shuffle_attr: theory attribute 

29 

30 
val setup : (theory > theory) list 

31 
end 

32 

33 
structure Shuffler :> Shuffler = 

34 
struct 

35 

36 
val debug = ref false 

37 

38 
fun if_debug f x = if !debug then f x else () 

39 
val message = if_debug writeln 

40 

41 
(*Prints exceptions readably to users*) 

42 
fun print_sign_exn_unit sign e = 

43 
case e of 

44 
THM (msg,i,thms) => 

45 
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); 

46 
seq print_thm thms) 

47 
 THEORY (msg,thys) => 

48 
(writeln ("Exception THEORY raised:\n" ^ msg); 

49 
seq (Pretty.writeln o Display.pretty_theory) thys) 

50 
 TERM (msg,ts) => 

51 
(writeln ("Exception TERM raised:\n" ^ msg); 

52 
seq (writeln o Sign.string_of_term sign) ts) 

53 
 TYPE (msg,Ts,ts) => 

54 
(writeln ("Exception TYPE raised:\n" ^ msg); 

55 
seq (writeln o Sign.string_of_typ sign) Ts; 

56 
seq (writeln o Sign.string_of_term sign) ts) 

57 
 e => raise e 

58 

59 
(*Prints an exception, then fails*) 

60 
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e) 

61 

62 
val string_of_thm = Library.setmp print_mode [] string_of_thm 

63 
val string_of_cterm = Library.setmp print_mode [] string_of_cterm 

64 

65 
val commafy = String.concat o separate ", " 

66 

67 
fun mk_meta_eq th = 

68 
(case concl_of th of 

69 
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection 

70 
 Const("==",_) $ _ $ _ => th 

71 
 _ => raise THM("Not an equality",0,[th])) 

72 
handle _ => raise THM("Couldn't make meta equality",0,[th]) 

73 

74 
fun mk_obj_eq th = 

75 
(case concl_of th of 

76 
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th 

77 
 Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq 

78 
 _ => raise THM("Not an equality",0,[th])) 

79 
handle _ => raise THM("Couldn't make object equality",0,[th]) 

80 

81 
structure ShuffleDataArgs: THEORY_DATA_ARGS = 

82 
struct 

83 
val name = "HOL/shuffles" 

84 
type T = thm list 

85 
val empty = [] 

86 
val copy = I 

87 
val prep_ext = I 

88 
val merge = Library.gen_union Thm.eq_thm 

89 
fun print sg thms = 

90 
Pretty.writeln (Pretty.big_list "Shuffle theorems:" 

91 
(map Display.pretty_thm thms)) 

92 
end 

93 

94 
structure ShuffleData = TheoryDataFun(ShuffleDataArgs) 

95 

96 
val weaken = 

97 
let 

98 
val cert = cterm_of (sign_of ProtoPure.thy) 

99 
val P = Free("P",propT) 

100 
val Q = Free("Q",propT) 

101 
val PQ = Logic.mk_implies(P,Q) 

102 
val PPQ = Logic.mk_implies(P,PQ) 

103 
val cP = cert P 

104 
val cQ = cert Q 

105 
val cPQ = cert PQ 

106 
val cPPQ = cert PPQ 

107 
val th1 = assume cPQ > implies_intr_list [cPQ,cP] 

108 
val th3 = assume cP 

109 
val th4 = implies_elim_list (assume cPPQ) [th3,th3] 

110 
> implies_intr_list [cPPQ,cP] 

111 
in 

112 
equal_intr th4 th1 > standard 

113 
end 

114 

115 
val imp_comm = 

116 
let 

117 
val cert = cterm_of (sign_of ProtoPure.thy) 

118 
val P = Free("P",propT) 

119 
val Q = Free("Q",propT) 

120 
val R = Free("R",propT) 

121 
val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R)) 

122 
val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R)) 

123 
val cP = cert P 

124 
val cQ = cert Q 

125 
val cPQR = cert PQR 

126 
val cQPR = cert QPR 

127 
val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ] 

128 
> implies_intr_list [cPQR,cQ,cP] 

129 
val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP] 

130 
> implies_intr_list [cQPR,cP,cQ] 

131 
in 

132 
equal_intr th1 th2 > standard 

133 
end 

134 

135 
val def_norm = 

136 
let 

137 
val cert = cterm_of (sign_of ProtoPure.thy) 

138 
val aT = TFree("'a",logicS) 

139 
val bT = TFree("'b",logicS) 

140 
val v = Free("v",aT) 

141 
val P = Free("P",aT>bT) 

142 
val Q = Free("Q",aT>bT) 

143 
val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) 

144 
val cPQ = cert (Logic.mk_equals(P,Q)) 

145 
val cv = cert v 

146 
val rew = assume cvPQ 

147 
> forall_elim cv 

148 
> abstract_rule "v" cv 

149 
val (lhs,rhs) = Logic.dest_equals(concl_of rew) 

150 
val th1 = transitive (transitive 

151 
(eta_conversion (cert lhs) > symmetric) 

152 
rew) 

153 
(eta_conversion (cert rhs)) 

154 
> implies_intr cvPQ 

155 
val th2 = combination (assume cPQ) (reflexive cv) 

156 
> forall_intr cv 

157 
> implies_intr cPQ 

158 
in 

159 
equal_intr th1 th2 > standard 

160 
end 

161 

162 
val all_comm = 

163 
let 

164 
val cert = cterm_of (sign_of ProtoPure.thy) 

165 
val xT = TFree("'a",logicS) 

166 
val yT = TFree("'b",logicS) 

167 
val P = Free("P",xT>yT>propT) 

168 
val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0)))) 

169 
val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1)))) 

170 
val cl = cert lhs 

171 
val cr = cert rhs 

172 
val cx = cert (Free("x",xT)) 

173 
val cy = cert (Free("y",yT)) 

174 
val th1 = assume cr 

175 
> forall_elim_list [cy,cx] 

176 
> forall_intr_list [cx,cy] 

177 
> implies_intr cr 

178 
val th2 = assume cl 

179 
> forall_elim_list [cx,cy] 

180 
> forall_intr_list [cy,cx] 

181 
> implies_intr cl 

182 
in 

183 
equal_intr th1 th2 > standard 

184 
end 

185 

186 
val equiv_comm = 

187 
let 

188 
val cert = cterm_of (sign_of ProtoPure.thy) 

189 
val T = TFree("'a",[]) 

190 
val t = Free("t",T) 

191 
val u = Free("u",T) 

192 
val ctu = cert (Logic.mk_equals(t,u)) 

193 
val cut = cert (Logic.mk_equals(u,t)) 

194 
val th1 = assume ctu > symmetric > implies_intr ctu 

195 
val th2 = assume cut > symmetric > implies_intr cut 

196 
in 

197 
equal_intr th1 th2 > standard 

198 
end 

199 

200 
(* This simplification procedure rewrites !!x y. P x y 

201 
deterministicly, in order for the normalization function, defined 

202 
below, to handle nested quantifiers robustly *) 

203 

204 
local 

205 

206 
exception RESULT of int 

207 

208 
fun find_bound n (Bound i) = if i = n then raise RESULT 0 

209 
else if i = n+1 then raise RESULT 1 

210 
else () 

211 
 find_bound n (t $ u) = (find_bound n t; find_bound n u) 

212 
 find_bound n (Abs(_,_,t)) = find_bound (n+1) t 

213 
 find_bound _ _ = () 

214 

215 
fun swap_bound n (Bound i) = if i = n then Bound (n+1) 

216 
else if i = n+1 then Bound n 

217 
else Bound i 

218 
 swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u) 

219 
 swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t) 

220 
 swap_bound n t = t 

221 

222 
fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t = 

223 
let 

224 
val lhs = list_all ([xv,yv],t) 

225 
val rhs = list_all ([yv,xv],swap_bound 0 t) 

226 
val rew = Logic.mk_equals (lhs,rhs) 

227 
val init = trivial (cterm_of sg rew) 

228 
in 

229 
(all_comm RS init handle e => (message "rew_th"; print_exn e)) 

230 
end 

231 

232 
fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = 

233 
let 

234 
val res = (find_bound 0 body;2) handle RESULT i => i 

235 
in 

236 
case res of 

237 
0 => Some (rew_th sg (x,xT) (y,yT) body) 

238 
 1 => if string_ord(y,x) = LESS 

239 
then 

240 
let 

241 
val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body))) 

242 
val t_th = reflexive (cterm_of sg t) 

243 
val newt_th = reflexive (cterm_of sg newt) 

244 
in 

245 
Some (transitive t_th newt_th) 

246 
end 

247 
else None 

248 
 _ => error "norm_term (quant_rewrite) internal error" 

249 
end 

250 
 quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; None) 

251 

252 
fun freeze_thaw_term t = 

253 
let 

254 
val tvars = term_tvars t 

255 
val tfree_names = add_term_tfree_names(t,[]) 

256 
val (type_inst,_) = 

257 
foldl (fn ((inst,used),(w as (v,_),S)) => 

258 
let 

259 
val v' = variant used v 

260 
in 

261 
((w,TFree(v',S))::inst,v'::used) 

262 
end) 

263 
(([],tfree_names),tvars) 

264 
val t' = subst_TVars type_inst t 

265 
in 

14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

266 
(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S)) 
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

267 
 _ => error "Internal error in Shuffler.freeze_thaw") type_inst) 
14516  268 
end 
269 

270 
fun inst_tfrees sg [] thm = thm 

271 
 inst_tfrees sg ((name,U)::rest) thm = 

272 
let 

273 
val cU = ctyp_of sg U 

274 
val tfree_names = add_term_tfree_names (prop_of thm,[]) 

275 
val (thm',rens) = varifyT' (tfree_names \ name) thm 

276 
val mid = 

277 
case rens of 

278 
[] => thm' 

279 
 [(_,idx)] => instantiate ([(idx,cU)],[]) thm' 

280 
 _ => error "Shuffler.inst_tfrees internal error" 

281 
in 

282 
inst_tfrees sg rest mid 

283 
end 

284 

285 
fun is_Abs (Abs _) = true 

286 
 is_Abs _ = false 

287 

288 
fun eta_redex (t $ Bound 0) = 

289 
let 

290 
fun free n (Bound i) = i = n 

291 
 free n (t $ u) = free n t orelse free n u 

292 
 free n (Abs(_,_,t)) = free (n+1) t 

293 
 free n _ = false 

294 
in 

295 
not (free 0 t) 

296 
end 

297 
 eta_redex _ = false 

298 

299 
fun eta_contract sg assumes origt = 

300 
let 

301 
val (typet,Tinst) = freeze_thaw_term origt 

302 
val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet)) 

303 
val final = inst_tfrees sg Tinst o thaw 

304 
val t = #1 (Logic.dest_equals (prop_of init)) 

305 
val _ = 

306 
let 

307 
val lhs = #1 (Logic.dest_equals (prop_of (final init))) 

308 
in 

309 
if not (lhs aconv origt) 

310 
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; 

311 
writeln (string_of_cterm (cterm_of sg origt)); 

312 
writeln (string_of_cterm (cterm_of sg lhs)); 

313 
writeln (string_of_cterm (cterm_of sg typet)); 

314 
writeln (string_of_cterm (cterm_of sg t)); 

315 
app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst; 

316 
writeln "done") 

317 
else () 

318 
end 

319 
in 

320 
case t of 

321 
Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => 

322 
((if eta_redex P andalso eta_redex Q 

323 
then 

324 
let 

325 
val cert = cterm_of sg 

326 
val v = Free(variant (add_term_free_names(t,[])) "v",xT) 

327 
val cv = cert v 

328 
val ct = cert t 

329 
val th = (assume ct) 

330 
> forall_elim cv 

331 
> abstract_rule x cv 

332 
val ext_th = eta_conversion (cert (Abs(x,xT,P))) 

333 
val th' = transitive (symmetric ext_th) th 

334 
val cu = cert (prop_of th') 

335 
val uth = combination (assume cu) (reflexive cv) 

336 
val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v))) 

337 
> transitive uth 

338 
> forall_intr cv 

339 
> implies_intr cu 

340 
val rew_th = equal_intr (th' > implies_intr ct) uth' 

341 
val res = final rew_th 

342 
val lhs = (#1 (Logic.dest_equals (prop_of res))) 

343 
in 

344 
Some res 

345 
end 

346 
else None) 

347 
handle e => (writeln "eta_contract:";print_exn e)) 

348 
 _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); None) 

349 
end 

350 

351 
fun beta_fun sg assume t = 

352 
Some (beta_conversion true (cterm_of sg t)) 

353 

354 
fun eta_expand sg assumes origt = 

355 
let 

356 
val (typet,Tinst) = freeze_thaw_term origt 

357 
val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet)) 

358 
val final = inst_tfrees sg Tinst o thaw 

359 
val t = #1 (Logic.dest_equals (prop_of init)) 

360 
val _ = 

361 
let 

362 
val lhs = #1 (Logic.dest_equals (prop_of (final init))) 

363 
in 

364 
if not (lhs aconv origt) 

365 
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; 

366 
writeln (string_of_cterm (cterm_of sg origt)); 

367 
writeln (string_of_cterm (cterm_of sg lhs)); 

368 
writeln (string_of_cterm (cterm_of sg typet)); 

369 
writeln (string_of_cterm (cterm_of sg t)); 

370 
app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst; 

371 
writeln "done") 

372 
else () 

373 
end 

374 
in 

375 
case t of 

376 
Const("==",T) $ P $ Q => 

377 
if is_Abs P orelse is_Abs Q 

378 
then (case domain_type T of 

379 
Type("fun",[aT,bT]) => 

380 
let 

381 
val cert = cterm_of sg 

382 
val vname = variant (add_term_free_names(t,[])) "v" 

383 
val v = Free(vname,aT) 

384 
val cv = cert v 

385 
val ct = cert t 

386 
val th1 = (combination (assume ct) (reflexive cv)) 

387 
> forall_intr cv 

388 
> implies_intr ct 

389 
val concl = cert (concl_of th1) 

390 
val th2 = (assume concl) 

391 
> forall_elim cv 

392 
> abstract_rule vname cv 

393 
val (lhs,rhs) = Logic.dest_equals (prop_of th2) 

394 
val elhs = eta_conversion (cert lhs) 

395 
val erhs = eta_conversion (cert rhs) 

396 
val th2' = transitive 

397 
(transitive (symmetric elhs) th2) 

398 
erhs 

399 
val res = equal_intr th1 (th2' > implies_intr concl) 

400 
val res' = final res 

401 
in 

402 
Some res' 

403 
end 

404 
 _ => None) 

405 
else None 

406 
 _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); None) 

407 
end 

408 
handle e => (writeln "eta_expand internal error";print_exn e) 

409 

410 
fun mk_tfree s = TFree("'"^s,logicS) 

411 
val xT = mk_tfree "a" 

412 
val yT = mk_tfree "b" 

413 
val P = Var(("P",0),xT>yT>propT) 

414 
val Q = Var(("Q",0),xT>yT) 

415 
val R = Var(("R",0),xT>yT) 

416 
val S = Var(("S",0),xT) 

417 
in 

418 
fun beta_simproc sg = Simplifier.simproc_i 

419 
sg 

420 
"Betacontraction" 

421 
[Abs("x",xT,Q) $ S] 

422 
beta_fun 

423 

424 
fun quant_simproc sg = Simplifier.simproc_i 

425 
sg 

426 
"Ordered rewriting of nested quantifiers" 

427 
[all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))] 

428 
quant_rewrite 

429 
fun eta_expand_simproc sg = Simplifier.simproc_i 

430 
sg 

431 
"Smart etaexpansion by equivalences" 

432 
[Logic.mk_equals(Q,R)] 

433 
eta_expand 

434 
fun eta_contract_simproc sg = Simplifier.simproc_i 

435 
sg 

436 
"Smart handling of etacontractions" 

437 
[all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))] 

438 
eta_contract 

439 
end 

440 

441 
(* Disambiguates the names of bound variables in a term, returning t 

442 
== t' where all the names of bound variables in t' are unique *) 

443 

444 
fun disamb_bound sg t = 

445 
let 

446 

447 
fun F (t $ u,idx) = 

448 
let 

449 
val (t',idx') = F (t,idx) 

450 
val (u',idx'') = F (u,idx') 

451 
in 

452 
(t' $ u',idx'') 

453 
end 

454 
 F (Abs(x,xT,t),idx) = 

455 
let 

456 
val x' = "x" ^ (LargeInt.toString idx) (* amazing *) 

457 
val (t',idx') = F (t,idx+1) 

458 
in 

459 
(Abs(x',xT,t'),idx') 

460 
end 

461 
 F arg = arg 

462 
val (t',_) = F (t,0) 

463 
val ct = cterm_of sg t 

464 
val ct' = cterm_of sg t' 

465 
val res = transitive (reflexive ct) (reflexive ct') 

466 
val _ = message ("disamb_term: " ^ (string_of_thm res)) 

467 
in 

468 
res 

469 
end 

470 

471 
(* Transforms a term t to some normal form t', returning the theorem t 

472 
== t'. This is originally a help function for make_equal, but might 

473 
be handy in its own right, for example for indexing terms. *) 

474 

475 
fun norm_term thy t = 

476 
let 

477 
val sg = sign_of thy 

478 

479 
val norms = ShuffleData.get thy 

480 
val ss = empty_ss setmksimps single 

481 
addsimps (map (transfer_sg sg) norms) 

482 
fun chain f th = 

483 
let 

484 
val rhs = snd (dest_equals (cprop_of th)) 

485 
in 

486 
transitive th (f rhs) 

487 
end 

488 

489 
val th = 

490 
t > disamb_bound sg 

491 
> chain (Simplifier.full_rewrite 

492 
(ss addsimprocs [quant_simproc sg,eta_expand_simproc sg,eta_contract_simproc sg])) 

493 
> chain eta_conversion 

494 
> strip_shyps 

495 
val _ = message ("norm_term: " ^ (string_of_thm th)) 

496 
in 

497 
th 

498 
end 

499 
handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e) 

500 

501 
fun is_logic_var sg v = 

502 
Type.of_sort (Sign.tsig_of sg) (type_of v,logicS) 

503 

504 
(* Closes a theorem with respect to free and schematic variables (does 

505 
not touch type variables, though). *) 

506 

507 
fun close_thm th = 

508 
let 

509 
val sg = sign_of_thm th 

510 
val c = prop_of th 

511 
val all_vars = add_term_frees (c,add_term_vars(c,[])) 

512 
val all_rel_vars = filter (is_logic_var sg) all_vars 

513 
in 

514 
Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th 

515 
end 

516 
handle e => (writeln "close_thm internal error"; print_exn e) 

517 

518 
(* Normalizes a theorem's conclusion using norm_term. *) 

519 

520 
fun norm_thm thy th = 

521 
let 

522 
val c = prop_of th 

523 
in 

524 
equal_elim (norm_term thy c) th 

525 
end 

526 

527 
(* make_equal sg t u tries to construct the theorem t == u under the 

528 
signature sg. If it succeeds, Some (t == u) is returned, otherwise 

529 
None is returned. *) 

530 

531 
fun make_equal sg t u = 

532 
let 

533 
val t_is_t' = norm_term sg t 

534 
val u_is_u' = norm_term sg u 

535 
val th = transitive t_is_t' (symmetric u_is_u') 

536 
val _ = message ("make_equal: Some " ^ (string_of_thm th)) 

537 
in 

538 
Some th 

539 
end 

540 
handle e as THM _ => (message "make_equal: None";None) 

541 

542 
fun match_consts ignore t (* th *) = 

543 
let 

544 
fun add_consts (Const (c, _), cs) = 

545 
if c mem_string ignore 

546 
then cs 

547 
else c ins_string cs 

548 
 add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) 

549 
 add_consts (Abs (_, _, t), cs) = add_consts (t, cs) 

550 
 add_consts (_, cs) = cs 

551 
val t_consts = add_consts(t,[]) 

552 
in 

553 
fn (name,th) => 

554 
let 

555 
val th_consts = add_consts(prop_of th,[]) 

556 
in 

557 
eq_set(t_consts,th_consts) 

558 
end 

559 
end 

560 

561 
val collect_ignored = 

562 
foldr (fn (thm,cs) => 

563 
let 

564 
val (lhs,rhs) = Logic.dest_equals (prop_of thm) 

565 
val ignore_lhs = term_consts lhs \\ term_consts rhs 

566 
val ignore_rhs = term_consts rhs \\ term_consts lhs 

567 
in 

568 
foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs) 

569 
end) 

570 

571 
(* set_prop t thms tries to make a theorem with the proposition t from 

572 
one of the theorems thms, by shuffling the propositions around. If it 

573 
succeeds, Some theorem is returned, otherwise None. *) 

574 

575 
fun set_prop thy t = 

576 
let 

577 
val sg = sign_of thy 

578 
val all_vars = add_term_frees (t,add_term_vars (t,[])) 

579 
val all_rel_vars = filter (is_logic_var sg) all_vars 

580 
val closed_t = foldr (fn (v,body) => let val vT = type_of v 

581 
in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t) 

582 
val rew_th = norm_term thy closed_t 

583 
val rhs = snd (dest_equals (cprop_of rew_th)) 

584 

585 
val shuffles = ShuffleData.get thy 

586 
fun process [] = None 

587 
 process ((name,th)::thms) = 

588 
let 

589 
val norm_th = varifyT (norm_thm thy (close_thm (transfer_sg sg th))) 

590 
val triv_th = trivial rhs 

591 
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) 

592 
val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of 

593 
Some(th,_) => Some th 

594 
 None => None 

595 
in 

596 
case mod_th of 

597 
Some mod_th => 

598 
let 

599 
val closed_th = equal_elim (symmetric rew_th) mod_th 

600 
in 

601 
message ("Shuffler.set_prop succeeded by " ^ name); 

602 
Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th) 

603 
end 

604 
 None => process thms 

605 
end 

606 
handle e as THM _ => process thms 

607 
in 

608 
fn thms => 

609 
case process thms of 

610 
res as Some (name,th) => if (prop_of th) aconv t 

611 
then res 

612 
else error "Internal error in set_prop" 

613 
 None => None 

614 
end 

615 
handle e => (writeln "set_prop internal error"; print_exn e) 

616 

617 
fun find_potential thy t = 

618 
let 

619 
val shuffles = ShuffleData.get thy 

620 
val ignored = collect_ignored(shuffles,[]) 

621 
val rel_consts = term_consts t \\ ignored 

622 
val pot_thms = PureThy.thms_containing_consts thy rel_consts 

623 
in 

624 
filter (match_consts ignored t) pot_thms 

625 
end 

626 

627 
fun gen_shuffle_tac thy search thms i st = 

628 
let 

629 
val _ = message ("Shuffling " ^ (string_of_thm st)) 

630 
val t = nth_elem(i1,prems_of st) 

631 
val set = set_prop thy t 

632 
fun process_tac thms st = 

633 
case set thms of 

634 
Some (_,th) => Seq.of_list (compose (th,i,st)) 

635 
 None => Seq.empty 

636 
in 

637 
(process_tac thms APPEND (if search 

638 
then process_tac (find_potential thy t) 

639 
else no_tac)) st 

640 
end 

641 

642 
fun shuffle_tac thms i st = 

643 
gen_shuffle_tac (the_context()) false thms i st 

644 

645 
fun search_tac thms i st = 

646 
gen_shuffle_tac (the_context()) true thms i st 

647 

648 
fun shuffle_meth (thms:thm list) ctxt = 

649 
let 

650 
val thy = ProofContext.theory_of ctxt 

651 
in 

652 
Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy false (map (pair "") thms)) 

653 
end 

654 

655 
fun search_meth ctxt = 

656 
let 

657 
val thy = ProofContext.theory_of ctxt 

658 
val prems = ProofContext.prems_of ctxt 

659 
in 

660 
Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems)) 

661 
end 

662 

663 
val print_shuffles = ShuffleData.print 

664 

665 
fun add_shuffle_rule thm thy = 

666 
let 

667 
val shuffles = ShuffleData.get thy 

668 
in 

669 
if exists (curry Thm.eq_thm thm) shuffles 

670 
then (warning ((string_of_thm thm) ^ " already known to the shuffler"); 

671 
thy) 

672 
else ShuffleData.put (thm::shuffles) thy 

673 
end 

674 

675 
fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm) 

676 

677 
val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"), 

678 
Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"), 

679 
ShuffleData.init, 

680 
add_shuffle_rule weaken, 

681 
add_shuffle_rule equiv_comm, 

682 
add_shuffle_rule imp_comm, 

683 
add_shuffle_rule Drule.norm_hhf_eq, 

684 
add_shuffle_rule Drule.triv_forall_equality, 

685 
Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]] 

686 
end 