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