64 val Delsimprocs: simproc list -> unit |
64 val Delsimprocs: simproc list -> unit |
65 |
65 |
66 val simp_tac: simpset -> int -> tactic |
66 val simp_tac: simpset -> int -> tactic |
67 val asm_simp_tac: simpset -> int -> tactic |
67 val asm_simp_tac: simpset -> int -> tactic |
68 val full_simp_tac: simpset -> int -> tactic |
68 val full_simp_tac: simpset -> int -> tactic |
|
69 val asm_lr_simp_tac: simpset -> int -> tactic |
69 val asm_full_simp_tac: simpset -> int -> tactic |
70 val asm_full_simp_tac: simpset -> int -> tactic |
70 val safe_asm_full_simp_tac: simpset -> int -> tactic |
71 val safe_asm_full_simp_tac: simpset -> int -> tactic |
71 val Simp_tac: int -> tactic |
72 val Simp_tac: int -> tactic |
72 val Asm_simp_tac: int -> tactic |
73 val Asm_simp_tac: int -> tactic |
73 val Full_simp_tac: int -> tactic |
74 val Full_simp_tac: int -> tactic |
|
75 val Asm_lr_simp_tac: int -> tactic |
74 val Asm_full_simp_tac: int -> tactic |
76 val Asm_full_simp_tac: int -> tactic |
75 val simplify: simpset -> thm -> thm |
77 val simplify: simpset -> thm -> thm |
76 val asm_simplify: simpset -> thm -> thm |
78 val asm_simplify: simpset -> thm -> thm |
77 val full_simplify: simpset -> thm -> thm |
79 val full_simplify: simpset -> thm -> thm |
78 val asm_full_simplify: simpset -> thm -> thm |
80 val asm_full_simplify: simpset -> thm -> thm |
324 |
326 |
325 |
327 |
326 val simp_tac = gen_simp_tac (false, false, false); |
328 val simp_tac = gen_simp_tac (false, false, false); |
327 val asm_simp_tac = gen_simp_tac (false, true, false); |
329 val asm_simp_tac = gen_simp_tac (false, true, false); |
328 val full_simp_tac = gen_simp_tac (true, false, false); |
330 val full_simp_tac = gen_simp_tac (true, false, false); |
329 val asm_full_simp_tac = gen_simp_tac (true, true, false); |
331 val asm_lr_simp_tac = gen_simp_tac (true, true, false); |
|
332 val asm_full_simp_tac = gen_simp_tac (true, true, true); |
330 |
333 |
331 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
334 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
332 val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true, false); |
335 val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true, false); |
333 |
336 |
334 (** The abstraction over the proof state delays the dereferencing **) |
337 (** The abstraction over the proof state delays the dereferencing **) |
335 |
338 |
336 fun Simp_tac i st = simp_tac (simpset ()) i st; |
339 fun Simp_tac i st = simp_tac (simpset ()) i st; |
337 fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st; |
340 fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st; |
338 fun Full_simp_tac i st = full_simp_tac (simpset ()) i st; |
341 fun Full_simp_tac i st = full_simp_tac (simpset ()) i st; |
|
342 fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st; |
339 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st; |
343 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st; |
340 |
344 |
341 |
345 |
342 (** simplification meta rules **) |
346 (** simplification meta rules **) |
343 |
347 |