1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Find_Names
8imports Pure
9keywords "find_names" :: diag
10begin
11
12text \<open>The @{command find_names} command, when given a theorem,
13  finds other names the theorem appears under, via matching on the whole
14  proposition. It will not identify unnamed theorems.\<close>
15
16ML \<open>
17
18local
19(* all_facts_of and pretty_ref taken verbatim from non-exposed version
20   in Find_Theorems.ML of official Isabelle/HOL distribution *)
21fun all_facts_of ctxt =
22  let
23    val thy = Proof_Context.theory_of ctxt;
24    val transfer = Global_Theory.transfer_theories thy;
25    val local_facts = Proof_Context.facts_of ctxt;
26    val global_facts = Global_Theory.facts_of thy;
27  in
28   (Facts.dest_all (Context.Proof ctxt) false [global_facts] local_facts
29    @ Facts.dest_all (Context.Proof ctxt) false [] global_facts)
30   |> maps Facts.selections
31   |> map (apsnd transfer)
32  end;
33
34fun pretty_ref ctxt thmref =
35  let
36    val (name, sel) =
37      (case thmref of
38        Facts.Named ((name, _), sel) => (name, sel)
39      | Facts.Fact _ => raise Fail "Illegal literal fact");
40  in
41    [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name),
42      Pretty.str (Facts.string_of_selection sel)]
43  end;
44
45in
46
47fun find_names ctxt thm =
48  let
49    fun eq_filter body thmref = (body = Thm.full_prop_of (snd thmref));
50  in
51    (filter (eq_filter (Thm.full_prop_of thm))) (all_facts_of ctxt)
52    |> map #1
53  end;
54
55fun pretty_find_names ctxt thm =
56  let
57    val results = find_names ctxt thm;
58    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
59  in
60    ((Pretty.mark position_markup (Pretty.keyword1 "find_names")) ::
61      Par_List.map (Pretty.item o (pretty_ref ctxt)) results)
62    |> Pretty.fbreaks |> Pretty.block |> Pretty.writeln
63  end
64
65end
66
67val _ =
68  Outer_Syntax.command @{command_keyword find_names}
69    "find other names of a named theorem"
70    (Parse.thms1 >> (fn srcs => Toplevel.keep (fn st =>
71      pretty_find_names (Toplevel.context_of st)
72        (hd (Attrib.eval_thms (Toplevel.context_of st) srcs)))));
73\<close>
74
75end
76