1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Simp_No_Conditional
8
9imports Main
10
11begin
12
13text \<open>
14Simplification without conditional rewriting. Setting the simplifier depth
15limit to zero prevents attempts at conditional rewriting. This should make
16the simplifier faster and more predictable on average. It may be particularly
17useful in derived tactics and methods to avoid situations where the simplifier
18repeatedly attempts and fails a conditional rewrite.
19
20As always, there are caveats. Failing to perform a simple conditional rewrite
21may open the door to expensive alternatives. Various simprocs which are
22conditional in nature will not be deactivated.
23\<close>
24
25ML \<open>
26
27structure Simp_No_Conditional = struct
28
29val set_no_cond = Config.put Raw_Simplifier.simp_depth_limit 0
30
31val simp_tac = Simplifier.simp_tac o set_no_cond
32val asm_simp_tac = Simplifier.asm_simp_tac o set_no_cond
33val full_simp_tac = Simplifier.full_simp_tac o set_no_cond
34val asm_full_simp_tac = Simplifier.asm_full_simp_tac o set_no_cond
35
36val clarsimp_tac = Clasimp.clarsimp_tac o set_no_cond
37val auto_tac = Clasimp.auto_tac o set_no_cond
38
39fun mk_method secs tac
40    = Method.sections secs >> K (SIMPLE_METHOD' o tac)
41val mk_clasimp_method = mk_method Clasimp.clasimp_modifiers
42
43fun mk_clasimp_all_method tac =
44    Method.sections Clasimp.clasimp_modifiers >> K (SIMPLE_METHOD o tac)
45
46val simp_method = mk_method Simplifier.simp_modifiers
47    (CHANGED_PROP oo asm_full_simp_tac)
48val clarsimp_method = mk_clasimp_method (CHANGED_PROP oo clarsimp_tac)
49val auto_method = mk_clasimp_all_method (CHANGED_PROP o auto_tac)
50
51end
52
53\<close>
54
55method_setup simp_no_cond = \<open>Simp_No_Conditional.simp_method\<close>
56    "Simplification with no conditional simplification."
57
58method_setup clarsimp_no_cond = \<open>Simp_No_Conditional.clarsimp_method\<close>
59    "Clarsimp with no conditional simplification."
60
61method_setup auto_no_cond = \<open>Simp_No_Conditional.auto_method\<close>
62    "Auto with no conditional simplification."
63
64end
65