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