1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Repeat_Attribute 8imports Main 9begin 10 11ML \<open> 12local 13 14val attribute_generic = Context.cases Attrib.attribute_global Attrib.attribute 15 16fun apply_attributes attrs thm ctxt = 17 let 18 val (thm', ctxt') = fold (uncurry o Thm.apply_attribute) attrs (thm, ctxt) 19 in if Thm.eq_thm (thm, thm') 20 then (SOME ctxt', SOME thm) 21 else 22 apply_attributes attrs thm' ctxt' 23 handle e => 24 (if Exn.is_interrupt e then Exn.reraise e else (); 25 (SOME ctxt', SOME thm')) 26 end 27 28fun repeat_attribute_cmd attr_srcs (ctxt, thm) = 29 let val attrs = map (attribute_generic ctxt) attr_srcs 30 in apply_attributes attrs thm ctxt end 31 32in 33 34val _ = Theory.setup 35 (Attrib.setup @{binding REPEAT} 36 (Attrib.attribs >> repeat_attribute_cmd) 37 "higher order attribute combinator to repeatedly apply other attributes one or more times") 38 39end 40\<close> 41 42text \<open> 43 44 The @{attribute REPEAT} attribute is an attribute combinator that repeatedly applies 45 other attributes one or more times. It will stop applying the attributes once they can 46 either no longer be applied, or if applying them would not change the theorem being 47 modified. 48 49 Usage: 50 thm foo[REPEAT [<attributes>]] 51 52\<close> 53 54section \<open>Examples\<close> 55 56experiment begin 57 lemma test1: "True \<Longrightarrow> True" . 58 lemma test2: "True \<Longrightarrow> True \<Longrightarrow> True" . 59 lemmas tests = test1 test2 60 text \<open> 61 `tests[OF TrueI]` would only discharge one of the assumptions of @{thm test2}, but 62 @{attribute REPEAT} handles both cases. 63 \<close> 64 thm tests[REPEAT [OF TrueI]] 65 66 text \<open> 67 @{attribute REPEAT} succesfully terminates when applying an attribute that could loop, 68 such as @{attribute simplified} and @{attribute simp}. Importantly, it still updates 69 the context if necessary, in this case by adding P to the simp set. 70 \<close> 71 lemma 72 assumes P[REPEAT [simplified], REPEAT [simp]]: "P \<or> False" 73 shows P 74 by simp 75 76end 77 78end 79