merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
authorblanchet
Fri Jun 25 16:42:06 2010 +0200 (2010-06-25)
changeset 375775379f41a1322
parent 37576 512cf962d54c
child 37578 9367cb36b1c4
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 25 16:29:07 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 25 16:42:06 2010 +0200
     1.3 @@ -319,7 +319,6 @@
     1.4    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
     1.5    Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
     1.6    Tools/Sledgehammer/sledgehammer_fol_clause.ML \
     1.7 -  Tools/Sledgehammer/sledgehammer_hol_clause.ML \
     1.8    Tools/Sledgehammer/sledgehammer_isar.ML \
     1.9    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
    1.10    Tools/Sledgehammer/sledgehammer_tptp_format.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 25 16:29:07 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 25 16:42:06 2010 +0200
     2.3 @@ -325,7 +325,7 @@
     2.4        NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     2.5      | SOME _ => (message, SH_FAIL (time_isa, time_atp))
     2.6    end
     2.7 -  handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     2.8 +  handle Sledgehammer_FOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     2.9         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    2.10         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    2.11  
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 16:29:07 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 16:42:06 2010 +0200
     3.3 @@ -15,7 +15,6 @@
     3.4    ("Tools/Sledgehammer/meson_tactic.ML")
     3.5    ("Tools/Sledgehammer/sledgehammer_util.ML")
     3.6    ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
     3.7 -  ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
     3.8    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     3.9    ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
    3.10    ("Tools/ATP_Manager/atp_manager.ML")
    3.11 @@ -92,7 +91,6 @@
    3.12  
    3.13  use "Tools/Sledgehammer/sledgehammer_util.ML"
    3.14  use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    3.15 -use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
    3.16  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    3.17  use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    3.18  use "Tools/ATP_Manager/atp_manager.ML"
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:29:07 2010 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:42:06 2010 +0200
     4.3 @@ -67,7 +67,7 @@
     4.4  
     4.5  open Sledgehammer_Util
     4.6  open Sledgehammer_Fact_Filter
     4.7 -open Sledgehammer_HOL_Clause
     4.8 +open Sledgehammer_FOL_Clause
     4.9  open Sledgehammer_Proof_Reconstruct
    4.10  
    4.11  (** problems, results, provers, etc. **)
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 16:29:07 2010 +0200
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 16:42:06 2010 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4  
     5.5  open Clausifier
     5.6  open Sledgehammer_Util
     5.7 -open Sledgehammer_HOL_Clause
     5.8 +open Sledgehammer_FOL_Clause
     5.9  open Sledgehammer_Fact_Filter
    5.10  open Sledgehammer_Proof_Reconstruct
    5.11  open Sledgehammer_TPTP_Format
     6.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:29:07 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:42:06 2010 +0200
     6.3 @@ -21,7 +21,6 @@
     6.4  open Clausifier
     6.5  open Sledgehammer_Util
     6.6  open Sledgehammer_FOL_Clause
     6.7 -open Sledgehammer_HOL_Clause
     6.8  
     6.9  exception METIS of string * string
    6.10  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 16:29:07 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 16:42:06 2010 +0200
     7.3 @@ -23,7 +23,6 @@
     7.4  
     7.5  open Clausifier
     7.6  open Sledgehammer_FOL_Clause
     7.7 -open Sledgehammer_HOL_Clause
     7.8  
     7.9  (* Experimental feature: Filter theorems in natural form or in CNF? *)
    7.10  val use_natural_form = Unsynchronized.ref false
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:29:07 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:42:06 2010 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4  
     8.5  open Clausifier
     8.6  open Sledgehammer_Util
     8.7 -open Sledgehammer_HOL_Clause
     8.8 +open Sledgehammer_FOL_Clause
     8.9  open Sledgehammer_Proof_Reconstruct
    8.10  open ATP_Manager
    8.11  
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Jun 25 16:29:07 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Jun 25 16:42:06 2010 +0200
     9.3 @@ -4,12 +4,38 @@
     9.4  
     9.5  Storing/printing FOL clauses and arity clauses.  Typed equality is
     9.6  treated differently.
     9.7 -
     9.8 -FIXME: combine with sledgehammer_hol_clause!
     9.9  *)
    9.10  
    9.11  signature SLEDGEHAMMER_FOL_CLAUSE =
    9.12  sig
    9.13 +  type cnf_thm = Clausifier.cnf_thm
    9.14 +  type name = string * string
    9.15 +  type name_pool = string Symtab.table * string Symtab.table
    9.16 +  datatype kind = Axiom | Conjecture
    9.17 +  datatype type_literal =
    9.18 +    TyLitVar of string * name |
    9.19 +    TyLitFree of string * name
    9.20 +  datatype arLit =
    9.21 +      TConsLit of class * string * string list
    9.22 +    | TVarLit of class * string
    9.23 +  datatype arity_clause = ArityClause of
    9.24 +   {axiom_name: string, conclLit: arLit, premLits: arLit list}
    9.25 +  datatype classrel_clause = ClassrelClause of
    9.26 +   {axiom_name: string, subclass: class, superclass: class}
    9.27 +  datatype combtyp =
    9.28 +    TyVar of name |
    9.29 +    TyFree of name |
    9.30 +    TyConstr of name * combtyp list
    9.31 +  datatype combterm =
    9.32 +    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    9.33 +    CombVar of name * combtyp |
    9.34 +    CombApp of combterm * combterm
    9.35 +  datatype literal = Literal of bool * combterm
    9.36 +  datatype hol_clause =
    9.37 +    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    9.38 +                  literals: literal list, ctypes_sorts: typ list}
    9.39 +  exception TRIVIAL of unit
    9.40 +
    9.41    val type_wrapper_name : string
    9.42    val schematic_var_prefix: string
    9.43    val fixed_var_prefix: string
    9.44 @@ -30,30 +56,34 @@
    9.45    val make_fixed_const : string -> string
    9.46    val make_fixed_type_const : string -> string
    9.47    val make_type_class : string -> string
    9.48 -  type name = string * string
    9.49 -  type name_pool = string Symtab.table * string Symtab.table
    9.50    val empty_name_pool : bool -> name_pool option
    9.51    val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    9.52    val nice_name : name -> name_pool option -> string * name_pool option
    9.53 -  datatype kind = Axiom | Conjecture
    9.54 -  datatype type_literal =
    9.55 -    TyLitVar of string * name |
    9.56 -    TyLitFree of string * name
    9.57    val type_literals_for_types : typ list -> type_literal list
    9.58 -  datatype arLit =
    9.59 -      TConsLit of class * string * string list
    9.60 -    | TVarLit of class * string
    9.61 -  datatype arity_clause = ArityClause of
    9.62 -   {axiom_name: string, conclLit: arLit, premLits: arLit list}
    9.63 -  datatype classrel_clause = ClassrelClause of
    9.64 -   {axiom_name: string, subclass: class, superclass: class}
    9.65    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    9.66    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    9.67 +  val type_of_combterm : combterm -> combtyp
    9.68 +  val strip_combterm_comb : combterm -> combterm * combterm list
    9.69 +  val literals_of_term : theory -> term -> literal list * typ list
    9.70 +  val conceal_skolem_somes :
    9.71 +    int -> (string * term) list -> term -> (string * term) list * term
    9.72 +  val is_quasi_fol_theorem : theory -> thm -> bool
    9.73 +  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
    9.74 +  val tfree_classes_of_terms : term list -> string list
    9.75 +  val tvar_classes_of_terms : term list -> string list
    9.76 +  val type_consts_of_terms : theory -> term list -> string list
    9.77 +  val prepare_clauses :
    9.78 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    9.79 +    -> string vector
    9.80 +       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
    9.81 +          * classrel_clause list * arity_clause list)
    9.82  end
    9.83  
    9.84  structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
    9.85  struct
    9.86  
    9.87 +open Clausifier
    9.88 +
    9.89  val type_wrapper_name = "ti"
    9.90  
    9.91  val schematic_var_prefix = "V_";
    9.92 @@ -240,7 +270,7 @@
    9.93  
    9.94  (**** Definitions and functions for FOL clauses for TPTP format output ****)
    9.95  
    9.96 -datatype kind = Axiom | Conjecture;
    9.97 +datatype kind = Axiom | Conjecture
    9.98  
    9.99  (**** Isabelle FOL clauses ****)
   9.100  
   9.101 @@ -362,4 +392,294 @@
   9.102    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   9.103    in  (classes', multi_arity_clause cpairs)  end;
   9.104  
   9.105 +datatype combtyp =
   9.106 +  TyVar of name |
   9.107 +  TyFree of name |
   9.108 +  TyConstr of name * combtyp list
   9.109 +
   9.110 +datatype combterm =
   9.111 +  CombConst of name * combtyp * combtyp list (* Const and Free *) |
   9.112 +  CombVar of name * combtyp |
   9.113 +  CombApp of combterm * combterm
   9.114 +
   9.115 +datatype literal = Literal of bool * combterm
   9.116 +
   9.117 +datatype hol_clause =
   9.118 +  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
   9.119 +                literals: literal list, ctypes_sorts: typ list}
   9.120 +
   9.121 +(*********************************************************************)
   9.122 +(* convert a clause with type Term.term to a clause with type clause *)
   9.123 +(*********************************************************************)
   9.124 +
   9.125 +(*Result of a function type; no need to check that the argument type matches.*)
   9.126 +fun result_type (TyConstr (_, [_, tp2])) = tp2
   9.127 +  | result_type _ = raise Fail "non-function type"
   9.128 +
   9.129 +fun type_of_combterm (CombConst (_, tp, _)) = tp
   9.130 +  | type_of_combterm (CombVar (_, tp)) = tp
   9.131 +  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
   9.132 +
   9.133 +(*gets the head of a combinator application, along with the list of arguments*)
   9.134 +fun strip_combterm_comb u =
   9.135 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   9.136 +        |   stripc  x =  x
   9.137 +    in stripc(u,[]) end
   9.138 +
   9.139 +fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
   9.140 +      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
   9.141 +  | isFalse _ = false;
   9.142 +
   9.143 +fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
   9.144 +      (pol andalso c = "c_True") orelse
   9.145 +      (not pol andalso c = "c_False")
   9.146 +  | isTrue _ = false;
   9.147 +
   9.148 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
   9.149 +
   9.150 +fun type_of (Type (a, Ts)) =
   9.151 +    let val (folTypes,ts) = types_of Ts in
   9.152 +      (TyConstr (`make_fixed_type_const a, folTypes), ts)
   9.153 +    end
   9.154 +  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
   9.155 +  | type_of (tp as TVar (x, _)) =
   9.156 +    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
   9.157 +and types_of Ts =
   9.158 +    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   9.159 +      (folTyps, union_all ts)
   9.160 +    end
   9.161 +
   9.162 +(* same as above, but no gathering of sort information *)
   9.163 +fun simp_type_of (Type (a, Ts)) =
   9.164 +      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
   9.165 +  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
   9.166 +  | simp_type_of (TVar (x, _)) =
   9.167 +    TyVar (make_schematic_type_var x, string_of_indexname x)
   9.168 +
   9.169 +(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   9.170 +fun combterm_of thy (Const (c, T)) =
   9.171 +      let
   9.172 +        val (tp, ts) = type_of T
   9.173 +        val tvar_list =
   9.174 +          (if String.isPrefix skolem_theory_name c then
   9.175 +             [] |> Term.add_tvarsT T |> map TVar
   9.176 +           else
   9.177 +             (c, T) |> Sign.const_typargs thy)
   9.178 +          |> map simp_type_of
   9.179 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   9.180 +      in  (c',ts)  end
   9.181 +  | combterm_of _ (Free(v, T)) =
   9.182 +      let val (tp,ts) = type_of T
   9.183 +          val v' = CombConst (`make_fixed_var v, tp, [])
   9.184 +      in  (v',ts)  end
   9.185 +  | combterm_of _ (Var(v, T)) =
   9.186 +      let val (tp,ts) = type_of T
   9.187 +          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   9.188 +      in  (v',ts)  end
   9.189 +  | combterm_of thy (P $ Q) =
   9.190 +      let val (P', tsP) = combterm_of thy P
   9.191 +          val (Q', tsQ) = combterm_of thy Q
   9.192 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   9.193 +  | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
   9.194 +
   9.195 +fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   9.196 +  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
   9.197 +
   9.198 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   9.199 +    literals_of_term1 args thy P
   9.200 +  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   9.201 +    literals_of_term1 (literals_of_term1 args thy P) thy Q
   9.202 +  | literals_of_term1 (lits, ts) thy P =
   9.203 +    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   9.204 +      (Literal (pol, pred) :: lits, union (op =) ts ts')
   9.205 +    end
   9.206 +val literals_of_term = literals_of_term1 ([], [])
   9.207 +
   9.208 +fun skolem_name i j num_T_args =
   9.209 +  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   9.210 +  skolem_infix ^ "g"
   9.211 +
   9.212 +fun conceal_skolem_somes i skolem_somes t =
   9.213 +  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
   9.214 +    let
   9.215 +      fun aux skolem_somes
   9.216 +              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
   9.217 +          let
   9.218 +            val (skolem_somes, s) =
   9.219 +              if i = ~1 then
   9.220 +                (skolem_somes, @{const_name undefined})
   9.221 +              else case AList.find (op aconv) skolem_somes t of
   9.222 +                s :: _ => (skolem_somes, s)
   9.223 +              | [] =>
   9.224 +                let
   9.225 +                  val s = skolem_theory_name ^ "." ^
   9.226 +                          skolem_name i (length skolem_somes)
   9.227 +                                        (length (Term.add_tvarsT T []))
   9.228 +                in ((s, t) :: skolem_somes, s) end
   9.229 +          in (skolem_somes, Const (s, T)) end
   9.230 +        | aux skolem_somes (t1 $ t2) =
   9.231 +          let
   9.232 +            val (skolem_somes, t1) = aux skolem_somes t1
   9.233 +            val (skolem_somes, t2) = aux skolem_somes t2
   9.234 +          in (skolem_somes, t1 $ t2) end
   9.235 +        | aux skolem_somes (Abs (s, T, t')) =
   9.236 +          let val (skolem_somes, t') = aux skolem_somes t' in
   9.237 +            (skolem_somes, Abs (s, T, t'))
   9.238 +          end
   9.239 +        | aux skolem_somes t = (skolem_somes, t)
   9.240 +    in aux skolem_somes t end
   9.241 +  else
   9.242 +    (skolem_somes, t)
   9.243 +
   9.244 +fun is_quasi_fol_theorem thy =
   9.245 +  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
   9.246 +
   9.247 +(* Trivial problem, which resolution cannot handle (empty clause) *)
   9.248 +exception TRIVIAL of unit
   9.249 +
   9.250 +(* making axiom and conjecture clauses *)
   9.251 +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
   9.252 +  let
   9.253 +    val (skolem_somes, t) =
   9.254 +      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
   9.255 +    val (lits, ctypes_sorts) = literals_of_term thy t
   9.256 +  in
   9.257 +    if forall isFalse lits then
   9.258 +      raise TRIVIAL ()
   9.259 +    else
   9.260 +      (skolem_somes,
   9.261 +       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   9.262 +                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   9.263 +  end
   9.264 +
   9.265 +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
   9.266 +  let
   9.267 +    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   9.268 +  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   9.269 +
   9.270 +fun make_axiom_clauses thy clauses =
   9.271 +  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
   9.272 +
   9.273 +fun make_conjecture_clauses thy =
   9.274 +  let
   9.275 +    fun aux _ _ [] = []
   9.276 +      | aux n skolem_somes (th :: ths) =
   9.277 +        let
   9.278 +          val (skolem_somes, cls) =
   9.279 +            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
   9.280 +        in cls :: aux (n + 1) skolem_somes ths end
   9.281 +  in aux 0 [] end
   9.282 +
   9.283 +(** Helper clauses **)
   9.284 +
   9.285 +fun count_combterm (CombConst ((c, _), _, _)) =
   9.286 +    Symtab.map_entry c (Integer.add 1)
   9.287 +  | count_combterm (CombVar _) = I
   9.288 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   9.289 +fun count_literal (Literal (_, t)) = count_combterm t
   9.290 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   9.291 +
   9.292 +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
   9.293 +fun cnf_helper_thms thy raw =
   9.294 +  map (`Thm.get_name_hint)
   9.295 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   9.296 +
   9.297 +val optional_helpers =
   9.298 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   9.299 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   9.300 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
   9.301 +val optional_typed_helpers =
   9.302 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
   9.303 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   9.304 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   9.305 +
   9.306 +val init_counters =
   9.307 +  Symtab.make (maps (maps (map (rpair 0) o fst))
   9.308 +                    [optional_helpers, optional_typed_helpers])
   9.309 +
   9.310 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
   9.311 +  let
   9.312 +    val axclauses = map snd (make_axiom_clauses thy axcls)
   9.313 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   9.314 +    fun is_needed c = the (Symtab.lookup ct c) > 0
   9.315 +    val cnfs =
   9.316 +      (optional_helpers
   9.317 +       |> full_types ? append optional_typed_helpers
   9.318 +       |> maps (fn (ss, (raw, ths)) =>
   9.319 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
   9.320 +                   else []))
   9.321 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   9.322 +  in map snd (make_axiom_clauses thy cnfs) end
   9.323 +
   9.324 +fun make_clause_table xs =
   9.325 +  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
   9.326 +
   9.327 +
   9.328 +(***************************************************************)
   9.329 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
   9.330 +(***************************************************************)
   9.331 +
   9.332 +fun set_insert (x, s) = Symtab.update (x, ()) s
   9.333 +
   9.334 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   9.335 +
   9.336 +(*Remove this trivial type class*)
   9.337 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   9.338 +
   9.339 +fun tfree_classes_of_terms ts =
   9.340 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   9.341 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   9.342 +
   9.343 +fun tvar_classes_of_terms ts =
   9.344 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   9.345 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   9.346 +
   9.347 +(*fold type constructors*)
   9.348 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   9.349 +  | fold_type_consts _ _ x = x;
   9.350 +
   9.351 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   9.352 +fun add_type_consts_in_term thy =
   9.353 +  let
   9.354 +    val const_typargs = Sign.const_typargs thy
   9.355 +    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   9.356 +      | aux (Abs (_, _, u)) = aux u
   9.357 +      | aux (Const (@{const_name skolem_id}, _) $ _) = I
   9.358 +      | aux (t $ u) = aux t #> aux u
   9.359 +      | aux _ = I
   9.360 +  in aux end
   9.361 +
   9.362 +fun type_consts_of_terms thy ts =
   9.363 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   9.364 +
   9.365 +(* Remove existing axiom clauses from the conjecture clauses, as this can
   9.366 +   dramatically boost an ATP's performance (for some reason). *)
   9.367 +fun subtract_cls ax_clauses =
   9.368 +  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   9.369 +
   9.370 +(* prepare for passing to writer,
   9.371 +   create additional clauses based on the information from extra_cls *)
   9.372 +fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   9.373 +  let
   9.374 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   9.375 +    val ccls = subtract_cls extra_cls goal_cls
   9.376 +    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   9.377 +    val ccltms = map prop_of ccls
   9.378 +    and axtms = map (prop_of o #1) extra_cls
   9.379 +    val subs = tfree_classes_of_terms ccltms
   9.380 +    and supers = tvar_classes_of_terms axtms
   9.381 +    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   9.382 +    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   9.383 +    val conjectures = make_conjecture_clauses thy ccls
   9.384 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   9.385 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   9.386 +    val helper_clauses =
   9.387 +      get_helper_clauses thy is_FO full_types conjectures extra_cls
   9.388 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   9.389 +    val classrel_clauses = make_classrel_clauses thy subs supers'
   9.390 +  in
   9.391 +    (Vector.fromList clnames,
   9.392 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   9.393 +  end
   9.394 +
   9.395  end;
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 16:29:07 2010 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,349 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
    10.5 -    Author:     Jia Meng, NICTA
    10.6 -    Author:     Jasmin Blanchette, TU Muenchen
    10.7 -
    10.8 -FOL clauses translated from HOL formulas.
    10.9 -*)
   10.10 -
   10.11 -signature SLEDGEHAMMER_HOL_CLAUSE =
   10.12 -sig
   10.13 -  type cnf_thm = Clausifier.cnf_thm
   10.14 -  type name = Sledgehammer_FOL_Clause.name
   10.15 -  type name_pool = Sledgehammer_FOL_Clause.name_pool
   10.16 -  type kind = Sledgehammer_FOL_Clause.kind
   10.17 -  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   10.18 -  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
   10.19 -
   10.20 -  datatype combtyp =
   10.21 -    TyVar of name |
   10.22 -    TyFree of name |
   10.23 -    TyConstr of name * combtyp list
   10.24 -  datatype combterm =
   10.25 -    CombConst of name * combtyp * combtyp list (* Const and Free *) |
   10.26 -    CombVar of name * combtyp |
   10.27 -    CombApp of combterm * combterm
   10.28 -  datatype literal = Literal of bool * combterm
   10.29 -  datatype hol_clause =
   10.30 -    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
   10.31 -                  literals: literal list, ctypes_sorts: typ list}
   10.32 -  exception TRIVIAL of unit
   10.33 -
   10.34 -  val type_of_combterm : combterm -> combtyp
   10.35 -  val strip_combterm_comb : combterm -> combterm * combterm list
   10.36 -  val literals_of_term : theory -> term -> literal list * typ list
   10.37 -  val conceal_skolem_somes :
   10.38 -    int -> (string * term) list -> term -> (string * term) list * term
   10.39 -  val is_quasi_fol_theorem : theory -> thm -> bool
   10.40 -  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
   10.41 -  val tfree_classes_of_terms : term list -> string list
   10.42 -  val tvar_classes_of_terms : term list -> string list
   10.43 -  val type_consts_of_terms : theory -> term list -> string list
   10.44 -  val prepare_clauses :
   10.45 -    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
   10.46 -    -> string vector
   10.47 -       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
   10.48 -          * classrel_clause list * arity_clause list)
   10.49 -end
   10.50 -
   10.51 -structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
   10.52 -struct
   10.53 -
   10.54 -open Clausifier
   10.55 -open Sledgehammer_Util
   10.56 -open Sledgehammer_FOL_Clause
   10.57 -
   10.58 -(******************************************************)
   10.59 -(* data types for typed combinator expressions        *)
   10.60 -(******************************************************)
   10.61 -
   10.62 -datatype combtyp =
   10.63 -  TyVar of name |
   10.64 -  TyFree of name |
   10.65 -  TyConstr of name * combtyp list
   10.66 -
   10.67 -datatype combterm =
   10.68 -  CombConst of name * combtyp * combtyp list (* Const and Free *) |
   10.69 -  CombVar of name * combtyp |
   10.70 -  CombApp of combterm * combterm
   10.71 -
   10.72 -datatype literal = Literal of bool * combterm
   10.73 -
   10.74 -datatype hol_clause =
   10.75 -  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
   10.76 -                literals: literal list, ctypes_sorts: typ list}
   10.77 -
   10.78 -(*********************************************************************)
   10.79 -(* convert a clause with type Term.term to a clause with type clause *)
   10.80 -(*********************************************************************)
   10.81 -
   10.82 -(*Result of a function type; no need to check that the argument type matches.*)
   10.83 -fun result_type (TyConstr (_, [_, tp2])) = tp2
   10.84 -  | result_type _ = raise Fail "non-function type"
   10.85 -
   10.86 -fun type_of_combterm (CombConst (_, tp, _)) = tp
   10.87 -  | type_of_combterm (CombVar (_, tp)) = tp
   10.88 -  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
   10.89 -
   10.90 -(*gets the head of a combinator application, along with the list of arguments*)
   10.91 -fun strip_combterm_comb u =
   10.92 -    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   10.93 -        |   stripc  x =  x
   10.94 -    in stripc(u,[]) end
   10.95 -
   10.96 -fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
   10.97 -      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
   10.98 -  | isFalse _ = false;
   10.99 -
  10.100 -fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
  10.101 -      (pol andalso c = "c_True") orelse
  10.102 -      (not pol andalso c = "c_False")
  10.103 -  | isTrue _ = false;
  10.104 -
  10.105 -fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
  10.106 -
  10.107 -fun type_of (Type (a, Ts)) =
  10.108 -    let val (folTypes,ts) = types_of Ts in
  10.109 -      (TyConstr (`make_fixed_type_const a, folTypes), ts)
  10.110 -    end
  10.111 -  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
  10.112 -  | type_of (tp as TVar (x, _)) =
  10.113 -    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
  10.114 -and types_of Ts =
  10.115 -    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
  10.116 -      (folTyps, union_all ts)
  10.117 -    end
  10.118 -
  10.119 -(* same as above, but no gathering of sort information *)
  10.120 -fun simp_type_of (Type (a, Ts)) =
  10.121 -      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
  10.122 -  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
  10.123 -  | simp_type_of (TVar (x, _)) =
  10.124 -    TyVar (make_schematic_type_var x, string_of_indexname x)
  10.125 -
  10.126 -(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
  10.127 -fun combterm_of thy (Const (c, T)) =
  10.128 -      let
  10.129 -        val (tp, ts) = type_of T
  10.130 -        val tvar_list =
  10.131 -          (if String.isPrefix skolem_theory_name c then
  10.132 -             [] |> Term.add_tvarsT T |> map TVar
  10.133 -           else
  10.134 -             (c, T) |> Sign.const_typargs thy)
  10.135 -          |> map simp_type_of
  10.136 -        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
  10.137 -      in  (c',ts)  end
  10.138 -  | combterm_of _ (Free(v, T)) =
  10.139 -      let val (tp,ts) = type_of T
  10.140 -          val v' = CombConst (`make_fixed_var v, tp, [])
  10.141 -      in  (v',ts)  end
  10.142 -  | combterm_of _ (Var(v, T)) =
  10.143 -      let val (tp,ts) = type_of T
  10.144 -          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
  10.145 -      in  (v',ts)  end
  10.146 -  | combterm_of thy (P $ Q) =
  10.147 -      let val (P', tsP) = combterm_of thy P
  10.148 -          val (Q', tsQ) = combterm_of thy Q
  10.149 -      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
  10.150 -  | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
  10.151 -
  10.152 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
  10.153 -  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
  10.154 -
  10.155 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
  10.156 -    literals_of_term1 args thy P
  10.157 -  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
  10.158 -    literals_of_term1 (literals_of_term1 args thy P) thy Q
  10.159 -  | literals_of_term1 (lits, ts) thy P =
  10.160 -    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
  10.161 -      (Literal (pol, pred) :: lits, union (op =) ts ts')
  10.162 -    end
  10.163 -val literals_of_term = literals_of_term1 ([], [])
  10.164 -
  10.165 -fun skolem_name i j num_T_args =
  10.166 -  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
  10.167 -  skolem_infix ^ "g"
  10.168 -
  10.169 -fun conceal_skolem_somes i skolem_somes t =
  10.170 -  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
  10.171 -    let
  10.172 -      fun aux skolem_somes
  10.173 -              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
  10.174 -          let
  10.175 -            val (skolem_somes, s) =
  10.176 -              if i = ~1 then
  10.177 -                (skolem_somes, @{const_name undefined})
  10.178 -              else case AList.find (op aconv) skolem_somes t of
  10.179 -                s :: _ => (skolem_somes, s)
  10.180 -              | [] =>
  10.181 -                let
  10.182 -                  val s = skolem_theory_name ^ "." ^
  10.183 -                          skolem_name i (length skolem_somes)
  10.184 -                                        (length (Term.add_tvarsT T []))
  10.185 -                in ((s, t) :: skolem_somes, s) end
  10.186 -          in (skolem_somes, Const (s, T)) end
  10.187 -        | aux skolem_somes (t1 $ t2) =
  10.188 -          let
  10.189 -            val (skolem_somes, t1) = aux skolem_somes t1
  10.190 -            val (skolem_somes, t2) = aux skolem_somes t2
  10.191 -          in (skolem_somes, t1 $ t2) end
  10.192 -        | aux skolem_somes (Abs (s, T, t')) =
  10.193 -          let val (skolem_somes, t') = aux skolem_somes t' in
  10.194 -            (skolem_somes, Abs (s, T, t'))
  10.195 -          end
  10.196 -        | aux skolem_somes t = (skolem_somes, t)
  10.197 -    in aux skolem_somes t end
  10.198 -  else
  10.199 -    (skolem_somes, t)
  10.200 -
  10.201 -fun is_quasi_fol_theorem thy =
  10.202 -  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
  10.203 -
  10.204 -(* Trivial problem, which resolution cannot handle (empty clause) *)
  10.205 -exception TRIVIAL of unit
  10.206 -
  10.207 -(* making axiom and conjecture clauses *)
  10.208 -fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
  10.209 -  let
  10.210 -    val (skolem_somes, t) =
  10.211 -      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
  10.212 -    val (lits, ctypes_sorts) = literals_of_term thy t
  10.213 -  in
  10.214 -    if forall isFalse lits then
  10.215 -      raise TRIVIAL ()
  10.216 -    else
  10.217 -      (skolem_somes,
  10.218 -       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
  10.219 -                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
  10.220 -  end
  10.221 -
  10.222 -fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
  10.223 -  let
  10.224 -    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
  10.225 -  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
  10.226 -
  10.227 -fun make_axiom_clauses thy clauses =
  10.228 -  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
  10.229 -
  10.230 -fun make_conjecture_clauses thy =
  10.231 -  let
  10.232 -    fun aux _ _ [] = []
  10.233 -      | aux n skolem_somes (th :: ths) =
  10.234 -        let
  10.235 -          val (skolem_somes, cls) =
  10.236 -            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
  10.237 -        in cls :: aux (n + 1) skolem_somes ths end
  10.238 -  in aux 0 [] end
  10.239 -
  10.240 -(** Helper clauses **)
  10.241 -
  10.242 -fun count_combterm (CombConst ((c, _), _, _)) =
  10.243 -    Symtab.map_entry c (Integer.add 1)
  10.244 -  | count_combterm (CombVar _) = I
  10.245 -  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
  10.246 -fun count_literal (Literal (_, t)) = count_combterm t
  10.247 -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
  10.248 -
  10.249 -fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
  10.250 -fun cnf_helper_thms thy raw =
  10.251 -  map (`Thm.get_name_hint)
  10.252 -  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
  10.253 -
  10.254 -val optional_helpers =
  10.255 -  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
  10.256 -   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
  10.257 -   (["c_COMBS"], (false, @{thms COMBS_def}))]
  10.258 -val optional_typed_helpers =
  10.259 -  [(["c_True", "c_False"], (true, @{thms True_or_False})),
  10.260 -   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
  10.261 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
  10.262 -
  10.263 -val init_counters =
  10.264 -  Symtab.make (maps (maps (map (rpair 0) o fst))
  10.265 -                    [optional_helpers, optional_typed_helpers])
  10.266 -
  10.267 -fun get_helper_clauses thy is_FO full_types conjectures axcls =
  10.268 -  let
  10.269 -    val axclauses = map snd (make_axiom_clauses thy axcls)
  10.270 -    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
  10.271 -    fun is_needed c = the (Symtab.lookup ct c) > 0
  10.272 -    val cnfs =
  10.273 -      (optional_helpers
  10.274 -       |> full_types ? append optional_typed_helpers
  10.275 -       |> maps (fn (ss, (raw, ths)) =>
  10.276 -                   if exists is_needed ss then cnf_helper_thms thy raw ths
  10.277 -                   else []))
  10.278 -      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
  10.279 -  in map snd (make_axiom_clauses thy cnfs) end
  10.280 -
  10.281 -fun make_clause_table xs =
  10.282 -  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
  10.283 -
  10.284 -
  10.285 -(***************************************************************)
  10.286 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
  10.287 -(***************************************************************)
  10.288 -
  10.289 -fun set_insert (x, s) = Symtab.update (x, ()) s
  10.290 -
  10.291 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  10.292 -
  10.293 -(*Remove this trivial type class*)
  10.294 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
  10.295 -
  10.296 -fun tfree_classes_of_terms ts =
  10.297 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
  10.298 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  10.299 -
  10.300 -fun tvar_classes_of_terms ts =
  10.301 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
  10.302 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  10.303 -
  10.304 -(*fold type constructors*)
  10.305 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
  10.306 -  | fold_type_consts _ _ x = x;
  10.307 -
  10.308 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  10.309 -fun add_type_consts_in_term thy =
  10.310 -  let
  10.311 -    val const_typargs = Sign.const_typargs thy
  10.312 -    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
  10.313 -      | aux (Abs (_, _, u)) = aux u
  10.314 -      | aux (Const (@{const_name skolem_id}, _) $ _) = I
  10.315 -      | aux (t $ u) = aux t #> aux u
  10.316 -      | aux _ = I
  10.317 -  in aux end
  10.318 -
  10.319 -fun type_consts_of_terms thy ts =
  10.320 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
  10.321 -
  10.322 -(* Remove existing axiom clauses from the conjecture clauses, as this can
  10.323 -   dramatically boost an ATP's performance (for some reason). *)
  10.324 -fun subtract_cls ax_clauses =
  10.325 -  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
  10.326 -
  10.327 -(* prepare for passing to writer,
  10.328 -   create additional clauses based on the information from extra_cls *)
  10.329 -fun prepare_clauses full_types goal_cls axcls extra_cls thy =
  10.330 -  let
  10.331 -    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
  10.332 -    val ccls = subtract_cls extra_cls goal_cls
  10.333 -    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
  10.334 -    val ccltms = map prop_of ccls
  10.335 -    and axtms = map (prop_of o #1) extra_cls
  10.336 -    val subs = tfree_classes_of_terms ccltms
  10.337 -    and supers = tvar_classes_of_terms axtms
  10.338 -    and tycons = type_consts_of_terms thy (ccltms @ axtms)
  10.339 -    (*TFrees in conjecture clauses; TVars in axiom clauses*)
  10.340 -    val conjectures = make_conjecture_clauses thy ccls
  10.341 -    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
  10.342 -    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
  10.343 -    val helper_clauses =
  10.344 -      get_helper_clauses thy is_FO full_types conjectures extra_cls
  10.345 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  10.346 -    val classrel_clauses = make_classrel_clauses thy subs supers'
  10.347 -  in
  10.348 -    (Vector.fromList clnames,
  10.349 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
  10.350 -  end
  10.351 -
  10.352 -end;
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 16:29:07 2010 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 16:42:06 2010 +0200
    11.3 @@ -30,7 +30,6 @@
    11.4  open Clausifier
    11.5  open Sledgehammer_Util
    11.6  open Sledgehammer_FOL_Clause
    11.7 -open Sledgehammer_HOL_Clause
    11.8  
    11.9  type minimize_command = string list -> string
   11.10  
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jun 25 16:29:07 2010 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jun 25 16:42:06 2010 +0200
    12.3 @@ -11,7 +11,7 @@
    12.4    type type_literal = Sledgehammer_FOL_Clause.type_literal
    12.5    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    12.6    type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    12.7 -  type hol_clause = Sledgehammer_HOL_Clause.hol_clause
    12.8 +  type hol_clause = Sledgehammer_FOL_Clause.hol_clause
    12.9  
   12.10    val tptp_of_type_literal :
   12.11      bool -> type_literal -> name_pool option -> string * name_pool option
   12.12 @@ -27,7 +27,6 @@
   12.13  
   12.14  open Sledgehammer_Util
   12.15  open Sledgehammer_FOL_Clause
   12.16 -open Sledgehammer_HOL_Clause
   12.17  
   12.18  type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   12.19