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