implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Translation of HOL to FOL for Sledgehammer.
9 signature SLEDGEHAMMER_ATP_TRANSLATE =
11 type 'a problem = 'a ATP_Problem.problem
12 type translated_formula
14 datatype type_system =
21 val fact_prefix : string
22 val conjecture_prefix : string
23 val is_fully_typed : type_system -> bool
24 val num_atp_type_args : theory -> type_system -> string -> int
25 val translate_atp_fact :
26 Proof.context -> (string * 'a) * thm
27 -> translated_formula option * ((string * 'a) * thm)
28 val prepare_atp_problem :
29 Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
30 -> (translated_formula option * ((string * 'a) * thm)) list
31 -> string problem * string Symtab.table * int * (string * 'a) list vector
34 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
39 open Sledgehammer_Util
41 val fact_prefix = "fact_"
42 val conjecture_prefix = "conj_"
43 val helper_prefix = "help_"
44 val class_rel_clause_prefix = "clrel_";
45 val arity_clause_prefix = "arity_"
46 val tfree_prefix = "tfree_"
48 (* Freshness almost guaranteed! *)
49 val sledgehammer_weak_prefix = "Sledgehammer:"
51 type translated_formula =
54 combformula: (name, combterm) formula,
55 ctypes_sorts: typ list}
57 datatype type_system =
64 fun is_fully_typed (Tags full_types) = full_types
65 | is_fully_typed (Preds full_types) = full_types
66 | is_fully_typed _ = false
68 (* This is an approximation. If it returns "true" for a constant that isn't
69 overloaded (i.e., that has one uniform definition), needless clutter is
70 generated; if it returns "false" for an overloaded constant, the ATP gets a
71 license to do unsound reasoning if the type system is "overloaded_args". *)
72 fun is_overloaded thy s =
73 length (Defs.specifications_of (Theory.defs_of thy) s) > 1
75 fun needs_type_args thy type_sys s =
77 Tags full_types => not full_types
78 | Preds full_types => not full_types
80 | Overload_Args => is_overloaded thy s
83 fun num_atp_type_args thy type_sys s =
84 if needs_type_args thy type_sys s then num_type_args thy s else 0
86 fun mk_anot phi = AConn (ANot, [phi])
87 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
88 fun mk_ahorn [] phi = phi
89 | mk_ahorn (phi :: phis) psi =
90 AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
92 fun combformula_for_prop thy =
94 val do_term = combterm_from_term thy
95 fun do_quant bs q s T t' =
96 let val s = Name.variant (map fst bs) s in
97 do_formula ((s, T) :: bs) t'
98 #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
100 and do_conn bs c t1 t2 =
101 do_formula bs t1 ##>> do_formula bs t2
102 #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
103 and do_formula bs t =
106 do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
107 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
108 do_quant bs AForall s T t'
109 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
110 do_quant bs AExists s T t'
111 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
112 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
113 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
114 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
115 do_conn bs AIff t1 t2
116 | _ => (fn ts => do_term bs (Envir.eta_contract t)
117 |>> AAtom ||> union (op =) ts)
120 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
122 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
123 fun conceal_bounds Ts t =
124 subst_bounds (map (Free o apfst concealed_bound_name)
125 (0 upto length Ts - 1 ~~ Ts), t)
126 fun reveal_bounds Ts =
127 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
128 (0 upto length Ts - 1 ~~ Ts))
130 (* Removes the lambdas from an equation of the form "t = (%x. u)".
131 (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
132 fun extensionalize_term t =
134 fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
135 | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
136 Type (_, [_, res_T])]))
137 $ t2 $ Abs (var_s, var_T, t')) =
138 if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
139 let val var_t = Var ((var_s, j), var_T) in
140 Const (s, T' --> T' --> res_T)
141 $ betapply (t2, var_t) $ subst_bound (var_t, t')
147 in aux (maxidx_of_term t + 1) t end
149 fun introduce_combinators_in_term ctxt kind t =
150 let val thy = ProofContext.theory_of ctxt in
151 if Meson.is_fol_term thy t then
157 @{const Not} $ t1 => @{const Not} $ aux Ts t1
158 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
159 t0 $ Abs (s, T, aux (T :: Ts) t')
160 | (t0 as Const (@{const_name All}, _)) $ t1 =>
161 aux Ts (t0 $ eta_expand Ts t1 1)
162 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
163 t0 $ Abs (s, T, aux (T :: Ts) t')
164 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
165 aux Ts (t0 $ eta_expand Ts t1 1)
166 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
167 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
168 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
169 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
171 t0 $ aux Ts t1 $ aux Ts t2
172 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
175 t |> conceal_bounds Ts
176 |> Envir.eta_contract
178 |> Meson_Clausify.introduce_combinators_in_cterm
179 |> prop_of |> Logic.dest_equals |> snd
181 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
182 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
184 (* A type variable of sort "{}" will make abstraction fail. *)
185 if kind = Conjecture then HOLogic.false_const
186 else HOLogic.true_const
189 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
190 same in Sledgehammer to prevent the discovery of unreplable proofs. *)
193 fun aux (t $ u) = aux t $ aux u
194 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
195 | aux (Var ((s, i), T)) =
196 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
198 in t |> exists_subterm is_Var t ? aux end
200 (* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
201 it leaves metaequalities over "prop"s alone. *)
204 fun aux (@{const Trueprop} $ t1) = t1
205 | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
206 HOLogic.all_const T $ Abs (s, T, aux t')
207 | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
208 | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
209 HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
210 | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
211 HOLogic.eq_const T $ t1 $ t2
212 | aux _ = raise Fail "aux"
213 in perhaps (try aux) end
215 (* making fact and conjecture formulas *)
216 fun make_formula ctxt presimp name kind t =
218 val thy = ProofContext.theory_of ctxt
219 val t = t |> Envir.beta_eta_contract
220 |> transform_elim_term
222 val need_trueprop = (fastype_of t = HOLogic.boolT)
223 val t = t |> need_trueprop ? HOLogic.mk_Trueprop
224 |> extensionalize_term
225 |> presimp ? presimplify_term thy
226 |> perhaps (try (HOLogic.dest_Trueprop))
227 |> introduce_combinators_in_term ctxt kind
228 |> kind <> Axiom ? freeze_term
229 val (combformula, ctypes_sorts) = combformula_for_prop thy t []
231 {name = name, combformula = combformula, kind = kind,
232 ctypes_sorts = ctypes_sorts}
235 fun make_fact ctxt presimp ((name, _), th) =
236 case make_formula ctxt presimp name Axiom (prop_of th) of
237 {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
238 | formula => SOME formula
239 fun make_conjecture ctxt ts =
240 let val last = length ts - 1 in
241 map2 (fn j => make_formula ctxt true (Int.toString j)
242 (if j = last then Conjecture else Hypothesis))
248 fun count_combterm (CombConst ((s, _), _, _)) =
249 Symtab.map_entry s (Integer.add 1)
250 | count_combterm (CombVar _) = I
251 | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
252 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
253 | count_combformula (AConn (_, phis)) = fold count_combformula phis
254 | count_combformula (AAtom tm) = count_combterm tm
255 fun count_translated_formula ({combformula, ...} : translated_formula) =
256 count_combformula combformula
258 val optional_helpers =
259 [(["c_COMBI"], @{thms Meson.COMBI_def}),
260 (["c_COMBK"], @{thms Meson.COMBK_def}),
261 (["c_COMBB"], @{thms Meson.COMBB_def}),
262 (["c_COMBC"], @{thms Meson.COMBC_def}),
263 (["c_COMBS"], @{thms Meson.COMBS_def})]
264 val optional_fully_typed_helpers =
265 [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
266 (["c_If"], @{thms if_True if_False})]
267 val mandatory_helpers = @{thms Metis.fequal_def}
270 [optional_helpers, optional_fully_typed_helpers] |> maps (maps fst)
271 |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
273 fun get_helper_facts ctxt is_FO type_sys conjectures facts =
276 fold (fold count_translated_formula) [conjectures, facts] init_counters
277 fun is_needed c = the (Symtab.lookup ct c) > 0
278 fun baptize th = ((Thm.get_name_hint th, false), th)
281 |> is_fully_typed type_sys ? append optional_fully_typed_helpers
282 |> maps (fn (ss, ths) =>
283 if exists is_needed ss then map baptize ths else [])) @
284 (if is_FO then [] else map baptize mandatory_helpers)
285 |> map_filter (make_fact ctxt false)
288 fun translate_atp_fact ctxt = `(make_fact ctxt true)
290 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
292 val thy = ProofContext.theory_of ctxt
293 val fact_ts = map (prop_of o snd o snd) rich_facts
294 val (facts, fact_names) =
296 |> map_filter (fn (NONE, _) => NONE
297 | (SOME fact, (name, _)) => SOME (fact, name))
299 (* Remove existing facts from the conjecture, as this can dramatically
300 boost an ATP's performance (for some reason). *)
301 val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
302 val goal_t = Logic.list_implies (hyp_ts, concl_t)
303 val is_FO = Meson.is_fol_term thy goal_t
304 val subs = tfree_classes_of_terms [goal_t]
305 val supers = tvar_classes_of_terms fact_ts
306 val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
307 (* TFrees in the conjecture; TVars in the facts *)
308 val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
309 val helper_facts = get_helper_facts ctxt is_FO type_sys conjectures facts
310 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
311 val class_rel_clauses = make_class_rel_clauses thy subs supers'
313 (fact_names |> map single |> Vector.fromList,
314 (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses))
317 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
319 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
320 | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
321 | fo_term_for_combtyp (CombType (name, tys)) =
322 ATerm (name, map fo_term_for_combtyp tys)
324 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
325 (true, ATerm (class, [ATerm (name, [])]))
326 | fo_literal_for_type_literal (TyLitFree (class, name)) =
327 (true, ATerm (class, [ATerm (name, [])]))
329 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
331 fun fo_term_for_combterm thy type_sys =
333 fun aux top_level u =
335 val (head, args) = strip_combterm_comb u
338 CombConst (name as (s, s'), _, ty_args) =>
339 (case strip_prefix_and_unascii const_prefix s of
342 if top_level andalso length args = 2 then (name, [])
343 else (("c_fequal", @{const_name Metis.fequal}), ty_args)
348 val s'' = invert_const s''
350 if needs_type_args thy type_sys s'' then ty_args else []
354 "c_False" => (("$false", s'), [])
355 | "c_True" => (("$true", s'), [])
356 | _ => (name, ty_args)
360 | CombVar (name, _) => (name, [])
361 | CombApp _ => raise Fail "impossible \"CombApp\""
362 val t = ATerm (x, map fo_term_for_combtyp ty_args @
363 map (aux false) args)
365 t |> (if type_sys = Tags true then
366 wrap_type (fo_term_for_combtyp (combtyp_of u))
372 fun formula_for_combformula thy type_sys =
374 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
375 | aux (AConn (c, phis)) = AConn (c, map aux phis)
376 | aux (AAtom tm) = AAtom (fo_term_for_combterm thy type_sys tm)
379 fun formula_for_fact thy type_sys
380 ({combformula, ctypes_sorts, ...} : translated_formula) =
381 mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
382 (type_literals_for_types ctypes_sorts))
383 (formula_for_combformula thy type_sys combformula)
385 fun problem_line_for_fact thy prefix type_sys (formula as {name, kind, ...}) =
386 Fof (prefix ^ ascii_of name, kind, formula_for_fact thy type_sys formula)
388 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
390 let val ty_arg = ATerm (("T", "T"), []) in
391 Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
392 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
393 AAtom (ATerm (superclass, [ty_arg]))]))
396 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
397 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
398 | fo_literal_for_arity_literal (TVarLit (c, sort)) =
399 (false, ATerm (c, [ATerm (sort, [])]))
401 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
403 Fof (arity_clause_prefix ^ ascii_of name, Axiom,
404 mk_ahorn (map (formula_for_fo_literal o apfst not
405 o fo_literal_for_arity_literal) premLits)
406 (formula_for_fo_literal
407 (fo_literal_for_arity_literal conclLit)))
409 fun problem_line_for_conjecture thy type_sys
410 ({name, kind, combformula, ...} : translated_formula) =
411 Fof (conjecture_prefix ^ name, kind,
412 formula_for_combformula thy type_sys combformula)
414 fun free_type_literals_for_conjecture
415 ({ctypes_sorts, ...} : translated_formula) =
416 map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
418 fun problem_line_for_free_type j lit =
419 Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
420 fun problem_lines_for_free_types conjectures =
422 val litss = map free_type_literals_for_conjecture conjectures
423 val lits = fold (union (op =)) litss []
424 in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
426 (** "hBOOL" and "hAPP" **)
428 type const_info = {min_arity: int, max_arity: int, sub_level: bool}
430 fun consider_term top_level (ATerm ((s, _), ts)) =
431 (if is_atp_variable s then
434 let val n = length ts in
436 (s, {min_arity = n, max_arity = 0, sub_level = false})
437 (fn {min_arity, max_arity, sub_level} =>
438 {min_arity = Int.min (n, min_arity),
439 max_arity = Int.max (n, max_arity),
440 sub_level = sub_level orelse not top_level})
442 #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
443 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
444 | consider_formula (AConn (_, phis)) = fold consider_formula phis
445 | consider_formula (AAtom tm) = consider_term true tm
447 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
448 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
450 fun const_table_for_problem explicit_apply problem =
451 if explicit_apply then NONE
452 else SOME (Symtab.empty |> consider_problem problem)
454 fun min_arity_of thy type_sys NONE s =
455 (if s = "equal" orelse s = type_wrapper_name orelse
456 String.isPrefix type_const_prefix s orelse
457 String.isPrefix class_prefix s then
458 16383 (* large number *)
459 else case strip_prefix_and_unascii const_prefix s of
460 SOME s' => num_atp_type_args thy type_sys (invert_const s')
462 | min_arity_of _ _ (SOME the_const_tab) s =
463 case Symtab.lookup the_const_tab s of
464 SOME ({min_arity, ...} : const_info) => min_arity
467 fun full_type_of (ATerm ((s, _), [ty, _])) =
468 if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
469 | full_type_of _ = raise Fail "expected type wrapper"
471 fun list_hAPP_rev _ t1 [] = t1
472 | list_hAPP_rev NONE t1 (t2 :: ts2) =
473 ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
474 | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
475 let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
476 [full_type_of t2, ty]) in
477 ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
480 fun repair_applications_in_term thy type_sys const_tab =
482 fun aux opt_ty (ATerm (name as (s, _), ts)) =
483 if s = type_wrapper_name then
485 [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
486 | _ => raise Fail "malformed type wrapper"
489 val ts = map (aux NONE) ts
490 val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts
491 in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
494 fun boolify t = ATerm (`I "hBOOL", [t])
496 (* True if the constant ever appears outside of the top-level position in
497 literals, or if it appears with different arities (e.g., because of different
498 type instantiations). If false, the constant always receives all of its
499 arguments and is used as a predicate. *)
500 fun is_predicate NONE s =
501 s = "equal" orelse s = "$false" orelse s = "$true" orelse
502 String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
503 | is_predicate (SOME the_const_tab) s =
504 case Symtab.lookup the_const_tab s of
505 SOME {min_arity, max_arity, sub_level} =>
506 not sub_level andalso min_arity = max_arity
509 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
510 if s = type_wrapper_name then
512 [_, t' as ATerm ((s', _), _)] =>
513 if is_predicate const_tab s' then t' else boolify t
514 | _ => raise Fail "malformed type wrapper"
516 t |> not (is_predicate const_tab s) ? boolify
518 fun close_universally phi =
520 fun term_vars bounds (ATerm (name as (s, _), tms)) =
521 (is_atp_variable s andalso not (member (op =) bounds name))
523 #> fold (term_vars bounds) tms
524 fun formula_vars bounds (AQuant (_, xs, phi)) =
525 formula_vars (xs @ bounds) phi
526 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
527 | formula_vars bounds (AAtom tm) = term_vars bounds tm
529 case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
532 fun repair_formula thy explicit_forall type_sys const_tab =
534 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
535 | aux (AConn (c, phis)) = AConn (c, map aux phis)
537 AAtom (tm |> repair_applications_in_term thy type_sys const_tab
538 |> repair_predicates_in_term const_tab)
539 in aux #> explicit_forall ? close_universally end
541 fun repair_problem_line thy explicit_forall type_sys const_tab
542 (Fof (ident, kind, phi)) =
543 Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
544 fun repair_problem_with_const_table thy =
545 map o apsnd o map ooo repair_problem_line thy
547 fun repair_problem thy explicit_forall type_sys explicit_apply problem =
548 repair_problem_with_const_table thy explicit_forall type_sys
549 (const_table_for_problem explicit_apply problem) problem
551 fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
552 explicit_apply hyp_ts concl_t facts =
554 val thy = ProofContext.theory_of ctxt
555 val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
557 translate_formulas ctxt type_sys hyp_ts concl_t facts
558 val fact_lines = map (problem_line_for_fact thy fact_prefix type_sys) facts
560 map (problem_line_for_fact thy helper_prefix type_sys) helper_facts
561 val conjecture_lines =
562 map (problem_line_for_conjecture thy type_sys) conjectures
563 val tfree_lines = problem_lines_for_free_types conjectures
564 val class_rel_lines =
565 map problem_line_for_class_rel_clause class_rel_clauses
566 val arity_lines = map problem_line_for_arity_clause arity_clauses
567 (* Reordering these might or might not confuse the proof reconstruction
568 code or the SPASS Flotter hack. *)
570 [("Relevant facts", fact_lines),
571 ("Class relationships", class_rel_lines),
572 ("Arity declarations", arity_lines),
573 ("Helper facts", helper_lines),
574 ("Conjectures", conjecture_lines),
575 ("Type variables", tfree_lines)]
576 |> repair_problem thy explicit_forall type_sys explicit_apply
577 val (problem, pool) = nice_atp_problem readable_names problem
578 val conjecture_offset =
579 length fact_lines + length class_rel_lines + length arity_lines
580 + length helper_lines
583 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
584 conjecture_offset, fact_names)