--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 25 14:25:19 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 25 14:26:38 2011 -0700
@@ -896,7 +896,7 @@
arguments, to resolve overloading.
\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
+tagged with its type using a function $\mathit{type\/}(\tau, t)$.
\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
Like for \textit{poly\_guards} constants are annotated with their types to
@@ -905,8 +905,8 @@
\item[$\bullet$]
\textbf{%
-\textit{mono\_guards}, \textit{mono\_tags} (sound);
-\textit{mono\_args} (unsound):} \\
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
+\textit{raw\_mono\_args} (unsound):} \\
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
respectively, but the problem is additionally monomorphized, meaning that type
variables are instantiated with heuristically chosen ground types.
@@ -915,33 +915,34 @@
\item[$\bullet$]
\textbf{%
-\textit{mangled\_guards},
-\textit{mangled\_tags} (sound); \\
-\textit{mangled\_args} (unsound):} \\
+\textit{mono\_guards}, \textit{mono\_tags} (sound);
+\textit{mono\_args} (unsound):} \\
Similar to
-\textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_args},
-respectively but types are mangled in constant names instead of being supplied
-as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
-becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
-$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
-$\mathit{type\_info\_}\tau(t)$.
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
+\textit{raw\_mono\_args}, respectively but types are mangled in constant names
+instead of being supplied as ground term arguments. The binary predicate
+$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
+$\mathit{has\_type\_}\tau(t)$, and the binary function
+$\mathit{type\/}(\tau, t)$ becomes a unary function
+$\mathit{type\_}\tau(t)$.
\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
types if the prover supports the TFF or THF syntax; otherwise, fall back on
-\textit{mangled\_guards}. The problem is monomorphized.
+\textit{mono\_guards}. The problem is monomorphized.
\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
higher-order types if the prover supports the THF syntax; otherwise, fall back
-on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
+on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
monomorphized.
\item[$\bullet$]
\textbf{%
-\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
-\textit{mangled\_guards}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
+\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
+\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
+\textit{simple}? (quasi-sound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, and \textit{simple} are fully
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, and \textit{simple} are fully
typed and sound. For each of these, Sledgehammer also provides a lighter,
virtually sound variant identified by a question mark (`{?}')\ that detects and
erases monotonic types, notably infinite types. (For \textit{simple}, the types
@@ -952,12 +953,12 @@
\item[$\bullet$]
\textbf{%
-\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mangled\_guards}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
-(mildly unsound):} \\
+\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
+\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
+\textit{simple\_higher}! (mildly unsound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
-\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
+\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
+\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
a mildly unsound (but very efficient) variant identified by an exclamation mark
(`{!}') that detects and erases erases all types except those that are clearly
finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
@@ -973,7 +974,7 @@
available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
nonuniform variants are generally more efficient and are the default; the
uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
-\textit{mangled\_guards\_uniform}{?}).
+\textit{mono\_guards\_uniform}{?}).
For SMT solvers, the type encoding is always \textit{simple}, irrespective of
the value of this option.
--- a/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:26:38 2011 -0700
@@ -62,10 +62,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
@@ -74,10 +74,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
@@ -86,10 +86,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
@@ -98,10 +98,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
@@ -110,10 +110,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -123,10 +123,10 @@
sledgehammer [type_enc = poly_tags, expect = some] ()
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] ()
-sledgehammer [type_enc = mangled_tags?, expect = some] ()
-sledgehammer [type_enc = mangled_tags, expect = some] ()
-sledgehammer [type_enc = mangled_guards?, expect = some] ()
-sledgehammer [type_enc = mangled_guards, expect = some] ()
+sledgehammer [type_enc = mono_tags?, expect = some] ()
+sledgehammer [type_enc = mono_tags, expect = some] ()
+sledgehammer [type_enc = mono_guards?, expect = some] ()
+sledgehammer [type_enc = mono_guards, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
@@ -135,10 +135,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
@@ -147,10 +147,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
@@ -159,10 +159,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
@@ -171,10 +171,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
@@ -183,10 +183,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
@@ -195,10 +195,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
@@ -207,10 +207,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
@@ -219,10 +219,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
@@ -231,10 +231,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
@@ -243,10 +243,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
@@ -255,10 +255,10 @@
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:26:38 2011 -0700
@@ -29,42 +29,42 @@
"poly_tags",
"poly_tags_uniform",
"poly_args",
+ "raw_mono_guards",
+ "raw_mono_guards_uniform",
+ "raw_mono_tags",
+ "raw_mono_tags_uniform",
+ "raw_mono_args",
"mono_guards",
"mono_guards_uniform",
"mono_tags",
"mono_tags_uniform",
"mono_args",
- "mangled_guards",
- "mangled_guards_uniform",
- "mangled_tags",
- "mangled_tags_uniform",
- "mangled_args",
"simple",
"poly_guards?",
"poly_guards_uniform?",
"poly_tags?",
"poly_tags_uniform?",
+ "raw_mono_guards?",
+ "raw_mono_guards_uniform?",
+ "raw_mono_tags?",
+ "raw_mono_tags_uniform?",
"mono_guards?",
"mono_guards_uniform?",
"mono_tags?",
"mono_tags_uniform?",
- "mangled_guards?",
- "mangled_guards_uniform?",
- "mangled_tags?",
- "mangled_tags_uniform?",
"simple?",
"poly_guards!",
"poly_guards_uniform!",
"poly_tags!",
"poly_tags_uniform!",
+ "raw_mono_guards!",
+ "raw_mono_guards_uniform!",
+ "raw_mono_tags!",
+ "raw_mono_tags_uniform!",
"mono_guards!",
"mono_guards_uniform!",
"mono_tags!",
"mono_tags_uniform!",
- "mangled_guards!",
- "mangled_guards_uniform!",
- "mangled_tags!",
- "mangled_tags_uniform!",
"simple!"]
fun metis_exhaust_tac ctxt ths =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 25 14:26:38 2011 -0700
@@ -484,9 +484,8 @@
case result of
SH_OK (time_isa, time_prover, names) =>
let
- fun get_thms (_, ATP_Translate.Chained) = NONE
- | get_thms (name, loc) =
- SOME ((name, loc), thms_of_name (Proof.context_of st) name)
+ fun get_thms (name, loc) =
+ SOME ((name, loc), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
if trivial then () else change_data id inc_sh_nontriv_success;
--- a/src/HOL/SMT.thy Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/SMT.thy Thu Aug 25 14:26:38 2011 -0700
@@ -329,9 +329,24 @@
if_True if_False not_not
lemma [z3_rule]:
+ "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
+ "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
+ "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
+ "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
+ "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
+ "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
+ by auto
+
+lemma [z3_rule]:
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
"(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+ "(True \<longrightarrow> P) = P"
+ "(P \<longrightarrow> True) = True"
+ "(False \<longrightarrow> P) = True"
+ "(P \<longrightarrow> P) = True"
by auto
lemma [z3_rule]:
@@ -339,8 +354,18 @@
by auto
lemma [z3_rule]:
+ "(\<not>True) = False"
+ "(\<not>False) = True"
+ "(x = x) = True"
+ "(P = True) = P"
+ "(True = P) = P"
+ "(P = False) = (\<not>P)"
+ "(False = P) = (\<not>P)"
"((\<not>P) = P) = False"
"(P = (\<not>P)) = False"
+ "((\<not>P) = (\<not>Q)) = (P = Q)"
+ "\<not>(P = (\<not>Q)) = (P = Q)"
+ "\<not>((\<not>P) = Q) = (P = Q)"
"(P \<noteq> Q) = (Q = (\<not>P))"
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
"(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
@@ -351,11 +376,36 @@
"(if \<not>P then \<not>P else P) = True"
"(if P then True else False) = P"
"(if P then False else True) = (\<not>P)"
+ "(if P then Q else True) = ((\<not>P) \<or> Q)"
+ "(if P then Q else True) = (Q \<or> (\<not>P))"
+ "(if P then Q else \<not>Q) = (P = Q)"
+ "(if P then Q else \<not>Q) = (Q = P)"
+ "(if P then \<not>Q else Q) = (P = (\<not>Q))"
+ "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
"(if \<not>P then x else y) = (if P then y else x)"
+ "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
+ "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
+ "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
+ "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
+ "(if P then x else if P then y else z) = (if P then x else z)"
+ "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
+ "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
+ "(if P then x = y else x = z) = (x = (if P then y else z))"
+ "(if P then x = y else y = z) = (y = (if P then x else z))"
+ "(if P then x = y else z = y) = (y = (if P then x else z))"
"f (if P then x else y) = (if P then f x else f y)"
by auto
lemma [z3_rule]:
+ "0 + (x::int) = x"
+ "x + 0 = x"
+ "x + x = 2 * x"
+ "0 * x = 0"
+ "1 * x = x"
+ "x + y = y + x"
+ by auto
+
+lemma [z3_rule]: (* for def-axiom *)
"P = Q \<or> P \<or> Q"
"P = Q \<or> \<not>P \<or> \<not>Q"
"(\<not>P) = Q \<or> \<not>P \<or> Q"
@@ -370,14 +420,18 @@
"P \<or> Q \<or> (\<not>P) \<noteq> Q"
"P \<or> \<not>Q \<or> P \<noteq> Q"
"\<not>P \<or> Q \<or> P \<noteq> Q"
- by auto
-
-lemma [z3_rule]:
- "0 + (x::int) = x"
- "x + 0 = x"
- "0 * x = 0"
- "1 * x = x"
- "x + y = y + x"
+ "P \<or> y = (if P then x else y)"
+ "P \<or> (if P then x else y) = y"
+ "\<not>P \<or> x = (if P then x else y)"
+ "\<not>P \<or> (if P then x else y) = x"
+ "P \<or> R \<or> \<not>(if P then Q else R)"
+ "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
+ "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
+ "\<not>(if P then Q else R) \<or> P \<or> R"
+ "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
+ "(if P then Q else R) \<or> P \<or> \<not>R"
+ "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
+ "(if P then Q else \<not>R) \<or> P \<or> R"
by auto
--- a/src/HOL/Set.thy Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Set.thy Thu Aug 25 14:26:38 2011 -0700
@@ -1378,6 +1378,9 @@
lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
by (fact compl_eq_compl_iff)
+lemma Compl_insert: "- insert x A = (-A) - {x}"
+ by blast
+
text {* \medskip Bounded quantifiers.
The following are not added to the default simpset because
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Aug 25 14:26:38 2011 -0700
@@ -50,6 +50,7 @@
val tptp_ho_forall : string
val tptp_exists : string
val tptp_ho_exists : string
+ val tptp_choice : string
val tptp_not : string
val tptp_and : string
val tptp_or : string
@@ -147,6 +148,7 @@
val tptp_ho_forall = "!!"
val tptp_exists = "?"
val tptp_ho_exists = "??"
+val tptp_choice = "@+"
val tptp_not = "~"
val tptp_and = "&"
val tptp_or = "|"
@@ -264,13 +266,21 @@
space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
|> is_format_thf format ? enclose "(" ")"
else
- (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
- (true, [AAbs ((s', ty), tm)]) =>
+ (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
+ s = tptp_choice andalso format = THF With_Choice, ts) of
+ (true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
string_for_formula format
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
+ | (_, true, [AAbs ((s', ty), tm)]) =>
+ (*There is code in ATP_Translate to ensure that Eps is always applied
+ to an abstraction*)
+ tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
+ string_for_term format tm ^ ""
+ |> enclose "(" ")"
+
| _ =>
let val ss = map (string_for_term format) ts in
if is_format_thf format then
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 14:26:38 2011 -0700
@@ -216,11 +216,11 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
- (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
+ [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
+ (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
+ (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
+ [(1.0, (true, (500, FOF, "mono_tags?", method)))]
end}
val e = (eN, e_config)
@@ -293,9 +293,9 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+ [(0.333, (false, (150, FOF, "mono_tags", sosN))),
(0.333, (false, (300, FOF, "poly_tags?", sosN))),
- (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
+ (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -324,7 +324,6 @@
[(GaveUp, "UNPROVABLE"),
(GaveUp, "CANNOT PROVE"),
(GaveUp, "SZS status GaveUp"),
- (ProofIncomplete, "predicate_definition_introduction,[]"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
@@ -336,8 +335,8 @@
(* FUDGE *)
(if is_old_vampire_version () then
[(0.333, (false, (150, FOF, "poly_guards", sosN))),
- (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
- (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+ (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
+ (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
else
[(0.333, (false, (150, TFF, "poly_guards", sosN))),
(0.334, (true, (50, TFF, "simple", no_sosN))),
@@ -360,14 +359,15 @@
[(GaveUp, "SZS status Satisfiable"),
(GaveUp, "SZS status CounterSatisfiable"),
(GaveUp, "SZS status GaveUp"),
+ (GaveUp, "SZS status Unknown"),
(ProofMissing, "SZS status Unsatisfiable"),
(ProofMissing, "SZS status Theorem")],
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, TFF, "simple", ""))),
- (0.25, (false, (125, TFF, "simple", ""))),
+ K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
+ (0.25, (false, (125, FOF, "mono_guards?", ""))),
(0.125, (false, (62, TFF, "simple", ""))),
(0.125, (false, (31, TFF, "simple", "")))]}
@@ -449,7 +449,7 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mangled_tags?") (* FUDGE *))
+ (K (750, FOF, "mono_tags?") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
(K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
@@ -462,7 +462,7 @@
remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
+ Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -476,7 +476,7 @@
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis Hypothesis
- (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
+ (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 14:26:38 2011 -0700
@@ -20,7 +20,7 @@
Chained
datatype order = First_Order | Higher_Order
- datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
@@ -35,6 +35,8 @@
Guards of polymorphism * type_level * type_uniformity |
Tags of polymorphism * type_level * type_uniformity
+ val type_tag_idempotence : bool Config.T
+ val type_tag_arguments : bool Config.T
val no_lambdasN : string
val concealedN : string
val liftingN : string
@@ -114,6 +116,11 @@
type name = string * string
+val type_tag_idempotence =
+ Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
+val type_tag_arguments =
+ Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
+
val no_lambdasN = "no_lambdas"
val concealedN = "concealed"
val liftingN = "lifting"
@@ -141,6 +148,7 @@
val tfree_prefix = "t_"
val const_prefix = "c_"
val type_const_prefix = "tc_"
+val simple_type_prefix = "s_"
val class_prefix = "cl_"
val polymorphic_free_prefix = "poly_free"
@@ -165,11 +173,10 @@
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
-val predicator_name = "p"
-val app_op_name = "a"
-val type_guard_name = "g"
-val type_tag_name = "t"
-val simple_type_prefix = "ty_"
+val predicator_name = "pp"
+val app_op_name = "aa"
+val type_guard_name = "gg"
+val type_tag_name = "tt"
val prefixed_predicator_name = const_prefix ^ predicator_name
val prefixed_app_op_name = const_prefix ^ app_op_name
@@ -308,8 +315,10 @@
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
(* "HOL.eq" is mapped to the ATP's equality. *)
-fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
- | make_fixed_const c = const_prefix ^ lookup_const c
+fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
+ | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
+ tptp_choice
+ | make_fixed_const _ c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
@@ -483,38 +492,38 @@
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
Also accumulates sort infomation. *)
-fun iterm_from_term thy bs (P $ Q) =
+fun iterm_from_term thy format bs (P $ Q) =
let
- val (P', P_atomics_Ts) = iterm_from_term thy bs P
- val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
+ val (P', P_atomics_Ts) = iterm_from_term thy format bs P
+ val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
- | iterm_from_term thy _ (Const (c, T)) =
- (IConst (`make_fixed_const c, T,
+ | iterm_from_term thy format _ (Const (c, T)) =
+ (IConst (`(make_fixed_const (SOME format)) c, T,
if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy),
atyps_of T)
- | iterm_from_term _ _ (Free (s, T)) =
+ | iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
if String.isPrefix polymorphic_free_prefix s then [T] else []),
atyps_of T)
- | iterm_from_term _ _ (Var (v as (s, _), T)) =
+ | iterm_from_term _ format _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val Ts = T |> strip_type |> swap |> op ::
val s' = new_skolem_const_name s (length Ts)
- in IConst (`make_fixed_const s', T, Ts) end
+ in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
else
IVar ((make_schematic_var v, s), T), atyps_of T)
- | iterm_from_term _ bs (Bound j) =
+ | iterm_from_term _ _ bs (Bound j) =
nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
- | iterm_from_term thy bs (Abs (s, T, t)) =
+ | iterm_from_term thy format bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
val name = `make_bound_var s
- val (tm, atomic_Ts) = iterm_from_term thy ((s, (name, T)) :: bs) t
+ val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
datatype locality =
@@ -522,7 +531,7 @@
Chained
datatype order = First_Order | Higher_Order
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
@@ -544,10 +553,10 @@
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
- case try (unprefix "mono_") s of
- SOME s => (SOME Monomorphic, s)
+ case try (unprefix "raw_mono_") s of
+ SOME s => (SOME Raw_Monomorphic, s)
| NONE =>
- case try (unprefix "mangled_") s of
+ case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
||> (fn s =>
@@ -882,15 +891,20 @@
| _ => IConst (name, T, [])
else
IConst (proxy_base |>> prefix const_prefix, T, T_args)
- | NONE => IConst (name, T, T_args))
+ | NONE => if s = tptp_choice then
+ (*this could be made neater by adding c_Eps as a proxy,
+ but we'd need to be able to "see" Hilbert_Choice.Eps
+ at this level in order to define fEps*)
+ tweak_ho_quant tptp_choice T args
+ else IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
| intro _ _ tm = tm
in intro true [] end
-fun iformula_from_prop thy type_enc eq_as_iff =
+fun iformula_from_prop thy format type_enc eq_as_iff =
let
fun do_term bs t atomic_types =
- iterm_from_term thy bs (Envir.eta_contract t)
+ iterm_from_term thy format bs (Envir.eta_contract t)
|>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q pos s T t' =
@@ -1041,10 +1055,10 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy type_enc eq_as_iff name loc kind t =
+fun make_formula thy format type_enc eq_as_iff name loc kind t =
let
val (iformula, atomic_types) =
- iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
+ iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
in
{name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
@@ -1052,8 +1066,8 @@
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
- loc Axiom of
+ case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
+ name loc Axiom of
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
@@ -1065,7 +1079,7 @@
fun make_conjecture thy format type_enc =
map (fn ((name, loc), (kind, t)) =>
t |> kind = Conjecture ? s_not_trueprop
- |> make_formula thy type_enc (format <> CNF) name loc kind)
+ |> make_formula thy format type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
@@ -1097,17 +1111,15 @@
| should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
(Noninf_Nonmono_Types soundness) T =
- exists (type_instance ctxt T orf type_generalization ctxt T)
- maybe_nonmono_Ts andalso
+ exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
not (exists (type_instance ctxt T) surely_infinite_Ts orelse
(not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
maybe_nonmono_Ts, ...}
Fin_Nonmono_Types T =
- exists (type_instance ctxt T orf type_generalization ctxt T)
- maybe_nonmono_Ts andalso
- (exists (type_instance ctxt T) surely_finite_Ts orelse
+ exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+ (exists (type_generalization ctxt T) surely_finite_Ts orelse
(not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
is_type_surely_finite ctxt T))
| should_encode_type _ _ _ _ = false
@@ -1245,7 +1257,7 @@
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
- (make_fixed_const @{const_name undefined},
+ (make_fixed_const NONE @{const_name undefined},
{pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
@@ -1282,7 +1294,7 @@
| NONE => false
val predicator_combconst =
- IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+ IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
fun predicator tm = IApp (predicator_combconst, tm)
fun introduce_predicators_in_iterm sym_tab tm =
@@ -1293,7 +1305,7 @@
fun list_app head args = fold (curry (IApp o swap)) args head
-val app_op = `make_fixed_const app_op_name
+val app_op = `(make_fixed_const NONE) app_op_name
fun explicit_app arg head =
let
@@ -1348,7 +1360,8 @@
| aux arity (IConst (name as (s, _), T, T_args)) =
(case strip_prefix_and_unascii const_prefix s of
NONE =>
- (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
+ (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
+ then [] else T_args)
| SOME s'' =>
let
val s'' = invert_const s''
@@ -1435,7 +1448,7 @@
|> bound_tvars type_enc atomic_Ts
|> close_formula_universally
-val type_tag = `make_fixed_const type_tag_name
+val type_tag = `(make_fixed_const NONE) type_tag_name
fun type_tag_idempotence_fact type_enc =
let
@@ -1449,7 +1462,7 @@
end
fun should_specialize_helper type_enc t =
- polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
+ polymorphism_of_type_enc type_enc <> Polymorphic andalso
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
@@ -1582,7 +1595,7 @@
(conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
end
-val type_guard = `make_fixed_const type_guard_name
+val type_guard = `(make_fixed_const NONE) type_guard_name
fun type_guard_iterm ctxt format type_enc T tm =
IApp (IConst (type_guard, T --> @{typ bool}, [T])
@@ -1792,7 +1805,7 @@
fun add_undefined_const T =
let
val (s, s') =
- `make_fixed_const @{const_name undefined}
+ `(make_fixed_const (SOME format)) @{const_name undefined}
|> (case type_arg_policy type_enc @{const_name undefined} of
Mangled_Type_Args _ => mangled_const_name format type_enc [T]
| _ => I)
@@ -1992,7 +2005,8 @@
end
in
[] |> not pred_sym ? add_formula_for_res
- |> fold add_formula_for_arg (ary - 1 downto 0)
+ |> Config.get ctxt type_tag_arguments
+ ? fold add_formula_for_arg (ary - 1 downto 0)
end
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
@@ -2054,11 +2068,12 @@
syms []
in mono_lines @ decl_lines end
-fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+ Config.get ctxt type_tag_idempotence andalso
poly <> Mangled_Monomorphic andalso
((level = All_Types andalso uniformity = Nonuniform) orelse
is_type_level_monotonicity_based level)
- | needs_type_tag_idempotence _ = false
+ | needs_type_tag_idempotence _ _ = false
fun offset_of_heading_in_problem _ [] j = j
| offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -2128,7 +2143,7 @@
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt format helper_prefix I false true mono
type_enc)
- |> (if needs_type_tag_idempotence type_enc then
+ |> (if needs_type_tag_idempotence ctxt type_enc then
cons (type_tag_idempotence_fact type_enc)
else
I)
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Aug 25 14:26:38 2011 -0700
@@ -17,6 +17,7 @@
val string_from_time : Time.time -> string
val type_instance : Proof.context -> typ -> typ -> bool
val type_generalization : Proof.context -> typ -> typ -> bool
+ val type_intersect : Proof.context -> typ -> typ -> bool
val type_aconv : Proof.context -> typ * typ -> bool
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
@@ -117,6 +118,8 @@
fun type_instance ctxt T T' =
Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
fun type_generalization ctxt T T' = type_instance ctxt T' T
+fun type_intersect ctxt T T' =
+ type_instance ctxt T T' orelse type_generalization ctxt T T'
fun type_aconv ctxt (T, T') =
type_instance ctxt T T' andalso type_instance ctxt T' T
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Aug 25 14:26:38 2011 -0700
@@ -9,14 +9,16 @@
signature METIS_RECONSTRUCT =
sig
+ type type_enc = ATP_Translate.type_enc
+
exception METIS of string * string
val hol_clause_from_metis :
- Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
- -> term
+ Proof.context -> type_enc -> int Symtab.table -> (string * term) list
+ -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val replay_one_inference :
- Proof.context -> (string * term) list -> int Symtab.table
+ Proof.context -> type_enc -> (string * term) list -> int Symtab.table
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -33,38 +35,39 @@
exception METIS of string * string
-fun atp_name_from_metis s =
- case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
+fun atp_name_from_metis type_enc s =
+ case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
SOME ((s, _), (_, swap)) => (s, swap)
| _ => (s, false)
-fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
- let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
- ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
+fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
+ let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
+ ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
end
- | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
+ | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
-fun hol_term_from_metis ctxt sym_tab =
- atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
+fun hol_term_from_metis ctxt type_enc sym_tab =
+ atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
-fun atp_literal_from_metis (pos, atom) =
- atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
- | atp_clause_from_metis lits =
- lits |> map atp_literal_from_metis |> mk_aconns AOr
+fun atp_literal_from_metis type_enc (pos, atom) =
+ atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
+ |> AAtom |> not pos ? mk_anot
+fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
+ | atp_clause_from_metis type_enc lits =
+ lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
fun reveal_old_skolems_and_infer_types ctxt old_skolems =
map (reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-fun hol_clause_from_metis ctxt sym_tab old_skolems =
+fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
Metis_Thm.clause
#> Metis_LiteralSet.toList
- #> atp_clause_from_metis
+ #> atp_clause_from_metis type_enc
#> prop_from_atp ctxt false sym_tab
#> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
-fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
- let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
+fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
+ let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -111,10 +114,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
in cterm_instantiate substs th end;
-fun assume_inference ctxt old_skolems sym_tab atom =
+fun assume_inference ctxt type_enc old_skolems sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+ (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -122,7 +125,7 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
let val thy = Proof_Context.theory_of ctxt
val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -130,7 +133,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolems_and_infer_types" below. *)
- val t = hol_term_from_metis ctxt sym_tab y
+ val t = hol_term_from_metis ctxt type_enc sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -255,7 +258,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 =
let
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
@@ -271,7 +274,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
+ singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -300,10 +303,11 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inference ctxt old_skolems sym_tab t =
+fun refl_inference ctxt type_enc old_skolems sym_tab t =
let
val thy = Proof_Context.theory_of ctxt
- val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
+ val i_t =
+ singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -313,11 +317,11 @@
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
-fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atom
val [i_atom, i_tm] =
- hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
+ hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -336,7 +340,8 @@
#> the #> unmangled_const_name))
in
if s = metis_predicator orelse s = predicator_name orelse
- s = metis_type_tag orelse s = type_tag_name then
+ s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
+ orelse s = type_tag_name then
path_finder tm ps (nth ts p)
else if s = metis_app_op orelse s = app_op_name then
let
@@ -377,21 +382,22 @@
val factor = Seq.hd o distinct_subgoals_tac
-fun one_step ctxt old_skolems sym_tab th_pairs p =
+fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
| (_, Metis_Proof.Assume f_atom) =>
- assume_inference ctxt old_skolems sym_tab f_atom
+ assume_inference ctxt type_enc old_skolems sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
+ inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
|> factor
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
- resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
+ resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
+ f_th2
|> factor
| (_, Metis_Proof.Refl f_tm) =>
- refl_inference ctxt old_skolems sym_tab f_tm
+ refl_inference ctxt type_enc old_skolems sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
+ equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -443,7 +449,8 @@
end
end
-fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
+fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
+ th_pairs =
if not (null th_pairs) andalso
prop_of (snd (hd th_pairs)) aconv @{prop False} then
(* Isabelle sometimes identifies literals (premises) that are distinct in
@@ -458,7 +465,7 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
+ val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
--- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:26:38 2011 -0700
@@ -39,7 +39,7 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_enc = "mangled_tags_uniform"
+val really_full_type_enc = "mono_tags_uniform"
val full_type_enc = "poly_guards_uniform_query"
val partial_type_enc = "poly_args"
val no_type_enc = "erased"
@@ -74,9 +74,9 @@
"t => t'", where "t" and "t'" are the same term modulo type tags.
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt sym_tab old_skolems mth of
+ case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -91,14 +91,7 @@
fun clause_params type_enc =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals =
- (* Type axioms seem to benefit from the positive literal order, but for
- compatibility we keep the unsigned order for Metis's default
- "partial_types" mode. *)
- if is_type_enc_fairly_sound type_enc then
- Metis_Clause.PositiveLiteralOrder
- else
- Metis_Clause.UnsignedLiteralOrder,
+ orderLiterals = Metis_Clause.UnsignedLiteralOrder,
orderTerms = true}
fun active_params type_enc =
{clause = clause_params type_enc,
@@ -133,7 +126,7 @@
val (sym_tab, axioms, old_skolems) =
prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
+ reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
@@ -155,7 +148,7 @@
val proof = Metis_Proof.proof mth
val result =
axioms
- |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
+ |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
val used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
--- a/src/HOL/Tools/Metis/metis_translate.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Aug 25 14:26:38 2011 -0700
@@ -18,13 +18,14 @@
val metis_equal : string
val metis_predicator : string
val metis_app_op : string
- val metis_type_tag : string
+ val metis_systematic_type_tag : string
+ val metis_ad_hoc_type_tag : string
val metis_generated_var_prefix : string
val trace : bool Config.T
val verbose : bool Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose_warning : Proof.context -> string -> unit
- val metis_name_table : ((string * int) * (string * bool)) list
+ val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
Proof.context -> type_enc -> thm list -> thm list
@@ -39,8 +40,10 @@
val metis_equal = "="
val metis_predicator = "{}"
-val metis_app_op = "."
-val metis_type_tag = ":"
+val metis_app_op = Metis_Name.toString Metis_Term.appName
+val metis_systematic_type_tag =
+ Metis_Name.toString Metis_Term.hasTypeFunctionName
+val metis_ad_hoc_type_tag = "**"
val metis_generated_var_prefix = "_"
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
@@ -51,11 +54,13 @@
if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
val metis_name_table =
- [((tptp_equal, 2), (metis_equal, false)),
- ((tptp_old_equal, 2), (metis_equal, false)),
- ((prefixed_predicator_name, 1), (metis_predicator, false)),
- ((prefixed_app_op_name, 2), (metis_app_op, false)),
- ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
+ [((tptp_equal, 2), (K metis_equal, false)),
+ ((tptp_old_equal, 2), (K metis_equal, false)),
+ ((prefixed_predicator_name, 1), (K metis_predicator, false)),
+ ((prefixed_app_op_name, 2), (K metis_app_op, false)),
+ ((prefixed_type_tag_name, 2),
+ (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
+ | _ => metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^
@@ -114,32 +119,34 @@
val prepare_helper =
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
-fun metis_term_from_atp (ATerm (s, tms)) =
+fun metis_term_from_atp type_enc (ATerm (s, tms)) =
if is_tptp_variable s then
Metis_Term.Var (Metis_Name.fromString s)
else
- let
- val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
- |> the_default (s, false)
- in
- Metis_Term.Fn (Metis_Name.fromString s,
- tms |> map metis_term_from_atp |> swap ? rev)
- end
-fun metis_atom_from_atp (AAtom tm) =
- (case metis_term_from_atp tm of
+ (case AList.lookup (op =) metis_name_table (s, length tms) of
+ SOME (f, swap) => (f type_enc, swap)
+ | NONE => (s, false))
+ |> (fn (s, swap) =>
+ Metis_Term.Fn (Metis_Name.fromString s,
+ tms |> map (metis_term_from_atp type_enc)
+ |> swap ? rev))
+fun metis_atom_from_atp type_enc (AAtom tm) =
+ (case metis_term_from_atp type_enc tm of
Metis_Term.Fn x => x
| _ => raise Fail "non CNF -- expected function")
- | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
-fun metis_literal_from_atp (AConn (ANot, [phi])) =
- (false, metis_atom_from_atp phi)
- | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
-fun metis_literals_from_atp (AConn (AOr, phis)) =
- maps metis_literals_from_atp phis
- | metis_literals_from_atp phi = [metis_literal_from_atp phi]
-fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
+ | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
+ (false, metis_atom_from_atp type_enc phi)
+ | metis_literal_from_atp type_enc phi =
+ (true, metis_atom_from_atp type_enc phi)
+fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
+ maps (metis_literals_from_atp type_enc) phis
+ | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
+fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
let
fun some isa =
- SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+ SOME (phi |> metis_literals_from_atp type_enc
+ |> Metis_LiteralSet.fromList
|> Metis_Thm.axiom, isa)
in
if ident = type_tag_idempotence_helper_name orelse
@@ -164,7 +171,7 @@
in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
| NONE => TrueI |> Isa_Raw |> some
end
- | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
+ | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
@@ -205,8 +212,8 @@
*)
(* "rev" is for compatibility. *)
val axioms =
- atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
- |> rev
+ atp_problem
+ |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
in (sym_tab, axioms, old_skolems) end
end;
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Aug 25 14:26:38 2011 -0700
@@ -152,16 +152,14 @@
fun prep (ct, vars) (maxidx, all_vars) =
let
- val maxidx' = maxidx_of ct + maxidx + 1
+ val maxidx' = maxidx + maxidx_of ct + 1
fun part (v as (i, cv)) =
(case AList.lookup (op =) all_vars i of
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
| NONE =>
- if not (exists (equal_var cv) all_vars) then apsnd (cons v)
- else
- let val cv' = Thm.incr_indexes_cterm maxidx' cv
- in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
+ let val cv' = Thm.incr_indexes_cterm maxidx cv
+ in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
val (inst, vars') =
if null vars then ([], vars)
@@ -170,7 +168,7 @@
in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
in
fun mk_fun f ts =
- let val (cts, (_, vars)) = fold_map prep ts (~1, [])
+ let val (cts, (_, vars)) = fold_map prep ts (0, [])
in f cts |> Option.map (rpair vars) end
end
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu Aug 25 14:26:38 2011 -0700
@@ -147,13 +147,15 @@
val remove_weight = mk_meta_eq @{thm SMT.weight_def}
val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
- fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
- (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
+ fun rewrite_conv _ [] = Conv.all_conv
+ | rewrite_conv ctxt eqs = Simplifier.full_rewrite
+ (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
remove_fun_app, Z3_Proof_Literals.rewrite_true]
- fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+ fun rewrite _ [] = I
+ | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
@@ -630,7 +632,8 @@
in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
val sk_rules = @{lemma
- "(EX x. P x) = P (SOME x. P x)" "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
+ "c = (SOME x. P x) ==> (EX x. P x) = P c"
+ "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
by (metis someI_ex)+}
in
@@ -638,9 +641,10 @@
apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
fun discharge_sk_tac i st = (
- Tactic.rtac @{thm trans}
- THEN' Tactic.resolve_tac sk_rules
- THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
+ Tactic.rtac @{thm trans} i
+ THEN Tactic.resolve_tac sk_rules i
+ THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+ THEN Tactic.rtac @{thm refl} i) st
end
@@ -654,7 +658,7 @@
Z3_Proof_Tools.by_tac (
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
ORELSE' NAMED ctxt' "simp+arith" (
- Simplifier.simp_tac simpset
+ Simplifier.asm_full_simp_tac simpset
THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
@@ -717,13 +721,15 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
@@ -731,7 +737,8 @@
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Z3_Proof_Tools.by_tac (
- NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 25 14:25:19 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 25 14:26:38 2011 -0700
@@ -148,7 +148,7 @@
| _ => value)
| NONE => (name, value)
-(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
+(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
correctly. *)
fun implode_param [s, "?"] = s ^ "?"
| implode_param [s, "!"] = s ^ "!"