author | haftmann |
Sun, 04 Mar 2012 00:15:08 +0100 | |
changeset 46803 | f8875c15cbe1 |
parent 46218 | ecf6375e2abb |
child 47024 | 6c2b7b0421b5 |
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 |
Author: Sebastian Skalberg, TU Muenchen |
3 |
||
4 |
Package for proving two terms equal by normalizing (hence the |
|
5 |
"shuffler" name). Uses the simplifier for the normalization. |
|
6 |
*) |
|
7 |
||
8 |
signature Shuffler = |
|
9 |
sig |
|
32740 | 10 |
val debug : bool Unsynchronized.ref |
14516 | 11 |
|
12 |
val norm_term : theory -> term -> thm |
|
13 |
val make_equal : theory -> term -> term -> thm option |
|
14 |
val set_prop : theory -> term -> (string * thm) list -> (string * thm) option |
|
15 |
||
16 |
val find_potential: theory -> term -> (string * thm) list |
|
17 |
||
31241 | 18 |
val gen_shuffle_tac: Proof.context -> bool -> (string * thm) list -> int -> tactic |
19 |
val shuffle_tac: Proof.context -> thm list -> int -> tactic |
|
20 |
val search_tac : Proof.context -> int -> tactic |
|
14516 | 21 |
|
22 |
val print_shuffles: theory -> unit |
|
23 |
||
24 |
val add_shuffle_rule: thm -> theory -> theory |
|
18728 | 25 |
val shuffle_attr: attribute |
14516 | 26 |
|
18708 | 27 |
val setup : theory -> theory |
14516 | 28 |
end |
29 |
||
46803 | 30 |
structure Shuffler : Shuffler = |
14516 | 31 |
struct |
32 |
||
32740 | 33 |
val debug = Unsynchronized.ref false |
14516 | 34 |
|
35 |
fun if_debug f x = if !debug then f x else () |
|
36 |
val message = if_debug writeln |
|
37 |
||
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
36945
diff
changeset
|
38 |
val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context; |
14516 | 39 |
|
33522 | 40 |
structure ShuffleData = Theory_Data |
22846 | 41 |
( |
42 |
type T = thm list |
|
43 |
val empty = [] |
|
44 |
val extend = I |
|
33522 | 45 |
val merge = Thm.merge_thms |
22846 | 46 |
) |
14516 | 47 |
|
22846 | 48 |
fun print_shuffles thy = |
49 |
Pretty.writeln (Pretty.big_list "Shuffle theorems:" |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset
|
50 |
(map (Display.pretty_thm_global thy) (ShuffleData.get thy))) |
14516 | 51 |
|
52 |
val weaken = |
|
53 |
let |
|
26424 | 54 |
val cert = cterm_of Pure.thy |
21588 | 55 |
val P = Free("P",propT) |
56 |
val Q = Free("Q",propT) |
|
57 |
val PQ = Logic.mk_implies(P,Q) |
|
58 |
val PPQ = Logic.mk_implies(P,PQ) |
|
59 |
val cP = cert P |
|
60 |
val cPQ = cert PQ |
|
61 |
val cPPQ = cert PPQ |
|
36945 | 62 |
val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP] |
63 |
val th3 = Thm.assume cP |
|
64 |
val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3] |
|
21588 | 65 |
|> implies_intr_list [cPPQ,cP] |
14516 | 66 |
in |
36945 | 67 |
Thm.equal_intr th4 th1 |> Drule.export_without_context |
14516 | 68 |
end |
69 |
||
70 |
val imp_comm = |
|
71 |
let |
|
26424 | 72 |
val cert = cterm_of Pure.thy |
21588 | 73 |
val P = Free("P",propT) |
74 |
val Q = Free("Q",propT) |
|
75 |
val R = Free("R",propT) |
|
76 |
val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R)) |
|
77 |
val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R)) |
|
78 |
val cP = cert P |
|
79 |
val cQ = cert Q |
|
80 |
val cPQR = cert PQR |
|
81 |
val cQPR = cert QPR |
|
36945 | 82 |
val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ] |
21588 | 83 |
|> implies_intr_list [cPQR,cQ,cP] |
36945 | 84 |
val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP] |
21588 | 85 |
|> implies_intr_list [cQPR,cP,cQ] |
14516 | 86 |
in |
36945 | 87 |
Thm.equal_intr th1 th2 |> Drule.export_without_context |
14516 | 88 |
end |
89 |
||
90 |
val all_comm = |
|
91 |
let |
|
26424 | 92 |
val cert = cterm_of Pure.thy |
21588 | 93 |
val xT = TFree("'a",[]) |
94 |
val yT = TFree("'b",[]) |
|
27330 | 95 |
val x = Free("x",xT) |
96 |
val y = Free("y",yT) |
|
21588 | 97 |
val P = Free("P",xT-->yT-->propT) |
27330 | 98 |
val lhs = Logic.all x (Logic.all y (P $ x $ y)) |
99 |
val rhs = Logic.all y (Logic.all x (P $ x $ y)) |
|
21588 | 100 |
val cl = cert lhs |
101 |
val cr = cert rhs |
|
27330 | 102 |
val cx = cert x |
103 |
val cy = cert y |
|
36945 | 104 |
val th1 = Thm.assume cr |
21588 | 105 |
|> forall_elim_list [cy,cx] |
106 |
|> forall_intr_list [cx,cy] |
|
36945 | 107 |
|> Thm.implies_intr cr |
108 |
val th2 = Thm.assume cl |
|
21588 | 109 |
|> forall_elim_list [cx,cy] |
110 |
|> forall_intr_list [cy,cx] |
|
36945 | 111 |
|> Thm.implies_intr cl |
14516 | 112 |
in |
36945 | 113 |
Thm.equal_intr th1 th2 |> Drule.export_without_context |
14516 | 114 |
end |
115 |
||
116 |
val equiv_comm = |
|
117 |
let |
|
26424 | 118 |
val cert = cterm_of Pure.thy |
21588 | 119 |
val T = TFree("'a",[]) |
120 |
val t = Free("t",T) |
|
121 |
val u = Free("u",T) |
|
122 |
val ctu = cert (Logic.mk_equals(t,u)) |
|
123 |
val cut = cert (Logic.mk_equals(u,t)) |
|
36945 | 124 |
val th1 = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu |
125 |
val th2 = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut |
|
14516 | 126 |
in |
36945 | 127 |
Thm.equal_intr th1 th2 |> Drule.export_without_context |
14516 | 128 |
end |
129 |
||
130 |
(* This simplification procedure rewrites !!x y. P x y |
|
131 |
deterministicly, in order for the normalization function, defined |
|
132 |
below, to handle nested quantifiers robustly *) |
|
133 |
||
134 |
local |
|
135 |
||
136 |
exception RESULT of int |
|
137 |
||
138 |
fun find_bound n (Bound i) = if i = n then raise RESULT 0 |
|
21588 | 139 |
else if i = n+1 then raise RESULT 1 |
140 |
else () |
|
14516 | 141 |
| find_bound n (t $ u) = (find_bound n t; find_bound n u) |
142 |
| find_bound n (Abs(_,_,t)) = find_bound (n+1) t |
|
143 |
| find_bound _ _ = () |
|
144 |
||
145 |
fun swap_bound n (Bound i) = if i = n then Bound (n+1) |
|
21588 | 146 |
else if i = n+1 then Bound n |
147 |
else Bound i |
|
14516 | 148 |
| swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u) |
149 |
| swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t) |
|
150 |
| swap_bound n t = t |
|
151 |
||
46803 | 152 |
fun rew_th thy xv yv t = |
14516 | 153 |
let |
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
46201
diff
changeset
|
154 |
val lhs = Logic.list_all ([xv,yv],t) |
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
46201
diff
changeset
|
155 |
val rhs = Logic.list_all ([yv,xv],swap_bound 0 t) |
21588 | 156 |
val rew = Logic.mk_equals (lhs,rhs) |
36945 | 157 |
val init = Thm.trivial (cterm_of thy rew) |
14516 | 158 |
in |
37778
87b5dfe00387
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
wenzelm
parents:
37146
diff
changeset
|
159 |
all_comm RS init |
14516 | 160 |
end |
161 |
||
46201 | 162 |
fun quant_rewrite thy _ (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = |
14516 | 163 |
let |
21588 | 164 |
val res = (find_bound 0 body;2) handle RESULT i => i |
14516 | 165 |
in |
21588 | 166 |
case res of |
167 |
0 => SOME (rew_th thy (x,xT) (y,yT) body) |
|
168 |
| 1 => if string_ord(y,x) = LESS |
|
169 |
then |
|
170 |
let |
|
171 |
val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body))) |
|
36945 | 172 |
val t_th = Thm.reflexive (cterm_of thy t) |
173 |
val newt_th = Thm.reflexive (cterm_of thy newt) |
|
21588 | 174 |
in |
36945 | 175 |
SOME (Thm.transitive t_th newt_th) |
21588 | 176 |
end |
177 |
else NONE |
|
178 |
| _ => error "norm_term (quant_rewrite) internal error" |
|
14516 | 179 |
end |
15531 | 180 |
| quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE) |
14516 | 181 |
|
182 |
fun freeze_thaw_term t = |
|
183 |
let |
|
44121 | 184 |
val tvars = Misc_Legacy.term_tvars t |
185 |
val tfree_names = Misc_Legacy.add_term_tfree_names(t,[]) |
|
21588 | 186 |
val (type_inst,_) = |
33245 | 187 |
fold (fn (w as (v,_), S) => fn (inst, used) => |
21588 | 188 |
let |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42368
diff
changeset
|
189 |
val v' = singleton (Name.variant_list used) v |
21588 | 190 |
in |
191 |
((w,TFree(v',S))::inst,v'::used) |
|
192 |
end) |
|
33245 | 193 |
tvars ([], tfree_names) |
21588 | 194 |
val t' = subst_TVars type_inst t |
14516 | 195 |
in |
33245 | 196 |
(t', map (fn (w,TFree(v,S)) => (v,TVar(w,S)) |
21588 | 197 |
| _ => error "Internal error in Shuffler.freeze_thaw") type_inst) |
14516 | 198 |
end |
199 |
||
21078 | 200 |
fun inst_tfrees thy [] thm = thm |
21588 | 201 |
| inst_tfrees thy ((name,U)::rest) thm = |
14516 | 202 |
let |
21588 | 203 |
val cU = ctyp_of thy U |
44121 | 204 |
val tfrees = Misc_Legacy.add_term_tfrees (prop_of thm,[]) |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset
|
205 |
val (rens, thm') = Thm.varifyT_global' |
20951
868120282837
gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents:
20897
diff
changeset
|
206 |
(remove (op = o apsnd fst) name tfrees) thm |
21588 | 207 |
val mid = |
208 |
case rens of |
|
209 |
[] => thm' |
|
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43324
diff
changeset
|
210 |
| [((_, S), idx)] => Drule.instantiate_normalize |
21078 | 211 |
([(ctyp_of thy (TVar (idx, S)), cU)], []) thm' |
21588 | 212 |
| _ => error "Shuffler.inst_tfrees internal error" |
14516 | 213 |
in |
21588 | 214 |
inst_tfrees thy rest mid |
14516 | 215 |
end |
216 |
||
217 |
fun is_Abs (Abs _) = true |
|
218 |
| is_Abs _ = false |
|
219 |
||
220 |
fun eta_redex (t $ Bound 0) = |
|
221 |
let |
|
21588 | 222 |
fun free n (Bound i) = i = n |
223 |
| free n (t $ u) = free n t orelse free n u |
|
224 |
| free n (Abs(_,_,t)) = free (n+1) t |
|
225 |
| free n _ = false |
|
14516 | 226 |
in |
21588 | 227 |
not (free 0 t) |
14516 | 228 |
end |
229 |
| eta_redex _ = false |
|
230 |
||
46201 | 231 |
fun eta_contract thy _ origt = |
14516 | 232 |
let |
21588 | 233 |
val (typet,Tinst) = freeze_thaw_term origt |
36945 | 234 |
val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) |
21588 | 235 |
val final = inst_tfrees thy Tinst o thaw |
236 |
val t = #1 (Logic.dest_equals (prop_of init)) |
|
237 |
val _ = |
|
238 |
let |
|
239 |
val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
|
240 |
in |
|
241 |
if not (lhs aconv origt) |
|
32432
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
242 |
then |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
243 |
writeln (cat_lines |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
244 |
(["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)", |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
245 |
Syntax.string_of_term_global thy origt, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
246 |
Syntax.string_of_term_global thy lhs, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
247 |
Syntax.string_of_term_global thy typet, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
248 |
Syntax.string_of_term_global thy t] @ |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
249 |
map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst)) |
21588 | 250 |
else () |
251 |
end |
|
14516 | 252 |
in |
21588 | 253 |
case t of |
46201 | 254 |
Const("all",_) $ (Abs(x,xT,Const("==",_) $ P $ Q)) => |
37778
87b5dfe00387
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
wenzelm
parents:
37146
diff
changeset
|
255 |
(if eta_redex P andalso eta_redex Q |
21588 | 256 |
then |
257 |
let |
|
258 |
val cert = cterm_of thy |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42368
diff
changeset
|
259 |
val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT) |
21588 | 260 |
val cv = cert v |
261 |
val ct = cert t |
|
36945 | 262 |
val th = (Thm.assume ct) |
263 |
|> Thm.forall_elim cv |
|
264 |
|> Thm.abstract_rule x cv |
|
265 |
val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P))) |
|
266 |
val th' = Thm.transitive (Thm.symmetric ext_th) th |
|
21588 | 267 |
val cu = cert (prop_of th') |
36945 | 268 |
val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv) |
269 |
val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v))) |
|
270 |
|> Thm.transitive uth |
|
271 |
|> Thm.forall_intr cv |
|
272 |
|> Thm.implies_intr cu |
|
273 |
val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth' |
|
21588 | 274 |
val res = final rew_th |
275 |
in |
|
276 |
SOME res |
|
277 |
end |
|
278 |
else NONE) |
|
279 |
| _ => NONE |
|
17440
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17188
diff
changeset
|
280 |
end |
14516 | 281 |
|
46201 | 282 |
fun eta_expand thy _ origt = |
14516 | 283 |
let |
21588 | 284 |
val (typet,Tinst) = freeze_thaw_term origt |
36945 | 285 |
val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) |
21588 | 286 |
val final = inst_tfrees thy Tinst o thaw |
287 |
val t = #1 (Logic.dest_equals (prop_of init)) |
|
288 |
val _ = |
|
289 |
let |
|
290 |
val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
|
291 |
in |
|
292 |
if not (lhs aconv origt) |
|
32432
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
293 |
then |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
294 |
writeln (cat_lines |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
295 |
(["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)", |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
296 |
Syntax.string_of_term_global thy origt, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
297 |
Syntax.string_of_term_global thy lhs, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
298 |
Syntax.string_of_term_global thy typet, |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
299 |
Syntax.string_of_term_global thy t] @ |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
300 |
map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst)) |
21588 | 301 |
else () |
302 |
end |
|
14516 | 303 |
in |
21588 | 304 |
case t of |
305 |
Const("==",T) $ P $ Q => |
|
306 |
if is_Abs P orelse is_Abs Q |
|
307 |
then (case domain_type T of |
|
46803 | 308 |
Type("fun",[aT,_]) => |
21588 | 309 |
let |
310 |
val cert = cterm_of thy |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42368
diff
changeset
|
311 |
val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v" |
21588 | 312 |
val v = Free(vname,aT) |
313 |
val cv = cert v |
|
314 |
val ct = cert t |
|
36945 | 315 |
val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv)) |
316 |
|> Thm.forall_intr cv |
|
317 |
|> Thm.implies_intr ct |
|
21588 | 318 |
val concl = cert (concl_of th1) |
36945 | 319 |
val th2 = (Thm.assume concl) |
320 |
|> Thm.forall_elim cv |
|
321 |
|> Thm.abstract_rule vname cv |
|
21588 | 322 |
val (lhs,rhs) = Logic.dest_equals (prop_of th2) |
36945 | 323 |
val elhs = Thm.eta_conversion (cert lhs) |
324 |
val erhs = Thm.eta_conversion (cert rhs) |
|
325 |
val th2' = Thm.transitive |
|
326 |
(Thm.transitive (Thm.symmetric elhs) th2) |
|
21588 | 327 |
erhs |
36945 | 328 |
val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl) |
21588 | 329 |
val res' = final res |
330 |
in |
|
331 |
SOME res' |
|
332 |
end |
|
333 |
| _ => NONE) |
|
334 |
else NONE |
|
32432
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
335 |
| _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t) |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32091
diff
changeset
|
336 |
end; |
14516 | 337 |
|
14854 | 338 |
fun mk_tfree s = TFree("'"^s,[]) |
20326 | 339 |
fun mk_free s t = Free (s,t) |
14516 | 340 |
val xT = mk_tfree "a" |
341 |
val yT = mk_tfree "b" |
|
27330 | 342 |
val x = Free ("x", xT) |
343 |
val y = Free ("y", yT) |
|
20326 | 344 |
val P = mk_free "P" (xT-->yT-->propT) |
345 |
val Q = mk_free "Q" (xT-->yT) |
|
346 |
val R = mk_free "R" (xT-->yT) |
|
14516 | 347 |
in |
17188 | 348 |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38558
diff
changeset
|
349 |
fun quant_simproc thy = Simplifier.simproc_global_i |
21588 | 350 |
thy |
351 |
"Ordered rewriting of nested quantifiers" |
|
27330 | 352 |
[Logic.all x (Logic.all y (P $ x $ y))] |
21588 | 353 |
quant_rewrite |
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38558
diff
changeset
|
354 |
fun eta_expand_simproc thy = Simplifier.simproc_global_i |
21588 | 355 |
thy |
356 |
"Smart eta-expansion by equivalences" |
|
357 |
[Logic.mk_equals(Q,R)] |
|
358 |
eta_expand |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38558
diff
changeset
|
359 |
fun eta_contract_simproc thy = Simplifier.simproc_global_i |
21588 | 360 |
thy |
361 |
"Smart handling of eta-contractions" |
|
27330 | 362 |
[Logic.all x (Logic.mk_equals (Q $ x, R $ x))] |
21588 | 363 |
eta_contract |
14516 | 364 |
end |
365 |
||
366 |
(* Disambiguates the names of bound variables in a term, returning t |
|
367 |
== t' where all the names of bound variables in t' are unique *) |
|
368 |
||
21078 | 369 |
fun disamb_bound thy t = |
14516 | 370 |
let |
21588 | 371 |
|
372 |
fun F (t $ u,idx) = |
|
373 |
let |
|
374 |
val (t',idx') = F (t,idx) |
|
375 |
val (u',idx'') = F (u,idx') |
|
376 |
in |
|
377 |
(t' $ u',idx'') |
|
378 |
end |
|
46803 | 379 |
| F (Abs(_,xT,t),idx) = |
21588 | 380 |
let |
41491 | 381 |
val x' = "x" ^ string_of_int idx |
21588 | 382 |
val (t',idx') = F (t,idx+1) |
383 |
in |
|
384 |
(Abs(x',xT,t'),idx') |
|
385 |
end |
|
386 |
| F arg = arg |
|
387 |
val (t',_) = F (t,0) |
|
388 |
val ct = cterm_of thy t |
|
389 |
val ct' = cterm_of thy t' |
|
36945 | 390 |
val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct') |
21588 | 391 |
val _ = message ("disamb_term: " ^ (string_of_thm res)) |
14516 | 392 |
in |
21588 | 393 |
res |
14516 | 394 |
end |
395 |
||
396 |
(* Transforms a term t to some normal form t', returning the theorem t |
|
397 |
== t'. This is originally a help function for make_equal, but might |
|
398 |
be handy in its own right, for example for indexing terms. *) |
|
399 |
||
400 |
fun norm_term thy t = |
|
401 |
let |
|
21588 | 402 |
val norms = ShuffleData.get thy |
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
35021
diff
changeset
|
403 |
val ss = Simplifier.global_context thy empty_ss |
21588 | 404 |
addsimps (map (Thm.transfer thy) norms) |
21078 | 405 |
addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] |
21588 | 406 |
fun chain f th = |
407 |
let |
|
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset
|
408 |
val rhs = Thm.rhs_of th |
21588 | 409 |
in |
36945 | 410 |
Thm.transitive th (f rhs) |
21588 | 411 |
end |
412 |
val th = |
|
21078 | 413 |
t |> disamb_bound thy |
21588 | 414 |
|> chain (Simplifier.full_rewrite ss) |
36945 | 415 |
|> chain Thm.eta_conversion |
36614
b6c031ad3690
minor tuning of Thm.strip_shyps -- no longer pervasive;
wenzelm
parents:
36543
diff
changeset
|
416 |
|> Thm.strip_shyps |
21588 | 417 |
val _ = message ("norm_term: " ^ (string_of_thm th)) |
14516 | 418 |
in |
21588 | 419 |
th |
17463 | 420 |
end |
14516 | 421 |
|
422 |
||
423 |
(* Closes a theorem with respect to free and schematic variables (does |
|
424 |
not touch type variables, though). *) |
|
425 |
||
426 |
fun close_thm th = |
|
427 |
let |
|
22578 | 428 |
val thy = Thm.theory_of_thm th |
21588 | 429 |
val c = prop_of th |
44121 | 430 |
val vars = Misc_Legacy.add_term_frees (c, Misc_Legacy.add_term_vars(c,[])) |
14516 | 431 |
in |
21588 | 432 |
Drule.forall_intr_list (map (cterm_of thy) vars) th |
14516 | 433 |
end |
37778
87b5dfe00387
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
wenzelm
parents:
37146
diff
changeset
|
434 |
|
14516 | 435 |
|
436 |
(* Normalizes a theorem's conclusion using norm_term. *) |
|
437 |
||
438 |
fun norm_thm thy th = |
|
439 |
let |
|
21588 | 440 |
val c = prop_of th |
14516 | 441 |
in |
36945 | 442 |
Thm.equal_elim (norm_term thy c) th |
14516 | 443 |
end |
444 |
||
21078 | 445 |
(* make_equal thy t u tries to construct the theorem t == u under the |
446 |
signature thy. If it succeeds, SOME (t == u) is returned, otherwise |
|
15531 | 447 |
NONE is returned. *) |
14516 | 448 |
|
21078 | 449 |
fun make_equal thy t u = |
14516 | 450 |
let |
21588 | 451 |
val t_is_t' = norm_term thy t |
452 |
val u_is_u' = norm_term thy u |
|
36945 | 453 |
val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u') |
21588 | 454 |
val _ = message ("make_equal: SOME " ^ (string_of_thm th)) |
14516 | 455 |
in |
21588 | 456 |
SOME th |
14516 | 457 |
end |
46803 | 458 |
handle THM _ => (message "make_equal: NONE";NONE) |
21588 | 459 |
|
14516 | 460 |
fun match_consts ignore t (* th *) = |
461 |
let |
|
21588 | 462 |
fun add_consts (Const (c, _), cs) = |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36614
diff
changeset
|
463 |
if member (op =) ignore c |
21588 | 464 |
then cs |
465 |
else insert (op =) c cs |
|
466 |
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) |
|
467 |
| add_consts (Abs (_, _, t), cs) = add_consts (t, cs) |
|
468 |
| add_consts (_, cs) = cs |
|
469 |
val t_consts = add_consts(t,[]) |
|
14516 | 470 |
in |
46803 | 471 |
fn (_,th) => |
21588 | 472 |
let |
473 |
val th_consts = add_consts(prop_of th,[]) |
|
474 |
in |
|
33038 | 475 |
eq_set (op =) (t_consts, th_consts) |
21588 | 476 |
end |
14516 | 477 |
end |
21588 | 478 |
|
33040 | 479 |
val collect_ignored = fold_rev (fn thm => fn cs => |
480 |
let |
|
481 |
val (lhs, rhs) = Logic.dest_equals (prop_of thm); |
|
482 |
val consts_lhs = Term.add_const_names lhs []; |
|
483 |
val consts_rhs = Term.add_const_names rhs []; |
|
484 |
val ignore_lhs = subtract (op =) consts_rhs consts_lhs; |
|
485 |
val ignore_rhs = subtract (op =) consts_lhs consts_rhs; |
|
486 |
in |
|
487 |
fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs) |
|
488 |
end) |
|
14516 | 489 |
|
490 |
(* set_prop t thms tries to make a theorem with the proposition t from |
|
491 |
one of the theorems thms, by shuffling the propositions around. If it |
|
15531 | 492 |
succeeds, SOME theorem is returned, otherwise NONE. *) |
14516 | 493 |
|
494 |
fun set_prop thy t = |
|
495 |
let |
|
44121 | 496 |
val vars = Misc_Legacy.add_term_frees (t, Misc_Legacy.add_term_vars (t,[])) |
27330 | 497 |
val closed_t = fold_rev Logic.all vars t |
21588 | 498 |
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
|
499 |
val rhs = Thm.rhs_of rew_th |
14516 | 500 |
|
21588 | 501 |
fun process [] = NONE |
502 |
| process ((name,th)::thms) = |
|
503 |
let |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset
|
504 |
val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th))) |
36945 | 505 |
val triv_th = Thm.trivial rhs |
21588 | 506 |
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) |
31945 | 507 |
val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of |
21588 | 508 |
SOME(th,_) => SOME th |
509 |
| NONE => NONE |
|
510 |
in |
|
511 |
case mod_th of |
|
512 |
SOME mod_th => |
|
513 |
let |
|
36945 | 514 |
val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th |
21588 | 515 |
in |
516 |
message ("Shuffler.set_prop succeeded by " ^ name); |
|
517 |
SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th) |
|
518 |
end |
|
519 |
| NONE => process thms |
|
520 |
end |
|
46803 | 521 |
handle THM _ => process thms |
14516 | 522 |
in |
21588 | 523 |
fn thms => |
524 |
case process thms of |
|
46803 | 525 |
res as SOME (_,th) => if (prop_of th) aconv t |
21588 | 526 |
then res |
527 |
else error "Internal error in set_prop" |
|
528 |
| NONE => NONE |
|
14516 | 529 |
end |
530 |
||
531 |
fun find_potential thy t = |
|
532 |
let |
|
21588 | 533 |
val shuffles = ShuffleData.get thy |
534 |
val ignored = collect_ignored shuffles [] |
|
26662 | 535 |
val all_thms = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39159
diff
changeset
|
536 |
map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (Global_Theory.facts_of thy))) |
14516 | 537 |
in |
33317 | 538 |
filter (match_consts ignored t) all_thms |
14516 | 539 |
end |
540 |
||
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42364
diff
changeset
|
541 |
fun gen_shuffle_tac ctxt search thms = SUBGOAL (fn (t, i) => |
14516 | 542 |
let |
42361 | 543 |
val thy = Proof_Context.theory_of ctxt |
21588 | 544 |
val set = set_prop thy t |
545 |
fun process_tac thms st = |
|
546 |
case set thms of |
|
547 |
SOME (_,th) => Seq.of_list (compose (th,i,st)) |
|
548 |
| NONE => Seq.empty |
|
14516 | 549 |
in |
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42364
diff
changeset
|
550 |
process_tac thms APPEND |
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42364
diff
changeset
|
551 |
(if search then process_tac (find_potential thy t) else no_tac) |
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42364
diff
changeset
|
552 |
end) |
14516 | 553 |
|
31244
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
554 |
fun shuffle_tac ctxt thms = |
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
555 |
gen_shuffle_tac ctxt false (map (pair "") thms); |
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
556 |
|
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
557 |
fun search_tac ctxt = |
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
558 |
gen_shuffle_tac ctxt true (map (pair "premise") (Assumption.all_prems_of ctxt)); |
14516 | 559 |
|
560 |
fun add_shuffle_rule thm thy = |
|
561 |
let |
|
21588 | 562 |
val shuffles = ShuffleData.get thy |
14516 | 563 |
in |
21588 | 564 |
if exists (curry Thm.eq_thm thm) shuffles |
565 |
then (warning ((string_of_thm thm) ^ " already known to the shuffler"); |
|
566 |
thy) |
|
567 |
else ShuffleData.put (thm::shuffles) thy |
|
14516 | 568 |
end |
569 |
||
20897 | 570 |
val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I); |
14516 | 571 |
|
18708 | 572 |
val setup = |
31241 | 573 |
Method.setup @{binding shuffle_tac} |
31244
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset
|
574 |
(Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt ths))) |
31241 | 575 |
"solve goal by shuffling terms around" #> |
576 |
Method.setup @{binding search_tac} |
|
577 |
(Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #> |
|
18708 | 578 |
add_shuffle_rule weaken #> |
579 |
add_shuffle_rule equiv_comm #> |
|
580 |
add_shuffle_rule imp_comm #> |
|
581 |
add_shuffle_rule Drule.norm_hhf_eq #> |
|
582 |
add_shuffle_rule Drule.triv_forall_equality #> |
|
30528 | 583 |
Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler"; |
18708 | 584 |
|
14516 | 585 |
end |