75 #-> fold_rev (Logic.all o Free); |
75 #-> fold_rev (Logic.all o Free); |
76 |
76 |
77 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids |
77 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids |
78 conjecture_id fact_helper_ids proof = |
78 conjecture_id fact_helper_ids proof = |
79 let |
79 let |
80 val thy = Proof_Context.theory_of ctxt |
|
81 |
|
82 fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
80 fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
83 let |
81 let |
84 val sid = string_of_int id |
82 val sid = string_of_int id |
85 |
83 |
86 val concl' = concl |
84 val concl' = concl |
87 |> reorder_foralls (* crucial for skolemization steps *) |
85 |> reorder_foralls (* crucial for skolemization steps *) |
88 |> postprocess_step_conclusion thy rewrite_rules ll_defs |
86 |> postprocess_step_conclusion ctxt rewrite_rules ll_defs |
89 fun standard_step role = |
87 fun standard_step role = |
90 ((sid, []), role, concl', Z3_Proof.string_of_rule rule, |
88 ((sid, []), role, concl', Z3_Proof.string_of_rule rule, |
91 map (fn id => (string_of_int id, [])) prems) |
89 map (fn id => (string_of_int id, [])) prems) |
92 in |
90 in |
93 (case rule of |
91 (case rule of |
97 hyp_ts concl_t of |
95 hyp_ts concl_t of |
98 NONE => [] |
96 NONE => [] |
99 | SOME (role0, concl00) => |
97 | SOME (role0, concl00) => |
100 let |
98 let |
101 val name0 = (sid ^ "a", ss) |
99 val name0 = (sid ^ "a", ss) |
102 val concl0 = unskolemize_names concl00 |
100 val concl0 = unskolemize_names ctxt concl00 |
103 in |
101 in |
104 (if role0 = Axiom then [] |
102 (if role0 = Axiom then [] |
105 else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @ |
103 else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @ |
106 [((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite, |
104 [((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite, |
107 name0 :: normalizing_prems ctxt concl0)] |
105 name0 :: normalizing_prems ctxt concl0)] |