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