used more descriptive assert names in SMT-Lib output

--- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -24,7 +24,8 @@
       val id_of_index = Integer.add num_ll_defs
       val index_of_id = Integer.add (~ num_ll_defs)
 
-      val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
+      val used_assert_ids =
+        map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output
       val used_assm_js =
         map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
           used_assert_ids

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -15,7 +15,7 @@
 
   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   val add_extra_norm: SMT_Util.class * extra_norm -> Context.generic -> Context.generic
-  val normalize: Proof.context -> thm list -> (int * thm) list
+  val normalize: Proof.context -> (SMT_Util.role * thm) list -> ((int * SMT_Util.role) * thm) list
 end;
 
 structure SMT_Normalize: SMT_NORMALIZE =
@@ -448,7 +448,7 @@
   let
     val (is, thms) = split_list ithms
     val (thms', extra_thms) = f thms
-  in (is ~~ thms') @ map (pair ~1) extra_thms end
+  in (is ~~ thms') @ map (pair (~1, SMT_Util.Axiom)) extra_thms end
 
 fun unfold_conv ctxt =
   rewrite_case_bool_conv ctxt then_conv
@@ -515,7 +515,7 @@
 
 fun normalize ctxt wthms =
   wthms
-  |> map_index I
+  |> map_index (fn (n, (role, thm)) => ((n, role), thm))
   |> gen_normalize ctxt
   |> unfold_polymorph ctxt
   |> monomorph ctxt

--- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -249,7 +249,7 @@
 
 fun apply_solver_and_replay ctxt thms0 =
   let
-    val thms = map (check_topsort ctxt) thms0
+    val thms = map (pair SMT_Util.Axiom o check_topsort ctxt) thms0
     val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt
     val (output, replay_data) =
       invoke name command [] smt_options (SMT_Normalize.normalize ctxt thms) ctxt
@@ -270,13 +270,15 @@
       | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal"))
 
     val conjecture = Thm.assume cprop
-    val facts = map snd xfacts
-    val thms = conjecture :: prems @ facts
-    val thms' = map (check_topsort ctxt) thms
+    val thms =
+      (SMT_Util.Conjecture, conjecture) ::
+      map (pair SMT_Util.Hypothesis) prems @
+      map (pair SMT_Util.Axiom o snd) xfacts
+      |> map (apsnd (check_topsort ctxt))
 
     val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt
     val (output, replay_data) =
-      invoke name command options smt_options (SMT_Normalize.normalize ctxt thms') ctxt
+      invoke name command options smt_options (SMT_Normalize.normalize ctxt thms) ctxt
   in
     parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
   end

--- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -24,7 +24,8 @@
     order: SMT_Util.order,
     logic: string -> term list -> string,
     fp_kinds: BNF_Util.fp_kind list,
-    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
+    serialize: (string * string) list -> string list -> sign -> (SMT_Util.role * sterm) list ->
+      string }
   type replay_data = {
     context: Proof.context,
     typs: typ Symtab.table,
@@ -35,7 +36,8 @@
 
   (*translation*)
   val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
-  val translate: Proof.context -> string -> (string * string) list -> string list -> (int * thm) list ->
+  val translate: Proof.context -> string -> (string * string) list -> string list ->
+    ((int * SMT_Util.role) * thm) list ->
     string * replay_data
 end;
 
@@ -68,7 +70,8 @@
   order: SMT_Util.order,
   logic: string -> term list -> string,
   fp_kinds: BNF_Util.fp_kind list,
-  serialize: (string * string) list -> string list -> sign -> sterm list -> string }
+  serialize: (string * string) list -> string list -> sign -> (SMT_Util.role * sterm) list ->
+    string }
 
 type replay_data = {
   context: Proof.context,
@@ -130,7 +133,7 @@
     val terms' = Termtab.fold add_fun terms Symtab.empty
   in
     {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules,
-     assms = assms}
+     assms = map (apfst fst) assms}
   end
 
 
@@ -142,7 +145,7 @@
   let
     val (fp_decls, ctxt') =
       ([], ctxt)
-      |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts
+      |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds) o snd) ts
       |>> flat
 
     fun is_decl_typ T = exists (equal T o fst o snd) fp_decls
@@ -228,7 +231,7 @@
 
     and abs_expand (n, T, t) = Abs (n, T, expand t)
 
-  in map expand end
+  in map (apsnd expand) end
 
 end
 
@@ -277,7 +280,7 @@
       | n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^
           ": " ^ string_of_int n))
 
-    val (arities, types) = fold get_arities ts (Termtab.empty, Typtab.empty)
+    val (arities, types) = fold (get_arities o snd) ts (Termtab.empty, Typtab.empty)
     val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types)
 
     fun app_func t T ts =
@@ -314,7 +317,7 @@
       | in_pat Ts ((p as \<^Const_>\<open>nopat _\<close>) $ t) = p $ traverse Ts t
       | in_pat _ t = raise TERM ("bad pattern", [t])
     and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
-  in map (traverse []) ts end
+  in map (apsnd (traverse [])) ts end
 
 val fun_app_eq = mk_meta_eq @{thm fun_app_def}
 
@@ -381,7 +384,7 @@
               | NONE => in_term false t))
       | _ => in_term false t)
   in
-    map in_form #>
+    map (apsnd in_form) #>
     pair (fol_rules, I)
   end
 
@@ -463,7 +466,7 @@
           add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
       end
 
-    val (us, trx') = fold_map trans ts trx
+    val (us, trx') = fold_map (fn (role, t) => apfst (pair role) o trans t) ts trx
   in ((sign_of (logic ts) dtyps trx', us), trx') end
 
 
@@ -487,14 +490,14 @@
         "for solver class " ^ quote (SMT_Util.string_of_class cs)))
   end
 
-fun translate ctxt prover smt_options comments ithms =
+fun translate ctxt prover smt_options comments (ithms : ((int * SMT_Util.role) * thm) list) =
   let
     val {order, logic, fp_kinds, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
 
-    val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms
+    val ts1 = map (SMT_Util.map_prod snd (Envir.beta_eta_contract o SMT_Util.prop_of)) ithms
 
     val ((funcs, dtyps, tr_context, ctxt1), ts2) =
       ((empty_tr_context, ctxt), ts1)
@@ -517,10 +520,10 @@
       ts2
       |> eta_expand ctxt1 funcs
       |> rpair ctxt1
-      |-> Lambda_Lifting.lift_lambdas NONE is_binder
+      |-> Lambda_Lifting.lift_lambdas' NONE is_binder
       |-> (fn (ts', ll_defs) => fn ctxt' =>
         let
-          val ts'' = map mk_trigger ll_defs @ ts'
+          val ts'' = map (pair SMT_Util.Axiom o mk_trigger) ll_defs @ ts'
             |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
         in
           (ctxt', (ts'', ll_defs))
@@ -529,7 +532,7 @@
       |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
-    |-> intermediate (logic prover) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
+    |-> intermediate (logic prover o map snd) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
     |>> uncurry (serialize smt_options comments)
     ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
   end

--- a/src/HOL/Tools/SMT/smt_util.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -9,8 +9,10 @@
   (*basic combinators*)
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
+  val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> ('b * 'd)
 
   datatype order = First_Order | Higher_Order
+  datatype role = Conjecture | Hypothesis | Axiom
 
   (*class dictionaries*)
   type class = string list
@@ -78,12 +80,19 @@
   let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
   in rep end
 
+val map_prod = Ctr_Sugar_Util.map_prod
+
 
 (* order *)
 
 datatype order = First_Order | Higher_Order
 
 
+(* role *)
+
+ datatype role = Conjecture | Hypothesis | Axiom
+
+
 (* class dictionaries *)
 
 type class = string list

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -13,9 +13,8 @@
   val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
-  val assert_name_of_index: int -> string
-  val assert_index_of_name: string -> int
-  val assert_prefix : string
+  val assert_name_of_role_and_index: SMT_Util.role -> int -> string
+  val role_and_index_of_assert_name: string -> SMT_Util.role * int
 end;
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -137,10 +136,24 @@
 
 fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
 
-val assert_prefix = "a"
+val conjecture_prefix = "conjecture" (* FUDGE *)
+val hypothesis_prefix = "hypothesis" (* FUDGE *)
+val axiom_prefix = "axiom" (* FUDGE *)
+
+fun assert_prefix_of_role SMT_Util.Conjecture = conjecture_prefix
+  | assert_prefix_of_role SMT_Util.Hypothesis = hypothesis_prefix
+  | assert_prefix_of_role SMT_Util.Axiom = axiom_prefix
 
-fun assert_name_of_index i = assert_prefix ^ string_of_int i
-fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
+fun assert_name_of_role_and_index role i = assert_prefix_of_role role ^ string_of_int i
+
+fun unprefix_axiom s =
+  try (pair SMT_Util.Conjecture o unprefix conjecture_prefix) s
+  |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix hypothesis_prefix) s)
+  |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix axiom_prefix) s)
+  |> the
+
+fun role_and_index_of_assert_name s =
+  apsnd (the_default ~1 o Int.fromString) (unprefix_axiom s)
 
 fun sdtyp (fp, dtyps) =
   Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
@@ -158,8 +171,9 @@
     |> fold sdtyp (AList.coalesce (op =) dtyps)
     |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
         (sort (fast_string_ord o apply2 fst) funcs)
-    |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
-        (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
+    |> fold (fn (i, (role, t)) => Buffer.add (enclose "(assert " ")\n"
+        (SMTLIB.str_of (named_sterm (assert_name_of_role_and_index role i) (tree_of_sterm 0 t)))))
+        (map_index I ts)
     |> Buffer.add "(check-sat)\n"
     |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n")
     |> Buffer.content

--- a/src/HOL/Tools/SMT/verit_isar.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -34,7 +34,7 @@
       in
         if rule = input_rule then
           let
-            val id_num = the (Int.fromString (unprefix assert_prefix id))
+            val id_num = snd (SMTLIB_Interface.role_and_index_of_assert_name id)
             val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
           in
             (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids

--- a/src/HOL/Tools/SMT/verit_proof.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -483,13 +483,13 @@
   end
 
 fun normalized_rule_name id rule =
-  (case (rule = input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
+  (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of
     (true, true) => normalized_input_rule
   | (true, _) => local_input_rule
   | _ => rule)
 
 fun is_assm_repetition id rule =
-  rule = input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
+  rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id
 
 fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
   | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)

--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -24,7 +24,7 @@
 open Verit_Proof
 
 fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) =
-  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems)
+  union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems)
 
 fun parse_proof
     ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data)
@@ -36,7 +36,8 @@
     val index_of_id = Integer.add (~ num_ll_defs)
 
     fun step_of_assume j (_, th) =
-      Verit_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
+      Verit_Proof.VeriT_Step
+        {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
         rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
 
     val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt

--- a/src/HOL/Tools/SMT/verit_replay.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -79,12 +79,12 @@
 
 fun add_used_asserts_in_step (Verit_Proof.VeriT_Replay_Node {prems,
     subproof = (_, _, _, subproof), ...}) =
-  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems @
+  union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems @
      flat (map (fn x => add_used_asserts_in_step x []) subproof))
 
 fun remove_rewrite_rules_from_rules n =
   (fn (step as Verit_Proof.VeriT_Replay_Node {id, ...}) =>
-    (case try SMTLIB_Interface.assert_index_of_name id of
+    (case try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id of
       NONE => SOME step
     | SOME a => if a < n then NONE else SOME step))
 
@@ -245,7 +245,7 @@
 
     fun step_of_assume (j, (_, th)) =
       Verit_Proof.VeriT_Replay_Node {
-        id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
+        id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
         rule = Verit_Proof.input_rule,
         args = [],
         prems = [],
@@ -280,10 +280,13 @@
           then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end)
         used_assert_ids
     val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) =>
-           let val (thm, stats) = replay_assumed assms ll_defs rewrite_rules stats ctxt thm
-           in (Symtab.update (SMTLIB_Interface.assert_name_of_index id, ([], thm)) assumed, stats)
-           end)
-         used_rew_js (assumed, Symtab.cons_list ("parsing", parsing_time) Symtab.empty)
+      let
+        val (thm, stats) = replay_assumed assms ll_defs rewrite_rules stats ctxt thm
+        val name = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom id
+      in
+        (Symtab.update (name, ([], thm)) assumed, stats)
+      end)
+      used_rew_js (assumed, Symtab.cons_list ("parsing", parsing_time) Symtab.empty)
 
     val ctxt4 =
       ctxt3

--- a/src/HOL/Tools/lambda_lifting.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/lambda_lifting.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -16,6 +16,8 @@
   val finish: context -> term list * Proof.context
   val lift_lambdas: string option -> (term -> bool) -> term list ->
     Proof.context -> (term list * term list) * Proof.context
+  val lift_lambdas': string option -> (term -> bool) -> ('a * term) list ->
+    Proof.context -> (('a * term) list * term list) * Proof.context
 end
 
 structure Lambda_Lifting: LAMBDA_LIFTING =
@@ -87,4 +89,9 @@
   |> fold_map (lift_lambdas1 is_binder basename) ts
   |-> (fn ts' => finish #>> pair ts')
 
+fun lift_lambdas' basename is_binder ts ctxt =
+  init ctxt
+  |> fold_map (fn (x, t) => apfst (pair x) o lift_lambdas1 is_binder basename t) ts
+  |-> (fn ts' => finish #>> pair ts')
+
 end