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