--- a/NEWS Fri May 20 14:03:42 2011 +0200
+++ b/NEWS Fri May 20 14:12:59 2011 +0200
@@ -58,11 +58,20 @@
*** HOL ***
+* Finite_Set.thy: more coherent development of fold_set locales:
+
+ locale fun_left_comm ~> locale comp_fun_commute
+ locale fun_left_comm_idem ~> locale comp_fun_idem
+
+Both use point-free characterisation; interpretation proofs may need adjustment.
+INCOMPATIBILITY.
+
+* Code generation:
+ - theory Library/Code_Char_ord provides native ordering of characters
+ in the target language.
+
* Declare ext [intro] by default. Rare INCOMPATIBILITY.
-* Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
-interpretation proofs may need adjustment. INCOMPATIBILITY.
-
* Nitpick:
- Added "need" and "total_consts" options.
- Reintroduced "show_skolems" option by popular demand.
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 14:03:42 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 14:12:59 2011 +0200
@@ -118,7 +118,7 @@
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
\texttt{src/HOL/Metis\_Examples} directory.
Comments and bug reports concerning Sledgehammer or this manual should be
-directed to \authoremail.
+directed to the author at \authoremail.
\vskip2.5\smallskipamount
@@ -169,9 +169,10 @@
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
+with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
-reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
+reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
+say, Vampire 11.5.}%
. Since the ATPs' output formats are neither documented nor stable, other
versions of the ATPs might or might not work well with Sledgehammer. Ideally,
also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
@@ -254,19 +255,19 @@
%
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
+Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
\postw
@@ -282,7 +283,7 @@
the proof found by E looks perfect, so click it to finish the proof.
You can ask Sledgehammer for an Isar text proof by passing the
-\textit{isar\_proof} option:
+\textit{isar\_proof} option (\S\ref{output-format}):
\prew
\textbf{sledgehammer} [\textit{isar\_proof}]
@@ -295,6 +296,10 @@
\section{Hints}
\label{hints}
+This section presents a few hints that should help you get the most out of
+Sledgehammer and Metis. Frequently (and infrequently) asked questions are
+answered in \S\ref{frequently-asked-questions}.
+
\newcommand\point[1]{{\sl\bfseries#1}\par\nopagebreak}
\point{Presimplify the goal}
@@ -320,49 +325,54 @@
familiarize themselves with the following options:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{provers}} specifies the ATP and SMT solvers to
-use (e.g., ``\textit{provers} = \textit{e spass remote\_vampire}'').
+\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
+the automatic provers (ATPs and SMT solvers) that should be run whenever
+Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
+remote\_vampire}'').
-\item[$\bullet$] \textbf{\textit{timeout}} controls the time limit. It is set to
-30 seconds, but since Sledgehammer runs asynchronously you should not hesitate
-to crank up this limit to 60 or 120 seconds if you are the kind of user who can
-think clearly while ATPs are active.
+\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) controls
+the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
+asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
+if you are the kind of user who can think clearly while ATPs are active.
-\item[$\bullet$] \textbf{\textit{full\_types}} specifies whether type-sound
-encodings should be used. By default, Sledgehammer employs a mixture of
-type-sound and type-unsound encodings, occasionally yielding unsound ATP proofs.
-(SMT solver proofs should always be sound, although we occasionally find
-soundness bugs in the solvers.)
+\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
+specifies whether type-sound encodings should be used. By default, Sledgehammer
+employs a mixture of type-sound and type-unsound encodings, occasionally
+yielding unsound ATP proofs. (SMT solver proofs should always be sound, although
+we occasionally find soundness bugs in the solvers.)
-\item[$\bullet$] \textbf{\textit{max\_relevant}} specifies the maximum number of
-facts that should be passed to the provers. By default, the value is
-prover-dependent but varies between about 150 and 1000. If the provers time out,
-you can try lowering this value to, say, 100 or 50 and see if that helps.
+\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
+specifies the maximum number of facts that should be passed to the provers. By
+default, the value is prover-dependent but varies between about 150 and 1000. If
+the provers time out, you can try lowering this value to, say, 100 or 50 and see
+if that helps.
-\item[$\bullet$] \textbf{\textit{isar\_proof}} specifies that Isar proofs should
-be generated, instead of one-liner Metis proofs. The length of the Isar proofs
-can be controlled by setting \textit{isar\_shrink\_factor}.
+\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
+that Isar proofs should be generated, instead of one-liner Metis proofs. The
+length of the Isar proofs can be controlled by setting
+\textit{isar\_shrink\_factor} (\S\ref{output-format}).
\end{enum}
-Options can be set globally using \textbf{sledgehammer\_params}. Fact selection
-can be influenced by specifying ``$(\textit{add}{:}~\textit{some\_facts})$'' after
-the \textbf{sledgehammer} call to ensure that certain facts are included, or
-simply ``$(\textit{some\_facts})$'' to force Sledgehammer to run only with
-$\textit{some\_facts}$.
+Options can be set globally using \textbf{sledgehammer\_params}
+(\S\ref{command-syntax}). Fact selection can be influenced by specifying
+``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer}
+call to ensure that certain facts are included, or simply
+``$(\textit{my\_facts})$'' to force Sledgehammer to run only with
+$\textit{my\_facts}$.
\section{Frequently Asked Questions}
\label{frequently-asked-questions}
\point{Why does Metis fail to reconstruct the proof?}
-There can be many reasons. If Metis runs seemingly forever, that's a sign that
-the proof is too difficult for it. Metis is complete, so it should eventually
-find it, but that's little consolation. There are several possible solutions:
+There are many reasons. If Metis runs seemingly forever, that is a sign that the
+proof is too difficult for it. Metis is complete, so it should eventually find
+it, but that's little consolation. There are several possible solutions:
\begin{enum}
-\item[$\bullet$] Try the \textit{isar\_proof} option to obtain a step-by-step
-Isar proof where each step is justified by Metis. Since the steps are fairly
-small, Metis is more likely to be able to replay them.
+\item[$\bullet$] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
+obtain a step-by-step Isar proof where each step is justified by Metis. Since
+the steps are fairly small, Metis is more likely to be able to replay them.
\item[$\bullet$] Try the \textit{smt} proof method instead of \textit{metis}. It
is usually stronger, but you need to have Z3 available to replay the proofs,
@@ -374,70 +384,119 @@
\textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
\end{enum}
-% * sometimes Metis runs into some error, e.g. a type error. then it tries
-% again with metisFT, where FT stands for ``full type information'
-% * metisFT is much slower, but its proof search is fully typed, and it also
-% includes more powerful rules such as the axiom ``$x = \mathit{True}
-% \mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places
-% (e.g., in set comprehensions)
-%
-% * finally, in some cases the ATP proof is simply type-incorrect.
-% Sledgehammer drops some type information to speed up the search. Try
-% Sledgehammer again with full type information: \textit{full\_types}
-% (\S\ref{problem-encoding}), or choose a specific type encoding with
-% \textit{type\_sys} (\S\ref{problem-encoding}). Older versions of
-% Sledgehammer were frequent victims of this problem. Now this should very
-% seldom be an issue, but if you notice too many unsound proofs, contact
-%
-%\point{How can I easily tell whether a Sledgehammer proof is sound?}
-%
-%Easiest way: Once it's found: ... by (metis facts)
-%try
-%sledgehammer [full\_types] (facts)
-%
-%should usually give unprovable or refind the proof fairly quickly
-%
-%Same trick if you believe that there exists a proof with certain facts.
-%
-%\point{Which facts does Sledgehammer select?}
-%
-% * heuristic
-% * and several hundreds
-% * show them: debug
-% * influence it with sledgehammer (add: xxx)
-%
-% * S/h good at finding short proofs combining a handful of existing lemmas
-% * for deeper proofs, you must restrict the number of facts, e.g.
-% max\_relevant = 50
-% * but then proof reconstruction is an issue
-%
-%\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
-%
-% * experimental
-% * working on this
-% * there is a large body of research into transforming resolution proofs into
-% natural deduction proofs (e.g., Isar proofs)
-% * meantime: isar\_shrink\_factor
-%
-%
-%\point{Should I let Sledgehammer minimize the number of lemmas?}
-%
-% * in general, yes
-% * proofs involving fewer lemmas tend to be shorter as well, and hence easier
-% to re-find by Metis
-% * but the opposite is sometimes the case
+In some rare cases, Metis fails fairly quickly. This usually indicates that
+Sledgehammer found a type-incorrect proof. Sledgehammer erases some type
+information to speed up the search. Try Sledgehammer again with full type
+information: \textit{full\_types} (\S\ref{problem-encoding}), or choose a
+specific type encoding with \textit{type\_sys} (\S\ref{problem-encoding}). Older
+versions of Sledgehammer were frequent victims of this problem. Now this should
+very seldom be an issue, but if you notice many unsound proofs, contact the
+author at \authoremail.
+
+\point{How can I tell whether a Sledgehammer proof is sound?}
+
+First, if \emph{metis} (or \emph{metisFT}) can reconstruct it, the proof is
+sound (modulo soundness of Isabelle's inference kernel). If it fails or runs
+seemingly forever, you can try
+
+\prew
+\textbf{apply}~\textbf{--} \\
+\textbf{sledgehammer} [\textit{type\_sys} = \textit{poly\_tags}] (\textit{metis\_facts})
+\postw
+
+where \textit{metis\_facts} is the list of facts appearing in the suggested
+Metis call. The automatic provers should be able to refind the proof very
+quickly if it is sound, and the \textit{type\_sys} $=$ \textit{poly\_tags}
+option (\S\ref{problem-encoding}) ensures that no unsound proofs are found.
+
+The \textit{full\_types} option (\S\ref{problem-encoding}) can also be used
+here, but it is unsound in extremely rare degenerate cases such as the
+following:
+
+\prew
+\textbf{lemma} ``$\forall x\> y\Colon{'}a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}a.\ f \not= g$'' \\
+\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
+\postw
+
+\point{How does Sledgehammer select the facts that should be passed to the
+automatic provers?}
+
+Briefly, the relevance filter assigns a score to every available fact (lemma,
+theorem, definition, or axiom)\ based upon how many constants that fact shares
+with the conjecture; this process iterates to include facts relevant to those
+just accepted, but with a decay factor to ensure termination. The constants are
+weighted to give unusual ones greater significance. The relevance filter copes
+best when the conjecture contains some unusual constants; if all the constants
+are common, it is unable to discriminate among the hundreds of facts that are
+picked up. The relevance filter is also memoryless: It has no information about
+how many times a particular fact has been used in a proof, and it cannot learn.
+
+The number of facts included in a problem varies from prover to prover, since
+some provers get overwhelmed quicker than others. You can show the number of
+facts given using the \textit{verbose} option (\S\ref{output-format}) and the
+actual facts using \textit{debug} (\S\ref{output-format}).
+
+Sledgehammer is good at finding short proofs combining a handful of existing
+lemmas. If you are looking for longer proofs, you must typically restrict the
+number of facts, by setting the \textit{max\_relevant} option
+(\S\ref{relevance-filter}) to, say, 50 or 100.
+
+\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
+
+The current implementation is experimental and explodes exponentially in the
+worst case. Work on a new implementation has begun. There is a large body of
+research into transforming resolution proofs into natural deduction proofs (such
+as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
+set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
+value or to try several provers and keep the nicest-looking proof.
+
+\point{Should I let Sledgehammer minimize the number of lemmas?}
+
+In general, minimization is a good idea, because proofs involving fewer lemmas
+tend to be shorter as well, and hence easier to re-find by Metis. But the
+opposite is sometimes the case.
+
+\point{Why does the minimizer sometimes starts of its own?}
+
+There are two scenarios in which this can happen. First, some provers (e.g.,
+CVC3 and Yices) do not provide proofs or provide incomplete proofs. The
+minimizer is then invoked to find out which facts are actually needed from the
+(large) set of facts that was initinally given to the prover. Second, if a
+prover returns a proof with lots of facts, the minimizer is invoked
+automatically since Metis is unlikely to refind the proof.
+
+\point{What is metisFT?}
+
+The \textit{metisFT} proof method is the fully-typed version of Metis. It is
+much slower than \textit{metis}, but the proof search is fully typed, and it
+also includes more powerful rules such as the axiom ``$x = \mathit{True}
+\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
+in set comprehensions). The method kicks in automatically as a fallback when
+\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
+\textit{metis} if the proof obviously requires type information.
+
+If you see the warning
+
+\prew
+\textsl
+Metis: Falling back on ``\textit{metisFT}''.
+\postw
+
+in a successful Metis proof, you can advantageously replace the \textit{metis}
+call with \textit{metisFT}.
\point{I got a strange error from Sledgehammer---what should I do?}
Sledgehammer tries to give informative error messages. Please report any strange
-error to \authoremail. This applies double if you get the message
+error to the author at \authoremail. This applies double if you get the message
-\begin{quote}
+\prew
\slshape
-The prover found a type-unsound proof even though a supposedly type-sound
-encoding was used (or, very unlikely, your axioms are inconsistent). You
-might want to report this to the Isabelle developers.
-\end{quote}
+The prover found a type-unsound proof involving ``\textit{foo}'',
+``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding
+was used (or, less likely, your axioms are inconsistent). You might want to
+report this to the Isabelle developers.
+\postw
\point{Auto can solve it---why not Sledgehammer?}
@@ -446,6 +505,13 @@
Because the system refers to all theorems known to Isabelle, it is particularly
suitable when your goal has a short proof from lemmas that you don't know about.
+\point{Why are there so many options?}
+
+Sledgehammer's philosophy should work out of the box, without user guidance.
+Many of the options are meant to be used mostly by the Sledgehammer developers
+for experimentation purposes. Of course, feel free to experiment with them if
+you are so inclined.
+
\section{Command Syntax}
\label{command-syntax}
@@ -632,7 +698,7 @@
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
servers. This ATP supports a fragment of the TPTP many-typed first-order format
(TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}).
+\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
@@ -669,17 +735,18 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opnodefault{atps}{string}
-Legacy alias for \textit{provers}.
+%\opnodefault{atps}{string}
+%Legacy alias for \textit{provers}.
-\opnodefault{atp}{string}
-Legacy alias for \textit{provers}.
+%\opnodefault{atp}{string}
+%Legacy alias for \textit{provers}.
\opdefault{timeout}{float\_or\_none}{\upshape 30}
Specifies the maximum number of seconds that the automatic provers should spend
-searching for a proof. 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.
+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.
\opfalse{blocking}{non\_blocking}
Specifies whether the \textbf{sledgehammer} command should operate
@@ -732,45 +799,42 @@
option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
\opdefault{type\_sys}{string}{smart}
-Specifies the type system to use in ATP problems. The option can take the
-following values:
+Specifies the type system to use in ATP problems. Some of the type systems are
+unsound, meaning that they can give rise to spurious proofs (unreconstructible
+using Metis). The supported type systems are listed below, with an indication of
+their soundness in parentheses:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate
-$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
-Constants are annotated with their types, supplied as extra arguments, to
-resolve overloading.
+\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
+supplied to the ATP. Types are simply erased.
-\item[$\bullet$] \textbf{\textit{poly\_tags}:} Each term and subterm is tagged with
-its type using a function $\mathit{type\_info\/}(\tau, t)$.
+\item[$\bullet$] \textbf{\textit{poly\_preds} (sound):} Types are encoded using
+a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range
+of bound variables. Constants are annotated with their types, supplied as extra
+arguments, to resolve overloading.
-\item[$\bullet$] \textbf{\textit{poly\_args}:}
-Like for the other sound encodings, constants are annotated with their types to
+\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
+tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
+
+\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
+Like for \textit{poly\_preds} constants are annotated with their types to
resolve overloading, but otherwise no type information is encoded.
-\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
-the ATP. Types are simply erased.
-
\item[$\bullet$]
\textbf{%
-\textit{mono\_preds},
-\textit{mono\_tags},
-\textit{mono\_args}:} \\
+\textit{mono\_preds}, \textit{mono\_tags} (sound);
+\textit{mono\_args} (unsound):} \\
Similar to \textit{poly\_preds}, \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.
Monomorphization can simplify reasoning but also leads to larger fact bases,
which can slow down the ATPs.
-\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for
-simply typed first-order logic if available; otherwise, fall back on
-\textit{mangled\_preds}. The problem is monomorphized.
-
\item[$\bullet$]
\textbf{%
\textit{mangled\_preds},
-\textit{mangled\_tags},
-\textit{mangled\_args}:} \\
+\textit{mangled\_tags} (sound); \\
+\textit{mangled\_args} (unsound):} \\
Similar to
\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
respectively but types are mangled in constant names instead of being supplied
@@ -779,50 +843,52 @@
$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
$\mathit{type\_info\_}\tau(t)$.
+\item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for
+simply typed first-order logic if available; otherwise, fall back on
+\textit{mangled\_preds}. The problem is monomorphized.
+
\item[$\bullet$]
\textbf{%
-\textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple\_types}?, \\
-\textit{mangled\_preds}?, \textit{mangled\_tags}?:} \\
-The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
-\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
-virtually sound---except for pathological cases, all found proofs are
-type-correct. For each of these, Sledgehammer also provides a lighter (but
-virtually sound) variant identified by a question mark (`{?}')\ that detects and
-erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
-types are not actually erased but rather replaced by a shared uniform type of
-individuals.)
+\textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
+\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
+The type systems \textit{poly\_preds}, \textit{poly\_tags},
+\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
+\textit{mangled\_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 are not actually erased
+but rather replaced by a shared uniform type of individuals.)
\item[$\bullet$]
\textbf{%
-\textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
-\textit{simple\_types}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\
+\textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
+\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}! \\
+(mildly unsound):} \\
The type systems \textit{poly\_preds}, \textit{poly\_tags},
-\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
-\textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat
-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\_types}, the types are not actually
-erased but rather replaced by a shared uniform type of individuals.)
+\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
+\textit{mangled\_tags}, and \textit{simple} 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}, the types are not actually erased but
+rather replaced by a shared uniform type of individuals.)
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
-uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
-actual encoding used depends on the ATP and should be the most efficient for
-that ATP.
+uses a sound or virtually sound encoding; otherwise, uses any encoding. The actual
+encoding used depends on the ATP and should be the most efficient for that ATP.
\end{enum}
-For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
+In addition, all the \textit{preds} and \textit{tags} type systems are available
+in two variants, a lightweight and a heavyweight variant. The lightweight
+variants are generally more efficient and are the default; the heavyweight
+variants are identified by a \textit{\_heavy} suffix (e.g.,
+\textit{mangled\_preds\_heavy}{?}).
-\opdefault{max\_mono\_iters}{int}{\upshape 5}
-Specifies the maximum number of iterations for the monomorphization fixpoint
-construction. The higher this limit is, the more monomorphic instances are
-potentially generated. Whether monomorphization takes place depends on the
-type system used.
+For SMT solvers and ToFoF-E, the type system is always \textit{simple},
+irrespective of the value of this option.
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 250}
-Specifies the maximum number of monomorphic instances to generate beyond
-\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
-are potentially generated. Whether monomorphization takes place depends on the
-type system used.
+\nopagebreak
+{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
+and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
\end{enum}
\subsection{Relevance Filter}
@@ -843,6 +909,23 @@
empirically found to be appropriate for the prover. A typical value would be
300.
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
+Specifies the maximum number of monomorphic instances to generate beyond
+\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
+are potentially generated. Whether monomorphization takes place depends on the
+type system used.
+
+\nopagebreak
+{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+
+\opdefault{max\_mono\_iters}{int}{\upshape 3}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated. Whether monomorphization takes place depends on the
+type system used.
+
+\nopagebreak
+{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
\end{enum}
\subsection{Output Format}
--- a/doc-src/manual.bib Fri May 20 14:03:42 2011 +0200
+++ b/doc-src/manual.bib Fri May 20 14:12:59 2011 +0200
@@ -421,7 +421,7 @@
@misc{yices,
author = {Bruno Dutertre and Leonardo de Moura},
title = {The {Yices} {SMT} Solver},
- publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+ howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
year = 2006}
@incollection{dybjer91,
@@ -648,10 +648,15 @@
number = 5,
month = May}
-@misc{sine,
- author = "Kry\v{s}tof Hoder",
- title = "{SInE} (Sumo Inference Engine)",
- note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
+@inproceedings{sine,
+ author = "Kry\v{s}tof Hoder and Andrei Voronkov",
+ title = "Sine Qua Non for Large Theory Reasoning",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011,
+ note = "To appear."}
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
--- a/src/HOL/Big_Operators.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Big_Operators.thy Fri May 20 14:12:59 2011 +0200
@@ -1205,7 +1205,7 @@
proof qed (rule inf_assoc inf_commute inf_idem)+
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
-by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
+by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
by (induct pred: finite) (auto intro: le_infI1)
--- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri May 20 14:12:59 2011 +0200
@@ -4,7 +4,7 @@
header {* Generating code using pretty literals and natural number literals *}
theory Candidates_Pretty
-imports Candidates Code_Char Efficient_Nat
+imports Candidates Code_Char_ord Efficient_Nat
begin
end
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri May 20 14:12:59 2011 +0200
@@ -9,8 +9,6 @@
lemma [code, code del]: "nat_of_char = nat_of_char" ..
lemma [code, code del]: "char_of_nat = char_of_nat" ..
-lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
-lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
subsection {* Check whether generated code compiles *}
--- a/src/HOL/Finite_Set.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Finite_Set.thy Fri May 20 14:12:59 2011 +0200
@@ -532,13 +532,13 @@
if @{text f} is ``left-commutative'':
*}
-locale fun_left_comm =
+locale comp_fun_commute =
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
begin
lemma fun_left_comm: "f x (f y z) = f y (f x z)"
- using commute_comp by (simp add: fun_eq_iff)
+ using comp_fun_commute by (simp add: fun_eq_iff)
end
@@ -565,7 +565,7 @@
subsubsection{*From @{const fold_graph} to @{term fold}*}
-context fun_left_comm
+context comp_fun_commute
begin
lemma fold_graph_insertE_aux:
@@ -578,12 +578,12 @@
assume "x \<noteq> a"
then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
using insertI by auto
- have 1: "f x y = f a (f x y')"
+ have "f x y = f a (f x y')"
unfolding y by (rule fun_left_comm)
- have 2: "fold_graph f z (insert x A - {a}) (f x y')"
+ moreover have "fold_graph f z (insert x A - {a}) (f x y')"
using y' and `x \<noteq> a` and `x \<notin> A`
by (simp add: insert_Diff_if fold_graph.insertI)
- from 1 2 show ?case by fast
+ ultimately show ?case by fast
qed
qed simp
@@ -626,11 +626,12 @@
text{* The various recursion equations for @{const fold}: *}
lemma fold_insert [simp]:
- "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
-apply (rule fold_equality)
-apply (erule fold_graph.insertI)
-apply (erule fold_graph_fold)
-done
+ assumes "finite A" and "x \<notin> A"
+ shows "fold f z (insert x A) = f x (fold f z A)"
+proof (rule fold_equality)
+ from `finite A` have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold)
+ with `x \<notin> A`show "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI)
+qed
lemma fold_fun_comm:
"finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
@@ -646,8 +647,8 @@
by (simp add: fold_fun_comm)
lemma fold_rec:
-assumes "finite A" and "x \<in> A"
-shows "fold f z A = f x (fold f z (A - {x}))"
+ assumes "finite A" and "x \<in> A"
+ shows "fold f z A = f x (fold f z (A - {x}))"
proof -
have A: "A = insert x (A - {x})" using `x \<in> A` by blast
then have "fold f z A = fold f z (insert x (A - {x}))" by simp
@@ -671,13 +672,12 @@
text{* A simplified version for idempotent functions: *}
-locale fun_left_comm_idem = fun_left_comm +
- assumes fun_left_idem: "f x (f x z) = f x z"
+locale comp_fun_idem = comp_fun_commute +
+ assumes comp_fun_idem: "f x o f x = f x"
begin
-text{* The nice version: *}
-lemma fun_comp_idem : "f x o f x = f x"
-by (simp add: fun_left_idem fun_eq_iff)
+lemma fun_left_idem: "f x (f x z) = f x z"
+ using comp_fun_idem by (simp add: fun_eq_iff)
lemma fold_insert_idem:
assumes fin: "finite A"
@@ -701,33 +701,33 @@
subsubsection {* Expressing set operations via @{const fold} *}
-lemma (in fun_left_comm) fun_left_comm_apply:
- "fun_left_comm (\<lambda>x. f (g x))"
+lemma (in comp_fun_commute) comp_comp_fun_commute:
+ "comp_fun_commute (f \<circ> g)"
proof
-qed (simp_all add: commute_comp)
+qed (simp_all add: comp_fun_commute)
-lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
- "fun_left_comm_idem (\<lambda>x. f (g x))"
- by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
- (simp_all add: fun_left_idem)
+lemma (in comp_fun_idem) comp_comp_fun_idem:
+ "comp_fun_idem (f \<circ> g)"
+ by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
+ (simp_all add: comp_fun_idem)
-lemma fun_left_comm_idem_insert:
- "fun_left_comm_idem insert"
+lemma comp_fun_idem_insert:
+ "comp_fun_idem insert"
proof
qed auto
-lemma fun_left_comm_idem_remove:
- "fun_left_comm_idem (\<lambda>x A. A - {x})"
+lemma comp_fun_idem_remove:
+ "comp_fun_idem (\<lambda>x A. A - {x})"
proof
qed auto
-lemma (in semilattice_inf) fun_left_comm_idem_inf:
- "fun_left_comm_idem inf"
+lemma (in semilattice_inf) comp_fun_idem_inf:
+ "comp_fun_idem inf"
proof
qed (auto simp add: inf_left_commute)
-lemma (in semilattice_sup) fun_left_comm_idem_sup:
- "fun_left_comm_idem sup"
+lemma (in semilattice_sup) comp_fun_idem_sup:
+ "comp_fun_idem sup"
proof
qed (auto simp add: sup_left_commute)
@@ -735,7 +735,7 @@
assumes "finite A"
shows "A \<union> B = fold insert B A"
proof -
- interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
+ interpret comp_fun_idem insert by (fact comp_fun_idem_insert)
from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
qed
@@ -743,7 +743,7 @@
assumes "finite A"
shows "B - A = fold (\<lambda>x A. A - {x}) B A"
proof -
- interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+ interpret comp_fun_idem "\<lambda>x A. A - {x}" by (fact comp_fun_idem_remove)
from `finite A` show ?thesis by (induct A arbitrary: B) auto
qed
@@ -754,7 +754,7 @@
assumes "finite A"
shows "inf B (Inf A) = fold inf B A"
proof -
- interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+ interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
from `finite A` show ?thesis by (induct A arbitrary: B)
(simp_all add: Inf_insert inf_commute fold_fun_comm)
qed
@@ -763,7 +763,7 @@
assumes "finite A"
shows "sup B (Sup A) = fold sup B A"
proof -
- interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+ interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
from `finite A` show ?thesis by (induct A arbitrary: B)
(simp_all add: Sup_insert sup_commute fold_fun_comm)
qed
@@ -780,34 +780,34 @@
lemma inf_INFI_fold_inf:
assumes "finite A"
- shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold")
+ shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
proof (rule sym)
- interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
- interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
+ interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
+ interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?inf"
- by (induct A arbitrary: B)
- (simp_all add: INFI_def Inf_insert inf_left_commute)
+ by (induct A arbitrary: B)
+ (simp_all add: INFI_def Inf_insert inf_left_commute)
qed
lemma sup_SUPR_fold_sup:
assumes "finite A"
- shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold")
+ shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
proof (rule sym)
- interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
- interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
+ interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
+ interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?sup"
- by (induct A arbitrary: B)
- (simp_all add: SUPR_def Sup_insert sup_left_commute)
+ by (induct A arbitrary: B)
+ (simp_all add: SUPR_def Sup_insert sup_left_commute)
qed
lemma INFI_fold_inf:
assumes "finite A"
- shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
+ shows "INFI A f = fold (inf \<circ> f) top A"
using assms inf_INFI_fold_inf [of A top] by simp
lemma SUPR_fold_sup:
assumes "finite A"
- shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
+ shows "SUPR A f = fold (sup \<circ> f) bot A"
using assms sup_SUPR_fold_sup [of A bot] by simp
end
@@ -816,84 +816,49 @@
subsection {* The derived combinator @{text fold_image} *}
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
-where "fold_image f g = fold (%x y. f (g x) y)"
+ where "fold_image f g = fold (\<lambda>x y. f (g x) y)"
lemma fold_image_empty[simp]: "fold_image f g z {} = z"
-by(simp add:fold_image_def)
+ by (simp add:fold_image_def)
context ab_semigroup_mult
begin
lemma fold_image_insert[simp]:
-assumes "finite A" and "a \<notin> A"
-shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
+ assumes "finite A" and "a \<notin> A"
+ shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
proof -
- interpret I: fun_left_comm "%x y. (g x) * y" proof
+ interpret comp_fun_commute "%x y. (g x) * y" proof
qed (simp add: fun_eq_iff mult_ac)
show ?thesis using assms by (simp add: fold_image_def)
qed
-(*
-lemma fold_commute:
- "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
- apply (induct set: finite)
- apply simp
- apply (simp add: mult_left_commute [of x])
- done
-
-lemma fold_nest_Un_Int:
- "finite A ==> finite B
- ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
- apply (induct set: finite)
- apply simp
- apply (simp add: fold_commute Int_insert_left insert_absorb)
- done
-
-lemma fold_nest_Un_disjoint:
- "finite A ==> finite B ==> A Int B = {}
- ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
- by (simp add: fold_nest_Un_Int)
-*)
-
lemma fold_image_reindex:
-assumes fin: "finite A"
-shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
-using fin by induct auto
-
-(*
-text{*
- Fusion theorem, as described in Graham Hutton's paper,
- A Tutorial on the Universality and Expressiveness of Fold,
- JFP 9:4 (355-372), 1999.
-*}
-
-lemma fold_fusion:
- assumes "ab_semigroup_mult g"
- assumes fin: "finite A"
- and hyp: "\<And>x y. h (g x y) = times x (h y)"
- shows "h (fold g j w A) = fold times j (h w) A"
-proof -
- class_interpret ab_semigroup_mult [g] by fact
- show ?thesis using fin hyp by (induct set: finite) simp_all
-qed
-*)
+ assumes "finite A"
+ shows "inj_on h A \<Longrightarrow> fold_image times g z (h ` A) = fold_image times (g \<circ> h) z A"
+ using assms by induct auto
lemma fold_image_cong:
- "finite A \<Longrightarrow>
- (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
-apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C")
- apply simp
-apply (erule finite_induct, simp)
-apply (simp add: subset_insert_iff, clarify)
-apply (subgoal_tac "finite C")
- prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
-apply (subgoal_tac "C = insert x (C - {x})")
- prefer 2 apply blast
-apply (erule ssubst)
-apply (drule spec)
-apply (erule (1) notE impE)
-apply (simp add: Ball_def del: insert_Diff_single)
-done
+ assumes "finite A" and g_h: "\<And>x. x\<in>A \<Longrightarrow> g x = h x"
+ shows "fold_image times g z A = fold_image times h z A"
+proof -
+ from `finite A`
+ have "\<And>C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C"
+ proof (induct arbitrary: C)
+ case empty then show ?case by simp
+ next
+ case (insert x F) then show ?case apply -
+ apply (simp add: subset_insert_iff, clarify)
+ apply (subgoal_tac "finite C")
+ prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+ apply (subgoal_tac "C = insert x (C - {x})")
+ prefer 2 apply blast
+ apply (erule ssubst)
+ apply (simp add: Ball_def del: insert_Diff_single)
+ done
+ qed
+ with g_h show ?thesis by simp
+qed
end
@@ -1051,14 +1016,14 @@
context ab_semigroup_mult
begin
-lemma fun_left_comm: "fun_left_comm (op *)" proof
+lemma comp_fun_commute: "comp_fun_commute (op *)" proof
qed (simp add: fun_eq_iff mult_ac)
lemma fold_graph_insert_swap:
assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
shows "fold_graph times z (insert b A) (z * y)"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
from assms show ?thesis
proof (induct rule: fold_graph.induct)
case emptyI show ?case by (subst mult_commute [of z b], fast)
@@ -1098,7 +1063,7 @@
lemma fold1_eq_fold:
assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
from assms show ?thesis
apply (simp add: fold1_def fold_def)
apply (rule the_equality)
@@ -1125,7 +1090,7 @@
assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
from nonempty obtain a A' where "A = insert a A' & a ~: A'"
by (auto simp add: nonempty_iff)
with A show ?thesis
@@ -1137,15 +1102,15 @@
context ab_semigroup_idem_mult
begin
-lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
-qed (simp add: fun_eq_iff mult_left_commute, rule mult_left_idem)
+lemma comp_fun_idem: "comp_fun_idem (op *)" proof
+qed (simp_all add: fun_eq_iff mult_left_commute)
lemma fold1_insert_idem [simp]:
assumes nonempty: "A \<noteq> {}" and A: "finite A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (rule fun_left_comm_idem)
+ interpret comp_fun_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (rule comp_fun_idem)
from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
by (auto simp add: nonempty_iff)
show ?thesis
@@ -1190,7 +1155,7 @@
case False
with assms show ?thesis by (simp add: fold1_eq_fold)
next
- interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+ interpret comp_fun_idem times by (fact comp_fun_idem)
case True then obtain b B
where A: "A = insert a B" and "a \<notin> B" by (rule set_insert)
with assms have "finite B" by auto
@@ -1314,7 +1279,7 @@
locale folding =
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A"
begin
@@ -1326,8 +1291,8 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = F A \<circ> f x"
proof -
- interpret fun_left_comm f proof
- qed (insert commute_comp, simp add: fun_eq_iff)
+ interpret comp_fun_commute f proof
+ qed (insert comp_fun_commute, simp add: fun_eq_iff)
from fold_insert2 assms
have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
@@ -1350,38 +1315,38 @@
lemma commute_left_comp:
"f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
- by (simp add: o_assoc commute_comp)
+ by (simp add: o_assoc comp_fun_commute)
-lemma commute_comp':
+lemma comp_fun_commute':
assumes "finite A"
shows "f x \<circ> F A = F A \<circ> f x"
using assms by (induct A)
- (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] commute_comp)
+ (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
lemma commute_left_comp':
assumes "finite A"
shows "f x \<circ> (F A \<circ> g) = F A \<circ> (f x \<circ> g)"
- using assms by (simp add: o_assoc commute_comp')
+ using assms by (simp add: o_assoc comp_fun_commute')
-lemma commute_comp'':
+lemma comp_fun_commute'':
assumes "finite A" and "finite B"
shows "F B \<circ> F A = F A \<circ> F B"
using assms by (induct A)
- (simp_all add: o_assoc, simp add: o_assoc [symmetric] commute_comp')
+ (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
lemma commute_left_comp'':
assumes "finite A" and "finite B"
shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
- using assms by (simp add: o_assoc commute_comp'')
+ using assms by (simp add: o_assoc comp_fun_commute'')
-lemmas commute_comps = o_assoc [symmetric] commute_comp commute_left_comp
- commute_comp' commute_left_comp' commute_comp'' commute_left_comp''
+lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
+ comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
lemma union_inter:
assumes "finite A" and "finite B"
shows "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B"
using assms by (induct A)
- (simp_all del: o_apply add: insert_absorb Int_insert_left commute_comps,
+ (simp_all del: o_apply add: insert_absorb Int_insert_left comp_fun_commutes,
simp add: o_assoc)
lemma union:
@@ -1410,7 +1375,7 @@
assumes "finite A" and "x \<in> A"
shows "F A \<circ> f x = F A"
using assms by (induct A)
- (auto simp add: commute_comps idem_comp, simp add: commute_left_comp' [symmetric] commute_comp')
+ (auto simp add: comp_fun_commutes idem_comp, simp add: commute_left_comp' [symmetric] comp_fun_commute')
lemma subset_comp_idem:
assumes "finite A" and "B \<subseteq> A"
@@ -1459,7 +1424,7 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = g x * F A"
proof -
- interpret fun_left_comm "%x y. (g x) * y" proof
+ interpret comp_fun_commute "%x y. (g x) * y" proof
qed (simp add: ac_simps fun_eq_iff)
with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
by (simp add: fold_image_def)
@@ -1696,8 +1661,8 @@
with `finite A` have "finite B" by simp
interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
qed (simp_all add: fun_eq_iff ac_simps)
- thm fold.commute_comp' [of B b, simplified fun_eq_iff, simplified]
- from `finite B` fold.commute_comp' [of B x]
+ thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified]
+ from `finite B` fold.comp_fun_commute' [of B x]
have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)
from `finite B` * fold.insert [of B b]
--- a/src/HOL/GCD.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/GCD.thy Fri May 20 14:12:59 2011 +0200
@@ -1436,16 +1436,16 @@
lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
-lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
proof qed (auto simp add: gcd_ac_nat)
-lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
+lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
proof qed (auto simp add: gcd_ac_int)
-lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
proof qed (auto simp add: lcm_ac_nat)
-lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
+lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
proof qed (auto simp add: lcm_ac_int)
@@ -1516,8 +1516,8 @@
assumes "finite N"
shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
proof -
- interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
- by (rule fun_left_comm_idem_lcm_nat)
+ interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
+ by (rule comp_fun_idem_lcm_nat)
from assms show ?thesis by(simp add: Lcm_def)
qed
@@ -1525,8 +1525,8 @@
assumes "finite N"
shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
proof -
- interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
- by (rule fun_left_comm_idem_lcm_int)
+ interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
+ by (rule comp_fun_idem_lcm_int)
from assms show ?thesis by(simp add: Lcm_def)
qed
@@ -1534,8 +1534,8 @@
assumes "finite N"
shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
proof -
- interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
- by (rule fun_left_comm_idem_gcd_nat)
+ interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
+ by (rule comp_fun_idem_gcd_nat)
from assms show ?thesis by(simp add: Gcd_def)
qed
@@ -1543,8 +1543,8 @@
assumes "finite N"
shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
proof -
- interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
- by (rule fun_left_comm_idem_gcd_int)
+ interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
+ by (rule comp_fun_idem_gcd_int)
from assms show ?thesis by(simp add: Gcd_def)
qed
@@ -1685,28 +1685,28 @@
lemma Lcm_set_nat [code_unfold]:
"Lcm (set ns) = foldl lcm (1::nat) ns"
proof -
- interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
+ interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_lcm_nat)
show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
qed
lemma Lcm_set_int [code_unfold]:
"Lcm (set is) = foldl lcm (1::int) is"
proof -
- interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
+ interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_lcm_int)
show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
qed
lemma Gcd_set_nat [code_unfold]:
"Gcd (set ns) = foldl gcd (0::nat) ns"
proof -
- interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
+ interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_gcd_nat)
show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
qed
lemma Gcd_set_int [code_unfold]:
"Gcd (set ns) = foldl gcd (0::int) ns"
proof -
- interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
+ interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_gcd_int)
show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
qed
--- a/src/HOL/IsaMakefile Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/IsaMakefile Fri May 20 14:12:59 2011 +0200
@@ -437,7 +437,7 @@
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
- Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy \
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
@@ -1193,6 +1193,7 @@
Probability/ex/Dining_Cryptographers.thy \
Probability/ex/Koepf_Duermuth_Countermeasure.thy \
Probability/Finite_Product_Measure.thy \
+ Probability/Independent_Family.thy \
Probability/Infinite_Product_Measure.thy Probability/Information.thy \
Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
Probability/Measure.thy Probability/Probability_Measure.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Char_ord.thy Fri May 20 14:12:59 2011 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/Library/Code_Char_ord.thy
+ Author: Lukas Bulwahn, Florian Haftmann, Rene Thiemann
+*)
+
+header {* Code generation of orderings for pretty characters *}
+
+theory Code_Char_ord
+imports Code_Char Char_ord
+begin
+
+code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (SML "!((_ : char) <= _)")
+ (OCaml "!((_ : char) <= _)")
+ (Haskell infix 4 "<=")
+ (Scala infixl 4 "<=")
+ (Eval infixl 6 "<=")
+
+code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (SML "!((_ : char) < _)")
+ (OCaml "!((_ : char) < _)")
+ (Haskell infix 4 "<")
+ (Scala infixl 4 "<")
+ (Eval infixl 6 "<")
+
+end
\ No newline at end of file
--- a/src/HOL/Library/More_List.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Library/More_List.thy Fri May 20 14:12:59 2011 +0200
@@ -158,11 +158,11 @@
text {* @{const Finite_Set.fold} and @{const fold} *}
-lemma (in fun_left_comm) fold_set_remdups:
+lemma (in comp_fun_commute) fold_set_remdups:
"Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
-lemma (in fun_left_comm_idem) fold_set:
+lemma (in comp_fun_idem) fold_set:
"Finite_Set.fold f y (set xs) = fold f xs y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
@@ -170,7 +170,7 @@
assumes "xs \<noteq> []"
shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
proof -
- interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+ interpret comp_fun_idem times by (fact comp_fun_idem)
from assms obtain y ys where xs: "xs = y # ys"
by (cases xs) auto
show ?thesis
@@ -239,8 +239,8 @@
lemma (in complete_lattice) Inf_set_fold:
"Inf (set xs) = fold inf xs top"
proof -
- interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_inf)
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_inf)
show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
qed
@@ -251,8 +251,8 @@
lemma (in complete_lattice) Sup_set_fold:
"Sup (set xs) = fold sup xs bot"
proof -
- interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_sup)
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_sup)
show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
qed
--- a/src/HOL/Library/More_Set.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Library/More_Set.thy Fri May 20 14:12:59 2011 +0200
@@ -15,11 +15,11 @@
definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
"remove x A = A - {x}"
-lemma fun_left_comm_idem_remove:
- "fun_left_comm_idem remove"
+lemma comp_fun_idem_remove:
+ "comp_fun_idem remove"
proof -
have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
- show ?thesis by (simp only: fun_left_comm_idem_remove rem)
+ show ?thesis by (simp only: comp_fun_idem_remove rem)
qed
lemma minus_fold_remove:
@@ -66,8 +66,8 @@
lemma union_set:
"set xs \<union> A = fold Set.insert xs A"
proof -
- interpret fun_left_comm_idem Set.insert
- by (fact fun_left_comm_idem_insert)
+ interpret comp_fun_idem Set.insert
+ by (fact comp_fun_idem_insert)
show ?thesis by (simp add: union_fold_insert fold_set)
qed
@@ -82,8 +82,8 @@
lemma minus_set:
"A - set xs = fold remove xs A"
proof -
- interpret fun_left_comm_idem remove
- by (fact fun_left_comm_idem_remove)
+ interpret comp_fun_idem remove
+ by (fact comp_fun_idem_remove)
show ?thesis
by (simp add: minus_fold_remove [of _ A] fold_set)
qed
@@ -124,6 +124,6 @@
lemma not_set_compl:
"Not \<circ> set xs = - set xs"
- by (simp add: fun_Compl_def bool_Compl_def comp_def fun_eq_iff)
+ by (simp add: fun_Compl_def comp_def fun_eq_iff)
end
--- a/src/HOL/Library/Multiset.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Library/Multiset.thy Fri May 20 14:12:59 2011 +0200
@@ -1457,7 +1457,7 @@
lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
unfolding fold_mset_def by blast
-context fun_left_comm
+context comp_fun_commute
begin
lemma fold_msetG_determ:
@@ -1563,10 +1563,10 @@
qed
lemma fold_mset_fusion:
- assumes "fun_left_comm g"
+ assumes "comp_fun_commute g"
shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
proof -
- interpret fun_left_comm g by (fact assms)
+ interpret comp_fun_commute g by (fact assms)
show "PROP ?P" by (induct A) auto
qed
@@ -1598,7 +1598,7 @@
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
"image_mset f = fold_mset (op + o single o f) {#}"
-interpretation image_left_comm: fun_left_comm "op + o single o f"
+interpretation image_fun_commute: comp_fun_commute "op + o single o f"
proof qed (simp add: add_ac fun_eq_iff)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
--- a/src/HOL/Library/ROOT.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Library/ROOT.ML Fri May 20 14:12:59 2011 +0200
@@ -2,4 +2,4 @@
(* Classical Higher-order Logic -- batteries included *)
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
+ "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
--- a/src/HOL/List.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/List.thy Fri May 20 14:12:59 2011 +0200
@@ -2478,11 +2478,11 @@
text {* @{const Finite_Set.fold} and @{const foldl} *}
-lemma (in fun_left_comm) fold_set_remdups:
+lemma (in comp_fun_commute) fold_set_remdups:
"fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
-lemma (in fun_left_comm_idem) fold_set:
+lemma (in comp_fun_idem) fold_set:
"fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
@@ -2490,7 +2490,7 @@
assumes "xs \<noteq> []"
shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
proof -
- interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+ interpret comp_fun_idem times by (fact comp_fun_idem)
from assms obtain y ys where xs: "xs = y # ys"
by (cases xs) auto
show ?thesis
@@ -2543,16 +2543,16 @@
lemma (in complete_lattice) Inf_set_fold [code_unfold]:
"Inf (set xs) = foldl inf top xs"
proof -
- interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_inf)
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_inf)
show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
qed
lemma (in complete_lattice) Sup_set_fold [code_unfold]:
"Sup (set xs) = foldl sup bot xs"
proof -
- interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_sup)
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_sup)
show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
qed
@@ -3762,8 +3762,8 @@
"insort x (insort y xs) = insort y (insort x xs)"
by (cases "x = y") (auto intro: insort_key_left_comm)
-lemma fun_left_comm_insort:
- "fun_left_comm insort"
+lemma comp_fun_commute_insort:
+ "comp_fun_commute insort"
proof
qed (simp add: insort_left_comm fun_eq_iff)
@@ -4249,7 +4249,7 @@
assumes "finite A"
shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
proof -
- interpret fun_left_comm insort by (fact fun_left_comm_insort)
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
qed
@@ -4261,7 +4261,7 @@
lemma sorted_list_of_set_sort_remdups:
"sorted_list_of_set (set xs) = sort (remdups xs)"
proof -
- interpret fun_left_comm insort by (fact fun_left_comm_insort)
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
qed
--- a/src/HOL/Metis_Examples/HO_Reas.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy Fri May 20 14:12:59 2011 +0200
@@ -56,50 +56,60 @@
lemma "id (op =) x x"
sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id True"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "\<not> id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "x = id True \<or> x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id x = id True \<or> id x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
@@ -107,120 +117,144 @@
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [type_sys = erased, expect = none] ()
sledgehammer [type_sys = poly_args, expect = none] ()
-sledgehammer [type_sys = poly_tags!, expect = some] ()
+sledgehammer [type_sys = poly_tags?, expect = some] ()
sledgehammer [type_sys = poly_tags, expect = some] ()
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_preds!, expect = some] ()
+sledgehammer [type_sys = mangled_tags?, expect = some] ()
+sledgehammer [type_sys = mangled_tags, expect = some] ()
sledgehammer [type_sys = mangled_preds?, expect = some] ()
sledgehammer [type_sys = mangled_preds, expect = some] ()
by metisFT
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
by (metis id_apply)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 14:12:59 2011 +0200
@@ -1826,8 +1826,8 @@
lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
-lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp"
- unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto
+lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp"
+ unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto
lemma support_clauses:
"\<And>f g s. support opp f {} = {}"
@@ -1850,12 +1850,12 @@
proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
show ?thesis unfolding iterate_def if_P[OF True] * by auto
next case False note x=this
- note * = fun_left_comm.fun_left_comm_apply[OF fun_left_comm_monoidal[OF assms(1)]]
+ note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
show ?thesis proof(cases "f x = neutral opp")
case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
unfolding True monoidal_simps[OF assms(1)] by auto
next case False show ?thesis unfolding iterate_def fold'_def if_not_P[OF x] support_clauses if_not_P[OF False]
- apply(subst fun_left_comm.fold_insert[OF * finite_support])
+ apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
using `finite s` unfolding support_def using False x by auto qed qed
lemma iterate_some:
--- a/src/HOL/Nat_Transfer.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Nat_Transfer.thy Fri May 20 14:12:59 2011 +0200
@@ -11,12 +11,10 @@
subsection {* Generic transfer machinery *}
definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
- where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
+ where "transfer_morphism f A \<longleftrightarrow> True"
-lemma transfer_morphismI:
- assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
- shows "transfer_morphism f A"
- using assms by (auto simp add: transfer_morphism_def)
+lemma transfer_morphismI[intro]: "transfer_morphism f A"
+ by (simp add: transfer_morphism_def)
use "Tools/transfer.ML"
@@ -27,8 +25,7 @@
text {* set up transfer direction *}
-lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
- by (rule transfer_morphismI) simp
+lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
declare transfer_morphism_nat_int [transfer add
mode: manual
@@ -266,8 +263,7 @@
text {* set up transfer direction *}
-lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
-by (rule transfer_morphismI) simp
+lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
declare transfer_morphism_int_nat [transfer add
mode: manual
--- a/src/HOL/Probability/Borel_Space.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Fri May 20 14:12:59 2011 +0200
@@ -658,6 +658,26 @@
qed
qed auto
+lemma borel_eq_atLeastLessThan:
+ "borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S")
+proof (intro algebra.equality antisym)
+ interpret sigma_algebra ?S
+ by (rule sigma_algebra_sigma) auto
+ show "sets borel \<subseteq> sets ?S"
+ unfolding borel_eq_lessThan
+ proof (intro sets_sigma_subset subsetI)
+ have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto
+ fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>"
+ then obtain x where "A = {..< x}" by auto
+ then have "A = (\<Union>i::nat. {-real i ..< x})"
+ by (auto simp: move_uminus real_arch_simple)
+ then show "A \<in> sets ?S"
+ by (auto simp: sets_sigma intro!: sigma_sets.intros)
+ qed simp
+ show "sets ?S \<subseteq> sets borel"
+ by (intro borel.sets_sigma_subset) auto
+qed simp_all
+
lemma borel_eq_halfspace_le:
"borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
(is "_ = ?SIGMA")
--- a/src/HOL/Probability/Complete_Measure.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Complete_Measure.thy Fri May 20 14:12:59 2011 +0200
@@ -144,7 +144,7 @@
have "(\<Union>i. S i) \<in> sets completion" using S by auto
from null_part[OF this] guess N' .. note N' = this
let ?N = "(\<Union>i. N i) \<union> N'"
- have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
+ have null_set: "?N \<in> null_sets" using N' UN_N by (intro nullsets.Un) auto
have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
using N' by auto
also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
@@ -212,7 +212,7 @@
from choice[OF this] obtain N where
N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
- have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
+ have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
show ?thesis unfolding simple_function_def
proof (safe intro!: exI[of _ ?f'])
have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Independent_Family.thy Fri May 20 14:12:59 2011 +0200
@@ -0,0 +1,312 @@
+(* Title: HOL/Probability/Independent_Family.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {* Independent families of events, event sets, and random variables *}
+
+theory Independent_Family
+ imports Probability_Measure
+begin
+
+definition (in prob_space)
+ "indep_events A I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
+
+definition (in prob_space)
+ "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow>
+ (\<forall>A\<in>(\<Pi> j\<in>J. F j). prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
+
+definition (in prob_space)
+ "indep_sets2 A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
+
+definition (in prob_space)
+ "indep_rv M' X I \<longleftrightarrow>
+ (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
+ indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
+
+lemma (in prob_space) indep_sets_finite_index_sets:
+ "indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)"
+proof (intro iffI allI impI)
+ assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J"
+ show "indep_sets F I" unfolding indep_sets_def
+ proof (intro conjI ballI allI impI)
+ fix i assume "i \<in> I"
+ with *[THEN spec, of "{i}"] show "F i \<subseteq> events"
+ by (auto simp: indep_sets_def)
+ qed (insert *, auto simp: indep_sets_def)
+qed (auto simp: indep_sets_def)
+
+lemma (in prob_space) indep_sets_mono_index:
+ "J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J"
+ unfolding indep_sets_def by auto
+
+lemma (in prob_space) indep_sets_mono_sets:
+ assumes indep: "indep_sets F I"
+ assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i"
+ shows "indep_sets G I"
+proof -
+ have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)"
+ using mono by auto
+ moreover have "\<And>A J. J \<subseteq> I \<Longrightarrow> A \<in> (\<Pi> j\<in>J. G j) \<Longrightarrow> A \<in> (\<Pi> j\<in>J. F j)"
+ using mono by (auto simp: Pi_iff)
+ ultimately show ?thesis
+ using indep by (auto simp: indep_sets_def)
+qed
+
+lemma (in prob_space) indep_setsI:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events"
+ and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
+ shows "indep_sets F I"
+ using assms unfolding indep_sets_def by (auto simp: Pi_iff)
+
+lemma (in prob_space) indep_setsD:
+ assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j"
+ shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
+ using assms unfolding indep_sets_def by auto
+
+lemma dynkin_systemI':
+ assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
+ assumes empty: "{} \<in> sets M"
+ assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
+ assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
+ \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+ shows "dynkin_system M"
+proof -
+ from Diff[OF empty] have "space M \<in> sets M" by auto
+ from 1 this Diff 2 show ?thesis
+ by (intro dynkin_systemI) auto
+qed
+
+lemma (in prob_space) indep_sets_dynkin:
+ assumes indep: "indep_sets F I"
+ shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
+ (is "indep_sets ?F I")
+proof (subst indep_sets_finite_index_sets, intro allI impI ballI)
+ fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}"
+ with indep have "indep_sets F J"
+ by (subst (asm) indep_sets_finite_index_sets) auto
+ { fix J K assume "indep_sets F K"
+ let "?G S i" = "if i \<in> S then ?F i else F i"
+ assume "finite J" "J \<subseteq> K"
+ then have "indep_sets (?G J) K"
+ proof induct
+ case (insert j J)
+ moreover def G \<equiv> "?G J"
+ ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K"
+ by (auto simp: indep_sets_def)
+ let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }"
+ { fix X assume X: "X \<in> events"
+ assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i)
+ \<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))"
+ have "indep_sets (G(j := {X})) K"
+ proof (rule indep_setsI)
+ fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events"
+ using G X by auto
+ next
+ fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i"
+ show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
+ proof cases
+ assume "j \<in> J"
+ with J have "A j = X" by auto
+ show ?thesis
+ proof cases
+ assume "J = {j}" then show ?thesis by simp
+ next
+ assume "J \<noteq> {j}"
+ have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
+ using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
+ proof (rule indep)
+ show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
+ using J `J \<noteq> {j}` `j \<in> J` by auto
+ show "\<forall>i\<in>J - {j}. A i \<in> G i"
+ using J by auto
+ qed
+ also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
+ using `A j = X` by simp
+ also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
+ unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob (A i)"]
+ using `j \<in> J` by (simp add: insert_absorb)
+ finally show ?thesis .
+ qed
+ next
+ assume "j \<notin> J"
+ with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
+ with J show ?thesis
+ by (intro indep_setsD[OF G(1)]) auto
+ qed
+ qed }
+ note indep_sets_insert = this
+ have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>"
+ proof (rule dynkin_systemI', simp_all, safe)
+ show "indep_sets (G(j := {{}})) K"
+ by (rule indep_sets_insert) auto
+ next
+ fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K"
+ show "indep_sets (G(j := {space M - X})) K"
+ proof (rule indep_sets_insert)
+ fix J A assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "j \<notin> J" and A: "\<forall>i\<in>J. A i \<in> G i"
+ then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
+ using G by auto
+ have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
+ prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
+ using A_sets sets_into_space X `J \<noteq> {}`
+ by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
+ using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
+ by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
+ finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
+ prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
+ moreover {
+ have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
+ using J A `finite J` by (intro indep_setsD[OF G(1)]) auto
+ then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))"
+ using prob_space by simp }
+ moreover {
+ have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
+ using J A `j \<in> K` by (intro indep_setsD[OF G']) auto
+ then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
+ using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) }
+ ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
+ by (simp add: field_simps)
+ also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
+ using X A by (simp add: finite_measure_compl)
+ finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" .
+ qed (insert X, auto)
+ next
+ fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D"
+ then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto
+ show "indep_sets (G(j := {\<Union>k. F k})) K"
+ proof (rule indep_sets_insert)
+ fix J A assume J: "j \<notin> J" "J \<noteq> {}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> G i"
+ then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
+ using G by auto
+ have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
+ using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
+ proof (rule finite_measure_UNION)
+ show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
+ using disj by (rule disjoint_family_on_bisimulation) auto
+ show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
+ using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
+ qed
+ moreover { fix k
+ from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
+ by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm)
+ also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
+ using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto
+ finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
+ ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))"
+ by simp
+ moreover
+ have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))"
+ using disj F(1) by (intro finite_measure_UNION sums_mult2) auto
+ then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))"
+ using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto
+ ultimately
+ show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
+ by (auto dest!: sums_unique)
+ qed (insert F, auto)
+ qed (insert sets_into_space, auto)
+ then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq>
+ sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>"
+ proof (rule dynkin_system.dynkin_subset, simp_all, safe)
+ fix X assume "X \<in> G j"
+ then show "X \<in> events" using G `j \<in> K` by auto
+ from `indep_sets G K`
+ show "indep_sets (G(j := {X})) K"
+ by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto)
+ qed
+ have "indep_sets (G(j:=?D)) K"
+ proof (rule indep_setsI)
+ fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events"
+ using G(2) by auto
+ next
+ fix A J assume J: "J\<noteq>{}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> (G(j := ?D)) i"
+ show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
+ proof cases
+ assume "j \<in> J"
+ with A have indep: "indep_sets (G(j := {A j})) K" by auto
+ from J A show ?thesis
+ by (intro indep_setsD[OF indep]) auto
+ next
+ assume "j \<notin> J"
+ with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
+ with J show ?thesis
+ by (intro indep_setsD[OF G(1)]) auto
+ qed
+ qed
+ then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K"
+ by (rule indep_sets_mono_sets) (insert mono, auto)
+ then show ?case
+ by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def)
+ qed (insert `indep_sets F K`, simp) }
+ from this[OF `indep_sets F J` `finite J` subset_refl]
+ show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J"
+ by (rule indep_sets_mono_sets) auto
+qed
+
+lemma (in prob_space) indep_sets_sigma:
+ assumes indep: "indep_sets F I"
+ assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
+ shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I"
+proof -
+ from indep_sets_dynkin[OF indep]
+ show ?thesis
+ proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
+ fix i assume "i \<in> I"
+ with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
+ with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
+ qed
+qed
+
+lemma (in prob_space) indep_sets_sigma_sets:
+ assumes "indep_sets F I"
+ assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
+ shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
+ using indep_sets_sigma[OF assms] by (simp add: sets_sigma)
+
+lemma (in prob_space) indep_sets2_eq:
+ "indep_sets2 A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
+ unfolding indep_sets2_def
+proof (intro iffI ballI conjI)
+ assume indep: "indep_sets (bool_case A B) UNIV"
+ { fix a b assume "a \<in> A" "b \<in> B"
+ with indep_setsD[OF indep, of UNIV "bool_case a b"]
+ show "prob (a \<inter> b) = prob a * prob b"
+ unfolding UNIV_bool by (simp add: ac_simps) }
+ from indep show "A \<subseteq> events" "B \<subseteq> events"
+ unfolding indep_sets_def UNIV_bool by auto
+next
+ assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
+ show "indep_sets (bool_case A B) UNIV"
+ proof (rule indep_setsI)
+ fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
+ using * by (auto split: bool.split)
+ next
+ fix J X assume "J \<noteq> {}" "J \<subseteq> UNIV" and X: "\<forall>j\<in>J. X j \<in> (case j of True \<Rightarrow> A | False \<Rightarrow> B)"
+ then have "J = {True} \<or> J = {False} \<or> J = {True,False}"
+ by (auto simp: UNIV_bool)
+ then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))"
+ using X * by auto
+ qed
+qed
+
+lemma (in prob_space) indep_sets2_sigma_sets:
+ assumes "indep_sets2 A B"
+ assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>"
+ assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>"
+ shows "indep_sets2 (sigma_sets (space M) A) (sigma_sets (space M) B)"
+proof -
+ have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
+ proof (rule indep_sets_sigma_sets)
+ show "indep_sets (bool_case A B) UNIV"
+ by (rule `indep_sets2 A B`[unfolded indep_sets2_def])
+ fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A | False \<Rightarrow> B\<rparr>"
+ using A B by (cases i) auto
+ qed
+ then show ?thesis
+ unfolding indep_sets2_def
+ by (rule indep_sets_mono_sets) (auto split: bool.split)
+qed
+
+end
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri May 20 14:12:59 2011 +0200
@@ -917,8 +917,9 @@
with i show "A \<in> sigma_sets ?O ?G"
by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
qed
- finally show "sets (Pi\<^isub>P I M) = sets ?S"
+ also have "\<dots> = sets ?S"
by (simp add: sets_sigma)
+ finally show "sets (Pi\<^isub>P I M) = sets ?S" .
qed simp_all
lemma (in product_prob_space) measurable_into_infprod_algebra:
@@ -941,6 +942,57 @@
(auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def)
qed
+lemma (in product_prob_space) measurable_singleton_infprod:
+ assumes "i \<in> I"
+ shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "(\<lambda>x. x i) \<in> space (Pi\<^isub>P I M) \<rightarrow> space (M i)"
+ using M.sets_into_space `i \<in> I`
+ by (auto simp: infprod_algebra_def generator_def)
+ fix A assume "A \<in> sets (M i)"
+ have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) = emb I {i} (\<Pi>\<^isub>E _\<in>{i}. A)"
+ by (auto simp: infprod_algebra_def generator_def emb_def)
+ also have "\<dots> \<in> sets (Pi\<^isub>P I M)"
+ using `i \<in> I` `A \<in> sets (M i)`
+ by (intro emb_in_infprod_algebra product_algebraI) auto
+ finally show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)" .
+qed
+
+lemma (in product_prob_space) sigma_product_algebra_sigma_eq:
+ assumes M: "\<And>i. i \<in> I \<Longrightarrow> M i = sigma (E i)"
+ shows "sets (Pi\<^isub>P I M) = sigma_sets (space (Pi\<^isub>P I M)) (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (E i))"
+proof -
+ let ?E = "(\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (E i))"
+ let ?M = "(\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i))"
+ { fix i A assume "i\<in>I" "A \<in> sets (E i)"
+ then have "A \<in> sets (M i)" using M by auto
+ then have "A \<in> Pow (space (M i))" using M.sets_into_space by auto
+ then have "A \<in> Pow (space (E i))" using M[OF `i \<in> I`] by auto }
+ moreover
+ have "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) \<in> space infprod_algebra \<rightarrow> space (E i)"
+ by (auto simp: M infprod_algebra_def generator_def Pi_iff)
+ ultimately have "sigma_sets (space (Pi\<^isub>P I M)) ?M \<subseteq> sigma_sets (space (Pi\<^isub>P I M)) ?E"
+ apply (intro sigma_sets_mono UN_least)
+ apply (simp add: sets_sigma M)
+ apply (subst sigma_sets_vimage[symmetric])
+ apply (auto intro!: sigma_sets_mono')
+ done
+ moreover have "sigma_sets (space (Pi\<^isub>P I M)) ?E \<subseteq> sigma_sets (space (Pi\<^isub>P I M)) ?M"
+ by (intro sigma_sets_mono') (auto simp: M)
+ ultimately show ?thesis
+ by (subst infprod_algebra_alt2) (auto simp: sets_sigma)
+qed
+
+lemma (in product_prob_space) Int_proj_eq_emb:
+ assumes "J \<noteq> {}" "J \<subseteq> I"
+ shows "(\<Inter>i\<in>J. (\<lambda>x. x i) -` A i \<inter> space (Pi\<^isub>P I M)) = emb I J (Pi\<^isub>E J A)"
+ using assms by (auto simp: infprod_algebra_def generator_def emb_def Pi_iff)
+
+lemma (in product_prob_space) emb_insert:
+ "i \<notin> J \<Longrightarrow> emb I J (Pi\<^isub>E J f) \<inter> ((\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) =
+ emb I (insert i J) (Pi\<^isub>E (insert i J) (f(i := A)))"
+ by (auto simp: emb_def Pi_iff infprod_algebra_def generator_def split: split_if_asm)
+
subsection {* Sequence space *}
locale sequence_space = product_prob_space M "UNIV :: nat set" for M
--- a/src/HOL/Probability/Measure.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Measure.thy Fri May 20 14:12:59 2011 +0200
@@ -552,16 +552,20 @@
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
-lemma (in measure_space) null_sets_Un[intro]:
- assumes "N \<in> null_sets" "N' \<in> null_sets"
- shows "N \<union> N' \<in> null_sets"
-proof (intro conjI CollectI)
- show "N \<union> N' \<in> sets M" using assms by auto
- then have "0 \<le> \<mu> (N \<union> N')" by simp
- moreover have "\<mu> (N \<union> N') \<le> \<mu> N + \<mu> N'"
- using assms by (intro measure_subadditive) auto
- ultimately show "\<mu> (N \<union> N') = 0" using assms by auto
-qed
+sublocale measure_space \<subseteq> nullsets!: ring_of_sets "\<lparr> space = space M, sets = null_sets \<rparr>"
+ where "space \<lparr> space = space M, sets = null_sets \<rparr> = space M"
+ and "sets \<lparr> space = space M, sets = null_sets \<rparr> = null_sets"
+proof -
+ { fix A B assume sets: "A \<in> sets M" "B \<in> sets M"
+ moreover then have "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B" "\<mu> (A - B) \<le> \<mu> A"
+ by (auto intro!: measure_subadditive measure_mono)
+ moreover assume "\<mu> B = 0" "\<mu> A = 0"
+ ultimately have "\<mu> (A - B) = 0" "\<mu> (A \<union> B) = 0"
+ by (auto intro!: antisym) }
+ note null = this
+ show "ring_of_sets \<lparr> space = space M, sets = null_sets \<rparr>"
+ by default (insert sets_into_space null, auto)
+qed simp_all
lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
proof -
@@ -583,17 +587,6 @@
ultimately show "\<mu> (\<Union>i. N i) = 0" using assms by auto
qed
-lemma (in measure_space) null_sets_finite_UN:
- assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
- shows "(\<Union>i\<in>S. A i) \<in> null_sets"
-proof (intro CollectI conjI)
- show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
- then have "0 \<le> \<mu> (\<Union>i\<in>S. A i)" by simp
- moreover have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
- using assms by (intro measure_finitely_subadditive) auto
- ultimately show "\<mu> (\<Union>i\<in>S. A i) = 0" using assms by auto
-qed
-
lemma (in measure_space) null_set_Int1:
assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets"
using assms proof (intro CollectI conjI)
--- a/src/HOL/Probability/Probability.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Probability.thy Fri May 20 14:12:59 2011 +0200
@@ -4,6 +4,7 @@
Lebesgue_Measure
Probability_Measure
Infinite_Product_Measure
+ Independent_Family
Information
"ex/Dining_Cryptographers"
"ex/Koepf_Duermuth_Countermeasure"
--- a/src/HOL/Probability/Probability_Measure.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Fri May 20 14:12:59 2011 +0200
@@ -543,6 +543,115 @@
sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default
sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default
+locale product_finite_prob_space =
+ fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
+ and I :: "'i set"
+ assumes finite_space: "\<And>i. finite_prob_space (M i)" and finite_index: "finite I"
+
+sublocale product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space .
+sublocale product_finite_prob_space \<subseteq> finite_product_sigma_finite M I by default (rule finite_index)
+sublocale product_finite_prob_space \<subseteq> prob_space "Pi\<^isub>M I M"
+proof
+ show "\<mu> (space P) = 1"
+ using measure_times[OF M.top] M.measure_space_1
+ by (simp add: setprod_1 space_product_algebra)
+qed
+
+lemma funset_eq_UN_fun_upd_I:
+ assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
+ and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
+ and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
+ shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
+proof safe
+ fix f assume f: "f \<in> F (insert a A)"
+ show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
+ proof (rule UN_I[of "f(a := d)"])
+ show "f(a := d) \<in> F A" using *[OF f] .
+ show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
+ proof (rule image_eqI[of _ _ "f a"])
+ show "f a \<in> G (f(a := d))" using **[OF f] .
+ qed simp
+ qed
+next
+ fix f x assume "f \<in> F A" "x \<in> G f"
+ from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
+qed
+
+lemma extensional_funcset_insert_eq[simp]:
+ assumes "a \<notin> A"
+ shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
+ apply (rule funset_eq_UN_fun_upd_I)
+ using assms
+ by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
+
+lemma finite_extensional_funcset[simp, intro]:
+ assumes "finite A" "finite B"
+ shows "finite (extensional A \<inter> (A \<rightarrow> B))"
+ using assms by induct (auto simp: extensional_funcset_insert_eq)
+
+lemma finite_PiE[simp, intro]:
+ assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
+ shows "finite (Pi\<^isub>E A B)"
+proof -
+ have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
+ show ?thesis
+ using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
+qed
+
+sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
+proof
+ show "finite (space P)"
+ using finite_index M.finite_space by auto
+
+ { fix x assume "x \<in> space P"
+ then have x: "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
+ proof safe
+ fix y assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
+ show "y = x"
+ proof
+ fix i show "y i = x i"
+ using * `x \<in> space P` by (cases "i \<in> I") (auto simp: extensional_def)
+ qed
+ qed auto
+ with `x \<in> space P` have "{x} \<in> sets P"
+ by (auto intro!: in_P) }
+ note x_in_P = this
+
+ have "Pow (space P) \<subseteq> sets P"
+ proof
+ fix X assume "X \<in> Pow (space P)"
+ moreover then have "finite X"
+ using `finite (space P)` by (blast intro: finite_subset)
+ ultimately have "(\<Union>x\<in>X. {x}) \<in> sets P"
+ by (intro finite_UN x_in_P) auto
+ then show "X \<in> sets P" by simp
+ qed
+ with space_closed show [simp]: "sets P = Pow (space P)" ..
+
+
+ { fix x assume "x \<in> space P"
+ from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto
+ then show "\<mu> {x} \<noteq> \<infinity>"
+ using measure_space_1 by auto }
+qed
+
+lemma (in product_finite_prob_space) measure_finite_times:
+ "(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))"
+ by (rule measure_times) simp
+
+lemma (in product_finite_prob_space) prob_times:
+ assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)"
+ shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
+proof -
+ have "extreal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)"
+ using X by (intro finite_measure_eq[symmetric] in_P) auto
+ also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i (X i))"
+ using measure_finite_times X by simp
+ also have "\<dots> = extreal (\<Prod>i\<in>I. M.\<mu>' i (X i))"
+ using X by (simp add: M.finite_measure_eq setprod_extreal)
+ finally show ?thesis by simp
+qed
+
lemma (in prob_space) joint_distribution_finite_prob_space:
assumes X: "finite_random_variable MX X"
assumes Y: "finite_random_variable MY Y"
@@ -611,12 +720,6 @@
(auto simp add: disjoint_family_on_def sets_eq_Pow
intro!: arg_cong[where f=\<mu>'])
-lemma (in finite_prob_space) sum_over_space_real_distribution:
- "(\<Sum>x\<in>X`space M. distribution X {x}) = 1"
- unfolding distribution_def prob_space[symmetric] using finite_space
- by (subst finite_measure_finite_Union[symmetric])
- (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob])
-
lemma (in finite_prob_space) finite_sum_over_space_eq_1:
"(\<Sum>x\<in>space M. prob {x}) = 1"
using prob_space finite_space
@@ -942,4 +1045,21 @@
qed
qed
+subsection "Bernoulli space"
+
+definition "bernoulli_space p = \<lparr> space = UNIV, sets = UNIV,
+ measure = extreal \<circ> setsum (\<lambda>b. if b then min 1 (max 0 p) else 1 - min 1 (max 0 p)) \<rparr>"
+
+interpretation bernoulli: finite_prob_space "bernoulli_space p" for p
+ by (rule finite_prob_spaceI)
+ (auto simp: bernoulli_space_def UNIV_bool one_extreal_def setsum_Un_disjoint intro!: setsum_nonneg)
+
+lemma bernoulli_measure:
+ "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p B = (\<Sum>b\<in>B. if b then p else 1 - p)"
+ unfolding bernoulli.\<mu>'_def unfolding bernoulli_space_def by (auto intro!: setsum_cong)
+
+lemma bernoulli_measure_True: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p {True} = p"
+ and bernoulli_measure_False: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p {False} = 1 - p"
+ unfolding bernoulli_measure by simp_all
+
end
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri May 20 14:12:59 2011 +0200
@@ -975,7 +975,7 @@
finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" by simp }
from this[OF borel(1) refl] this[OF borel(2) f]
have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>} \<in> null_sets" by simp_all
- then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule null_sets_Un)
+ then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule nullsets.Un)
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def)
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri May 20 14:12:59 2011 +0200
@@ -77,6 +77,42 @@
lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
by (metis Int_absorb2 sets_into_space)
+lemma (in ring_of_sets) sets_Collect_conj:
+ assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
+ shows "{x\<in>space M. Q x \<and> P x} \<in> sets M"
+proof -
+ have "{x\<in>space M. Q x \<and> P x} = {x\<in>space M. Q x} \<inter> {x\<in>space M. P x}"
+ by auto
+ with assms show ?thesis by auto
+qed
+
+lemma (in ring_of_sets) sets_Collect_disj:
+ assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
+ shows "{x\<in>space M. Q x \<or> P x} \<in> sets M"
+proof -
+ have "{x\<in>space M. Q x \<or> P x} = {x\<in>space M. Q x} \<union> {x\<in>space M. P x}"
+ by auto
+ with assms show ?thesis by auto
+qed
+
+lemma (in ring_of_sets) sets_Collect_finite_All:
+ assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S" "S \<noteq> {}"
+ shows "{x\<in>space M. \<forall>i\<in>S. P i x} \<in> sets M"
+proof -
+ have "{x\<in>space M. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>space M. P i x})"
+ using `S \<noteq> {}` by auto
+ with assms show ?thesis by auto
+qed
+
+lemma (in ring_of_sets) sets_Collect_finite_Ex:
+ assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S"
+ shows "{x\<in>space M. \<exists>i\<in>S. P i x} \<in> sets M"
+proof -
+ have "{x\<in>space M. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>space M. P i x})"
+ by auto
+ with assms show ?thesis by auto
+qed
+
locale algebra = ring_of_sets +
assumes top [iff]: "space M \<in> sets M"
@@ -134,6 +170,22 @@
qed
qed
+lemma (in algebra) sets_Collect_neg:
+ assumes "{x\<in>space M. P x} \<in> sets M"
+ shows "{x\<in>space M. \<not> P x} \<in> sets M"
+proof -
+ have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}" by auto
+ with assms show ?thesis by auto
+qed
+
+lemma (in algebra) sets_Collect_imp:
+ "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x \<longrightarrow> P x} \<in> sets M"
+ unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)
+
+lemma (in algebra) sets_Collect_const:
+ "{x\<in>space M. P} \<in> sets M"
+ by (cases P) auto
+
section {* Restricted algebras *}
abbreviation (in algebra)
@@ -212,6 +264,26 @@
algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
+lemma (in sigma_algebra) sets_Collect_countable_All:
+ assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
+ shows "{x\<in>space M. \<forall>i::'i::countable. P i x} \<in> sets M"
+proof -
+ have "{x\<in>space M. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>space M. P i x})" by auto
+ with assms show ?thesis by auto
+qed
+
+lemma (in sigma_algebra) sets_Collect_countable_Ex:
+ assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
+ shows "{x\<in>space M. \<exists>i::'i::countable. P i x} \<in> sets M"
+proof -
+ have "{x\<in>space M. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>space M. P i x})" by auto
+ with assms show ?thesis by auto
+qed
+
+lemmas (in sigma_algebra) sets_Collect =
+ sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
+ sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
+
subsection {* Binary Unions *}
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
@@ -441,6 +513,18 @@
lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
unfolding sigma_def sigma_sets_eq by simp
+lemma restricted_sigma:
+ assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
+ shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"
+proof -
+ from S sigma_sets_into_sp[OF M]
+ have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M"
+ by (auto simp: sigma_def)
+ from sigma_sets_Int[OF this]
+ show ?thesis
+ by (simp add: sigma_def)
+qed
+
section {* Measurable functions *}
definition
@@ -1417,4 +1501,37 @@
using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
using measurable_up_sigma[of M N] N by auto
+lemma (in sigma_algebra) measurable_Least:
+ assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> sets M"
+ shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
+proof -
+ { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
+ proof cases
+ assume i: "(LEAST j. False) = i"
+ have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
+ {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
+ by (simp add: set_eq_iff, safe)
+ (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
+ with meas show ?thesis
+ by (auto intro!: Int)
+ next
+ assume i: "(LEAST j. False) \<noteq> i"
+ then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
+ {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
+ proof (simp add: set_eq_iff, safe)
+ fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
+ have "\<exists>j. P j x"
+ by (rule ccontr) (insert neq, auto)
+ then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
+ qed (auto dest: Least_le intro!: Least_equality)
+ with meas show ?thesis
+ by (auto intro!: Int)
+ qed }
+ then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
+ by (intro countable_UN) auto
+ moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
+ (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
+ ultimately show ?thesis by auto
+qed
+
end
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 14:12:59 2011 +0200
@@ -3,7 +3,7 @@
Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
-Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax.
+Abstract representation of ATP proofs and TSTP/SPASS syntax.
*)
signature ATP_PROOF =
@@ -15,7 +15,8 @@
Unprovable |
IncompleteUnprovable |
ProofMissing |
- UnsoundProof of bool |
+ ProofIncomplete |
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
OutOfResources |
@@ -46,8 +47,8 @@
val extract_known_failure :
(failure * string) list -> string -> failure option
val extract_tstplike_proof_and_outcome :
- bool -> bool -> bool -> int -> (string * string) list
- -> (failure * string) list -> string -> string * failure option
+ bool -> bool -> int -> (string * string) list -> (failure * string) list
+ -> string -> string * failure option
val is_same_step : step_name * step_name -> bool
val atp_proof_from_tstplike_proof : string -> string proof
val map_term_names_in_atp_proof :
@@ -64,7 +65,8 @@
Unprovable |
IncompleteUnprovable |
ProofMissing |
- UnsoundProof of bool |
+ ProofIncomplete |
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
OutOfResources |
@@ -117,20 +119,27 @@
" appears to be missing. You will need to install it if you want to invoke \
\remote provers."
+fun involving [] = ""
+ | involving ss = "involving " ^ commas_quote ss ^ " "
+
fun string_for_failure Unprovable =
"The problem is unprovable."
| string_for_failure IncompleteUnprovable =
"The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
- | string_for_failure (UnsoundProof false) =
- "The prover found a type-unsound proof (or, very unlikely, your axioms \
- \are inconsistent). Try passing the \"full_types\" option to Sledgehammer \
- \to avoid such spurious proofs."
- | string_for_failure (UnsoundProof true) =
- "The prover found a type-unsound proof even though a supposedly type-sound \
- \encoding was used (or, very unlikely, your axioms are inconsistent). You \
- \might want to report this to the Isabelle developers."
+ | string_for_failure ProofIncomplete =
+ "The prover claims the conjecture is a theorem but provided an incomplete \
+ \proof."
+ | string_for_failure (UnsoundProof (false, ss)) =
+ "The prover found a type-unsound proof " ^ involving ss ^
+ "(or, less likely, your axioms are inconsistent). Try passing the \
+ \\"full_types\" option to Sledgehammer to avoid such spurious proofs."
+ | string_for_failure (UnsoundProof (true, ss)) =
+ "The prover found a type-unsound proof " ^ involving ss ^
+ "even though a supposedly type-sound encoding was used (or, less likely, \
+ \your axioms are inconsistent). You might want to report this to the \
+ \Isabelle developers."
| string_for_failure CantConnect = "Cannot connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The prover ran out of resources."
@@ -193,24 +202,18 @@
|> find_first (fn (_, pattern) => String.isSubstring pattern output)
|> Option.map fst
-fun extract_tstplike_proof_and_outcome debug verbose complete res_code
- proof_delims known_failures output =
- case extract_known_failure known_failures output of
- NONE =>
- (case extract_tstplike_proof proof_delims output of
- "" =>
- ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then
- ProofMissing
- else
- UnknownError (short_output verbose output)))
- | tstplike_proof =>
- if res_code = 0 then (tstplike_proof, NONE)
- else ("", SOME (UnknownError (short_output verbose output))))
- | SOME failure =>
- ("", SOME (if failure = IncompleteUnprovable andalso complete then
- Unprovable
- else
- failure))
+fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
+ known_failures output =
+ case (extract_tstplike_proof proof_delims output,
+ extract_known_failure known_failures output) of
+ (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
+ | ("", SOME failure) =>
+ ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable
+ else failure))
+ | ("", NONE) =>
+ ("", SOME (if res_code = 0 andalso output = "" then ProofMissing
+ else UnknownError (short_output verbose output)))
+ | (tstplike_proof, _) => (tstplike_proof, NONE)
fun mk_anot (AConn (ANot, [phi])) = phi
| mk_anot phi = AConn (ANot, [phi])
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri May 20 14:12:59 2011 +0200
@@ -209,6 +209,7 @@
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
(Unprovable, "SZS status CounterSatisfiable"),
+ (ProofMissing, "SZS status Theorem"),
(TimedOut, "Failure: Resource limit exceeded (time)"),
(TimedOut, "time limit exceeded"),
(OutOfResources,
@@ -221,11 +222,12 @@
best_slices = fn ctxt =>
(* FUDGE *)
if effective_e_weight_method ctxt = e_slicesN then
- [(0.333, (true, (100, ["mangled_preds?"]))) (* sym_offset_weight *),
- (0.333, (true, (800, ["poly_tags!"]))) (* auto *),
- (0.334, (true, (200, ["mangled_preds?"]))) (* fun_weight *)]
+ [(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *),
+ (0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *),
+ (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
+ (* fun_weight *)]
else
- [(1.0, (true, (250, ["mangled_preds?"])))]}
+ [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]}
val e = (eN, e_config)
@@ -243,7 +245,7 @@
arguments = fn ctxt => fn slice => fn timeout => fn _ =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
- |> (slice = 0 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
+ |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
known_perl_failures @
@@ -259,8 +261,9 @@
formats = [Fof],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *),
- (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]
+ [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *),
+ (0.333, (false, (150, ["mangled_preds?"]))) (* SOS *),
+ (0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)]
|> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -278,7 +281,7 @@
arguments = fn ctxt => fn slice => fn timeout => fn _ =>
"--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
" --thanks \"Andrei and Krystof\" --input_file"
- |> (slice = 0 orelse Config.get ctxt vampire_force_sos)
+ |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
? prefix "--sos on ",
proof_delims =
[("=========== Refutation ==========",
@@ -289,8 +292,7 @@
[(Unprovable, "UNPROVABLE"),
(IncompleteUnprovable, "CANNOT PROVE"),
(IncompleteUnprovable, "SZS status GaveUp"),
- (ProofMissing, "[predicate definition introduction]"),
- (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
+ (ProofIncomplete, "predicate_definition_introduction,[]"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
@@ -301,8 +303,9 @@
formats = [Fof],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *),
- (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]
+ [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
+ (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
+ (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
|> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -403,14 +406,14 @@
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
val remote_tofof_e =
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *))
+ Axiom Conjecture [Tff] (K (200, ["simple"]) (* FUDGE *))
val remote_sine_e =
remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
- (K (500, ["poly_args"]) (* FUDGE *))
+ (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Conjecture
- [Tff, Fof] (K (250, ["simple_types"]) (* FUDGE *))
+ [Tff, Fof] (K (250, ["simple"]) (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri May 20 14:12:59 2011 +0200
@@ -132,7 +132,7 @@
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
-fun neg_clausify ctxt =
+val neg_clausify =
single
#> Meson.make_clauses_unsorted
#> map Meson_Clausify.introduce_combinators_in_theorem
@@ -158,7 +158,7 @@
(verbose_warning ctxt "Proof state contains the universal sort {}";
Seq.empty)
else
- Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 14:12:59 2011 +0200
@@ -654,11 +654,9 @@
equality helpers by default in Metis breaks a few existing proofs. *)
(true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
- ("fFalse", (true, [@{lemma "x = fTrue | x = fFalse"
- by (unfold fFalse_def fTrue_def) fast}])),
+ ("fFalse", (true, @{thms True_or_False})),
("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
- ("fTrue", (true, [@{lemma "x = fTrue | x = fFalse"
- by (unfold fFalse_def fTrue_def) fast}])),
+ ("fTrue", (true, @{thms True_or_False})),
("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
("fNot",
(false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
@@ -673,7 +671,7 @@
(false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
"~ fimplies P Q | ~ P | Q"
by (unfold fimplies_def) fast+})),
- ("If", (true, @{thms if_True if_False True_or_False})) (* FIXME *)]
+ ("If", (true, @{thms if_True if_False True_or_False}))]
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 14:12:59 2011 +0200
@@ -14,7 +14,7 @@
type minimize_command = string list -> string
type metis_params =
string * minimize_command * type_system * string proof * int
- * (string * locality) list vector * thm * int
+ * (string * locality) list vector * int list * thm * int
type isar_params =
Proof.context * bool * int * string Symtab.table * int list list
* int Symtab.table
@@ -22,14 +22,14 @@
val repair_conjecture_shape_and_fact_names :
type_system -> string -> int list list -> int
- -> (string * locality) list vector
- -> int list list * int * (string * locality) list vector
+ -> (string * locality) list vector -> int list
+ -> int list list * int * (string * locality) list vector * int list
val used_facts_in_atp_proof :
type_system -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
- val is_unsound_proof :
+ val used_facts_in_unsound_atp_proof :
type_system -> int list list -> int -> (string * locality) list vector
- -> string proof -> bool
+ -> string proof -> string list option
val apply_on_subgoal : string -> int -> int -> string
val command_call : string -> string list -> string
val try_command_line : string -> string -> string
@@ -55,7 +55,7 @@
type minimize_command = string list -> string
type metis_params =
string * minimize_command * type_system * string proof * int
- * (string * locality) list vector * thm * int
+ * (string * locality) list vector * int list * thm * int
type isar_params =
Proof.context * bool * int * string Symtab.table * int list list
* int Symtab.table
@@ -64,6 +64,9 @@
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+val is_typed_helper_name =
+ String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
fun find_first_in_list_vector vec key =
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
| (_, value) => value) NONE vec
@@ -102,7 +105,7 @@
? (space_implode "_" o tl o space_explode "_")
fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
- fact_offset fact_names =
+ fact_offset fact_names typed_helpers =
if String.isSubstring set_ClauseFormulaRelationN output then
let
val j0 = hd (hd conjecture_shape)
@@ -122,13 +125,17 @@
error ("No such fact: " ^ quote name ^ "."))
in
(conjecture_shape |> map (maps renumber_conjecture), 0,
- seq |> map names_for_number |> Vector.fromList)
+ seq |> map names_for_number |> Vector.fromList,
+ name_map |> filter (forall is_typed_helper_name o snd) |> map fst)
end
else
- (conjecture_shape, fact_offset, fact_names)
+ (conjecture_shape, fact_offset, fact_names, typed_helpers)
val vampire_step_prefix = "f" (* grrr... *)
+val extract_step_number =
+ Int.fromString o perhaps (try (unprefix vampire_step_prefix))
+
fun resolve_fact type_sys _ fact_names (_, SOME s) =
(case try (unprefix fact_prefix) s of
SOME s' =>
@@ -139,15 +146,18 @@
end
| NONE => [])
| resolve_fact _ facts_offset fact_names (num, NONE) =
- case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
- SOME j =>
- let val j = j - facts_offset in
- if j > 0 andalso j <= Vector.length fact_names then
- Vector.sub (fact_names, j - 1)
- else
- []
- end
- | NONE => []
+ (case extract_step_number num of
+ SOME j =>
+ let val j = j - facts_offset in
+ if j > 0 andalso j <= Vector.length fact_names then
+ Vector.sub (fact_names, j - 1)
+ else
+ []
+ end
+ | NONE => [])
+
+fun is_fact type_sys conjecture_shape =
+ not o null o resolve_fact type_sys 0 conjecture_shape
fun resolve_conjecture _ (_, SOME s) =
(case try (unprefix conjecture_prefix) s of
@@ -157,18 +167,21 @@
| NONE => [])
| NONE => [])
| resolve_conjecture conjecture_shape (num, NONE) =
- case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
- SOME i =>
- (case find_index (exists (curry (op =) i)) conjecture_shape of
- ~1 => []
- | j => [j])
+ case extract_step_number num of
+ SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
+ ~1 => []
+ | j => [j])
| NONE => []
-fun is_fact type_sys conjecture_shape =
- not o null o resolve_fact type_sys 0 conjecture_shape
fun is_conjecture conjecture_shape =
not o null o resolve_conjecture conjecture_shape
+fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s
+ | is_typed_helper typed_helpers (num, NONE) =
+ (case extract_step_number num of
+ SOME i => member (op =) typed_helpers i
+ | NONE => false)
+
fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
append (resolve_fact type_sys facts_offset fact_names name)
| add_fact _ _ _ _ = I
@@ -181,10 +194,18 @@
exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
| _ => false)
-fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
- not o is_conjecture_referred_to_in_proof conjecture_shape andf
- forall (is_locality_global o snd)
- o used_facts_in_atp_proof type_sys facts_offset fact_names
+fun used_facts_in_unsound_atp_proof type_sys conjecture_shape facts_offset
+ fact_names atp_proof =
+ let
+ val used_facts = used_facts_in_atp_proof type_sys facts_offset fact_names
+ atp_proof
+ in
+ if forall (is_locality_global o snd) used_facts andalso
+ not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
+ SOME (map fst used_facts)
+ else
+ NONE
+ end
(** Soft-core proof reconstruction: Metis one-liner **)
@@ -219,15 +240,21 @@
List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
+fun uses_typed_helpers typed_helpers =
+ exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
+ | _ => false)
+
fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
- facts_offset, fact_names, goal, i) =
+ facts_offset, fact_names, typed_helpers, goal, i) =
let
val (chained, extra) =
atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
|> split_used_facts
+ val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
+ val metis = metis_command full_types i n ([], map fst extra)
in
- (try_command_line banner (metis_command false i n ([], map fst extra)) ^
+ (try_command_line banner metis ^
minimize_line minimize_command (map fst (extra @ chained)),
extra @ chained)
end
@@ -911,7 +938,7 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt0 i n =
+fun string_for_proof ctxt0 full_types i n =
let
val ctxt =
ctxt0 |> Config.put show_free_types false
@@ -934,7 +961,7 @@
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
fun do_facts (ls, ss) =
- metis_command false 1 1
+ metis_command full_types 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
@@ -971,11 +998,12 @@
fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape,
sym_tab)
(metis_params as (_, _, type_sys, atp_proof, facts_offset,
- fact_names, goal, i)) =
+ fact_names, typed_helpers, goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+ val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
val (one_line_proof, lemma_names) = metis_proof_text metis_params
fun isar_proof_for () =
@@ -987,7 +1015,7 @@
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt i n of
+ |> string_for_proof ctxt full_types i n of
"" => "\nNo structured proof available (proof too short)."
| proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 14:12:59 2011 +0200
@@ -28,6 +28,8 @@
val readable_names : bool Config.T
val fact_prefix : string
val conjecture_prefix : string
+ val helper_prefix : string
+ val typed_helper_suffix : string
val predicator_base : string
val explicit_app_base : string
val type_pred_base : string
@@ -46,7 +48,7 @@
-> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
- * (string * 'a) list vector * int Symtab.table
+ * (string * 'a) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -61,6 +63,16 @@
(* experimental *)
val generate_useful_info = false
+fun useful_isabelle_info s =
+ if generate_useful_info then
+ SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
+ else
+ NONE
+
+val intro_info = useful_isabelle_info "intro"
+val elim_info = useful_isabelle_info "elim"
+val simp_info = useful_isabelle_info "simp"
+
(* Readable names are often much shorter, especially if types are mangled in
names. Also, the logic for generating legal SNARK sort names is only
implemented for readable names. Finally, readable names are, well, more
@@ -77,6 +89,9 @@
val arity_clause_prefix = "arity_"
val tfree_prefix = "tfree_"
+val typed_helper_suffix = "_T"
+val untyped_helper_suffix = "_U"
+
val predicator_base = "hBOOL"
val explicit_app_base = "hAPP"
val type_pred_base = "is"
@@ -120,31 +135,21 @@
| NONE => (All_Types, s))
||> apsnd (fn s =>
case try (unsuffix "_heavy") s of
- SOME s => (SOME Heavy, s)
- | NONE =>
- case try (unsuffix "_light") s of
- SOME s => (SOME Light, s)
- | NONE => (NONE, s))
+ SOME s => (Heavy, s)
+ | NONE => (Light, s))
|> (fn (poly, (level, (heaviness, core))) =>
case (core, (poly, level, heaviness)) of
- ("simple_types", (NONE, level, NONE)) => Simple_Types level
- | ("preds", (SOME Polymorphic, level, _)) =>
- if level = All_Types then
- Preds (Polymorphic, level, heaviness |> the_default Light)
- else
- raise Same.SAME
- | ("preds", (SOME poly, level, _)) =>
- Preds (poly, level, heaviness |> the_default Light)
- | ("tags", (SOME Polymorphic, level, _)) =>
- if level = All_Types orelse level = Finite_Types then
- Tags (Polymorphic, level, heaviness |> the_default Light)
- else
- raise Same.SAME
- | ("tags", (SOME poly, level, _)) =>
- Tags (poly, level, heaviness |> the_default Light)
- | ("args", (SOME poly, All_Types (* naja *), NONE)) =>
+ ("simple", (NONE, _, Light)) => Simple_Types level
+ | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
+ | ("tags", (SOME Polymorphic, All_Types, _)) =>
+ Tags (Polymorphic, All_Types, heaviness)
+ | ("tags", (SOME Polymorphic, _, _)) =>
+ (* The actual light encoding is very unsound. *)
+ Tags (Polymorphic, level, Heavy)
+ | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
+ | ("args", (SOME poly, All_Types (* naja *), Light)) =>
Preds (poly, Const_Arg_Types, Light)
- | ("erased", (NONE, All_Types (* naja *), NONE)) =>
+ | ("erased", (NONE, All_Types (* naja *), Light)) =>
Preds (Polymorphic, No_Types, Light)
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
@@ -174,15 +179,24 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
+fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
+ | aconn_fold pos f (AImplies, [phi1, phi2]) =
+ f (Option.map not pos) phi1 #> f pos phi2
+ | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
+ | aconn_fold pos f (AOr, phis) = fold (f pos) phis
+ | aconn_fold _ f (_, phis) = fold (f NONE) phis
+
+fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
+ | aconn_map pos f (AImplies, [phi1, phi2]) =
+ AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
+ | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
+ | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
+ | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
+
fun formula_fold pos f =
let
fun aux pos (AQuant (_, _, phi)) = aux pos phi
- | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
- | aux pos (AConn (AImplies, [phi1, phi2])) =
- aux (Option.map not pos) phi1 #> aux pos phi2
- | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
- | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
- | aux _ (AConn (_, phis)) = fold (aux NONE) phis
+ | aux pos (AConn conn) = aconn_fold pos aux conn
| aux pos (AAtom tm) = f pos tm
in aux pos end
@@ -474,7 +488,7 @@
if prem_kind = Conjecture then update_combformula mk_anot
else I)
in
- make_formula ctxt true true (string_of_int j) Chained kind t
+ make_formula ctxt true true (string_of_int j) General kind t
|> maybe_negate
end)
(0 upto last) ts
@@ -482,21 +496,27 @@
(** Finite and infinite type inference **)
+fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
+ | deep_freeze_atyp T = T
+val deep_freeze_type = map_atyps deep_freeze_atyp
+
+val type_instance = Sign.typ_instance o Proof_Context.theory_of
+
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Löwenheim-Skolem). *)
-fun should_encode_type _ (nonmono_Ts as _ :: _) _ T =
- exists (curry Type.raw_instance T) nonmono_Ts
+fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
+ exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
| should_encode_type _ _ All_Types _ = true
| should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
| should_encode_type _ _ _ _ = false
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
should_predicate_on_var T =
- (heaviness = Heavy orelse should_predicate_on_var ()) andalso
- should_encode_type ctxt nonmono_Ts level T
+ (heaviness = Heavy orelse should_predicate_on_var ()) andalso
+ should_encode_type ctxt nonmono_Ts level T
| should_predicate_on_type _ _ _ _ _ = false
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
@@ -711,7 +731,7 @@
in
Formula (helper_prefix ^ "ti_ti", Axiom,
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
- |> close_formula_universally, NONE, NONE)
+ |> close_formula_universally, simp_info, NONE)
end
fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
@@ -721,8 +741,10 @@
val thy = Proof_Context.theory_of ctxt
val unmangled_s = mangled_s |> unmangled_const_name
fun dub_and_inst c needs_some_types (th, j) =
- ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
- Chained),
+ ((c ^ "_" ^ string_of_int j ^
+ (if needs_some_types then typed_helper_suffix
+ else untyped_helper_suffix),
+ General),
let val t = th |> prop_of in
t |> ((case general_type_arg_policy type_sys of
Mangled_Type_Args _ => true
@@ -786,17 +808,17 @@
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
+fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T])
|> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
tm)
- |> AAtom
-fun var_occurs_naked_in_term name (ATerm ((s, _), tms)) accum =
- accum orelse
- (s = "equal" andalso member (op =) tms (ATerm (name, [])))
-fun var_occurs_naked_in_formula phi name =
- formula_fold NONE (K (var_occurs_naked_in_term name)) phi false
+fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
+ | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
+ accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, [])))
+fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
+ | is_var_nonmonotonic_in_formula pos phi _ name =
+ formula_fold pos (var_occurs_positively_naked_in_term name) phi false
fun tag_with_type ctxt nonmono_Ts type_sys T tm =
CombConst (`make_fixed_const type_tag_name, T --> T, [T])
@@ -825,34 +847,38 @@
end
and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var =
let
+ val do_term = term_from_combterm ctxt nonmono_Ts type_sys Top_Level
val do_bound_type =
case type_sys of
Simple_Types level =>
SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
| _ => K NONE
- fun do_out_of_bound_type phi (name, T) =
+ fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_sys
- (fn () => should_predicate_on_var phi name) T then
+ (fn () => should_predicate_on_var pos phi universal name) T then
CombVar (name, T)
- |> type_pred_combatom ctxt nonmono_Ts type_sys T
- |> do_formula |> SOME
+ |> type_pred_combterm ctxt nonmono_Ts type_sys T
+ |> do_term |> AAtom |> SOME
else
NONE
- and do_formula (AQuant (q, xs, phi)) =
- let val phi = phi |> do_formula in
+ fun do_formula pos (AQuant (q, xs, phi)) =
+ let
+ val phi = phi |> do_formula pos
+ val universal = Option.map (q = AExists ? not) pos
+ in
AQuant (q, xs |> map (apsnd (fn NONE => NONE
| SOME T => do_bound_type T)),
(if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
(map_filter
(fn (_, NONE) => NONE
| (s, SOME T) =>
- do_out_of_bound_type phi (s, T)) xs)
+ do_out_of_bound_type pos phi universal (s, T))
+ xs)
phi)
end
- | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
- | do_formula (AAtom tm) =
- AAtom (term_from_combterm ctxt nonmono_Ts type_sys Top_Level tm)
- in do_formula end
+ | do_formula pos (AConn conn) = aconn_map pos do_formula conn
+ | do_formula _ (AAtom tm) = AAtom (do_term tm)
+ in do_formula o SOME end
fun bound_atomic_types type_sys Ts =
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
@@ -863,12 +889,10 @@
combformula
|> close_combformula_universally
|> formula_from_combformula ctxt nonmono_Ts type_sys
- var_occurs_naked_in_formula
+ is_var_nonmonotonic_in_formula true
|> bound_atomic_types type_sys atomic_types
|> close_formula_universally
-fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
-
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
@@ -878,14 +902,11 @@
else string_of_int j ^ "_") ^
ascii_of name,
kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
- if generate_useful_info then
- case locality of
- Intro => useful_isabelle_info "intro"
- | Elim => useful_isabelle_info "elim"
- | Simp => useful_isabelle_info "simp"
- | _ => NONE
- else
- NONE)
+ case locality of
+ Intro => intro_info
+ | Elim => elim_info
+ | Simp => simp_info
+ | _ => NONE)
fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
@@ -893,7 +914,7 @@
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
AAtom (ATerm (superclass, [ty_arg]))])
- |> close_formula_universally, NONE, NONE)
+ |> close_formula_universally, intro_info, NONE)
end
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
@@ -908,13 +929,13 @@
o fo_literal_from_arity_literal) premLits)
(formula_from_fo_literal
(fo_literal_from_arity_literal conclLit))
- |> close_formula_universally, NONE, NONE)
+ |> close_formula_universally, intro_info, NONE)
fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
({name, kind, combformula, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
formula_from_combformula ctxt nonmono_Ts type_sys
- var_occurs_naked_in_formula
+ is_var_nonmonotonic_in_formula false
(close_combformula_universally combformula)
|> close_formula_universally, NONE, NONE)
@@ -933,10 +954,10 @@
(** Symbol declarations **)
-fun insert_type get_T x xs =
+fun insert_type ctxt get_T x xs =
let val T = get_T x in
- if exists (curry Type.raw_instance T o get_T) xs then xs
- else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
+ if exists (curry (type_instance ctxt) T o get_T) xs then xs
+ else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
end
fun should_declare_sym type_sys pred_sym s =
@@ -947,7 +968,7 @@
| Tags (_, _, Light) => true
| _ => false) orelse not pred_sym)
-fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
let
fun add_combterm in_conj tm =
let val (head, args) = strip_combterm_comb tm in
@@ -956,8 +977,8 @@
let val pred_sym = is_pred_sym repaired_sym_tab s in
if should_declare_sym type_sys pred_sym s then
Symtab.map_default (s, [])
- (insert_type #3 (s', T_args, T, pred_sym, length args,
- in_conj))
+ (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
+ in_conj))
else
I
end
@@ -972,35 +993,37 @@
? (fold (add_fact true) conjs #> fold (add_fact false) facts)
end
+(* These types witness that the type classes they belong to allow infinite
+ models and hence that any types with these type classes is monotonic. *)
+val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}]
+
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
+fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
| add_combterm_nonmonotonic_types ctxt level _
(CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
tm2)) =
(exists is_var_or_bound_var [tm1, tm2] andalso
(case level of
- Nonmonotonic_Types => not (is_type_surely_infinite ctxt T)
+ Nonmonotonic_Types =>
+ not (is_type_surely_infinite ctxt known_infinite_types T)
| Finite_Types => is_type_surely_finite ctxt T
- | _ => true)) ? insert_type I T
+ | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
| add_combterm_nonmonotonic_types _ _ _ _ = I
fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
: translated_formula) =
formula_fold (SOME (kind <> Conjecture))
(add_combterm_nonmonotonic_types ctxt level) combformula
-fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
+fun nonmonotonic_types_for_facts ctxt type_sys facts =
let val level = level_of_type_sys type_sys in
- (case level of
- Nonmonotonic_Types => true
- | Finite_Types =>
- heaviness_of_type_sys type_sys = Light andalso
- polymorphism_of_type_sys type_sys <> Polymorphic
- | _ => false)
- ? (fold (add_fact_nonmonotonic_types ctxt level) facts
- (* We must add bool in case the helper "True_or_False" is added later.
- In addition, several places in the code rely on the list of
- nonmonotonic types not being empty. *)
- #> insert_type I @{typ bool})
+ if level = Nonmonotonic_Types orelse level = Finite_Types then
+ [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
+ (* We must add "bool" in case the helper "True_or_False" is added
+ later. In addition, several places in the code rely on the list of
+ nonmonotonic types not being empty. *)
+ |> insert_type ctxt I @{typ bool}
+ else
+ []
end
fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
@@ -1035,20 +1058,25 @@
(if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
- |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
+ |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
+ |> AAtom
|> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt nonmono_Ts type_sys (K (K true))
+ |> formula_from_combformula ctxt nonmono_Ts type_sys
+ (K (K (K (K true)))) true
|> n > 1 ? bound_atomic_types type_sys (atyps_of T)
|> close_formula_universally
|> maybe_negate,
- NONE, NONE)
+ intro_info, NONE)
end
-fun formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s
- (j, (s', T_args, T, pred_sym, ary, _)) =
+fun formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s
+ (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
+ val (kind, maybe_negate) =
+ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+ else (Axiom, I)
val (arg_Ts, res_T) = chop_fun ary T
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
@@ -1060,13 +1088,14 @@
else AAtom (ATerm (`I "equal", tms)))
|> bound_atomic_types type_sys atomic_Ts
|> close_formula_universally
+ |> maybe_negate
val should_encode = should_encode_type ctxt nonmono_Ts All_Types
val tag_with = tag_with_type ctxt nonmono_Ts type_sys
val add_formula_for_res =
if should_encode res_T then
- cons (Formula (ident_base ^ "_res", Axiom,
+ cons (Formula (ident_base ^ "_res", kind,
eq [tag_with res_T (const bounds), const bounds],
- NONE, NONE))
+ simp_info, NONE))
else
I
fun add_formula_for_arg k =
@@ -1074,11 +1103,11 @@
if should_encode arg_T then
case chop k bounds of
(bounds1, bound :: bounds2) =>
- cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), Axiom,
+ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
eq [const (bounds1 @ tag_with arg_T bound ::
bounds2),
const bounds],
- NONE, NONE))
+ simp_info, NONE))
| _ => raise Fail "expected nonempty tail"
else
I
@@ -1100,7 +1129,7 @@
case decls of
decl :: (decls' as _ :: _) =>
let val T = result_type_of_decl decl in
- if forall ((fn T' => Type.raw_instance (T', T))
+ if forall (curry (type_instance ctxt o swap) T
o result_type_of_decl) decls' then
[decl]
else
@@ -1123,7 +1152,8 @@
| Light =>
let val n = length decls in
(0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s)
+ |> maps (formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts
+ type_sys n s)
end)
fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
@@ -1173,8 +1203,7 @@
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
- val nonmono_Ts =
- [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
+ val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
@@ -1182,8 +1211,12 @@
repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts type_sys repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
+ val helper_lines =
+ map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys)
+ (0 upto length helpers - 1 ~~ helpers)
+ |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ())
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
@@ -1192,11 +1225,7 @@
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
- (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
- type_sys)
- (0 upto length helpers - 1 ~~ helpers)
- |> should_add_ti_ti_helper type_sys
- ? cons (ti_ti_helper_fact ())),
+ (helpersN, helper_lines),
(conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
conjs),
(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
@@ -1209,6 +1238,13 @@
| _ => I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
+ val helpers_offset = offset_of_heading_in_problem helpersN problem 0
+ val typed_helpers =
+ map_filter (fn (j, {name, ...}) =>
+ if String.isSuffix typed_helper_suffix name then SOME j
+ else NONE)
+ ((helpers_offset + 1 upto helpers_offset + length helpers)
+ ~~ helpers)
fun add_sym_arity (s, {min_ary, ...} : sym_info) =
if min_ary > 0 then
case strip_prefix_and_unascii const_prefix s of
@@ -1222,6 +1258,7 @@
offset_of_heading_in_problem conjsN problem 0,
offset_of_heading_in_problem factsN problem 0,
fact_names |> Vector.fromList,
+ typed_helpers,
Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 14:12:59 2011 +0200
@@ -404,13 +404,17 @@
val atp_important_message_keep_quotient = 10
val fallback_best_type_systems =
- [Preds (Polymorphic, Const_Arg_Types, Light),
- Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
+ [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
fun adjust_dumb_type_sys formats (Simple_Types level) =
if member (op =) formats Tff then (Tff, Simple_Types level)
else (Fof, Preds (Mangled_Monomorphic, level, Heavy))
- | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
+ | adjust_dumb_type_sys formats type_sys =
+ (* We could return (Tff, type_sys) in all cases but this would require the
+ TFF provers to accept problems in which constants are implicitly
+ declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *)
+ if member (op =) formats Fof then (Fof, type_sys)
+ else (Tff, Simple_Types All_Types)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys
| determine_format_and_type_sys best_type_systems formats
@@ -530,7 +534,7 @@
else
()
val (atp_problem, pool, conjecture_offset, facts_offset,
- fact_names, sym_tab) =
+ fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
explicit_apply hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
@@ -560,30 +564,32 @@
I)
|>> (if measure_run_time then split_time else rpair NONE)
val (atp_proof, outcome) =
- extract_tstplike_proof_and_outcome debug verbose complete
- res_code proof_delims known_failures output
+ extract_tstplike_proof_and_outcome verbose complete res_code
+ proof_delims known_failures output
|>> atp_proof_from_tstplike_proof
- val (conjecture_shape, facts_offset, fact_names) =
+ val (conjecture_shape, facts_offset, fact_names,
+ typed_helpers) =
if is_none outcome then
repair_conjecture_shape_and_fact_names type_sys output
- conjecture_shape facts_offset fact_names
+ conjecture_shape facts_offset fact_names typed_helpers
else
(* don't bother repairing *)
- (conjecture_shape, facts_offset, fact_names)
+ (conjecture_shape, facts_offset, fact_names, typed_helpers)
val outcome =
case outcome of
NONE =>
- if is_unsound_proof type_sys conjecture_shape facts_offset
- fact_names atp_proof then
- SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
- else
- NONE
+ used_facts_in_unsound_atp_proof type_sys
+ conjecture_shape facts_offset fact_names atp_proof
+ |> Option.map (fn facts =>
+ UnsoundProof (is_type_sys_virtually_sound type_sys,
+ facts))
| SOME Unprovable =>
if null blacklist then outcome
else SOME IncompleteUnprovable
| _ => outcome
in
- ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+ ((pool, conjecture_shape, facts_offset, fact_names,
+ typed_helpers, sym_tab),
(output, msecs, type_sys, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
@@ -603,9 +609,9 @@
end
| maybe_run_slice _ _ result = result
fun maybe_blacklist_facts_and_retry iter blacklist
- (result as ((_, _, facts_offset, fact_names, _),
+ (result as ((_, _, facts_offset, fact_names, _, _),
(_, _, type_sys, atp_proof,
- SOME (UnsoundProof false)))) =
+ SOME (UnsoundProof (false, _))))) =
(case used_facts_in_atp_proof type_sys facts_offset fact_names
atp_proof of
[] => result
@@ -620,7 +626,7 @@
result)
| maybe_blacklist_facts_and_retry _ _ result = result
in
- ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty),
+ ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
("", SOME 0, hd fallback_best_type_systems, [],
SOME InternalError))
|> fold (maybe_run_slice []) actual_slices
@@ -640,7 +646,8 @@
()
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
- val ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+ val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
+ sym_tab),
(output, msecs, type_sys, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
@@ -664,15 +671,17 @@
(ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
val metis_params =
(proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
- fact_names, goal, subgoal)
+ fact_names, typed_helpers, goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
NONE =>
(NONE, proof_text isar_proof isar_params metis_params
|>> append_to_message)
- | SOME ProofMissing =>
- (NONE, metis_proof_text metis_params |>> append_to_message)
- | SOME failure => (outcome, (string_for_failure failure, []))
+ | SOME failure =>
+ if failure = ProofMissing orelse failure = ProofIncomplete then
+ (NONE, metis_proof_text metis_params |>> append_to_message)
+ else
+ (outcome, (string_for_failure failure, []))
in
{outcome = outcome, message = message, used_facts = used_facts,
run_time_in_msecs = msecs}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 20 14:12:59 2011 +0200
@@ -92,8 +92,9 @@
{state, goal, subgoal, subgoal_count, facts, smt_filter} name =
let
val ctxt = Proof.context_of state
+ val hard_timeout = Time.+ (timeout, timeout)
val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
+ val death_time = Time.+ (birth_time, hard_timeout)
val max_relevant =
max_relevant
|> the_default (default_max_relevant_for_prover ctxt slicing name)
@@ -143,7 +144,7 @@
Pretty.mark Markup.hilite (Pretty.str message)]))
end
else if blocking then
- let val (success, message) = TimeLimit.timeLimit timeout go () in
+ let val (success, message) = TimeLimit.timeLimit hard_timeout go () in
List.app Output.urgent_message
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
(success, state)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 14:12:59 2011 +0200
@@ -22,7 +22,7 @@
val instantiate_type : theory -> typ -> typ -> typ -> typ
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
val is_type_surely_finite : Proof.context -> typ -> bool
- val is_type_surely_infinite : Proof.context -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_term : term -> term
@@ -126,28 +126,31 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card T =
+fun tiny_card_of_type ctxt default_card assigns T =
let
+ val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
fun aux slack avoid T =
- (if member (op =) avoid T then
- 0
- else case T of
- Type (@{type_name fun}, [T1, T2]) =>
- (case (aux slack avoid T1, aux slack avoid T2) of
- (k, 1) => if slack andalso k = 0 then 0 else 1
- | (0, _) => 0
- | (_, 0) => 0
- | (k1, k2) =>
- if k1 >= max orelse k2 >= max then max
- else Int.min (max, Integer.pow k2 k1))
- | @{typ prop} => 2
- | @{typ bool} => 2 (* optimization *)
- | @{typ nat} => 0 (* optimization *)
- | @{typ int} => 0 (* optimization *)
- | Type (s, _) =>
- let val thy = Proof_Context.theory_of ctxt in
- case datatype_constrs thy T of
+ if member (op =) avoid T then
+ 0
+ else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
+ SOME k => k
+ | NONE =>
+ case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ prop} => 2
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | @{typ int} => 0 (* optimization *)
+ | Type (s, _) =>
+ (case datatype_constrs thy T of
constrs as _ :: _ =>
let
val constr_cards =
@@ -174,18 +177,19 @@
0 => 0
| 1 => 1
| _ => default_card)
- | [] => default_card
- end
- | TFree _ =>
- (* Very slightly unsound: Type variables are assumed not to be
- constrained to cardinality 1. (In practice, the user would most
- likely have used "unit" directly anyway.) *)
- if default_card = 1 then 2 else default_card
- | _ => default_card)
+ | [] => default_card)
+ (* Very slightly unsound: Type variables are assumed not to be
+ constrained to cardinality 1. (In practice, the user would most
+ likely have used "unit" directly anyway.) *)
+ | TFree _ => if default_card = 1 then 2 else default_card
+ (* Schematic type variables that contain only unproblematic sorts
+ (with no finiteness axiom) can safely be considered infinite. *)
+ | TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
-fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
+fun is_type_surely_infinite ctxt infinite_Ts T =
+ tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
--- a/src/HOL/ex/tptp_export.ML Fri May 20 14:03:42 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Fri May 20 14:12:59 2011 +0200
@@ -103,7 +103,7 @@
else Sledgehammer_ATP_Translate.Const_Arg_Types,
Sledgehammer_ATP_Translate.Heavy)
val explicit_apply = false
- val (atp_problem, _, _, _, _, _) =
+ val (atp_problem, _, _, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom
ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts
val infers =