99 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
99 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
100 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
100 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
101 if have_common_thm used cls then NONE else SOME name) |
101 if have_common_thm used cls then NONE else SOME name) |
102 in |
102 in |
103 if not (null cls) andalso not (have_common_thm used cls) then |
103 if not (null cls) andalso not (have_common_thm used cls) then |
104 verbose_warning ctxt "Metis: The assumptions are inconsistent" |
104 verbose_warning ctxt "The assumptions are inconsistent" |
105 else |
105 else |
106 (); |
106 (); |
107 if not (null unused) then |
107 if not (null unused) then |
108 verbose_warning ctxt ("Metis: Unused theorems: " ^ |
108 verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused) |
109 commas_quote unused) |
|
110 else |
109 else |
111 (); |
110 (); |
112 case result of |
111 case result of |
113 (_,ith)::_ => |
112 (_,ith)::_ => |
114 (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
113 (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
115 [discharge_skolem_premises ctxt dischargers ith]) |
114 [discharge_skolem_premises ctxt dischargers ith]) |
116 | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
115 | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
117 end |
116 end |
118 | Metis_Resolution.Satisfiable _ => |
117 | Metis_Resolution.Satisfiable _ => |
119 (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); |
118 (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); |
|
119 if mode <> FT then |
|
120 raise METIS ("FOL_SOLVE", |
|
121 "No first-order proof with the lemmas supplied") |
|
122 else |
|
123 (); |
120 []) |
124 []) |
121 end; |
125 end; |
122 |
126 |
123 (* Extensionalize "th", because that makes sense and that's what Sledgehammer |
127 (* Extensionalize "th", because that makes sense and that's what Sledgehammer |
124 does, but also keep an unextensionalized version of "th" for backward |
128 does, but also keep an unextensionalized version of "th" for backward |
151 let |
155 let |
152 val _ = trace_msg ctxt (fn () => |
156 val _ = trace_msg ctxt (fn () => |
153 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
157 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
154 in |
158 in |
155 if exists_type type_has_top_sort (prop_of st0) then |
159 if exists_type type_has_top_sort (prop_of st0) then |
156 (verbose_warning ctxt "Metis: Proof state contains the universal sort {}"; |
160 (verbose_warning ctxt "Proof state contains the universal sort {}"; |
157 Seq.empty) |
161 Seq.empty) |
158 else |
162 else |
159 Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) |
163 Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) |
160 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
164 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
161 ctxt i st0 |
165 ctxt i st0 |
162 handle ERROR message => |
166 handle METIS (loc, msg) => |
163 error (message |> mode <> FT |
167 if mode <> FT then |
164 ? suffix "\nHint: You might want to try out \ |
168 (verbose_warning ctxt ("Falling back on \"metisFT\"."); |
165 \\"metisFT\".") |
169 generic_metis_tac FT ctxt ths i st0) |
|
170 else |
|
171 error ("Failed to replay Metis proof in Isabelle." ^ |
|
172 (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg |
|
173 else "")) |
|
174 |
166 end |
175 end |
167 |
176 |
168 val metis_tac = generic_metis_tac HO |
177 val metis_tac = generic_metis_tac HO |
169 val metisF_tac = generic_metis_tac FO |
178 val metisF_tac = generic_metis_tac FO |
170 val metisFT_tac = generic_metis_tac FT |
179 val metisFT_tac = generic_metis_tac FT |