1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Try_Attribute
8imports Main
9begin
10
11ML \<open>
12local
13
14val parse_warn = Scan.lift (Scan.optional (Args.parens (Parse.reserved "warn") >> K true) false)
15
16val attribute_generic = Context.cases Attrib.attribute_global Attrib.attribute
17
18fun try_attribute_cmd (warn, attr_srcs) (ctxt, thm) =
19  let
20    val attrs = map (attribute_generic ctxt) attr_srcs
21    val (th', context') =
22      fold (uncurry o Thm.apply_attribute) attrs (thm, ctxt)
23      handle e =>
24        (if Exn.is_interrupt e then Exn.reraise e
25         else if warn then warning ("TRY: ignoring exception: " ^ (@{make_string} e))
26         else ();
27        (thm, ctxt))
28  in (SOME context', SOME th') end
29
30in
31
32val _ = Theory.setup
33  (Attrib.setup @{binding TRY}
34    (parse_warn -- Attrib.attribs >> try_attribute_cmd)
35    "higher order attribute combinator to try other attributes, ignoring failure")
36
37end
38\<close>
39
40text \<open>
41  The @{attribute TRY} attribute is an attribute combinator that applies other
42  attributes, ignoring any failures by returning the original state. Note that since attributes
43  are applied separately to each theorem in a theorem list, @{attribute TRY} will leave
44  failing theorems unchanged while modifying the rest.
45
46  Accepts a "warn" flag to print any errors encountered.
47
48  Usage:
49    thm foo[TRY [<attributes>]]
50
51    thm foo[TRY (warn) [<attributes>]]
52\<close>
53
54section \<open>Examples\<close>
55
56experiment begin
57  lemma eq1: "(1 :: nat) = 1 + 0" by simp
58  lemma eq2: "(2 :: nat) = 1 + 1" by simp
59
60  lemmas eqs = eq1 TrueI eq2
61
62  text \<open>
63    `eqs[symmetric]` would fail because there are no unifiers with @{term True}, but
64    @{attribute TRY} ignores that.
65  \<close>
66  lemma
67    "1 + 0 = (1 :: nat)"
68    "True"
69    "1 + 1 = (2 :: nat)"
70    by (rule eqs[TRY [symmetric]])+
71
72  text \<open>
73    You can chain calls to @{attribute TRY} at the top level, to apply different attributes to
74    different theorems.
75  \<close>
76  lemma ineq: "(1 :: nat) < 2" by simp
77  lemmas ineqs = eq1 ineq
78  lemma
79    "1 + 0 = (1 :: nat)"
80    "(1 :: nat) \<le> 2"
81    by (rule ineqs[TRY [symmetric], TRY [THEN order.strict_implies_order]])+
82
83  text \<open>
84    You can chain calls to @{attribute TRY} within each other, to chain more attributes onto
85    particular theorems.
86  \<close>
87  lemmas more_eqs = eq1 eq2
88  lemma
89    "1 = (1 :: nat)"
90    "1 + 1 = (2 :: nat)"
91    by (rule more_eqs[TRY [symmetric, TRY [simplified add_0_right]]])+
92
93  text \<open>
94    The 'warn' flag will print out any exceptions encountered. Since @{attribute symmetric}
95    doesn't apply to @{term True} or @{term "(1 :: nat) < 2"}, this will log two errors.
96  \<close>
97  lemmas yet_another_group = eq1 TrueI eq2 ineq
98  thm yet_another_group[TRY (warn) [symmetric]]
99
100  text \<open>@{attribute TRY} should handle pretty much anything it might encounter.\<close>
101  thm eq1[TRY (warn) [where x=5]]
102  thm eq1[TRY (warn) [OF refl]]
103end
104
105end