Basic support for the SMT prover veriT.
(* Title: HOL/Tools/SMT2/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 SMTLIB2_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 proof =
let
val thy = Proof_Context.theory_of ctxt
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
let
val sid = string_of_int id
val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
fun standard_step role =
((sid, []), role, concl', rule,
map (fn id => (id, [])) prems)
in
if rule = verit_proof_input_rule then
let
val ss = the_list (AList.lookup (op =) fact_helper_ids id)
val name0 = (sid ^ "a", ss)
val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids
fact_helper_ts hyp_ts concl_t concl
val normalizing_prems = normalize_prems ctxt concl0
in
[(name0, role0, concl0, rule, []),
((sid, []), Plain, concl', verit_rewrite,
name0 :: normalizing_prems)] end
else
[standard_step Plain]
end
in
maps steps_of proof
end
end;