1 (* Title: HOL/Tools/SMT/verit_isar.ML |
1 (* Title: HOL/Tools/SMT/lethe_isar.ML |
2 Author: Mathias Fleury, TU Muenchen |
2 Author: Mathias Fleury, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 |
4 |
5 VeriT proofs as generic ATP proofs for Isar proof reconstruction. |
5 VeriT proofs as generic ATP proofs for Isar proof reconstruction. |
6 *) |
6 *) |
7 |
7 |
8 signature VERIT_ISAR = |
8 signature VERIT_ISAR = |
9 sig |
9 sig |
10 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
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 -> |
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 -> |
12 (string * term) list -> int list -> int -> (int * string) list -> Verit_Proof.veriT_step list -> |
13 (term, string) ATP_Proof.atp_step list |
13 (term, string) ATP_Proof.atp_step list |
14 end; |
14 end; |
15 |
15 |
16 structure VeriT_Isar: VERIT_ISAR = |
16 structure VeriT_Isar: VERIT_ISAR = |
17 struct |
17 struct |
20 open ATP_Problem |
20 open ATP_Problem |
21 open ATP_Proof |
21 open ATP_Proof |
22 open ATP_Proof_Reconstruct |
22 open ATP_Proof_Reconstruct |
23 open SMTLIB_Interface |
23 open SMTLIB_Interface |
24 open SMTLIB_Isar |
24 open SMTLIB_Isar |
25 open VeriT_Proof |
25 open Verit_Proof |
26 |
26 |
27 fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids |
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 = |
28 conjecture_id fact_helper_ids = |
29 let |
29 let |
30 fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
30 fun steps_of (Verit_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
31 let |
31 let |
32 val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl |
32 val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl |
33 fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems) |
33 fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems) |
34 in |
34 in |
35 if rule = veriT_input_rule then |
35 if rule = input_rule then |
36 let |
36 let |
37 val id_num = the (Int.fromString (unprefix assert_prefix id)) |
37 val id_num = the (Int.fromString (unprefix assert_prefix id)) |
38 val ss = the_list (AList.lookup (op =) fact_helper_ids id_num) |
38 val ss = the_list (AList.lookup (op =) fact_helper_ids id_num) |
39 in |
39 in |
40 (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids |
40 (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids |
44 let |
44 let |
45 val name0 = (id ^ "a", ss) |
45 val name0 = (id ^ "a", ss) |
46 val concl0 = unskolemize_names ctxt concl00 |
46 val concl0 = unskolemize_names ctxt concl00 |
47 in |
47 in |
48 [(name0, role0, concl0, rule, []), |
48 [(name0, role0, concl0, rule, []), |
49 ((id, []), Plain, concl', veriT_rewrite_rule, |
49 ((id, []), Plain, concl', rewrite_rule, |
50 name0 :: normalizing_prems ctxt concl0)] |
50 name0 :: normalizing_prems ctxt concl0)] |
51 end) |
51 end) |
52 end |
52 end |
53 else |
53 else |
54 [standard_step (if null prems then Lemma else Plain)] |
54 [standard_step (if null prems then Lemma else Plain)] |