1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory SimpStrategy 8imports Main 9begin 10 11text \<open> 12Support for defining alternative simplifier strategies for some parts of terms 13or some premises of rewrite rules. The "name" parameter to the simp_strategy 14constant is used to identify which simplification strategy should be used on 15this term. Note that, although names have type nat, it is safe for them to all 16be defined as 0. The important thing is that the simplifier doesn't know they're 17equal. 18\<close> 19 20definition 21 simp_strategy :: "nat \<Rightarrow> ('a :: {}) \<Rightarrow> 'a" 22where 23 "simp_strategy name x \<equiv> x" 24 25text \<open> 26This congruence rule forbids the simplifier from simplifying the arguments of 27simp_strategy normally. 28\<close> 29 30lemma simp_strategy_cong[cong]: 31 "simp_strategy name x = simp_strategy name x" 32 by simp 33 34text \<open> 35This strategy, or rather lack thereof, can be used to forbid simplification. 36\<close> 37 38definition 39 NoSimp :: nat 40where "NoSimp = 0" 41 42text \<open> 43This strategy indicates that a boolean subterm should be simplified only by 44using explicit assumptions of the simpset. 45\<close> 46 47definition 48 ByAssum :: nat 49where "ByAssum = 0" 50 51lemma Eq_TrueI_ByAssum: 52 "P \<Longrightarrow> simp_strategy ByAssum P \<equiv> True" 53 by (simp add: simp_strategy_def) 54 55simproc_setup simp_strategy_ByAssum ("simp_strategy ByAssum b") = 56 \<open>K (fn ss => fn ct => let 57 val b = Thm.dest_arg ct 58 val t = Thm.instantiate ([],[((("P",0),@{typ bool}), b)]) 59 @{thm Eq_TrueI_ByAssum} 60 val prems = Raw_Simplifier.prems_of ss 61 in get_first (try (fn p => p RS t)) prems end)\<close> 62 63lemma ByAssum: 64 "simp_strategy ByAssum P \<Longrightarrow> P" 65 by (simp add: simp_strategy_def) 66 67lemma simp_ByAssum_test: 68 "P \<Longrightarrow> simp_strategy ByAssum P" 69 by simp 70 71text \<open> 72Generic framework for instantiating a simproc which simplifies within a 73simp_strategy with a given simpset. 74 75The boolean determines whether simp_strategy Name True should be rewritten 76to True. 77\<close> 78 79lemma simp_strategy_Eq_True: 80 "simp_strategy name True \<equiv> True" 81 by (simp add: simp_strategy_def) 82 83ML \<open> 84fun simp_strategy_True_conv ct = case Thm.term_of ct of 85 (Const (@{const_name simp_strategy}, _) $ _ $ @{term True}) 86 => Thm.instantiate ([], [((("name",0), @{typ nat}), Thm.dest_arg1 ct)]) 87 @{thm simp_strategy_Eq_True} 88 | _ => Conv.all_conv ct 89 90fun new_simp_strategy thy (name : term) ss rewr_True = 91let 92 val ctxt = Proof_Context.init_global thy; 93 val ss = Simplifier.make_simproc ctxt ("simp_strategy_" ^ fst (dest_Const name)) 94 {lhss = [@{term simp_strategy} $ name $ @{term x}], 95 proc = (fn _ => fn ctxt' => fn ct => 96 ct 97 |> (Conv.arg_conv (Simplifier.rewrite (put_simpset ss ctxt')) 98 then_conv (if rewr_True then simp_strategy_True_conv 99 else Conv.all_conv)) 100 |> (fn c => if Thm.is_reflexive c then NONE else SOME c)) 101 } 102in 103 ss 104end 105\<close> 106 107end 108