--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Sep 05 22:30:25 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Sep 06 07:41:15 2011 -0700
@@ -108,11 +108,11 @@
results are correct by construction.
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
-Sledgehammer also provides an automatic mode that can be enabled via the
-``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
-this mode, Sledgehammer is run on every newly entered theorem. The time limit
-for Auto Sledgehammer and other automatic tools can be set using the ``Auto
-Tools Time Limit'' option.
+Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
+Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
+Sledgehammer is run on every newly entered theorem. The time limit for Auto
+Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
+Limit'' option.
\newbox\boxA
\setbox\boxA=\hbox{\texttt{nospam}}
@@ -633,8 +633,8 @@
highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
You can instruct Sledgehammer to run automatically on newly entered theorems by
-enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
-General. For automatic runs, only the first prover set using \textit{provers}
+enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
+For automatic runs, only the first prover set using \textit{provers}
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{sound}
(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
@@ -724,7 +724,7 @@
\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP higher-order syntax (THF).
+with support for the TPTP many-typed higher-order syntax (THF0).
\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
the external provers, Metis itself can be used for proof search.
@@ -737,7 +737,7 @@
\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP higher-order syntax (THF).
+support for the TPTP many-typed higher-order syntax (THF0).
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
@@ -752,7 +752,7 @@
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
-supports the TPTP many-typed first-order format (TFF).
+supports the TPTP many-typed first-order format (TFF0).
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
SRI \cite{yices}. To use Yices, set the environment variable
@@ -767,7 +767,7 @@
\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
-formats (FOF and TFF). It is included for experimental purposes. It requires
+formats (FOF and TFF0). It is included for experimental purposes. It requires
version 3.0 or above.
\end{enum}
@@ -787,7 +787,7 @@
\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP many-typed first-order format (TFF). The
+servers. This ATP supports the TPTP many-typed first-order format (TFF0). The
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
@@ -798,7 +798,7 @@
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
-TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
+TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on
Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
@@ -818,17 +818,16 @@
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
+By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
the SMT module's \textit{smt\_solver} configuration option is set to), and (if
appropriate) Waldmeister in parallel---either locally or remotely, depending on
the number of processor cores available. For historical reasons, the default
value of this option can be overridden using the option ``Sledgehammer:
-Provers'' from the ``Isabelle'' menu in Proof General.
+Provers'' in Proof General's ``Isabelle'' menu.
-It is a good idea to run several provers in parallel, although it could slow
-down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
-success rate to running the most effective of these for 120~seconds
-\cite{boehme-nipkow-2010}.
+It is generally a good idea to run several provers in parallel. Running E,
+SPASS, and Vampire for 5~seconds yields a similar success rate to running the
+most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
For the \textit{min} subcommand, the default prover is \textit{metis}. If
several provers are set, the first one is used.
@@ -884,7 +883,13 @@
Specifies the type encoding to use in ATP problems. Some of the type encodings
are unsound, meaning that they can give rise to spurious proofs
(unreconstructible using Metis). The supported type encodings are listed below,
-with an indication of their soundness in parentheses:
+with an indication of their soundness in parentheses.
+%
+All the encodings with \textit{guards} or \textit{tags} in their name are
+available in 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{mono\_guards\_uniform}{?}).
\begin{enum}
\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
@@ -926,27 +931,27 @@
$\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{mono\_guards}. The problem is monomorphized.
+\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
+first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
+falls back on \textit{mono\_guards\_uniform}. 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{mono\_guards\_uniform}. The problem is
+\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
+higher-order types if the prover supports the THF0 syntax; otherwise, falls back
+on \textit{mono\_simple} or \textit{mono\_guards\_uniform}. The problem is
monomorphized.
\item[$\bullet$]
\textbf{%
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
-\textit{simple}? (quasi-sound):} \\
+\textit{mono\_simple}? (quasi-sound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
-\textit{mono\_tags}, and \textit{simple} are fully
+\textit{mono\_tags}, and \textit{mono\_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
-are not actually erased but rather replaced by a shared uniform type of
+erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
+types are not actually erased but rather replaced by a shared uniform type of
individuals.) As argument to the \textit{metis} proof method, the question mark
is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
is enabled, these encodings are fully sound.
@@ -954,30 +959,25 @@
\item[$\bullet$]
\textbf{%
\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):} \\
+\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
+\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
\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},
-the types are not actually erased but rather replaced by a shared uniform type
-of individuals.) As argument to the \textit{metis} proof method, the exclamation
-mark is replaced by the suffix \hbox{``\textit{\_bang}''}.
+\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_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{mono\_simple} and
+\textit{mono\_simple\_higher}, the types are not actually erased but rather
+replaced by a shared uniform type of individuals.) As argument to the
+\textit{metis} proof method, the exclamation mark is replaced by the suffix
+\hbox{``\textit{\_bang}''}.
\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
-In addition, all the \textit{guards} and \textit{tags} type encodings are
-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{mono\_guards\_uniform}{?}).
-
-For SMT solvers, the type encoding is always \textit{simple}, irrespective of
-the value of this option.
+For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
+of the value of this option.
\nopagebreak
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
@@ -1091,8 +1091,7 @@
Specifies the maximum number of seconds that the automatic provers should spend
searching for a proof. This excludes problem preparation and is a soft limit.
For historical reasons, the default value of this option can be overridden using
-the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
-General.
+the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
Specifies the maximum number of seconds that Metis should be spent trying to
--- a/src/HOL/Finite_Set.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Finite_Set.thy Tue Sep 06 07:41:15 2011 -0700
@@ -2054,6 +2054,11 @@
apply(auto intro:ccontr)
done
+lemma card_le_Suc_iff: "finite A \<Longrightarrow>
+ Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
+by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
+ dest: subset_singletonD split: nat.splits if_splits)
+
lemma finite_fun_UNIVD2:
assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
shows "finite (UNIV :: 'b set)"
--- a/src/HOL/Fun.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Fun.thy Tue Sep 06 07:41:15 2011 -0700
@@ -612,6 +612,10 @@
lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
by (auto intro: ext)
+lemma UNION_fun_upd:
+ "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
+by (auto split: if_splits)
+
subsection {* @{text override_on} *}
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Tue Sep 06 07:41:15 2011 -0700
@@ -12,17 +12,20 @@
import_theory bool;
+type_maps
+ bool > HOL.bool;
+
const_maps
- T > True
- F > False
- "!" > All
+ T > HOL.True
+ F > HOL.False
+ "!" > HOL.All
"/\\" > HOL.conj
"\\/" > HOL.disj
- "?" > Ex
- "?!" > Ex1
- "~" > Not
+ "?" > HOL.Ex
+ "?!" > HOL.Ex1
+ "~" > HOL.Not
COND > HOL.If
- bool_case > Datatype.bool.bool_case
+ bool_case > Product_Type.bool.bool_case
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > Fun.surj
TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
@@ -46,7 +49,7 @@
import_theory sum;
type_maps
- sum > "+";
+ sum > Sum_Type.sum;
const_maps
INL > Sum_Type.Inl
@@ -55,7 +58,7 @@
ISR > HOL4Compat.ISR
OUTL > HOL4Compat.OUTL
OUTR > HOL4Compat.OUTR
- sum_case > Datatype.sum.sum_case;
+ sum_case > Sum_Type.sum.sum_case;
ignore_thms
sum_TY_DEF
@@ -63,7 +66,6 @@
IS_SUM_REP
INL_DEF
INR_DEF
- sum_axiom
sum_Axiom;
end_import;
@@ -125,13 +127,13 @@
prod > Product_Type.prod;
const_maps
- "," > Pair
- FST > fst
- SND > snd
- CURRY > curry
- UNCURRY > split
- "##" > map_pair
- pair_case > split;
+ "," > Product_Type.Pair
+ FST > Product_Type.fst
+ SND > Product_Type.snd
+ CURRY > Product_Type.curry
+ UNCURRY > Product_Type.prod.prod_case
+ "##" > Product_Type.map_pair
+ pair_case > Product_Type.prod.prod_case;
ignore_thms
prod_TY_DEF
@@ -145,11 +147,11 @@
import_theory num;
type_maps
- num > nat;
+ num > Nat.nat;
const_maps
- SUC > Suc
- 0 > 0 :: nat;
+ SUC > Nat.Suc
+ 0 > Groups.zero_class.zero :: nat;
ignore_thms
num_TY_DEF
@@ -165,7 +167,7 @@
import_theory prim_rec;
const_maps
- "<" > Orderings.less :: "[nat,nat]=>bool";
+ "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
end_import;
@@ -180,15 +182,15 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > Orderings.less_eq :: "[nat,nat]=>bool"
- "+" > Groups.plus :: "[nat,nat]=>nat"
- "*" > Groups.times :: "[nat,nat]=>nat"
- "-" > Groups.minus :: "[nat,nat]=>nat"
- MIN > Orderings.min :: "[nat,nat]=>nat"
- MAX > Orderings.max :: "[nat,nat]=>nat"
- DIV > Divides.div :: "[nat,nat]=>nat"
- MOD > Divides.mod :: "[nat,nat]=>nat"
- EXP > Power.power :: "[nat,nat]=>nat";
+ "<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ "+" > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "*" > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ "-" > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ MIN > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ DIV > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat";
end_import;
@@ -207,7 +209,7 @@
import_theory divides;
const_maps
- divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
+ divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
end_import;
@@ -227,7 +229,7 @@
HD > List.hd
TL > List.tl
MAP > List.map
- MEM > "List.op mem"
+ MEM > HOL4Compat.list_mem
FILTER > List.filter
FOLDL > List.foldl
EVERY > List.list_all
@@ -236,12 +238,12 @@
FRONT > List.butlast
APPEND > List.append
FLAT > List.concat
- LENGTH > Nat.size
+ LENGTH > Nat.size_class.size
REPLICATE > List.replicate
list_size > HOL4Compat.list_size
SUM > HOL4Compat.sum
FOLDR > HOL4Compat.FOLDR
- EXISTS > HOL4Compat.list_exists
+ EXISTS > List.list_ex
MAP2 > HOL4Compat.map2
ZIP > HOL4Compat.ZIP
UNZIP > HOL4Compat.unzip;
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Tue Sep 06 07:41:15 2011 -0700
@@ -16,13 +16,17 @@
real > RealDef.real;
const_maps
- real_0 > Groups.zero :: real
- real_1 > Groups.one :: real
- real_neg > Groups.uminus :: "real => real"
- inv > Groups.inverse :: "real => real"
- real_add > Groups.plus :: "[real,real] => real"
- real_mul > Groups.times :: "[real,real] => real"
- real_lt > Orderings.less :: "[real,real] => bool";
+ real_0 > Groups.zero_class.zero :: real
+ real_1 > Groups.one_class.one :: real
+ real_neg > Groups.uminus_class.uminus :: "real \<Rightarrow> real"
+ inv > Fields.inverse_class.inverse :: "real \<Rightarrow> real"
+ real_add > Groups.plus_class.plus :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_mul > Groups.times_class.times :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_div > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
+ mk_real > HOL.undefined (* Otherwise proof_import_concl fails *)
+ dest_real > HOL.undefined
ignore_thms
real_TY_DEF
@@ -50,11 +54,11 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > Orderings.less_eq :: "[real,real] => bool"
- real_sub > Groups.minus :: "[real,real] => real"
- "/" > Fields.divide :: "[real,real] => real"
- pow > Power.power :: "[real,nat] => real"
- abs > Groups.abs :: "real => real"
+ real_lte > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
+ real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
+ "/" > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
+ pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
+ abs > Groups.abs_class.abs :: "real => real"
real_of_num > RealDef.real :: "nat => real";
end_import;
--- a/src/HOL/Import/HOL4Compat.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Import/HOL4Compat.thy Tue Sep 06 07:41:15 2011 -0700
@@ -63,6 +63,14 @@
lemma OUTR: "OUTR (Inr x) = x"
by simp
+lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
+ apply (intro allI ex1I[of _ "sum_case f g"] conjI)
+ apply (simp_all add: o_def fun_eq_iff)
+ apply (rule)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
by simp
@@ -491,4 +499,6 @@
lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
by simp
+definition [hol4rew]: "list_mem x xs = List.member xs x"
+
end
--- a/src/HOL/Set.thy Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Set.thy Tue Sep 06 07:41:15 2011 -0700
@@ -785,6 +785,26 @@
lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
by auto
+lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"
+shows "insert a A = insert b B \<longleftrightarrow>
+ (if a=b then A=B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
+ (is "?L \<longleftrightarrow> ?R")
+proof
+ assume ?L
+ show ?R
+ proof cases
+ assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
+ next
+ assume "a\<noteq>b"
+ let ?C = "A - {b}"
+ have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
+ using assms `?L` `a\<noteq>b` by auto
+ thus ?R using `a\<noteq>b` by auto
+ qed
+next
+ assume ?R thus ?L by(auto split: if_splits)
+qed
+
subsubsection {* Singletons, using insert *}
lemma singletonI [intro!,no_atp]: "a : {a}"
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 07:41:15 2011 -0700
@@ -263,7 +263,7 @@
| str _ (ATyAbs (ss, ty)) =
tptp_pi_binder ^ "[" ^
commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
- ss) ^ "] : " ^ str false ty
+ ss) ^ "]: " ^ str false ty
in str true ty end
fun string_for_type (THF0 _) ty = str_for_type ty
@@ -308,7 +308,7 @@
| (_, 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 ^ "] : " ^
+ tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ""
|> enclose "(" ")"
@@ -320,12 +320,12 @@
s ^ "(" ^ commas ss ^ ")"
end)
| string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
- "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
+ "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ")"
| string_for_term _ _ = raise Fail "unexpected term in first-order format"
and string_for_formula format (AQuant (q, xs, phi)) =
string_for_quantifier q ^
- "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
+ "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
string_for_formula format phi
|> enclose "(" ")"
| string_for_formula format
--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Sep 05 22:30:25 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 07:41:15 2011 -0700
@@ -579,14 +579,18 @@
|> (fn (poly, (level, (uniformity, core))) =>
case (core, (poly, level, uniformity)) of
("simple", (SOME poly, _, Nonuniform)) =>
- (case poly of
- Raw_Monomorphic => raise Same.SAME
- | _ => Simple_Types (First_Order, poly, level))
+ (case (poly, level) of
+ (Polymorphic, All_Types) =>
+ Simple_Types (First_Order, Polymorphic, All_Types)
+ | (Mangled_Monomorphic, _) =>
+ Simple_Types (First_Order, Mangled_Monomorphic, level)
+ | _ => raise Same.SAME)
| ("simple_higher", (SOME poly, _, Nonuniform)) =>
(case (poly, level) of
- (Raw_Monomorphic, _) => raise Same.SAME
- | (_, Noninf_Nonmono_Types _) => raise Same.SAME
- | _ => Simple_Types (Higher_Order, poly, level))
+ (_, Noninf_Nonmono_Types _) => raise Same.SAME
+ | (Mangled_Monomorphic, _) =>
+ Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+ | _ => raise Same.SAME)
| ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
| ("tags", (SOME Polymorphic, _, _)) =>
Tags (Polymorphic, level, uniformity)
@@ -1369,16 +1373,14 @@
fun filter_type_args _ _ _ [] = []
| filter_type_args thy s arity T_args =
- let val U = robust_const_type thy s in
- case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
- [] => []
- | res_U_vars =>
- let val U_args = (s, U) |> Sign.const_typargs thy in
- U_args ~~ T_args
- |> map (fn (U, T) =>
- if member (op =) res_U_vars (dest_TVar U) then T
- else dummyT)
- end
+ let
+ val U = robust_const_type thy s
+ val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
+ val U_args = (s, U) |> robust_const_typargs thy
+ in
+ U_args ~~ T_args
+ |> map (fn (U, T) =>
+ if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
end
handle TYPE _ => T_args
@@ -1394,14 +1396,13 @@
| SOME s'' =>
let
val s'' = invert_const s''
- fun filtered_T_args false = T_args
- | filtered_T_args true = filter_type_args thy s'' arity T_args
+ fun filter_T_args false = T_args
+ | filter_T_args true = filter_type_args thy s'' arity T_args
in
case type_arg_policy type_enc s'' of
- Explicit_Type_Args drop_args =>
- (name, filtered_T_args drop_args)
+ Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
| Mangled_Type_Args drop_args =>
- (mangled_const_name format type_enc (filtered_T_args drop_args)
+ (mangled_const_name format type_enc (filter_T_args drop_args)
name, [])
| No_Type_Args => (name, [])
end)
@@ -1555,9 +1556,8 @@
let
fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
| add (t $ u) = add t #> add u
- | add (Const (x as (s, _))) =
- if String.isPrefix skolem_const_prefix s then I
- else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
+ | add (Const x) =
+ x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
| add (Free (s, T)) =
if String.isPrefix polymorphic_free_prefix s then
T |> fold_type_constrs set_insert