81 (* It is not entirely clear why this should be necessary, especially for abstractions variables. *) |
81 (* It is not entirely clear why this should be necessary, especially for abstractions variables. *) |
82 val unskolemize_names = |
82 val unskolemize_names = |
83 Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
83 Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
84 #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) |
84 #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) |
85 |
85 |
86 fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof = |
86 fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof = |
87 let |
87 let |
88 fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
88 val thy = Proof_Context.theory_of ctxt |
|
89 |
|
90 fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
89 let |
91 let |
90 fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) |
92 fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) |
91 |
93 |
92 val name as (_, ss) = step_name_of id |
94 val name as (sid, ss) = step_name_of id |
93 |
95 |
94 val role = |
96 val concl' = |
95 (case rule of |
97 concl |
96 Z3_New_Proof.Asserted => |
|
97 if not (null ss) then Axiom |
|
98 else if id = conjecture_id then Negated_Conjecture |
|
99 else Hypothesis |
|
100 | Z3_New_Proof.Rewrite => Lemma |
|
101 | Z3_New_Proof.Rewrite_Star => Lemma |
|
102 | Z3_New_Proof.Skolemize => Lemma |
|
103 | Z3_New_Proof.Th_Lemma _ => Lemma |
|
104 | _ => Plain) |
|
105 |
|
106 val concl' = concl |
|
107 |> Raw_Simplifier.rewrite_term thy rewrite_rules [] |
98 |> Raw_Simplifier.rewrite_term thy rewrite_rules [] |
108 |> Object_Logic.atomize_term thy |
99 |> Object_Logic.atomize_term thy |
109 |> simplify_bool |
100 |> simplify_bool |
110 |> unskolemize_names |
101 |> unskolemize_names |
111 |> HOLogic.mk_Trueprop |
102 |> HOLogic.mk_Trueprop |
|
103 |
|
104 fun standard_step role = |
|
105 (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems) |
112 in |
106 in |
113 (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems) |
107 (case rule of |
|
108 Z3_New_Proof.Asserted => |
|
109 let |
|
110 val name0 = (sid ^ "a", ss) |
|
111 val (role0, concl0) = |
|
112 if not (null ss) then |
|
113 (Axiom, concl(*FIXME*)) |
|
114 else if id = conjecture_id then |
|
115 (Conjecture, concl_t) |
|
116 else |
|
117 (Hypothesis, |
|
118 (case find_index (curry (op =) id) prem_ids of |
|
119 ~1 => concl |
|
120 | i => nth hyp_ts i)) |
|
121 |
|
122 val normalize_prems = |
|
123 SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ |
|
124 SMT2_Normalize.abs_min_max_table |
|
125 |> map_filter (fn (c, th) => |
|
126 if exists_Const (curry (op =) c o fst) concl0 then |
|
127 let val s = short_thm_name ctxt th in SOME (s, [s]) end |
|
128 else |
|
129 NONE) |
|
130 in |
|
131 if null normalize_prems then |
|
132 [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])] |
|
133 else |
|
134 [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []), |
|
135 (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite, |
|
136 name0 :: normalize_prems)] |
|
137 end |
|
138 | Z3_New_Proof.Rewrite => [standard_step Lemma] |
|
139 | Z3_New_Proof.Rewrite_Star => [standard_step Lemma] |
|
140 | Z3_New_Proof.Skolemize => [standard_step Lemma] |
|
141 | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma] |
|
142 | _ => [standard_step Plain]) |
114 end |
143 end |
115 in |
144 in |
116 proof |
145 proof |
117 |> map step_of |
146 |> maps steps_of |
118 |> inline_z3_defs [] |
147 |> inline_z3_defs [] |
119 |> inline_z3_hypotheses [] [] |
148 |> inline_z3_hypotheses [] [] |
120 end |
149 end |
121 |
150 |
122 end; |
151 end; |