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