author | wenzelm |
Tue, 01 Jun 2004 12:33:50 +0200 | |
changeset 14854 | 61bdf2ae4dc5 |
parent 14848 | 83f1dc18f1f1 |
child 15531 | 08c8dad8e399 |
permissions | -rw-r--r-- |
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 |
|
27 |
val shuffle_attr: theory attribute |
|
28 |
||
29 |
val setup : (theory -> theory) list |
|
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*) |
|
41 |
fun print_sign_exn_unit sign e = |
|
42 |
case e of |
|
43 |
THM (msg,i,thms) => |
|
44 |
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); |
|
45 |
seq print_thm thms) |
|
46 |
| THEORY (msg,thys) => |
|
47 |
(writeln ("Exception THEORY raised:\n" ^ msg); |
|
48 |
seq (Pretty.writeln o Display.pretty_theory) thys) |
|
49 |
| TERM (msg,ts) => |
|
50 |
(writeln ("Exception TERM raised:\n" ^ msg); |
|
51 |
seq (writeln o Sign.string_of_term sign) ts) |
|
52 |
| TYPE (msg,Ts,ts) => |
|
53 |
(writeln ("Exception TYPE raised:\n" ^ msg); |
|
54 |
seq (writeln o Sign.string_of_typ sign) Ts; |
|
55 |
seq (writeln o Sign.string_of_term sign) ts) |
|
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 |
||
14848 | 61 |
val string_of_thm = Library.setmp print_mode [] string_of_thm; |
62 |
val string_of_cterm = Library.setmp print_mode [] string_of_cterm; |
|
14516 | 63 |
|
64 |
fun mk_meta_eq th = |
|
65 |
(case concl_of th of |
|
66 |
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection |
|
67 |
| Const("==",_) $ _ $ _ => th |
|
68 |
| _ => raise THM("Not an equality",0,[th])) |
|
69 |
handle _ => raise THM("Couldn't make meta equality",0,[th]) |
|
70 |
||
71 |
fun mk_obj_eq th = |
|
72 |
(case concl_of th of |
|
73 |
Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th |
|
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 |
||
78 |
structure ShuffleDataArgs: THEORY_DATA_ARGS = |
|
79 |
struct |
|
80 |
val name = "HOL/shuffles" |
|
81 |
type T = thm list |
|
82 |
val empty = [] |
|
83 |
val copy = I |
|
84 |
val prep_ext = I |
|
85 |
val merge = Library.gen_union Thm.eq_thm |
|
86 |
fun print sg thms = |
|
87 |
Pretty.writeln (Pretty.big_list "Shuffle theorems:" |
|
88 |
(map Display.pretty_thm thms)) |
|
89 |
end |
|
90 |
||
91 |
structure ShuffleData = TheoryDataFun(ShuffleDataArgs) |
|
92 |
||
93 |
val weaken = |
|
94 |
let |
|
95 |
val cert = cterm_of (sign_of ProtoPure.thy) |
|
96 |
val P = Free("P",propT) |
|
97 |
val Q = Free("Q",propT) |
|
98 |
val PQ = Logic.mk_implies(P,Q) |
|
99 |
val PPQ = Logic.mk_implies(P,PQ) |
|
100 |
val cP = cert P |
|
101 |
val cQ = cert Q |
|
102 |
val cPQ = cert PQ |
|
103 |
val cPPQ = cert PPQ |
|
104 |
val th1 = assume cPQ |> implies_intr_list [cPQ,cP] |
|
105 |
val th3 = assume cP |
|
106 |
val th4 = implies_elim_list (assume cPPQ) [th3,th3] |
|
107 |
|> implies_intr_list [cPPQ,cP] |
|
108 |
in |
|
109 |
equal_intr th4 th1 |> standard |
|
110 |
end |
|
111 |
||
112 |
val imp_comm = |
|
113 |
let |
|
114 |
val cert = cterm_of (sign_of ProtoPure.thy) |
|
115 |
val P = Free("P",propT) |
|
116 |
val Q = Free("Q",propT) |
|
117 |
val R = Free("R",propT) |
|
118 |
val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R)) |
|
119 |
val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R)) |
|
120 |
val cP = cert P |
|
121 |
val cQ = cert Q |
|
122 |
val cPQR = cert PQR |
|
123 |
val cQPR = cert QPR |
|
124 |
val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ] |
|
125 |
|> implies_intr_list [cPQR,cQ,cP] |
|
126 |
val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP] |
|
127 |
|> implies_intr_list [cQPR,cP,cQ] |
|
128 |
in |
|
129 |
equal_intr th1 th2 |> standard |
|
130 |
end |
|
131 |
||
132 |
val def_norm = |
|
133 |
let |
|
134 |
val cert = cterm_of (sign_of ProtoPure.thy) |
|
14854 | 135 |
val aT = TFree("'a",[]) |
136 |
val bT = TFree("'b",[]) |
|
14516 | 137 |
val v = Free("v",aT) |
138 |
val P = Free("P",aT-->bT) |
|
139 |
val Q = Free("Q",aT-->bT) |
|
140 |
val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) |
|
141 |
val cPQ = cert (Logic.mk_equals(P,Q)) |
|
142 |
val cv = cert v |
|
143 |
val rew = assume cvPQ |
|
144 |
|> forall_elim cv |
|
145 |
|> abstract_rule "v" cv |
|
146 |
val (lhs,rhs) = Logic.dest_equals(concl_of rew) |
|
147 |
val th1 = transitive (transitive |
|
148 |
(eta_conversion (cert lhs) |> symmetric) |
|
149 |
rew) |
|
150 |
(eta_conversion (cert rhs)) |
|
151 |
|> implies_intr cvPQ |
|
152 |
val th2 = combination (assume cPQ) (reflexive cv) |
|
153 |
|> forall_intr cv |
|
154 |
|> implies_intr cPQ |
|
155 |
in |
|
156 |
equal_intr th1 th2 |> standard |
|
157 |
end |
|
158 |
||
159 |
val all_comm = |
|
160 |
let |
|
161 |
val cert = cterm_of (sign_of ProtoPure.thy) |
|
14854 | 162 |
val xT = TFree("'a",[]) |
163 |
val yT = TFree("'b",[]) |
|
14516 | 164 |
val P = Free("P",xT-->yT-->propT) |
165 |
val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0)))) |
|
166 |
val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1)))) |
|
167 |
val cl = cert lhs |
|
168 |
val cr = cert rhs |
|
169 |
val cx = cert (Free("x",xT)) |
|
170 |
val cy = cert (Free("y",yT)) |
|
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 |
|
179 |
in |
|
180 |
equal_intr th1 th2 |> standard |
|
181 |
end |
|
182 |
||
183 |
val equiv_comm = |
|
184 |
let |
|
185 |
val cert = cterm_of (sign_of ProtoPure.thy) |
|
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 |
|
193 |
in |
|
194 |
equal_intr th1 th2 |> standard |
|
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 |
|
206 |
else if i = n+1 then raise RESULT 1 |
|
207 |
else () |
|
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) |
|
213 |
else if i = n+1 then Bound n |
|
214 |
else Bound i |
|
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 |
||
219 |
fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t = |
|
220 |
let |
|
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 sg rew) |
|
225 |
in |
|
226 |
(all_comm RS init handle e => (message "rew_th"; print_exn e)) |
|
227 |
end |
|
228 |
||
229 |
fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = |
|
230 |
let |
|
231 |
val res = (find_bound 0 body;2) handle RESULT i => i |
|
232 |
in |
|
233 |
case res of |
|
234 |
0 => Some (rew_th sg (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 sg t) |
|
240 |
val newt_th = reflexive (cterm_of sg newt) |
|
241 |
in |
|
242 |
Some (transitive t_th newt_th) |
|
243 |
end |
|
244 |
else None |
|
245 |
| _ => error "norm_term (quant_rewrite) internal error" |
|
246 |
end |
|
247 |
| quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; None) |
|
248 |
||
249 |
fun freeze_thaw_term t = |
|
250 |
let |
|
251 |
val tvars = term_tvars t |
|
252 |
val tfree_names = add_term_tfree_names(t,[]) |
|
253 |
val (type_inst,_) = |
|
254 |
foldl (fn ((inst,used),(w as (v,_),S)) => |
|
255 |
let |
|
256 |
val v' = 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 |
|
262 |
in |
|
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
263 |
(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
|
264 |
| _ => error "Internal error in Shuffler.freeze_thaw") type_inst) |
14516 | 265 |
end |
266 |
||
267 |
fun inst_tfrees sg [] thm = thm |
|
268 |
| inst_tfrees sg ((name,U)::rest) thm = |
|
269 |
let |
|
270 |
val cU = ctyp_of sg U |
|
271 |
val tfree_names = add_term_tfree_names (prop_of thm,[]) |
|
272 |
val (thm',rens) = varifyT' (tfree_names \ name) thm |
|
273 |
val mid = |
|
274 |
case rens of |
|
275 |
[] => thm' |
|
276 |
| [(_,idx)] => instantiate ([(idx,cU)],[]) thm' |
|
277 |
| _ => error "Shuffler.inst_tfrees internal error" |
|
278 |
in |
|
279 |
inst_tfrees sg rest mid |
|
280 |
end |
|
281 |
||
282 |
fun is_Abs (Abs _) = true |
|
283 |
| is_Abs _ = false |
|
284 |
||
285 |
fun eta_redex (t $ Bound 0) = |
|
286 |
let |
|
287 |
fun free n (Bound i) = i = n |
|
288 |
| free n (t $ u) = free n t orelse free n u |
|
289 |
| free n (Abs(_,_,t)) = free (n+1) t |
|
290 |
| free n _ = false |
|
291 |
in |
|
292 |
not (free 0 t) |
|
293 |
end |
|
294 |
| eta_redex _ = false |
|
295 |
||
296 |
fun eta_contract sg assumes origt = |
|
297 |
let |
|
298 |
val (typet,Tinst) = freeze_thaw_term origt |
|
299 |
val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet)) |
|
300 |
val final = inst_tfrees sg Tinst o thaw |
|
301 |
val t = #1 (Logic.dest_equals (prop_of init)) |
|
302 |
val _ = |
|
303 |
let |
|
304 |
val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
|
305 |
in |
|
306 |
if not (lhs aconv origt) |
|
307 |
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; |
|
308 |
writeln (string_of_cterm (cterm_of sg origt)); |
|
309 |
writeln (string_of_cterm (cterm_of sg lhs)); |
|
310 |
writeln (string_of_cterm (cterm_of sg typet)); |
|
311 |
writeln (string_of_cterm (cterm_of sg t)); |
|
312 |
app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst; |
|
313 |
writeln "done") |
|
314 |
else () |
|
315 |
end |
|
316 |
in |
|
317 |
case t of |
|
318 |
Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) => |
|
319 |
((if eta_redex P andalso eta_redex Q |
|
320 |
then |
|
321 |
let |
|
322 |
val cert = cterm_of sg |
|
323 |
val v = Free(variant (add_term_free_names(t,[])) "v",xT) |
|
324 |
val cv = cert v |
|
325 |
val ct = cert t |
|
326 |
val th = (assume ct) |
|
327 |
|> forall_elim cv |
|
328 |
|> abstract_rule x cv |
|
329 |
val ext_th = eta_conversion (cert (Abs(x,xT,P))) |
|
330 |
val th' = transitive (symmetric ext_th) th |
|
331 |
val cu = cert (prop_of th') |
|
332 |
val uth = combination (assume cu) (reflexive cv) |
|
333 |
val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v))) |
|
334 |
|> transitive uth |
|
335 |
|> forall_intr cv |
|
336 |
|> implies_intr cu |
|
337 |
val rew_th = equal_intr (th' |> implies_intr ct) uth' |
|
338 |
val res = final rew_th |
|
339 |
val lhs = (#1 (Logic.dest_equals (prop_of res))) |
|
340 |
in |
|
341 |
Some res |
|
342 |
end |
|
343 |
else None) |
|
344 |
handle e => (writeln "eta_contract:";print_exn e)) |
|
345 |
| _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); None) |
|
346 |
end |
|
347 |
||
348 |
fun beta_fun sg assume t = |
|
349 |
Some (beta_conversion true (cterm_of sg t)) |
|
350 |
||
351 |
fun eta_expand sg assumes origt = |
|
352 |
let |
|
353 |
val (typet,Tinst) = freeze_thaw_term origt |
|
354 |
val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet)) |
|
355 |
val final = inst_tfrees sg Tinst o thaw |
|
356 |
val t = #1 (Logic.dest_equals (prop_of init)) |
|
357 |
val _ = |
|
358 |
let |
|
359 |
val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
|
360 |
in |
|
361 |
if not (lhs aconv origt) |
|
362 |
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)"; |
|
363 |
writeln (string_of_cterm (cterm_of sg origt)); |
|
364 |
writeln (string_of_cterm (cterm_of sg lhs)); |
|
365 |
writeln (string_of_cterm (cterm_of sg typet)); |
|
366 |
writeln (string_of_cterm (cterm_of sg t)); |
|
367 |
app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst; |
|
368 |
writeln "done") |
|
369 |
else () |
|
370 |
end |
|
371 |
in |
|
372 |
case t of |
|
373 |
Const("==",T) $ P $ Q => |
|
374 |
if is_Abs P orelse is_Abs Q |
|
375 |
then (case domain_type T of |
|
376 |
Type("fun",[aT,bT]) => |
|
377 |
let |
|
378 |
val cert = cterm_of sg |
|
379 |
val vname = variant (add_term_free_names(t,[])) "v" |
|
380 |
val v = Free(vname,aT) |
|
381 |
val cv = cert v |
|
382 |
val ct = cert t |
|
383 |
val th1 = (combination (assume ct) (reflexive cv)) |
|
384 |
|> forall_intr cv |
|
385 |
|> implies_intr ct |
|
386 |
val concl = cert (concl_of th1) |
|
387 |
val th2 = (assume concl) |
|
388 |
|> forall_elim cv |
|
389 |
|> abstract_rule vname cv |
|
390 |
val (lhs,rhs) = Logic.dest_equals (prop_of th2) |
|
391 |
val elhs = eta_conversion (cert lhs) |
|
392 |
val erhs = eta_conversion (cert rhs) |
|
393 |
val th2' = transitive |
|
394 |
(transitive (symmetric elhs) th2) |
|
395 |
erhs |
|
396 |
val res = equal_intr th1 (th2' |> implies_intr concl) |
|
397 |
val res' = final res |
|
398 |
in |
|
399 |
Some res' |
|
400 |
end |
|
401 |
| _ => None) |
|
402 |
else None |
|
403 |
| _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); None) |
|
404 |
end |
|
405 |
handle e => (writeln "eta_expand internal error";print_exn e) |
|
406 |
||
14854 | 407 |
fun mk_tfree s = TFree("'"^s,[]) |
14516 | 408 |
val xT = mk_tfree "a" |
409 |
val yT = mk_tfree "b" |
|
410 |
val P = Var(("P",0),xT-->yT-->propT) |
|
411 |
val Q = Var(("Q",0),xT-->yT) |
|
412 |
val R = Var(("R",0),xT-->yT) |
|
413 |
val S = Var(("S",0),xT) |
|
414 |
in |
|
415 |
fun beta_simproc sg = Simplifier.simproc_i |
|
416 |
sg |
|
417 |
"Beta-contraction" |
|
418 |
[Abs("x",xT,Q) $ S] |
|
419 |
beta_fun |
|
420 |
||
421 |
fun quant_simproc sg = Simplifier.simproc_i |
|
422 |
sg |
|
423 |
"Ordered rewriting of nested quantifiers" |
|
424 |
[all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))] |
|
425 |
quant_rewrite |
|
426 |
fun eta_expand_simproc sg = Simplifier.simproc_i |
|
427 |
sg |
|
428 |
"Smart eta-expansion by equivalences" |
|
429 |
[Logic.mk_equals(Q,R)] |
|
430 |
eta_expand |
|
431 |
fun eta_contract_simproc sg = Simplifier.simproc_i |
|
432 |
sg |
|
433 |
"Smart handling of eta-contractions" |
|
434 |
[all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))] |
|
435 |
eta_contract |
|
436 |
end |
|
437 |
||
438 |
(* Disambiguates the names of bound variables in a term, returning t |
|
439 |
== t' where all the names of bound variables in t' are unique *) |
|
440 |
||
441 |
fun disamb_bound sg t = |
|
442 |
let |
|
443 |
||
444 |
fun F (t $ u,idx) = |
|
445 |
let |
|
446 |
val (t',idx') = F (t,idx) |
|
447 |
val (u',idx'') = F (u,idx') |
|
448 |
in |
|
449 |
(t' $ u',idx'') |
|
450 |
end |
|
451 |
| F (Abs(x,xT,t),idx) = |
|
452 |
let |
|
453 |
val x' = "x" ^ (LargeInt.toString idx) (* amazing *) |
|
454 |
val (t',idx') = F (t,idx+1) |
|
455 |
in |
|
456 |
(Abs(x',xT,t'),idx') |
|
457 |
end |
|
458 |
| F arg = arg |
|
459 |
val (t',_) = F (t,0) |
|
460 |
val ct = cterm_of sg t |
|
461 |
val ct' = cterm_of sg t' |
|
462 |
val res = transitive (reflexive ct) (reflexive ct') |
|
463 |
val _ = message ("disamb_term: " ^ (string_of_thm res)) |
|
464 |
in |
|
465 |
res |
|
466 |
end |
|
467 |
||
468 |
(* Transforms a term t to some normal form t', returning the theorem t |
|
469 |
== t'. This is originally a help function for make_equal, but might |
|
470 |
be handy in its own right, for example for indexing terms. *) |
|
471 |
||
472 |
fun norm_term thy t = |
|
473 |
let |
|
474 |
val sg = sign_of thy |
|
475 |
||
476 |
val norms = ShuffleData.get thy |
|
477 |
val ss = empty_ss setmksimps single |
|
478 |
addsimps (map (transfer_sg sg) norms) |
|
479 |
fun chain f th = |
|
480 |
let |
|
481 |
val rhs = snd (dest_equals (cprop_of th)) |
|
482 |
in |
|
483 |
transitive th (f rhs) |
|
484 |
end |
|
485 |
||
486 |
val th = |
|
487 |
t |> disamb_bound sg |
|
488 |
|> chain (Simplifier.full_rewrite |
|
489 |
(ss addsimprocs [quant_simproc sg,eta_expand_simproc sg,eta_contract_simproc sg])) |
|
490 |
|> chain eta_conversion |
|
491 |
|> strip_shyps |
|
492 |
val _ = message ("norm_term: " ^ (string_of_thm th)) |
|
493 |
in |
|
494 |
th |
|
495 |
end |
|
496 |
handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e) |
|
497 |
||
498 |
||
499 |
(* Closes a theorem with respect to free and schematic variables (does |
|
500 |
not touch type variables, though). *) |
|
501 |
||
502 |
fun close_thm th = |
|
503 |
let |
|
504 |
val sg = sign_of_thm th |
|
505 |
val c = prop_of th |
|
14854 | 506 |
val vars = add_term_frees (c,add_term_vars(c,[])) |
14516 | 507 |
in |
14854 | 508 |
Drule.forall_intr_list (map (cterm_of sg) vars) th |
14516 | 509 |
end |
510 |
handle e => (writeln "close_thm internal error"; print_exn e) |
|
511 |
||
512 |
(* Normalizes a theorem's conclusion using norm_term. *) |
|
513 |
||
514 |
fun norm_thm thy th = |
|
515 |
let |
|
516 |
val c = prop_of th |
|
517 |
in |
|
518 |
equal_elim (norm_term thy c) th |
|
519 |
end |
|
520 |
||
521 |
(* make_equal sg t u tries to construct the theorem t == u under the |
|
522 |
signature sg. If it succeeds, Some (t == u) is returned, otherwise |
|
523 |
None is returned. *) |
|
524 |
||
525 |
fun make_equal sg t u = |
|
526 |
let |
|
527 |
val t_is_t' = norm_term sg t |
|
528 |
val u_is_u' = norm_term sg u |
|
529 |
val th = transitive t_is_t' (symmetric u_is_u') |
|
530 |
val _ = message ("make_equal: Some " ^ (string_of_thm th)) |
|
531 |
in |
|
532 |
Some th |
|
533 |
end |
|
534 |
handle e as THM _ => (message "make_equal: None";None) |
|
535 |
||
536 |
fun match_consts ignore t (* th *) = |
|
537 |
let |
|
538 |
fun add_consts (Const (c, _), cs) = |
|
539 |
if c mem_string ignore |
|
540 |
then cs |
|
541 |
else c ins_string cs |
|
542 |
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) |
|
543 |
| add_consts (Abs (_, _, t), cs) = add_consts (t, cs) |
|
544 |
| add_consts (_, cs) = cs |
|
545 |
val t_consts = add_consts(t,[]) |
|
546 |
in |
|
547 |
fn (name,th) => |
|
548 |
let |
|
549 |
val th_consts = add_consts(prop_of th,[]) |
|
550 |
in |
|
551 |
eq_set(t_consts,th_consts) |
|
552 |
end |
|
553 |
end |
|
554 |
||
555 |
val collect_ignored = |
|
556 |
foldr (fn (thm,cs) => |
|
557 |
let |
|
558 |
val (lhs,rhs) = Logic.dest_equals (prop_of thm) |
|
559 |
val ignore_lhs = term_consts lhs \\ term_consts rhs |
|
560 |
val ignore_rhs = term_consts rhs \\ term_consts lhs |
|
561 |
in |
|
562 |
foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs) |
|
563 |
end) |
|
564 |
||
565 |
(* set_prop t thms tries to make a theorem with the proposition t from |
|
566 |
one of the theorems thms, by shuffling the propositions around. If it |
|
567 |
succeeds, Some theorem is returned, otherwise None. *) |
|
568 |
||
569 |
fun set_prop thy t = |
|
570 |
let |
|
571 |
val sg = sign_of thy |
|
14854 | 572 |
val vars = add_term_frees (t,add_term_vars (t,[])) |
14516 | 573 |
val closed_t = foldr (fn (v,body) => let val vT = type_of v |
14854 | 574 |
in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t) |
14516 | 575 |
val rew_th = norm_term thy closed_t |
576 |
val rhs = snd (dest_equals (cprop_of rew_th)) |
|
577 |
||
578 |
val shuffles = ShuffleData.get thy |
|
579 |
fun process [] = None |
|
580 |
| process ((name,th)::thms) = |
|
581 |
let |
|
582 |
val norm_th = varifyT (norm_thm thy (close_thm (transfer_sg sg th))) |
|
583 |
val triv_th = trivial rhs |
|
584 |
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) |
|
585 |
val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of |
|
586 |
Some(th,_) => Some th |
|
587 |
| None => None |
|
588 |
in |
|
589 |
case mod_th of |
|
590 |
Some mod_th => |
|
591 |
let |
|
592 |
val closed_th = equal_elim (symmetric rew_th) mod_th |
|
593 |
in |
|
594 |
message ("Shuffler.set_prop succeeded by " ^ name); |
|
14854 | 595 |
Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th) |
14516 | 596 |
end |
597 |
| None => process thms |
|
598 |
end |
|
599 |
handle e as THM _ => process thms |
|
600 |
in |
|
601 |
fn thms => |
|
602 |
case process thms of |
|
603 |
res as Some (name,th) => if (prop_of th) aconv t |
|
604 |
then res |
|
605 |
else error "Internal error in set_prop" |
|
606 |
| None => None |
|
607 |
end |
|
608 |
handle e => (writeln "set_prop internal error"; print_exn e) |
|
609 |
||
610 |
fun find_potential thy t = |
|
611 |
let |
|
612 |
val shuffles = ShuffleData.get thy |
|
613 |
val ignored = collect_ignored(shuffles,[]) |
|
614 |
val rel_consts = term_consts t \\ ignored |
|
615 |
val pot_thms = PureThy.thms_containing_consts thy rel_consts |
|
616 |
in |
|
617 |
filter (match_consts ignored t) pot_thms |
|
618 |
end |
|
619 |
||
620 |
fun gen_shuffle_tac thy search thms i st = |
|
621 |
let |
|
622 |
val _ = message ("Shuffling " ^ (string_of_thm st)) |
|
623 |
val t = nth_elem(i-1,prems_of st) |
|
624 |
val set = set_prop thy t |
|
625 |
fun process_tac thms st = |
|
626 |
case set thms of |
|
627 |
Some (_,th) => Seq.of_list (compose (th,i,st)) |
|
628 |
| None => Seq.empty |
|
629 |
in |
|
630 |
(process_tac thms APPEND (if search |
|
631 |
then process_tac (find_potential thy t) |
|
632 |
else no_tac)) st |
|
633 |
end |
|
634 |
||
635 |
fun shuffle_tac thms i st = |
|
636 |
gen_shuffle_tac (the_context()) false thms i st |
|
637 |
||
638 |
fun search_tac thms i st = |
|
639 |
gen_shuffle_tac (the_context()) true thms i st |
|
640 |
||
641 |
fun shuffle_meth (thms:thm list) ctxt = |
|
642 |
let |
|
643 |
val thy = ProofContext.theory_of ctxt |
|
644 |
in |
|
645 |
Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy false (map (pair "") thms)) |
|
646 |
end |
|
647 |
||
648 |
fun search_meth ctxt = |
|
649 |
let |
|
650 |
val thy = ProofContext.theory_of ctxt |
|
651 |
val prems = ProofContext.prems_of ctxt |
|
652 |
in |
|
653 |
Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems)) |
|
654 |
end |
|
655 |
||
656 |
val print_shuffles = ShuffleData.print |
|
657 |
||
658 |
fun add_shuffle_rule thm thy = |
|
659 |
let |
|
660 |
val shuffles = ShuffleData.get thy |
|
661 |
in |
|
662 |
if exists (curry Thm.eq_thm thm) shuffles |
|
663 |
then (warning ((string_of_thm thm) ^ " already known to the shuffler"); |
|
664 |
thy) |
|
665 |
else ShuffleData.put (thm::shuffles) thy |
|
666 |
end |
|
667 |
||
668 |
fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm) |
|
669 |
||
670 |
val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"), |
|
671 |
Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"), |
|
672 |
ShuffleData.init, |
|
673 |
add_shuffle_rule weaken, |
|
674 |
add_shuffle_rule equiv_comm, |
|
675 |
add_shuffle_rule imp_comm, |
|
676 |
add_shuffle_rule Drule.norm_hhf_eq, |
|
677 |
add_shuffle_rule Drule.triv_forall_equality, |
|
678 |
Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]] |
|
679 |
end |