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