57704
|
1 |
(* Title: HOL/Tools/SMT2/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 SMTLIB2_Isar
|
|
24 |
open VeriT_Proof
|
|
25 |
|
|
26 |
fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
|
|
27 |
conjecture_id fact_helper_ids proof =
|
|
28 |
let
|
|
29 |
val thy = Proof_Context.theory_of ctxt
|
|
30 |
|
|
31 |
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
|
|
32 |
let
|
|
33 |
val sid = string_of_int id
|
|
34 |
val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
|
|
35 |
fun standard_step role =
|
|
36 |
((sid, []), role, concl', rule,
|
|
37 |
map (fn id => (id, [])) prems)
|
|
38 |
in
|
|
39 |
if rule = verit_proof_input_rule then
|
|
40 |
let
|
|
41 |
val ss = the_list (AList.lookup (op =) fact_helper_ids id)
|
|
42 |
val name0 = (sid ^ "a", ss)
|
|
43 |
val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids
|
|
44 |
fact_helper_ts hyp_ts concl_t concl
|
|
45 |
|
|
46 |
val normalizing_prems = normalize_prems ctxt concl0
|
|
47 |
in
|
|
48 |
[(name0, role0, concl0, rule, []),
|
|
49 |
((sid, []), Plain, concl', verit_rewrite,
|
|
50 |
name0 :: normalizing_prems)] end
|
|
51 |
else
|
|
52 |
[standard_step Plain]
|
|
53 |
end
|
|
54 |
in
|
|
55 |
maps steps_of proof
|
|
56 |
end
|
|
57 |
|
|
58 |
end;
|