renamed type systems for more consistency
authorblanchet
Thu May 12 15:29:18 2011 +0200 (2011-05-12)
changeset 42722626e292d22a7
parent 42715 fe8ee8099b47
child 42723 c1909691bbf0
renamed type systems for more consistency
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Metis_Examples/HO_Reas.thy
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 11:03:48 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:18 2011 +0200
     1.3 @@ -460,7 +460,7 @@
     1.4  developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
     1.5  servers. This ATP supports a fragment of the TPTP many-typed first-order format
     1.6  (TFF). It is supported primarily for experimenting with the
     1.7 -\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
     1.8 +\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}).
     1.9  
    1.10  \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
    1.11  developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
    1.12 @@ -571,85 +571,81 @@
    1.13  following values:
    1.14  
    1.15  \begin{enum}
    1.16 -\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for
    1.17 -many-typed first-order logic if available; otherwise, fall back on
    1.18 -\textit{mangled\_preds}. The problem is monomorphized, meaning that the
    1.19 -problem's type variables are instantiated with heuristically chosen ground
    1.20 -types. Monomorphization can simplify reasoning but also leads to larger fact
    1.21 -bases, which can slow down the ATPs.
    1.22 +%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for
    1.23 +%polymorphic first-order logic if available; otherwise, fall back on
    1.24 +%\textit{poly\_preds}.
    1.25  
    1.26 -\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate
    1.27 +\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate
    1.28  $\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
    1.29  Constants are annotated with their types, supplied as extra arguments, to
    1.30  resolve overloading.
    1.31  
    1.32 -\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
    1.33 +\item[$\bullet$] \textbf{\textit{poly\_tags}:} Each term and subterm is tagged with
    1.34  its type using a function $\mathit{type\_info\/}(\tau, t)$.
    1.35  
    1.36 -\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
    1.37 -the problem is additionally monomorphized.
    1.38 +\item[$\bullet$] \textbf{\textit{poly\_args}:}
    1.39 +Like for the other sound encodings, constants are annotated with their types to
    1.40 +resolve overloading, but otherwise no type information is encoded.
    1.41  
    1.42 -\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
    1.43 -the problem is additionally monomorphized.
    1.44 +\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
    1.45 +the ATP. Types are simply erased.
    1.46  
    1.47 -\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
    1.48 -\textit{mono\_preds}, but types are mangled in constant names instead of being
    1.49 -supplied as ground term arguments. The binary predicate
    1.50 -$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
    1.51 -$\mathit{has\_type\_}\tau(t)$.
    1.52 +\item[$\bullet$]
    1.53 +\textbf{%
    1.54 +\textit{mono\_preds},
    1.55 +\textit{mono\_tags},
    1.56 +\textit{mono\_args}:} \\
    1.57 +Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args},
    1.58 +respectively, but the problem is additionally monomorphized, meaning that type
    1.59 +variables are instantiated with heuristically chosen ground types.
    1.60 +Monomorphization can simplify reasoning but also leads to larger fact bases,
    1.61 +which can slow down the ATPs.
    1.62  
    1.63 -\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
    1.64 -\textit{mono\_tags}, but types are mangled in constant names instead of being
    1.65 -supplied as ground term arguments. The binary function
    1.66 +\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for
    1.67 +simply typed first-order logic if available; otherwise, fall back on
    1.68 +\textit{mangled\_preds}. The problem is monomorphized.
    1.69 +
    1.70 +\item[$\bullet$]
    1.71 +\textbf{%
    1.72 +\textit{mangled\_preds},
    1.73 +\textit{mangled\_tags},
    1.74 +\textit{mangled\_args}:} \\
    1.75 +Similar to
    1.76 +\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
    1.77 +respectively but types are mangled in constant names instead of being supplied
    1.78 +as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
    1.79 +becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
    1.80  $\mathit{type\_info\/}(\tau, t)$ becomes a unary function
    1.81  $\mathit{type\_info\_}\tau(t)$.
    1.82  
    1.83  \item[$\bullet$]
    1.84  \textbf{%
    1.85 -\textit{simple}?,
    1.86 -\textit{preds}?,
    1.87 -\textit{mono\_preds}?,
    1.88 -\textit{mangled\_preds}?, \\
    1.89 -\textit{tags}?,
    1.90 -\textit{mono\_tags}?,
    1.91 -\textit{mangled\_tags}?:} \\
    1.92 -The type systems \textit{simple}, \textit{preds}, \textit{mono\_preds},
    1.93 -\textit{mangled\_preds}, \textit{tags}, \textit{mono\_tags}, and
    1.94 -\textit{mangled\_tags} are fully typed and virtually sound---i.e., except for
    1.95 -pathological cases, all found proofs are type-correct. For each of these,
    1.96 -Sledgehammer also provides a just-as-sound partially typed variant identified by
    1.97 -a question mark (`{?}')\ that detects and erases monotonic types, notably infinite
    1.98 -types. (For \textit{simple}, the types are not actually erased but rather
    1.99 -replaced by a shared uniform ``top'' type.)
   1.100 +\textit{simple\_types}?,
   1.101 +\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
   1.102 +The type systems \textit{poly\_preds}, \textit{poly\_tags},
   1.103 +\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
   1.104 +\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
   1.105 +virtually sound---except for pathological cases, all found proofs are
   1.106 +type-correct. For each of these, Sledgehammer also provides a just-as-sound
   1.107 +partially typed variant identified by a question mark (`{?}')\ that detects and
   1.108 +erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
   1.109 +types are not actually erased but rather replaced by a shared uniform type.)
   1.110  
   1.111  \item[$\bullet$]
   1.112  \textbf{%
   1.113 -\textit{simple}!,
   1.114 -\textit{preds}!,
   1.115 -\textit{mono\_preds}!,
   1.116 -\textit{mangled\_preds}!, \\
   1.117 -\textit{tags}!,
   1.118 -\textit{mono\_tags}!,
   1.119 -\textit{mangled\_tags}!:} \\
   1.120 +\textit{simple\_types}!,
   1.121 +\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\
   1.122  If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
   1.123  translation erases all types except those that are clearly finite (e.g.,
   1.124  \textit{bool}). This encoding is unsound.
   1.125  
   1.126 -\item[$\bullet$] \textbf{\textit{args}:}
   1.127 -Like for the other sound encodings, constants are annotated with their types to
   1.128 -resolve overloading, but otherwise no type information is encoded. This encoding
   1.129 -is hence less sound than the exclamation mark (`{!}')\ variants described above.
   1.130 -
   1.131 -\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
   1.132 -the ATP. Types are simply erased.
   1.133 -
   1.134  \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
   1.135  uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
   1.136  actual encoding used depends on the ATP and should be the most efficient for
   1.137  that ATP.
   1.138  \end{enum}
   1.139  
   1.140 -For SMT solvers and ToFoF-E, the type system is always \textit{simple}.
   1.141 +For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
   1.142  
   1.143  \opdefault{monomorphize\_limit}{int}{\upshape 4}
   1.144  Specifies the maximum number of iterations for the monomorphization fixpoint
     2.1 --- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 11:03:48 2011 +0200
     2.2 +++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:18 2011 +0200
     2.3 @@ -14,12 +14,12 @@
     2.4  
     2.5  lemma "id True"
     2.6  sledgehammer [type_sys = erased, expect = some] (id_apply)
     2.7 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
     2.8 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
     2.9 -sledgehammer [type_sys = tags, expect = some] (id_apply)
    2.10 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
    2.11 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
    2.12 -sledgehammer [type_sys = preds, expect = some] (id_apply)
    2.13 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
    2.14 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
    2.15 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
    2.16 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
    2.17 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
    2.18 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
    2.19  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
    2.20  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    2.21  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    2.22 @@ -27,12 +27,12 @@
    2.23  
    2.24  lemma "\<not> id False"
    2.25  sledgehammer [type_sys = erased, expect = some] (id_apply)
    2.26 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
    2.27 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
    2.28 -sledgehammer [type_sys = tags, expect = some] (id_apply)
    2.29 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
    2.30 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
    2.31 -sledgehammer [type_sys = preds, expect = some] (id_apply)
    2.32 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
    2.33 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
    2.34 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
    2.35 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
    2.36 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
    2.37 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
    2.38  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
    2.39  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    2.40  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    2.41 @@ -40,12 +40,12 @@
    2.42  
    2.43  lemma "x = id True \<or> x = id False"
    2.44  sledgehammer [type_sys = erased, expect = some] (id_apply)
    2.45 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
    2.46 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
    2.47 -sledgehammer [type_sys = tags, expect = some] (id_apply)
    2.48 -sledgehammer [type_sys = preds, expect = some] (id_apply)
    2.49 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
    2.50 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
    2.51 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
    2.52 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
    2.53 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
    2.54 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
    2.55 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
    2.56 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
    2.57  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
    2.58  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    2.59  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    2.60 @@ -53,12 +53,12 @@
    2.61  
    2.62  lemma "id x = id True \<or> id x = id False"
    2.63  sledgehammer [type_sys = erased, expect = some] (id_apply)
    2.64 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
    2.65 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
    2.66 -sledgehammer [type_sys = tags, expect = some] (id_apply)
    2.67 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
    2.68 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
    2.69 -sledgehammer [type_sys = preds, expect = some] (id_apply)
    2.70 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
    2.71 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
    2.72 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
    2.73 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
    2.74 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
    2.75 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
    2.76  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
    2.77  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    2.78  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    2.79 @@ -66,13 +66,13 @@
    2.80  
    2.81  lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
    2.82  sledgehammer [type_sys = erased, expect = none] ()
    2.83 -sledgehammer [type_sys = args, expect = none] ()
    2.84 -sledgehammer [type_sys = tags!, expect = some] ()
    2.85 -sledgehammer [type_sys = tags?, expect = some] ()
    2.86 -sledgehammer [type_sys = tags, expect = some] ()
    2.87 -sledgehammer [type_sys = preds!, expect = some] ()
    2.88 -sledgehammer [type_sys = preds?, expect = some] ()
    2.89 -sledgehammer [type_sys = preds, expect = some] ()
    2.90 +sledgehammer [type_sys = poly_args, expect = none] ()
    2.91 +sledgehammer [type_sys = poly_tags!, expect = some] ()
    2.92 +sledgehammer [type_sys = poly_tags?, expect = some] ()
    2.93 +sledgehammer [type_sys = poly_tags, expect = some] ()
    2.94 +sledgehammer [type_sys = poly_preds!, expect = some] ()
    2.95 +sledgehammer [type_sys = poly_preds?, expect = some] ()
    2.96 +sledgehammer [type_sys = poly_preds, expect = some] ()
    2.97  sledgehammer [type_sys = mangled_preds!, expect = some] ()
    2.98  sledgehammer [type_sys = mangled_preds?, expect = some] ()
    2.99  sledgehammer [type_sys = mangled_preds, expect = some] ()
   2.100 @@ -80,12 +80,12 @@
   2.101  
   2.102  lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
   2.103  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.104 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.105 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.106 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.107 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.108 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.109 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.110 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.111 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.112 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.113 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.114 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.115 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.116  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.117  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.118  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.119 @@ -93,12 +93,12 @@
   2.120  
   2.121  lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
   2.122  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.123 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.124 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.125 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.126 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.127 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.128 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.129 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.130 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.131 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.132 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.133 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.134 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.135  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.136  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.137  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.138 @@ -106,12 +106,12 @@
   2.139  
   2.140  lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
   2.141  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.142 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.143 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.144 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.145 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.146 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.147 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.148 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.149 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.150 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.151 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.152 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.153 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.154  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.155  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.156  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.157 @@ -119,12 +119,12 @@
   2.158  
   2.159  lemma "id (a \<and> b) \<Longrightarrow> id a"
   2.160  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.161 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.162 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.163 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.164 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.165 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.166 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.167 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.168 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.169 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.170 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.171 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.172 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.173  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.174  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.175  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.176 @@ -132,12 +132,12 @@
   2.177  
   2.178  lemma "id (a \<and> b) \<Longrightarrow> id b"
   2.179  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.180 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.181 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.182 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.183 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.184 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.185 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.186 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.187 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.188 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.189 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.190 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.191 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.192  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.193  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.194  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.195 @@ -145,12 +145,12 @@
   2.196  
   2.197  lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
   2.198  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.199 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.200 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.201 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.202 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.203 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.204 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.205 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.206 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.207 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.208 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.209 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.210 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.211  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.212  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.213  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.214 @@ -158,12 +158,12 @@
   2.215  
   2.216  lemma "id a \<Longrightarrow> id (a \<or> b)"
   2.217  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.218 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.219 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.220 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.221 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.222 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.223 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.224 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.225 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.226 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.227 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.228 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.229 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.230  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.231  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.232  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.233 @@ -171,12 +171,12 @@
   2.234  
   2.235  lemma "id b \<Longrightarrow> id (a \<or> b)"
   2.236  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.237 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.238 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.239 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.240 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.241 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.242 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.243 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.244 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.245 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.246 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.247 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.248 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.249  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.250  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.251  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.252 @@ -184,12 +184,12 @@
   2.253  
   2.254  lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
   2.255  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.256 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.257 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.258 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.259 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.260 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.261 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.262 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.263 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.264 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.265 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.266 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.267 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.268  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.269  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.270  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.271 @@ -197,12 +197,12 @@
   2.272  
   2.273  lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
   2.274  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.275 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.276 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.277 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.278 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.279 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.280 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.281 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.282 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.283 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.284 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.285 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.286 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.287  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.288  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.289  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   2.290 @@ -210,12 +210,12 @@
   2.291  
   2.292  lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
   2.293  sledgehammer [type_sys = erased, expect = some] (id_apply)
   2.294 -sledgehammer [type_sys = tags!, expect = some] (id_apply)
   2.295 -sledgehammer [type_sys = tags?, expect = some] (id_apply)
   2.296 -sledgehammer [type_sys = tags, expect = some] (id_apply)
   2.297 -sledgehammer [type_sys = preds!, expect = some] (id_apply)
   2.298 -sledgehammer [type_sys = preds?, expect = some] (id_apply)
   2.299 -sledgehammer [type_sys = preds, expect = some] (id_apply)
   2.300 +sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
   2.301 +sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
   2.302 +sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
   2.303 +sledgehammer [type_sys = poly_preds!, expect = some] (id_apply)
   2.304 +sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
   2.305 +sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
   2.306  sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
   2.307  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   2.308  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 11:03:48 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:18 2011 +0200
     3.3 @@ -23,6 +23,12 @@
     3.4                 * string fo_term option * string fo_term option
     3.5    type 'a problem = (string * 'a problem_line list) list
     3.6  
     3.7 +(* official TPTP syntax *)
     3.8 +  val tptp_tff_type_of_types : string
     3.9 +  val tptp_tff_bool_type : string
    3.10 +  val tptp_tff_individual_type : string
    3.11 +  val tptp_false : string
    3.12 +  val tptp_true : string
    3.13    val timestamp : unit -> string
    3.14    val hashw : word * word -> word
    3.15    val hashw_string : string * word -> word
    3.16 @@ -55,6 +61,13 @@
    3.17               * string fo_term option * string fo_term option
    3.18  type 'a problem = (string * 'a problem_line list) list
    3.19  
    3.20 +(* official TPTP syntax *)
    3.21 +val tptp_tff_type_of_types = "$tType"
    3.22 +val tptp_tff_bool_type = "$o"
    3.23 +val tptp_tff_individual_type = "$i"
    3.24 +val tptp_false = "$false"
    3.25 +val tptp_true = "$true"
    3.26 +
    3.27  val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    3.28  
    3.29  (* This hash function is recommended in Compilers: Principles, Techniques, and
    3.30 @@ -87,20 +100,21 @@
    3.31    | string_for_connective AIf = "<="
    3.32    | string_for_connective AIff = "<=>"
    3.33    | string_for_connective ANotIff = "<~>"
    3.34 -fun string_for_bound_var (s, NONE) = s
    3.35 -  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty
    3.36 -fun string_for_formula (AQuant (q, xs, phi)) =
    3.37 +fun string_for_bound_var Fof (s, _) = s
    3.38 +  | string_for_bound_var Tff (s, ty) =
    3.39 +    s ^ " : " ^ (ty |> the_default tptp_tff_individual_type)
    3.40 +fun string_for_formula format (AQuant (q, xs, phi)) =
    3.41      "(" ^ string_for_quantifier q ^
    3.42 -    "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
    3.43 -    string_for_formula phi ^ ")"
    3.44 -  | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
    3.45 +    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
    3.46 +    string_for_formula format phi ^ ")"
    3.47 +  | string_for_formula _ (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
    3.48      space_implode " != " (map string_for_term ts)
    3.49 -  | string_for_formula (AConn (c, [phi])) =
    3.50 -    "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
    3.51 -  | string_for_formula (AConn (c, phis)) =
    3.52 +  | string_for_formula format (AConn (c, [phi])) =
    3.53 +    "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
    3.54 +  | string_for_formula format (AConn (c, phis)) =
    3.55      "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
    3.56 -                        (map string_for_formula phis) ^ ")"
    3.57 -  | string_for_formula (AAtom tm) = string_for_term tm
    3.58 +                        (map (string_for_formula format) phis) ^ ")"
    3.59 +  | string_for_formula _ (AAtom tm) = string_for_term tm
    3.60  
    3.61  fun string_for_symbol_type [] res_ty = res_ty
    3.62    | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
    3.63 @@ -117,7 +131,7 @@
    3.64                              (Formula (ident, kind, phi, source, useful_info)) =
    3.65      (case format of Fof => "fof" | Tff => "tff") ^
    3.66      "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
    3.67 -    string_for_formula phi ^ ")" ^
    3.68 +    string_for_formula format phi ^ ")" ^
    3.69      (case (source, useful_info) of
    3.70         (NONE, NONE) => ""
    3.71       | (SOME tm, NONE) => ", " ^ string_for_term tm
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 11:03:48 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:18 2011 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4      All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
     4.5  
     4.6    datatype type_system =
     4.7 -    Simple of type_level |
     4.8 +    Simple_Types of type_level |
     4.9      Preds of polymorphism * type_level |
    4.10      Tags of polymorphism * type_level
    4.11  
    4.12 @@ -84,12 +84,6 @@
    4.13  
    4.14  fun make_tff_type s = tff_type_prefix ^ ascii_of s
    4.15  
    4.16 -(* official TPTP syntax *)
    4.17 -val tptp_tff_type_of_types = "$tType"
    4.18 -val tptp_tff_bool_type = "$o"
    4.19 -val tptp_false = "$false"
    4.20 -val tptp_true = "$true"
    4.21 -
    4.22  (* Freshness almost guaranteed! *)
    4.23  val sledgehammer_weak_prefix = "Sledgehammer:"
    4.24  
    4.25 @@ -98,7 +92,7 @@
    4.26    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    4.27  
    4.28  datatype type_system =
    4.29 -  Simple of type_level |
    4.30 +  Simple_Types of type_level |
    4.31    Preds of polymorphism * type_level |
    4.32    Tags of polymorphism * type_level
    4.33  
    4.34 @@ -106,12 +100,15 @@
    4.35    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    4.36  
    4.37  fun type_sys_from_string s =
    4.38 -  (case try (unprefix "mangled_") s of
    4.39 -     SOME s => (Mangled_Monomorphic, s)
    4.40 +  (case try (unprefix "poly_") s of
    4.41 +     SOME s => (SOME Polymorphic, s)
    4.42     | NONE =>
    4.43       case try (unprefix "mono_") s of
    4.44 -       SOME s => (Monomorphic, s)
    4.45 -     | NONE => (Polymorphic, s))
    4.46 +       SOME s => (SOME Monomorphic, s)
    4.47 +     | NONE =>
    4.48 +       case try (unprefix "mangled_") s of
    4.49 +         SOME s => (SOME Mangled_Monomorphic, s)
    4.50 +       | NONE => (NONE, s))
    4.51    ||> (fn s =>
    4.52            (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
    4.53            case try_unsuffixes ["?", "_query"] s of
    4.54 @@ -120,22 +117,22 @@
    4.55              case try_unsuffixes ["!", "_bang"] s of
    4.56                SOME s => (Finite_Types, s)
    4.57              | NONE => (All_Types, s))
    4.58 -  |> (fn (polymorphism, (level, core)) =>
    4.59 -         case (core, (polymorphism, level)) of
    4.60 -           ("simple", (Polymorphic (* naja *), level)) => Simple level
    4.61 -         | ("preds", extra) => Preds extra
    4.62 -         | ("tags", extra) => Tags extra
    4.63 -         | ("args", (_, All_Types (* naja *))) =>
    4.64 -           Preds (polymorphism, Const_Arg_Types)
    4.65 -         | ("erased", (Polymorphic, All_Types (* naja *))) =>
    4.66 -           Preds (polymorphism, No_Types)
    4.67 +  |> (fn (poly, (level, core)) =>
    4.68 +         case (core, (poly, level)) of
    4.69 +           ("simple_types", (NONE, level)) => Simple_Types level
    4.70 +         | ("preds", (SOME poly, level)) => Preds (poly, level)
    4.71 +         | ("tags", (SOME poly, level)) => Tags (poly, level)
    4.72 +         | ("args", (SOME poly, All_Types (* naja *))) =>
    4.73 +           Preds (poly, Const_Arg_Types)
    4.74 +         | ("erased", (NONE, All_Types (* naja *))) =>
    4.75 +           Preds (Polymorphic, No_Types)
    4.76           | _ => error ("Unknown type system: " ^ quote s ^ "."))
    4.77  
    4.78 -fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
    4.79 +fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
    4.80    | polymorphism_of_type_sys (Preds (poly, _)) = poly
    4.81    | polymorphism_of_type_sys (Tags (poly, _)) = poly
    4.82  
    4.83 -fun level_of_type_sys (Simple level) = level
    4.84 +fun level_of_type_sys (Simple_Types level) = level
    4.85    | level_of_type_sys (Preds (_, level)) = level
    4.86    | level_of_type_sys (Tags (_, level)) = level
    4.87  
    4.88 @@ -830,7 +827,7 @@
    4.89        end
    4.90      val do_bound_type =
    4.91        case type_sys of
    4.92 -        Simple level =>
    4.93 +        Simple_Types level =>
    4.94          SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
    4.95        | _ => K NONE
    4.96      fun do_out_of_bound_type (s, T) =
    4.97 @@ -933,7 +930,7 @@
    4.98  fun should_declare_sym type_sys pred_sym s =
    4.99    not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   4.100    not (String.isPrefix "$" s) andalso
   4.101 -  ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
   4.102 +  ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym)
   4.103  
   4.104  fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
   4.105    let
   4.106 @@ -1029,7 +1026,7 @@
   4.107  fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
   4.108                                  (s, decls) =
   4.109    case type_sys of
   4.110 -    Simple _ => map (decl_line_for_sym s) decls
   4.111 +    Simple_Types _ => map (decl_line_for_sym s) decls
   4.112    | _ =>
   4.113      let
   4.114        val decls =
   4.115 @@ -1129,7 +1126,7 @@
   4.116      val problem =
   4.117        problem
   4.118        |> (case type_sys of
   4.119 -            Simple _ =>
   4.120 +            Simple_Types _ =>
   4.121              cons (type_declsN,
   4.122                    map decl_line_for_tff_type (tff_types_in_problem problem))
   4.123            | _ => I)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 11:03:48 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
     5.3 @@ -346,14 +346,12 @@
     5.4  val atp_important_message_keep_quotient = 10
     5.5  
     5.6  val fallback_best_type_systems =
     5.7 -  [Preds (Polymorphic, Const_Arg_Types), Simple All_Types]
     5.8 +  [Preds (Polymorphic, Const_Arg_Types), Simple_Types All_Types]
     5.9  
    5.10 -fun adjust_dumb_type_sys formats (Simple level) =
    5.11 -    if member (op =) formats Tff then (Tff, Simple level)
    5.12 +fun adjust_dumb_type_sys formats (Simple_Types level) =
    5.13 +    if member (op =) formats Tff then (Tff, Simple_Types level)
    5.14      else (Fof, Preds (Mangled_Monomorphic, level))
    5.15 -  | adjust_dumb_type_sys formats type_sys =
    5.16 -    if member (op =) formats Fof then (Fof, type_sys)
    5.17 -    else (Tff, Simple (level_of_type_sys type_sys))
    5.18 +  | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
    5.19  fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
    5.20      adjust_dumb_type_sys formats type_sys
    5.21    | determine_format_and_type_sys best_type_systems formats