# HG changeset patch # User huffman # Date 1315320075 25200 # Node ID ab7522fbe1a254a4596aa9898662cb34e87f4305 # Parent 9e4f7d3b53767b6073bbcee8e1f6da103348db8a# Parent bdf8eb8f126b1a13df6e58f7f8d0b12764e98036 merged diff -r 9e4f7d3b5376 -r ab7522fbe1a2 doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Finite_Set.thy --- 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 \ + Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ 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 \ 'b) set)" shows "finite (UNIV :: 'b set)" diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Fun.thy --- 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 \ (g(x := y)) = (f \ g)(x := f y)" by (auto intro: ext) +lemma UNION_fun_upd: + "UNION J (A(i:=B)) = (UNION (J-{i}) A \ (if i\J then B else {}))" +by (auto split: if_splits) + subsection {* @{text override_on} *} diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 \ nat \ 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 \ nat \ bool" + "+" > Groups.plus_class.plus :: "nat \ nat \ nat" + "*" > Groups.times_class.times :: "nat \ nat \ nat" + "-" > Groups.minus_class.minus :: "nat \ nat \ nat" + MIN > Orderings.ord_class.min :: "nat \ nat \ nat" + MAX > Orderings.ord_class.max :: "nat \ nat \ nat" + DIV > Divides.div_class.div :: "nat \ nat \ nat" + MOD > Divides.div_class.mod :: "nat \ nat \ nat" + EXP > Power.power_class.power :: "nat \ nat \ 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 \ nat \ 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; diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- 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 \ real" + inv > Fields.inverse_class.inverse :: "real \ real" + real_add > Groups.plus_class.plus :: "real \ real \ real" + real_sub > Groups.minus_class.minus :: "real \ real \ real" + real_mul > Groups.times_class.times :: "real \ real \ real" + real_div > Fields.inverse_class.divide :: "real \ real \ real" + real_lt > Orderings.ord_class.less :: "real \ real \ 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 \ real \ bool" + real_sub > Groups.minus_class.minus :: "real \ real \ real" + "/" > Fields.inverse_class.divide :: "real \ real \ real" + pow > Power.power_class.power :: "real \ nat \ real" + abs > Groups.abs_class.abs :: "real => real" real_of_num > RealDef.real :: "nat => real"; end_import; diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Import/HOL4Compat.thy --- 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 diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Set.thy --- 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 \ A" "b \ B" +shows "insert a A = insert b B \ + (if a=b then A=B else \C. A = insert b C \ b \ C \ B = insert a C \ a \ C)" + (is "?L \ ?R") +proof + assume ?L + show ?R + proof cases + assume "a=b" with assms `?L` show ?R by (simp add: insert_ident) + next + assume "a\b" + let ?C = "A - {b}" + have "A = insert b ?C \ b \ ?C \ B = insert a ?C \ a \ ?C" + using assms `?L` `a\b` by auto + thus ?R using `a\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}" diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r 9e4f7d3b5376 -r ab7522fbe1a2 src/HOL/Tools/ATP/atp_translate.ML --- 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