--- a/doc-src/Nitpick/nitpick.tex Tue Feb 09 16:07:09 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 09 21:32:57 2010 +0100
@@ -154,7 +154,7 @@
the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
+\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
@@ -311,9 +311,9 @@
\slshape Constant: \nopagebreak \\
\hbox{}\qquad $\mathit{The} = \undef{}
(\!\begin{aligned}[t]%
- & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
- & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
- & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
+ & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
+ & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
+ & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
\postw
Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
@@ -550,7 +550,7 @@
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = []$ \\
-\hbox{}\qquad\qquad $\textit{y} = a_3$
+\hbox{}\qquad\qquad $\textit{y} = a_1$
\postw
To see why the counterexample is genuine, we enable \textit{show\_consts}
@@ -558,21 +558,21 @@
\prew
{\slshape Datatype:} \\
-\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
+\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
{\slshape Constants:} \\
-\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
-\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
+\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
+\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
\postw
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
including $a_2$.
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
-append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
-a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
+append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
+a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
representable in the subset of $'a$~\textit{list} considered by Nitpick, which
is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
-appending $[a_3, a_3]$ to itself gives $\unk$.
+appending $[a_1, a_1]$ to itself gives $\unk$.
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
considers the following subsets:
@@ -600,8 +600,8 @@
All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
are listed and only those. As an example of a non-subterm-closed subset,
-consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
-that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
+consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
+that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
\mathcal{S}$ as a subterm.
Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
@@ -613,11 +613,11 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
-\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
+\hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
-\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
+\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
\postw
Because datatypes are approximated using a three-valued logic, there is usually
@@ -642,11 +642,11 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
+\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
\hbox{}\qquad\qquad $x = \Abs{2}$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
+\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
\postw
%% MARK
@@ -664,12 +664,13 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
-\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
+\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
+\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
-\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
+\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
+& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
+& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
\postw
Finally, Nitpick provides rudimentary support for rationals and reals using a
@@ -956,16 +957,16 @@
depth}~= 1:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
-\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
-\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
-\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
+\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
+\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
+\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
Total time: 726 ms.
\postw
-The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
-$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
-$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
+The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
+$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
+$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
the segment leading to the binder is the stem.
@@ -1000,15 +1001,15 @@
\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]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $a = a_2$ \\
+\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
-\textit{LCons}~a_2~\omega$ \\
-\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
+\textit{LCons}~a_1~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad Codatatype:\strut \nopagebreak \\
\hbox{}\qquad\qquad $'a~\textit{llist} =
\{\!\begin{aligned}[t]
- & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
- & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
+ & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
+ & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
\\[2\smallskipamount]
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
that the counterexample is genuine. \\[2\smallskipamount]
@@ -1198,8 +1199,8 @@
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
-\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
+\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
Total time: 1636 ms.
\postw
@@ -1377,21 +1378,21 @@
\prew
\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $a = a_4$ \\
-\hbox{}\qquad\qquad $b = a_3$ \\
-\hbox{}\qquad\qquad $t = \xi_3$ \\
-\hbox{}\qquad\qquad $u = \xi_4$ \\
+\hbox{}\qquad\qquad $a = a_1$ \\
+\hbox{}\qquad\qquad $b = a_2$ \\
+\hbox{}\qquad\qquad $t = \xi_1$ \\
+\hbox{}\qquad\qquad $u = \xi_2$ \\
\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
\hbox{}\qquad\qquad $\textit{labels} = \undef
(\!\begin{aligned}[t]%
- & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
- & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
- & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
+ & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
+ & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
+ & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
(\!\begin{aligned}[t]%
- & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
- & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
- & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
+ & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
+ & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
+ & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
\postw
@@ -1406,7 +1407,7 @@
allowing unreachable states in the preceding example (by removing the ``$n \in
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
set of objects over which the induction is performed while doing the step
-so as to test the induction hypothesis's strength.}
+in order to test the induction hypothesis's strength.}
The new trees are so nonstandard that we know nothing about them, except what
the induction hypothesis states and what can be proved about all trees without
relying on induction or case distinction. The key observation is,
@@ -1417,8 +1418,8 @@
objects, and Nitpick won't find any nonstandard counterexample.}
\end{quote}
%
-But here, Nitpick did find some nonstandard trees $t = \xi_3$
-and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
+But here, Nitpick did find some nonstandard trees $t = \xi_1$
+and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
Because neither tree contains both $a$ and $b$, the induction hypothesis tells
us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
@@ -1441,7 +1442,7 @@
\postw
This time, Nitpick won't find any nonstandard counterexample, and we can perform
-the induction step using \textbf{auto}.
+the induction step using \textit{auto}.
\section{Case Studies}
\label{case-studies}
@@ -1694,7 +1695,7 @@
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
+{\slshape Nitpick found no counterexample.}
\postw
Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
@@ -1726,8 +1727,8 @@
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
-\hbox{}\qquad\qquad $x = a_4$
+\hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
+\hbox{}\qquad\qquad $x = a_2$
\postw
It's hard to see why this is a counterexample. To improve readability, we will
@@ -1756,7 +1757,7 @@
\prew
\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
\postw
Insertion should transform the set of elements represented by the tree in the
@@ -1766,14 +1767,14 @@
\textbf{theorem} \textit{dataset\_insort}:\kern.4em
``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
\postw
-We could continue like this and sketch a complete theory of AA trees without
-performing a single proof. Once the definitions and main theorems are in place
-and have been thoroughly tested using Nitpick, we could start working on the
-proofs. Developing theories this way usually saves time, because faulty theorems
-and definitions are discovered much earlier in the process.
+We could continue like this and sketch a complete theory of AA trees. Once the
+definitions and main theorems are in place and have been thoroughly tested using
+Nitpick, we could start working on the proofs. Developing theories this way
+usually saves time, because faulty theorems and definitions are discovered much
+earlier in the process.
\section{Option Reference}
\label{option-reference}
@@ -2138,7 +2139,7 @@
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{MiniSatJNI}. Also be aware that many of the counterexamples may look
+\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.
@@ -2150,7 +2151,7 @@
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{MiniSatJNI}. Also be aware that many of the
+\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.
@@ -2243,7 +2244,7 @@
to be faster than their Java counterparts, but they can be more difficult to
install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
\textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
-you will need an incremental SAT solver, such as \textit{MiniSatJNI}
+you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
(recommended) or \textit{SAT4J}.
The supported solvers are listed below:
@@ -2257,7 +2258,7 @@
\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{MiniSatJNI}}: The JNI (Java Native Interface)
+\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, the JNI version can be used incrementally.
@@ -2279,7 +2280,7 @@
\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{zChaffJNI}}: The JNI version of zChaff is
+\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}.
@@ -2295,7 +2296,7 @@
executable. The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
-\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
+\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}
@@ -2313,7 +2314,7 @@
install the official SAT4J packages, because their API is incompatible with
Kodkod.
-\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
+\item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
optimized for small problems. It can also be used incrementally.
\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
@@ -2324,7 +2325,7 @@
\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
\textit{smart}, Nitpick selects the first solver among MiniSat,
-PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
+PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
should always be available. If \textit{verbose} (\S\ref{output-format}) is
enabled, Nitpick displays which SAT solver was chosen.
--- a/doc-src/manual.bib Tue Feb 09 16:07:09 2010 +0100
+++ b/doc-src/manual.bib Tue Feb 09 21:32:57 2010 +0100
@@ -3,7 +3,7 @@
%publishers
@string{AP="Academic Press"}
@string{CUP="Cambridge University Press"}
-@string{IEEE="{\sc ieee} Computer Society Press"}
+@string{IEEE="IEEE Computer Society Press"}
@string{LNCS="Lecture Notes in Computer Science"}
@string{MIT="MIT Press"}
@string{NH="North-Holland"}
--- a/src/HOL/IsaMakefile Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 09 21:32:57 2010 +0100
@@ -207,6 +207,7 @@
Tools/Nitpick/nitpick_mono.ML \
Tools/Nitpick/nitpick_nut.ML \
Tools/Nitpick/nitpick_peephole.ML \
+ Tools/Nitpick/nitpick_preproc.ML \
Tools/Nitpick/nitpick_rep.ML \
Tools/Nitpick/nitpick_scope.ML \
Tools/Nitpick/nitpick_tests.ML \
@@ -624,12 +625,13 @@
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
- Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \
- Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \
- Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
- Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
- Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
- Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
+ Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
+ Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
+ Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
+ Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
+ Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
+ Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
+ Nitpick_Examples/Typedef_Nits.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
--- a/src/HOL/Nitpick.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick.thy Tue Feb 09 21:32:57 2010 +0100
@@ -13,6 +13,7 @@
("Tools/Nitpick/kodkod_sat.ML")
("Tools/Nitpick/nitpick_util.ML")
("Tools/Nitpick/nitpick_hol.ML")
+ ("Tools/Nitpick/nitpick_preproc.ML")
("Tools/Nitpick/nitpick_mono.ML")
("Tools/Nitpick/nitpick_scope.ML")
("Tools/Nitpick/nitpick_peephole.ML")
@@ -237,6 +238,7 @@
use "Tools/Nitpick/kodkod_sat.ML"
use "Tools/Nitpick/nitpick_util.ML"
use "Tools/Nitpick/nitpick_hol.ML"
+use "Tools/Nitpick/nitpick_preproc.ML"
use "Tools/Nitpick/nitpick_mono.ML"
use "Tools/Nitpick/nitpick_scope.ML"
use "Tools/Nitpick/nitpick_peephole.ML"
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Core_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick's functional core.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Datatype_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick applied to datatypes.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -0,0 +1,57 @@
+(* Title: HOL/Nitpick_Examples/Hotel_Nits.thy
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010
+
+Nitpick example based on Tobias Nipkow's hotel key card formalization.
+*)
+
+header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
+ Formalization *}
+
+theory Hotel_Nits
+imports Main
+begin
+
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
+
+typedecl guest
+typedecl key
+typedecl room
+
+types keycard = "key \<times> key"
+
+record state =
+ owns :: "room \<Rightarrow> guest option"
+ currk :: "room \<Rightarrow> key"
+ issued :: "key set"
+ cards :: "guest \<Rightarrow> keycard set"
+ roomk :: "room \<Rightarrow> key"
+ isin :: "room \<Rightarrow> guest set"
+ safe :: "room \<Rightarrow> bool"
+
+inductive_set reach :: "state set" where
+init:
+"inj initk \<Longrightarrow>
+ \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
+ roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
+check_in:
+"\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow>
+ s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
+ cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
+ owns := (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
+enter_room:
+"\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
+ s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
+ roomk := (roomk s)(r := k'),
+ safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
+ \<or> safe s r)\<rparr> \<in> reach" |
+exit_room:
+"\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
+
+theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
+nitpick [card room = 1, card guest = 2, card "guest option" = 3,
+ card key = 4, card state = 6, expect = genuine]
+nitpick [card room = 1, card guest = 2, expect = genuine]
+oops
+
+end
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Induct_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick applied to (co)inductive definitions.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Integer_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick applied to natural numbers and integers.
*)
@@ -11,7 +11,7 @@
imports Nitpick
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
lemma "Suc x = x + 1"
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples from the Nitpick manual.
*)
@@ -13,7 +13,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
subsection {* 3.1. Propositional Logic *}
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Mini_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Minipick, the minimalistic version of Nitpick.
*)
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Mono_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick's monotonicity check.
*)
@@ -16,7 +16,7 @@
val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
val def_table = Nitpick_HOL.const_def_table @{context} defs
-val ext_ctxt : Nitpick_HOL.extended_context =
+val hol_ctxt : Nitpick_HOL.hol_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
binary_ints = SOME false, destroy_constrs = false, specialize = false,
@@ -29,7 +29,7 @@
special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
(* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
+val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
Nitpick_Mono.Plus [] []
fun is_const t =
let val T = fastype_of t in
--- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,13 +1,13 @@
(* Title: HOL/Nitpick_Examples/Nitpick_Examples.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Nitpick examples.
*)
theory Nitpick_Examples
-imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits
- Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
- Typedef_Nits
+imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
+ Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
+ Tests_Nits Typedef_Nits
begin
end
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Pattern_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick's "destroy_constrs" optimization.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 14]
lemma "x = (case u of () \<Rightarrow> y)"
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Record_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick applied to records.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Refute_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Refute examples adapted to Nitpick.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Special_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick's "specialize" optimization.
*)
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 4]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Tests_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Nitpick tests.
*)
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 09 21:32:57 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Typedef_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Examples featuring Nitpick applied to typedefs.
*)
@@ -11,7 +11,8 @@
imports Main Rational
begin
-nitpick_params [card = 1\<midarrow>4, timeout = 30 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
+ card = 1\<midarrow>4]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Feb 09 21:32:57 2010 +0100
@@ -4,6 +4,8 @@
* Added "std" option and implemented support for nonstandard models
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
+ * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
+ "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
Version 2009-1
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 09 21:32:57 2010 +0100
@@ -1054,23 +1054,23 @@
let
val code =
bash ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^
- "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
- \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
- \$JAVA_LIBRARY_PATH\" \
- \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
- \$LD_LIBRARY_PATH\" \
- \\"$KODKODI\"/bin/kodkodi" ^
- (if ms >= 0 then " -max-msecs " ^ string_of_int ms
- else "") ^
- (if max_solutions > 1 then " -solve-all" else "") ^
- " -max-solutions " ^ string_of_int max_solutions ^
- (if max_threads > 0 then
- " -max-threads " ^ string_of_int max_threads
- else
- "") ^
- " < " ^ File.shell_path in_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path)
+ "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
+ \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
+ \$JAVA_LIBRARY_PATH\" \
+ \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
+ \$LD_LIBRARY_PATH\" \
+ \\"$KODKODI\"/bin/kodkodi" ^
+ (if ms >= 0 then " -max-msecs " ^ string_of_int ms
+ else "") ^
+ (if max_solutions > 1 then " -solve-all" else "") ^
+ " -max-solutions " ^ string_of_int max_solutions ^
+ (if max_threads > 0 then
+ " -max-threads " ^ string_of_int max_threads
+ else
+ "") ^
+ " < " ^ File.shell_path in_path ^
+ " > " ^ File.shell_path out_path ^
+ " 2> " ^ File.shell_path err_path)
val (ps, nontriv_js) = read_output_file out_path
|>> map (apfst reindex) ||> map reindex
val js = triv_js @ nontriv_js
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 09 21:32:57 2010 +0100
@@ -42,12 +42,12 @@
if berkmin_exec = "" then "BerkMin561"
else berkmin_exec, [], "Satisfiable !!",
"solution =", "UNSATISFIABLE !!")),
- ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
+ ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
- ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
+ ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+ ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
- ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
+ ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"])),
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 09 21:32:57 2010 +0100
@@ -69,6 +69,7 @@
open Nitpick_Util
open Nitpick_HOL
+open Nitpick_Preproc
open Nitpick_Mono
open Nitpick_Scope
open Nitpick_Peephole
@@ -273,7 +274,7 @@
val intro_table = inductive_intro_table ctxt def_table
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table thy
- val (ext_ctxt as {wf_cache, ...}) =
+ val (hol_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
@@ -292,7 +293,7 @@
val _ = null (Term.add_tvars assms_t []) orelse
raise NOT_SUPPORTED "schematic type variables"
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = preprocess_term ext_ctxt assms_t
+ core_t) = preprocess_term hol_ctxt assms_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -319,9 +320,9 @@
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
- val core_u = nut_from_term ext_ctxt Eq core_t
- val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
- val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
+ val core_u = nut_from_term hol_ctxt Eq core_t
+ val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
+ val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
val (free_names, const_names) =
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
val (sel_names, nonsel_names) =
@@ -338,18 +339,18 @@
fun is_type_always_monotonic T =
(is_datatype thy T andalso not (is_quot_type thy T) andalso
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
- is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
+ is_number_type thy T orelse is_bit_type T
fun is_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
| _ => is_type_always_monotonic T orelse
- formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
+ formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
fun is_deep_datatype T =
is_datatype thy T andalso
(is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names)
- val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
+ val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
exists (member (op =) [nat_T, int_T]) all_Ts then
@@ -522,7 +523,7 @@
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
- val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
+ val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = univ_card nat_card int_card main_j0
@@ -553,7 +554,7 @@
if loc = "Nitpick_Kodkod.check_arity" andalso
not (Typtab.is_empty ofs) then
problem_for_scope liberal
- {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
+ {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth,
datatypes = datatypes, ofs = Typtab.empty}
else if loc = "Nitpick.pick_them_nits_in_term.\
@@ -891,7 +892,7 @@
end
val (skipped, the_scopes) =
- all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
+ all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
val _ = if skipped > 0 then
print_m (fn () => "Too many scopes. Skipping " ^
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 09 21:32:57 2010 +0100
@@ -13,7 +13,7 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
- type extended_context = {
+ type hol_context = {
thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
@@ -46,12 +46,24 @@
wf_cache: wf_cache Unsynchronized.ref,
constr_cache: (typ * styp list) list Unsynchronized.ref}
+ datatype fixpoint_kind = Lfp | Gfp | NoFp
+ datatype boxability =
+ InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
+
val name_sep : string
val numeral_prefix : string
+ val ubfp_prefix : string
+ val lbfp_prefix : string
val skolem_prefix : string
+ val special_prefix : string
+ val uncurry_prefix : string
val eval_prefix : string
val original_name : string -> string
val s_conj : term * term -> term
+ val s_disj : term * term -> term
+ val strip_any_connective : term -> term list * term
+ val conjuncts_of : term -> term list
+ val disjuncts_of : term -> term list
val unbit_and_unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
@@ -76,6 +88,7 @@
val is_record_type : typ -> bool
val is_number_type : theory -> typ -> bool
val const_for_iterator_type : typ -> styp
+ val strip_n_binders : int -> typ -> typ list * typ
val nth_range_type : int -> typ -> typ
val num_factors_in_type : typ -> int
val num_binder_types : typ -> int
@@ -96,16 +109,20 @@
val is_rep_fun : theory -> styp -> bool
val is_quot_abs_fun : Proof.context -> styp -> bool
val is_quot_rep_fun : Proof.context -> styp -> bool
+ val mate_of_rep_fun : theory -> styp -> styp
+ val is_constr_like : theory -> styp -> bool
+ val is_stale_constr : theory -> styp -> bool
val is_constr : theory -> styp -> bool
- val is_stale_constr : theory -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
+ val box_type : hol_context -> boxability -> typ -> typ
val discr_for_constr : styp -> styp
val num_sels_for_constr_type : typ -> int
val nth_sel_name_for_constr_name : string -> int -> string
val nth_sel_for_constr : styp -> int -> styp
- val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
+ val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
val sel_no_from_name : string -> int
+ val close_form : term -> term
val eta_expand : typ list -> term -> int -> term
val extensionalize : term -> term
val distinctness_formula : typ -> term list -> term
@@ -113,19 +130,25 @@
val unregister_frac_type : string -> theory -> theory
val register_codatatype : typ -> string -> styp list -> theory -> theory
val unregister_codatatype : typ -> theory -> theory
- val datatype_constrs : extended_context -> typ -> styp list
- val boxed_datatype_constrs : extended_context -> typ -> styp list
- val num_datatype_constrs : extended_context -> typ -> int
+ val datatype_constrs : hol_context -> typ -> styp list
+ val boxed_datatype_constrs : hol_context -> typ -> styp list
+ val num_datatype_constrs : hol_context -> typ -> int
val constr_name_for_sel_like : string -> string
- val boxed_constr_for_sel : extended_context -> styp -> styp
+ val boxed_constr_for_sel : hol_context -> styp -> styp
+ val discriminate_value : hol_context -> styp -> term -> term
+ val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
+ val construct_value : theory -> styp -> term list -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_exact_card_of_type :
- extended_context -> int -> int -> (typ * int) list -> typ -> int
- val is_finite_type : extended_context -> typ -> bool
+ hol_context -> int -> int -> (typ * int) list -> typ -> int
+ val is_finite_type : hol_context -> typ -> bool
+ val special_bounds : term list -> (indexname * typ) list
+ val is_funky_typedef : theory -> typ -> bool
val all_axioms_of : theory -> term list * term list * term list
val arity_of_built_in_const : bool -> styp -> int option
val is_built_in_const : bool -> styp -> bool
+ val term_under_def : term -> term
val case_const_names : theory -> (string * int) list
val const_def_table : Proof.context -> term list -> const_table
val const_nondef_table : term list -> const_table
@@ -134,22 +157,33 @@
val inductive_intro_table : Proof.context -> const_table -> const_table
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : theory -> (string * string) list
+ val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
+ val inverse_axioms_for_rep_fun : theory -> styp -> term list
+ val optimized_typedef_axioms : theory -> string * typ list -> term list
+ val optimized_quot_type_axioms : theory -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
- val is_inductive_pred : extended_context -> styp -> bool
+ val fixpoint_kind_of_const :
+ theory -> const_table -> string * typ -> fixpoint_kind
+ val is_inductive_pred : hol_context -> styp -> bool
+ val is_equational_fun : hol_context -> styp -> bool
val is_constr_pattern_lhs : theory -> term -> bool
val is_constr_pattern_formula : theory -> term -> bool
+ val unfold_defs_in_term : hol_context -> term -> term
+ val codatatype_bisim_axioms : hol_context -> typ -> term list
+ val is_well_founded_inductive_pred : hol_context -> styp -> bool
+ val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
+ val equational_fun_axioms : hol_context -> styp -> term list
+ val is_equational_fun_surely_complete : hol_context -> styp -> bool
val merge_type_vars_in_terms : term list -> term list
- val ground_types_in_type : extended_context -> typ -> typ list
- val ground_types_in_terms : extended_context -> term list -> typ list
+ val ground_types_in_type : hol_context -> typ -> typ list
+ val ground_types_in_terms : hol_context -> term list -> typ list
val format_type : int list -> int list -> typ -> typ
val format_term_type :
theory -> const_table -> (term option * int list) list -> term -> typ
val user_friendly_const :
- extended_context -> string * string -> (term option * int list) list
+ hol_context -> string * string -> (term option * int list) list
-> styp -> term * typ
val assign_operator_for_const : styp -> string
- val preprocess_term :
- extended_context -> term -> ((term list * term list) * (bool * bool)) * term
end;
structure Nitpick_HOL : NITPICK_HOL =
@@ -162,7 +196,7 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
-type extended_context = {
+type hol_context = {
thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
@@ -195,6 +229,10 @@
wf_cache: wf_cache Unsynchronized.ref,
constr_cache: (typ * styp list) list Unsynchronized.ref}
+datatype fixpoint_kind = Lfp | Gfp | NoFp
+datatype boxability =
+ InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
+
structure Data = Theory_Data(
type T = {frac_types: (string * (string * string) list) list,
codatatypes: (string * (string * styp list)) list}
@@ -222,20 +260,11 @@
val special_prefix = nitpick_prefix ^ "sp"
val uncurry_prefix = nitpick_prefix ^ "unc"
val eval_prefix = nitpick_prefix ^ "eval"
-val bound_var_prefix = "b"
-val cong_var_prefix = "c"
val iter_var_prefix = "i"
-val val_var_prefix = nitpick_prefix ^ "v"
val arg_var_prefix = "x"
(* int -> string *)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
-fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
-(* int -> int -> string *)
-fun skolem_prefix_for k j =
- skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
-fun uncurry_prefix_for k j =
- uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
(* string -> string * string *)
val strip_first_name_sep =
@@ -260,9 +289,6 @@
| s_disj (t1, t2) =
if t1 = @{const True} orelse t2 = @{const True} then @{const True}
else HOLogic.mk_disj (t1, t2)
-(* term -> term -> term *)
-fun mk_exists v t =
- HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
(* term -> term -> term list *)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -276,8 +302,8 @@
([t], @{const Not})
| strip_any_connective t = ([t], @{const Not})
(* term -> term list *)
-val conjuncts = strip_connective @{const "op &"}
-val disjuncts = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const "op &"}
+val disjuncts_of = strip_connective @{const "op |"}
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -373,8 +399,6 @@
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
(* string -> term -> term *)
val prefix_abs_vars = Term.map_abs_vars o prefix_name
-(* term -> term *)
-val shorten_abs_vars = Term.map_abs_vars shortest_name
(* string -> string *)
fun short_name s =
case space_explode name_sep s of
@@ -441,7 +465,7 @@
| const_for_iterator_type T =
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
-(* int -> typ -> typ * typ *)
+(* int -> typ -> typ list * typ *)
fun strip_n_binders 0 T = ([], T)
| strip_n_binders n (Type ("fun", [T1, T2])) =
strip_n_binders (n - 1) T2 |>> cons T1
@@ -552,7 +576,7 @@
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
- | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
+ | is_quot_type _ (Type ("FSet.fset", _)) = true
| is_quot_type _ _ = false
fun is_codatatype thy (T as Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
@@ -619,11 +643,11 @@
| NONE => false)
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
- | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
+fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
+ | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
- | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
+fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
+ | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
@@ -682,9 +706,6 @@
String.isPrefix sel_prefix
orf (member (op =) [@{const_name fst}, @{const_name snd}])
-datatype boxability =
- InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
-
(* boxability -> boxability *)
fun in_fun_lhs_for InConstr = InSel
| in_fun_lhs_for _ = InFunLHS
@@ -693,8 +714,8 @@
| in_fun_rhs_for InFunRHS1 = InFunRHS2
| in_fun_rhs_for _ = InFunRHS1
-(* extended_context -> boxability -> typ -> bool *)
-fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
+(* hol_context -> boxability -> typ -> bool *)
+fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
case T of
Type ("fun", _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
@@ -702,31 +723,31 @@
| Type ("*", Ts) =>
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
((boxy = InExpr orelse boxy = InFunLHS) andalso
- exists (is_boxing_worth_it ext_ctxt InPair)
- (map (box_type ext_ctxt InPair) Ts))
+ exists (is_boxing_worth_it hol_ctxt InPair)
+ (map (box_type hol_ctxt InPair) Ts))
| _ => false
-(* extended_context -> boxability -> string * typ list -> string *)
-and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
+(* hol_context -> boxability -> string * typ list -> string *)
+and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
case triple_lookup (type_match thy) boxes (Type z) of
SOME (SOME box_me) => box_me
- | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
-(* extended_context -> boxability -> typ -> typ *)
-and box_type ext_ctxt boxy T =
+ | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
+(* hol_context -> boxability -> typ -> typ *)
+and box_type hol_ctxt boxy T =
case T of
Type (z as ("fun", [T1, T2])) =>
if boxy <> InConstr andalso boxy <> InSel andalso
- should_box_type ext_ctxt boxy z then
+ should_box_type hol_ctxt boxy z then
Type (@{type_name fun_box},
- [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
+ [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
else
- box_type ext_ctxt (in_fun_lhs_for boxy) T1
- --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
+ box_type hol_ctxt (in_fun_lhs_for boxy) T1
+ --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
| Type (z as ("*", Ts)) =>
if boxy <> InConstr andalso boxy <> InSel
- andalso should_box_type ext_ctxt boxy z then
- Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
+ andalso should_box_type hol_ctxt boxy z then
+ Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
else
- Type ("*", map (box_type ext_ctxt
+ Type ("*", map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
| _ => T
@@ -747,9 +768,9 @@
| nth_sel_for_constr (s, T) n =
(nth_sel_name_for_constr_name s n,
body_type T --> nth (maybe_curried_binder_types T) n)
-(* extended_context -> styp -> int -> styp *)
-fun boxed_nth_sel_for_constr ext_ctxt =
- apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
+(* hol_context -> styp -> int -> styp *)
+fun boxed_nth_sel_for_constr hol_ctxt =
+ apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
(* string -> int *)
fun sel_no_from_name s =
@@ -762,6 +783,22 @@
else
0
+(* term -> term *)
+val close_form =
+ let
+ (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
+ fun close_up zs zs' =
+ fold (fn (z as ((s, _), T)) => fn t' =>
+ Term.all T $ Abs (s, T, abstract_over (Var z, t')))
+ (take (length zs' - length zs) zs')
+ (* (indexname * typ) list -> term -> term *)
+ fun aux zs (@{const "==>"} $ t1 $ t2) =
+ let val zs' = Term.add_vars t1 zs in
+ close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
+ end
+ | aux zs t = close_up zs (Term.add_vars t zs) t
+ in aux [] end
+
(* typ list -> term -> int -> term *)
fun eta_expand _ t 0 = t
| eta_expand Ts (Abs (s, T, t')) n =
@@ -791,8 +828,8 @@
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* extended_context -> typ -> styp list *)
-fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
+(* hol_context -> typ -> styp list *)
+fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
@@ -829,49 +866,49 @@
else
[])
| uncached_datatype_constrs _ _ = []
-(* extended_context -> typ -> styp list *)
-fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
+(* hol_context -> typ -> styp list *)
+fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
| NONE =>
- let val xs = uncached_datatype_constrs ext_ctxt T in
+ let val xs = uncached_datatype_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
-fun boxed_datatype_constrs ext_ctxt =
- map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
-(* extended_context -> typ -> int *)
+fun boxed_datatype_constrs hol_ctxt =
+ map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
+(* hol_context -> typ -> int *)
val num_datatype_constrs = length oo datatype_constrs
(* string -> string *)
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
| constr_name_for_sel_like s' = original_name s'
-(* extended_context -> styp -> styp *)
-fun boxed_constr_for_sel ext_ctxt (s', T') =
+(* hol_context -> styp -> styp *)
+fun boxed_constr_for_sel hol_ctxt (s', T') =
let val s = constr_name_for_sel_like s' in
- AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
+ AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
|> the |> pair s
end
-(* extended_context -> styp -> term *)
-fun discr_term_for_constr ext_ctxt (x as (s, T)) =
+(* hol_context -> styp -> term *)
+fun discr_term_for_constr hol_ctxt (x as (s, T)) =
let val dataT = body_type T in
if s = @{const_name Suc} then
Abs (Name.uu, dataT,
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
- else if num_datatype_constrs ext_ctxt dataT >= 2 then
+ else if num_datatype_constrs hol_ctxt dataT >= 2 then
Const (discr_for_constr x)
else
Abs (Name.uu, dataT, @{const True})
end
-(* extended_context -> styp -> term -> term *)
-fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
+(* hol_context -> styp -> term -> term *)
+fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
case strip_comb t of
(Const x', args) =>
if x = x' then @{const True}
else if is_constr_like thy x' then @{const False}
- else betapply (discr_term_for_constr ext_ctxt x, t)
- | _ => betapply (discr_term_for_constr ext_ctxt x, t)
+ else betapply (discr_term_for_constr hol_ctxt x, t)
+ | _ => betapply (discr_term_for_constr hol_ctxt x, t)
(* styp -> term -> term *)
fun nth_arg_sel_term_for_constr (x as (s, T)) n =
@@ -920,25 +957,9 @@
| _ => list_comb (Const x, args)
end
-(* extended_context -> typ -> term -> term *)
-fun constr_expand (ext_ctxt as {thy, ...}) T t =
- (case head_of t of
- Const x => if is_constr_like thy x then t else raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- let
- val x' as (_, T') =
- if is_pair_type T then
- let val (T1, T2) = HOLogic.dest_prodT T in
- (@{const_name Pair}, T1 --> T2 --> T)
- end
- else
- datatype_constrs ext_ctxt T |> hd
- val arg_Ts = binder_types T'
- in
- list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
- (index_seq 0 (length arg_Ts)) arg_Ts)
- end
+(* The higher this number is, the more nonstandard models can be generated. It's
+ not important enough to be a user option, though. *)
+val xi_card = 8
(* (typ * int) list -> typ -> int *)
fun card_of_type assigns (Type ("fun", [T1, T2])) =
@@ -949,6 +970,7 @@
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
| card_of_type _ @{typ unit} = 1
+ | card_of_type _ @{typ \<xi>} = xi_card
| card_of_type assigns T =
case AList.lookup (op =) assigns T of
SOME k => k
@@ -975,8 +997,8 @@
card_of_type assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
-(* extended_context -> int -> (typ * int) list -> typ -> int *)
-fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
+(* hol_context -> int -> (typ * int) list -> typ -> int *)
+fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
let
(* typ list -> typ -> int *)
fun aux avoid T =
@@ -1005,14 +1027,15 @@
| @{typ prop} => 2
| @{typ bool} => 2
| @{typ unit} => 1
+ | @{typ \<xi>} => xi_card
| Type _ =>
- (case datatype_constrs ext_ctxt T of
+ (case datatype_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
else raise SAME ()
| constrs =>
let
val constr_cards =
- datatype_constrs ext_ctxt T
+ datatype_constrs hol_ctxt T
|> map (Integer.prod o map (aux (T :: avoid)) o binder_types
o snd)
in
@@ -1024,9 +1047,9 @@
AList.lookup (op =) assigns T |> the_default default_card
in Int.min (max, aux [] T) end
-(* extended_context -> typ -> bool *)
-fun is_finite_type ext_ctxt =
- not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
+(* hol_context -> typ -> bool *)
+fun is_finite_type hol_ctxt =
+ not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -1052,7 +1075,7 @@
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
@{type_name int}] s orelse
is_frac_type thy (Type (s, []))
-(* theory -> term -> bool *)
+(* theory -> typ -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
(* term -> bool *)
@@ -1199,8 +1222,6 @@
|> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
-datatype fixpoint_kind = Lfp | Gfp | NoFp
-
(* term -> fixpoint_kind *)
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
| fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
@@ -1299,35 +1320,6 @@
Unsynchronized.change simp_table
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
-(* Similar to "Refute.specialize_type" but returns all matches rather than only
- the first (preorder) match. *)
-(* theory -> styp -> term -> term list *)
-fun multi_specialize_type thy slack (x as (s, T)) t =
- let
- (* term -> (typ * term) list -> (typ * term) list *)
- fun aux (Const (s', T')) ys =
- if s = s' then
- ys |> (if AList.defined (op =) ys T' then
- I
- else
- cons (T', Refute.monomorphic_term
- (Sign.typ_match thy (T', T) Vartab.empty) t)
- handle Type.TYPE_MATCH => I
- | Refute.REFUTE _ =>
- if slack then
- I
- else
- raise NOT_SUPPORTED ("too much polymorphism in \
- \axiom involving " ^ quote s))
- else
- ys
- | aux _ ys = ys
- in map snd (fold_aterms aux t []) end
-
-(* theory -> bool -> const_table -> styp -> term list *)
-fun nondef_props_for_const thy slack table (x as (s, _)) =
- these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
-
(* theory -> styp -> term list *)
fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
let val abs_T = domain_type T in
@@ -1336,7 +1328,7 @@
|> pairself (Refute.specialize_type thy x o prop_of o the)
||> single |> op ::
end
-(* theory -> styp list -> term list *)
+(* theory -> string * typ list -> term list *)
fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
let val abs_T = Type abs_z in
if is_univ_typedef thy abs_T then
@@ -1392,15 +1384,15 @@
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-(* extended_context -> typ -> int * styp -> term -> term *)
-fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
+(* hol_context -> typ -> int * styp -> term -> term *)
+fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
+ $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
$ res_t
-(* extended_context -> typ -> typ -> term *)
-fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
+(* hol_context -> typ -> typ -> term *)
+fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
let
- val xs = datatype_constrs ext_ctxt dataT
+ val xs = datatype_constrs hol_ctxt dataT
val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
in
@@ -1409,19 +1401,19 @@
val (xs'', x) = split_last xs'
in
constr_case_body thy (1, x)
- |> fold_rev (add_constr_case ext_ctxt res_T)
+ |> fold_rev (add_constr_case hol_ctxt res_T)
(length xs' downto 2 ~~ xs'')
end
else
Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
- |> fold_rev (add_constr_case ext_ctxt res_T)
+ |> fold_rev (add_constr_case hol_ctxt res_T)
(length xs' downto 1 ~~ xs'))
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-(* extended_context -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
- let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
+(* hol_context -> string -> typ -> typ -> term -> term *)
+fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
+ let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
Type (_, Ts as _ :: _) =>
@@ -1430,16 +1422,16 @@
val j = num_record_fields thy rec_T - 1
in
select_nth_constr_arg thy constr_x t j res_T
- |> optimized_record_get ext_ctxt s rec_T' res_T
+ |> optimized_record_get hol_ctxt s rec_T' res_T
end
| _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
[]))
| j => select_nth_constr_arg thy constr_x t j res_T
end
-(* extended_context -> string -> typ -> term -> term -> term *)
-fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
+(* hol_context -> string -> typ -> term -> term -> term *)
+fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
let
- val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
+ val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
val Ts = binder_types constr_T
val n = length Ts
val special_j = no_of_record_field thy s rec_T
@@ -1450,7 +1442,7 @@
if j = special_j then
betapply (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
- optimized_record_update ext_ctxt s
+ optimized_record_update hol_ctxt s
(rec_T |> dest_Type |> snd |> List.last) fun_t t
else
t
@@ -1473,19 +1465,19 @@
fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-(* extended_context -> styp -> bool *)
+(* hol_context -> styp -> bool *)
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
- : extended_context) x =
+ : hol_context) x =
not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
fixpoint_kind_of_const thy def_table x <> NoFp
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
- : extended_context) x =
+ : hol_context) x =
exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
[!simp_table, psimp_table]
-fun is_inductive_pred ext_ctxt =
- is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
-fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
- (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
+fun is_inductive_pred hol_ctxt =
+ is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
+fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
+ (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
andf (not o has_trivial_definition thy def_table)
@@ -1522,11 +1514,11 @@
SOME t' => is_constr_pattern_lhs thy t'
| NONE => false
+(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
val unfold_max_depth = 255
-val axioms_max_depth = 255
-(* extended_context -> term -> term *)
-fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
+(* hol_context -> term -> term *)
+fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
case_names, def_table, ground_thm_table,
ersatz_table, ...}) =
let
@@ -1600,7 +1592,7 @@
val (dataT, res_T) = nth_range_type n T
|> pairf domain_type range_type
in
- (optimized_case_def ext_ctxt dataT res_T
+ (optimized_case_def hol_ctxt dataT res_T
|> do_term (depth + 1) Ts, ts)
end
| _ =>
@@ -1628,11 +1620,11 @@
else if is_record_get thy x then
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
- | _ => (optimized_record_get ext_ctxt s (domain_type T)
+ | _ => (optimized_record_get hol_ctxt s (domain_type T)
(range_type T) (do_term depth Ts (hd ts)), tl ts)
else if is_record_update thy x then
case length ts of
- 2 => (optimized_record_update ext_ctxt
+ 2 => (optimized_record_update hol_ctxt
(unsuffix Record.updateN s) (nth_range_type 2 T)
(do_term depth Ts (hd ts))
(do_term depth Ts (nth ts 1)), [])
@@ -1645,7 +1637,7 @@
else
(Const x, ts)
end
- else if is_equational_fun ext_ctxt x then
+ else if is_equational_fun hol_ctxt x then
(Const x, ts)
else case def_of_const thy def_table x of
SOME def =>
@@ -1662,10 +1654,10 @@
in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
in do_term 0 [] end
-(* extended_context -> typ -> term list *)
-fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
+(* hol_context -> typ -> term list *)
+fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
let
- val xs = datatype_constrs ext_ctxt T
+ val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
val iter_T = @{typ bisim_iterator}
val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
@@ -1688,14 +1680,14 @@
let
val arg_Ts = binder_types T
val core_t =
- discriminate_value ext_ctxt x y_var ::
+ discriminate_value hol_ctxt x y_var ::
map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
|> foldr1 s_conj
in List.foldr absdummy core_t arg_Ts end
in
[HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
$ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
- $ (betapplys (optimized_case_def ext_ctxt T bool_T,
+ $ (betapplys (optimized_case_def hol_ctxt T bool_T,
map case_func xs @ [x_var]))),
HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
$ (Const (@{const_name insert}, T --> set_T --> set_T)
@@ -1754,10 +1746,10 @@
val termination_tacs = [Lexicographic_Order.lex_order_tac true,
ScnpReconstruct.sizechange_tac]
-(* extended_context -> const_table -> styp -> bool *)
+(* hol_context -> const_table -> styp -> bool *)
fun uncached_is_well_founded_inductive_pred
({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
- : extended_context) (x as (_, T)) =
+ : hol_context) (x as (_, T)) =
case def_props_for_const thy fast_descrs intro_table x of
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
@@ -1797,11 +1789,11 @@
handle List.Empty => false
| NO_TRIPLE () => false
-(* The type constraint below is a workaround for a Poly/ML bug. *)
+(* The type constraint below is a workaround for a Poly/ML crash. *)
-(* extended_context -> styp -> bool *)
+(* hol_context -> styp -> bool *)
fun is_well_founded_inductive_pred
- (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
+ (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
@@ -1811,7 +1803,7 @@
| NONE =>
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
+ val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
in
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
end
@@ -1842,14 +1834,14 @@
| do_disjunct j t =
case num_occs_of_bound_in_term j t of
0 => true
- | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
+ | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
| _ => false
(* term -> bool *)
fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
let val (xs, body) = strip_abs t2 in
case length xs of
1 => false
- | n => forall (do_disjunct (n - 1)) (disjuncts body)
+ | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
end
| do_lfp_def _ = false
in do_lfp_def o strip_abs_body end
@@ -1887,7 +1879,7 @@
end
val (nonrecs, recs) =
List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
- (disjuncts body)
+ (disjuncts_of body)
val base_body = nonrecs |> List.foldl s_disj @{const False}
val step_body = recs |> map (repair_rec j)
|> List.foldl s_disj @{const False}
@@ -1901,8 +1893,8 @@
raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
in aux end
-(* extended_context -> styp -> term -> term *)
-fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
+(* hol_context -> styp -> term -> term *)
+fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
def =
let
val j = maxidx_of_term def + 1
@@ -1933,11 +1925,11 @@
$ list_comb (Const step_x, outer_bounds)))
$ list_comb (Const base_x, outer_bounds)
|> ap_curry tuple_arg_Ts tuple_T bool_T)
- |> unfold_defs_in_term ext_ctxt
+ |> unfold_defs_in_term hol_ctxt
end
-(* extended_context -> bool -> styp -> term *)
-fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
+(* hol_context -> bool -> styp -> term *)
+fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
def_table, simp_table, ...})
gfp (x as (s, T)) =
let
@@ -1946,11 +1938,11 @@
val unrolled_const = Const x' $ zero_const iter_T
val def = the (def_of_const thy def_table x)
in
- if is_equational_fun ext_ctxt x' then
+ if is_equational_fun hol_ctxt x' then
unrolled_const (* already done *)
else if not gfp andalso is_linear_inductive_pred_def def andalso
star_linear_preds then
- starred_linear_pred_const ext_ctxt x def
+ starred_linear_pred_const hol_ctxt x def
else
let
val j = maxidx_of_term def + 1
@@ -1973,8 +1965,8 @@
in unrolled_const end
end
-(* extended_context -> styp -> term *)
-fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
+(* hol_context -> styp -> term *)
+fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
let
val def = the (def_of_const thy def_table x)
val (outer, fp_app) = strip_abs def
@@ -1992,24 +1984,29 @@
HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
|> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
end
-fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
+fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
let val x' = (after_name_sep s, T) in
- raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
+ raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
end
else
- raw_inductive_pred_axiom ext_ctxt x
+ raw_inductive_pred_axiom hol_ctxt x
-(* extended_context -> styp -> term list *)
-fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
+(* hol_context -> styp -> term list *)
+fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
psimp_table, ...}) (x as (s, _)) =
case def_props_for_const thy fast_descrs (!simp_table) x of
[] => (case def_props_for_const thy fast_descrs psimp_table x of
- [] => [inductive_pred_axiom ext_ctxt x]
+ [] => [inductive_pred_axiom hol_ctxt x]
| psimps => psimps)
| simps => simps
-
val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
+(* hol_context -> styp -> bool *)
+fun is_equational_fun_surely_complete hol_ctxt x =
+ case raw_equational_fun_axioms hol_ctxt x of
+ [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
+ strip_comb t1 |> snd |> forall is_Var
+ | _ => false
(* term list -> term list *)
fun merge_type_vars_in_terms ts =
@@ -2028,1261 +2025,29 @@
| coalesce T = T
in map (map_types (map_atyps coalesce)) ts end
-(* extended_context -> typ -> typ list -> typ list *)
-fun add_ground_types ext_ctxt T accum =
+(* hol_context -> typ -> typ list -> typ list *)
+fun add_ground_types hol_ctxt T accum =
case T of
- Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
- | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
- | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
+ Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
+ | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
+ | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
| Type (_, Ts) =>
- if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
+ if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
+ @{typ \<xi>} :: accum) T then
accum
else
T :: accum
- |> fold (add_ground_types ext_ctxt)
- (case boxed_datatype_constrs ext_ctxt T of
+ |> fold (add_ground_types hol_ctxt)
+ (case boxed_datatype_constrs hol_ctxt T of
[] => Ts
| xs => map snd xs)
| _ => insert (op =) T accum
-(* extended_context -> typ -> typ list *)
-fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
-(* extended_context -> term list -> typ list *)
-fun ground_types_in_terms ext_ctxt ts =
- fold (fold_types (add_ground_types ext_ctxt)) ts []
-(* typ list -> int -> term -> bool *)
-fun has_heavy_bounds_or_vars Ts level t =
- let
- (* typ list -> bool *)
- fun aux [] = false
- | aux [T] = is_fun_type T orelse is_pair_type T
- | aux _ = true
- in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-
-(* typ list -> int -> int -> int -> term -> term *)
-fun fresh_value_var Ts k n j t =
- Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
-
-(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
- -> term * term list *)
-fun pull_out_constr_comb thy Ts relax k level t args seen =
- let val t_comb = list_comb (t, args) in
- case t of
- Const x =>
- if not relax andalso is_constr thy x andalso
- not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
- has_heavy_bounds_or_vars Ts level t_comb andalso
- not (loose_bvar (t_comb, level)) then
- let
- val (j, seen) = case find_index (curry (op =) t_comb) seen of
- ~1 => (0, t_comb :: seen)
- | j => (j, seen)
- in (fresh_value_var Ts k (length seen) j t_comb, seen) end
- else
- (t_comb, seen)
- | _ => (t_comb, seen)
- end
-
-(* (term -> term) -> typ list -> int -> term list -> term list *)
-fun equations_for_pulled_out_constrs mk_eq Ts k seen =
- let val n = length seen in
- map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
- (index_seq 0 n) seen
- end
-
-(* theory -> bool -> term -> term *)
-fun pull_out_universal_constrs thy def t =
- let
- val k = maxidx_of_term t + 1
- (* typ list -> bool -> term -> term list -> term list -> term * term list *)
- fun do_term Ts def t args seen =
- case t of
- (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
- do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "==>"}) $ t1 $ t2 =>
- if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
- | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
- do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "op -->"}) $ t1 $ t2 =>
- do_eq_or_imp Ts false def t0 t1 t2 seen
- | Abs (s, T, t') =>
- let val (t', seen) = do_term (T :: Ts) def t' [] seen in
- (list_comb (Abs (s, T, t'), args), seen)
- end
- | t1 $ t2 =>
- let val (t2, seen) = do_term Ts def t2 [] seen in
- do_term Ts def t1 (t2 :: args) seen
- end
- | _ => pull_out_constr_comb thy Ts def k 0 t args seen
- (* typ list -> bool -> bool -> term -> term -> term -> term list
- -> term * term list *)
- and do_eq_or_imp Ts eq def t0 t1 t2 seen =
- let
- val (t2, seen) = if eq andalso def then (t2, seen)
- else do_term Ts false t2 [] seen
- val (t1, seen) = do_term Ts false t1 [] seen
- in (t0 $ t1 $ t2, seen) end
- val (concl, seen) = do_term [] def t [] []
- in
- Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
- seen, concl)
- end
-
-(* extended_context -> bool -> term -> term *)
-fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
- let
- (* styp -> int *)
- val num_occs_of_var =
- fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
- | _ => I) t (K 0)
- (* bool -> term -> term *)
- fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
- | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
- | aux _ t = t
- (* bool -> bool -> term -> term -> term -> term *)
- and aux_eq careful pass1 t0 t1 t2 =
- ((if careful then
- raise SAME ()
- else if axiom andalso is_Var t2 andalso
- num_occs_of_var (dest_Var t2) = 1 then
- @{const True}
- else case strip_comb t2 of
- (* The first case is not as general as it could be. *)
- (Const (@{const_name PairBox}, _),
- [Const (@{const_name fst}, _) $ Var z1,
- Const (@{const_name snd}, _) $ Var z2]) =>
- if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
- else raise SAME ()
- | (Const (x as (s, T)), args) =>
- let val arg_Ts = binder_types T in
- if length arg_Ts = length args andalso
- (is_constr thy x orelse s = @{const_name Pair} orelse
- x = (@{const_name Suc}, nat_T --> nat_T)) andalso
- (not careful orelse not (is_Var t1) orelse
- String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- discriminate_value ext_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
- |> foldr1 s_conj
- else
- raise SAME ()
- end
- | _ => raise SAME ())
- |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
- handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
- else t0 $ aux false t2 $ aux false t1
- (* styp -> term -> int -> typ -> term -> term *)
- and sel_eq x t n nth_T nth_t =
- HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
- |> aux false
- in aux axiom t end
-
-(* theory -> term -> term *)
-fun simplify_constrs_and_sels thy t =
- let
- (* term -> int -> term *)
- fun is_nth_sel_on t' n (Const (s, _) $ t) =
- (t = t' andalso is_sel_like_and_no_discr s andalso
- sel_no_from_name s = n)
- | is_nth_sel_on _ _ _ = false
- (* term -> term list -> term *)
- fun do_term (Const (@{const_name Rep_Frac}, _)
- $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
- | do_term (Const (@{const_name Abs_Frac}, _)
- $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
- | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
- | do_term (t as Const (x as (s, T))) (args as _ :: _) =
- ((if is_constr_like thy x then
- if length args = num_binder_types T then
- case hd args of
- Const (x' as (_, T')) $ t' =>
- if domain_type T' = body_type T andalso
- forall (uncurry (is_nth_sel_on t'))
- (index_seq 0 (length args) ~~ args) then
- t'
- else
- raise SAME ()
- | _ => raise SAME ()
- else
- raise SAME ()
- else if is_sel_like_and_no_discr s then
- case strip_comb (hd args) of
- (Const (x' as (s', T')), ts') =>
- if is_constr_like thy x' andalso
- constr_name_for_sel_like s = s' andalso
- not (exists is_pair_type (binder_types T')) then
- list_comb (nth ts' (sel_no_from_name s), tl args)
- else
- raise SAME ()
- | _ => raise SAME ()
- else
- raise SAME ())
- handle SAME () => betapplys (t, args))
- | do_term (Abs (s, T, t')) args =
- betapplys (Abs (s, T, do_term t' []), args)
- | do_term t args = betapplys (t, args)
- in do_term t [] end
-
-(* term -> term *)
-fun curry_assms (@{const "==>"} $ (@{const Trueprop}
- $ (@{const "op &"} $ t1 $ t2)) $ t3) =
- curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
- | curry_assms (@{const "==>"} $ t1 $ t2) =
- @{const "==>"} $ curry_assms t1 $ curry_assms t2
- | curry_assms t = t
-
-(* term -> term *)
-val destroy_universal_equalities =
- let
- (* term list -> (indexname * typ) list -> term -> term *)
- fun aux prems zs t =
- case t of
- @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
- | _ => Logic.list_implies (rev prems, t)
- (* term list -> (indexname * typ) list -> term -> term -> term *)
- and aux_implies prems zs t1 t2 =
- case t1 of
- Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
- aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
- aux_eq prems zs z t' t1 t2
- | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
- (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
- -> term -> term *)
- and aux_eq prems zs z t' t1 t2 =
- if not (member (op =) zs z) andalso
- not (exists_subterm (curry (op =) (Var z)) t') then
- aux prems zs (subst_free [(Var z, t')] t2)
- else
- aux (t1 :: prems) (Term.add_vars t1 zs) t2
- in aux [] [] end
-
-(* theory -> term -> term *)
-fun pull_out_existential_constrs thy t =
- let
- val k = maxidx_of_term t + 1
- (* typ list -> int -> term -> term list -> term list -> term * term list *)
- fun aux Ts num_exists t args seen =
- case t of
- (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
- let
- val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
- val n = length seen'
- (* unit -> term list *)
- fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
- in
- (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
- |> List.foldl s_conj t1 |> fold mk_exists (vars ())
- |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
- end
- | t1 $ t2 =>
- let val (t2, seen) = aux Ts num_exists t2 [] seen in
- aux Ts num_exists t1 (t2 :: args) seen
- end
- | Abs (s, T, t') =>
- let
- val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
- in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
- | _ =>
- if num_exists > 0 then
- pull_out_constr_comb thy Ts false k num_exists t args seen
- else
- (list_comb (t, args), seen)
- in aux [] 0 t [] [] |> fst end
-
-(* theory -> int -> term list -> term list -> (term * term list) option *)
-fun find_bound_assign _ _ _ [] = NONE
- | find_bound_assign thy j seen (t :: ts) =
- let
- (* bool -> term -> term -> (term * term list) option *)
- fun aux pass1 t1 t2 =
- (if loose_bvar1 (t2, j) then
- if pass1 then aux false t2 t1 else raise SAME ()
- else case t1 of
- Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
- | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
- if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
- SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
- ts @ seen)
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () => find_bound_assign thy j (t :: seen) ts
- in
- case t of
- Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
- | _ => find_bound_assign thy j (t :: seen) ts
- end
-
-(* int -> term -> term -> term *)
-fun subst_one_bound j arg t =
- let
- fun aux (Bound i, lev) =
- if i < lev then raise SAME ()
- else if i = lev then incr_boundvars (lev - j) arg
- else Bound (i - 1)
- | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
- | aux (f $ t, lev) =
- (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
- handle SAME () => f $ aux (t, lev))
- | aux _ = raise SAME ()
- in aux (t, j) handle SAME () => t end
-
-(* theory -> term -> term *)
-fun destroy_existential_equalities thy =
- let
- (* string list -> typ list -> term list -> term *)
- fun kill [] [] ts = foldr1 s_conj ts
- | kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign thy (length ss) [] ts of
- SOME (_, []) => @{const True}
- | SOME (arg_t, ts) =>
- kill ss Ts (map (subst_one_bound (length ss)
- (incr_bv (~1, length ss + 1, arg_t))) ts)
- | NONE =>
- Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
- $ Abs (s, T, kill ss Ts ts))
- | kill _ _ _ = raise UnequalLengths
- (* string list -> typ list -> term -> term *)
- fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
- gather (ss @ [s1]) (Ts @ [T1]) t1
- | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
- | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
- | gather [] [] t = t
- | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
- in gather [] [] end
-
-(* term -> term *)
-fun distribute_quantifiers t =
- case t of
- (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
- (case t1 of
- (t10 as @{const "op &"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const Not}) $ t11 =>
- t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
- $ Abs (s, T1, t11))
- | t1 =>
- if not (loose_bvar1 (t1, 0)) then
- distribute_quantifiers (incr_boundvars ~1 t1)
- else
- t0 $ Abs (s, T1, distribute_quantifiers t1))
- | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
- (case distribute_quantifiers t1 of
- (t10 as @{const "op |"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const "op -->"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
- $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const Not}) $ t11 =>
- t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
- $ Abs (s, T1, t11))
- | t1 =>
- if not (loose_bvar1 (t1, 0)) then
- distribute_quantifiers (incr_boundvars ~1 t1)
- else
- t0 $ Abs (s, T1, distribute_quantifiers t1))
- | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
- | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
- | _ => t
-
-(* int -> int -> (int -> int) -> term -> term *)
-fun renumber_bounds j n f t =
- case t of
- t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
- | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
- | Bound j' =>
- Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
- | _ => t
-
-val quantifier_cluster_threshold = 7
-
-(* theory -> term -> term *)
-fun push_quantifiers_inward thy =
- let
- (* string -> string list -> typ list -> term -> term *)
- fun aux quant_s ss Ts t =
- (case t of
- (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
- if s0 = quant_s then
- aux s0 (s1 :: ss) (T1 :: Ts) t1
- else if quant_s = "" andalso
- (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
- aux s0 [s1] [T1] t1
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- case t of
- t1 $ t2 =>
- if quant_s = "" then
- aux "" [] [] t1 $ aux "" [] [] t2
- else
- let
- val typical_card = 4
- (* ('a -> ''b list) -> 'a list -> ''b list *)
- fun big_union proj ps =
- fold (fold (insert (op =)) o proj) ps []
- val (ts, connective) = strip_any_connective t
- val T_costs =
- map (bounded_card_of_type 65536 typical_card []) Ts
- val t_costs = map size_of_term ts
- val num_Ts = length Ts
- (* int -> int *)
- val flip = curry (op -) (num_Ts - 1)
- val t_boundss = map (map flip o loose_bnos) ts
- (* (int list * int) list -> int list
- -> (int list * int) list *)
- fun merge costly_boundss [] = costly_boundss
- | merge costly_boundss (j :: js) =
- let
- val (yeas, nays) =
- List.partition (fn (bounds, _) =>
- member (op =) bounds j)
- costly_boundss
- val yeas_bounds = big_union fst yeas
- val yeas_cost = Integer.sum (map snd yeas)
- * nth T_costs j
- in merge ((yeas_bounds, yeas_cost) :: nays) js end
- (* (int list * int) list -> int list -> int *)
- val cost = Integer.sum o map snd oo merge
- (* Inspired by Claessen & Sörensson's polynomial binary
- splitting heuristic (p. 5 of their MODEL 2003 paper). *)
- (* (int list * int) list -> int list -> int list *)
- fun heuristically_best_permutation _ [] = []
- | heuristically_best_permutation costly_boundss js =
- let
- val (costly_boundss, (j, js)) =
- js |> map (`(merge costly_boundss o single))
- |> sort (int_ord
- o pairself (Integer.sum o map snd o fst))
- |> split_list |>> hd ||> pairf hd tl
- in
- j :: heuristically_best_permutation costly_boundss js
- end
- val js =
- if length Ts <= quantifier_cluster_threshold then
- all_permutations (index_seq 0 num_Ts)
- |> map (`(cost (t_boundss ~~ t_costs)))
- |> sort (int_ord o pairself fst) |> hd |> snd
- else
- heuristically_best_permutation (t_boundss ~~ t_costs)
- (index_seq 0 num_Ts)
- val back_js = map (fn j => find_index (curry (op =) j) js)
- (index_seq 0 num_Ts)
- val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
- ts
- (* (term * int list) list -> term *)
- fun mk_connection [] =
- raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
- \mk_connection", "")
- | mk_connection ts_cum_bounds =
- ts_cum_bounds |> map fst
- |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
- (* (term * int list) list -> int list -> term *)
- fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
- | build ts_cum_bounds (j :: js) =
- let
- val (yeas, nays) =
- List.partition (fn (_, bounds) =>
- member (op =) bounds j)
- ts_cum_bounds
- ||> map (apfst (incr_boundvars ~1))
- in
- if null yeas then
- build nays js
- else
- let val T = nth Ts (flip j) in
- build ((Const (quant_s, (T --> bool_T) --> bool_T)
- $ Abs (nth ss (flip j), T,
- mk_connection yeas),
- big_union snd yeas) :: nays) js
- end
- end
- in build (ts ~~ t_boundss) js end
- | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
- | _ => t
- in aux "" [] [] end
-
-(* polarity -> string -> bool *)
-fun is_positive_existential polar quant_s =
- (polar = Pos andalso quant_s = @{const_name Ex}) orelse
- (polar = Neg andalso quant_s <> @{const_name Ex})
-
-(* extended_context -> int -> term -> term *)
-fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
- skolem_depth =
- let
- (* int list -> int list *)
- val incrs = map (Integer.add 1)
- (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
- fun aux ss Ts js depth polar t =
- let
- (* string -> typ -> string -> typ -> term -> term *)
- fun do_quantifier quant_s quant_T abs_s abs_T t =
- if not (loose_bvar1 (t, 0)) then
- aux ss Ts js depth polar (incr_boundvars ~1 t)
- else if depth <= skolem_depth andalso
- is_positive_existential polar quant_s then
- let
- val j = length (!skolems) + 1
- val sko_s = skolem_prefix_for (length js) j ^ abs_s
- val _ = Unsynchronized.change skolems (cons (sko_s, ss))
- val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
- map Bound (rev js))
- val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
- in
- if null js then betapply (abs_t, sko_t)
- else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
- end
- else
- Const (quant_s, quant_T)
- $ Abs (abs_s, abs_T,
- if is_higher_order_type abs_T then
- t
- else
- aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
- (depth + 1) polar t)
- in
- case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
- | @{const Pure.conjunction} $ t1 $ t2 =>
- @{const Pure.conjunction} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const Trueprop} $ t1 =>
- @{const Trueprop} $ aux ss Ts js depth polar t1
- | @{const Not} $ t1 =>
- @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
- | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
- | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
- t0 $ t1 $ aux ss Ts js depth polar t2
- | Const (x as (s, T)) =>
- if is_inductive_pred ext_ctxt x andalso
- not (is_well_founded_inductive_pred ext_ctxt x) then
- let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val (pref, connective, set_oper) =
- if gfp then
- (lbfp_prefix,
- @{const "op |"},
- @{const_name semilattice_sup_fun_inst.sup_fun})
- else
- (ubfp_prefix,
- @{const "op &"},
- @{const_name semilattice_inf_fun_inst.inf_fun})
- (* unit -> term *)
- fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
- |> aux ss Ts js depth polar
- fun neg () = Const (pref ^ s, T)
- in
- (case polar |> gfp ? flip_polarity of
- Pos => pos ()
- | Neg => neg ()
- | Neut =>
- if is_fun_type T then
- let
- val ((trunk_arg_Ts, rump_arg_T), body_T) =
- T |> strip_type |>> split_last
- val set_T = rump_arg_T --> body_T
- (* (unit -> term) -> term *)
- fun app f =
- list_comb (f (),
- map Bound (length trunk_arg_Ts - 1 downto 0))
- in
- List.foldr absdummy
- (Const (set_oper, set_T --> set_T --> set_T)
- $ app pos $ app neg) trunk_arg_Ts
- end
- else
- connective $ pos () $ neg ())
- end
- else
- Const x
- | t1 $ t2 =>
- betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
- aux ss Ts [] depth Neut t2)
- | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
- | _ => t
- end
- in aux [] [] [] 0 Pos end
-
-(* extended_context -> styp -> (int * term option) list *)
-fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
- let
- (* term -> term list -> term list -> term list list *)
- fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
- | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
- | fun_calls t args =
- (case t of
- Const (x' as (s', T')) =>
- x = x' orelse (case AList.lookup (op =) ersatz_table s' of
- SOME s'' => x = (s'', T')
- | NONE => false)
- | _ => false) ? cons args
- (* term list list -> term list list -> term list -> term list list *)
- fun call_sets [] [] vs = [vs]
- | call_sets [] uss vs = vs :: call_sets uss [] []
- | call_sets ([] :: _) _ _ = []
- | call_sets ((t :: ts) :: tss) uss vs =
- OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
- val sets = call_sets (fun_calls t [] []) [] []
- val indexed_sets = sets ~~ (index_seq 0 (length sets))
- in
- fold_rev (fn (set, j) =>
- case set of
- [Var _] => AList.lookup (op =) indexed_sets set = SOME j
- ? cons (j, NONE)
- | [t as Const _] => cons (j, SOME t)
- | [t as Free _] => cons (j, SOME t)
- | _ => I) indexed_sets []
- end
-(* extended_context -> styp -> term list -> (int * term option) list *)
-fun static_args_in_terms ext_ctxt x =
- map (static_args_in_term ext_ctxt x)
- #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
-
-(* term -> term list *)
-fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
- | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
- | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
- snd (strip_comb t1)
- | params_in_equation _ = []
-
-(* styp -> styp -> int list -> term list -> term list -> term -> term *)
-fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
- let
- val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
- + 1
- val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
- val fixed_params = filter_indices fixed_js (params_in_equation t)
- (* term list -> term -> term *)
- fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
- | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
- | aux args t =
- if t = Const x then
- list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
- else
- let val j = find_index (curry (op =) t) fixed_params in
- list_comb (if j >= 0 then nth fixed_args j else t, args)
- end
- in aux [] t end
-
-(* typ list -> term -> bool *)
-fun is_eligible_arg Ts t =
- let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
- null bad_Ts orelse
- (is_higher_order_type (fastype_of1 (Ts, t)) andalso
- forall (not o is_higher_order_type) bad_Ts)
- end
-
-(* (int * term option) list -> (int * term) list -> int list *)
-fun overlapping_indices [] _ = []
- | overlapping_indices _ [] = []
- | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
- if j1 < j2 then overlapping_indices ps1' ps2
- else if j1 > j2 then overlapping_indices ps1 ps2'
- else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
-
-val special_depth = 20
-
-(* extended_context -> int -> term -> term *)
-fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
- special_funs, ...}) depth t =
- if not specialize orelse depth > special_depth then
- t
- else
- let
- val blacklist = if depth = 0 then []
- else case term_under_def t of Const x => [x] | _ => []
- (* term list -> typ list -> term -> term *)
- fun aux args Ts (Const (x as (s, T))) =
- ((if not (member (op =) blacklist x) andalso not (null args) andalso
- not (String.isPrefix special_prefix s) andalso
- is_equational_fun ext_ctxt x then
- let
- val eligible_args = filter (is_eligible_arg Ts o snd)
- (index_seq 0 (length args) ~~ args)
- val _ = not (null eligible_args) orelse raise SAME ()
- val old_axs = equational_fun_axioms ext_ctxt x
- |> map (destroy_existential_equalities thy)
- val static_params = static_args_in_terms ext_ctxt x old_axs
- val fixed_js = overlapping_indices static_params eligible_args
- val _ = not (null fixed_js) orelse raise SAME ()
- val fixed_args = filter_indices fixed_js args
- val vars = fold Term.add_vars fixed_args []
- |> sort (TermOrd.fast_indexname_ord o pairself fst)
- val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
- fixed_args []
- |> sort int_ord
- val live_args = filter_out_indices fixed_js args
- val extra_args = map Var vars @ map Bound bound_js @ live_args
- val extra_Ts = map snd vars @ filter_indices bound_js Ts
- val k = maxidx_of_term t + 1
- (* int -> term *)
- fun var_for_bound_no j =
- Var ((bound_var_prefix ^
- nat_subscript (find_index (curry (op =) j) bound_js
- + 1), k),
- nth Ts j)
- val fixed_args_in_axiom =
- map (curry subst_bounds
- (map var_for_bound_no (index_seq 0 (length Ts))))
- fixed_args
- in
- case AList.lookup (op =) (!special_funs)
- (x, fixed_js, fixed_args_in_axiom) of
- SOME x' => list_comb (Const x', extra_args)
- | NONE =>
- let
- val extra_args_in_axiom =
- map Var vars @ map var_for_bound_no bound_js
- val x' as (s', _) =
- (special_prefix_for (length (!special_funs) + 1) ^ s,
- extra_Ts @ filter_out_indices fixed_js (binder_types T)
- ---> body_type T)
- val new_axs =
- map (specialize_fun_axiom x x' fixed_js
- fixed_args_in_axiom extra_args_in_axiom) old_axs
- val _ =
- Unsynchronized.change special_funs
- (cons ((x, fixed_js, fixed_args_in_axiom), x'))
- val _ = add_simps simp_table s' new_axs
- in list_comb (Const x', extra_args) end
- end
- else
- raise SAME ())
- handle SAME () => list_comb (Const x, args))
- | aux args Ts (Abs (s, T, t)) =
- list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
- | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
- | aux args _ t = list_comb (t, args)
- in aux [] [] t end
-
-(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
-fun add_to_uncurry_table thy t =
- let
- (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
- fun aux (t1 $ t2) args table =
- let val table = aux t2 [] table in aux t1 (t2 :: args) table end
- | aux (Abs (_, _, t')) _ table = aux t' [] table
- | aux (t as Const (x as (s, _))) args table =
- if is_built_in_const true x orelse is_constr_like thy x orelse
- is_sel s orelse s = @{const_name Sigma} then
- table
- else
- Termtab.map_default (t, 65536) (curry Int.min (length args)) table
- | aux _ _ table = table
- in aux t [] end
-
-(* int Termtab.tab term -> term *)
-fun uncurry_term table t =
- let
- (* term -> term list -> term *)
- fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
- | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
- | aux (t as Const (s, T)) args =
- (case Termtab.lookup table t of
- SOME n =>
- if n >= 2 then
- let
- val (arg_Ts, rest_T) = strip_n_binders n T
- val j =
- if hd arg_Ts = @{typ bisim_iterator} orelse
- is_fp_iterator_type (hd arg_Ts) then
- 1
- else case find_index (not_equal bool_T) arg_Ts of
- ~1 => n
- | j => j
- val ((before_args, tuple_args), after_args) =
- args |> chop n |>> chop j
- val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
- T |> strip_n_binders n |>> chop j
- val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
- in
- if n - j < 2 then
- betapplys (t, args)
- else
- betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
- before_arg_Ts ---> tuple_T --> rest_T),
- before_args @ [mk_flat_tuple tuple_T tuple_args] @
- after_args)
- end
- else
- betapplys (t, args)
- | NONE => betapplys (t, args))
- | aux t args = betapplys (t, args)
- in aux t [] end
-
-(* (term -> term) -> int -> term -> term *)
-fun coerce_bound_no f j t =
- case t of
- t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
- | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
- | Bound j' => if j' = j then f t else t
- | _ => t
-
-(* extended_context -> bool -> term -> term *)
-fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
- let
- (* typ -> typ *)
- fun box_relational_operator_type (Type ("fun", Ts)) =
- Type ("fun", map box_relational_operator_type Ts)
- | box_relational_operator_type (Type ("*", Ts)) =
- Type ("*", map (box_type ext_ctxt InPair) Ts)
- | box_relational_operator_type T = T
- (* typ -> typ -> term -> term *)
- fun coerce_bound_0_in_term new_T old_T =
- old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
- (* typ list -> typ -> term -> term *)
- and coerce_term Ts new_T old_T t =
- if old_T = new_T then
- t
- else
- case (new_T, old_T) of
- (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type ("fun", [old_T1, old_T2])) =>
- (case eta_expand Ts t 1 of
- Abs (s, _, t') =>
- Abs (s, new_T1,
- t' |> coerce_bound_0_in_term new_T1 old_T1
- |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
- |> Envir.eta_contract
- |> new_s <> "fun"
- ? construct_value thy (@{const_name FunBox},
- Type ("fun", new_Ts) --> new_T) o single
- | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \coerce_term", [t']))
- | (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = "*" then
- case constr_expand ext_ctxt old_T t of
- Const (@{const_name FunBox}, _) $ t1 =>
- if new_s = "fun" then
- coerce_term Ts new_T (Type ("fun", old_Ts)) t1
- else
- construct_value thy
- (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- [coerce_term Ts (Type ("fun", new_Ts))
- (Type ("fun", old_Ts)) t1]
- | Const _ $ t1 $ t2 =>
- construct_value thy
- (if new_s = "*" then @{const_name Pair}
- else @{const_name PairBox}, new_Ts ---> new_T)
- [coerce_term Ts new_T1 old_T1 t1,
- coerce_term Ts new_T2 old_T2 t2]
- | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \coerce_term", [t'])
- else
- raise TYPE ("coerce_term", [new_T, old_T], [t])
- | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
- (* indexname * typ -> typ * term -> typ option list -> typ option list *)
- fun add_boxed_types_for_var (z as (_, T)) (T', t') =
- case t' of
- Var z' => z' = z ? insert (op =) T'
- | Const (@{const_name Pair}, _) $ t1 $ t2 =>
- (case T' of
- Type (_, [T1, T2]) =>
- fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
- | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \add_boxed_types_for_var", [T'], []))
- | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
- (* typ list -> typ list -> term -> indexname * typ -> typ *)
- fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
- case t of
- @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
- | Const (s0, _) $ t1 $ _ =>
- if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
- let
- val (t', args) = strip_comb t1
- val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
- in
- case fold (add_boxed_types_for_var z)
- (fst (strip_n_binders (length args) T') ~~ args) [] of
- [T''] => T''
- | _ => T
- end
- else
- T
- | _ => T
- (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
- -> term -> term *)
- and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
- let
- val abs_T' =
- if polar = Neut orelse is_positive_existential polar quant_s then
- box_type ext_ctxt InFunLHS abs_T
- else
- abs_T
- val body_T = body_type quant_T
- in
- Const (quant_s, (abs_T' --> body_T) --> body_T)
- $ Abs (abs_s, abs_T',
- t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
- end
- (* typ list -> typ list -> string -> typ -> term -> term -> term *)
- and do_equals new_Ts old_Ts s0 T0 t1 t2 =
- let
- val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
- val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
- val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
- in
- list_comb (Const (s0, T --> T --> body_type T0),
- map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
- end
- (* string -> typ -> term *)
- and do_description_operator s T =
- let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
- Const (s, (T1 --> bool_T) --> T1)
- end
- (* typ list -> typ list -> polarity -> term -> term *)
- and do_term new_Ts old_Ts polar t =
- case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
- do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | @{const Pure.conjunction} $ t1 $ t2 =>
- @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const Trueprop} $ t1 =>
- @{const Trueprop} $ do_term new_Ts old_Ts polar t1
- | @{const Not} $ t1 =>
- @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
- do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | Const (s as @{const_name The}, T) => do_description_operator s T
- | Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
- let val T' = box_type ext_ctxt InSel T2 in
- Const (@{const_name quot_normal}, T' --> T')
- end
- | Const (s as @{const_name Tha}, T) => do_description_operator s T
- | Const (x as (s, T)) =>
- Const (s, if s = @{const_name converse} orelse
- s = @{const_name trancl} then
- box_relational_operator_type T
- else if is_built_in_const fast_descrs x orelse
- s = @{const_name Sigma} then
- T
- else if is_constr_like thy x then
- box_type ext_ctxt InConstr T
- else if is_sel s
- orelse is_rep_fun thy x then
- box_type ext_ctxt InSel T
- else
- box_type ext_ctxt InExpr T)
- | t1 $ Abs (s, T, t2') =>
- let
- val t1 = do_term new_Ts old_Ts Neut t1
- val T1 = fastype_of1 (new_Ts, t1)
- val (s1, Ts1) = dest_Type T1
- val T' = hd (snd (dest_Type (hd Ts1)))
- val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
- val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
- in
- betapply (if s1 = "fun" then
- t1
- else
- select_nth_constr_arg thy
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
- end
- | t1 $ t2 =>
- let
- val t1 = do_term new_Ts old_Ts Neut t1
- val T1 = fastype_of1 (new_Ts, t1)
- val (s1, Ts1) = dest_Type T1
- val t2 = do_term new_Ts old_Ts Neut t2
- val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
- in
- betapply (if s1 = "fun" then
- t1
- else
- select_nth_constr_arg thy
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
- end
- | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
- | Var (z as (x, T)) =>
- Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
- else box_type ext_ctxt InExpr T)
- | Bound _ => t
- | Abs (s, T, t') =>
- Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
- in do_term [] [] Pos orig_t end
-
-(* int -> term -> term *)
-fun eval_axiom_for_term j t =
- Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
-
-(* extended_context -> styp -> bool *)
-fun is_equational_fun_surely_complete ext_ctxt x =
- case raw_equational_fun_axioms ext_ctxt x of
- [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
- strip_comb t1 |> snd |> forall is_Var
- | _ => false
-
-type special = int list * term list * styp
-
-(* styp -> special -> special -> term *)
-fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
- let
- val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
- val Ts = binder_types T
- val max_j = fold (fold Integer.max) [js1, js2] ~1
- val (eqs, (args1, args2)) =
- fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
- (js1 ~~ ts1, js2 ~~ ts2) of
- (SOME t1, SOME t2) => apfst (cons (t1, t2))
- | (SOME t1, NONE) => apsnd (apsnd (cons t1))
- | (NONE, SOME t2) => apsnd (apfst (cons t2))
- | (NONE, NONE) =>
- let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
- nth Ts j) in
- apsnd (pairself (cons v))
- end) (max_j downto 0) ([], ([], []))
- in
- Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
- |> map Logic.mk_equals,
- Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
- list_comb (Const x2, bounds2 @ args2)))
- |> Refute.close_form (* TODO: needed? *)
- end
-
-(* extended_context -> styp list -> term list *)
-fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
- let
- val groups =
- !special_funs
- |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
- |> AList.group (op =)
- |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
- |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
- (* special -> int *)
- fun generality (js, _, _) = ~(length js)
- (* special -> special -> bool *)
- fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
- x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
- (j2 ~~ t2, j1 ~~ t1)
- (* styp -> special list -> special list -> special list -> term list
- -> term list *)
- fun do_pass_1 _ [] [_] [_] = I
- | do_pass_1 x skipped _ [] = do_pass_2 x skipped
- | do_pass_1 x skipped all (z :: zs) =
- case filter (is_more_specific z) all
- |> sort (int_ord o pairself generality) of
- [] => do_pass_1 x (z :: skipped) all zs
- | (z' :: _) => cons (special_congruence_axiom x z z')
- #> do_pass_1 x skipped all zs
- (* styp -> special list -> term list -> term list *)
- and do_pass_2 _ [] = I
- | do_pass_2 x (z :: zs) =
- fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
- in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
-
-(* term -> bool *)
-val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
-
-(* 'a Symtab.table -> 'a list *)
-fun all_table_entries table = Symtab.fold (append o snd) table []
-(* const_table -> string -> const_table *)
-fun extra_table table s = Symtab.make [(s, all_table_entries table)]
-
-(* extended_context -> term -> (term list * term list) * (bool * bool) *)
-fun axioms_for_term
- (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
- def_table, nondef_table, user_nondefs, ...}) t =
- let
- type accumulator = styp list * (term list * term list)
- (* (term list * term list -> term list)
- -> ((term list -> term list) -> term list * term list
- -> term list * term list)
- -> int -> term -> accumulator -> accumulator *)
- fun add_axiom get app depth t (accum as (xs, axs)) =
- let
- val t = t |> unfold_defs_in_term ext_ctxt
- |> skolemize_term_and_more ext_ctxt ~1
- in
- if is_trivial_equation t then
- accum
- else
- let val t' = t |> specialize_consts_in_term ext_ctxt depth in
- if exists (member (op aconv) (get axs)) [t, t'] then accum
- else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
- end
- end
- (* int -> term -> accumulator -> accumulator *)
- and add_def_axiom depth = add_axiom fst apfst depth
- and add_nondef_axiom depth = add_axiom snd apsnd depth
- and add_maybe_def_axiom depth t =
- (if head_of t <> @{const "==>"} then add_def_axiom
- else add_nondef_axiom) depth t
- and add_eq_axiom depth t =
- (if is_constr_pattern_formula thy t then add_def_axiom
- else add_nondef_axiom) depth t
- (* int -> term -> accumulator -> accumulator *)
- and add_axioms_for_term depth t (accum as (xs, axs)) =
- case t of
- t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
- | Const (x as (s, T)) =>
- (if member (op =) xs x orelse is_built_in_const fast_descrs x then
- accum
- else
- let val accum as (xs, _) = (x :: xs, axs) in
- if depth > axioms_max_depth then
- raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
- \add_axioms_for_term",
- "too many nested axioms (" ^
- string_of_int depth ^ ")")
- else if Refute.is_const_of_class thy x then
- let
- val class = Logic.class_of_const s
- val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
- class)
- val ax1 = try (Refute.specialize_type thy x) of_class
- val ax2 = Option.map (Refute.specialize_type thy x o snd)
- (Refute.get_classdef thy class)
- in
- fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
- accum
- end
- else if is_constr thy x then
- accum
- else if is_equational_fun ext_ctxt x then
- fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
- accum
- else if is_abs_fun thy x then
- if is_quot_type thy (range_type T) then
- raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
- (extra_table def_table s) x)
- else if is_rep_fun thy x then
- if is_quot_type thy (domain_type T) then
- raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
- (extra_table def_table s) x)
- |> add_axioms_for_term depth
- (Const (mate_of_rep_fun thy x))
- |> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun thy x)
- else
- accum |> user_axioms <> SOME false
- ? fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- end)
- |> add_axioms_for_type depth T
- | Free (_, T) => add_axioms_for_type depth T accum
- | Var (_, T) => add_axioms_for_type depth T accum
- | Bound _ => accum
- | Abs (_, T, t) => accum |> add_axioms_for_term depth t
- |> add_axioms_for_type depth T
- (* int -> typ -> accumulator -> accumulator *)
- and add_axioms_for_type depth T =
- case T of
- Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
- | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
- | @{typ prop} => I
- | @{typ bool} => I
- | @{typ unit} => I
- | TFree (_, S) => add_axioms_for_sort depth T S
- | TVar (_, S) => add_axioms_for_sort depth T S
- | Type (z as (s, Ts)) =>
- fold (add_axioms_for_type depth) Ts
- #> (if is_pure_typedef thy T then
- fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
- else if is_quot_type thy T then
- fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
- else if max_bisim_depth >= 0 andalso is_codatatype thy T then
- fold (add_maybe_def_axiom depth)
- (codatatype_bisim_axioms ext_ctxt T)
- else
- I)
- (* int -> typ -> sort -> accumulator -> accumulator *)
- and add_axioms_for_sort depth T S =
- let
- val supers = Sign.complete_sort thy S
- val class_axioms =
- maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
- handle ERROR _ => [])) supers
- val monomorphic_class_axioms =
- map (fn t => case Term.add_tvars t [] of
- [] => t
- | [(x, S)] =>
- Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
- | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
- \add_axioms_for_sort", [t]))
- class_axioms
- in fold (add_nondef_axiom depth) monomorphic_class_axioms end
- val (mono_user_nondefs, poly_user_nondefs) =
- List.partition (null o Term.hidden_polymorphism) user_nondefs
- val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
- evals
- val (xs, (defs, nondefs)) =
- ([], ([], [])) |> add_axioms_for_term 1 t
- |> fold_rev (add_def_axiom 1) eval_axioms
- |> user_axioms = SOME true
- ? fold (add_nondef_axiom 1) mono_user_nondefs
- val defs = defs @ special_congruence_axioms ext_ctxt xs
- in
- ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
- null poly_user_nondefs))
- end
+(* hol_context -> typ -> typ list *)
+fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
+(* hol_context -> term list -> typ list *)
+fun ground_types_in_terms hol_ctxt ts =
+ fold (fold_types (add_ground_types hol_ctxt)) ts []
(* theory -> const_table -> styp -> int list *)
fun const_format thy def_table (x as (s, T)) =
@@ -3356,10 +2121,10 @@
|> map (rev o filter_out (member (op =) js))
|> filter_out null |> map length |> rev
-(* extended_context -> string * string -> (term option * int list) list
+(* hol_context -> string * string -> (term option * int list) list
-> styp -> term * typ *)
fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
- : extended_context) (base_name, step_name) formats =
+ : hol_context) (base_name, step_name) formats =
let
val default_format = the (AList.lookup (op =) formats NONE)
(* styp -> term * typ *)
@@ -3460,7 +2225,7 @@
(t, format_term_type thy def_table formats t)
end)
|>> map_types unbit_and_unbox_type
- |>> shorten_names_in_term |>> shorten_abs_vars
+ |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
(* styp -> string *)
@@ -3474,84 +2239,4 @@
else
"="
-val binary_int_threshold = 4
-
-(* term -> bool *)
-fun may_use_binary_ints (t1 $ t2) =
- may_use_binary_ints t1 andalso may_use_binary_ints t2
- | may_use_binary_ints (t as Const (s, _)) =
- t <> @{const Suc} andalso
- not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
- @{const_name nat_gcd}, @{const_name nat_lcm},
- @{const_name Frac}, @{const_name norm_frac}] s)
- | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
- | may_use_binary_ints _ = true
-fun should_use_binary_ints (t1 $ t2) =
- should_use_binary_ints t1 orelse should_use_binary_ints t2
- | should_use_binary_ints (Const (s, _)) =
- member (op =) [@{const_name times_nat_inst.times_nat},
- @{const_name div_nat_inst.div_nat},
- @{const_name times_int_inst.times_int},
- @{const_name div_int_inst.div_int}] s orelse
- (String.isPrefix numeral_prefix s andalso
- let val n = the (Int.fromString (unprefix numeral_prefix s)) in
- n <= ~ binary_int_threshold orelse n >= binary_int_threshold
- end)
- | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
- | should_use_binary_ints _ = false
-
-(* typ -> typ *)
-fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
- | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
- | binarize_nat_and_int_in_type (Type (s, Ts)) =
- Type (s, map binarize_nat_and_int_in_type Ts)
- | binarize_nat_and_int_in_type T = T
-(* term -> term *)
-val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
-
-(* extended_context -> term
- -> ((term list * term list) * (bool * bool)) * term *)
-fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
- skolemize, uncurry, ...}) t =
- let
- val skolem_depth = if skolemize then 4 else ~1
- val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = t |> unfold_defs_in_term ext_ctxt
- |> Refute.close_form
- |> skolemize_term_and_more ext_ctxt skolem_depth
- |> specialize_consts_in_term ext_ctxt 0
- |> `(axioms_for_term ext_ctxt)
- val binarize =
- case binary_ints of
- SOME false => false
- | _ =>
- forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
- (binary_ints = SOME true orelse
- exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
- val box = exists (not_equal (SOME false) o snd) boxes
- val table =
- Termtab.empty |> uncurry
- ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
- (* bool -> bool -> term -> term *)
- fun do_rest def core =
- binarize ? binarize_nat_and_int_in_term
- #> uncurry ? uncurry_term table
- #> box ? box_fun_and_pair_in_term ext_ctxt def
- #> destroy_constrs ? (pull_out_universal_constrs thy def
- #> pull_out_existential_constrs thy
- #> destroy_pulled_out_constrs ext_ctxt def)
- #> curry_assms
- #> destroy_universal_equalities
- #> destroy_existential_equalities thy
- #> simplify_constrs_and_sels thy
- #> distribute_quantifiers
- #> push_quantifiers_inward thy
- #> not core ? Refute.close_form
- #> shorten_abs_vars
- in
- (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
- (got_all_mono_user_axioms, no_poly_user_axioms)),
- do_rest false true core_t)
- end
-
end;
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 09 21:32:57 2010 +0100
@@ -7,7 +7,7 @@
signature NITPICK_KODKOD =
sig
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type dtype_spec = Nitpick_Scope.dtype_spec
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
type nut = Nitpick_Nut.nut
@@ -33,7 +33,7 @@
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- extended_context -> int -> int Typtab.table -> kodkod_constrs
+ hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
@@ -316,7 +316,15 @@
if R2 = Formula Neut then
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
- [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
+ [KK.TupleSet [],
+ if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
+ index_seq delta (epsilon - delta)
+ |> map (fn j =>
+ KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
+ KK.TupleAtomSeq (j, j0)))
+ |> foldl1 KK.TupleUnion
+ else
+ KK.TupleProduct (ts, upper_bound_for_rep R2)]
end)
end
| bound_for_sel_rel _ _ _ u =
@@ -732,12 +740,12 @@
(* nut NameTable.table -> styp -> KK.rel_expr *)
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> styp -> int -> nfa_transition list *)
-fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs)
+fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
rel_table (dtypes : dtype_spec list) constr_x n =
let
- val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n
+ val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
val (r, R, arity) = const_triple rel_table x
val type_schema = type_schema_of_rep T R
in
@@ -746,17 +754,17 @@
else SOME (kk_project r (map KK.Num [0, j]), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> styp -> nfa_transition list *)
-fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) =
- maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)
+fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
+ maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
| nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
- SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
+ | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
+ SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
o #const) constrs)
val empty_rel = KK.Product (KK.None, KK.None)
@@ -812,23 +820,23 @@
fun acyclicity_axiom_for_datatype dtypes kk nfa start =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> KK.formula list *)
-fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
- map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
+fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
+ map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
|> strongly_connected_sub_nfas
|> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
nfa)
-(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
- -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
-fun sel_axiom_for_sel ext_ctxt j0
+(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
+ -> constr_spec -> int -> KK.formula *)
+fun sel_axiom_for_sel hol_ctxt j0
(kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
kk_join, ...}) rel_table dom_r
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
n =
let
- val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n
+ val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
val (r, R, arity) = const_triple rel_table x
val R2 = dest_Func R |> snd
val z = (epsilon - delta, delta + j0)
@@ -842,9 +850,9 @@
(kk_n_ary_function kk R2 r') (kk_no r'))
end
end
-(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> constr_spec -> KK.formula list *)
-fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
+fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
val honors_explicit_max =
@@ -866,19 +874,19 @@
" too small for \"max\"")
in
max_axiom ::
- map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
+ map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> KK.formula list *)
-fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
+fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
- maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
+ maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
-> KK.formula list *)
-fun uniqueness_axiom_for_constr ext_ctxt
+fun uniqueness_axiom_for_constr hol_ctxt
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
: kodkod_constrs) rel_table ({const, ...} : constr_spec) =
let
@@ -887,7 +895,7 @@
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
val num_sels = num_sels_for_constr_type (snd const)
val triples = map (const_triple rel_table
- o boxed_nth_sel_for_constr ext_ctxt const)
+ o boxed_nth_sel_for_constr hol_ctxt const)
(~1 upto num_sels - 1)
val j0 = case triples |> hd |> #2 of
Func (Atom (_, j0), _) => j0
@@ -903,11 +911,11 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
-> KK.formula list *)
-fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
+fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
({constrs, ...} : dtype_spec) =
- map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
+ map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
(* constr_spec -> int *)
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
@@ -924,31 +932,31 @@
kk_disjoint_sets kk rs]
end
-(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec -> KK.formula list *)
fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
+ | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
(dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
+ sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> KK.formula list *)
-fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
- acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
- maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
+fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
+ acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
+ maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut bits ofs liberal
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
- kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
- kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
- kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,
- kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,
- ...}) u =
+ kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
+ kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
+ kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
+ kk_comprehension, kk_project, kk_project_seq, kk_not3,
+ kk_nat_less, kk_int_less, ...}) u =
let
val main_j0 = offset_of_type ofs bool_T
val bool_j0 = main_j0
@@ -1108,7 +1116,7 @@
else
if is_lone_rep min_R then
if arity_of_rep min_R = 1 then
- kk_subset (kk_product r1 r2) KK.Iden
+ kk_lone (kk_union r1 r2)
else if not both_opt then
(r1, r2) |> is_opt_rep (rep_of u2) ? swap
|-> kk_subset
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 09 21:32:57 2010 +0100
@@ -56,26 +56,36 @@
val opt_flag = nitpick_prefix ^ "opt"
val non_opt_flag = nitpick_prefix ^ "non_opt"
-(* string -> int -> string *)
-fun atom_suffix s j =
- nat_subscript (j + 1)
+type atom_pool = ((string * int) * int list) list
+
+(* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
+fun nth_atom_suffix pool s j k =
+ (case AList.lookup (op =) (!pool) (s, k) of
+ SOME js =>
+ (case find_index (curry (op =) j) js of
+ ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
+ length js + 1)
+ | n => length js - n)
+ | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
+ |> nat_subscript
|> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
? prefix "\<^isub>,"
-(* string -> typ -> int -> string *)
-fun atom_name prefix (T as Type (s, _)) j =
+(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
+fun nth_atom_name pool prefix (T as Type (s, _)) j k =
let val s' = shortest_name s in
prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
- atom_suffix s j
+ nth_atom_suffix pool s j k
end
- | atom_name prefix (T as TFree (s, _)) j =
- prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
- | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
-(* bool -> typ -> int -> term *)
-fun atom for_auto T j =
+ | nth_atom_name pool prefix (T as TFree (s, _)) j k =
+ prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
+ | nth_atom_name _ _ T _ _ =
+ raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
+(* atom_pool Unsynchronized.ref -> bool -> typ -> int -> int -> term *)
+fun nth_atom pool for_auto T j k =
if for_auto then
- Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T)
+ Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
else
- Const (atom_name "" T j, T)
+ Const (nth_atom_name pool "" T j k, T)
(* term -> real *)
fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
@@ -251,9 +261,10 @@
-> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
-> int list list -> term *)
fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
- ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
+ ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
: scope) sel_names rel_table bounds =
let
+ val pool = Unsynchronized.ref []
val for_auto = (maybe_name = "")
(* int list list -> int *)
fun value_of_bits jss =
@@ -348,7 +359,7 @@
(unbit_and_unbox_type T1)
(unbit_and_unbox_type T2)
(* (typ * int) list -> typ -> typ -> int -> term *)
- fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
+ fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
let
val k1 = card_of_type card_assigns T1
val k2 = card_of_type card_assigns T2
@@ -360,37 +371,39 @@
signed_string_of_int j ^ " for " ^
string_for_rep (Vect (k1, Atom (k2, 0))))
end
- | term_for_atom seen (Type ("*", [T1, T2])) _ j =
- let val k1 = card_of_type card_assigns T1 in
+ | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
+ let
+ val k1 = card_of_type card_assigns T1
+ val k2 = k div k1
+ in
list_comb (HOLogic.pair_const T1 T2,
- map2 (fn T => term_for_atom seen T T) [T1, T2]
- [j div k1, j mod k1])
+ map3 (fn T => term_for_atom seen T T) [T1, T2]
+ [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
end
- | term_for_atom seen @{typ prop} _ j =
- HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j)
- | term_for_atom _ @{typ bool} _ j =
+ | term_for_atom seen @{typ prop} _ j k =
+ HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
+ | term_for_atom _ @{typ bool} _ j _ =
if j = 0 then @{const False} else @{const True}
- | term_for_atom _ @{typ unit} _ _ = @{const Unity}
- | term_for_atom seen T _ j =
+ | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
+ | term_for_atom seen T _ j k =
if T = nat_T then
HOLogic.mk_number nat_T j
else if T = int_T then
- HOLogic.mk_number int_T
- (int_for_atom (card_of_type card_assigns int_T, 0) j)
+ HOLogic.mk_number int_T (int_for_atom (k, 0) j)
else if is_fp_iterator_type T then
- HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
+ HOLogic.mk_number nat_T (k - j - 1)
else if T = @{typ bisim_iterator} then
HOLogic.mk_number nat_T j
else case datatype_spec datatypes T of
- NONE => atom for_auto T j
- | SOME {deep = false, ...} => atom for_auto T j
+ NONE => nth_atom pool for_auto T j k
+ | SOME {deep = false, ...} => nth_atom pool for_auto T j k
| SOME {co, constrs, ...} =>
let
(* styp -> int list *)
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
(* unit -> indexname * typ *)
- fun var () = ((atom_name "" T j, 0), T)
+ fun var () = ((nth_atom_name pool "" T j k, 0), T)
val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
constrs
val real_j = j + offset_of_type ofs T
@@ -400,7 +413,7 @@
else NONE)
(discr_jsss ~~ constrs) |> the
val arg_Ts = curried_binder_types constr_T
- val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
+ val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
(index_seq 0 (length arg_Ts))
val sel_Rs =
map (fn x => get_first
@@ -479,13 +492,14 @@
(* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
-> term *)
and term_for_vect seen k R T1 T2 T' js =
- make_fun true T1 T2 T' (map (term_for_atom seen T1 T1) (index_seq 0 k))
+ make_fun true T1 T2 T'
+ (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
(map (term_for_rep seen T2 T2 R o single)
(batch_list (arity_of_rep R) js))
(* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
- and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
+ and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
| term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
- if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
+ if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
| term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
let
@@ -586,7 +600,7 @@
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
-> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
- ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
+ ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
user_axioms, debug, binary_ints, destroy_constrs,
specialize, skolemize, star_linear_preds, uncurry,
fast_descrs, tac_timeout, evals, case_names, def_table,
@@ -598,7 +612,7 @@
let
val (wacky_names as (_, base_name, step_name, _), ctxt) =
add_wacky_syntax ctxt
- val ext_ctxt =
+ val hol_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
@@ -612,7 +626,7 @@
ersatz_table = ersatz_table, skolems = skolems,
special_funs = special_funs, unrolled_preds = unrolled_preds,
wf_cache = wf_cache, constr_cache = constr_cache}
- val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
+ val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
ofs = ofs}
(* typ -> typ -> rep -> int list list -> term *)
@@ -644,7 +658,7 @@
end
| ConstName (s, T, _) =>
(assign_operator_for_const (s, T),
- user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
+ user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
T)
| _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
\pretty_for_assign", [name])
@@ -724,15 +738,16 @@
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
-> KK.raw_bound list -> term -> bool option *)
-fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
+fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
+ val pool = Unsynchronized.ref []
(* typ * int -> term *)
fun free_type_assm (T, k) =
let
(* int -> term *)
- val atom = atom true T
+ fun atom j = nth_atom pool true T j k
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
val eqs = map equation_for_atom (index_seq 0 k)
val compreh_assm =
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Feb 09 21:32:57 2010 +0100
@@ -8,10 +8,10 @@
signature NITPICK_MONO =
sig
datatype sign = Plus | Minus
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
val formulas_monotonic :
- extended_context -> typ -> sign -> term list -> term list -> term -> bool
+ hol_context -> typ -> sign -> term list -> term list -> term -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -35,7 +35,7 @@
CRec of string * typ list
type cdata =
- {ext_ctxt: extended_context,
+ {hol_ctxt: hol_context,
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
@@ -114,9 +114,9 @@
| flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
| flatten_ctype C = [C]
-(* extended_context -> typ -> cdata *)
-fun initial_cdata ext_ctxt alpha_T =
- ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
+(* hol_context -> typ -> cdata *)
+fun initial_cdata hol_ctxt alpha_T =
+ ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
datatype_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []} : cdata)
@@ -188,7 +188,7 @@
in List.app repair_one (!constr_cache) end
(* cdata -> typ -> ctype *)
-fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
+fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
datatype_cache, constr_cache, ...} : cdata) =
let
(* typ -> typ -> ctype *)
@@ -217,7 +217,7 @@
| NONE =>
let
val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
- val xs = datatype_constrs ext_ctxt T
+ val xs = datatype_constrs hol_ctxt T
val (all_Cs, constr_Cs) =
fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
let
@@ -264,7 +264,7 @@
end
(* cdata -> styp -> ctype *)
-fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
+fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
...}) (x as (_, T)) =
if could_exist_alpha_sub_ctype thy alpha_T T then
case AList.lookup (op =) (!constr_cache) x of
@@ -278,8 +278,8 @@
AList.lookup (op =) (!constr_cache) x |> the)
else
fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
- x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
+fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
+ x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
|> sel_ctype_from_constr_ctype s
(* literal list -> ctype -> ctype *)
@@ -549,7 +549,7 @@
handle List.Empty => initial_gamma
(* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
+fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
max_fresh, ...}) =
let
(* typ -> ctype *)
@@ -806,7 +806,7 @@
in do_term end
(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
+fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
@@ -895,7 +895,7 @@
not (is_harmless_axiom t) ? consider_general_formula cdata sn t
(* cdata -> term -> accumulator -> accumulator *)
-fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
+fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
consider_nondefinitional_axiom cdata Plus t
else if is_harmless_axiom t then
@@ -945,13 +945,13 @@
map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
|> cat_lines |> print_g
-(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
+(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
core_t =
let
val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
- val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
+ val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
val (gamma, cset) =
(initial_gamma, slack)
|> fold (consider_definitional_axiom cdata) def_ts
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 09 21:32:57 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_NUT =
sig
type special_fun = Nitpick_HOL.special_fun
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
type rep = Nitpick_Rep.rep
@@ -106,7 +106,7 @@
val name_ord : (nut * nut) -> order
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
- val nut_from_term : extended_context -> op2 -> term -> nut
+ val nut_from_term : hol_context -> op2 -> term -> nut
val choose_reps_for_free_vars :
scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
val choose_reps_for_consts :
@@ -466,8 +466,8 @@
fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-(* extended_context -> op2 -> term -> nut *)
-fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
+(* hol_context -> op2 -> term -> nut *)
+fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -597,7 +597,7 @@
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
- (if is_finite_type ext_ctxt (domain_type T) then
+ (if is_finite_type hol_ctxt (domain_type T) then
Cst (True, bool_T, Any)
else case t1 of
Const (@{const_name top}, _) => Cst (False, bool_T, Any)
@@ -712,7 +712,7 @@
in (v :: vs, NameTable.update (v, R) table) end
(* scope -> bool -> nut -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
+fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
ofs, ...}) all_exact v (vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
@@ -747,10 +747,10 @@
(* scope -> styp -> int -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
+fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
(vs, table) =
let
- val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
+ val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
val R' = if n = ~1 orelse is_word_type (body_type T) orelse
(is_fun_type (range_type T') andalso
is_boolean_type (body_type T')) then
@@ -890,7 +890,7 @@
| untuple f u = if rep_of u = Unit then [] else [f u]
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
-fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
+fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, datatypes, ofs, ...})
liberal table def =
let
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 09 21:32:57 2010 +0100
@@ -0,0 +1,1431 @@
+(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2008, 2009, 2010
+
+Nitpick's HOL preprocessor.
+*)
+
+signature NITPICK_PREPROC =
+sig
+ type hol_context = Nitpick_HOL.hol_context
+ val preprocess_term :
+ hol_context -> term -> ((term list * term list) * (bool * bool)) * term
+end
+
+structure Nitpick_Preproc : NITPICK_PREPROC =
+struct
+
+open Nitpick_Util
+open Nitpick_HOL
+
+(* polarity -> string -> bool *)
+fun is_positive_existential polar quant_s =
+ (polar = Pos andalso quant_s = @{const_name Ex}) orelse
+ (polar = Neg andalso quant_s <> @{const_name Ex})
+
+(** Binary coding of integers **)
+
+(* If a formula contains a numeral whose absolute value is more than this
+ threshold, the unary coding is likely not to work well and we prefer the
+ binary coding. *)
+val binary_int_threshold = 3
+
+(* term -> bool *)
+fun may_use_binary_ints (t1 $ t2) =
+ may_use_binary_ints t1 andalso may_use_binary_ints t2
+ | may_use_binary_ints (t as Const (s, _)) =
+ t <> @{const Suc} andalso
+ not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
+ @{const_name nat_gcd}, @{const_name nat_lcm},
+ @{const_name Frac}, @{const_name norm_frac}] s)
+ | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
+ | may_use_binary_ints _ = true
+fun should_use_binary_ints (t1 $ t2) =
+ should_use_binary_ints t1 orelse should_use_binary_ints t2
+ | should_use_binary_ints (Const (s, _)) =
+ member (op =) [@{const_name times_nat_inst.times_nat},
+ @{const_name div_nat_inst.div_nat},
+ @{const_name times_int_inst.times_int},
+ @{const_name div_int_inst.div_int}] s orelse
+ (String.isPrefix numeral_prefix s andalso
+ let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+ n < ~ binary_int_threshold orelse n > binary_int_threshold
+ end)
+ | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
+ | should_use_binary_ints _ = false
+
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+ | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+ | binarize_nat_and_int_in_type (Type (s, Ts)) =
+ Type (s, map binarize_nat_and_int_in_type Ts)
+ | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
+(** Uncurrying **)
+
+(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
+fun add_to_uncurry_table thy t =
+ let
+ (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
+ fun aux (t1 $ t2) args table =
+ let val table = aux t2 [] table in aux t1 (t2 :: args) table end
+ | aux (Abs (_, _, t')) _ table = aux t' [] table
+ | aux (t as Const (x as (s, _))) args table =
+ if is_built_in_const true x orelse is_constr_like thy x orelse
+ is_sel s orelse s = @{const_name Sigma} then
+ table
+ else
+ Termtab.map_default (t, 65536) (curry Int.min (length args)) table
+ | aux _ _ table = table
+ in aux t [] end
+
+(* int -> int -> string *)
+fun uncurry_prefix_for k j =
+ uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* int Termtab.tab term -> term *)
+fun uncurry_term table t =
+ let
+ (* term -> term list -> term *)
+ fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
+ | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
+ | aux (t as Const (s, T)) args =
+ (case Termtab.lookup table t of
+ SOME n =>
+ if n >= 2 then
+ let
+ val (arg_Ts, rest_T) = strip_n_binders n T
+ val j =
+ if hd arg_Ts = @{typ bisim_iterator} orelse
+ is_fp_iterator_type (hd arg_Ts) then
+ 1
+ else case find_index (not_equal bool_T) arg_Ts of
+ ~1 => n
+ | j => j
+ val ((before_args, tuple_args), after_args) =
+ args |> chop n |>> chop j
+ val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
+ T |> strip_n_binders n |>> chop j
+ val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
+ in
+ if n - j < 2 then
+ betapplys (t, args)
+ else
+ betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
+ before_arg_Ts ---> tuple_T --> rest_T),
+ before_args @ [mk_flat_tuple tuple_T tuple_args] @
+ after_args)
+ end
+ else
+ betapplys (t, args)
+ | NONE => betapplys (t, args))
+ | aux t args = betapplys (t, args)
+ in aux t [] end
+
+(** Boxing **)
+
+(* hol_context -> typ -> term -> term *)
+fun constr_expand (hol_ctxt as {thy, ...}) T t =
+ (case head_of t of
+ Const x => if is_constr_like thy x then t else raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let
+ val x' as (_, T') =
+ if is_pair_type T then
+ let val (T1, T2) = HOLogic.dest_prodT T in
+ (@{const_name Pair}, T1 --> T2 --> T)
+ end
+ else
+ datatype_constrs hol_ctxt T |> hd
+ val arg_Ts = binder_types T'
+ in
+ list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
+ (index_seq 0 (length arg_Ts)) arg_Ts)
+ end
+
+(* hol_context -> bool -> term -> term *)
+fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
+ let
+ (* typ -> typ *)
+ fun box_relational_operator_type (Type ("fun", Ts)) =
+ Type ("fun", map box_relational_operator_type Ts)
+ | box_relational_operator_type (Type ("*", Ts)) =
+ Type ("*", map (box_type hol_ctxt InPair) Ts)
+ | box_relational_operator_type T = T
+ (* (term -> term) -> int -> term -> term *)
+ fun coerce_bound_no f j t =
+ case t of
+ t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+ | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+ | Bound j' => if j' = j then f t else t
+ | _ => t
+ (* typ -> typ -> term -> term *)
+ fun coerce_bound_0_in_term new_T old_T =
+ old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
+ (* typ list -> typ -> term -> term *)
+ and coerce_term Ts new_T old_T t =
+ if old_T = new_T then
+ t
+ else
+ case (new_T, old_T) of
+ (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type ("fun", [old_T1, old_T2])) =>
+ (case eta_expand Ts t 1 of
+ Abs (s, _, t') =>
+ Abs (s, new_T1,
+ t' |> coerce_bound_0_in_term new_T1 old_T1
+ |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
+ |> Envir.eta_contract
+ |> new_s <> "fun"
+ ? construct_value thy (@{const_name FunBox},
+ Type ("fun", new_Ts) --> new_T) o single
+ | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \coerce_term", [t']))
+ | (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type (old_s, old_Ts as [old_T1, old_T2])) =>
+ if old_s = @{type_name fun_box} orelse
+ old_s = @{type_name pair_box} orelse old_s = "*" then
+ case constr_expand hol_ctxt old_T t of
+ Const (@{const_name FunBox}, _) $ t1 =>
+ if new_s = "fun" then
+ coerce_term Ts new_T (Type ("fun", old_Ts)) t1
+ else
+ construct_value thy
+ (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+ [coerce_term Ts (Type ("fun", new_Ts))
+ (Type ("fun", old_Ts)) t1]
+ | Const _ $ t1 $ t2 =>
+ construct_value thy
+ (if new_s = "*" then @{const_name Pair}
+ else @{const_name PairBox}, new_Ts ---> new_T)
+ [coerce_term Ts new_T1 old_T1 t1,
+ coerce_term Ts new_T2 old_T2 t2]
+ | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \coerce_term", [t'])
+ else
+ raise TYPE ("coerce_term", [new_T, old_T], [t])
+ | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
+ (* indexname * typ -> typ * term -> typ option list -> typ option list *)
+ fun add_boxed_types_for_var (z as (_, T)) (T', t') =
+ case t' of
+ Var z' => z' = z ? insert (op =) T'
+ | Const (@{const_name Pair}, _) $ t1 $ t2 =>
+ (case T' of
+ Type (_, [T1, T2]) =>
+ fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
+ | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \add_boxed_types_for_var", [T'], []))
+ | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
+ (* typ list -> typ list -> term -> indexname * typ -> typ *)
+ fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
+ case t of
+ @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
+ | Const (s0, _) $ t1 $ _ =>
+ if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+ let
+ val (t', args) = strip_comb t1
+ val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
+ in
+ case fold (add_boxed_types_for_var z)
+ (fst (strip_n_binders (length args) T') ~~ args) [] of
+ [T''] => T''
+ | _ => T
+ end
+ else
+ T
+ | _ => T
+ (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
+ -> term -> term *)
+ and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
+ let
+ val abs_T' =
+ if polar = Neut orelse is_positive_existential polar quant_s then
+ box_type hol_ctxt InFunLHS abs_T
+ else
+ abs_T
+ val body_T = body_type quant_T
+ in
+ Const (quant_s, (abs_T' --> body_T) --> body_T)
+ $ Abs (abs_s, abs_T',
+ t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
+ end
+ (* typ list -> typ list -> string -> typ -> term -> term -> term *)
+ and do_equals new_Ts old_Ts s0 T0 t1 t2 =
+ let
+ val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
+ val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
+ val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
+ in
+ list_comb (Const (s0, T --> T --> body_type T0),
+ map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
+ end
+ (* string -> typ -> term *)
+ and do_description_operator s T =
+ let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
+ Const (s, (T1 --> bool_T) --> T1)
+ end
+ (* typ list -> typ list -> polarity -> term -> term *)
+ and do_term new_Ts old_Ts polar t =
+ case t of
+ Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
+ do_equals new_Ts old_Ts s0 T0 t1 t2
+ | @{const "==>"} $ t1 $ t2 =>
+ @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const Pure.conjunction} $ t1 $ t2 =>
+ @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const Trueprop} $ t1 =>
+ @{const Trueprop} $ do_term new_Ts old_Ts polar t1
+ | @{const Not} $ t1 =>
+ @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+ do_equals new_Ts old_Ts s0 T0 t1 t2
+ | @{const "op &"} $ t1 $ t2 =>
+ @{const "op &"} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const "op |"} $ t1 $ t2 =>
+ @{const "op |"} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const "op -->"} $ t1 $ t2 =>
+ @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ $ do_term new_Ts old_Ts polar t2
+ | Const (s as @{const_name The}, T) => do_description_operator s T
+ | Const (s as @{const_name Eps}, T) => do_description_operator s T
+ | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
+ let val T' = box_type hol_ctxt InSel T2 in
+ Const (@{const_name quot_normal}, T' --> T')
+ end
+ | Const (s as @{const_name Tha}, T) => do_description_operator s T
+ | Const (x as (s, T)) =>
+ Const (s, if s = @{const_name converse} orelse
+ s = @{const_name trancl} then
+ box_relational_operator_type T
+ else if is_built_in_const fast_descrs x orelse
+ s = @{const_name Sigma} then
+ T
+ else if is_constr_like thy x then
+ box_type hol_ctxt InConstr T
+ else if is_sel s
+ orelse is_rep_fun thy x then
+ box_type hol_ctxt InSel T
+ else
+ box_type hol_ctxt InExpr T)
+ | t1 $ Abs (s, T, t2') =>
+ let
+ val t1 = do_term new_Ts old_Ts Neut t1
+ val T1 = fastype_of1 (new_Ts, t1)
+ val (s1, Ts1) = dest_Type T1
+ val T' = hd (snd (dest_Type (hd Ts1)))
+ val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
+ val T2 = fastype_of1 (new_Ts, t2)
+ val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ in
+ betapply (if s1 = "fun" then
+ t1
+ else
+ select_nth_constr_arg thy
+ (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+ (Type ("fun", Ts1)), t2)
+ end
+ | t1 $ t2 =>
+ let
+ val t1 = do_term new_Ts old_Ts Neut t1
+ val T1 = fastype_of1 (new_Ts, t1)
+ val (s1, Ts1) = dest_Type T1
+ val t2 = do_term new_Ts old_Ts Neut t2
+ val T2 = fastype_of1 (new_Ts, t2)
+ val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ in
+ betapply (if s1 = "fun" then
+ t1
+ else
+ select_nth_constr_arg thy
+ (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+ (Type ("fun", Ts1)), t2)
+ end
+ | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
+ | Var (z as (x, T)) =>
+ Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
+ else box_type hol_ctxt InExpr T)
+ | Bound _ => t
+ | Abs (s, T, t') =>
+ Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
+ in do_term [] [] Pos orig_t end
+
+(** Destruction of constructors **)
+
+val val_var_prefix = nitpick_prefix ^ "v"
+
+(* typ list -> int -> int -> int -> term -> term *)
+fun fresh_value_var Ts k n j t =
+ Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
+
+(* typ list -> int -> term -> bool *)
+fun has_heavy_bounds_or_vars Ts level t =
+ let
+ (* typ list -> bool *)
+ fun aux [] = false
+ | aux [T] = is_fun_type T orelse is_pair_type T
+ | aux _ = true
+ in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
+
+(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
+ -> term * term list *)
+fun pull_out_constr_comb thy Ts relax k level t args seen =
+ let val t_comb = list_comb (t, args) in
+ case t of
+ Const x =>
+ if not relax andalso is_constr thy x andalso
+ not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+ has_heavy_bounds_or_vars Ts level t_comb andalso
+ not (loose_bvar (t_comb, level)) then
+ let
+ val (j, seen) = case find_index (curry (op =) t_comb) seen of
+ ~1 => (0, t_comb :: seen)
+ | j => (j, seen)
+ in (fresh_value_var Ts k (length seen) j t_comb, seen) end
+ else
+ (t_comb, seen)
+ | _ => (t_comb, seen)
+ end
+
+(* (term -> term) -> typ list -> int -> term list -> term list *)
+fun equations_for_pulled_out_constrs mk_eq Ts k seen =
+ let val n = length seen in
+ map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
+ (index_seq 0 n) seen
+ end
+
+(* theory -> bool -> term -> term *)
+fun pull_out_universal_constrs thy def t =
+ let
+ val k = maxidx_of_term t + 1
+ (* typ list -> bool -> term -> term list -> term list -> term * term list *)
+ fun do_term Ts def t args seen =
+ case t of
+ (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
+ do_eq_or_imp Ts true def t0 t1 t2 seen
+ | (t0 as @{const "==>"}) $ t1 $ t2 =>
+ if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
+ | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_eq_or_imp Ts true def t0 t1 t2 seen
+ | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+ do_eq_or_imp Ts false def t0 t1 t2 seen
+ | Abs (s, T, t') =>
+ let val (t', seen) = do_term (T :: Ts) def t' [] seen in
+ (list_comb (Abs (s, T, t'), args), seen)
+ end
+ | t1 $ t2 =>
+ let val (t2, seen) = do_term Ts def t2 [] seen in
+ do_term Ts def t1 (t2 :: args) seen
+ end
+ | _ => pull_out_constr_comb thy Ts def k 0 t args seen
+ (* typ list -> bool -> bool -> term -> term -> term -> term list
+ -> term * term list *)
+ and do_eq_or_imp Ts eq def t0 t1 t2 seen =
+ let
+ val (t2, seen) = if eq andalso def then (t2, seen)
+ else do_term Ts false t2 [] seen
+ val (t1, seen) = do_term Ts false t1 [] seen
+ in (t0 $ t1 $ t2, seen) end
+ val (concl, seen) = do_term [] def t [] []
+ in
+ Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
+ seen, concl)
+ end
+
+(* term -> term -> term *)
+fun mk_exists v t =
+ HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
+
+(* theory -> term -> term *)
+fun pull_out_existential_constrs thy t =
+ let
+ val k = maxidx_of_term t + 1
+ (* typ list -> int -> term -> term list -> term list -> term * term list *)
+ fun aux Ts num_exists t args seen =
+ case t of
+ (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
+ let
+ val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
+ val n = length seen'
+ (* unit -> term list *)
+ fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
+ in
+ (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
+ |> List.foldl s_conj t1 |> fold mk_exists (vars ())
+ |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
+ end
+ | t1 $ t2 =>
+ let val (t2, seen) = aux Ts num_exists t2 [] seen in
+ aux Ts num_exists t1 (t2 :: args) seen
+ end
+ | Abs (s, T, t') =>
+ let
+ val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
+ in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
+ | _ =>
+ if num_exists > 0 then
+ pull_out_constr_comb thy Ts false k num_exists t args seen
+ else
+ (list_comb (t, args), seen)
+ in aux [] 0 t [] [] |> fst end
+
+(* hol_context -> bool -> term -> term *)
+fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
+ let
+ (* styp -> int *)
+ val num_occs_of_var =
+ fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
+ | _ => I) t (K 0)
+ (* bool -> term -> term *)
+ fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+ aux_eq careful true t0 t1 t2
+ | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+ t0 $ aux false t1 $ aux careful t2
+ | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+ aux_eq careful true t0 t1 t2
+ | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+ t0 $ aux false t1 $ aux careful t2
+ | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
+ | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
+ | aux _ t = t
+ (* bool -> bool -> term -> term -> term -> term *)
+ and aux_eq careful pass1 t0 t1 t2 =
+ ((if careful then
+ raise SAME ()
+ else if axiom andalso is_Var t2 andalso
+ num_occs_of_var (dest_Var t2) = 1 then
+ @{const True}
+ else case strip_comb t2 of
+ (* The first case is not as general as it could be. *)
+ (Const (@{const_name PairBox}, _),
+ [Const (@{const_name fst}, _) $ Var z1,
+ Const (@{const_name snd}, _) $ Var z2]) =>
+ if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
+ else raise SAME ()
+ | (Const (x as (s, T)), args) =>
+ let val arg_Ts = binder_types T in
+ if length arg_Ts = length args andalso
+ (is_constr thy x orelse s = @{const_name Pair} orelse
+ x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+ (not careful orelse not (is_Var t1) orelse
+ String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
+ discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
+ |> foldr1 s_conj
+ else
+ raise SAME ()
+ end
+ | _ => raise SAME ())
+ |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
+ handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
+ else t0 $ aux false t2 $ aux false t1
+ (* styp -> term -> int -> typ -> term -> term *)
+ and sel_eq x t n nth_T nth_t =
+ HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
+ |> aux false
+ in aux axiom t end
+
+(** Destruction of universal and existential equalities **)
+
+(* term -> term *)
+fun curry_assms (@{const "==>"} $ (@{const Trueprop}
+ $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+ curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
+ | curry_assms (@{const "==>"} $ t1 $ t2) =
+ @{const "==>"} $ curry_assms t1 $ curry_assms t2
+ | curry_assms t = t
+
+(* term -> term *)
+val destroy_universal_equalities =
+ let
+ (* term list -> (indexname * typ) list -> term -> term *)
+ fun aux prems zs t =
+ case t of
+ @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
+ | _ => Logic.list_implies (rev prems, t)
+ (* term list -> (indexname * typ) list -> term -> term -> term *)
+ and aux_implies prems zs t1 t2 =
+ case t1 of
+ Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
+ | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+ aux_eq prems zs z t' t1 t2
+ | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+ aux_eq prems zs z t' t1 t2
+ | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
+ (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
+ -> term -> term *)
+ and aux_eq prems zs z t' t1 t2 =
+ if not (member (op =) zs z) andalso
+ not (exists_subterm (curry (op =) (Var z)) t') then
+ aux prems zs (subst_free [(Var z, t')] t2)
+ else
+ aux (t1 :: prems) (Term.add_vars t1 zs) t2
+ in aux [] [] end
+
+(* theory -> int -> term list -> term list -> (term * term list) option *)
+fun find_bound_assign _ _ _ [] = NONE
+ | find_bound_assign thy j seen (t :: ts) =
+ let
+ (* bool -> term -> term -> (term * term list) option *)
+ fun aux pass1 t1 t2 =
+ (if loose_bvar1 (t2, j) then
+ if pass1 then aux false t2 t1 else raise SAME ()
+ else case t1 of
+ Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
+ | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+ if j' = j andalso
+ s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
+ SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
+ ts @ seen)
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () => find_bound_assign thy j (t :: seen) ts
+ in
+ case t of
+ Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
+ | _ => find_bound_assign thy j (t :: seen) ts
+ end
+
+(* int -> term -> term -> term *)
+fun subst_one_bound j arg t =
+ let
+ fun aux (Bound i, lev) =
+ if i < lev then raise SAME ()
+ else if i = lev then incr_boundvars (lev - j) arg
+ else Bound (i - 1)
+ | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
+ | aux (f $ t, lev) =
+ (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
+ handle SAME () => f $ aux (t, lev))
+ | aux _ = raise SAME ()
+ in aux (t, j) handle SAME () => t end
+
+(* theory -> term -> term *)
+fun destroy_existential_equalities thy =
+ let
+ (* string list -> typ list -> term list -> term *)
+ fun kill [] [] ts = foldr1 s_conj ts
+ | kill (s :: ss) (T :: Ts) ts =
+ (case find_bound_assign thy (length ss) [] ts of
+ SOME (_, []) => @{const True}
+ | SOME (arg_t, ts) =>
+ kill ss Ts (map (subst_one_bound (length ss)
+ (incr_bv (~1, length ss + 1, arg_t))) ts)
+ | NONE =>
+ Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
+ $ Abs (s, T, kill ss Ts ts))
+ | kill _ _ _ = raise UnequalLengths
+ (* string list -> typ list -> term -> term *)
+ fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
+ gather (ss @ [s1]) (Ts @ [T1]) t1
+ | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
+ | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
+ | gather [] [] t = t
+ | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
+ in gather [] [] end
+
+(** Skolemization **)
+
+(* int -> int -> string *)
+fun skolem_prefix_for k j =
+ skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* hol_context -> int -> term -> term *)
+fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
+ skolem_depth =
+ let
+ (* int list -> int list *)
+ val incrs = map (Integer.add 1)
+ (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
+ fun aux ss Ts js depth polar t =
+ let
+ (* string -> typ -> string -> typ -> term -> term *)
+ fun do_quantifier quant_s quant_T abs_s abs_T t =
+ if not (loose_bvar1 (t, 0)) then
+ aux ss Ts js depth polar (incr_boundvars ~1 t)
+ else if depth <= skolem_depth andalso
+ is_positive_existential polar quant_s then
+ let
+ val j = length (!skolems) + 1
+ val sko_s = skolem_prefix_for (length js) j ^ abs_s
+ val _ = Unsynchronized.change skolems (cons (sko_s, ss))
+ val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
+ map Bound (rev js))
+ val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
+ in
+ if null js then betapply (abs_t, sko_t)
+ else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
+ end
+ else
+ Const (quant_s, quant_T)
+ $ Abs (abs_s, abs_T,
+ if is_higher_order_type abs_T then
+ t
+ else
+ aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+ (depth + 1) polar t)
+ in
+ case t of
+ Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | @{const "==>"} $ t1 $ t2 =>
+ @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
+ $ aux ss Ts js depth polar t2
+ | @{const Pure.conjunction} $ t1 $ t2 =>
+ @{const Pure.conjunction} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const Trueprop} $ t1 =>
+ @{const Trueprop} $ aux ss Ts js depth polar t1
+ | @{const Not} $ t1 =>
+ @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
+ | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | @{const "op &"} $ t1 $ t2 =>
+ @{const "op &"} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const "op |"} $ t1 $ t2 =>
+ @{const "op |"} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const "op -->"} $ t1 $ t2 =>
+ @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
+ $ aux ss Ts js depth polar t2
+ | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
+ t0 $ t1 $ aux ss Ts js depth polar t2
+ | Const (x as (s, T)) =>
+ if is_inductive_pred hol_ctxt x andalso
+ not (is_well_founded_inductive_pred hol_ctxt x) then
+ let
+ val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val (pref, connective, set_oper) =
+ if gfp then
+ (lbfp_prefix,
+ @{const "op |"},
+ @{const_name semilattice_sup_fun_inst.sup_fun})
+ else
+ (ubfp_prefix,
+ @{const "op &"},
+ @{const_name semilattice_inf_fun_inst.inf_fun})
+ (* unit -> term *)
+ fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
+ |> aux ss Ts js depth polar
+ fun neg () = Const (pref ^ s, T)
+ in
+ (case polar |> gfp ? flip_polarity of
+ Pos => pos ()
+ | Neg => neg ()
+ | Neut =>
+ if is_fun_type T then
+ let
+ val ((trunk_arg_Ts, rump_arg_T), body_T) =
+ T |> strip_type |>> split_last
+ val set_T = rump_arg_T --> body_T
+ (* (unit -> term) -> term *)
+ fun app f =
+ list_comb (f (),
+ map Bound (length trunk_arg_Ts - 1 downto 0))
+ in
+ List.foldr absdummy
+ (Const (set_oper, set_T --> set_T --> set_T)
+ $ app pos $ app neg) trunk_arg_Ts
+ end
+ else
+ connective $ pos () $ neg ())
+ end
+ else
+ Const x
+ | t1 $ t2 =>
+ betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
+ aux ss Ts [] depth Neut t2)
+ | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
+ | _ => t
+ end
+ in aux [] [] [] 0 Pos end
+
+(** Function specialization **)
+
+(* term -> term list *)
+fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
+ | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
+ | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+ snd (strip_comb t1)
+ | params_in_equation _ = []
+
+(* styp -> styp -> int list -> term list -> term list -> term -> term *)
+fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
+ let
+ val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
+ + 1
+ val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
+ val fixed_params = filter_indices fixed_js (params_in_equation t)
+ (* term list -> term -> term *)
+ fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
+ | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
+ | aux args t =
+ if t = Const x then
+ list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
+ else
+ let val j = find_index (curry (op =) t) fixed_params in
+ list_comb (if j >= 0 then nth fixed_args j else t, args)
+ end
+ in aux [] t end
+
+(* hol_context -> styp -> (int * term option) list *)
+fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
+ let
+ (* term -> term list -> term list -> term list list *)
+ fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
+ | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
+ | fun_calls t args =
+ (case t of
+ Const (x' as (s', T')) =>
+ x = x' orelse (case AList.lookup (op =) ersatz_table s' of
+ SOME s'' => x = (s'', T')
+ | NONE => false)
+ | _ => false) ? cons args
+ (* term list list -> term list list -> term list -> term list list *)
+ fun call_sets [] [] vs = [vs]
+ | call_sets [] uss vs = vs :: call_sets uss [] []
+ | call_sets ([] :: _) _ _ = []
+ | call_sets ((t :: ts) :: tss) uss vs =
+ OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
+ val sets = call_sets (fun_calls t [] []) [] []
+ val indexed_sets = sets ~~ (index_seq 0 (length sets))
+ in
+ fold_rev (fn (set, j) =>
+ case set of
+ [Var _] => AList.lookup (op =) indexed_sets set = SOME j
+ ? cons (j, NONE)
+ | [t as Const _] => cons (j, SOME t)
+ | [t as Free _] => cons (j, SOME t)
+ | _ => I) indexed_sets []
+ end
+(* hol_context -> styp -> term list -> (int * term option) list *)
+fun static_args_in_terms hol_ctxt x =
+ map (static_args_in_term hol_ctxt x)
+ #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
+
+(* (int * term option) list -> (int * term) list -> int list *)
+fun overlapping_indices [] _ = []
+ | overlapping_indices _ [] = []
+ | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
+ if j1 < j2 then overlapping_indices ps1' ps2
+ else if j1 > j2 then overlapping_indices ps1 ps2'
+ else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
+
+(* typ list -> term -> bool *)
+fun is_eligible_arg Ts t =
+ let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
+ null bad_Ts orelse
+ (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+ forall (not o is_higher_order_type) bad_Ts)
+ end
+
+(* int -> string *)
+fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
+
+(* If a constant's definition is picked up deeper than this threshold, we
+ prevent excessive specialization by not specializing it. *)
+val special_max_depth = 20
+
+val bound_var_prefix = "b"
+
+(* hol_context -> int -> term -> term *)
+fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
+ special_funs, ...}) depth t =
+ if not specialize orelse depth > special_max_depth then
+ t
+ else
+ let
+ val blacklist = if depth = 0 then []
+ else case term_under_def t of Const x => [x] | _ => []
+ (* term list -> typ list -> term -> term *)
+ fun aux args Ts (Const (x as (s, T))) =
+ ((if not (member (op =) blacklist x) andalso not (null args) andalso
+ not (String.isPrefix special_prefix s) andalso
+ is_equational_fun hol_ctxt x then
+ let
+ val eligible_args = filter (is_eligible_arg Ts o snd)
+ (index_seq 0 (length args) ~~ args)
+ val _ = not (null eligible_args) orelse raise SAME ()
+ val old_axs = equational_fun_axioms hol_ctxt x
+ |> map (destroy_existential_equalities thy)
+ val static_params = static_args_in_terms hol_ctxt x old_axs
+ val fixed_js = overlapping_indices static_params eligible_args
+ val _ = not (null fixed_js) orelse raise SAME ()
+ val fixed_args = filter_indices fixed_js args
+ val vars = fold Term.add_vars fixed_args []
+ |> sort (TermOrd.fast_indexname_ord o pairself fst)
+ val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
+ fixed_args []
+ |> sort int_ord
+ val live_args = filter_out_indices fixed_js args
+ val extra_args = map Var vars @ map Bound bound_js @ live_args
+ val extra_Ts = map snd vars @ filter_indices bound_js Ts
+ val k = maxidx_of_term t + 1
+ (* int -> term *)
+ fun var_for_bound_no j =
+ Var ((bound_var_prefix ^
+ nat_subscript (find_index (curry (op =) j) bound_js
+ + 1), k),
+ nth Ts j)
+ val fixed_args_in_axiom =
+ map (curry subst_bounds
+ (map var_for_bound_no (index_seq 0 (length Ts))))
+ fixed_args
+ in
+ case AList.lookup (op =) (!special_funs)
+ (x, fixed_js, fixed_args_in_axiom) of
+ SOME x' => list_comb (Const x', extra_args)
+ | NONE =>
+ let
+ val extra_args_in_axiom =
+ map Var vars @ map var_for_bound_no bound_js
+ val x' as (s', _) =
+ (special_prefix_for (length (!special_funs) + 1) ^ s,
+ extra_Ts @ filter_out_indices fixed_js (binder_types T)
+ ---> body_type T)
+ val new_axs =
+ map (specialize_fun_axiom x x' fixed_js
+ fixed_args_in_axiom extra_args_in_axiom) old_axs
+ val _ =
+ Unsynchronized.change special_funs
+ (cons ((x, fixed_js, fixed_args_in_axiom), x'))
+ val _ = add_simps simp_table s' new_axs
+ in list_comb (Const x', extra_args) end
+ end
+ else
+ raise SAME ())
+ handle SAME () => list_comb (Const x, args))
+ | aux args Ts (Abs (s, T, t)) =
+ list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
+ | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
+ | aux args _ t = list_comb (t, args)
+ in aux [] [] t end
+
+type special_triple = int list * term list * styp
+
+val cong_var_prefix = "c"
+
+(* styp -> special_triple -> special_triple -> term *)
+fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
+ let
+ val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
+ val Ts = binder_types T
+ val max_j = fold (fold Integer.max) [js1, js2] ~1
+ val (eqs, (args1, args2)) =
+ fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
+ (js1 ~~ ts1, js2 ~~ ts2) of
+ (SOME t1, SOME t2) => apfst (cons (t1, t2))
+ | (SOME t1, NONE) => apsnd (apsnd (cons t1))
+ | (NONE, SOME t2) => apsnd (apfst (cons t2))
+ | (NONE, NONE) =>
+ let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
+ nth Ts j) in
+ apsnd (pairself (cons v))
+ end) (max_j downto 0) ([], ([], []))
+ in
+ Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
+ |> map Logic.mk_equals,
+ Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
+ list_comb (Const x2, bounds2 @ args2)))
+ |> close_form (* TODO: needed? *)
+ end
+
+(* hol_context -> styp list -> term list *)
+fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
+ let
+ val groups =
+ !special_funs
+ |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
+ |> AList.group (op =)
+ |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
+ |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
+ (* special_triple -> int *)
+ fun generality (js, _, _) = ~(length js)
+ (* special_triple -> special_triple -> bool *)
+ fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
+ x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
+ (j2 ~~ t2, j1 ~~ t1)
+ (* styp -> special_triple list -> special_triple list -> special_triple list
+ -> term list -> term list *)
+ fun do_pass_1 _ [] [_] [_] = I
+ | do_pass_1 x skipped _ [] = do_pass_2 x skipped
+ | do_pass_1 x skipped all (z :: zs) =
+ case filter (is_more_specific z) all
+ |> sort (int_ord o pairself generality) of
+ [] => do_pass_1 x (z :: skipped) all zs
+ | (z' :: _) => cons (special_congruence_axiom x z z')
+ #> do_pass_1 x skipped all zs
+ (* styp -> special_triple list -> term list -> term list *)
+ and do_pass_2 _ [] = I
+ | do_pass_2 x (z :: zs) =
+ fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
+ in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
+
+(** Axiom selection **)
+
+(* Similar to "Refute.specialize_type" but returns all matches rather than only
+ the first (preorder) match. *)
+(* theory -> styp -> term -> term list *)
+fun multi_specialize_type thy slack (x as (s, T)) t =
+ let
+ (* term -> (typ * term) list -> (typ * term) list *)
+ fun aux (Const (s', T')) ys =
+ if s = s' then
+ ys |> (if AList.defined (op =) ys T' then
+ I
+ else
+ cons (T', Refute.monomorphic_term
+ (Sign.typ_match thy (T', T) Vartab.empty) t)
+ handle Type.TYPE_MATCH => I
+ | Refute.REFUTE _ =>
+ if slack then
+ I
+ else
+ raise NOT_SUPPORTED ("too much polymorphism in \
+ \axiom involving " ^ quote s))
+ else
+ ys
+ | aux _ ys = ys
+ in map snd (fold_aterms aux t []) end
+
+(* theory -> bool -> const_table -> styp -> term list *)
+fun nondef_props_for_const thy slack table (x as (s, _)) =
+ these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
+
+(* 'a Symtab.table -> 'a list *)
+fun all_table_entries table = Symtab.fold (append o snd) table []
+(* const_table -> string -> const_table *)
+fun extra_table table s = Symtab.make [(s, all_table_entries table)]
+
+(* int -> term -> term *)
+fun eval_axiom_for_term j t =
+ Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
+
+(* term -> bool *)
+val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
+
+(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
+val axioms_max_depth = 255
+
+(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+fun axioms_for_term
+ (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
+ def_table, nondef_table, user_nondefs, ...}) t =
+ let
+ type accumulator = styp list * (term list * term list)
+ (* (term list * term list -> term list)
+ -> ((term list -> term list) -> term list * term list
+ -> term list * term list)
+ -> int -> term -> accumulator -> accumulator *)
+ fun add_axiom get app depth t (accum as (xs, axs)) =
+ let
+ val t = t |> unfold_defs_in_term hol_ctxt
+ |> skolemize_term_and_more hol_ctxt ~1
+ in
+ if is_trivial_equation t then
+ accum
+ else
+ let val t' = t |> specialize_consts_in_term hol_ctxt depth in
+ if exists (member (op aconv) (get axs)) [t, t'] then accum
+ else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
+ end
+ end
+ (* int -> term -> accumulator -> accumulator *)
+ and add_def_axiom depth = add_axiom fst apfst depth
+ and add_nondef_axiom depth = add_axiom snd apsnd depth
+ and add_maybe_def_axiom depth t =
+ (if head_of t <> @{const "==>"} then add_def_axiom
+ else add_nondef_axiom) depth t
+ and add_eq_axiom depth t =
+ (if is_constr_pattern_formula thy t then add_def_axiom
+ else add_nondef_axiom) depth t
+ (* int -> term -> accumulator -> accumulator *)
+ and add_axioms_for_term depth t (accum as (xs, axs)) =
+ case t of
+ t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
+ | Const (x as (s, T)) =>
+ (if member (op =) xs x orelse is_built_in_const fast_descrs x then
+ accum
+ else
+ let val accum as (xs, _) = (x :: xs, axs) in
+ if depth > axioms_max_depth then
+ raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
+ \add_axioms_for_term",
+ "too many nested axioms (" ^
+ string_of_int depth ^ ")")
+ else if Refute.is_const_of_class thy x then
+ let
+ val class = Logic.class_of_const s
+ val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
+ class)
+ val ax1 = try (Refute.specialize_type thy x) of_class
+ val ax2 = Option.map (Refute.specialize_type thy x o snd)
+ (Refute.get_classdef thy class)
+ in
+ fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
+ accum
+ end
+ else if is_constr thy x then
+ accum
+ else if is_equational_fun hol_ctxt x then
+ fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
+ accum
+ else if is_abs_fun thy x then
+ if is_quot_type thy (range_type T) then
+ raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
+ (extra_table def_table s) x)
+ else if is_rep_fun thy x then
+ if is_quot_type thy (domain_type T) then
+ raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
+ (extra_table def_table s) x)
+ |> add_axioms_for_term depth
+ (Const (mate_of_rep_fun thy x))
+ |> fold (add_def_axiom depth)
+ (inverse_axioms_for_rep_fun thy x)
+ else
+ accum |> user_axioms <> SOME false
+ ? fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ end)
+ |> add_axioms_for_type depth T
+ | Free (_, T) => add_axioms_for_type depth T accum
+ | Var (_, T) => add_axioms_for_type depth T accum
+ | Bound _ => accum
+ | Abs (_, T, t) => accum |> add_axioms_for_term depth t
+ |> add_axioms_for_type depth T
+ (* int -> typ -> accumulator -> accumulator *)
+ and add_axioms_for_type depth T =
+ case T of
+ Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
+ | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
+ | @{typ prop} => I
+ | @{typ bool} => I
+ | @{typ unit} => I
+ | TFree (_, S) => add_axioms_for_sort depth T S
+ | TVar (_, S) => add_axioms_for_sort depth T S
+ | Type (z as (s, Ts)) =>
+ fold (add_axioms_for_type depth) Ts
+ #> (if is_pure_typedef thy T then
+ fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+ else if is_quot_type thy T then
+ fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
+ else if max_bisim_depth >= 0 andalso is_codatatype thy T then
+ fold (add_maybe_def_axiom depth)
+ (codatatype_bisim_axioms hol_ctxt T)
+ else
+ I)
+ (* int -> typ -> sort -> accumulator -> accumulator *)
+ and add_axioms_for_sort depth T S =
+ let
+ val supers = Sign.complete_sort thy S
+ val class_axioms =
+ maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
+ handle ERROR _ => [])) supers
+ val monomorphic_class_axioms =
+ map (fn t => case Term.add_tvars t [] of
+ [] => t
+ | [(x, S)] =>
+ Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+ | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
+ \add_axioms_for_sort", [t]))
+ class_axioms
+ in fold (add_nondef_axiom depth) monomorphic_class_axioms end
+ val (mono_user_nondefs, poly_user_nondefs) =
+ List.partition (null o Term.hidden_polymorphism) user_nondefs
+ val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
+ evals
+ val (xs, (defs, nondefs)) =
+ ([], ([], [])) |> add_axioms_for_term 1 t
+ |> fold_rev (add_def_axiom 1) eval_axioms
+ |> user_axioms = SOME true
+ ? fold (add_nondef_axiom 1) mono_user_nondefs
+ val defs = defs @ special_congruence_axioms hol_ctxt xs
+ in
+ ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
+ null poly_user_nondefs))
+ end
+
+(** Simplification of constructor/selector terms **)
+
+(* theory -> term -> term *)
+fun simplify_constrs_and_sels thy t =
+ let
+ (* term -> int -> term *)
+ fun is_nth_sel_on t' n (Const (s, _) $ t) =
+ (t = t' andalso is_sel_like_and_no_discr s andalso
+ sel_no_from_name s = n)
+ | is_nth_sel_on _ _ _ = false
+ (* term -> term list -> term *)
+ fun do_term (Const (@{const_name Rep_Frac}, _)
+ $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
+ | do_term (Const (@{const_name Abs_Frac}, _)
+ $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
+ | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
+ | do_term (t as Const (x as (s, T))) (args as _ :: _) =
+ ((if is_constr_like thy x then
+ if length args = num_binder_types T then
+ case hd args of
+ Const (x' as (_, T')) $ t' =>
+ if domain_type T' = body_type T andalso
+ forall (uncurry (is_nth_sel_on t'))
+ (index_seq 0 (length args) ~~ args) then
+ t'
+ else
+ raise SAME ()
+ | _ => raise SAME ()
+ else
+ raise SAME ()
+ else if is_sel_like_and_no_discr s then
+ case strip_comb (hd args) of
+ (Const (x' as (s', T')), ts') =>
+ if is_constr_like thy x' andalso
+ constr_name_for_sel_like s = s' andalso
+ not (exists is_pair_type (binder_types T')) then
+ list_comb (nth ts' (sel_no_from_name s), tl args)
+ else
+ raise SAME ()
+ | _ => raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () => betapplys (t, args))
+ | do_term (Abs (s, T, t')) args =
+ betapplys (Abs (s, T, do_term t' []), args)
+ | do_term t args = betapplys (t, args)
+ in do_term t [] end
+
+(** Quantifier massaging: Distributing quantifiers **)
+
+(* term -> term *)
+fun distribute_quantifiers t =
+ case t of
+ (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
+ (case t1 of
+ (t10 as @{const "op &"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const Not}) $ t11 =>
+ t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
+ $ Abs (s, T1, t11))
+ | t1 =>
+ if not (loose_bvar1 (t1, 0)) then
+ distribute_quantifiers (incr_boundvars ~1 t1)
+ else
+ t0 $ Abs (s, T1, distribute_quantifiers t1))
+ | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
+ (case distribute_quantifiers t1 of
+ (t10 as @{const "op |"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+ $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const Not}) $ t11 =>
+ t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+ $ Abs (s, T1, t11))
+ | t1 =>
+ if not (loose_bvar1 (t1, 0)) then
+ distribute_quantifiers (incr_boundvars ~1 t1)
+ else
+ t0 $ Abs (s, T1, distribute_quantifiers t1))
+ | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
+ | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
+ | _ => t
+
+(** Quantifier massaging: Pushing quantifiers inward **)
+
+(* int -> int -> (int -> int) -> term -> term *)
+fun renumber_bounds j n f t =
+ case t of
+ t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
+ | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
+ | Bound j' =>
+ Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
+ | _ => t
+
+(* Maximum number of quantifiers in a cluster for which the exponential
+ algorithm is used. Larger clusters use a heuristic inspired by Claessen &
+ Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+ paper). *)
+val quantifier_cluster_threshold = 7
+
+(* theory -> term -> term *)
+fun push_quantifiers_inward thy =
+ let
+ (* string -> string list -> typ list -> term -> term *)
+ fun aux quant_s ss Ts t =
+ (case t of
+ (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
+ if s0 = quant_s then
+ aux s0 (s1 :: ss) (T1 :: Ts) t1
+ else if quant_s = "" andalso
+ (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
+ aux s0 [s1] [T1] t1
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ case t of
+ t1 $ t2 =>
+ if quant_s = "" then
+ aux "" [] [] t1 $ aux "" [] [] t2
+ else
+ let
+ val typical_card = 4
+ (* ('a -> ''b list) -> 'a list -> ''b list *)
+ fun big_union proj ps =
+ fold (fold (insert (op =)) o proj) ps []
+ val (ts, connective) = strip_any_connective t
+ val T_costs =
+ map (bounded_card_of_type 65536 typical_card []) Ts
+ val t_costs = map size_of_term ts
+ val num_Ts = length Ts
+ (* int -> int *)
+ val flip = curry (op -) (num_Ts - 1)
+ val t_boundss = map (map flip o loose_bnos) ts
+ (* (int list * int) list -> int list
+ -> (int list * int) list *)
+ fun merge costly_boundss [] = costly_boundss
+ | merge costly_boundss (j :: js) =
+ let
+ val (yeas, nays) =
+ List.partition (fn (bounds, _) =>
+ member (op =) bounds j)
+ costly_boundss
+ val yeas_bounds = big_union fst yeas
+ val yeas_cost = Integer.sum (map snd yeas)
+ * nth T_costs j
+ in merge ((yeas_bounds, yeas_cost) :: nays) js end
+ (* (int list * int) list -> int list -> int *)
+ val cost = Integer.sum o map snd oo merge
+ (* (int list * int) list -> int list -> int list *)
+ fun heuristically_best_permutation _ [] = []
+ | heuristically_best_permutation costly_boundss js =
+ let
+ val (costly_boundss, (j, js)) =
+ js |> map (`(merge costly_boundss o single))
+ |> sort (int_ord
+ o pairself (Integer.sum o map snd o fst))
+ |> split_list |>> hd ||> pairf hd tl
+ in
+ j :: heuristically_best_permutation costly_boundss js
+ end
+ val js =
+ if length Ts <= quantifier_cluster_threshold then
+ all_permutations (index_seq 0 num_Ts)
+ |> map (`(cost (t_boundss ~~ t_costs)))
+ |> sort (int_ord o pairself fst) |> hd |> snd
+ else
+ heuristically_best_permutation (t_boundss ~~ t_costs)
+ (index_seq 0 num_Ts)
+ val back_js = map (fn j => find_index (curry (op =) j) js)
+ (index_seq 0 num_Ts)
+ val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
+ ts
+ (* (term * int list) list -> term *)
+ fun mk_connection [] =
+ raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
+ \mk_connection", "")
+ | mk_connection ts_cum_bounds =
+ ts_cum_bounds |> map fst
+ |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
+ (* (term * int list) list -> int list -> term *)
+ fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
+ | build ts_cum_bounds (j :: js) =
+ let
+ val (yeas, nays) =
+ List.partition (fn (_, bounds) =>
+ member (op =) bounds j)
+ ts_cum_bounds
+ ||> map (apfst (incr_boundvars ~1))
+ in
+ if null yeas then
+ build nays js
+ else
+ let val T = nth Ts (flip j) in
+ build ((Const (quant_s, (T --> bool_T) --> bool_T)
+ $ Abs (nth ss (flip j), T,
+ mk_connection yeas),
+ big_union snd yeas) :: nays) js
+ end
+ end
+ in build (ts ~~ t_boundss) js end
+ | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
+ | _ => t
+ in aux "" [] [] end
+
+(** Preprocessor entry point **)
+
+(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
+fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
+ skolemize, uncurry, ...}) t =
+ let
+ val skolem_depth = if skolemize then 4 else ~1
+ val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
+ core_t) = t |> unfold_defs_in_term hol_ctxt
+ |> close_form
+ |> skolemize_term_and_more hol_ctxt skolem_depth
+ |> specialize_consts_in_term hol_ctxt 0
+ |> `(axioms_for_term hol_ctxt)
+ val binarize =
+ case binary_ints of
+ SOME false => false
+ | _ =>
+ forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ (binary_ints = SOME true orelse
+ exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ val box = exists (not_equal (SOME false) o snd) boxes
+ val table =
+ Termtab.empty |> uncurry
+ ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+ (* bool -> bool -> term -> term *)
+ fun do_rest def core =
+ binarize ? binarize_nat_and_int_in_term
+ #> uncurry ? uncurry_term table
+ #> box ? box_fun_and_pair_in_term hol_ctxt def
+ #> destroy_constrs ? (pull_out_universal_constrs thy def
+ #> pull_out_existential_constrs thy
+ #> destroy_pulled_out_constrs hol_ctxt def)
+ #> curry_assms
+ #> destroy_universal_equalities
+ #> destroy_existential_equalities thy
+ #> simplify_constrs_and_sels thy
+ #> distribute_quantifiers
+ #> push_quantifiers_inward thy
+ #> close_form
+ #> Term.map_abs_vars shortest_name
+ in
+ (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
+ (got_all_mono_user_axioms, no_poly_user_axioms)),
+ do_rest false true core_t)
+ end
+
+end;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 09 21:32:57 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_SCOPE =
sig
type styp = Nitpick_Util.styp
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type constr_spec = {
const: styp,
@@ -28,7 +28,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -47,7 +47,7 @@
val scopes_equivalent : scope -> scope -> bool
val scope_less_eq : scope -> scope -> bool
val all_scopes :
- extended_context -> int -> (typ option * int list) list
+ hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
-> int list -> int list -> typ list -> typ list -> typ list
-> int * scope list
@@ -77,7 +77,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -131,10 +131,10 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
-fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
+fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, bisim_depth, datatypes, ...} : scope) =
let
- val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
+ val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@{typ bisim_iterator}]
val (iter_assigns, card_assigns) =
card_assigns |> filter_out (member (op =) boring_Ts o fst)
@@ -240,10 +240,9 @@
val max_bits = 31 (* Kodkod limit *)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ -> block *)
-fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ -> block *)
+fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
iters_assigns bitss bisim_depths T =
if T = @{typ unsigned_bit} then
[(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
@@ -261,18 +260,18 @@
(const_for_iterator_type T)))]
else
(Card T, lookup_type_ints_assign thy cards_assigns T) ::
- (case datatype_constrs ext_ctxt T of
+ (case datatype_constrs hol_ctxt T of
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ list -> typ list -> block list *)
-fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ list
+ -> typ list -> block list *)
+fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
bisim_depths mono_Ts nonmono_Ts =
let
(* typ -> block *)
- val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
+ val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
@@ -313,10 +312,10 @@
type scope_desc = (typ * int) list * (styp * int) list
-(* extended_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
+(* hol_context -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
(T, k) =
- case datatype_constrs ext_ctxt T of
+ case datatype_constrs hol_ctxt T of
[] => false
| xs =>
let
@@ -329,20 +328,20 @@
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
-(* extended_context -> (typ * int) list -> (typ * int) list
- -> (styp * int) list -> bool *)
-fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
- exists (is_surely_inconsistent_card_assign ext_ctxt
+(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
+ -> bool *)
+fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
+ exists (is_surely_inconsistent_card_assign hol_ctxt
(seen @ rest, max_assigns)) seen
-(* extended_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
+(* hol_context -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux seen ((T, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
- (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
+ (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
rest max_assigns then
raise SAME ()
else
@@ -374,12 +373,12 @@
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* extended_context -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
+(* hol_context -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
let
val (card_assigns, max_assigns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
+ val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
|> the
in
SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
@@ -427,15 +426,21 @@
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
else if not co andalso num_self_recs > 0 then
- if not self_rec andalso num_non_self_recs = 1 andalso
- domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1,
- exclusive = (s = @{const_name Nil} andalso length constrs = 2),
- total = true}
- else if s = @{const_name Cons} andalso length constrs = 2 then
- {delta = 1, epsilon = card, exclusive = true, total = false}
- else
- {delta = 0, epsilon = card, exclusive = false, total = false}
+ (if num_self_recs = 1 andalso num_non_self_recs = 1 then
+ if self_rec then
+ case constrs of
+ [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
+ {delta = 1, epsilon = card, exclusive = true, total = false}
+ | _ => raise SAME ()
+ else
+ if domain_card 2 card_assigns T = 1 then
+ {delta = 0, epsilon = 1, exclusive = true, total = true}
+ else
+ raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () =>
+ {delta = 0, epsilon = card, exclusive = false, total = false}
else if card = sum_dom_cards (card + 1) then
let val delta = next_delta () in
{delta = delta, epsilon = delta + domain_card card card_assigns T,
@@ -449,31 +454,32 @@
explicit_max = max, total = total} :: constrs
end
-(* extended_context -> (typ * int) list -> typ -> bool *)
-fun has_exact_card ext_ctxt card_assigns T =
+(* hol_context -> (typ * int) list -> typ -> bool *)
+fun has_exact_card hol_ctxt card_assigns T =
let val card = card_of_type card_assigns T in
- card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
+ card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
end
-(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
+(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
(desc as (card_assigns, _)) (T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
- val xs = boxed_datatype_constrs ext_ctxt T
+ val xs = boxed_datatype_constrs hol_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
- val complete = has_exact_card ext_ctxt card_assigns T
+ val complete = has_exact_card hol_ctxt card_assigns T
val concrete = xs |> maps (binder_types o snd) |> maps binder_types
- |> forall (has_exact_card ext_ctxt card_assigns)
+ |> forall (has_exact_card hol_ctxt card_assigns)
(* int -> int *)
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
- num_non_self_recs) (self_recs ~~ xs) []
+ num_non_self_recs)
+ (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
{typ = T, card = card, co = co, complete = complete, concrete = concrete,
deep = deep, constrs = constrs}
@@ -487,12 +493,12 @@
min_bits_for_nat_value (fold Integer.max
(map snd card_assigns @ map snd max_assigns) 0)
-(* extended_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
+(* hol_context -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
(desc as (card_assigns, _)) =
let
val datatypes =
- map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
+ map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
(filter (is_datatype thy o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
@@ -500,7 +506,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
- {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
+ {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
else offset_table_for_card_assigns thy card_assigns datatypes}
@@ -521,26 +527,26 @@
val max_scopes = 4096
val distinct_threshold = 512
-(* extended_context -> int -> (typ option * int list) list
+(* hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
+fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
let
val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
cards_assigns
- val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
+ val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts
nonmono_Ts
val ranks = map rank_of_block blocks
val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
val head = take max_scopes all
- val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
+ val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
head
in
(length all - length head,
descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
+ |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
end
end;
--- a/src/Tools/quickcheck.ML Tue Feb 09 16:07:09 2010 +0100
+++ b/src/Tools/quickcheck.ML Tue Feb 09 21:32:57 2010 +0100
@@ -153,9 +153,9 @@
|> ObjectLogic.atomize_term thy;
in test_term ctxt quiet generator_name size iterations gi' end;
-fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
+fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
| pretty_counterex ctxt (SOME cex) =
- Pretty.chunks (Pretty.str "Counterexample found:\n" ::
+ Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::
map (fn (s, t) =>
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);