24 open VeriT_Proof |
24 open VeriT_Proof |
25 |
25 |
26 fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids |
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 = |
27 conjecture_id fact_helper_ids proof = |
28 let |
28 let |
29 val thy = Proof_Context.theory_of ctxt |
|
30 fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
29 fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
31 let |
30 let |
32 val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl |
31 val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl |
33 fun standard_step role = ((id, []), role, concl', rule, map (fn id => (id, [])) prems) |
32 fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems) |
34 in |
33 in |
35 if rule = veriT_input_rule then |
34 if rule = veriT_input_rule then |
36 let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in |
35 let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in |
37 (case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id)) |
36 (case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id)) |
38 conjecture_id prem_ids fact_helper_ts hyp_ts concl_t of |
37 conjecture_id prem_ids fact_helper_ts hyp_ts concl_t of |
39 NONE => [] |
38 NONE => [] |
40 | SOME (role0, concl00) => |
39 | SOME (role0, concl00) => |
41 let |
40 let |
42 val name0 = (id ^ "a", ss) |
41 val name0 = (id ^ "a", ss) |
43 val concl0 = unskolemize_names concl00 |
42 val concl0 = unskolemize_names ctxt concl00 |
44 in |
43 in |
45 [(name0, role0, concl0, rule, []), |
44 [(name0, role0, concl0, rule, []), |
46 ((id, []), Plain, concl', veriT_rewrite_rule, |
45 ((id, []), Plain, concl', veriT_rewrite_rule, |
47 name0 :: normalizing_prems ctxt concl0)] |
46 name0 :: normalizing_prems ctxt concl0)] |
48 end) |
47 end) |