# HG changeset patch
# User nipkow
# Date 1716972202 -7200
# Node ID ca7e7e41374e582483a8bd8d327c4554f0509b9a
# Parent  5f053991315c4cd8c712743663d699d0b320c0bb
pretty-printing sledgehammer command: merge indexed theorems

diff -r 5f053991315c -r ca7e7e41374e src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat May 25 20:26:06 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed May 29 10:43:22 2024 +0200
@@ -93,6 +93,32 @@
 
 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
 
+(*
+Combine indexed fact names for pretty-printing.
+Example: [... "assms(1)" "assms(3)" ...] becomes [... "assms(1,3)" ...]
+Combines only adjacent same names.
+Input should not have same name with and without index.
+*)
+fun merge_indexed_facts (ss: string list) :string list =
+  let
+
+    fun split (s: string) : string * string =
+      case first_field "(" s of
+        NONE => (s,"")
+      | SOME (name,isp) => (name, String.substring (isp, 0, size isp - 1))
+
+    fun merge ((name1,is1) :: (name2,is2) :: zs) =
+        if name1 = name2
+        then merge ((name1,is1 ^ "," ^ is2) :: zs)
+        else (name1,is1) :: merge ((name2,is2) :: zs)
+      | merge xs = xs;
+
+    fun parents is = if is = "" then "" else "(" ^ is ^ ")"
+
+  in
+    map (fn (name,is) => name ^ parents is) (merge (map split ss))
+  end
+
 fun string_of_proof_method ss meth =
   let
     val meth_s =
@@ -117,7 +143,7 @@
       | Algebra_Method => "algebra"
       | Order_Method => "order")
   in
-    maybe_paren (space_implode " " (meth_s :: ss))
+    maybe_paren (space_implode " " (meth_s :: merge_indexed_facts ss))
   end
 
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
@@ -182,7 +208,8 @@
     val (indirect_ss, direct_ss) =
       if is_proof_method_direct meth then ([], extras) else (extras, [])
   in
-    (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
+    (if null indirect_ss then ""
+     else "using " ^ space_implode " " (merge_indexed_facts indirect_ss) ^ " ") ^
     apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^
     (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
   end