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