6 |
6 |
7 signature Z3_NEW_ISAR = |
7 signature Z3_NEW_ISAR = |
8 sig |
8 sig |
9 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
9 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
10 |
10 |
11 val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (int * string) list -> |
11 val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> |
12 (term, string) atp_step list |
12 (term, string) atp_step list |
13 end; |
13 end; |
14 |
14 |
15 structure Z3_New_Isar: Z3_NEW_ISAR = |
15 structure Z3_New_Isar: Z3_NEW_ISAR = |
16 struct |
16 struct |
72 | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) |
72 | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) |
73 | simplify_prop t = t |
73 | simplify_prop t = t |
74 |
74 |
75 fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) |
75 fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) |
76 |
76 |
77 fun atp_proof_of_z3_proof thy proof fact_ids = |
77 fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof = |
78 let |
78 let |
79 fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
79 fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
80 let |
80 let |
81 fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) |
81 fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) |
82 |
82 |
83 val name as (_, ss) = step_name_of id |
83 val name as (_, ss) = step_name_of id |
84 val role = |
84 val role = |
85 (case rule of |
85 (case rule of |
86 Z3_New_Proof.Asserted => |
86 Z3_New_Proof.Asserted => |
87 if null ss then Negated_Conjecture (* FIXME: or hypothesis! *) else Axiom |
87 if not (null ss) then Axiom |
|
88 else if id = conjecture_id then Negated_Conjecture |
|
89 else Hypothesis |
88 | Z3_New_Proof.Rewrite => Lemma |
90 | Z3_New_Proof.Rewrite => Lemma |
89 | Z3_New_Proof.Rewrite_Star => Lemma |
91 | Z3_New_Proof.Rewrite_Star => Lemma |
90 | Z3_New_Proof.Skolemize => Lemma |
92 | Z3_New_Proof.Skolemize => Lemma |
91 | Z3_New_Proof.Th_Lemma _ => Lemma |
93 | Z3_New_Proof.Th_Lemma _ => Lemma |
92 | _ => Plain) |
94 | _ => Plain) |