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