1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Miscellaneous Isabelle tools. *) 8theory NICTATools 9imports 10 Apply_Trace_Cmd 11 Apply_Debug 12 Find_Names 13 (* Solves_Tac *) 14 Rule_By_Method 15 Eisbach_Methods 16 TSubst 17 Time_Methods_Cmd 18 Try_Attribute 19 Repeat_Attribute 20 Trace_Schematic_Insts 21 Insulin 22 ShowTypes 23 AutoLevity_Hooks 24 Locale_Abbrev 25begin 26 27section "Detect unused meta-forall" 28 29(* 30 * Detect meta-foralls that are unused in "lemma" statements, 31 * and warn the user about them. 32 * 33 * They can sometimes create weird issues, usually due to the 34 * fact that they have the empty sort "'a::{}", which confuses 35 * certain tools, such as "atomize". 36 *) 37ML \<open> 38 39(* Return a list of meta-forall variable names that appear 40 * to be unused in the input term. *) 41fun find_unused_metaall (Const (@{const_name "Pure.all"}, _) $ Abs (n, _, t)) = 42 (if not (Term.is_dependent t) then [n] else []) @ find_unused_metaall t 43 | find_unused_metaall (Abs (_, _, t)) = 44 find_unused_metaall t 45 | find_unused_metaall (a $ b) = 46 find_unused_metaall a @ find_unused_metaall b 47 | find_unused_metaall _ = [] 48 49(* Given a proof state, analyse its assumptions for unused 50 * meta-foralls. *) 51fun detect_unused_meta_forall _ (state : Proof.state) = 52let 53 (* Fetch all assumptions and the main goal, and analyse them. *) 54 val {context = lthy, goal = goal, ...} = Proof.goal state 55 val checked_terms = 56 [Thm.concl_of goal] @ map Thm.term_of (Assumption.all_assms_of lthy) 57 val results = List.concat (map find_unused_metaall checked_terms) 58 59 (* Produce a message. *) 60 fun message results = 61 Pretty.paragraph [ 62 Pretty.str "Unused meta-forall(s): ", 63 Pretty.commas 64 (map (fn b => Pretty.mark_str (Markup.bound, b)) results) 65 |> Pretty.paragraph, 66 Pretty.str "." 67 ] 68 69 (* We use a warning instead of the standard mechanisms so that 70 * we can produce a "warning" icon in Isabelle/jEdit. *) 71 val _ = 72 if length results > 0 then 73 warning (message results |> Pretty.string_of) 74 else () 75in 76 (false, ("", [])) 77end 78 79(* Setup the tool, stealing the "auto_solve_direct" option. *) 80val _ = Try.tool_setup ("unused_meta_forall", 81 (1, @{system_option auto_solve_direct}, detect_unused_meta_forall)) 82\<close> 83 84lemma test_unused_meta_forall: "\<And>x. y \<or> \<not> y" 85 oops 86 87(* Hide rules used by Trace_Schematic_Insts from apply_trace. *) 88lemmas [no_trace] = 89 data_stash.elim data_stash.proof_state_add data_stash.proof_state_remove data_stash.rule_add 90 91end 92