28 let |
28 let |
29 val thy = Proof_Context.theory_of ctxt |
29 val thy = Proof_Context.theory_of ctxt |
30 |
30 |
31 fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
31 fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = |
32 let |
32 let |
33 val sid = string_of_int id |
|
34 val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs |
33 val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs |
35 fun standard_step role = |
34 fun standard_step role = |
36 ((sid, []), role, concl', rule, |
35 ((id, []), role, concl', rule, |
37 map (fn id => (id, [])) prems) |
36 map (fn id => (id, [])) prems) |
38 in |
37 in |
39 if rule = veriT_input_rule then |
38 if rule = veriT_input_rule then |
40 let |
39 let |
41 val ss = the_list (AList.lookup (op =) fact_helper_ids id) |
40 val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) |
42 val name0 = (sid ^ "a", ss) |
41 val name0 = (id ^ "a", ss) |
43 val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids |
42 val (role0, concl0) = distinguish_conjecture_and_hypothesis ss (the (Int.fromString id)) |
44 fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names |
43 conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names |
45 in |
44 in |
46 [(name0, role0, concl0, rule, []), |
45 [(name0, role0, concl0, rule, []), |
47 ((sid, []), Plain, concl', veriT_rewrite_rule, |
46 ((id, []), Plain, concl', veriT_rewrite_rule, |
48 name0 :: normalizing_prems ctxt concl0)] end |
47 name0 :: normalizing_prems ctxt concl0)] end |
49 else |
48 else |
50 [standard_step Plain] |
49 [standard_step Plain] |
51 end |
50 end |
52 in |
51 in |