author | fleury |
Wed, 30 Jul 2014 14:03:13 +0200 | |
changeset 57714 | 4856a7b8b9c3 |
parent 57712 | 3c4e6bc7455f |
child 57730 | d39815cdb7ba |
permissions | -rw-r--r-- |
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 |
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
|
31 |
let |
|
32 |
val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs |
|
33 |
fun standard_step role = |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
34 |
((id, []), role, concl', rule, |
57704 | 35 |
map (fn id => (id, [])) prems) |
36 |
in |
|
57705 | 37 |
if rule = veriT_input_rule then |
57704 | 38 |
let |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
39 |
val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
40 |
val name0 = (id ^ "a", ss) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
41 |
val (role0, concl0) = distinguish_conjecture_and_hypothesis ss (the (Int.fromString id)) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
42 |
conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names |
57704 | 43 |
in |
44 |
[(name0, role0, concl0, rule, []), |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57708
diff
changeset
|
45 |
((id, []), Plain, concl', veriT_rewrite_rule, |
57705 | 46 |
name0 :: normalizing_prems ctxt concl0)] end |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57712
diff
changeset
|
47 |
else if rule = veriT_tmp_ite_elim_rule then |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57712
diff
changeset
|
48 |
[standard_step Lemma] |
57704 | 49 |
else |
50 |
[standard_step Plain] |
|
51 |
end |
|
52 |
in |
|
53 |
maps steps_of proof |
|
54 |
end |
|
55 |
||
56 |
end; |