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