author  wenzelm 
Mon, 23 Jun 2008 23:45:39 +0200  
changeset 27330  1af2598b5f7d 
parent 27173  9ae98c3cd3d6 
child 27865  27a8ad9612a3 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

1 
(* Title: HOL/Import/shuffler.ML 
14516  2 
ID: $Id$ 
3 
Author: Sebastian Skalberg, TU Muenchen 

4 

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

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

7 
*) 

8 

9 
signature Shuffler = 

10 
sig 

11 
val debug : bool ref 

12 

13 
val norm_term : theory > term > thm 

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

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

16 

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

18 

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

20 

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

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

23 

24 
val print_shuffles: theory > unit 

25 

26 
val add_shuffle_rule: thm > theory > theory 

18728  27 
val shuffle_attr: attribute 
14516  28 

18708  29 
val setup : theory > theory 
14516  30 
end 
31 

32 
structure Shuffler :> Shuffler = 

33 
struct 

34 

35 
val debug = ref false 

36 

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

38 
val message = if_debug writeln 

39 

40 
(*Prints exceptions readably to users*) 

21588  41 
fun print_sign_exn_unit sign e = 
14516  42 
case e of 
43 
THM (msg,i,thms) => 

21588  44 
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); 
26928  45 
List.app Display.print_thm thms) 
14516  46 
 THEORY (msg,thys) => 
21588  47 
(writeln ("Exception THEORY raised:\n" ^ msg); 
48 
List.app (writeln o Context.str_of_thy) thys) 

14516  49 
 TERM (msg,ts) => 
21588  50 
(writeln ("Exception TERM raised:\n" ^ msg); 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset

51 
List.app (writeln o Syntax.string_of_term_global sign) ts) 
14516  52 
 TYPE (msg,Ts,ts) => 
21588  53 
(writeln ("Exception TYPE raised:\n" ^ msg); 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset

54 
List.app (writeln o Syntax.string_of_typ_global sign) Ts; 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset

55 
List.app (writeln o Syntax.string_of_term_global sign) ts) 
14516  56 
 e => raise e 
57 

58 
(*Prints an exception, then fails*) 

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

60 

26928  61 
val string_of_thm = PrintMode.setmp [] Display.string_of_thm; 
62 
val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm; 

14516  63 

64 
fun mk_meta_eq th = 

65 
(case concl_of th of 

21588  66 
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection 
14516  67 
 Const("==",_) $ _ $ _ => th 
68 
 _ => raise THM("Not an equality",0,[th])) 

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

21588  70 

14516  71 
fun mk_obj_eq th = 
72 
(case concl_of th of 

21588  73 
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th 
14516  74 
 Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq 
75 
 _ => raise THM("Not an equality",0,[th])) 

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

77 

22846  78 
structure ShuffleData = TheoryDataFun 
79 
( 

80 
type T = thm list 

81 
val empty = [] 

82 
val copy = I 

83 
val extend = I 

84 
fun merge _ = Library.gen_union Thm.eq_thm 

85 
) 

14516  86 

22846  87 
fun print_shuffles thy = 
88 
Pretty.writeln (Pretty.big_list "Shuffle theorems:" 

89 
(map Display.pretty_thm (ShuffleData.get thy))) 

14516  90 

91 
val weaken = 

92 
let 

26424  93 
val cert = cterm_of Pure.thy 
21588  94 
val P = Free("P",propT) 
95 
val Q = Free("Q",propT) 

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

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

98 
val cP = cert P 

99 
val cQ = cert Q 

100 
val cPQ = cert PQ 

101 
val cPPQ = cert PPQ 

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

103 
val th3 = assume cP 

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

105 
> implies_intr_list [cPPQ,cP] 

14516  106 
in 
21588  107 
equal_intr th4 th1 > standard 
14516  108 
end 
109 

110 
val imp_comm = 

111 
let 

26424  112 
val cert = cterm_of Pure.thy 
21588  113 
val P = Free("P",propT) 
114 
val Q = Free("Q",propT) 

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

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

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

118 
val cP = cert P 

119 
val cQ = cert Q 

120 
val cPQR = cert PQR 

121 
val cQPR = cert QPR 

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

123 
> implies_intr_list [cPQR,cQ,cP] 

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

125 
> implies_intr_list [cQPR,cP,cQ] 

14516  126 
in 
21588  127 
equal_intr th1 th2 > standard 
14516  128 
end 
129 

130 
val def_norm = 

131 
let 

26424  132 
val cert = cterm_of Pure.thy 
21588  133 
val aT = TFree("'a",[]) 
134 
val bT = TFree("'b",[]) 

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

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

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

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

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

140 
val cv = cert v 

141 
val rew = assume cvPQ 

142 
> forall_elim cv 

143 
> abstract_rule "v" cv 

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

145 
val th1 = transitive (transitive 

146 
(eta_conversion (cert lhs) > symmetric) 

147 
rew) 

148 
(eta_conversion (cert rhs)) 

149 
> implies_intr cvPQ 

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

151 
> forall_intr cv 

152 
> implies_intr cPQ 

14516  153 
in 
21588  154 
equal_intr th1 th2 > standard 
14516  155 
end 
156 

157 
val all_comm = 

158 
let 

26424  159 
val cert = cterm_of Pure.thy 
21588  160 
val xT = TFree("'a",[]) 
161 
val yT = TFree("'b",[]) 

27330  162 
val x = Free("x",xT) 
163 
val y = Free("y",yT) 

21588  164 
val P = Free("P",xT>yT>propT) 
27330  165 
val lhs = Logic.all x (Logic.all y (P $ x $ y)) 
166 
val rhs = Logic.all y (Logic.all x (P $ x $ y)) 

21588  167 
val cl = cert lhs 
168 
val cr = cert rhs 

27330  169 
val cx = cert x 
170 
val cy = cert y 

21588  171 
val th1 = assume cr 
172 
> forall_elim_list [cy,cx] 

173 
> forall_intr_list [cx,cy] 

174 
> implies_intr cr 

175 
val th2 = assume cl 

176 
> forall_elim_list [cx,cy] 

177 
> forall_intr_list [cy,cx] 

178 
> implies_intr cl 

14516  179 
in 
21588  180 
equal_intr th1 th2 > standard 
14516  181 
end 
182 

183 
val equiv_comm = 

184 
let 

26424  185 
val cert = cterm_of Pure.thy 
21588  186 
val T = TFree("'a",[]) 
187 
val t = Free("t",T) 

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

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

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

191 
val th1 = assume ctu > symmetric > implies_intr ctu 

192 
val th2 = assume cut > symmetric > implies_intr cut 

14516  193 
in 
21588  194 
equal_intr th1 th2 > standard 
14516  195 
end 
196 

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

198 
deterministicly, in order for the normalization function, defined 

199 
below, to handle nested quantifiers robustly *) 

200 

201 
local 

202 

203 
exception RESULT of int 

204 

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

21588  206 
else if i = n+1 then raise RESULT 1 
207 
else () 

14516  208 
 find_bound n (t $ u) = (find_bound n t; find_bound n u) 
209 
 find_bound n (Abs(_,_,t)) = find_bound (n+1) t 

210 
 find_bound _ _ = () 

211 

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

21588  213 
else if i = n+1 then Bound n 
214 
else Bound i 

14516  215 
 swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u) 
216 
 swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t) 

217 
 swap_bound n t = t 

218 

21078  219 
fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t = 
14516  220 
let 
21588  221 
val lhs = list_all ([xv,yv],t) 
222 
val rhs = list_all ([yv,xv],swap_bound 0 t) 

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

224 
val init = trivial (cterm_of thy rew) 

14516  225 
in 
21588  226 
(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e)) 
14516  227 
end 
228 

21078  229 
fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = 
14516  230 
let 
21588  231 
val res = (find_bound 0 body;2) handle RESULT i => i 
14516  232 
in 
21588  233 
case res of 
234 
0 => SOME (rew_th thy (x,xT) (y,yT) body) 

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

236 
then 

237 
let 

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

239 
val t_th = reflexive (cterm_of thy t) 

240 
val newt_th = reflexive (cterm_of thy newt) 

241 
in 

242 
SOME (transitive t_th newt_th) 

243 
end 

244 
else NONE 

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

14516  246 
end 
15531  247 
 quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE) 
14516  248 

249 
fun freeze_thaw_term t = 

250 
let 

21588  251 
val tvars = term_tvars t 
252 
val tfree_names = add_term_tfree_names(t,[]) 

253 
val (type_inst,_) = 

254 
Library.foldl (fn ((inst,used),(w as (v,_),S)) => 

255 
let 

256 
val v' = Name.variant used v 

257 
in 

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

259 
end) 

260 
(([],tfree_names),tvars) 

261 
val t' = subst_TVars type_inst t 

14516  262 
in 
21588  263 
(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S)) 
264 
 _ => error "Internal error in Shuffler.freeze_thaw") type_inst) 

14516  265 
end 
266 

21078  267 
fun inst_tfrees thy [] thm = thm 
21588  268 
 inst_tfrees thy ((name,U)::rest) thm = 
14516  269 
let 
21588  270 
val cU = ctyp_of thy U 
271 
val tfrees = add_term_tfrees (prop_of thm,[]) 

272 
val (rens, thm') = Thm.varifyT' 

20951
868120282837
gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents:
20897
diff
changeset

273 
(remove (op = o apsnd fst) name tfrees) thm 
21588  274 
val mid = 
275 
case rens of 

276 
[] => thm' 

277 
 [((_, S), idx)] => instantiate 

21078  278 
([(ctyp_of thy (TVar (idx, S)), cU)], []) thm' 
21588  279 
 _ => error "Shuffler.inst_tfrees internal error" 
14516  280 
in 
21588  281 
inst_tfrees thy rest mid 
14516  282 
end 
283 

284 
fun is_Abs (Abs _) = true 

285 
 is_Abs _ = false 

286 

287 
fun eta_redex (t $ Bound 0) = 

288 
let 

21588  289 
fun free n (Bound i) = i = n 
290 
 free n (t $ u) = free n t orelse free n u 

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

292 
 free n _ = false 

14516  293 
in 
21588  294 
not (free 0 t) 
14516  295 
end 
296 
 eta_redex _ = false 

297 

21078  298 
fun eta_contract thy assumes origt = 
14516  299 
let 
21588  300 
val (typet,Tinst) = freeze_thaw_term origt 
301 
val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet)) 

302 
val final = inst_tfrees thy Tinst o thaw 

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

304 
val _ = 

305 
let 

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

307 
in 

308 
if not (lhs aconv origt) 

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

26928  310 
writeln (Display.string_of_cterm (cterm_of thy origt)); 
311 
writeln (Display.string_of_cterm (cterm_of thy lhs)); 

312 
writeln (Display.string_of_cterm (cterm_of thy typet)); 

313 
writeln (Display.string_of_cterm (cterm_of thy t)); 

314 
app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; 

21588  315 
writeln "done") 
316 
else () 

317 
end 

14516  318 
in 
21588  319 
case t of 
320 
Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => 

321 
((if eta_redex P andalso eta_redex Q 

322 
then 

323 
let 

324 
val cert = cterm_of thy 

325 
val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT) 

326 
val cv = cert v 

327 
val ct = cert t 

328 
val th = (assume ct) 

329 
> forall_elim cv 

330 
> abstract_rule x cv 

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

332 
val th' = transitive (symmetric ext_th) th 

333 
val cu = cert (prop_of th') 

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

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

336 
> transitive uth 

337 
> forall_intr cv 

338 
> implies_intr cu 

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

340 
val res = final rew_th 

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

342 
in 

343 
SOME res 

344 
end 

345 
else NONE) 

346 
handle e => OldGoals.print_exn e) 

347 
 _ => NONE 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17188
diff
changeset

348 
end 
14516  349 

21078  350 
fun beta_fun thy assume t = 
351 
SOME (beta_conversion true (cterm_of thy t)) 

14516  352 

17188  353 
val meta_sym_rew = thm "refl" 
354 

21078  355 
fun equals_fun thy assume t = 
17188  356 
case t of 
21588  357 
Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE 
17188  358 
 _ => NONE 
359 

21078  360 
fun eta_expand thy assumes origt = 
14516  361 
let 
21588  362 
val (typet,Tinst) = freeze_thaw_term origt 
363 
val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet)) 

364 
val final = inst_tfrees thy Tinst o thaw 

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

366 
val _ = 

367 
let 

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

369 
in 

370 
if not (lhs aconv origt) 

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

26928  372 
writeln (Display.string_of_cterm (cterm_of thy origt)); 
373 
writeln (Display.string_of_cterm (cterm_of thy lhs)); 

374 
writeln (Display.string_of_cterm (cterm_of thy typet)); 

375 
writeln (Display.string_of_cterm (cterm_of thy t)); 

376 
app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst; 

21588  377 
writeln "done") 
378 
else () 

379 
end 

14516  380 
in 
21588  381 
case t of 
382 
Const("==",T) $ P $ Q => 

383 
if is_Abs P orelse is_Abs Q 

384 
then (case domain_type T of 

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

386 
let 

387 
val cert = cterm_of thy 

388 
val vname = Name.variant (add_term_free_names(t,[])) "v" 

389 
val v = Free(vname,aT) 

390 
val cv = cert v 

391 
val ct = cert t 

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

393 
> forall_intr cv 

394 
> implies_intr ct 

395 
val concl = cert (concl_of th1) 

396 
val th2 = (assume concl) 

397 
> forall_elim cv 

398 
> abstract_rule vname cv 

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

400 
val elhs = eta_conversion (cert lhs) 

401 
val erhs = eta_conversion (cert rhs) 

402 
val th2' = transitive 

403 
(transitive (symmetric elhs) th2) 

404 
erhs 

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

406 
val res' = final res 

407 
in 

408 
SOME res' 

409 
end 

410 
 _ => NONE) 

411 
else NONE 

412 
 _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE) 

14516  413 
end 
17959  414 
handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e) 
14516  415 

14854  416 
fun mk_tfree s = TFree("'"^s,[]) 
20326  417 
fun mk_free s t = Free (s,t) 
14516  418 
val xT = mk_tfree "a" 
419 
val yT = mk_tfree "b" 

27330  420 
val x = Free ("x", xT) 
421 
val y = Free ("y", yT) 

20326  422 
val P = mk_free "P" (xT>yT>propT) 
423 
val Q = mk_free "Q" (xT>yT) 

424 
val R = mk_free "R" (xT>yT) 

425 
val S = mk_free "S" xT 

426 
val S' = mk_free "S'" xT 

14516  427 
in 
21078  428 
fun beta_simproc thy = Simplifier.simproc_i 
21588  429 
thy 
430 
"Betacontraction" 

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

432 
beta_fun 

14516  433 

21078  434 
fun equals_simproc thy = Simplifier.simproc_i 
21588  435 
thy 
436 
"Ordered rewriting of meta equalities" 

437 
[Const("op ==",xT) $ S $ S'] 

438 
equals_fun 

17188  439 

21078  440 
fun quant_simproc thy = Simplifier.simproc_i 
21588  441 
thy 
442 
"Ordered rewriting of nested quantifiers" 

27330  443 
[Logic.all x (Logic.all y (P $ x $ y))] 
21588  444 
quant_rewrite 
21078  445 
fun eta_expand_simproc thy = Simplifier.simproc_i 
21588  446 
thy 
447 
"Smart etaexpansion by equivalences" 

448 
[Logic.mk_equals(Q,R)] 

449 
eta_expand 

21078  450 
fun eta_contract_simproc thy = Simplifier.simproc_i 
21588  451 
thy 
452 
"Smart handling of etacontractions" 

27330  453 
[Logic.all x (Logic.mk_equals (Q $ x, R $ x))] 
21588  454 
eta_contract 
14516  455 
end 
456 

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

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

459 

21078  460 
fun disamb_bound thy t = 
14516  461 
let 
21588  462 

463 
fun F (t $ u,idx) = 

464 
let 

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

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

467 
in 

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

469 
end 

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

471 
let 

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

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

474 
in 

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

476 
end 

477 
 F arg = arg 

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

479 
val ct = cterm_of thy t 

480 
val ct' = cterm_of thy t' 

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

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

14516  483 
in 
21588  484 
res 
14516  485 
end 
486 

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

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

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

490 

491 
fun norm_term thy t = 

492 
let 

21588  493 
val norms = ShuffleData.get thy 
494 
val ss = Simplifier.theory_context thy empty_ss 

17892  495 
setmksimps single 
21588  496 
addsimps (map (Thm.transfer thy) norms) 
21078  497 
addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] 
21588  498 
fun chain f th = 
499 
let 

22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

500 
val rhs = Thm.rhs_of th 
21588  501 
in 
502 
transitive th (f rhs) 

503 
end 

504 
val th = 

21078  505 
t > disamb_bound thy 
21588  506 
> chain (Simplifier.full_rewrite ss) 
20326  507 
> chain eta_conversion 
21588  508 
> strip_shyps 
509 
val _ = message ("norm_term: " ^ (string_of_thm th)) 

14516  510 
in 
21588  511 
th 
17463  512 
end 
21078  513 
handle e => (writeln "norm_term internal error"; print_sign_exn thy e) 
14516  514 

515 

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

517 
not touch type variables, though). *) 

518 

519 
fun close_thm th = 

520 
let 

22578  521 
val thy = Thm.theory_of_thm th 
21588  522 
val c = prop_of th 
523 
val vars = add_term_frees (c,add_term_vars(c,[])) 

14516  524 
in 
21588  525 
Drule.forall_intr_list (map (cterm_of thy) vars) th 
14516  526 
end 
17959  527 
handle e => (writeln "close_thm internal error"; OldGoals.print_exn e) 
14516  528 

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

530 

531 
fun norm_thm thy th = 

532 
let 

21588  533 
val c = prop_of th 
14516  534 
in 
21588  535 
equal_elim (norm_term thy c) th 
14516  536 
end 
537 

21078  538 
(* make_equal thy t u tries to construct the theorem t == u under the 
539 
signature thy. If it succeeds, SOME (t == u) is returned, otherwise 

15531  540 
NONE is returned. *) 
14516  541 

21078  542 
fun make_equal thy t u = 
14516  543 
let 
21588  544 
val t_is_t' = norm_term thy t 
545 
val u_is_u' = norm_term thy u 

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

547 
val _ = message ("make_equal: SOME " ^ (string_of_thm th)) 

14516  548 
in 
21588  549 
SOME th 
14516  550 
end 
15531  551 
handle e as THM _ => (message "make_equal: NONE";NONE) 
21588  552 

14516  553 
fun match_consts ignore t (* th *) = 
554 
let 

21588  555 
fun add_consts (Const (c, _), cs) = 
556 
if c mem_string ignore 

557 
then cs 

558 
else insert (op =) c cs 

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

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

561 
 add_consts (_, cs) = cs 

562 
val t_consts = add_consts(t,[]) 

14516  563 
in 
564 
fn (name,th) => 

21588  565 
let 
566 
val th_consts = add_consts(prop_of th,[]) 

567 
in 

568 
eq_set(t_consts,th_consts) 

569 
end 

14516  570 
end 
21588  571 

14516  572 
val collect_ignored = 
21078  573 
fold_rev (fn thm => fn cs => 
21588  574 
let 
575 
val (lhs,rhs) = Logic.dest_equals (prop_of thm) 

576 
val ignore_lhs = term_consts lhs \\ term_consts rhs 

577 
val ignore_rhs = term_consts rhs \\ term_consts lhs 

578 
in 

579 
fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs) 

580 
end) 

14516  581 

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

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

15531  584 
succeeds, SOME theorem is returned, otherwise NONE. *) 
14516  585 

586 
fun set_prop thy t = 

587 
let 

21588  588 
val vars = add_term_frees (t,add_term_vars (t,[])) 
27330  589 
val closed_t = fold_rev Logic.all vars t 
21588  590 
val rew_th = norm_term thy closed_t 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

591 
val rhs = Thm.rhs_of rew_th 
14516  592 

21588  593 
val shuffles = ShuffleData.get thy 
594 
fun process [] = NONE 

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

596 
let 

597 
val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th))) 

598 
val triv_th = trivial rhs 

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

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

601 
SOME(th,_) => SOME th 

602 
 NONE => NONE 

603 
in 

604 
case mod_th of 

605 
SOME mod_th => 

606 
let 

607 
val closed_th = equal_elim (symmetric rew_th) mod_th 

608 
in 

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

610 
SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th) 

611 
end 

612 
 NONE => process thms 

613 
end 

614 
handle e as THM _ => process thms 

14516  615 
in 
21588  616 
fn thms => 
617 
case process thms of 

618 
res as SOME (name,th) => if (prop_of th) aconv t 

619 
then res 

620 
else error "Internal error in set_prop" 

621 
 NONE => NONE 

14516  622 
end 
17959  623 
handle e => (writeln "set_prop internal error"; OldGoals.print_exn e) 
14516  624 

625 
fun find_potential thy t = 

626 
let 

21588  627 
val shuffles = ShuffleData.get thy 
628 
val ignored = collect_ignored shuffles [] 

26662  629 
val all_thms = 
27173  630 
map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) 
14516  631 
in 
26277  632 
List.filter (match_consts ignored t) all_thms 
14516  633 
end 
634 

635 
fun gen_shuffle_tac thy search thms i st = 

636 
let 

21588  637 
val _ = message ("Shuffling " ^ (string_of_thm st)) 
638 
val t = List.nth(prems_of st,i1) 

639 
val set = set_prop thy t 

640 
fun process_tac thms st = 

641 
case set thms of 

642 
SOME (_,th) => Seq.of_list (compose (th,i,st)) 

643 
 NONE => Seq.empty 

14516  644 
in 
21588  645 
(process_tac thms APPEND (if search 
646 
then process_tac (find_potential thy t) 

647 
else no_tac)) st 

14516  648 
end 
649 

650 
fun shuffle_tac thms i st = 

651 
gen_shuffle_tac (the_context()) false thms i st 

652 

653 
fun search_tac thms i st = 

654 
gen_shuffle_tac (the_context()) true thms i st 

655 

656 
fun shuffle_meth (thms:thm list) ctxt = 

657 
let 

21588  658 
val thy = ProofContext.theory_of ctxt 
14516  659 
in 
21588  660 
Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms)) 
14516  661 
end 
662 

663 
fun search_meth ctxt = 

664 
let 

21588  665 
val thy = ProofContext.theory_of ctxt 
666 
val prems = Assumption.prems_of ctxt 

14516  667 
in 
21588  668 
Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems)) 
14516  669 
end 
670 

671 
fun add_shuffle_rule thm thy = 

672 
let 

21588  673 
val shuffles = ShuffleData.get thy 
14516  674 
in 
21588  675 
if exists (curry Thm.eq_thm thm) shuffles 
676 
then (warning ((string_of_thm thm) ^ " already known to the shuffler"); 

677 
thy) 

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

14516  679 
end 
680 

20897  681 
val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I); 
14516  682 

18708  683 
val setup = 
22846  684 
Method.add_method ("shuffle_tac", 
685 
Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #> 

686 
Method.add_method ("search_tac", 

687 
Method.ctxt_args search_meth,"search for suitable theorems") #> 

18708  688 
add_shuffle_rule weaken #> 
689 
add_shuffle_rule equiv_comm #> 

690 
add_shuffle_rule imp_comm #> 

691 
add_shuffle_rule Drule.norm_hhf_eq #> 

692 
add_shuffle_rule Drule.triv_forall_equality #> 

18728  693 
Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")] 
18708  694 

14516  695 
end 