# HG changeset patch # User wenzelm # Date 1304600492 -7200 # Node ID 6ab174bfefe296b4f674084ad5e97a8d5fca119f # Parent d7c127478ee14e4c70620dde4e6365174d81e49e# Parent 8724f20bf69ca0539834f6ad3186dd7ae44fbed9 merged; diff -r 8724f20bf69c -r 6ab174bfefe2 doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Main.thy --- 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 {* diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Metis_Examples/HO_Reas.thy --- 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 "\ 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 \ 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 \ 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 \ P False \ 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 (\ a) \ \ 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) \ 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 (\ (id (\ a))) \ 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 \ b) \ 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 \ b) \ 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 \ id b \ id (a \ 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 \ id (a \ 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 \ id (a \ 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) \ id (\ b) \ id (\ (a \ 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) \ id (a \ 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 \ b) \ id (\ a \ 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) diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Record.thy --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/ATP/atp_systems.ML --- 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 *) diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 () => diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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 **) diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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))) diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 () diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/record.ML --- 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; diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/Tools/refute.ML --- 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' *) diff -r 8724f20bf69c -r 6ab174bfefe2 src/HOL/ex/Quickcheck_Examples.thy --- 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