1(*  Title:      HOL/Tools/SMT/verit_isar.ML
2    Author:     Mathias Fleury, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4
5VeriT proofs as generic ATP proofs for Isar proof reconstruction.
6*)
7
8signature VERIT_ISAR =
9sig
10  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
11  val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
12    (string * term) list -> int list -> int -> (int * string) list -> VeriT_Proof.veriT_step list ->
13    (term, string) ATP_Proof.atp_step list
14end;
15
16structure VeriT_Isar: VERIT_ISAR =
17struct
18
19open ATP_Util
20open ATP_Problem
21open ATP_Proof
22open ATP_Proof_Reconstruct
23open SMTLIB_Interface
24open SMTLIB_Isar
25open VeriT_Proof
26
27fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
28    conjecture_id fact_helper_ids =
29  let
30    fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
31      let
32        val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
33        fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
34      in
35        if rule = veriT_input_rule then
36          let
37            val id_num = the (Int.fromString (unprefix assert_prefix id))
38            val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
39          in
40            (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids
41                fact_helper_ts hyp_ts concl_t of
42              NONE => []
43            | SOME (role0, concl00) =>
44              let
45                val name0 = (id ^ "a", ss)
46                val concl0 = unskolemize_names ctxt concl00
47              in
48                [(name0, role0, concl0, rule, []),
49                 ((id, []), Plain, concl', veriT_rewrite_rule,
50                  name0 :: normalizing_prems ctxt concl0)]
51              end)
52          end
53        else
54          [standard_step (if null prems then Lemma else Plain)]
55      end
56  in
57    maps steps_of
58  end
59
60end;
61