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