--- a/doc-src/Sledgehammer/sledgehammer.tex Wed May 04 15:37:39 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 05 15:01:32 2011 +0200
@@ -460,7 +460,7 @@
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
servers. This ATP supports a fragment of the TPTP many-typed first-order format
(TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{many\_typed} option (\S\ref{problem-encoding}).
+\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
@@ -553,11 +553,11 @@
not be found.
\opfalse{full\_types}{partial\_types}
-Specifies whether full-type information is encoded in ATP problems. Enabling
-this option can prevent the discovery of type-incorrect proofs, but it also
-tends to slow down the ATPs significantly. For historical reasons, the default
-value of this option can be overridden using the option ``Sledgehammer: Full
-Types'' from the ``Isabelle'' menu in Proof General.
+Specifies whether full type information is encoded in ATP problems. Enabling
+this option prevents the discovery of type-incorrect proofs, but it also tends
+to slow down the ATPs significantly. For historical reasons, the default value
+of this option can be overridden using the option ``Sledgehammer: Full Types''
+from the ``Isabelle'' menu in Proof General.
\opfalse{full\_types}{partial\_types}
Specifies whether full-type information is encoded in ATP problems. Enabling
@@ -571,7 +571,7 @@
following values:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
+\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for
many-typed first-order logic if available; otherwise, fall back on
\textit{mangled\_preds}. The problem is monomorphized, meaning that the
problem's type variables are instantiated with heuristically chosen ground
@@ -583,10 +583,14 @@
Constants are annotated with their types, supplied as extra arguments, to
resolve overloading.
+\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
+its type using a function $\mathit{type\_info\/}(\tau, t)$.
+
\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
-the problem is additionally monomorphized. This corresponds to the traditional
-encoding of types in an untyped logic without overloading (e.g., such as
-performed by the ToFoF-E wrapper).
+the problem is additionally monomorphized.
+
+\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
+the problem is additionally monomorphized.
\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
\textit{mono\_preds}, but types are mangled in constant names instead of being
@@ -594,12 +598,6 @@
$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
$\mathit{has\_type\_}\tau(t)$.
-\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
-its type using a function $\mathit{type\_info\/}(\tau, t)$.
-
-\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
-the problem is additionally monomorphized.
-
\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
\textit{mono\_tags}, but types are mangled in constant names instead of being
supplied as ground term arguments. The binary function
@@ -608,33 +606,39 @@
\item[$\bullet$]
\textbf{%
+\textit{simple}?,
+\textit{preds}?,
+\textit{mono\_preds}?,
+\textit{mangled\_preds}?, \\
+\textit{tags}?,
+\textit{mono\_tags}?,
+\textit{mangled\_tags}?:} \\
+The type systems \textit{simple}, \textit{preds}, \textit{mono\_preds},
+\textit{mangled\_preds}, \textit{tags}, \textit{mono\_tags}, and
+\textit{mangled\_tags} are fully typed and virtually sound---i.e., except for
+pathological cases, all found proofs are type-correct. For each of these,
+Sledgehammer also provides a just-as-sound partially typed variant identified by
+a question mark (`{?}')\ that detects and erases monotonic types, notably infinite
+types. (For \textit{simple}, the types are not actually erased but rather
+replaced by a shared uniform ``top'' type.)
+
+\item[$\bullet$]
+\textbf{%
+\textit{simple}!,
\textit{preds}!,
\textit{mono\_preds}!,
\textit{mangled\_preds}!, \\
\textit{tags}!,
\textit{mono\_tags}!,
\textit{mangled\_tags}!:} \\
-The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
-\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
-and virtually sound. For each of these, Sledgehammer also provides a mildly
-unsound variant identified by an exclamation mark (!)\ that types only finite
-(and hence especially dangerous) types.
+If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
+translation erases all types except those that are clearly finite (e.g.,
+\textit{bool}). This encoding is unsound.
-\item[$\bullet$]
-\textbf{%
-\textit{preds}?,
-\textit{mono\_preds}?,
-\textit{mangled\_preds}?, \\
-\textit{tags}?,
-\textit{mono\_tags}?,
-\textit{mangled\_tags}?:} \\
-If the exclamation mark (!)\ is replaced by an question mark (?),\ the type
-systems type only nonmonotonic (and hence especially dangerous) types. Not
-implemented yet.
-
-\item[$\bullet$] \textbf{\textit{const\_args}:}
-Constants are annotated with their types, supplied as extra arguments, to
-resolve overloading. Variables are unbounded.
+\item[$\bullet$] \textbf{\textit{args}:}
+Like for the other sound encodings, constants are annotated with their types to
+resolve overloading, but otherwise no type information is encoded. This encoding
+is hence less sound than the exclamation mark (`{!}')\ variants described above.
\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
the ATP. Types are simply erased.
@@ -645,7 +649,7 @@
that ATP.
\end{enum}
-For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
+For SMT solvers and ToFoF-E, the type system is always \textit{simple}.
\opdefault{monomorphize\_limit}{int}{\upshape 4}
Specifies the maximum number of iterations for the monomorphization fixpoint
--- a/src/HOL/Main.thy Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Main.thy Thu May 05 15:01:32 2011 +0200
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Record Predicate_Compile Quickcheck_Exhaustive Nitpick
+imports Plain Predicate_Compile Nitpick
begin
text {*
--- a/src/HOL/Metis_Examples/HO_Reas.thy Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy Thu May 05 15:01:32 2011 +0200
@@ -15,161 +15,209 @@
lemma "id True"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "\<not> id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "x = id True \<or> x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id x = id True \<or> id x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = const_args, expect = none] ()
+sledgehammer [type_sys = args, expect = none] ()
sledgehammer [type_sys = tags!, expect = some] ()
+sledgehammer [type_sys = tags?, expect = some] ()
sledgehammer [type_sys = tags, expect = some] ()
sledgehammer [type_sys = preds!, expect = some] ()
+sledgehammer [type_sys = preds?, expect = some] ()
sledgehammer [type_sys = preds, expect = some] ()
sledgehammer [type_sys = mangled_preds!, expect = some] ()
+sledgehammer [type_sys = mangled_preds?, expect = some] ()
sledgehammer [type_sys = mangled_preds, expect = some] ()
by metisFT
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
sledgehammer [type_sys = tags!, expect = some] (id_apply)
+sledgehammer [type_sys = tags?, expect = some] (id_apply)
sledgehammer [type_sys = tags, expect = some] (id_apply)
sledgehammer [type_sys = preds!, expect = some] (id_apply)
+sledgehammer [type_sys = preds?, expect = some] (id_apply)
sledgehammer [type_sys = preds, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
--- a/src/HOL/Record.thy Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Record.thy Thu May 05 15:01:32 2011 +0200
@@ -9,7 +9,7 @@
header {* Extensible records with structural subtyping *}
theory Record
-imports Plain Quickcheck
+imports Plain Quickcheck_Exhaustive
uses ("Tools/record.ML")
begin
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 05 15:01:32 2011 +0200
@@ -210,7 +210,8 @@
(0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
else
[(1.0, (true, 250 (* FUDGE *)))],
- best_type_systems = ["const_args", "mangled_preds"]}
+ best_type_systems =
+ [ "args", "mangled_preds!", "mangled_preds?", "mangled_preds"]}
val e = (eN, e_config)
@@ -241,7 +242,8 @@
best_slices =
K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
(0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
- best_type_systems = ["mangled_preds"]}
+ best_type_systems =
+ ["mangled_preds!", "mangled_preds?", "args", "mangled_preds"]}
val spass = (spassN, spass_config)
@@ -277,7 +279,8 @@
best_slices =
K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
(0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
- best_type_systems = ["mangled_preds"]}
+ best_type_systems =
+ ["mangled_preds?", "mangled_preds!", "args", "mangled_preds"]}
val vampire = (vampireN, vampire_config)
@@ -299,7 +302,7 @@
hypothesis_kind = Hypothesis,
formats = [Fof],
best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
- best_type_systems = []}
+ best_type_systems = [] (* FIXME *)}
val z3_atp = (z3_atpN, z3_atp_config)
@@ -378,14 +381,14 @@
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
val remote_tofof_e =
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"]
+ Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
val remote_sine_e =
remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
- (#best_type_systems e_config)
+ ["args", "preds", "tags"]
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r024"]
[("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
- (K 250 (* FUDGE *)) ["many_typed"]
+ (K 250 (* FUDGE *)) ["simple"]
(* Setup *)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 05 15:01:32 2011 +0200
@@ -570,17 +570,6 @@
"Code_Numeral.code_numeral"] s orelse
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
-(* TODO: use "Term_Subst.instantiateT" instead? *)
-fun instantiate_type thy T1 T1' T2 =
- Same.commit (Envir.subst_type_same
- (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
- handle Type.TYPE_MATCH =>
- raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
-fun varify_and_instantiate_type ctxt T1 T1' T2 =
- let val thy = Proof_Context.theory_of ctxt in
- instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
- end
-
fun repair_constr_type ctxt body_T' T =
varify_and_instantiate_type ctxt (body_type T) body_T' T
@@ -980,6 +969,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
+(* Similar to "Sledgehammer_ATP_Translate.tiny_card_of_type". *)
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
assigns T =
let
@@ -990,23 +980,20 @@
raise SAME ()
else case T of
Type (@{type_name fun}, [T1, T2]) =>
- let
- val k1 = aux avoid T1
- val k2 = aux avoid T2
- in
- if k1 = 0 orelse k2 = 0 then 0
- else if k1 >= max orelse k2 >= max then max
- else Int.min (max, reasonable_power k2 k1)
- end
+ (case (aux avoid T1, aux avoid T2) of
+ (_, 1) => 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, reasonable_power k2 k1))
| Type (@{type_name prod}, [T1, T2]) =>
- let
- val k1 = aux avoid T1
- val k2 = aux avoid T2
- in
- if k1 = 0 orelse k2 = 0 then 0
- else if k1 >= max orelse k2 >= max then max
- else Int.min (max, k1 * k2)
- end
+ (case (aux avoid T1, aux avoid T2) of
+ (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, k1 * k2))
| Type (@{type_name itself}, _) => 1
| @{typ prop} => 2
| @{typ bool} => 2
@@ -1021,7 +1008,7 @@
constrs
in
if exists (curry (op =) 0) constr_cards then 0
- else Integer.sum constr_cards
+ else Int.min (max, Integer.sum constr_cards)
end)
| _ => raise SAME ())
handle SAME () =>
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 05 15:01:32 2011 +0200
@@ -64,11 +64,13 @@
val typ_of_dtyp :
Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
-> typ
+ val varify_type : Proof.context -> typ -> typ
+ val instantiate_type : theory -> typ -> typ -> typ -> typ
+ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
val is_of_class_const : theory -> string * typ -> bool
val get_class_def : theory -> string -> (string * term) option
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> string * typ -> term -> term
- val varify_type : Proof.context -> typ -> typ
val eta_expand : typ list -> term -> int -> term
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -263,16 +265,14 @@
val simple_string_of_typ = Refute.string_of_typ
val is_real_constr = Refute.is_IDT_constructor
-val typ_of_dtyp = Refute.typ_of_dtyp
+val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
+val varify_type = Sledgehammer_Util.varify_type
+val instantiate_type = Sledgehammer_Util.instantiate_type
+val varify_and_instantiate_type = Sledgehammer_Util.varify_and_instantiate_type
val is_of_class_const = Refute.is_const_of_class
val get_class_def = Refute.get_classdef
val monomorphic_term = Sledgehammer_Util.monomorphic_term
val specialize_type = Sledgehammer_Util.specialize_type
-
-fun varify_type ctxt T =
- Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
- |> snd |> the_single |> dest_Const |> snd
-
val eta_expand = Sledgehammer_Util.eta_expand
fun time_limit NONE = I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu May 05 15:01:32 2011 +0200
@@ -176,8 +176,8 @@
fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
not o is_conjecture_referred_to_in_proof conjecture_shape andf
- forall (is_global_locality o snd)
- o used_facts_in_atp_proof type_sys facts_offset fact_names
+ forall (is_locality_global o snd)
+ o used_facts_in_atp_proof type_sys facts_offset fact_names
(** Soft-core proof reconstruction: Metis one-liner **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 05 15:01:32 2011 +0200
@@ -17,7 +17,7 @@
All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
datatype type_system =
- Many_Typed |
+ Simple of type_level |
Preds of polymorphism * type_level |
Tags of polymorphism * type_level
@@ -96,10 +96,13 @@
All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
datatype type_system =
- Many_Typed |
+ Simple of type_level |
Preds of polymorphism * type_level |
Tags of polymorphism * type_level
+fun try_unsuffixes ss s =
+ fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
+
fun type_sys_from_string s =
(case try (unprefix "mangled_") s of
SOME s => (Mangled_Monomorphic, s)
@@ -108,34 +111,34 @@
SOME s => (Monomorphic, s)
| NONE => (Polymorphic, s))
||> (fn s =>
- case try (unsuffix " ?") s of
+ (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
+ case try_unsuffixes ["?", "_query"] s of
SOME s => (Nonmonotonic_Types, s)
| NONE =>
- case try (unsuffix " !") s of
+ case try_unsuffixes ["!", "_bang"] s of
SOME s => (Finite_Types, s)
| NONE => (All_Types, s))
|> (fn (polymorphism, (level, core)) =>
case (core, (polymorphism, level)) of
- ("many_typed", (Polymorphic (* naja *), All_Types)) =>
- Many_Typed
+ ("simple", (Polymorphic (* naja *), level)) => Simple level
| ("preds", extra) => Preds extra
| ("tags", extra) => Tags extra
- | ("const_args", (_, All_Types (* naja *))) =>
+ | ("args", (_, All_Types (* naja *))) =>
Preds (polymorphism, Const_Arg_Types)
| ("erased", (Polymorphic, All_Types (* naja *))) =>
Preds (polymorphism, No_Types)
| _ => error ("Unknown type system: " ^ quote s ^ "."))
-fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
+fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
| polymorphism_of_type_sys (Preds (poly, _)) = poly
| polymorphism_of_type_sys (Tags (poly, _)) = poly
-fun level_of_type_sys Many_Typed = All_Types
+fun level_of_type_sys (Simple level) = level
| level_of_type_sys (Preds (_, level)) = level
| level_of_type_sys (Tags (_, level)) = level
-fun is_type_level_virtually_sound s =
- s = All_Types orelse s = Nonmonotonic_Types
+fun is_type_level_virtually_sound level =
+ level = All_Types orelse level = Nonmonotonic_Types
val is_type_sys_virtually_sound =
is_type_level_virtually_sound o level_of_type_sys
@@ -143,13 +146,24 @@
is_type_level_virtually_sound level orelse level = Finite_Types
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+fun is_type_level_partial level =
+ level = Nonmonotonic_Types orelse level = Finite_Types
+
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi
- | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
- | formula_fold f (AAtom tm) = f tm
+fun formula_fold pos f =
+ let
+ fun aux pos (AQuant (_, _, phi)) = aux pos phi
+ | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
+ | aux pos (AConn (AImplies, [phi1, phi2])) =
+ aux (Option.map not pos) phi1 #> aux pos phi2
+ | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
+ | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
+ | aux _ (AConn (_, phis)) = fold (aux NONE) phis
+ | aux pos (AAtom tm) = f pos tm
+ in aux (SOME pos) end
type translated_formula =
{name: string,
@@ -174,7 +188,7 @@
Tags (_, All_Types) => true
| _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
member (op =) boring_consts s))
-
+
datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
fun general_type_arg_policy type_sys =
@@ -445,6 +459,106 @@
(0 upto last) ts
end
+(** Finite and infinite type inference **)
+
+(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
+ dangerous because their "exhaust" properties can easily lead to unsound ATP
+ proofs. On the other hand, all HOL infinite types can be given the same
+ models in first-order logic (via Löwenheim-Skolem). *)
+
+fun datatype_constrs thy (T as Type (s, Ts)) =
+ (case Datatype.get_info thy s of
+ SOME {index, descr, ...} =>
+ let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
+ map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
+ end
+ | NONE => [])
+ | datatype_constrs _ _ = []
+
+(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
+ 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
+ cardinality 2 or more. The specified default cardinality is returned if the
+ cardinality of the type can't be determined. *)
+fun tiny_card_of_type ctxt default_card T =
+ let
+ val max = 2 (* 1 would be too small for the "fun" case *)
+ fun aux slack avoid T =
+ (if member (op =) avoid T then
+ 0
+ else case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | @{typ int} => 0 (* optimization *)
+ | Type (s, _) =>
+ let val thy = Proof_Context.theory_of ctxt in
+ case datatype_constrs thy T of
+ constrs as _ :: _ =>
+ let
+ val constr_cards =
+ map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+ o snd) constrs
+ in
+ if exists (curry (op =) 0) constr_cards then 0
+ else Int.min (max, Integer.sum constr_cards)
+ end
+ | [] =>
+ case Typedef.get_info ctxt s of
+ ({abs_type, rep_type, ...}, _) :: _ =>
+ (* We cheat here by assuming that typedef types are infinite if
+ their underlying type is infinite. This is unsound in general
+ but it's hard to think of a realistic example where this would
+ not be the case. We are also slack with representation types:
+ If a representation type has the form "sigma => tau", we
+ consider it enough to check "sigma" for infiniteness. (Look
+ for "slack" in this function.) *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ | [] => default_card
+ end
+ | TFree _ =>
+ (* Very slightly unsound: Type variables are assumed not to be
+ constrained to cardinality 1. (In practice, the user would most
+ likely have used "unit" directly anyway.) *)
+ if default_card = 1 then 2 else default_card
+ | _ => default_card)
+ in Int.min (max, aux false [] T) end
+
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
+fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+
+fun should_encode_type _ _ All_Types _ = true
+ | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
+ | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
+ exists (curry Type.raw_instance T) nonmono_Ts
+ | should_encode_type _ _ _ _ = false
+
+fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
+ should_encode_type ctxt nonmono_Ts level T
+ | should_predicate_on_type _ _ _ _ = false
+
+fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
+ should_encode_type ctxt nonmono_Ts level T
+ | should_tag_with_type _ _ _ _ = false
+
+val homo_infinite_T = @{typ ind} (* any infinite type *)
+
+fun homogenized_type ctxt nonmono_Ts level T =
+ if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T
+
(** "hBOOL" and "hAPP" **)
type sym_info =
@@ -475,7 +589,7 @@
end
in aux true end
fun add_fact_syms_to_table explicit_apply =
- fact_lift (formula_fold (add_combterm_syms_to_table explicit_apply))
+ fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply)))
val default_sym_table_entries : (string * sym_info) list =
[("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
@@ -546,29 +660,46 @@
| (head, args) => list_explicit_app head (map aux args)
in aux end
-fun impose_type_arg_policy_in_combterm type_sys =
+fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
let
fun aux (CombApp tmp) = CombApp (pairself aux tmp)
| aux (CombConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
- NONE => (name, T_args)
- | SOME s'' =>
- let val s'' = invert_const s'' in
- case type_arg_policy type_sys s'' of
- No_Type_Args => (name, [])
- | Explicit_Type_Args => (name, T_args)
- | Mangled_Type_Args => (mangled_const_name T_args name, [])
- end)
- |> (fn (name, T_args) => CombConst (name, T, T_args))
+ let
+ val level = level_of_type_sys type_sys
+ val (T, T_args) =
+ (* Aggressively merge most "hAPPs" if the type system is unsound
+ anyway, by distinguishing overloads only on the homogenized
+ result type. *)
+ if s = const_prefix ^ explicit_app_base andalso
+ not (is_type_sys_virtually_sound type_sys) then
+ T_args |> map (homogenized_type ctxt nonmono_Ts level)
+ |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
+ (T --> T, tl Ts)
+ end)
+ else
+ (T, T_args)
+ in
+ (case strip_prefix_and_unascii const_prefix s of
+ NONE => (name, T_args)
+ | SOME s'' =>
+ let val s'' = invert_const s'' in
+ case type_arg_policy type_sys s'' of
+ No_Type_Args => (name, [])
+ | Explicit_Type_Args => (name, T_args)
+ | Mangled_Type_Args => (mangled_const_name T_args name, [])
+ end)
+ |> (fn (name, T_args) => CombConst (name, T, T_args))
+ end
| aux tm = tm
in aux end
-fun repair_combterm type_sys sym_tab =
+fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
introduce_explicit_apps_in_combterm sym_tab
#> introduce_predicators_in_combterm sym_tab
- #> impose_type_arg_policy_in_combterm type_sys
-fun repair_fact type_sys sym_tab =
- update_combformula (formula_map (repair_combterm type_sys sym_tab))
+ #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
+ update_combformula (formula_map
+ (repair_combterm ctxt nonmono_Ts type_sys sym_tab))
(** Helper facts **)
@@ -652,55 +783,17 @@
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
- considered dangerous because their "exhaust" properties can easily lead to
- unsound ATP proofs. The checks below are an (unsound) approximation of
- finiteness. *)
-
-fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true
- | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) =
- is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us
- | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false
-and is_type_finite ctxt (Type (s, Ts)) =
- is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts
- | is_type_finite _ _ = false
-and is_type_constr_finite ctxt s =
- let val thy = Proof_Context.theory_of ctxt in
- case Datatype_Data.get_info thy s of
- SOME {descr, ...} =>
- forall (fn (_, (_, _, constrs)) =>
- forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr
- | NONE =>
- case Typedef.get_info ctxt s of
- ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type
- | [] => true
- end
-
-fun should_encode_type _ All_Types _ = true
- | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T
- | should_encode_type _ Nonmonotonic_Types _ =
- error "Monotonicity inference not implemented yet."
- | should_encode_type _ _ _ = false
-
-fun should_predicate_on_type ctxt (Preds (_, level)) T =
- should_encode_type ctxt level T
- | should_predicate_on_type _ _ _ = false
-
-fun should_tag_with_type ctxt (Tags (_, level)) T =
- should_encode_type ctxt level T
- | should_tag_with_type _ _ _ = false
-
-fun type_pred_combatom type_sys T tm =
+fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
tm)
- |> impose_type_arg_policy_in_combterm type_sys
+ |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
|> AAtom
-fun formula_from_combformula ctxt type_sys =
+fun formula_from_combformula ctxt nonmono_Ts type_sys =
let
fun tag_with_type type_sys T tm =
CombConst (`make_fixed_const type_tag_name, T --> T, [T])
- |> impose_type_arg_policy_in_combterm type_sys
+ |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
|> do_term true
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
and do_term top_level u =
@@ -715,16 +808,20 @@
map (do_term false) args)
val T = combtyp_of u
in
- t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then
+ t |> (if not top_level andalso
+ should_tag_with_type ctxt nonmono_Ts type_sys T then
tag_with_type type_sys T
else
I)
end
val do_bound_type =
- if type_sys = Many_Typed then SOME o mangled_type_name else K NONE
+ case type_sys of
+ Simple level =>
+ SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
+ | _ => K NONE
fun do_out_of_bound_type (s, T) =
- if should_predicate_on_type ctxt type_sys T then
- type_pred_combatom type_sys T (CombVar (s, T))
+ if should_predicate_on_type ctxt nonmono_Ts type_sys T then
+ type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T))
|> do_formula |> SOME
else
NONE
@@ -740,11 +837,11 @@
| do_formula (AAtom tm) = AAtom (do_term true tm)
in do_formula end
-fun formula_for_fact ctxt type_sys
+fun formula_for_fact ctxt nonmono_Ts type_sys
({combformula, atomic_types, ...} : translated_formula) =
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
(atp_type_literals_for_types type_sys Axiom atomic_types))
- (formula_from_combformula ctxt type_sys
+ (formula_from_combformula ctxt nonmono_Ts type_sys
(close_combformula_universally combformula))
|> close_formula_universally
@@ -753,13 +850,12 @@
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
-fun formula_line_for_fact ctxt prefix type_sys
+fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
(j, formula as {name, locality, kind, ...}) =
- Formula (prefix ^
- (if polymorphism_of_type_sys type_sys = Polymorphic then ""
- else string_of_int j ^ "_") ^
+ Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
+ else string_of_int j ^ "_") ^
ascii_of name,
- kind, formula_for_fact ctxt type_sys formula, NONE,
+ kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
if generate_useful_info then
case locality of
Intro => useful_isabelle_info "intro"
@@ -792,10 +888,10 @@
(fo_literal_from_arity_literal conclLit))
|> close_formula_universally, NONE, NONE)
-fun formula_line_for_conjecture ctxt type_sys
+fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
({name, kind, combformula, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_combformula ctxt type_sys
+ formula_from_combformula ctxt nonmono_Ts type_sys
(close_combformula_universally combformula)
|> close_formula_universally, NONE, NONE)
@@ -814,52 +910,74 @@
(** Symbol declarations **)
+fun insert_type get_T x xs =
+ let val T = get_T x in
+ if exists (curry Type.raw_instance T o get_T) xs then xs
+ else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
+ end
+
fun should_declare_sym type_sys pred_sym s =
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
not (String.isPrefix "$" s) andalso
- (type_sys = Many_Typed orelse not pred_sym)
+ ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
-fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
+fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
let
- fun declare_sym (decl as (_, _, T, _, _)) decls =
- case type_sys of
- Preds (Polymorphic, All_Types) =>
- if exists (curry Type.raw_instance T o #3) decls then
- decls
- else
- decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls
- | _ => insert (op =) decl decls
- fun do_term tm =
+ fun add_combterm in_conj tm =
let val (head, args) = strip_combterm_comb tm in
(case head of
CombConst ((s, s'), T, T_args) =>
let val pred_sym = is_pred_sym repaired_sym_tab s in
if should_declare_sym type_sys pred_sym s then
Symtab.map_default (s, [])
- (declare_sym (s', T_args, T, pred_sym, length args))
+ (insert_type #3 (s', T_args, T, pred_sym, length args,
+ in_conj))
else
I
end
| _ => I)
- #> fold do_term args
+ #> fold (add_combterm in_conj) args
end
- in do_term end
-fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
- fact_lift (formula_fold
- (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
-fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
- Symtab.empty |> is_type_sys_fairly_sound type_sys
- ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
- facts
+ fun add_fact in_conj =
+ fact_lift (formula_fold true (K (add_combterm in_conj)))
+ in
+ Symtab.empty
+ |> is_type_sys_fairly_sound type_sys
+ ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
+ end
+
+fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+ String.isPrefix bound_var_prefix s
+ | is_var_or_bound_var (CombVar _) = true
+ | is_var_or_bound_var _ = false
+
+(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
+ out with monotonicity" paper presented at CADE 2011. *)
+fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
+ | add_combterm_nonmonotonic_types ctxt _
+ (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
+ tm2)) =
+ (exists is_var_or_bound_var [tm1, tm2] andalso
+ not (is_type_surely_infinite ctxt T)) ? insert_type I T
+ | add_combterm_nonmonotonic_types _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
+ : translated_formula) =
+ formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
+ combformula
+fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
+ level_of_type_sys type_sys = Nonmonotonic_Types
+ (* in case helper "True_or_False" is included (FIXME) *)
+ ? (insert_type I @{typ bool}
+ #> fold (add_fact_nonmonotonic_types ctxt) facts)
fun n_ary_strip_type 0 T = ([], T)
| n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
n_ary_strip_type (n - 1) ran_T |>> cons dom_T
| n_ary_strip_type _ _ = raise Fail "unexpected non-function"
-fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd
+fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd
-fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) =
+fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
let val (arg_Ts, res_T) = n_ary_strip_type ary T in
Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
@@ -867,7 +985,8 @@
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
-fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
+fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
+ (s', T_args, T, _, ary, in_conj) =
let
val (arg_Ts, res_T) = n_ary_strip_type ary T
val bound_names =
@@ -879,20 +998,21 @@
else NONE)
in
Formula (sym_decl_prefix ^ s ^
- (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
+ (if n > 1 then "_" ^ string_of_int j else ""),
+ if in_conj then Hypothesis else Axiom,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bound_tms
- |> type_pred_combatom type_sys res_T
+ |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
|> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt type_sys
+ |> formula_from_combformula ctxt nonmono_Ts type_sys
|> close_formula_universally,
NONE, NONE)
end
-fun problem_lines_for_sym_decls ctxt type_sys (s, decls) =
- if type_sys = Many_Typed then
- map (decl_line_for_sym_decl s) decls
- else
+fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
+ case type_sys of
+ Simple _ => map (decl_line_for_sym s) decls
+ | _ =>
let
val decls =
case decls of
@@ -907,15 +1027,16 @@
| _ => decls
val n = length decls
val decls =
- decls |> filter (should_predicate_on_type ctxt type_sys
+ decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
o result_type_of_decl)
in
- map2 (formula_line_for_sym_decl ctxt type_sys n s)
+ map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
(0 upto length decls - 1) decls
end
-fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab =
- Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys)
+fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
+ Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
+ type_sys)
sym_decl_tab []
fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
@@ -954,40 +1075,43 @@
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt type_sys hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
- val (conjs, facts) =
- (conjs, facts) |> pairself (map (repair_fact type_sys sym_tab))
+ val nonmono_Ts =
+ [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
+ val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
+ val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
+ val helpers =
+ repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
val sym_decl_lines =
- conjs @ facts
+ (conjs, facts) (* FIXME: what if "True_or_False" is among helpers? *)
|> sym_decl_table_for_facts type_sys repaired_sym_tab
- |> problem_lines_for_sym_decl_table ctxt type_sys
- val helpers =
- helper_facts_for_sym_table ctxt type_sys repaired_sym_tab
- |> map (repair_fact type_sys sym_tab)
+ |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
[(sym_declsN, sym_decl_lines),
- (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys)
+ (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
- (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
+ (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
+ type_sys)
(0 upto length helpers - 1 ~~ helpers)
|> (case type_sys of
Tags (Polymorphic, level) =>
- member (op =) [Finite_Types, Nonmonotonic_Types] level
+ is_type_level_partial level
? cons (ti_ti_helper_fact ())
| _ => I)),
- (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
+ (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
+ conjs),
(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
val problem =
problem
- |> (if type_sys = Many_Typed then
+ |> (case type_sys of
+ Simple _ =>
cons (type_declsN,
map decl_line_for_tff_type (tff_types_in_problem problem))
- else
- I)
+ | _ => I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
in
@@ -1009,7 +1133,7 @@
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
- formula_fold (add_term_weights weight) phi
+ formula_fold true (K (add_term_weights weight)) phi
| add_problem_line_weights _ _ = I
fun add_conjectures_weights [] = I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 05 15:01:32 2011 +0200
@@ -36,7 +36,7 @@
only : bool}
val trace : bool Config.T
- val is_global_locality : locality -> bool
+ val is_locality_global : locality -> bool
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
@@ -70,10 +70,10 @@
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
(* (quasi-)underapproximation of the truth *)
-fun is_global_locality Local = false
- | is_global_locality Assum = false
- | is_global_locality Chained = false
- | is_global_locality _ = true
+fun is_locality_global Local = false
+ | is_locality_global Assum = false
+ | is_locality_global Chained = false
+ | is_locality_global _ = true
type relevance_fudge =
{allow_ext : bool,
@@ -528,7 +528,7 @@
else
tab
-fun add_arities is_built_in_const th =
+fun consider_arities is_built_in_const th =
let
fun aux _ _ NONE = NONE
| aux t args (SOME tab) =
@@ -543,8 +543,9 @@
| _ => SOME tab
in aux (prop_of th) [] end
-fun needs_ext is_built_in_const facts =
- fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
+(* FIXME: This is currently only useful for polymorphic type systems. *)
+fun could_benefit_from_ext is_built_in_const facts =
+ fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
|> is_none
fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
@@ -640,7 +641,7 @@
|> iter 0 max_relevant threshold0 goal_const_tab []
|> not (null add_ths) ? add_facts add_ths
|> (fn accepts =>
- accepts |> needs_ext is_built_in_const accepts
+ accepts |> could_benefit_from_ext is_built_in_const accepts
? add_facts @{thms ext})
|> tap (fn accepts => trace_msg ctxt (fn () =>
"Total relevant: " ^ string_of_int (length accepts)))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 05 15:01:32 2011 +0200
@@ -167,13 +167,19 @@
prover :: avoid_too_many_local_threads ctxt n provers
end
+(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
+ correctly. *)
+fun implode_param_value [s, "?"] = s ^ "?"
+ | implode_param_value [s, "!"] = s ^ "!"
+ | implode_param_value ss = space_implode " " ss
+
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
[spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
- |> space_implode " "
+ |> implode_param_value
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params ctxt =
@@ -197,7 +203,7 @@
let
val override_params = map unalias_raw_param override_params
val raw_params = rev override_params @ rev default_params
- val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+ val lookup = Option.map implode_param_value o AList.lookup (op =) raw_params
val lookup_string = the_default "" o lookup
fun general_lookup_bool option default_value name =
case lookup name of
@@ -274,7 +280,7 @@
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
- key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
+ key ^ (case implode_param_value values of "" => "" | value => " = " ^ value)
fun minimize_command override_params i prover_name fact_names =
sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
@@ -317,7 +323,7 @@
Toplevel.keep (hammer_away params subcommand opt_i relevance_override
o Toplevel.proof_of)
-fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param_value value
fun sledgehammer_params_trans params =
Toplevel.theory
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 05 15:01:32 2011 +0200
@@ -346,14 +346,14 @@
val atp_important_message_keep_quotient = 10
val fallback_best_type_systems =
- [Preds (Polymorphic, Const_Arg_Types), Many_Typed]
+ [Preds (Polymorphic, Const_Arg_Types), Simple All_Types]
-fun adjust_dumb_type_sys formats Many_Typed =
- if member (op =) formats Tff then (Tff, Many_Typed)
- else (Fof, Preds (Mangled_Monomorphic, All_Types))
+fun adjust_dumb_type_sys formats (Simple level) =
+ if member (op =) formats Tff then (Tff, Simple level)
+ else (Fof, Preds (Mangled_Monomorphic, level))
| adjust_dumb_type_sys formats type_sys =
if member (op =) formats Fof then (Fof, type_sys)
- else (Tff, Many_Typed)
+ else (Tff, Simple (level_of_type_sys type_sys))
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys
| determine_format_and_type_sys best_type_systems formats
@@ -461,10 +461,10 @@
* 0.001) |> seconds
val _ =
if debug then
- quote name ^ " slice " ^ string_of_int (slice + 1) ^
- " of " ^ string_of_int num_actual_slices ^ " with " ^
- string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
- " for " ^ string_from_time slice_timeout ^ "..."
+ quote name ^ " slice #" ^ string_of_int (slice + 1) ^
+ " with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for " ^
+ string_from_time slice_timeout ^ "..."
|> Output.urgent_message
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 05 15:01:32 2011 +0200
@@ -15,6 +15,12 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
+ val typ_of_dtyp :
+ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
+ -> typ
+ val varify_type : Proof.context -> typ -> typ
+ val instantiate_type : theory -> typ -> typ -> typ -> typ
+ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_term : term -> term
@@ -80,6 +86,30 @@
Keyword.is_keyword s) ? quote
end
+fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
+ the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
+ | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
+ Type (s, map (typ_of_dtyp descr typ_assoc) Us)
+ | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
+ let val (s, ds, _) = the (AList.lookup (op =) descr i) in
+ Type (s, map (typ_of_dtyp descr typ_assoc) ds)
+ end
+
+fun varify_type ctxt T =
+ Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
+ |> snd |> the_single |> dest_Const |> snd
+
+(* TODO: use "Term_Subst.instantiateT" instead? *)
+fun instantiate_type thy T1 T1' T2 =
+ Same.commit (Envir.subst_type_same
+ (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
+ handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
+
+fun varify_and_instantiate_type ctxt T1 T1' T2 =
+ let val thy = Proof_Context.theory_of ctxt in
+ instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
+ end
+
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of
--- a/src/HOL/Tools/record.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/record.ML Thu May 05 15:01:32 2011 +0200
@@ -1795,7 +1795,7 @@
(* code generation *)
-fun instantiate_random_record tyco vs extN Ts thy =
+fun mk_random_eq tyco vs extN Ts =
let
val size = @{term "i::code_numeral"};
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
@@ -1810,26 +1810,52 @@
(map (fn (v, T') =>
((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ in
+ (lhs, rhs)
+ end
+
+fun mk_full_exhaustive_eq tyco vs extN Ts =
+ let
+ val size = @{term "i::code_numeral"};
+ fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+ val T = Type (tyco, map TFree vs);
+ val test_function = Free ("f", termifyT T --> @{typ "term list option"});
+ val params = Name.names Name.context "x" Ts;
+ fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+ --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+ fun mk_full_exhaustive T =
+ Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
+ full_exhaustiveT T)
+ val lhs = mk_full_exhaustive T $ test_function $ size;
+ val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
+ val rhs = fold_rev (fn (v, T) => fn cont =>
+ mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
+ in
+ (lhs, rhs)
+ end
+
+fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
+ let
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
in
thy
- |> Class.instantiation ([tyco], vs, @{sort random})
+ |> Class.instantiation ([tyco], vs, sort)
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_random_record ext_tyco vs extN Ts thy =
+ end
+
+fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
let
val algebra = Sign.classes_of thy;
- val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
+ val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
in
if has_inst then thy
else
- (case Quickcheck_Common.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
+ (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
SOME constrain =>
- instantiate_random_record ext_tyco (map constrain vs) extN
+ instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
| NONE => thy)
end;
@@ -1851,6 +1877,8 @@
|> Thm.instantiate
([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
|> AxClass.unoverload thy;
+ val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
+ val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
in
thy
|> Code.add_datatype [ext]
@@ -1866,6 +1894,7 @@
thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
|> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
|> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
+ |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
end;
--- a/src/HOL/Tools/refute.ML Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/Tools/refute.ML Thu May 05 15:01:32 2011 +0200
@@ -71,7 +71,6 @@
val is_IDT_recursor : theory -> string * typ -> bool
val is_const_of_class: theory -> string * typ -> bool
val string_of_typ : typ -> string
- val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
end;
structure Refute : REFUTE =
@@ -394,17 +393,7 @@
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
-fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) =
- (* replace a 'DtTFree' variable by the associated type *)
- the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
- | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) =
- Type (s, map (typ_of_dtyp descr typ_assoc) ds)
- | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
- let
- val (s, ds, _) = the (AList.lookup (op =) descr i)
- in
- Type (s, map (typ_of_dtyp descr typ_assoc) ds)
- end;
+val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
(* ------------------------------------------------------------------------- *)
(* close_form: universal closure over schematic variables in 't' *)
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed May 04 15:37:39 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Thu May 05 15:01:32 2011 +0200
@@ -294,6 +294,29 @@
quickcheck[random, size = 10]
oops
+subsection {* Examples with Records *}
+
+record point =
+ xpos :: nat
+ ypos :: nat
+
+lemma
+ "xpos r = xpos r' ==> r = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
+datatype colour = Red | Green | Blue
+
+record cpoint = point +
+ colour :: colour
+
+lemma
+ "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
subsection {* Examples with locales *}
locale Truth