--- a/doc-src/Nitpick/nitpick.tex Thu Mar 11 15:52:35 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 11 17:39:45 2010 +0100
@@ -4,6 +4,7 @@
\usepackage{amssymb}
\usepackage[english,french]{babel}
\usepackage{color}
+\usepackage{footmisc}
\usepackage{graphicx}
%\usepackage{mathpazo}
\usepackage{multicol}
@@ -136,8 +137,8 @@
suggesting several textual improvements.
% and Perry James for reporting a typo.
-\section{Overview}
-\label{overview}
+\section{First Steps}
+\label{first-steps}
This section introduces Nitpick by presenting small examples. If possible, you
should try out the examples on your workstation. Your theory file should start
@@ -149,12 +150,12 @@
\textbf{begin}
\postw
-The results presented here were obtained using the JNI version of MiniSat and
-with multithreading disabled to reduce nondeterminism and a time limit of
-15~seconds (instead of 30~seconds). This was done by adding the line
+The results presented here were obtained using the JNI (Java Native Interface)
+version of MiniSat and with multithreading disabled to reduce nondeterminism.
+This was done by adding the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
@@ -471,7 +472,7 @@
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
-\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
Nitpick found a potential counterexample: \\[2\smallskipamount]
@@ -628,7 +629,7 @@
unlikely that one could be found for smaller cardinalities.
\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
-\label{typedefs-records-rationals-and-reals}
+\label{typedefs-quotient-types-records-rationals-and-reals}
Nitpick generally treats types declared using \textbf{typedef} as datatypes
whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
@@ -683,7 +684,26 @@
In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
integers $0$ and $1$, respectively. Other representants would have been
-possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
+possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
+use \textit{my\_int} extensively, it pays off to install a term postprocessor
+that converts the pair notation to the standard mathematical notation:
+
+\prew
+$\textbf{ML}~\,\{{*} \\
+\!\begin{aligned}[t]
+%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
+%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
+& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
+& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
+& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
+& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
+{*}\}\end{aligned}$ \\[2\smallskipamount]
+$\textbf{setup}~\,\{{*} \\
+\!\begin{aligned}[t]
+& \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t]
+ & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt]
+{*}\}\end{aligned}$
+\postw
Records are also handled as datatypes with a single constructor:
@@ -770,25 +790,25 @@
\prew
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
-\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
+\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
\slshape The inductive predicate ``\textit{even}'' was proved well-founded.
Nitpick can compute it efficiently. \\[2\smallskipamount]
Trying 1 scope: \\
-\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
-Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
+\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
+Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
Nitpick could not find a better counterexample. \\[2\smallskipamount]
Total time: 2274 ms.
\postw
No genuine counterexample is possible because Nitpick cannot rule out the
-existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
+existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
existential quantifier:
\prew
-\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
-\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
+\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
+\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment
\postw
@@ -1019,7 +1039,7 @@
can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
bisimilarity check is then performed \textsl{after} the counterexample has been
found to ensure correctness. If this after-the-fact check fails, the
-counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
+counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
check for the previous example saves approximately 150~milli\-seconds; the speed
gains can be more significant for larger scopes.
@@ -1031,7 +1051,7 @@
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
-\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
+\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
@@ -1210,26 +1230,26 @@
Trying 8 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
-\textit{list}''~= 1, \\
-\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
-\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
+\textit{list\/}''~= 1, \\
+\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
-\textit{list}''~= 2, \\
-\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
-\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
+\textit{list\/}''~= 2, \\
+\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
\textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
-\textit{list}''~= 8, \\
-\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
-\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
+\textit{list\/}''~= 8, \\
+\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
\\[2\smallskipamount]
Nitpick found a counterexample for
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
-\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
-\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
+\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
@@ -1850,7 +1870,7 @@
The number of options can be overwhelming at first glance. Do not let that worry
you: Nitpick's defaults have been chosen so that it almost always does the right
thing, and the most important options have been covered in context in
-\S\ref{overview}.
+\S\ref{first-steps}.
The descriptions below refer to the following syntactic quantities:
@@ -1901,7 +1921,7 @@
\textbf{Warning:} If the option is set to \textit{true}, Nitpick might
nonetheless ignore some polymorphic axioms. Counterexamples generated under
-these conditions are tagged as ``likely genuine.'' The \textit{debug}
+these conditions are tagged as ``quasi genuine.'' The \textit{debug}
(\S\ref{output-format}) option can be used to find out which axioms were
considered.
@@ -2002,7 +2022,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
predicate as if it were well-founded. Since this is generally not sound when the
-predicate is not well-founded, the counterexamples are tagged as ``likely
+predicate is not well-founded, the counterexamples are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
@@ -2050,7 +2070,7 @@
of $-1$ means that no predicate is generated, in which case Nitpick performs an
after-the-fact check to see if the known coinductive datatype values are
bidissimilar. If two values are found to be bisimilar, the counterexample is
-tagged as ``likely genuine.'' The iteration counts are automatically bounded by
+tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
the sum of the cardinalities of the coinductive datatypes occurring in the
formula to falsify.
@@ -2100,7 +2120,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
-unsound, counterexamples generated under these conditions are tagged as ``likely
+unsound, counterexamples generated under these conditions are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
@@ -2202,11 +2222,9 @@
Specifies the maximum number of potential counterexamples to display. Setting
this option to 0 speeds up the search for a genuine counterexample. This option
is implicitly set to 0 for automatic runs. If you set this option to a value
-greater than 1, you will need an incremental SAT solver: For efficiency, it is
-recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
-\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
-identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
-enabled.
+greater than 1, you will need an incremental SAT solver, such as
+\textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
+the counterexamples may be identical.
\nopagebreak
{\small See also \textit{check\_potential} (\S\ref{authentication}) and
@@ -2214,11 +2232,9 @@
\opdefault{max\_genuine}{int}{$\mathbf{1}$}
Specifies the maximum number of genuine counterexamples to display. If you set
-this option to a value greater than 1, you will need an incremental SAT solver:
-For efficiency, it is recommended to install the JNI version of MiniSat and set
-\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
-counterexamples may look identical, unless the \textit{show\_all}
-(\S\ref{output-format}) option is enabled.
+this option to a value greater than 1, you will need an incremental SAT solver,
+such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
+many of the counterexamples may be identical.
\nopagebreak
{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
@@ -2268,7 +2284,7 @@
{\small See also \textit{max\_potential} (\S\ref{output-format}).}
\opfalse{check\_genuine}{trust\_genuine}
-Specifies whether genuine and likely genuine counterexamples should be given to
+Specifies whether genuine and quasi genuine counterexamples should be given to
Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
counterexample is shown to be spurious, the user is kindly asked to send a bug
report to the author at
@@ -2282,7 +2298,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
-\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
+\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
genuine'' counterexample (i.e., a counterexample that is genuine unless
it contradicts a missing axiom or a dangerous option was used inappropriately).
\item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
@@ -2313,63 +2329,77 @@
The supported solvers are listed below:
+\let\foo
+
\begin{enum}
\item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
-executable. The \cpp{} sources and executables for MiniSat are available at
+executable.%
+\footnote{Important note for Cygwin users: The path must be specified using
+native Windows syntax. Make sure to escape backslashes properly.%
+\label{cygwin-paths}}
+The \cpp{} sources and executables for MiniSat are available at
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.0 beta (2007-07-21).
\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
-version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
-you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
+version of MiniSat is bundled with Kodkodi and is precompiled for the major
+platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
+which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
version of MiniSat, the JNI version can be used incrementally.
-%%% No longer true:
-%%% "It is bundled with Kodkodi and requires no further installation or
-%%% configuration steps. Alternatively,"
\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
written in C. You can install a standard version of
PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
-that contains the \texttt{picosat} executable. The C sources for PicoSAT are
+that contains the \texttt{picosat} executable.%
+\footref{cygwin-paths}
+The C sources for PicoSAT are
available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
Nitpick has been tested with version 913.
\item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
-the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
-and executables for zChaff are available at
+the directory that contains the \texttt{zchaff} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources and executables for zChaff are available at
\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
versions 2004-05-13, 2004-11-15, and 2007-03-12.
\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
-bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
-Kodkod's web site \cite{kodkod-2009}.
+bundled with Kodkodi and is precompiled for the major
+platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
+which you will find on Kodkod's web site \cite{kodkod-2009}.
\item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
-directory that contains the \texttt{rsat} executable. The \cpp{} sources for
-RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
-tested with version 2.01.
+directory that contains the \texttt{rsat} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources for RSat are available at
+\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
+2.01.
\item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
written in C. To use BerkMin, set the environment variable
\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
-executable. The BerkMin executables are available at
+executable.\footref{cygwin-paths}
+The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
version of BerkMin, set the environment variable
\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
-executable.
+executable.%
+\footref{cygwin-paths}
\item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
written in C. To use Jerusat, set the environment variable
\texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
-executable. The C sources for Jerusat are available at
+executable.%
+\footref{cygwin-paths}
+The C sources for Jerusat are available at
\url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
\item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
@@ -2384,7 +2414,9 @@
\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
experimental solver written in \cpp. To use HaifaSat, set the environment
variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
-\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
+\texttt{HaifaSat} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources for HaifaSat are available at
\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
@@ -2609,7 +2641,7 @@
then Nitpick assumes that the definition was made using an inductive package and
based on the introduction rules marked with \textit{nitpick\_\allowbreak
-ind\_\allowbreak intros} tries to determine whether the definition is
+\allowbreak intros} tries to determine whether the definition is
well-founded.
\end{enum}
\end{enum}
@@ -2651,7 +2683,8 @@
Nitpick provides a rich Standard ML interface used mainly for internal purposes
and debugging. Among the most interesting functions exported by Nitpick are
those that let you invoke the tool programmatically and those that let you
-register and unregister custom coinductive datatypes.
+register and unregister custom coinductive datatypes as well as term
+postprocessors.
\subsection{Invocation of Nitpick}
\label{invocation-of-nitpick}
@@ -2668,7 +2701,7 @@
\postw
The return value is a new proof state paired with an outcome string
-(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
+(``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
\textit{params} type is a large record that lets you set Nitpick's options. The
current default options can be retrieved by calling the following function
defined in the \textit{Nitpick\_Isar} structure:
@@ -2682,7 +2715,7 @@
put into a \textit{params} record. Here is an example:
\prew
-$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
+$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
& \textit{state}~\textit{params}~\textit{false} \\[-2pt]
& \textit{subgoal}\end{aligned}$
@@ -2713,7 +2746,7 @@
\prew
$\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
& \textit{Nitpick.register\_codatatype} \\[-2pt]
-& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
+& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
& \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
\postw
@@ -2727,7 +2760,7 @@
\prew
$\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
-\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
+\kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$
\postw
Inductive datatypes can be registered as coinductive datatypes, given
@@ -2735,6 +2768,26 @@
the use of the inductive constructors---Nitpick will generate an error if they
are needed.
+\subsection{Registration of Term Postprocessors}
+\label{registration-of-term-postprocessors}
+
+It is possible to change the output of any term that Nitpick considers a
+datatype by registering a term postprocessor. The interface for registering and
+unregistering postprocessors consists of the following pair of functions defined
+in the \textit{Nitpick} structure:
+
+\prew
+$\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
+$\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
+$\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
+$\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\,
+\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
+\postw
+
+\S\ref{typedefs-quotient-types-records-rationals-and-reals} and
+\texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
+
\section{Known Bugs and Limitations}
\label{known-bugs-and-limitations}
--- a/src/HOL/Auth/TLS.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Auth/TLS.thy Thu Mar 11 17:39:45 2010 +0100
@@ -41,7 +41,7 @@
header{*The TLS Protocol: Transport Layer Security*}
-theory TLS imports Public Nat_Int_Bij begin
+theory TLS imports Public Nat_Bijection begin
definition certificate :: "[agent,key] => msg" where
"certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
@@ -74,19 +74,17 @@
specification (PRF)
inj_PRF: "inj PRF"
--{*the pseudo-random function is collision-free*}
- apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"])
- apply (simp add: inj_on_def)
- apply (blast dest!: nat2_to_nat_inj [THEN injD])
+ apply (rule exI [of _ "%(x,y,z). prod_encode(x, prod_encode(y,z))"])
+ apply (simp add: inj_on_def prod_encode_eq)
done
specification (sessionK)
inj_sessionK: "inj sessionK"
--{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
apply (rule exI [of _
- "%((x,y,z), r). nat2_to_nat(role_case 0 1 r,
- nat2_to_nat(x, nat2_to_nat(y,z)))"])
- apply (simp add: inj_on_def split: role.split)
- apply (blast dest!: nat2_to_nat_inj [THEN injD])
+ "%((x,y,z), r). prod_encode(role_case 0 1 r,
+ prod_encode(x, prod_encode(y,z)))"])
+ apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
axioms
--- a/src/HOL/Code_Numeral.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Mar 11 17:39:45 2010 +0100
@@ -247,7 +247,7 @@
"nat_of i = nat_of_aux i 0"
by (simp add: nat_of_aux_def)
-definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
+definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
[code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
lemma [code]:
--- a/src/HOL/IsaMakefile Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 11 17:39:45 2010 +0100
@@ -394,7 +394,7 @@
Library/Inner_Product.thy Library/Kleene_Algebra.thy \
Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
- Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy \
+ Library/State_Monad.thy Library/Multiset.thy \
Library/Permutation.thy Library/Quotient_Type.thy \
Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
Library/README.html Library/Continuity.thy \
@@ -416,6 +416,7 @@
Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
Library/Quotient_Option.thy Library/Quotient_Product.thy \
Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
+ Library/Nat_Bijection.thy \
$(SRC)/Tools/float.ML \
$(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
--- a/src/HOL/Library/Countable.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Library/Countable.thy Thu Mar 11 17:39:45 2010 +0100
@@ -5,7 +5,7 @@
header {* Encoding (almost) everything into natural numbers *}
theory Countable
-imports Main Rat Nat_Int_Bij
+imports Main Rat Nat_Bijection
begin
subsection {* The class of countable types *}
@@ -48,7 +48,7 @@
subsection {* Countable types *}
instance nat :: countable
- by (rule countable_classI [of "id"]) simp
+ by (rule countable_classI [of "id"]) simp
subclass (in finite) countable
proof
@@ -63,47 +63,9 @@
text {* Pairs *}
-primrec sum :: "nat \<Rightarrow> nat"
-where
- "sum 0 = 0"
-| "sum (Suc n) = Suc n + sum n"
-
-lemma sum_arith: "sum n = n * Suc n div 2"
- by (induct n) auto
-
-lemma sum_mono: "n \<ge> m \<Longrightarrow> sum n \<ge> sum m"
- by (induct n m rule: diff_induct) auto
-
-definition
- "pair_encode = (\<lambda>(m, n). sum (m + n) + m)"
-
-lemma inj_pair_cencode: "inj pair_encode"
- unfolding pair_encode_def
-proof (rule injI, simp only: split_paired_all split_conv)
- fix a b c d
- assume eq: "sum (a + b) + a = sum (c + d) + c"
- have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
- then
- show "(a, b) = (c, d)"
- proof (elim disjE)
- assume sumeq: "a + b = c + d"
- then have "a = c" using eq by auto
- moreover from sumeq this have "b = d" by auto
- ultimately show ?thesis by simp
- next
- assume "a + b \<ge> Suc (c + d)"
- from sum_mono[OF this] eq
- show ?thesis by auto
- next
- assume "c + d \<ge> Suc (a + b)"
- from sum_mono[OF this] eq
- show ?thesis by auto
- qed
-qed
-
instance "*" :: (countable, countable) countable
-by (rule countable_classI [of "\<lambda>(x, y). pair_encode (to_nat x, to_nat y)"])
- (auto dest: injD [OF inj_pair_cencode] injD [OF inj_to_nat])
+ by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
+ (auto simp add: prod_encode_eq)
text {* Sums *}
@@ -111,76 +73,28 @@
instance "+":: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
- (auto split:sum.splits)
+ (simp split: sum.split_asm)
text {* Integers *}
-lemma int_cases: "(i::int) = 0 \<or> i < 0 \<or> i > 0"
-by presburger
-
-lemma int_pos_neg_zero:
- obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
- | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
- | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
-apply atomize_elim
-apply (insert int_cases[of z])
-apply (auto simp:zsgn_def)
-apply (rule_tac x="nat (-z)" in exI, simp)
-apply (rule_tac x="nat z" in exI, simp)
-done
-
instance int :: countable
-proof (rule countable_classI [of "(\<lambda>i. to_nat (nat (sgn i + 1), nat (abs i)))"],
- auto dest: injD [OF inj_to_nat])
- fix x y
- assume a: "nat (sgn x + 1) = nat (sgn y + 1)" "nat (abs x) = nat (abs y)"
- show "x = y"
- proof (cases rule: int_pos_neg_zero[of x])
- case zero
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- next
- case (pos n)
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- next
- case (neg n)
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- qed
-qed
+ by (rule countable_classI [of "int_encode"])
+ (simp add: int_encode_eq)
text {* Options *}
instance option :: (countable) countable
-by (rule countable_classI[of "\<lambda>x. case x of None \<Rightarrow> 0
- | Some y \<Rightarrow> Suc (to_nat y)"])
- (auto split:option.splits)
+ by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
+ (simp split: option.split_asm)
text {* Lists *}
-lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
- by (simp add: comp_def)
-
-primrec
- list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
-where
- "list_encode [] = 0"
-| "list_encode (x#xs) = Suc (to_nat (x, list_encode xs))"
-
instance list :: (countable) countable
-proof (rule countable_classI [of "list_encode"])
- fix xs ys :: "'a list"
- assume cenc: "list_encode xs = list_encode ys"
- then show "xs = ys"
- proof (induct xs arbitrary: ys)
- case (Nil ys)
- with cenc show ?case by (cases ys, auto)
- next
- case (Cons x xs' ys)
- thus ?case by (cases ys) auto
- qed
-qed
+ by (rule countable_classI [of "list_encode \<circ> map to_nat"])
+ (simp add: list_encode_eq)
text {* Functions *}
@@ -200,8 +114,8 @@
subsection {* The Rationals are Countably Infinite *}
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
-"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
- in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
+"nat_to_rat_surj n = (let (a,b) = prod_decode n
+ in Fract (int_decode a) (int_decode b))"
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
unfolding surj_def
@@ -210,10 +124,9 @@
show "\<exists>n. r = nat_to_rat_surj n"
proof (cases r)
fix i j assume [simp]: "r = Fract i j" and "j > 0"
- have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
- in nat_to_rat_surj(nat2_to_nat (m,n)))"
- using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
- by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
+ have "r = (let m = int_encode i; n = int_encode j
+ in nat_to_rat_surj(prod_encode (m,n)))"
+ by (simp add: Let_def nat_to_rat_surj_def)
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
qed
qed
--- a/src/HOL/Library/Dlist.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Library/Dlist.thy Thu Mar 11 17:39:45 2010 +0100
@@ -123,8 +123,6 @@
"list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
by (simp add: filter_def)
-declare null_def [code] member_def [code] length_def [code] fold_def [code] -- {* explicit is better than implicit *}
-
section {* Implementation of sets by distinct lists -- canonical! *}
--- a/src/HOL/Library/Efficient_Nat.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Mar 11 17:39:45 2010 +0100
@@ -400,7 +400,7 @@
(SML "IntInf.max/ (/0,/ _)")
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
-text {* For Haskell ans Scala, things are slightly different again. *}
+text {* For Haskell and Scala, things are slightly different again. *}
code_const int and nat
(Haskell "toInteger" and "fromInteger")
--- a/src/HOL/Library/Multiset.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Mar 11 17:39:45 2010 +0100
@@ -1729,4 +1729,33 @@
"M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
by (fact multiset_order.less_asym)
+ML {*
+(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
+fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
+ (Const _ $ t') =
+ let
+ val (maybe_opt, ps) =
+ Nitpick_Model.dest_plain_fun t' ||> op ~~
+ ||> map (apsnd (snd o HOLogic.dest_number))
+ fun elems_for t =
+ case AList.lookup (op =) ps t of
+ SOME n => replicate n t
+ | NONE => [Const (maybe_name, elem_T --> elem_T) $ t]
+ in
+ case maps elems_for (all_values elem_T) @
+ (if maybe_opt then [Const (Nitpick_Model.unrep, elem_T)] else []) of
+ [] => Const (@{const_name zero_class.zero}, T)
+ | ts => foldl1 (fn (t1, t2) =>
+ Const (@{const_name plus_class.plus}, T --> T --> T)
+ $ t1 $ t2)
+ (map (curry (op $) (Const (@{const_name single},
+ elem_T --> T))) ts)
+ end
+ | multiset_postproc _ _ _ _ t = t
+*}
+
+setup {*
+Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
+*}
+
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Nat_Bijection.thy Thu Mar 11 17:39:45 2010 +0100
@@ -0,0 +1,370 @@
+(* Title: HOL/Nat_Bijection.thy
+ Author: Brian Huffman
+ Author: Florian Haftmann
+ Author: Stefan Richter
+ Author: Tobias Nipkow
+ Author: Alexander Krauss
+*)
+
+header {* Bijections between natural numbers and other types *}
+
+theory Nat_Bijection
+imports Main Parity
+begin
+
+subsection {* Type @{typ "nat \<times> nat"} *}
+
+text "Triangle numbers: 0, 1, 3, 6, 10, 15, ..."
+
+definition
+ triangle :: "nat \<Rightarrow> nat"
+where
+ "triangle n = n * Suc n div 2"
+
+lemma triangle_0 [simp]: "triangle 0 = 0"
+unfolding triangle_def by simp
+
+lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n"
+unfolding triangle_def by simp
+
+definition
+ prod_encode :: "nat \<times> nat \<Rightarrow> nat"
+where
+ "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)"
+
+text {* In this auxiliary function, @{term "triangle k + m"} is an invariant. *}
+
+fun
+ prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+where
+ "prod_decode_aux k m =
+ (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))"
+
+declare prod_decode_aux.simps [simp del]
+
+definition
+ prod_decode :: "nat \<Rightarrow> nat \<times> nat"
+where
+ "prod_decode = prod_decode_aux 0"
+
+lemma prod_encode_prod_decode_aux:
+ "prod_encode (prod_decode_aux k m) = triangle k + m"
+apply (induct k m rule: prod_decode_aux.induct)
+apply (subst prod_decode_aux.simps)
+apply (simp add: prod_encode_def)
+done
+
+lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
+unfolding prod_decode_def by (simp add: prod_encode_prod_decode_aux)
+
+lemma prod_decode_triangle_add:
+ "prod_decode (triangle k + m) = prod_decode_aux k m"
+apply (induct k arbitrary: m)
+apply (simp add: prod_decode_def)
+apply (simp only: triangle_Suc add_assoc)
+apply (subst prod_decode_aux.simps, simp)
+done
+
+lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x"
+unfolding prod_encode_def
+apply (induct x)
+apply (simp add: prod_decode_triangle_add)
+apply (subst prod_decode_aux.simps, simp)
+done
+
+lemma inj_prod_encode: "inj_on prod_encode A"
+by (rule inj_on_inverseI, rule prod_encode_inverse)
+
+lemma inj_prod_decode: "inj_on prod_decode A"
+by (rule inj_on_inverseI, rule prod_decode_inverse)
+
+lemma surj_prod_encode: "surj prod_encode"
+by (rule surjI, rule prod_decode_inverse)
+
+lemma surj_prod_decode: "surj prod_decode"
+by (rule surjI, rule prod_encode_inverse)
+
+lemma bij_prod_encode: "bij prod_encode"
+by (rule bijI [OF inj_prod_encode surj_prod_encode])
+
+lemma bij_prod_decode: "bij prod_decode"
+by (rule bijI [OF inj_prod_decode surj_prod_decode])
+
+lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
+by (rule inj_prod_encode [THEN inj_eq])
+
+lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
+by (rule inj_prod_decode [THEN inj_eq])
+
+text {* Ordering properties *}
+
+lemma le_prod_encode_1: "a \<le> prod_encode (a, b)"
+unfolding prod_encode_def by simp
+
+lemma le_prod_encode_2: "b \<le> prod_encode (a, b)"
+unfolding prod_encode_def by (induct b, simp_all)
+
+
+subsection {* Type @{typ "nat + nat"} *}
+
+definition
+ sum_encode :: "nat + nat \<Rightarrow> nat"
+where
+ "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))"
+
+definition
+ sum_decode :: "nat \<Rightarrow> nat + nat"
+where
+ "sum_decode n = (if even n then Inl (n div 2) else Inr (n div 2))"
+
+lemma sum_encode_inverse [simp]: "sum_decode (sum_encode x) = x"
+unfolding sum_decode_def sum_encode_def
+by (induct x) simp_all
+
+lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
+unfolding sum_decode_def sum_encode_def numeral_2_eq_2
+by (simp add: even_nat_div_two_times_two odd_nat_div_two_times_two_plus_one
+ del: mult_Suc)
+
+lemma inj_sum_encode: "inj_on sum_encode A"
+by (rule inj_on_inverseI, rule sum_encode_inverse)
+
+lemma inj_sum_decode: "inj_on sum_decode A"
+by (rule inj_on_inverseI, rule sum_decode_inverse)
+
+lemma surj_sum_encode: "surj sum_encode"
+by (rule surjI, rule sum_decode_inverse)
+
+lemma surj_sum_decode: "surj sum_decode"
+by (rule surjI, rule sum_encode_inverse)
+
+lemma bij_sum_encode: "bij sum_encode"
+by (rule bijI [OF inj_sum_encode surj_sum_encode])
+
+lemma bij_sum_decode: "bij sum_decode"
+by (rule bijI [OF inj_sum_decode surj_sum_decode])
+
+lemma sum_encode_eq: "sum_encode x = sum_encode y \<longleftrightarrow> x = y"
+by (rule inj_sum_encode [THEN inj_eq])
+
+lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y"
+by (rule inj_sum_decode [THEN inj_eq])
+
+
+subsection {* Type @{typ "int"} *}
+
+definition
+ int_encode :: "int \<Rightarrow> nat"
+where
+ "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))"
+
+definition
+ int_decode :: "nat \<Rightarrow> int"
+where
+ "int_decode n = (case sum_decode n of Inl a \<Rightarrow> int a | Inr b \<Rightarrow> - int b - 1)"
+
+lemma int_encode_inverse [simp]: "int_decode (int_encode x) = x"
+unfolding int_decode_def int_encode_def by simp
+
+lemma int_decode_inverse [simp]: "int_encode (int_decode n) = n"
+unfolding int_decode_def int_encode_def using sum_decode_inverse [of n]
+by (cases "sum_decode n", simp_all)
+
+lemma inj_int_encode: "inj_on int_encode A"
+by (rule inj_on_inverseI, rule int_encode_inverse)
+
+lemma inj_int_decode: "inj_on int_decode A"
+by (rule inj_on_inverseI, rule int_decode_inverse)
+
+lemma surj_int_encode: "surj int_encode"
+by (rule surjI, rule int_decode_inverse)
+
+lemma surj_int_decode: "surj int_decode"
+by (rule surjI, rule int_encode_inverse)
+
+lemma bij_int_encode: "bij int_encode"
+by (rule bijI [OF inj_int_encode surj_int_encode])
+
+lemma bij_int_decode: "bij int_decode"
+by (rule bijI [OF inj_int_decode surj_int_decode])
+
+lemma int_encode_eq: "int_encode x = int_encode y \<longleftrightarrow> x = y"
+by (rule inj_int_encode [THEN inj_eq])
+
+lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y"
+by (rule inj_int_decode [THEN inj_eq])
+
+
+subsection {* Type @{typ "nat list"} *}
+
+fun
+ list_encode :: "nat list \<Rightarrow> nat"
+where
+ "list_encode [] = 0"
+| "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))"
+
+function
+ list_decode :: "nat \<Rightarrow> nat list"
+where
+ "list_decode 0 = []"
+| "list_decode (Suc n) = (case prod_decode n of (x, y) \<Rightarrow> x # list_decode y)"
+by pat_completeness auto
+
+termination list_decode
+apply (relation "measure id", simp_all)
+apply (drule arg_cong [where f="prod_encode"])
+apply (simp add: le_imp_less_Suc le_prod_encode_2)
+done
+
+lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
+by (induct x rule: list_encode.induct) simp_all
+
+lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n"
+apply (induct n rule: list_decode.induct, simp)
+apply (simp split: prod.split)
+apply (simp add: prod_decode_eq [symmetric])
+done
+
+lemma inj_list_encode: "inj_on list_encode A"
+by (rule inj_on_inverseI, rule list_encode_inverse)
+
+lemma inj_list_decode: "inj_on list_decode A"
+by (rule inj_on_inverseI, rule list_decode_inverse)
+
+lemma surj_list_encode: "surj list_encode"
+by (rule surjI, rule list_decode_inverse)
+
+lemma surj_list_decode: "surj list_decode"
+by (rule surjI, rule list_encode_inverse)
+
+lemma bij_list_encode: "bij list_encode"
+by (rule bijI [OF inj_list_encode surj_list_encode])
+
+lemma bij_list_decode: "bij list_decode"
+by (rule bijI [OF inj_list_decode surj_list_decode])
+
+lemma list_encode_eq: "list_encode x = list_encode y \<longleftrightarrow> x = y"
+by (rule inj_list_encode [THEN inj_eq])
+
+lemma list_decode_eq: "list_decode x = list_decode y \<longleftrightarrow> x = y"
+by (rule inj_list_decode [THEN inj_eq])
+
+
+subsection {* Finite sets of naturals *}
+
+subsubsection {* Preliminaries *}
+
+lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
+apply (safe intro!: finite_vimageI inj_Suc)
+apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
+apply (rule subsetI, case_tac x, simp, simp)
+apply (rule finite_insert [THEN iffD2])
+apply (erule finite_imageI)
+done
+
+lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
+by auto
+
+lemma vimage_Suc_insert_Suc:
+ "Suc -` insert (Suc n) A = insert n (Suc -` A)"
+by auto
+
+lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
+by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
+
+lemma div2_even_ext_nat:
+ "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
+apply (rule mod_div_equality [of x 2, THEN subst])
+apply (rule mod_div_equality [of y 2, THEN subst])
+apply (case_tac "even x")
+apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
+apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
+done
+
+subsubsection {* From sets to naturals *}
+
+definition
+ set_encode :: "nat set \<Rightarrow> nat"
+where
+ "set_encode = setsum (op ^ 2)"
+
+lemma set_encode_empty [simp]: "set_encode {} = 0"
+by (simp add: set_encode_def)
+
+lemma set_encode_insert [simp]:
+ "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
+by (simp add: set_encode_def)
+
+lemma even_set_encode_iff: "finite A \<Longrightarrow> even (set_encode A) \<longleftrightarrow> 0 \<notin> A"
+unfolding set_encode_def by (induct set: finite, auto)
+
+lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2"
+apply (cases "finite A")
+apply (erule finite_induct, simp)
+apply (case_tac x)
+apply (simp add: even_nat_Suc_div_2 even_set_encode_iff vimage_Suc_insert_0)
+apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
+apply (simp add: set_encode_def finite_vimage_Suc_iff)
+done
+
+lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
+
+subsubsection {* From naturals to sets *}
+
+definition
+ set_decode :: "nat \<Rightarrow> nat set"
+where
+ "set_decode x = {n. odd (x div 2 ^ n)}"
+
+lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x"
+by (simp add: set_decode_def)
+
+lemma set_decode_Suc [simp]:
+ "Suc n \<in> set_decode x \<longleftrightarrow> n \<in> set_decode (x div 2)"
+by (simp add: set_decode_def div_mult2_eq)
+
+lemma set_decode_zero [simp]: "set_decode 0 = {}"
+by (simp add: set_decode_def)
+
+lemma set_decode_div_2: "set_decode (x div 2) = Suc -` set_decode x"
+by auto
+
+lemma set_decode_plus_power_2:
+ "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
+ apply (induct n arbitrary: z, simp_all)
+ apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
+ apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
+done
+
+lemma finite_set_decode [simp]: "finite (set_decode n)"
+apply (induct n rule: nat_less_induct)
+apply (case_tac "n = 0", simp)
+apply (drule_tac x="n div 2" in spec, simp)
+apply (simp add: set_decode_div_2)
+apply (simp add: finite_vimage_Suc_iff)
+done
+
+subsubsection {* Proof of isomorphism *}
+
+lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
+apply (induct n rule: nat_less_induct)
+apply (case_tac "n = 0", simp)
+apply (drule_tac x="n div 2" in spec, simp)
+apply (simp add: set_decode_div_2 set_encode_vimage_Suc)
+apply (erule div2_even_ext_nat)
+apply (simp add: even_set_encode_iff)
+done
+
+lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A"
+apply (erule finite_induct, simp_all)
+apply (simp add: set_decode_plus_power_2)
+done
+
+lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
+by (rule inj_on_inverseI [where g="set_decode"], simp)
+
+lemma set_encode_eq:
+ "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B"
+by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp)
+
+end
--- a/src/HOL/Library/Nat_Int_Bij.thy Thu Mar 11 15:52:35 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(* Title: HOL/Nat_Int_Bij.thy
- Author: Stefan Richter, Tobias Nipkow
-*)
-
-header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
-
-theory Nat_Int_Bij
-imports Main
-begin
-
-subsection{* A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
-
-text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
-
-definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
-"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
-definition nat_to_nat2:: "nat \<Rightarrow> (nat * nat)" where
-"nat_to_nat2 = inv nat2_to_nat"
-
-lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
-proof (cases "2 dvd a")
- case True
- then show ?thesis by (rule dvd_mult2)
-next
- case False
- then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
- then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
- then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
- then show ?thesis by (rule dvd_mult)
-qed
-
-lemma
- assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
- shows nat2_to_nat_help: "u+v \<le> x+y"
-proof (rule classical)
- assume "\<not> ?thesis"
- then have contrapos: "x+y < u+v"
- by simp
- have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
- by (unfold nat2_to_nat_def) (simp add: Let_def)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
- by (simp only: div_mult_self1_is_m)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
- + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
- proof -
- have "2 dvd (x+y)*Suc(x+y)"
- by (rule dvd2_a_x_suc_a)
- then have "(x+y)*Suc(x+y) mod 2 = 0"
- by (simp only: dvd_eq_mod_eq_0)
- also
- have "2 * Suc(x+y) mod 2 = 0"
- by (rule mod_mult_self1_is_0)
- ultimately have
- "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
- by simp
- then show ?thesis
- by simp
- qed
- also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
- by (rule div_add1_eq [symmetric])
- also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
- by (simp only: add_mult_distrib [symmetric])
- also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
- by (simp only: mult_le_mono div_le_mono)
- also have "\<dots> \<le> nat2_to_nat (u,v)"
- by (unfold nat2_to_nat_def) (simp add: Let_def)
- finally show ?thesis
- by (simp only: eq)
-qed
-
-theorem nat2_to_nat_inj: "inj nat2_to_nat"
-proof -
- {
- fix u v x y
- assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
- then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
- also from eq1 [symmetric] have "x+y \<le> u+v"
- by (rule nat2_to_nat_help)
- finally have eq2: "u+v = x+y" .
- with eq1 have ux: "u=x"
- by (simp add: nat2_to_nat_def Let_def)
- with eq2 have vy: "v=y" by simp
- with ux have "(u,v) = (x,y)" by simp
- }
- then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
- then show ?thesis unfolding inj_on_def by simp
-qed
-
-lemma nat_to_nat2_surj: "surj nat_to_nat2"
-by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
-
-
-lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
-using gauss_sum[where 'a = nat]
-by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
-
-lemma nat2_to_nat_surj: "surj nat2_to_nat"
-proof (unfold surj_def)
- {
- fix z::nat
- def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}"
- def x \<equiv> "z - (\<Sum>i\<le>r. i)"
-
- hence "finite {r. (\<Sum>i\<le>r. i) \<le> z}"
- by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
- also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}" by simp
- hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}" by fast
- ultimately have a: "r \<in> {r. (\<Sum>i\<le>r. i) \<le> z} \<and> (\<forall>s \<in> {r. (\<Sum>i\<le>r. i) \<le> z}. s \<le> r)"
- by (simp add: r_def del:mem_Collect_eq)
- {
- assume "r<x"
- hence "r+1\<le>x" by simp
- hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z" using x_def by arith
- hence "(r+1) \<in> {r. (\<Sum>i\<le>r. i) \<le> z}" by simp
- with a have "(r+1)\<le>r" by simp
- }
- hence b: "x\<le>r" by force
-
- def y \<equiv> "r-x"
- have "2*z=2*(\<Sum>i\<le>r. i)+2*x" using x_def a by simp arith
- also have "\<dots> = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp
- also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
- also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp }
- hence "\<dots> = 2 * nat2_to_nat(x,y)"
- using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
- finally have "z=nat2_to_nat (x, y)" by simp
- }
- thus "\<forall>y. \<exists>x. y = nat2_to_nat x" by fast
-qed
-
-lemma nat_to_nat2_inj: "inj nat_to_nat2"
- by (simp add: nat_to_nat2_def surj_imp_inj_inv nat2_to_nat_surj)
-
-
-subsection{* A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
-
-definition nat_to_int_bij :: "nat \<Rightarrow> int" where
-"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
-
-definition int_to_nat_bij :: "int \<Rightarrow> nat" where
-"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
-
-lemma i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
-by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
-
-lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
-proof -
- have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
- thus ?thesis
- by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
-qed
-
-lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
-by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
-
-lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
-by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
-
-lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
-by (blast intro: n2i_i2n_id surjI)
-
-lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
-by (blast intro: i2n_n2i_id surjI)
-
-lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
-by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
-
-lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
-by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
-
-lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
-by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
-
-lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
-by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
-
-
-end
--- a/src/HOL/Nitpick.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Nitpick.thy Thu Mar 11 17:39:45 2010 +0100
@@ -96,10 +96,10 @@
else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
-"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
+"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
-"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Mar 11 17:39:45 2010 +0100
@@ -206,4 +206,39 @@
nitpick [binary_ints, expect = none]
sorry
+datatype tree = Null | Node nat tree tree
+
+primrec labels where
+"labels Null = {}" |
+"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
+
+lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "labels (Node x t u) \<noteq> {}"
+nitpick [expect = none]
+oops
+
+lemma "card (labels t) > 0"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = none]
+nitpick [dont_finitize, expect = none]
+sorry
+
+lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = none]
+oops
+
end
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 17:39:45 2010 +0100
@@ -13,7 +13,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 15 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
subsection {* 3.1. Propositional Logic *}
@@ -117,6 +117,20 @@
nitpick [show_datatypes, expect = genuine]
oops
+ML {*
+(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
+fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
+ HOLogic.mk_number T (snd (HOLogic.dest_number t1)
+ - snd (HOLogic.dest_number t2))
+ | my_int_postproc _ _ _ _ t = t
+*}
+
+setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
+
+lemma "add x y = add x x"
+nitpick [show_datatypes]
+oops
+
record point =
Xcoord :: int
Ycoord :: int
@@ -136,11 +150,11 @@
"even n \<Longrightarrow> even (Suc (Suc n))"
lemma "\<exists>n. even n \<and> even (Suc n)"
-nitpick [card nat = 100, unary_ints, verbose, expect = potential]
+nitpick [card nat = 50, unary_ints, verbose, expect = potential]
oops
-lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
-nitpick [card nat = 100, unary_ints, verbose, expect = genuine]
+lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
+nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
oops
inductive even' where
@@ -243,7 +257,7 @@
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
subsection {* 3.11. Scope Monotonicity *}
@@ -317,7 +331,7 @@
case Leaf thus ?case by simp
next
case (Branch t u) thus ?case
- nitpick [non_std, show_all]
+ nitpick [non_std, card = 1\<midarrow>5, expect = none]
by auto
qed
@@ -365,7 +379,7 @@
theorem S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>3_complete:
@@ -384,19 +398,19 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
subsection {* 4.2. AA Trees *}
@@ -450,13 +464,13 @@
theorem dataset_skew_split:
"dataset (skew t) = dataset t"
"dataset (split t) = dataset t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem wf_skew_split:
"wf t \<Longrightarrow> skew t = t"
"wf t \<Longrightarrow> split t = t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
primrec insort\<^isub>1 where
@@ -480,11 +494,11 @@
(if x > y then insort\<^isub>2 u x else u))"
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
end
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Mar 11 17:39:45 2010 +0100
@@ -24,8 +24,6 @@
fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
*}
-ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
-
ML {* genuine 1 @{prop "x = Not"} *}
ML {* none 1 @{prop "\<exists>x. x = Not"} *}
ML {* none 1 @{prop "\<not> False"} *}
--- a/src/HOL/Probability/Borel.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Probability/Borel.thy Thu Mar 11 17:39:45 2010 +0100
@@ -15,11 +15,6 @@
definition indicator_fn where
"indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
-definition mono_convergent where
- "mono_convergent u f s \<equiv>
- (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
- (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
-
lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
sigma_algebra M \<and>
@@ -191,20 +186,20 @@
definition
nat_to_rat_surj :: "nat \<Rightarrow> rat" where
- "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
- in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
+ "nat_to_rat_surj n = (let (i,j) = prod_decode n
+ in Fract (int_decode i) (int_decode j))"
lemma nat_to_rat_surj: "surj nat_to_rat_surj"
proof (auto simp add: surj_def nat_to_rat_surj_def)
fix y
- show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
+ show "\<exists>x. y = (\<lambda>(i, j). Fract (int_decode i) (int_decode j)) (prod_decode x)"
proof (cases y)
case (Fract a b)
- obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
+ obtain i where i: "int_decode i = a" using surj_int_decode
by (metis surj_def)
- obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
+ obtain j where j: "int_decode j = b" using surj_int_decode
by (metis surj_def)
- obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
+ obtain n where n: "prod_decode n = (i,j)" using surj_prod_decode
by (metis surj_def)
from Fract i j n show ?thesis
@@ -375,6 +370,95 @@
by (fast intro: borel_measurable_add_borel_measurable
borel_measurable_uminus_borel_measurable f g)
+lemma (in measure_space) borel_measurable_setsum_borel_measurable:
+ assumes s: "finite s"
+ shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
+proof (induct s)
+ case empty
+ thus ?case
+ by (simp add: borel_measurable_const)
+next
+ case (insert x s)
+ thus ?case
+ by (auto simp add: borel_measurable_add_borel_measurable)
+qed
+
+lemma (in measure_space) borel_measurable_cong:
+ assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
+ shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
+using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
+
+lemma (in measure_space) borel_measurable_inverse:
+ assumes "f \<in> borel_measurable M"
+ shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
+ unfolding borel_measurable_ge_iff
+proof (safe, rule linorder_cases)
+ fix a :: real assume "0 < a"
+ { fix w
+ from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
+ by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
+ linorder_not_le real_le_refl real_le_trans real_less_def
+ xt1(7) zero_less_divide_1_iff) }
+ hence "{w \<in> space M. a \<le> inverse (f w)} =
+ {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
+ with Int assms[unfolded borel_measurable_gr_iff]
+ assms[unfolded borel_measurable_le_iff]
+ show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+next
+ fix a :: real assume "0 = a"
+ { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
+ unfolding `0 = a`[symmetric] by auto }
+ thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
+ using assms[unfolded borel_measurable_ge_iff] by simp
+next
+ fix a :: real assume "a < 0"
+ { fix w
+ from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
+ apply (cases "0 \<le> f w")
+ apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
+ zero_le_divide_1_iff)
+ apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
+ linorder_not_le real_le_refl real_le_trans)
+ done }
+ hence "{w \<in> space M. a \<le> inverse (f w)} =
+ {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
+ with Un assms[unfolded borel_measurable_ge_iff]
+ assms[unfolded borel_measurable_le_iff]
+ show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+qed
+
+lemma (in measure_space) borel_measurable_divide:
+ assumes "f \<in> borel_measurable M"
+ and "g \<in> borel_measurable M"
+ shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+ unfolding field_divide_inverse
+ by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+
+
+section "Monotone convergence"
+
+definition mono_convergent where
+ "mono_convergent u f s \<equiv>
+ (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
+ (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+
+definition "upclose f g x = max (f x) (g x)"
+
+primrec mon_upclose where
+"mon_upclose 0 u = u 0" |
+"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
+
+lemma mono_convergentD:
+ assumes "mono_convergent u f s" and "x \<in> s"
+ shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
+ using assms unfolding mono_convergent_def by auto
+
+lemma mono_convergentI:
+ assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
+ shows "mono_convergent u f s"
+ using assms unfolding mono_convergent_def by auto
+
lemma (in measure_space) mono_convergent_borel_measurable:
assumes u: "!!n. u n \<in> borel_measurable M"
assumes mc: "mono_convergent u f (space M)"
@@ -409,44 +493,11 @@
by (auto simp add: borel_measurable_le_iff)
qed
-lemma (in measure_space) borel_measurable_setsum_borel_measurable:
- assumes s: "finite s"
- shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
-proof (induct s)
- case empty
- thus ?case
- by (simp add: borel_measurable_const)
-next
- case (insert x s)
- thus ?case
- by (auto simp add: borel_measurable_add_borel_measurable)
-qed
-
-section "Monotone convergence"
-
-lemma mono_convergentD:
- assumes "mono_convergent u f s" and "x \<in> s"
- shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
- using assms unfolding mono_convergent_def by auto
-
-
-lemma mono_convergentI:
- assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
- assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
- shows "mono_convergent u f s"
- using assms unfolding mono_convergent_def by auto
-
lemma mono_convergent_le:
assumes "mono_convergent u f s" and "t \<in> s"
shows "u n t \<le> f t"
using mono_convergentD[OF assms] by (auto intro!: incseq_le)
-definition "upclose f g x = max (f x) (g x)"
-
-primrec mon_upclose where
-"mon_upclose 0 u = u 0" |
-"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
-
lemma mon_upclose_ex:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
@@ -561,4 +612,19 @@
qed
qed
+lemma mono_conv_outgrow:
+ assumes "incseq x" "x ----> y" "z < y"
+ shows "\<exists>b. \<forall> a \<ge> b. z < x a"
+using assms
+proof -
+ from assms have "y - z > 0" by simp
+ hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
+ unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+ by simp
+ have "\<forall>m. x m \<le> y" using incseq_le assms by auto
+ hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
+ by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+ from A B show ?thesis by auto
+qed
+
end
--- a/src/HOL/Probability/Caratheodory.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Thu Mar 11 17:39:45 2010 +0100
@@ -816,9 +816,9 @@
by (simp add: eqe)
finally show ?thesis using Series.summable_le2 [OF 1 2] by auto
qed
- def C \<equiv> "(split BB) o nat_to_nat2"
+ def C \<equiv> "(split BB) o prod_decode"
have C: "!!n. C n \<in> sets M"
- apply (rule_tac p="nat_to_nat2 n" in PairE)
+ apply (rule_tac p="prod_decode n" in PairE)
apply (simp add: C_def)
apply (metis BB subsetD rangeI)
done
@@ -828,11 +828,10 @@
assume x: "x \<in> A i"
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
- thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
- by (metis nat_to_nat2_surj internal_split_def prod.cases
- prod_case_split surj_f_inv_f)
+ thus "\<exists>i. x \<in> split BB (prod_decode i)"
+ by (metis prod_encode_inverse prod.cases prod_case_split)
qed
- have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
+ have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
also have "... sums suminf ll"
proof (rule suminf_2dimen)
--- a/src/HOL/Probability/Lebesgue.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy Thu Mar 11 17:39:45 2010 +0100
@@ -25,9 +25,58 @@
shows "nonneg (neg_part f)"
unfolding nonneg_def neg_part_def min_def by auto
+lemma (in measure_space)
+ assumes "f \<in> borel_measurable M"
+ shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"
+ and neg_part_borel_measurable: "neg_part f \<in> borel_measurable M"
+using assms
+proof -
+ { fix a :: real
+ { assume asm: "0 \<le> a"
+ from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
+ have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
+ unfolding pos_part_def using assms borel_measurable_le_iff by auto
+ hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
+ moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
+ unfolding pos_part_def using empty_sets by auto
+ ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
+ using le_less_linear by auto
+ } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+ { fix a :: real
+ { assume asm: "0 \<le> a"
+ from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
+ have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
+ unfolding neg_part_def using assms borel_measurable_ge_iff by auto
+ hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
+ moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
+ moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
+ ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
+ using le_less_linear by auto
+ } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+ from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
+qed
+
+lemma (in measure_space) pos_part_neg_part_borel_measurable_iff:
+ "f \<in> borel_measurable M \<longleftrightarrow>
+ pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
+proof -
+ { fix x
+ have "f x = pos_part f x - neg_part f x"
+ unfolding pos_part_def neg_part_def unfolding max_def min_def
+ by auto }
+ hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
+ hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
+ from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]
+ borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
+ this
+ show ?thesis by auto
+qed
+
context measure_space
begin
+section "Simple discrete step function"
+
definition
"pos_simple f =
{ (s :: nat set, a, x).
@@ -40,29 +89,6 @@
definition
"psfis f = pos_simple_integral ` (pos_simple f)"
-definition
- "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
- (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
-
-definition
- "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
-
-definition
- "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
-
-definition
- "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
-
-definition
- "countable_space_integral f \<equiv>
- let e = enumerate (f ` space M) in
- suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
-
-definition
- "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
- f \<in> borel_measurable M \<and>
- (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
-
lemma pos_simpleE[consumes 1]:
assumes ps: "(s, a, x) \<in> pos_simple f"
obtains "finite s" and "nonneg f" and "nonneg x"
@@ -105,6 +131,11 @@
shows "psfis f = psfis g"
unfolding psfis_def using pos_simple_cong[OF assms] by simp
+lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
+ unfolding psfis_def pos_simple_def pos_simple_integral_def
+ by (auto simp: nonneg_def
+ intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
+
lemma pos_simple_setsum_indicator_fn:
assumes ps: "(s, a, x) \<in> pos_simple f"
and "t \<in> space M"
@@ -121,28 +152,7 @@
using `i \<in> s` by simp
qed
-lemma (in measure_space) measure_setsum_split:
- assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
- assumes "(\<Union>i \<in> r. b i) = space M"
- assumes "disjoint_family_on b r"
- shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
-proof -
- have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
- using assms by auto
- show ?thesis unfolding *
- proof (rule measure_finitely_additive''[symmetric])
- show "finite r" using `finite r` by auto
- { fix i assume "i \<in> r"
- hence "b i \<in> sets M" using br_in_M by auto
- thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
- }
- show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
- using `disjoint_family_on b r`
- unfolding disjoint_family_on_def by auto
- qed
-qed
-
-lemma (in measure_space) pos_simple_common_partition:
+lemma pos_simple_common_partition:
assumes psf: "(s, a, x) \<in> pos_simple f"
assumes psg: "(s', b, y) \<in> pos_simple g"
obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
@@ -229,7 +239,7 @@
qed
qed
-lemma (in measure_space) pos_simple_integral_equal:
+lemma pos_simple_integral_equal:
assumes psx: "(s, a, x) \<in> pos_simple f"
assumes psy: "(s', b, y) \<in> pos_simple f"
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
@@ -269,7 +279,7 @@
finally show "?left = ?right" .
qed
-lemma (in measure_space)psfis_present:
+lemma psfis_present:
assumes "A \<in> psfis f"
assumes "B \<in> psfis g"
obtains z z' c k where
@@ -295,7 +305,7 @@
qed
qed
-lemma (in measure_space) pos_simple_integral_add:
+lemma pos_simple_integral_add:
assumes "(s, a, x) \<in> pos_simple f"
assumes "(s', b, y) \<in> pos_simple g"
obtains s'' c z where
@@ -468,70 +478,6 @@
thus ?thesis using r unfolding psfis_def image_def by auto
qed
-lemma pos_simple_integral_setsum_image:
- assumes "finite P"
- assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
- obtains s' a' x' where
- "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
- "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
-using assms that
-proof (induct P arbitrary:thesis rule:finite.induct)
- case emptyI note asms = this
- def s' == "{0 :: nat}"
- def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
- def x' == "\<lambda> x :: nat. (0 :: real)"
- have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
- unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
- moreover have "pos_simple_integral (s', a', x') = 0"
- unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
- ultimately show ?case using asms by auto
-next
-
- case (insertI P c) note asms = this
- then obtain s' a' x' where
- sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
- "pos_simple_integral (s', a', x') =
- (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
- by auto
-
- { assume "c \<in> P"
- hence "P = insert c P" by auto
- hence thesis using asms sax by auto
- }
- moreover
- { assume "c \<notin> P"
- from asms obtain s'' a'' x'' where
- sax': "s'' = s c" "a'' = a c" "x'' = x c"
- "(s'', a'', x'') \<in> pos_simple (f c)" by auto
- from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
- tybbie:
- "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
- "(pos_simple_integral (s', a', x') +
- pos_simple_integral (s'', a'', x'') =
- pos_simple_integral (k, b, z))"
- using pos_simple_integral_add by blast
-
- from tybbie have
- "pos_simple_integral (k, b, z) =
- pos_simple_integral (s', a', x') +
- pos_simple_integral (s'', a'', x'')" by simp
- also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
- + pos_simple_integral (s c, a c, x c)"
- using sax sax' by auto
- also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
- using asms `c \<notin> P` by auto
- finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
- by simp
-
- have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
- using `c \<notin> P` `finite P` by auto
- hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
- using tybbie by simp
-
- from A B have thesis using asms by auto
- } ultimately show thesis by blast
-qed
-
lemma psfis_setsum_image:
assumes "finite P"
assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
@@ -577,57 +523,6 @@
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
-lemma pos_part_neg_part_borel_measurable:
- assumes "f \<in> borel_measurable M"
- shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
-using assms
-proof -
- { fix a :: real
- { assume asm: "0 \<le> a"
- from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
- have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
- unfolding pos_part_def using assms borel_measurable_le_iff by auto
- hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
- moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
- unfolding pos_part_def using empty_sets by auto
- ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
- using le_less_linear by auto
- } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
- { fix a :: real
- { assume asm: "0 \<le> a"
- from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
- have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
- unfolding neg_part_def using assms borel_measurable_ge_iff by auto
- hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
- moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
- moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
- ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
- using le_less_linear by auto
- } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
- from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
-qed
-
-lemma pos_part_neg_part_borel_measurable_iff:
- "f \<in> borel_measurable M \<longleftrightarrow>
- pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
-proof -
- { fix x
- have "f x = pos_part f x - neg_part f x"
- unfolding pos_part_def neg_part_def unfolding max_def min_def
- by auto }
- hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
- hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
- from pos_part_neg_part_borel_measurable[of f]
- borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
- this
- show ?thesis by auto
-qed
-
-lemma borel_measurable_cong:
- assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
- shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
-using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
-
lemma psfis_borel_measurable:
assumes "a \<in> psfis f"
shows "f \<in> borel_measurable M"
@@ -654,21 +549,6 @@
show ?thesis by simp
qed
-lemma mono_conv_outgrow:
- assumes "incseq x" "x ----> y" "z < y"
- shows "\<exists>b. \<forall> a \<ge> b. z < x a"
-using assms
-proof -
- from assms have "y - z > 0" by simp
- hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
- unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
- by simp
- have "\<forall>m. x m \<le> y" using incseq_le assms by auto
- hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
- by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
- from A B show ?thesis by auto
-qed
-
lemma psfis_mono_conv_mono:
assumes mono: "mono_convergent u f (space M)"
and ps_u: "\<And>n. x n \<in> psfis (u n)"
@@ -679,7 +559,6 @@
proof (rule field_le_mult_one_interval)
fix z :: real assume "0 < z" and "z < 1"
hence "0 \<le> z" by auto
-(* def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
have "incseq x" unfolding incseq_def
@@ -783,6 +662,12 @@
qed
qed
+section "Continuous posititve integration"
+
+definition
+ "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
+ (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
+
lemma psfis_nnfis:
"a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
unfolding nnfis_def mono_convergent_def incseq_def
@@ -1136,11 +1021,6 @@
show ?thesis unfolding nnfis_def by auto
qed
-lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
- unfolding psfis_def pos_simple_def pos_simple_integral_def
- by (auto simp: nonneg_def
- intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
-
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
by (auto intro: the_equality nnfis_unique)
@@ -1158,6 +1038,14 @@
show ?thesis by safe
qed
+section "Lebesgue Integral"
+
+definition
+ "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
+
+definition
+ "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
+
lemma integral_cong:
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
shows "integral f = integral g"
@@ -1203,7 +1091,7 @@
(is "\<exists>x. x \<in> nnfis ?pp \<and> _")
proof (rule nnfis_dom_conv)
show "?pp \<in> borel_measurable M"
- using borel by (rule pos_part_neg_part_borel_measurable)
+ using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
fix t assume "t \<in> space M"
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1217,7 +1105,7 @@
(is "\<exists>x. x \<in> nnfis ?np \<and> _")
proof (rule nnfis_dom_conv)
show "?np \<in> borel_measurable M"
- using borel by (rule pos_part_neg_part_borel_measurable)
+ using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
fix t assume "t \<in> space M"
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1419,6 +1307,8 @@
by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
qed
+section "Lebesgue integration on finite space"
+
lemma integral_finite_on_sets:
assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
shows "integral (\<lambda>x. f x * indicator_fn a x) =
@@ -1489,51 +1379,12 @@
qed (auto intro!: image_eqI inj_onI)
qed
-lemma borel_measurable_inverse:
- assumes "f \<in> borel_measurable M"
- shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
- unfolding borel_measurable_ge_iff
-proof (safe, rule linorder_cases)
- fix a :: real assume "0 < a"
- { fix w
- from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
- by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
- linorder_not_le real_le_refl real_le_trans real_less_def
- xt1(7) zero_less_divide_1_iff) }
- hence "{w \<in> space M. a \<le> inverse (f w)} =
- {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
- with Int assms[unfolded borel_measurable_gr_iff]
- assms[unfolded borel_measurable_le_iff]
- show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
-next
- fix a :: real assume "0 = a"
- { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
- unfolding `0 = a`[symmetric] by auto }
- thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
- using assms[unfolded borel_measurable_ge_iff] by simp
-next
- fix a :: real assume "a < 0"
- { fix w
- from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
- apply (cases "0 \<le> f w")
- apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
- zero_le_divide_1_iff)
- apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
- linorder_not_le real_le_refl real_le_trans)
- done }
- hence "{w \<in> space M. a \<le> inverse (f w)} =
- {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
- with Un assms[unfolded borel_measurable_ge_iff]
- assms[unfolded borel_measurable_le_iff]
- show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
-qed
+section "Radon–Nikodym derivative"
-lemma borel_measurable_divide:
- assumes "f \<in> borel_measurable M"
- and "g \<in> borel_measurable M"
- shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
- unfolding field_divide_inverse
- by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+definition
+ "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
+ f \<in> borel_measurable M \<and>
+ (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
lemma RN_deriv_finite_singleton:
fixes v :: "'a set \<Rightarrow> real"
@@ -1577,6 +1428,11 @@
using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
qed fact
+section "Lebesgue integration on countable spaces"
+
+definition
+ "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
+
lemma countable_space_integral_reduce:
assumes "positive M (measure M)" and "f \<in> borel_measurable M"
and "countable (f ` space M)"
--- a/src/HOL/Probability/Measure.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Probability/Measure.thy Thu Mar 11 17:39:45 2010 +0100
@@ -997,4 +997,25 @@
\<Longrightarrow> measure_space M"
by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto)
+lemma (in measure_space) measure_setsum_split:
+ assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
+ assumes "(\<Union>i \<in> r. b i) = space M"
+ assumes "disjoint_family_on b r"
+ shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
+proof -
+ have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
+ using assms by auto
+ show ?thesis unfolding *
+ proof (rule measure_finitely_additive''[symmetric])
+ show "finite r" using `finite r` by auto
+ { fix i assume "i \<in> r"
+ hence "b i \<in> sets M" using br_in_M by auto
+ thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
+ }
+ show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
+ using `disjoint_family_on b r`
+ unfolding disjoint_family_on_def by auto
+ qed
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Probability/SeriesPlus.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Probability/SeriesPlus.thy Thu Mar 11 17:39:45 2010 +0100
@@ -1,5 +1,5 @@
theory SeriesPlus
- imports Complex_Main Nat_Int_Bij
+ imports Complex_Main Nat_Bijection
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -16,7 +16,7 @@
assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
and sumg: "summable g"
- shows "(f o nat_to_nat2) sums suminf g"
+ shows "(f o prod_decode) sums suminf g"
proof (simp add: sums_def)
{
fix x
@@ -31,18 +31,18 @@
thus "0 \<le> g m" using fsums [of m]
by (auto simp add: sums_iff)
qed
- show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
+ show "(\<lambda>n. \<Sum>x = 0..<n. f (prod_decode x)) ----> suminf g"
proof (rule increasing_LIMSEQ, simp add: f_nneg)
fix n
- def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
- def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
- have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
+ def i \<equiv> "Max (Domain (prod_decode ` {0..<n}))"
+ def j \<equiv> "Max (Range (prod_decode ` {0..<n}))"
+ have ij: "prod_decode ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
by (force simp add: i_def j_def
intro: finite_imageI Max_ge finite_Domain finite_Range)
- have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})"
- using setsum_reindex [of nat_to_nat2 "{0..<n}" f]
+ have "(\<Sum>x = 0..<n. f (prod_decode x)) = setsum f (prod_decode ` {0..<n})"
+ using setsum_reindex [of prod_decode "{0..<n}" f]
by (simp add: o_def)
- (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj)
+ (metis inj_prod_decode inj_prod_decode)
also have "... \<le> setsum f ({0..i} \<times> {0..j})"
by (rule setsum_mono2) (auto simp add: ij)
also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
@@ -56,10 +56,10 @@
by (auto simp add: sums_iff)
(metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
qed
- finally have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
+ finally have "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> setsum g {0..<Suc i}" .
also have "... \<le> suminf g"
by (rule series_pos_le [OF sumg]) (simp add: g_nneg)
- finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
+ finally show "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> suminf g" .
next
fix e :: real
assume e: "0 < e"
@@ -99,26 +99,25 @@
by auto
have finite_IJ: "finite IJ"
by (simp add: IJ_def)
- def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
- have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
+ def NIJ \<equiv> "Max (prod_decode -` IJ)"
+ have IJsb: "IJ \<subseteq> prod_decode ` {0..NIJ}"
proof (auto simp add: NIJ_def)
fix i j
assume ij:"(i,j) \<in> IJ"
- hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
- by (metis nat_to_nat2_surj surj_f_inv_f)
- thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+ hence "(i,j) = prod_decode (prod_encode (i,j))"
+ by simp
+ thus "(i,j) \<in> prod_decode ` {0..Max (prod_decode -` IJ)}"
by (rule image_eqI)
- (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
- nat_to_nat2_surj surj_f_inv_f)
+ (simp add: ij finite_vimageI [OF finite_IJ inj_prod_decode])
qed
- have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
+ have "setsum f IJ \<le> setsum f (prod_decode `{0..NIJ})"
by (rule setsum_mono2) (auto simp add: IJsb)
- also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
- by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV])
- also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
+ also have "... = (\<Sum>k = 0..NIJ. f (prod_decode k))"
+ by (simp add: setsum_reindex inj_prod_decode)
+ also have "... = (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))"
by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
- finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
- thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
+ finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))" .
+ thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (prod_decode x)) + e" using glessf
by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
qed
qed
--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 11 17:39:45 2010 +0100
@@ -7,7 +7,7 @@
header{*The Message Theory, Modified for SET*}
theory Message_SET
-imports Main Nat_Int_Bij
+imports Main Nat_Bijection
begin
subsection{*General Lemmas*}
@@ -81,17 +81,16 @@
definition nat_of_agent :: "agent => nat" where
- "nat_of_agent == agent_case (curry nat2_to_nat 0)
- (curry nat2_to_nat 1)
- (curry nat2_to_nat 2)
- (curry nat2_to_nat 3)
- (nat2_to_nat (4,0))"
+ "nat_of_agent == agent_case (curry prod_encode 0)
+ (curry prod_encode 1)
+ (curry prod_encode 2)
+ (curry prod_encode 3)
+ (prod_encode (4,0))"
--{*maps each agent to a unique natural number, for specifications*}
text{*The function is indeed injective*}
lemma inj_nat_of_agent: "inj nat_of_agent"
-by (simp add: nat_of_agent_def inj_on_def curry_def
- nat2_to_nat_inj [THEN inj_eq] split: agent.split)
+by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split)
constdefs
--- a/src/HOL/SET_Protocol/Purchase.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy Thu Mar 11 17:39:45 2010 +0100
@@ -280,9 +280,9 @@
inj_PANSecret: "inj PANSecret"
CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
--{*No CardSecret equals any PANSecret*}
- apply (rule_tac x="curry nat2_to_nat 0" in exI)
- apply (rule_tac x="curry nat2_to_nat 1" in exI)
- apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
+ apply (rule_tac x="curry prod_encode 0" in exI)
+ apply (rule_tac x="curry prod_encode 1" in exI)
+ apply (simp add: prod_encode_eq inj_on_def)
done
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
--- a/src/HOL/SET_Protocol/ROOT.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/SET_Protocol/ROOT.ML Thu Mar 11 17:39:45 2010 +0100
@@ -5,5 +5,5 @@
Root file for the SET protocol proofs.
*)
-no_document use_thys ["Nat_Int_Bij"];
+no_document use_thys ["Nat_Bijection"];
use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
--- a/src/HOL/Tools/Nitpick/HISTORY Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Thu Mar 11 17:39:45 2010 +0100
@@ -7,10 +7,12 @@
* Added support for quotient types
* Added support for local definitions (for "function" and "termination"
proofs)
+ * Added support for term postprocessors
* Optimized "Multiset.multiset" and "FinFun.finfun"
* Improved efficiency of "destroy_constrs" optimization
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
+ * Fixed soundness bug related to higher-order constructors
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 17:39:45 2010 +0100
@@ -157,7 +157,8 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- NotInstalled |
+ JavaNotInstalled |
+ KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
@@ -303,7 +304,8 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- NotInstalled |
+ JavaNotInstalled |
+ KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
@@ -893,7 +895,7 @@
map (fn b => (out_assign b; out ";")) expr_assigns;
out "solve "; out_outmost_f formula; out ";\n")
in
- out ("// This file was generated by Isabelle (probably Nitpick)\n" ^
+ out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
"// " ^ Date.fmt "%Y-%m-%d %H:%M:%S"
(Date.fromTimeLocal (Time.now ())) ^ "\n");
map out_problem problems
@@ -1083,8 +1085,11 @@
||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
val js = triv_js @ nontriv_js
val first_error =
- File.fold_lines (fn line => fn "" => line | s => s) err_path ""
- handle IO.Io _ => "" | OS.SysErr _ => ""
+ (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
+ handle IO.Io _ => "" | OS.SysErr _ => "")
+ |> perhaps (try (unsuffix "\r"))
+ |> perhaps (try (unsuffix "."))
+ |> perhaps (try (unprefix "Error: "))
in
if null ps then
if code = 2 then
@@ -1092,12 +1097,15 @@
else if code = 0 then
Normal ([], js, first_error)
else if first_error |> Substring.full
+ |> Substring.position "exec: java" |> snd
+ |> Substring.isEmpty |> not then
+ JavaNotInstalled
+ else if first_error |> Substring.full
|> Substring.position "NoClassDefFoundError" |> snd
|> Substring.isEmpty |> not then
- NotInstalled
+ KodkodiNotInstalled
else if first_error <> "" then
- Error (first_error |> perhaps (try (unsuffix "."))
- |> perhaps (try (unprefix "Error: ")), js)
+ Error (first_error, js)
else if io_error then
Error ("I/O error", js)
else
--- a/src/HOL/Tools/Nitpick/minipick.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Mar 11 17:39:45 2010 +0100
@@ -336,7 +336,8 @@
val max_solutions = 1
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
- NotInstalled => "unknown"
+ JavaNotInstalled => "unknown"
+ | KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 11 17:39:45 2010 +0100
@@ -8,6 +8,7 @@
signature NITPICK =
sig
type styp = Nitpick_Util.styp
+ type term_postprocessor = Nitpick_Model.term_postprocessor
type params = {
cards_assigns: (typ option * int list) list,
maxes_assigns: (styp option * int list) list,
@@ -58,6 +59,9 @@
val unregister_frac_type : string -> theory -> theory
val register_codatatype : typ -> string -> styp list -> theory -> theory
val unregister_codatatype : typ -> theory -> theory
+ val register_term_postprocessor :
+ typ -> term_postprocessor -> theory -> theory
+ val unregister_term_postprocessor : typ -> theory -> theory
val pick_nits_in_term :
Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
-> term list -> term -> string * Proof.state
@@ -149,6 +153,9 @@
(length ts downto 1) ts))]
(* unit -> string *)
+fun install_java_message () =
+ "Nitpick requires a Java 1.5 virtual machine called \"java\"."
+(* unit -> string *)
fun install_kodkodi_message () =
"Nitpick requires the external Java program Kodkodi. To install it, download \
\the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
@@ -726,7 +733,10 @@
else
case KK.solve_any_problem overlord deadline max_threads max_solutions
(map fst problems) of
- KK.NotInstalled =>
+ KK.JavaNotInstalled =>
+ (print_m install_java_message;
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
+ | KK.KodkodiNotInstalled =>
(print_m install_kodkodi_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
@@ -911,8 +921,7 @@
in
"Nitpick " ^ did_so_and_so ^
(if is_some (!checked_problems) andalso total > 0 then
- " after checking " ^
- string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
+ " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
string_of_int total ^ " scope" ^ plural_s total
else
"") ^ "."
@@ -922,7 +931,7 @@
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran out of some resource"); "unknown")
+ (print_m (fn () => excipit "checked"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (fn () =>
@@ -966,10 +975,11 @@
(false, max_potential, max_genuine, 0)
handle Exn.Interrupt => do_interrupted ())
handle TimeLimit.TimeOut =>
- (print_m (fn () => excipit "ran out of time");
+ (print_m (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then "potential" else "unknown")
- | Exn.Interrupt => if auto orelse debug then raise Interrupt
- else error (excipit "was interrupted")
+ | Exn.Interrupt =>
+ if auto orelse debug then raise Interrupt
+ else error (excipit "was interrupted after checking")
val _ = print_v (fn () => "Total time: " ^
signed_string_of_int (Time.toMilliseconds
(Timer.checkRealTimer timer)) ^ " ms.")
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 11 17:39:45 2010 +0100
@@ -72,9 +72,11 @@
val shortest_name : string -> string
val short_name : string -> string
val shorten_names_in_term : term -> term
+ val strict_type_match : theory -> typ * typ -> bool
val type_match : theory -> typ * typ -> bool
val const_match : theory -> styp * styp -> bool
val term_match : theory -> term * term -> bool
+ val frac_from_term_pair : typ -> term -> term -> term
val is_TFree : typ -> bool
val is_higher_order_type : typ -> bool
val is_fun_type : typ -> bool
@@ -457,6 +459,15 @@
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
| term_match _ (t1, t2) = t1 aconv t2
+(* typ -> term -> term -> term *)
+fun frac_from_term_pair T t1 t2 =
+ case snd (HOLogic.dest_number t1) of
+ 0 => HOLogic.mk_number T 0
+ | n1 => case snd (HOLogic.dest_number t2) of
+ 1 => HOLogic.mk_number T n1
+ | n2 => Const (@{const_name divide}, T --> T --> T)
+ $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
+
(* typ -> bool *)
fun is_TFree (TFree _) = true
| is_TFree _ = false
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 11 17:39:45 2010 +0100
@@ -1653,6 +1653,7 @@
else
kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]
(kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
+ |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1
end) sel_us arg_us
in fold1 kk_intersect set_rs end
| BoundRel (x, _, _, _) => KK.Var x
@@ -1723,10 +1724,8 @@
map2 (kk_not oo kk_n_ary_function kk)
(map (unopt_rep o rep_of) func_guard_us) func_guard_rs
in
- if null guard_fs then
- r
- else
- kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
+ if null guard_fs then r
+ else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
end
(* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
and to_project new_R old_R r j0 =
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 11 17:39:45 2010 +0100
@@ -16,11 +16,20 @@
show_skolems: bool,
show_datatypes: bool,
show_consts: bool}
+ type term_postprocessor =
+ Proof.context -> string -> (typ -> term list) -> typ -> term -> term
structure NameTable : TABLE
+ val irrelevant : string
+ val unknown : string
+ val unrep : string
+ val register_term_postprocessor :
+ typ -> term_postprocessor -> theory -> theory
+ val unregister_term_postprocessor : typ -> theory -> theory
val tuple_list_for_name :
nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
+ val dest_plain_fun : term -> bool * (term list * term list)
val reconstruct_hol_model :
params -> scope -> (term option * int list) list -> styp list -> nut list
-> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
@@ -47,6 +56,16 @@
show_datatypes: bool,
show_consts: bool}
+type term_postprocessor =
+ Proof.context -> string -> (typ -> term list) -> typ -> term -> term
+
+structure Data = Theory_Data(
+ type T = (typ * term_postprocessor) list
+ val empty = []
+ val extend = I
+ fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
+
+val irrelevant = "_"
val unknown = "?"
val unrep = "\<dots>"
val maybe_mixfix = "_\<^sup>?"
@@ -105,6 +124,11 @@
| ord => ord)
| _ => Term_Ord.fast_term_ord tp
+(* typ -> term_postprocessor -> theory -> theory *)
+fun register_term_postprocessor T p = Data.map (cons (T, p))
+(* typ -> theory -> theory *)
+fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
+
(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
fun tuple_list_for_name rel_table bounds name =
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
@@ -165,9 +189,9 @@
(* typ -> typ -> (term * term) list -> term *)
fun aux T1 T2 [] =
Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
- | aux T1 T2 ((t1, t2) :: ps) =
+ | aux T1 T2 ((t1, t2) :: tps) =
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
- $ aux T1 T2 ps $ t1 $ t2
+ $ aux T1 T2 tps $ t1 $ t2
in aux T1 T2 o rev end
(* term -> bool *)
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
@@ -178,9 +202,12 @@
val dest_plain_fun =
let
(* term -> bool * (term list * term list) *)
- fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
+ fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], []))
+ | aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
| aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
- let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
+ let val (maybe_opt, (ts1, ts2)) = aux t0 in
+ (maybe_opt, (t1 :: ts1, t2 :: ts2))
+ end
| aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
in apsnd (pairself rev) o aux end
@@ -210,22 +237,22 @@
(* typ -> typ -> typ -> typ -> term -> term *)
fun do_curry T1 T1a T1b T2 t =
let
- val (maybe_opt, ps) = dest_plain_fun t
- val ps =
- ps |>> map (break_in_two T1 T1a T1b)
- |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
- |> AList.coalesce (op =)
- |> map (apsnd (make_plain_fun maybe_opt T1b T2))
- in make_plain_fun maybe_opt T1a (T1b --> T2) ps end
+ val (maybe_opt, tsp) = dest_plain_fun t
+ val tps =
+ tsp |>> map (break_in_two T1 T1a T1b)
+ |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
+ |> AList.coalesce (op =)
+ |> map (apsnd (make_plain_fun maybe_opt T1b T2))
+ in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
(* typ -> typ -> term -> term *)
and do_uncurry T1 T2 t =
let
val (maybe_opt, tsp) = dest_plain_fun t
- val ps =
+ val tps =
tsp |> op ~~
|> maps (fn (t1, t2) =>
multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
- in make_plain_fun maybe_opt T1 T2 ps end
+ in make_plain_fun maybe_opt T1 T2 tps end
(* typ -> typ -> typ -> typ -> term -> term *)
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
| do_arrow T1' T2' T1 T2
@@ -271,12 +298,40 @@
| mk_tuple _ (t :: _) = t
| mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
+(* theory -> typ * typ -> bool *)
+fun varified_type_match thy (candid_T, pat_T) =
+ strict_type_match thy (candid_T, Logic.varifyT pat_T)
+
+(* atom_pool -> (string * string) * (string * string) -> scope -> nut list
+ -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
+ -> term list *)
+fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
+ sel_names rel_table bounds card T =
+ let
+ val card = if card = 0 then card_of_type card_assigns T else card
+ (* nat -> term *)
+ fun nth_value_of_type n =
+ let
+ (* bool -> term *)
+ fun term unfold =
+ reconstruct_term unfold pool wacky_names scope sel_names rel_table
+ bounds T T (Atom (card, 0)) [[n]]
+ in
+ case term false of
+ t as Const (s, _) =>
+ if String.isPrefix cyclic_const_prefix s then
+ HOLogic.mk_eq (t, term true)
+ else
+ t
+ | t => t
+ end
+ in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
(* bool -> atom_pool -> (string * string) * (string * string) -> scope
-> nut list -> nut list -> nut list -> nut NameTable.table
-> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
-fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
- ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
- ofs, ...} : scope) sel_names rel_table bounds =
+and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
+ (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
+ bits, datatypes, ofs, ...}) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
(* int list list -> int *)
@@ -288,6 +343,25 @@
fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
js 0
end
+ (* typ -> term list *)
+ val all_values =
+ all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
+ (* typ -> term -> term *)
+ fun postprocess_term (Type (@{type_name fun}, _)) = I
+ | postprocess_term T =
+ if null (Data.get thy) then
+ I
+ else case AList.lookup (varified_type_match thy) (Data.get thy) T of
+ SOME postproc => postproc ctxt maybe_name all_values T
+ | NONE => I
+ (* typ list -> term -> term *)
+ fun postprocess_subterms Ts (t1 $ t2) =
+ let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in
+ postprocess_term (fastype_of1 (Ts, t)) t
+ end
+ | postprocess_subterms Ts (Abs (s, T, t')) =
+ Abs (s, T, postprocess_subterms (T :: Ts) t')
+ | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
(* bool -> typ -> typ -> (term * term) list -> term *)
fun make_set maybe_opt T1 T2 tps =
let
@@ -322,16 +396,16 @@
(T1 --> T2) --> T1 --> T2 --> T1 --> T2)
(* (term * term) list -> term *)
fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
- | aux' ((t1, t2) :: ps) =
+ | aux' ((t1, t2) :: tps) =
(case t2 of
- Const (@{const_name None}, _) => aux' ps
- | _ => update_const $ aux' ps $ t1 $ t2)
- fun aux ps =
+ Const (@{const_name None}, _) => aux' tps
+ | _ => update_const $ aux' tps $ t1 $ t2)
+ fun aux tps =
if maybe_opt andalso not (is_complete_type datatypes false T1) then
- update_const $ aux' ps $ Const (unrep, T1)
+ update_const $ aux' tps $ Const (unrep, T1)
$ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
else
- aux' ps
+ aux' tps
in aux end
(* typ list -> term -> term *)
fun polish_funs Ts t =
@@ -366,7 +440,11 @@
| Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
| Const (s, Type (@{type_name fun}, [T1, T2])) =>
if s = opt_flag orelse s = non_opt_flag then
- Abs ("x", T1, Const (unknown, T2))
+ Abs ("x", T1,
+ Const (if is_complete_type datatypes false T1 then
+ irrelevant
+ else
+ unknown, T2))
else
t
| t => t
@@ -476,23 +554,11 @@
|> dest_n_tuple (length uncur_arg_Ts)
val t =
if constr_s = @{const_name Abs_Frac} then
- let
- val num_T = body_type T
- (* int -> term *)
- val mk_num = HOLogic.mk_number num_T
- in
- case ts of
- [Const (@{const_name Pair}, _) $ t1 $ t2] =>
- (case snd (HOLogic.dest_number t1) of
- 0 => mk_num 0
- | n1 => case HOLogic.dest_number t2 |> snd of
- 1 => mk_num n1
- | n2 => Const (@{const_name divide},
- num_T --> num_T --> num_T)
- $ mk_num n1 $ mk_num n2)
- | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
- \term_for_atom (Abs_Frac)", ts)
- end
+ case ts of
+ [Const (@{const_name Pair}, _) $ t1 $ t2] =>
+ frac_from_term_pair (body_type T) t1 t2
+ | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
+ \term_for_atom (Abs_Frac)", ts)
else if not for_auto andalso
(is_abs_fun thy constr_x orelse
constr_s = @{const_name Quot}) then
@@ -575,7 +641,10 @@
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
- in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
+ in
+ postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
+ oooo term_for_rep true []
+ end
(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
-> nut -> term *)
@@ -683,14 +752,14 @@
t
| t => t
end
- (* nat -> typ -> typ list *)
- fun all_values_of_type card T =
- index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
+ (* nat -> typ -> term list *)
+ val all_values =
+ all_values_of_type pool wacky_names scope sel_names rel_table bounds
(* dtype_spec list -> dtype_spec -> bool *)
fun is_codatatype_wellformed (cos : dtype_spec list)
({typ, card, ...} : dtype_spec) =
let
- val ts = all_values_of_type card typ
+ val ts = all_values card typ
val max_depth = Integer.sum (map #card cos)
in
forall (not o bisimilar_values (map #typ cos) max_depth)
@@ -731,7 +800,7 @@
| _ => []) @
[Pretty.str "=",
Pretty.enum "," "{" "}"
- (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
+ (map (Syntax.pretty_term ctxt) (all_values card typ) @
(if fun_from_pair complete false then []
else [Pretty.str unrep]))]))
(* typ -> dtype_spec list *)
--- a/src/HOL/Tools/recdef.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/recdef.ML Thu Mar 11 17:39:45 2010 +0100
@@ -184,6 +184,7 @@
fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
let
+ val _ = legacy_feature ("\"recdef\"; prefer \"function\" instead");
val _ = requires_recdef thy;
val name = Sign.intern_const thy raw_name;
--- a/src/HOL/Tools/transfer.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/Tools/transfer.ML Thu Mar 11 17:39:45 2010 +0100
@@ -51,7 +51,7 @@
(* data lookup *)
-fun transfer_rules_of { inj, embed, return, cong, ... } =
+fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) =
(inj, embed, return, cong);
fun get_by_direction context (a, D) =
--- a/src/HOLCF/IsaMakefile Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOLCF/IsaMakefile Thu Mar 11 17:39:45 2010 +0100
@@ -47,7 +47,6 @@
HOLCF.thy \
Lift.thy \
LowerPD.thy \
- NatIso.thy \
One.thy \
Pcpodef.thy \
Pcpo.thy \
--- a/src/HOLCF/NatIso.thy Thu Mar 11 15:52:35 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,241 +0,0 @@
-(* Title: HOLCF/NatIso.thy
- Author: Brian Huffman
-*)
-
-header {* Isomorphisms of the Natural Numbers *}
-
-theory NatIso
-imports Parity
-begin
-
-subsection {* Isomorphism between naturals and sums of naturals *}
-
-primrec
- sum2nat :: "nat + nat \<Rightarrow> nat"
-where
- "sum2nat (Inl a) = a + a"
-| "sum2nat (Inr b) = Suc (b + b)"
-
-primrec
- nat2sum :: "nat \<Rightarrow> nat + nat"
-where
- "nat2sum 0 = Inl 0"
-| "nat2sum (Suc n) = (case nat2sum n of
- Inl a \<Rightarrow> Inr a | Inr b \<Rightarrow> Inl (Suc b))"
-
-lemma nat2sum_sum2nat [simp]: "nat2sum (sum2nat x) = x"
-by (induct x, rule_tac [!] nat.induct, simp_all)
-
-lemma sum2nat_nat2sum [simp]: "sum2nat (nat2sum n) = n"
-by (induct n, auto split: sum.split)
-
-lemma inj_sum2nat: "inj sum2nat"
-by (rule inj_on_inverseI, rule nat2sum_sum2nat)
-
-lemma sum2nat_eq_iff [simp]: "sum2nat x = sum2nat y \<longleftrightarrow> x = y"
-by (rule inj_sum2nat [THEN inj_eq])
-
-lemma inj_nat2sum: "inj nat2sum"
-by (rule inj_on_inverseI, rule sum2nat_nat2sum)
-
-lemma nat2sum_eq_iff [simp]: "nat2sum x = nat2sum y \<longleftrightarrow> x = y"
-by (rule inj_nat2sum [THEN inj_eq])
-
-declare sum2nat.simps [simp del]
-declare nat2sum.simps [simp del]
-
-
-subsection {* Isomorphism between naturals and pairs of naturals *}
-
-function
- prod2nat :: "nat \<times> nat \<Rightarrow> nat"
-where
- "prod2nat (0, 0) = 0"
-| "prod2nat (0, Suc n) = Suc (prod2nat (n, 0))"
-| "prod2nat (Suc m, n) = Suc (prod2nat (m, Suc n))"
-by pat_completeness auto
-
-termination by (relation
- "inv_image (measure id <*lex*> measure id) (\<lambda>(x, y). (x+y, x))") auto
-
-primrec
- nat2prod :: "nat \<Rightarrow> nat \<times> nat"
-where
- "nat2prod 0 = (0, 0)"
-| "nat2prod (Suc x) =
- (case nat2prod x of (m, n) \<Rightarrow>
- (case n of 0 \<Rightarrow> (0, Suc m) | Suc n \<Rightarrow> (Suc m, n)))"
-
-lemma nat2prod_prod2nat [simp]: "nat2prod (prod2nat x) = x"
-by (induct x, rule prod2nat.induct, simp_all)
-
-lemma prod2nat_nat2prod [simp]: "prod2nat (nat2prod n) = n"
-by (induct n, auto split: prod.split nat.split)
-
-lemma inj_prod2nat: "inj prod2nat"
-by (rule inj_on_inverseI, rule nat2prod_prod2nat)
-
-lemma prod2nat_eq_iff [simp]: "prod2nat x = prod2nat y \<longleftrightarrow> x = y"
-by (rule inj_prod2nat [THEN inj_eq])
-
-lemma inj_nat2prod: "inj nat2prod"
-by (rule inj_on_inverseI, rule prod2nat_nat2prod)
-
-lemma nat2prod_eq_iff [simp]: "nat2prod x = nat2prod y \<longleftrightarrow> x = y"
-by (rule inj_nat2prod [THEN inj_eq])
-
-subsubsection {* Ordering properties *}
-
-lemma fst_snd_le_prod2nat: "fst x \<le> prod2nat x \<and> snd x \<le> prod2nat x"
-by (induct x rule: prod2nat.induct) auto
-
-lemma fst_le_prod2nat: "fst x \<le> prod2nat x"
-by (rule fst_snd_le_prod2nat [THEN conjunct1])
-
-lemma snd_le_prod2nat: "snd x \<le> prod2nat x"
-by (rule fst_snd_le_prod2nat [THEN conjunct2])
-
-lemma le_prod2nat_1: "a \<le> prod2nat (a, b)"
-using fst_le_prod2nat [where x="(a, b)"] by simp
-
-lemma le_prod2nat_2: "b \<le> prod2nat (a, b)"
-using snd_le_prod2nat [where x="(a, b)"] by simp
-
-declare prod2nat.simps [simp del]
-declare nat2prod.simps [simp del]
-
-
-subsection {* Isomorphism between naturals and finite sets of naturals *}
-
-subsubsection {* Preliminaries *}
-
-lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
-apply (safe intro!: finite_vimageI inj_Suc)
-apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
-apply (rule subsetI, case_tac x, simp, simp)
-apply (rule finite_insert [THEN iffD2])
-apply (erule finite_imageI)
-done
-
-lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
-by auto
-
-lemma vimage_Suc_insert_Suc:
- "Suc -` insert (Suc n) A = insert n (Suc -` A)"
-by auto
-
-lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
-by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
-
-lemma div2_even_ext_nat:
- "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
-apply (rule mod_div_equality [of x 2, THEN subst])
-apply (rule mod_div_equality [of y 2, THEN subst])
-apply (case_tac "even x")
-apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
-apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
-done
-
-subsubsection {* From sets to naturals *}
-
-definition
- set2nat :: "nat set \<Rightarrow> nat" where
- "set2nat = setsum (op ^ 2)"
-
-lemma set2nat_empty [simp]: "set2nat {} = 0"
-by (simp add: set2nat_def)
-
-lemma set2nat_insert [simp]:
- "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set2nat (insert n A) = 2^n + set2nat A"
-by (simp add: set2nat_def)
-
-lemma even_set2nat_iff: "finite A \<Longrightarrow> even (set2nat A) = (0 \<notin> A)"
-by (unfold set2nat_def, erule finite_induct, auto)
-
-lemma set2nat_vimage_Suc: "set2nat (Suc -` A) = set2nat A div 2"
-apply (case_tac "finite A")
-apply (erule finite_induct, simp)
-apply (case_tac x)
-apply (simp add: even_nat_Suc_div_2 even_set2nat_iff vimage_Suc_insert_0)
-apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
-apply (simp add: set2nat_def finite_vimage_Suc_iff)
-done
-
-lemmas set2nat_div_2 = set2nat_vimage_Suc [symmetric]
-
-subsubsection {* From naturals to sets *}
-
-definition
- nat2set :: "nat \<Rightarrow> nat set" where
- "nat2set x = {n. odd (x div 2 ^ n)}"
-
-lemma nat2set_0 [simp]: "0 \<in> nat2set x \<longleftrightarrow> odd x"
-by (simp add: nat2set_def)
-
-lemma nat2set_Suc [simp]:
- "Suc n \<in> nat2set x \<longleftrightarrow> n \<in> nat2set (x div 2)"
-by (simp add: nat2set_def div_mult2_eq)
-
-lemma nat2set_zero [simp]: "nat2set 0 = {}"
-by (simp add: nat2set_def)
-
-lemma nat2set_div_2: "nat2set (x div 2) = Suc -` nat2set x"
-by auto
-
-lemma nat2set_plus_power_2:
- "n \<notin> nat2set z \<Longrightarrow> nat2set (2 ^ n + z) = insert n (nat2set z)"
- apply (induct n arbitrary: z, simp_all)
- apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
- apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
-done
-
-lemma finite_nat2set [simp]: "finite (nat2set n)"
-apply (induct n rule: nat_less_induct)
-apply (case_tac "n = 0", simp)
-apply (drule_tac x="n div 2" in spec, simp)
-apply (simp add: nat2set_div_2)
-apply (simp add: finite_vimage_Suc_iff)
-done
-
-subsubsection {* Proof of isomorphism *}
-
-lemma set2nat_nat2set [simp]: "set2nat (nat2set n) = n"
-apply (induct n rule: nat_less_induct)
-apply (case_tac "n = 0", simp)
-apply (drule_tac x="n div 2" in spec, simp)
-apply (simp add: nat2set_div_2 set2nat_vimage_Suc)
-apply (erule div2_even_ext_nat)
-apply (simp add: even_set2nat_iff)
-done
-
-lemma nat2set_set2nat [simp]: "finite A \<Longrightarrow> nat2set (set2nat A) = A"
-apply (erule finite_induct, simp_all)
-apply (simp add: nat2set_plus_power_2)
-done
-
-lemma inj_nat2set: "inj nat2set"
-by (rule inj_on_inverseI, rule set2nat_nat2set)
-
-lemma nat2set_eq_iff [simp]: "nat2set x = nat2set y \<longleftrightarrow> x = y"
-by (rule inj_eq [OF inj_nat2set])
-
-lemma inj_on_set2nat: "inj_on set2nat (Collect finite)"
-by (rule inj_on_inverseI [where g="nat2set"], simp)
-
-lemma set2nat_eq_iff [simp]:
- "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set2nat A = set2nat B \<longleftrightarrow> A = B"
-by (rule iffI, simp add: inj_onD [OF inj_on_set2nat], simp)
-
-subsubsection {* Ordering properties *}
-
-lemma nat_less_power2: "n < 2^n"
-by (induct n) simp_all
-
-lemma less_set2nat: "\<lbrakk>finite A; x \<in> A\<rbrakk> \<Longrightarrow> x < set2nat A"
-unfolding set2nat_def
-apply (rule order_less_le_trans [where y="setsum (op ^ 2) {x}"])
-apply (simp add: nat_less_power2)
-apply (erule setsum_mono2, simp, simp)
-done
-
-end
\ No newline at end of file
--- a/src/HOLCF/ROOT.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOLCF/ROOT.ML Thu Mar 11 17:39:45 2010 +0100
@@ -4,6 +4,6 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
-no_document use_thys ["Nat_Int_Bij"];
+no_document use_thys ["Nat_Bijection"];
use_thys ["HOLCF"];
--- a/src/HOLCF/Universal.thy Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOLCF/Universal.thy Thu Mar 11 17:39:45 2010 +0100
@@ -3,7 +3,7 @@
*)
theory Universal
-imports CompactBasis NatIso
+imports CompactBasis Nat_Bijection
begin
subsection {* Basis datatype *}
@@ -13,7 +13,7 @@
definition
node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"
where
- "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))"
+ "node i a S = Suc (prod_encode (i, prod_encode (a, set_encode S)))"
lemma node_not_0 [simp]: "node i a S \<noteq> 0"
unfolding node_def by simp
@@ -24,30 +24,30 @@
lemma node_inject [simp]:
"\<lbrakk>finite S; finite T\<rbrakk>
\<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T"
-unfolding node_def by simp
+unfolding node_def by (simp add: prod_encode_eq set_encode_eq)
lemma node_gt0: "i < node i a S"
unfolding node_def less_Suc_eq_le
-by (rule le_prod2nat_1)
+by (rule le_prod_encode_1)
lemma node_gt1: "a < node i a S"
unfolding node_def less_Suc_eq_le
-by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2])
+by (rule order_trans [OF le_prod_encode_1 le_prod_encode_2])
lemma nat_less_power2: "n < 2^n"
by (induct n) simp_all
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S"
-unfolding node_def less_Suc_eq_le set2nat_def
-apply (rule order_trans [OF _ le_prod2nat_2])
-apply (rule order_trans [OF _ le_prod2nat_2])
+unfolding node_def less_Suc_eq_le set_encode_def
+apply (rule order_trans [OF _ le_prod_encode_2])
+apply (rule order_trans [OF _ le_prod_encode_2])
apply (rule order_trans [where y="setsum (op ^ 2) {b}"])
apply (simp add: nat_less_power2 [THEN order_less_imp_le])
apply (erule setsum_mono2, simp, simp)
done
-lemma eq_prod2nat_pairI:
- "\<lbrakk>fst (nat2prod x) = a; snd (nat2prod x) = b\<rbrakk> \<Longrightarrow> x = prod2nat (a, b)"
+lemma eq_prod_encode_pairI:
+ "\<lbrakk>fst (prod_decode x) = a; snd (prod_decode x) = b\<rbrakk> \<Longrightarrow> x = prod_encode (a, b)"
by (erule subst, erule subst, simp)
lemma node_cases:
@@ -57,10 +57,10 @@
apply (cases x)
apply (erule 1)
apply (rule 2)
- apply (rule finite_nat2set)
+ apply (rule finite_set_decode)
apply (simp add: node_def)
- apply (rule eq_prod2nat_pairI [OF refl])
- apply (rule eq_prod2nat_pairI [OF refl refl])
+ apply (rule eq_prod_encode_pairI [OF refl])
+ apply (rule eq_prod_encode_pairI [OF refl refl])
done
lemma node_induct:
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Mar 11 17:39:45 2010 +0100
@@ -849,17 +849,20 @@
fun splitasms ctxt (asms : thm list) : splittree =
let val {neqE, ...} = get_data ctxt
- fun elim_neq (asms', []) = Tip (rev asms')
- | elim_neq (asms', asm::asms) =
- (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
+ fun elim_neq [] (asms', []) = Tip (rev asms')
+ | elim_neq [] (asms', asms) = Tip (rev asms' @ asms)
+ | elim_neq (neq :: neqs) (asms', []) = elim_neq neqs ([],rev asms')
+ | elim_neq (neqs as (neq :: _)) (asms', asm::asms) =
+ (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
SOME spl =>
let val (ct1, ct2) = extract (cprop_of spl)
val thm1 = assume ct1
val thm2 = assume ct2
- in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
+ in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
+ ct2, elim_neq neqs (asms', asms@[thm2]))
end
- | NONE => elim_neq (asm::asms', asms))
-in elim_neq ([], asms) end;
+ | NONE => elim_neq neqs (asm::asms', asms))
+in elim_neq neqE ([], asms) end;
fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js)
| fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js =
--- a/src/Pure/General/sha1_polyml.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/Pure/General/sha1_polyml.ML Thu Mar 11 17:39:45 2010 +0100
@@ -15,15 +15,21 @@
let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
+val lib_path =
+ ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_system then "sha1.dll" else "libsha1.so"))
+ |> Path.explode;
+
fun digest_external str =
let
val digest = CInterface.alloc 20 CInterface.Cchar;
- val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer")
- (CInterface.STRING, CInterface.INT, CInterface.POINTER)
- CInterface.POINTER (str, size str, CInterface.address digest);
+ val _ =
+ CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
+ (CInterface.STRING, CInterface.INT, CInterface.POINTER)
+ CInterface.POINTER (str, size str, CInterface.address digest);
in fold (suffix o hex_string digest) (0 upto 19) "" end;
fun digest str = digest_external str
- handle CInterface.Foreign _ => SHA1.digest str;
+ handle CInterface.Foreign msg =>
+ (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
end;
--- a/src/Pure/Isar/constdefs.ML Thu Mar 11 15:52:35 2010 +0100
+++ b/src/Pure/Isar/constdefs.ML Thu Mar 11 17:39:45 2010 +0100
@@ -22,6 +22,8 @@
fun gen_constdef prep_vars prep_prop prep_att
structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
let
+ val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead");
+
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
val thy_ctxt = ProofContext.init thy;