src/HOL/Tools/SMT/verit_isar.ML
author nipkow
Wed Jan 10 15:25:09 2018 +0100 (19 months ago)
changeset 67399 eab6ce8368fa
parent 58515 6cf55e935a9d
permissions -rw-r--r--
ran isabelle update_op on all sources
     1 (*  Title:      HOL/Tools/SMT/verit_isar.ML
     2     Author:     Mathias Fleury, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 VeriT proofs as generic ATP proofs for Isar proof reconstruction.
     6 *)
     7 
     8 signature VERIT_ISAR =
     9 sig
    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
    14 end;
    15 
    16 structure VeriT_Isar: VERIT_ISAR =
    17 struct
    18 
    19 open ATP_Util
    20 open ATP_Problem
    21 open ATP_Proof
    22 open ATP_Proof_Reconstruct
    23 open SMTLIB_Interface
    24 open SMTLIB_Isar
    25 open VeriT_Proof
    26 
    27 fun 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 
    60 end;