equal
deleted
inserted
replaced
22 open ATP_Proof_Reconstruct |
22 open ATP_Proof_Reconstruct |
23 open VeriT_Isar |
23 open VeriT_Isar |
24 open Verit_Proof |
24 open Verit_Proof |
25 |
25 |
26 fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) = |
26 fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) = |
27 union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems) |
27 union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems) |
28 |
28 |
29 fun parse_proof |
29 fun parse_proof |
30 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
30 ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
31 xfacts prems concl output = |
31 xfacts prems concl output = |
32 let |
32 let |
34 |
34 |
35 val id_of_index = Integer.add num_ll_defs |
35 val id_of_index = Integer.add num_ll_defs |
36 val index_of_id = Integer.add (~ num_ll_defs) |
36 val index_of_id = Integer.add (~ num_ll_defs) |
37 |
37 |
38 fun step_of_assume j (_, th) = |
38 fun step_of_assume j (_, th) = |
39 Verit_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j), |
39 Verit_Proof.VeriT_Step |
|
40 {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), |
40 rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} |
41 rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} |
41 |
42 |
42 val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt |
43 val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt |
43 val used_assert_ids = fold add_used_asserts_in_step actual_steps [] |
44 val used_assert_ids = fold add_used_asserts_in_step actual_steps [] |
44 val used_assm_js = |
45 val used_assm_js = |