# 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