34 val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs |
34 val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs |
35 fun standard_step role = |
35 fun standard_step role = |
36 ((sid, []), role, concl', rule, |
36 ((sid, []), role, concl', rule, |
37 map (fn id => (id, [])) prems) |
37 map (fn id => (id, [])) prems) |
38 in |
38 in |
39 if rule = verit_proof_input_rule then |
39 if rule = veriT_input_rule then |
40 let |
40 let |
41 val ss = the_list (AList.lookup (op =) fact_helper_ids id) |
41 val ss = the_list (AList.lookup (op =) fact_helper_ids id) |
42 val name0 = (sid ^ "a", ss) |
42 val name0 = (sid ^ "a", ss) |
43 val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids |
43 val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids |
44 fact_helper_ts hyp_ts concl_t concl |
44 fact_helper_ts hyp_ts concl_t concl |
45 |
|
46 val normalizing_prems = normalize_prems ctxt concl0 |
|
47 in |
45 in |
48 [(name0, role0, concl0, rule, []), |
46 [(name0, role0, concl0, rule, []), |
49 ((sid, []), Plain, concl', verit_rewrite, |
47 ((sid, []), Plain, concl', veriT_rewrite_rule, |
50 name0 :: normalizing_prems)] end |
48 name0 :: normalizing_prems ctxt concl0)] end |
51 else |
49 else |
52 [standard_step Plain] |
50 [standard_step Plain] |
53 end |
51 end |
54 in |
52 in |
55 maps steps_of proof |
53 maps steps_of proof |