478 |
478 |
479 (* simplification *) |
479 (* simplification *) |
480 |
480 |
481 val colon = Args.$$$ ":"; |
481 val colon = Args.$$$ ":"; |
482 |
482 |
|
483 val simp_options = |
|
484 (Args.$$$ "no_asm" -- colon >> K simp_tac || |
|
485 Args.$$$ "no_asm_simp" -- colon >> K asm_simp_tac || |
|
486 Args.$$$ "no_asm_use" -- colon >> K full_simp_tac || |
|
487 Scan.succeed asm_full_simp_tac); |
|
488 |
483 val simp_modifiers = |
489 val simp_modifiers = |
484 [Args.$$$ simpN -- colon >> K (I, simp_add_local), |
490 [Args.$$$ simpN -- colon >> K (I, simp_add_local), |
485 Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local), |
491 Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local), |
486 Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local), |
492 Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local), |
487 Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local), |
493 Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local), |
491 [Args.$$$ addN -- colon >> K (I, simp_add_local), |
497 [Args.$$$ addN -- colon >> K (I, simp_add_local), |
492 Args.$$$ delN -- colon >> K (I, simp_del_local), |
498 Args.$$$ delN -- colon >> K (I, simp_del_local), |
493 Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local), |
499 Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local), |
494 Args.$$$ otherN -- colon >> K (I, I)]; |
500 Args.$$$ otherN -- colon >> K (I, I)]; |
495 |
501 |
496 fun simp_method more_mods tac = |
502 fun simp_args more_mods = |
497 (fn prems => fn ctxt => Method.METHOD (fn facts => |
503 Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers'); |
498 ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_simpset ctxt))) |
504 |
499 |> Method.bang_sectioned_args (more_mods @ simp_modifiers'); |
505 |
500 |
506 fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts => |
501 fun simp_method' more_mods tac = |
507 ALLGOALS (Method.insert_tac (prems @ facts)) THEN |
502 (fn prems => fn ctxt => Method.METHOD (fn facts => |
508 (CHANGED o ALLGOALS o tac) (get_local_simpset ctxt)); |
503 HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) |
509 |
504 |> Method.bang_sectioned_args (more_mods @ simp_modifiers'); |
510 fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts => |
|
511 HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt))); |
505 |
512 |
506 |
513 |
507 (* setup_methods *) |
514 (* setup_methods *) |
508 |
515 |
509 fun setup_methods more_mods = Method.add_methods |
516 fun setup_methods more_mods = Method.add_methods |
510 [(simpN, simp_method' more_mods |
517 [(simpN, simp_args more_mods simp_method', "simplification"), |
511 (CHANGED oo asm_full_simp_tac), "full simplification"), |
518 ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")]; |
512 ("simp_all", simp_method more_mods (CHANGED o ALLGOALS o asm_full_simp_tac), |
|
513 "full simplification (all goals)"), |
|
514 ("simp_tac", simp_method' more_mods simp_tac, "simp_tac (improper!)"), |
|
515 ("asm_simp_tac", simp_method' more_mods asm_simp_tac, "asm_simp_tac (improper!)"), |
|
516 ("full_simp_tac", simp_method' more_mods full_simp_tac, "full_simp_tac (improper!)"), |
|
517 ("asm_full_simp_tac", simp_method' more_mods asm_full_simp_tac, "asm_full_simp_tac (improper!)"), |
|
518 ("asm_lr_simp_tac", simp_method' more_mods asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")]; |
|
519 |
519 |
520 |
520 |
521 |
521 |
522 (** theory setup **) |
522 (** theory setup **) |
523 |
523 |