# HG changeset patch
# User blanchet
# Date 1743432794 -7200
# Node ID 0f8a51fedae6bc1d2fce0a7ef34203c76c7cba90
# Parent  7ed32d7f83175ce9078f0e20cf59fab34bf5c636
garbage collection

diff -r 7ed32d7f8317 -r 0f8a51fedae6 src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Mon Mar 31 10:15:48 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      HOL/Tools/SMT/verit_isar.ML
-    Author:     Mathias Fleury, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-
-VeriT proofs as generic ATP proofs for Isar proof reconstruction.
-*)
-
-signature VERIT_ISAR =
-sig
-  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
-  val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
-    (string * term) list -> int list -> int -> (int * string) list -> Verit_Proof.veriT_step list ->
-    (term, string) ATP_Proof.atp_step list
-end;
-
-structure VeriT_Isar: VERIT_ISAR =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open SMTLIB_Interface
-open SMTLIB_Isar
-open Verit_Proof
-
-fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
-    conjecture_id fact_helper_ids =
-  let
-    fun steps_of (Verit_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
-      let
-        val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
-        fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
-      in
-        if rule = input_rule then
-          let
-            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
-                fact_helper_ts hyp_ts concl_t of
-              NONE => []
-            | SOME (role0, concl00) =>
-              let
-                val name0 = (id ^ "a", ss)
-                val concl0 = unskolemize_names ctxt concl00
-              in
-                [(name0, role0, concl0, rule, []),
-                 ((id, []), Plain, concl', rewrite_rule,
-                  name0 :: normalizing_prems ctxt concl0)]
-              end)
-          end
-        else
-          [standard_step (if null prems then Lemma else Plain)]
-      end
-  in
-    maps steps_of
-  end
-
-end;
diff -r 7ed32d7f8317 -r 0f8a51fedae6 src/HOL/Tools/SMT/verit_proof_parse.ML
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Mon Mar 31 10:15:48 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(*  Title:      HOL/Tools/SMT/verit_proof_parse.ML
-    Author:     Mathias Fleury, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-
-VeriT proof parsing.
-*)
-
-signature VERIT_PROOF_PARSE =
-sig
-  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
-  val parse_proof: SMT_Translate.replay_data ->
-    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
-    SMT_Solver.parsed_proof
-end;
-
-structure VeriT_Proof_Parse: VERIT_PROOF_PARSE =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open VeriT_Isar
-open Verit_Proof
-
-fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {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)
-    xfacts prems concl output =
-  let
-    val num_ll_defs = length ll_defs
-
-    val id_of_index = Integer.add num_ll_defs
-    val index_of_id = Integer.add (~ num_ll_defs)
-
-    fun step_of_assume j ((_, role), th) =
-      Verit_Proof.VeriT_Step
-        {id = SMTLIB_Interface.assert_name_of_role_and_index role (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
-    val used_assert_ids = fold add_used_asserts_in_step actual_steps []
-    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
-    val used_assms = map (nth assms) used_assm_js
-    val assm_steps = map2 step_of_assume used_assm_js used_assms
-    val steps = assm_steps @ actual_steps
-
-    val conjecture_i = 0
-    val prems_i = conjecture_i + 1
-    val num_prems = length prems
-    val facts_i = prems_i + num_prems
-    val num_facts = length xfacts
-    val helpers_i = facts_i + num_facts
-
-    val conjecture_id = id_of_index conjecture_i
-    val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
-    val fact_ids' =
-      map_filter (fn j =>
-        let val ((i, _), _) = nth assms j in
-          try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
-        end) used_assm_js
-    val helper_ids' =
-      map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms
-
-    val fact_helper_ts =
-      map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @
-      map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids'
-    val fact_helper_ids' =
-      map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
-  in
-    {outcome = NONE, fact_ids = SOME fact_ids',
-     atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
-       fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
-  end
-
-end;