--- a/Admin/isatest/settings/mac-poly Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/mac-poly Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2"
- ML_SYSTEM="polyml-5.2"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="ppc-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/Admin/isatest/settings/mac-poly-M4 Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/mac-poly-M4 Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/Admin/isatest/settings/mac-poly-M8 Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/mac-poly-M8 Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/Admin/isatest/settings/mac-poly64-M4 Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/mac-poly64-M4 Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 4000 --immutable 2000"
--- a/Admin/isatest/settings/mac-poly64-M8 Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/mac-poly64-M8 Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 4000 --immutable 2000"
--- a/Admin/isatest/settings/sun-poly Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/isatest/settings/sun-poly Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="sparc-solaris"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 1000"
--- a/Admin/polyml/README Tue Nov 10 06:47:55 2009 -0800
+++ b/Admin/polyml/README Tue Nov 10 06:48:26 2009 -0800
@@ -1,19 +1,18 @@
-This distribution of Poly/ML 5.2.1 has been compiled from the original
+This distribution of Poly/ML 5.3 has been compiled from the original
sources as follows:
- tar xvzf polyml.5.2.1.tar.gz
- cd polyml.5.2.1
- ./configure --prefix=/tmp/polyml
+ tar xvzf polyml.5.3.tar.gz
+ cd polyml.5.3
+ ./configure --prefix="$HOME/tmp/polyml"
make
make install
-Now /tmp/polyml/bin/* and /tmp/polyml/lib/* are moved to the
-platform-specific target directory (e.g. polyml-5.2.1/x86-linux). Note
-that Isabelle/lib/scripts/polyml-platform identifies your platform.
+Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the
+platform-specific target directory (e.g. polyml-5.3.0/x86-linux).
+Note that Isabelle/lib/scripts/polyml-platform identifies your
+platform.
Makarius
- 22-Oct-2008
-
-$Id$
+ 09-Nov-2009
--- a/doc-src/Nitpick/nitpick.tex Tue Nov 10 06:47:55 2009 -0800
+++ b/doc-src/Nitpick/nitpick.tex Tue Nov 10 06:48:26 2009 -0800
@@ -2,7 +2,7 @@
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
-\usepackage[french,english]{babel}
+\usepackage[english,french]{babel}
\usepackage{color}
\usepackage{graphicx}
%\usepackage{mathpazo}
@@ -40,6 +40,8 @@
\begin{document}
+\selectlanguage{english}
+
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
Picking Nits \\[\smallskipamount]
\Large A User's Guide to Nitpick for Isabelle/HOL 2010}
@@ -112,6 +114,13 @@
machine called \texttt{java}. The examples presented in this manual can be found
in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
+Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
+Nitpick also provides an automatic mode that can be enabled using the
+``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
+mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
+The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
+the ``Auto Counterexample Time Limit'' option.
+
\newbox\boxA
\setbox\boxA=\hbox{\texttt{nospam}}
@@ -154,16 +163,6 @@
configured SAT solvers in Isabelle (e.g., for Refute), these will also be
available to Nitpick.
-Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
-Nitpick also provides an automatic mode that can be enabled by specifying
-
-\prew
-\textbf{nitpick\_params} [\textit{auto}]
-\postw
-
-at the beginning of the theory file. In this mode, Nitpick is run for up to 5
-seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
-
\subsection{Propositional Logic}
\label{propositional-logic}
@@ -1595,6 +1594,17 @@
(\S\ref{authentication}), optimizations
(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
+You can instruct Nitpick to run automatically on newly entered theorems by
+enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
+General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
+and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
+\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
+disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
+\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
+Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
+concise.
+
The number of options can be overwhelming at first glance. Do not let that worry
you: Nitpick's defaults have been chosen so that it almost always does the right
thing, and the most important options have been covered in context in
@@ -1622,35 +1632,19 @@
\end{enum}
Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
-options, ``= \textit{true}'' may be omitted.
+counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
+Boolean options, ``= \textit{true}'' may be omitted.
\subsection{Mode of Operation}
\label{mode-of-operation}
\begin{enum}
-\opfalse{auto}{no\_auto}
-Specifies whether Nitpick should be run automatically on newly entered theorems.
-For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
-\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
-\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
-(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
-disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
-\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
-\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
-
-\nopagebreak
-{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
-
\optrue{blocking}{non\_blocking}
Specifies whether the \textbf{nitpick} command should operate synchronously.
The asynchronous (non-blocking) mode lets the user start proving the putative
theorem while Nitpick looks for a counterexample, but it can also be more
confusing. For technical reasons, automatic runs currently always block.
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
\optrue{falsify}{satisfy}
Specifies whether Nitpick should look for falsifying examples (countermodels) or
satisfying examples (models). This manual assumes throughout that
@@ -1670,16 +1664,15 @@
considered.
\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
-(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
+{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
+(\S\ref{output-format}).}
\optrue{assms}{no\_assms}
Specifies whether the relevant assumptions in structured proof should be
considered. The option is implicitly enabled for automatic runs.
\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
+{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
\opfalse{overlord}{no\_overlord}
Specifies whether Nitpick should put its temporary files in
@@ -1836,14 +1829,14 @@
\nopagebreak
{\small See also \textit{card} (\S\ref{scope-of-search}),
-\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
+\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
(\S\ref{output-format}).}
\opsmart{mono}{non\_box}
Specifies the default monotonicity setting to use. This can be overridden on a
per-type basis using the \textit{mono}~\qty{type} option described above.
-\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
+\opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
Specifies whether type variables with the same sort constraints should be
merged. Setting this option to \textit{true} can reduce the number of scopes
tried and the size of the generated Kodkod formulas, but it also diminishes the
@@ -1861,9 +1854,6 @@
option is useful to determine which scopes are tried or which SAT solver is
used. This option is implicitly disabled for automatic runs.
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
\opfalse{debug}{no\_debug}
Specifies whether Nitpick should display additional debugging information beyond
what \textit{verbose} already displays. Enabling \textit{debug} also enables
@@ -1871,8 +1861,8 @@
option is implicitly disabled for automatic runs.
\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
-(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
+{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
+\textit{batch\_size} (\S\ref{optimizations}).}
\optrue{show\_skolems}{hide\_skolem}
Specifies whether the values of Skolem constants should be displayed as part of
@@ -1910,8 +1900,7 @@
enabled.
\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}),
-\textit{check\_potential} (\S\ref{authentication}), and
+{\small See also \textit{check\_potential} (\S\ref{authentication}) and
\textit{sat\_solver} (\S\ref{optimizations}).}
\opt{max\_genuine}{int}{$\mathbf{1}$}
@@ -1968,8 +1957,7 @@
shown to be genuine, Nitpick displays a message to this effect and terminates.
\nopagebreak
-{\small See also \textit{max\_potential} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_potential} (\S\ref{output-format}).}
\opfalse{check\_genuine}{trust\_genuine}
Specifies whether genuine and likely genuine counterexamples should be given to
@@ -1979,8 +1967,7 @@
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
\nopagebreak
-{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
\ops{expect}{string}
Specifies the expected outcome, which must be one of the following:
@@ -2206,21 +2193,14 @@
Specifies the maximum amount of time that the \textbf{nitpick} command should
spend looking for a counterexample. Nitpick tries to honor this constraint as
well as it can but offers no guarantees. For automatic runs,
-\textit{auto\_timeout} is used instead.
+\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
+a time slot whose length is specified by the ``Auto Counterexample Time
+Limit'' option in Proof General.
\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{max\_threads} (\S\ref{optimizations}).}
-
-\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
-Specifies the maximum amount of time that Nitpick should use to find a
-counterexample when running automatically. Nitpick tries to honor this
-constraint as well as it can but offers no guarantees.
-
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
-\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
+{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
+
+\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
Specifies the maximum amount of time that the \textit{auto} tactic should use
when checking a counterexample, and similarly that \textit{lexicographic\_order}
and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
@@ -2398,11 +2378,11 @@
& \textit{subgoal}\end{aligned}$
\postw
+\let\antiq=\textrm
+
\subsection{Registration of Coinductive Datatypes}
\label{registration-of-coinductive-datatypes}
-\let\antiq=\textrm
-
If you have defined a custom coinductive datatype, you can tell Nitpick about
it, so that it can use an efficient Kodkod axiomatization similar to the one it
uses for lazy lists. The interface for registering and unregistering coinductive
@@ -2440,6 +2420,11 @@
\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
\postw
+Inductive datatypes can be registered as coinductive datatypes, given
+appropriate coinductive constructors. However, doing so precludes
+the use of the inductive constructors---Nitpick will generate an error if they
+are needed.
+
\section{Known Bugs and Limitations}
\label{known-bugs-and-limitations}
@@ -2467,12 +2452,21 @@
representation of functions synthesized by Isabelle, which is an implementation
detail.
+\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
+which can become invalid if you change the definition of an inductive predicate
+that is registered in the cache. To clear the cache,
+run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
+501$\,\textit{ms}$).
+
\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
\item[$\bullet$] The \textit{nitpick\_} attributes and the
\textit{Nitpick.register\_} functions can cause havoc if used improperly.
+\item[$\bullet$] Although this has never been observed, arbitrary theorem
+morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
+
\item[$\bullet$] Local definitions are not supported and result in an error.
\item[$\bullet$] All constants and types whose names start with
Binary file doc-src/gfx/isabelle_nitpick.pdf has changed
--- a/etc/settings Tue Nov 10 06:47:55 2009 -0800
+++ b/etc/settings Tue Nov 10 06:48:26 2009 -0800
@@ -29,23 +29,18 @@
ML_OPTIONS="-H 200"
ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.2.1
+# Poly/ML 5.3.0
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.2.1
+#ML_SYSTEM=polyml-5.3.0
#ML_OPTIONS="-H 500"
+#ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.2.1 (64 bit)
+# Poly/ML 5.3.0 (64 bit)
#ML_PLATFORM=x86_64-linux
#ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.2.1
+#ML_SYSTEM=polyml-5.3.0
#ML_OPTIONS="-H 1000"
-
-# Poly/ML 5.3 (experimental)
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-experimental
-#ML_OPTIONS="-H 500"
#ML_SOURCES="$ML_HOME/../src"
# Standard ML of New Jersey (slow!)
--- a/src/HOL/IsaMakefile Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/IsaMakefile Tue Nov 10 06:48:26 2009 -0800
@@ -103,6 +103,7 @@
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
+ $(SRC)/Tools/Auto_Counterexample.thy \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_preproc.ML \
@@ -115,6 +116,7 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
+ $(SRC)/Tools/auto_counterexample.ML \
$(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
--- a/src/HOL/Main.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Main.thy Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Nitpick Predicate_Compile Recdef
+imports Plain Nitpick Predicate_Compile
begin
text {*
--- a/src/HOL/Nitpick.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Nitpick.thy Tue Nov 10 06:48:26 2009 -0800
@@ -8,7 +8,7 @@
header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
theory Nitpick
-imports Map SAT
+imports Map Quickcheck SAT
uses ("Tools/Nitpick/kodkod.ML")
("Tools/Nitpick/kodkod_sat.ML")
("Tools/Nitpick/nitpick_util.ML")
@@ -117,12 +117,16 @@
apply (simp only: unit.cases)
by simp
+declare unit.cases [nitpick_simp del]
+
lemma nat_case_def [nitpick_def]:
"nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
apply (rule eq_reflection)
by (case_tac n) auto
-lemmas dvd_def = dvd_eq_mod_eq_0 [THEN eq_reflection, nitpick_def]
+declare nat.cases [nitpick_simp del]
+
+lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
lemma list_size_simp [nitpick_simp]:
"list_size f xs = (if xs = [] then 0
@@ -206,6 +210,21 @@
definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
"of_frac q \<equiv> of_int (num q) / of_int (denom q)"
+(* While Nitpick normally avoids to unfold definitions for locales, it
+ unfortunately needs to unfold them when dealing with the following built-in
+ constants. A cleaner approach would be to change "Nitpick_HOL" and
+ "Nitpick_Nits" so that they handle the unexpanded overloaded constants
+ directly, but this is slightly more tricky to implement. *)
+lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
+ div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
+ minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
+ one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
+ ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
+ ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
+ times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
+ upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
+ zero_nat_inst.zero_nat
+
use "Tools/Nitpick/kodkod.ML"
use "Tools/Nitpick/kodkod_sat.ML"
use "Tools/Nitpick/nitpick_util.ML"
@@ -222,6 +241,8 @@
use "Tools/Nitpick/nitpick_tests.ML"
use "Tools/Nitpick/minipick.ML"
+setup {* Nitpick_Isar.setup *}
+
hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
@@ -230,10 +251,10 @@
hide (open) type bisim_iterator pair_box fun_box
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
- The_psimp Eps_psimp unit_case_def nat_case_def dvd_def list_size_simp
- nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def
- one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def
- times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def
- less_eq_frac_def of_frac_def
+ The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
+ nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
+ num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
+ uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
+ of_frac_def
end
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Nov 10 06:48:26 2009 -0800
@@ -28,7 +28,7 @@
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
(* term -> bool *)
-val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
+val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
fun is_const t =
let val T = fastype_of t in
is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Nov 10 06:48:26 2009 -0800
@@ -173,15 +173,15 @@
Ycoord :: int
lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
-nitpick [expect = unknown]
+nitpick [expect = none]
by (rule Rep_point_ext_type_inverse)
lemma "Fract a b = of_int a / of_int b"
-nitpick [card = 1\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Fract_of_int_quotient)
lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Rep_Rat_inverse)
end
--- a/src/HOL/Probability/Borel.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/Borel.thy Tue Nov 10 06:48:26 2009 -0800
@@ -17,8 +17,8 @@
definition mono_convergent where
"mono_convergent u f s \<equiv>
- (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
- (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+ (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+ (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
@@ -222,7 +222,7 @@
shows "{w \<in> space M. f w < g w} \<in> sets M"
proof -
have "{w \<in> space M. f w < g w} =
- (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+ (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
by (auto simp add: Rats_dense_in_real)
thus ?thesis using f g
by (simp add: borel_measurable_less_iff [of f]
@@ -247,7 +247,7 @@
shows "{w \<in> space M. f w = g w} \<in> sets M"
proof -
have "{w \<in> space M. f w = g w} =
- {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+ {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
by auto
thus ?thesis using f g
by (simp add: borel_measurable_leq_borel_measurable Int)
--- a/src/HOL/Probability/Caratheodory.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/Caratheodory.thy Tue Nov 10 06:48:26 2009 -0800
@@ -2,7 +2,6 @@
theory Caratheodory
imports Sigma_Algebra SupInf SeriesPlus
-
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -136,7 +135,7 @@
proof
fix n
show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
- by (induct n) (auto simp add: binaryset_def f)
+ by (induct n) (auto simp add: binaryset_def f)
qed
moreover
have "... ----> f A + f B" by (rule LIMSEQ_const)
@@ -198,30 +197,30 @@
proof -
from xl yl show ?thesis
proof (auto simp add: positive_def lambda_system_eq Int)
- fix u
- assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
+ fix u
+ assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
- have "u - x \<inter> y \<in> sets M"
- by (metis Diff Diff_Int Un u x y)
- moreover
- have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
- moreover
- have "u - x \<inter> y - y = u - y" by blast
- ultimately
- have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
- by force
- have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
+ have "u - x \<inter> y \<in> sets M"
+ by (metis Diff Diff_Int Un u x y)
+ moreover
+ have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
+ moreover
+ have "u - x \<inter> y - y = u - y" by blast
+ ultimately
+ have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
+ by force
+ have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
= (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
- by (simp add: ey)
- also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
- by (simp add: Int_ac)
- also have "... = f (u \<inter> y) + f (u - y)"
- using fx [THEN bspec, of "u \<inter> y"] Int y u
- by force
- also have "... = f u"
- by (metis fy u)
- finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
+ by (simp add: ey)
+ also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
+ by (simp add: Int_ac)
+ also have "... = f (u \<inter> y) + f (u - y)"
+ using fx [THEN bspec, of "u \<inter> y"] Int y u
+ by force
+ also have "... = f u"
+ by (metis fy u)
+ finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
qed
qed
@@ -478,11 +477,11 @@
have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
proof (rule antisym)
show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
- by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
+ by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
- by (rule suminf_le [OF sumfA])
+ by (rule suminf_le [OF sumfA])
(metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
- lambda_system_positive lambda_system_additive
+ lambda_system_positive lambda_system_additive
subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
qed
{
@@ -491,58 +490,58 @@
have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
proof -
have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A''
- apply -
- apply (rule summable_comparison_test [OF _ sumfA])
- apply (rule_tac x="0" in exI)
- apply (simp add: positive_def)
- apply (auto simp add: )
- apply (subst abs_of_nonneg)
- apply (metis A'' Int UNIV_I a image_subset_iff)
- apply (blast intro: increasingD [OF inc] a)
- done
+ apply -
+ apply (rule summable_comparison_test [OF _ sumfA])
+ apply (rule_tac x="0" in exI)
+ apply (simp add: positive_def)
+ apply (auto simp add: )
+ apply (subst abs_of_nonneg)
+ apply (metis A'' Int UNIV_I a image_subset_iff)
+ apply (blast intro: increasingD [OF inc] a)
+ done
show ?thesis
proof (rule antisym)
- have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
- by blast
- moreover
- have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
- by (auto simp add: disjoint_family_def)
- moreover
- have "a \<inter> (\<Union>i. A i) \<in> sets M"
- by (metis Int U_in a)
- ultimately
- have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
- using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
- by (simp add: o_def)
- moreover
- have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) \<le> f a - f (a - (\<Union>i. A i))"
- proof (rule suminf_le [OF summ])
- fix n
- have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
- by (metis A'' UNION_in_sets)
- have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
- by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
- have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
- using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
- by (simp add: A)
- hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
- by (simp add: lambda_system_eq UNION_in Diff_Compl a)
- have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
- by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
+ have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
+ by blast
+ moreover
+ have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+ by (auto simp add: disjoint_family_def)
+ moreover
+ have "a \<inter> (\<Union>i. A i) \<in> sets M"
+ by (metis Int U_in a)
+ ultimately
+ have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
+ using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
+ by (simp add: o_def)
+ moreover
+ have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) \<le> f a - f (a - (\<Union>i. A i))"
+ proof (rule suminf_le [OF summ])
+ fix n
+ have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+ by (metis A'' UNION_in_sets)
+ have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+ by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
+ have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
+ using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
+ by (simp add: A)
+ hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
+ by (simp add: lambda_system_eq UNION_in Diff_Compl a)
+ have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+ by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
UNION_in U_in a)
- thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
- using eq_fa
- by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
+ thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
+ using eq_fa
+ by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
a A disj)
- qed
- ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
- by arith
+ qed
+ ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
+ by arith
next
- have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
- by (blast intro: increasingD [OF inc] a U_in)
- also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
- by (blast intro: subadditiveD [OF sa] Int Diff U_in)
- finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
+ have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
+ by (blast intro: increasingD [OF inc] a U_in)
+ also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+ by (blast intro: subadditiveD [OF sa] Int Diff U_in)
+ finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
qed
qed
}
@@ -654,20 +653,20 @@
have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
proof (rule countably_additiveD [OF ca])
show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
- by blast
+ by blast
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
- by (auto simp add: disjoint_family_def)
+ by (auto simp add: disjoint_family_def)
show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
- by (metis UN_extend_simps(4) s seq)
+ by (metis UN_extend_simps(4) s seq)
qed
hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
by (metis Int_commute UN_simps(4) seq sums_iff)
also have "... \<le> suminf (f \<circ> A)"
proof (rule summable_le [OF _ _ sm])
show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
- by (force intro: increasingD [OF inc])
+ by (force intro: increasingD [OF inc])
show "summable (\<lambda>i. f (A i \<inter> s))" using sums
- by (simp add: sums_iff)
+ by (simp add: sums_iff)
qed
also have "... = z" by (rule si)
finally show "f s \<le> z" .
@@ -722,9 +721,9 @@
proof (auto)
fix n
have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
- by (auto simp add: positive_def image_subset_iff)
+ by (auto simp add: positive_def image_subset_iff)
also have "... \<le> f (A n)"
- by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+ by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
qed
from Series.summable_le2 [OF this sm]
@@ -787,32 +786,32 @@
and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
by auto blast
have llpos: "!!n. 0 \<le> ll n"
- by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
+ by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
range_subsetD BB)
have sll: "summable ll &
suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
proof -
- have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
- by (rule sums_mult [OF power_half_series])
- hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
- and eqe: "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
- by (auto simp add: sums_iff)
- have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
+ have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
+ by (rule sums_mult [OF power_half_series])
+ hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
+ and eqe: "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
+ by (auto simp add: sums_iff)
+ have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
suminf (\<lambda>n. e * (1/2)^(Suc n)) =
suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
- by (rule suminf_add [OF sum1 sum0])
- have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
- by (metis ll llpos abs_of_nonneg)
- have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
- by (rule summable_add [OF sum1 sum0])
- have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
- using Series.summable_le2 [OF 1 2] by auto
- also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
+ by (rule suminf_add [OF sum1 sum0])
+ have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
+ by (metis ll llpos abs_of_nonneg)
+ have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
+ by (rule summable_add [OF sum1 sum0])
+ have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
+ using Series.summable_le2 [OF 1 2] by auto
+ also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
(\<Sum>n. e * (1 / 2) ^ Suc n)"
- by (metis 0)
- also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
- by (simp add: eqe)
- finally show ?thesis using Series.summable_le2 [OF 1 2] by auto
+ by (metis 0)
+ also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
+ by (simp add: eqe)
+ finally show ?thesis using Series.summable_le2 [OF 1 2] by auto
qed
def C \<equiv> "(split BB) o nat_to_nat2"
have C: "!!n. C n \<in> sets M"
@@ -822,24 +821,24 @@
done
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
proof (auto simp add: C_def)
- fix x i
- assume x: "x \<in> A i"
- with sbBB [of i] obtain j where "x \<in> BB i j"
- by blast
- thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
- by (metis nat_to_nat2_surj internal_split_def prod.cases
+ fix x i
+ assume x: "x \<in> A i"
+ with sbBB [of i] obtain j where "x \<in> BB i j"
+ by blast
+ thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
+ by (metis nat_to_nat2_surj internal_split_def prod.cases
prod_case_split surj_f_inv_f)
qed
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
by (rule ext) (auto simp add: C_def)
also have "... sums suminf ll"
proof (rule suminf_2dimen)
- show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
- by (force simp add: positive_def)
- show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
- by (force simp add: o_def)
- show "summable ll" using sll
- by auto
+ show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
+ by (force simp add: positive_def)
+ show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
+ by (force simp add: o_def)
+ show "summable ll" using sll
+ by auto
qed
finally have Csums: "(f \<circ> C) sums suminf ll" .
have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
@@ -882,24 +881,24 @@
from inf_measure_close [OF posf e s]
obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
- and l: "l \<le> Inf (measure_set M f s) + e"
- by auto
+ and l: "l \<le> Inf (measure_set M f s) + e"
+ by auto
have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
(f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
- by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
+ by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
have [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
- by (subst additiveD [OF add, symmetric])
- (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
+ by (subst additiveD [OF add, symmetric])
+ (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
have fsumb: "summable (f \<circ> A)"
- by (metis fsums sums_iff)
+ by (metis fsums sums_iff)
{ fix u
- assume u: "u \<in> sets M"
- have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
- by (simp add: positive_imp_pos [OF posf] increasingD [OF inc]
+ assume u: "u \<in> sets M"
+ have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
+ by (simp add: positive_imp_pos [OF posf] increasingD [OF inc]
u Int range_subsetD [OF A])
- have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
+ have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
by (rule summable_comparison_test [OF _ fsumb]) simp
- have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
+ have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
proof (rule Inf_lower)
show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
apply (simp add: measure_set_def)
@@ -920,14 +919,14 @@
and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
\<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
- by (metis Diff lesum top x)+
+ by (metis Diff lesum top x)+
hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
\<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
- by (simp add: x)
+ by (simp add: x)
also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
- by (simp add: x) (simp add: o_def)
+ by (simp add: x) (simp add: o_def)
also have "... \<le> Inf (measure_set M f s) + e"
- by (metis fsums l sums_unique)
+ by (metis fsums l sums_unique)
finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
\<le> Inf (measure_set M f s) + e" .
qed
@@ -940,7 +939,7 @@
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
apply (rule subadditiveD)
apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
- inf_measure_positive inf_measure_countably_subadditive posf inc)
+ inf_measure_positive inf_measure_countably_subadditive posf inc)
apply (auto simp add: subsetD [OF s])
done
finally show ?thesis .
--- a/src/HOL/Probability/Measure.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/Measure.thy Tue Nov 10 06:48:26 2009 -0800
@@ -46,8 +46,8 @@
definition
measurable where
"measurable a b = {f . sigma_algebra a & sigma_algebra b &
- f \<in> (space a -> space b) &
- (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
+ f \<in> (space a -> space b) &
+ (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
definition
measure_preserving where
@@ -258,23 +258,23 @@
fix x
assume x: "x \<in> smallest_ccdi_sets M"
thus "x \<in> C"
- proof (induct rule: smallest_ccdi_sets.induct)
- case (Basic x)
- thus ?case
- by (metis Basic subsetD sbC)
- next
- case (Compl x)
- thus ?case
- by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
- next
- case (Inc A)
- thus ?case
- by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
- next
- case (Disj A)
- thus ?case
- by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
- qed
+ proof (induct rule: smallest_ccdi_sets.induct)
+ case (Basic x)
+ thus ?case
+ by (metis Basic subsetD sbC)
+ next
+ case (Compl x)
+ thus ?case
+ by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
+ next
+ case (Inc A)
+ thus ?case
+ by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
+ next
+ case (Disj A)
+ thus ?case
+ by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
+ qed
qed
finally show ?thesis .
qed
@@ -292,12 +292,12 @@
have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
proof (rule sigma_property_disjoint_lemma)
show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
- by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
+ by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
next
show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
- by (simp add: closed_cdi_def compl inc disj)
+ by (simp add: closed_cdi_def compl inc disj)
(metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
- IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
+ IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
qed
thus ?thesis
by blast
@@ -349,7 +349,7 @@
case 0 show ?case by simp
next
case (Suc m) thus ?case
- by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
+ by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
qed
}
hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
@@ -371,17 +371,17 @@
have "(measure M \<circ> A) n =
setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
proof (induct n)
- case 0 thus ?case by (auto simp add: A0 empty_measure)
+ case 0 thus ?case by (auto simp add: A0 empty_measure)
next
- case (Suc m)
- have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
- by (metis ASuc Un_Diff_cancel Un_absorb1)
- hence "measure M (A (Suc m)) =
+ case (Suc m)
+ have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
+ by (metis ASuc Un_Diff_cancel Un_absorb1)
+ hence "measure M (A (Suc m)) =
measure M (A m) + measure M (A (Suc m) - A m)"
- by (subst measure_additive)
+ by (subst measure_additive)
(auto simp add: measure_additive range_subsetD [OF A])
- with Suc show ?case
- by simp
+ with Suc show ?case
+ by simp
qed
}
hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
@@ -390,13 +390,13 @@
proof (rule UN_finite2_eq [where k=1], simp)
fix i
show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
- proof (induct i)
- case 0 thus ?case by (simp add: A0)
- next
- case (Suc i)
- thus ?case
- by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
- qed
+ proof (induct i)
+ case 0 thus ?case by (simp add: A0)
+ next
+ case (Suc i)
+ thus ?case
+ by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
+ qed
qed
have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
by (metis A Diff range_subsetD)
@@ -461,23 +461,23 @@
assume A: "range A \<subseteq> (vimage f) ` (sets b)"
have "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
proof -
- def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
- {
- fix i
- have "A i \<in> (vimage f) ` (sets b)" using A
- by blast
- hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
- by blast
- hence "B i \<in> sets b \<and> f -` B i = A i"
- by (simp add: B_def) (erule someI_ex)
- } note B = this
- show ?thesis
- proof
- show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
- by (simp add: vimage_UN B)
- show "(\<Union>i. B i) \<in> sets b" using B
- by (auto intro: sigma_algebra.countable_UN [OF b])
- qed
+ def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
+ {
+ fix i
+ have "A i \<in> (vimage f) ` (sets b)" using A
+ by blast
+ hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
+ by blast
+ hence "B i \<in> sets b \<and> f -` B i = A i"
+ by (simp add: B_def) (erule someI_ex)
+ } note B = this
+ show ?thesis
+ proof
+ show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
+ by (simp add: vimage_UN B)
+ show "(\<Union>i. B i) \<in> sets b" using B
+ by (auto intro: sigma_algebra.countable_UN [OF b])
+ qed
qed
}
thus "\<forall>A::nat \<Rightarrow> 'a set.
@@ -496,26 +496,26 @@
fix x
assume "x \<in> sigma_sets X B"
thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
- proof induct
- case (Basic a)
- thus ?case
- by (auto simp add: ba) (metis B subsetD PowD)
+ proof induct
+ case (Basic a)
+ thus ?case
+ by (auto simp add: ba) (metis B subsetD PowD)
next
- case Empty
- thus ?case
- by auto
+ case Empty
+ thus ?case
+ by auto
next
- case (Compl a)
- have [simp]: "f -` X \<inter> space M = space M"
- by (auto simp add: funcset_mem [OF f])
- thus ?case
- by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
- next
- case (Union a)
- thus ?case
- by (simp add: vimage_UN, simp only: UN_extend_simps(4))
- (blast intro: countable_UN)
- qed
+ case (Compl a)
+ have [simp]: "f -` X \<inter> space M = space M"
+ by (auto simp add: funcset_mem [OF f])
+ thus ?case
+ by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+ next
+ case (Union a)
+ thus ?case
+ by (simp add: vimage_UN, simp only: UN_extend_simps(4))
+ (blast intro: countable_UN)
+ qed
qed
thus ?thesis
by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
@@ -553,122 +553,122 @@
show ?thesis using fmp
proof (clarsimp simp add: measure_preserving_def m1 m2)
assume fm: "f \<in> measurable m1 (m a)"
- and mam: "measure_space (m a)"
- and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
+ and mam: "measure_space (m a)"
+ and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
- by (rule subsetD [OF measurable_subset fm])
+ by (rule subsetD [OF measurable_subset fm])
also have "... = measurable m1 m2"
- by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
+ by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
finally have f12: "f \<in> measurable m1 m2" .
hence ffn: "f \<in> space m1 \<rightarrow> space m2"
- by (simp add: measurable_def)
+ by (simp add: measurable_def)
have "space m1 \<subseteq> f -` (space m2)"
- by auto (metis PiE ffn)
+ by auto (metis PiE ffn)
hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
- by blast
+ by blast
{
- fix y
- assume y: "y \<in> sets m2"
- have ama: "algebra (m a)" using mam
- by (simp add: measure_space_def sigma_algebra_iff)
- have spa: "space m2 \<in> a" using algebra.top [OF ama]
- by (simp add: m_def)
- have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
- by (simp add: m_def)
- also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
- proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
- fix x
- assume x: "x \<in> a"
- thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
- by (simp add: meq)
- next
- fix s
- assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
- and s: "s \<in> sigma_sets (space m2) a"
- hence s2: "s \<in> sets m2"
- by (simp add: setsm2)
- thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
+ fix y
+ assume y: "y \<in> sets m2"
+ have ama: "algebra (m a)" using mam
+ by (simp add: measure_space_def sigma_algebra_iff)
+ have spa: "space m2 \<in> a" using algebra.top [OF ama]
+ by (simp add: m_def)
+ have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
+ by (simp add: m_def)
+ also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
+ proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
+ fix x
+ assume x: "x \<in> a"
+ thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
+ by (simp add: meq)
+ next
+ fix s
+ assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
+ and s: "s \<in> sigma_sets (space m2) a"
+ hence s2: "s \<in> sets m2"
+ by (simp add: setsm2)
+ thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
measure m2 (space m2 - s)" using f12
- by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
- measure_space.measure_compl measurable_def)
- (metis fveq meq spa)
- next
- fix A
- assume A0: "A 0 = {}"
- and ASuc: "!!n. A n \<subseteq> A (Suc n)"
- and rA1: "range A \<subseteq>
- {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
- and "range A \<subseteq> sigma_sets (space m2) a"
- hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
- have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
- using rA1 by blast
- have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
- by (simp add: o_def eq1)
- also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
- proof (rule measure_space.measure_countable_increasing [OF m1])
- show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
- using f12 rA2 by (auto simp add: measurable_def)
- show "f -` A 0 \<inter> space m1 = {}" using A0
- by blast
- show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
- using ASuc by auto
- qed
- also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
- by (simp add: vimage_UN)
- finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
- moreover
- have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
- by (rule measure_space.measure_countable_increasing
- [OF m2 rA2, OF A0 ASuc])
- ultimately
- show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+ by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
+ measure_space.measure_compl measurable_def)
+ (metis fveq meq spa)
+ next
+ fix A
+ assume A0: "A 0 = {}"
+ and ASuc: "!!n. A n \<subseteq> A (Suc n)"
+ and rA1: "range A \<subseteq>
+ {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+ and "range A \<subseteq> sigma_sets (space m2) a"
+ hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+ have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+ using rA1 by blast
+ have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
+ by (simp add: o_def eq1)
+ also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ proof (rule measure_space.measure_countable_increasing [OF m1])
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+ using f12 rA2 by (auto simp add: measurable_def)
+ show "f -` A 0 \<inter> space m1 = {}" using A0
+ by blast
+ show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
+ using ASuc by auto
+ qed
+ also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+ by (simp add: vimage_UN)
+ finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
+ moreover
+ have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
+ by (rule measure_space.measure_countable_increasing
+ [OF m2 rA2, OF A0 ASuc])
+ ultimately
+ show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
measure m2 (\<Union>i. A i)"
- by (rule LIMSEQ_unique)
- next
- fix A :: "nat => 'a2 set"
- assume dA: "disjoint_family A"
- and rA1: "range A \<subseteq>
- {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
- and "range A \<subseteq> sigma_sets (space m2) a"
- hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
- hence Um2: "(\<Union>i. A i) \<in> sets m2"
- by (metis range_subsetD setsm2 sigma_sets.Union)
- have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
- using rA1 by blast
- hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
- by (simp add: o_def)
- also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
- proof (rule measure_space.measure_countably_additive [OF m1] )
- show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
- using f12 rA2 by (auto simp add: measurable_def)
- show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
- by (auto simp add: disjoint_family_def)
- show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
- proof (rule sigma_algebra.countable_UN [OF sa1])
- show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
- by (auto simp add: measurable_def)
- qed
- qed
- finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
- with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
- have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
- by (metis sums_unique)
+ by (rule LIMSEQ_unique)
+ next
+ fix A :: "nat => 'a2 set"
+ assume dA: "disjoint_family A"
+ and rA1: "range A \<subseteq>
+ {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+ and "range A \<subseteq> sigma_sets (space m2) a"
+ hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+ hence Um2: "(\<Union>i. A i) \<in> sets m2"
+ by (metis range_subsetD setsm2 sigma_sets.Union)
+ have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+ using rA1 by blast
+ hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
+ by (simp add: o_def)
+ also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ proof (rule measure_space.measure_countably_additive [OF m1] )
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+ using f12 rA2 by (auto simp add: measurable_def)
+ show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
+ by (auto simp add: disjoint_family_def)
+ show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
+ proof (rule sigma_algebra.countable_UN [OF sa1])
+ show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
+ by (auto simp add: measurable_def)
+ qed
+ qed
+ finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
+ with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
+ have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
+ by (metis sums_unique)
- moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
- by (simp add: vimage_UN)
- ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+ moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+ by (simp add: vimage_UN)
+ ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
measure m2 (\<Union>i. A i)"
- by metis
- qed
- finally have "sigma_sets (space m2) a
+ by metis
+ qed
+ finally have "sigma_sets (space m2) a
\<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
- hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
- by (force simp add: setsm2)
+ hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
+ by (force simp add: setsm2)
}
thus "f \<in> measurable m1 m2 \<and>
(\<forall>y\<in>sets m2.
measure m1 (f -` y \<inter> space m1) = measure m2 y)"
- by (blast intro: f12)
+ by (blast intro: f12)
qed
qed
--- a/src/HOL/Probability/Probability.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/Probability.thy Tue Nov 10 06:48:26 2009 -0800
@@ -1,5 +1,5 @@
-theory Probability imports
- Measure
+theory Probability
+imports Measure Borel
begin
end
--- a/src/HOL/Probability/ROOT.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/ROOT.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1,6 +1,1 @@
-(*
- no_document use_thy "ThisTheory";
- use_thy "ThatTheory";
-*)
-
use_thy "Probability";
--- a/src/HOL/Probability/SeriesPlus.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/SeriesPlus.thy Tue Nov 10 06:48:26 2009 -0800
@@ -1,6 +1,5 @@
theory SeriesPlus
imports Complex_Main Nat_Int_Bij
-
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -28,9 +27,9 @@
proof -
fix m
have "0 \<le> suminf (\<lambda>n. f (m,n))"
- by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
+ by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
thus "0 \<le> g m" using fsums [of m]
- by (auto simp add: sums_iff)
+ by (auto simp add: sums_iff)
qed
show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
proof (rule increasing_LIMSEQ, simp add: f_nneg)
@@ -48,14 +47,14 @@
by (rule setsum_mono2) (auto simp add: ij)
also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
- setsum_cartesian_product split_eta)
+ setsum_cartesian_product split_eta)
also have "... \<le> setsum g {0..<Suc i}"
proof (rule setsum_mono, simp add: less_Suc_eq_le)
- fix m
- assume m: "m \<le> i"
- thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
- by (auto simp add: sums_iff)
- (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
+ fix m
+ assume m: "m \<le> i"
+ thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
+ by (auto simp add: sums_iff)
+ (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
qed
finally have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
also have "... \<le> suminf g"
@@ -73,13 +72,13 @@
{ fix m
assume m: "m<N"
hence enneg: "0 < e / (2 * real N)" using e
- by (simp add: zero_less_divide_iff)
+ by (simp add: zero_less_divide_iff)
hence "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
- using fsums [of m] m
+ using fsums [of m] m
by (force simp add: sums_def LIMSEQ_def dist_real_def)
hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)"
- using fsums [of m]
- by (auto simp add: sums_iff)
+ using fsums [of m]
+ by (auto simp add: sums_iff)
(metis abs_diff_less_iff add_less_cancel_right eq_diff_eq')
}
hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
@@ -103,13 +102,13 @@
def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
proof (auto simp add: NIJ_def)
- fix i j
- assume ij:"(i,j) \<in> IJ"
- hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
- by (metis nat_to_nat2_surj surj_f_inv_f)
- thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
- by (rule image_eqI)
- (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
+ fix i j
+ assume ij:"(i,j) \<in> IJ"
+ hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
+ by (metis nat_to_nat2_surj surj_f_inv_f)
+ thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+ by (rule image_eqI)
+ (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
nat_to_nat2_surj surj_f_inv_f)
qed
have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 10 06:48:26 2009 -0800
@@ -235,4 +235,3 @@
by (simp add: sigma_def sigma_sets_subset)
end
-
--- a/src/HOL/Quickcheck.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Quickcheck.thy Tue Nov 10 06:48:26 2009 -0800
@@ -126,6 +126,8 @@
shows "random_aux k = rhs k"
using assms by (rule code_numeral.induct)
+setup {* Quickcheck.setup *}
+
subsection {* the Random-Predicate Monad *}
types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
--- a/src/HOL/Series.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Series.thy Tue Nov 10 06:48:26 2009 -0800
@@ -293,11 +293,11 @@
have "convergent (\<lambda>n. setsum f {0..<n})"
proof (rule Bseq_mono_convergent)
show "Bseq (\<lambda>n. setsum f {0..<n})"
- by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+ by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
(auto simp add: le pos)
next
show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
- by (auto intro: setsum_mono2 pos)
+ by (auto intro: setsum_mono2 pos)
qed
then obtain L where "(%n. setsum f {0..<n}) ----> L"
by (blast dest: convergentD)
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 10 06:48:26 2009 -0800
@@ -6,7 +6,14 @@
"nitpick_ind_intro" to "nitpick_intro"
* Replaced "special_depth" and "skolemize_depth" options by "specialize"
and "skolemize"
+ * Renamed "coalesce_type_vars" to "merge_type_vars"
+ * Optimized Kodkod encoding of datatypes whose constructors don't appear in
+ the formula to falsify
+ * Added support for codatatype view of datatypes
+ * Fixed soundness bug related to sets of sets
* Fixed monotonicity check
+ * Fixed error in display of uncurried constants
+ * Speeded up scope enumeration
Version 1.2.2 (16 Oct 2009)
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1027,12 +1027,10 @@
val err_path = path_for "kodkodi" "err"
val _ = write_problem_file out (map snd indexed_problems)
val _ = File.write_buffer in_path (!in_buf)
- (* (int list -> outcome) -> outcome *)
- fun stopped constr =
- let val nontriv_js = map reindex (snd (read_output_file out_path)) in
- constr (triv_js @ nontriv_js)
- handle Exn.Interrupt => Interrupted NONE
- end
+ (* unit -> unit *)
+ fun remove_temporary_files () =
+ if overlord then ()
+ else List.app File.rm [in_path, out_path, err_path]
in
let
val ms =
@@ -1085,12 +1083,16 @@
else
Normal (ps, js)
end
- in
- if overlord then ()
- else List.app File.rm [in_path, out_path, err_path];
- outcome
- end
- handle Exn.Interrupt => stopped (Interrupted o SOME)
+ in remove_temporary_files (); outcome end
+ handle Exn.Interrupt =>
+ let
+ val nontriv_js = map reindex (snd (read_output_file out_path))
+ in
+ (remove_temporary_files ();
+ Interrupted (SOME (triv_js @ nontriv_js)))
+ handle Exn.Interrupt =>
+ (remove_temporary_files (); Interrupted NONE)
+ end
end
end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 10 06:48:26 2009 -0800
@@ -23,7 +23,7 @@
overlord: bool,
user_axioms: bool option,
assms: bool,
- coalesce_type_vars: bool,
+ merge_type_vars: bool,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -88,7 +88,7 @@
overlord: bool,
user_axioms: bool option,
assms: bool,
- coalesce_type_vars: bool,
+ merge_type_vars: bool,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -137,6 +137,15 @@
Pretty.str (if j = 1 then "." else ";")])
(length ts downto 1) ts))]
+(* unit -> string *)
+fun install_kodkodi_message () =
+ "Nitpick requires the external Java program Kodkodi. To install it, download \
+ \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
+ \directory's full path to \"" ^
+ Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME_USER" ::
+ map Path.basic ["etc", "components"]))) ^ "\"."
+
val max_liberal_delay_ms = 200
val max_liberal_delay_percent = 2
@@ -166,6 +175,9 @@
val has_weaselly_sorts =
exists_type o exists_subtype o is_tfree_with_weaselly_sort
+(* (unit -> string) -> Pretty.T *)
+fun plazy f = Pretty.blk (0, pstrs (f ()))
+
(* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
orig_t =
@@ -175,7 +187,7 @@
val ctxt = Proof.context_of state
val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
- user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
+ user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
show_skolems, show_datatypes, show_consts, evals, formats,
@@ -187,7 +199,7 @@
val pprint =
if auto then
Unsynchronized.change state_ref o Proof.goal_message o K
- o curry Pretty.blk 0 o cons (Pretty.str "") o single
+ o Pretty.chunks o cons (Pretty.str "") o single
o Pretty.mark Markup.hilite
else
priority o Pretty.string_of
@@ -198,9 +210,9 @@
(* string -> unit *)
val print = pprint o curry Pretty.blk 0 o pstrs
(* (unit -> string) -> unit *)
- fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)
- fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)
- fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)
+ val print_m = pprint_m o K o plazy
+ val print_v = pprint_v o K o plazy
+ val print_d = pprint_d o K o plazy
(* unit -> unit *)
fun check_deadline () =
@@ -220,7 +232,7 @@
neg_t
val (assms_t, evals) =
assms_t :: evals
- |> coalesce_type_vars ? coalesce_type_vars_in_terms
+ |> merge_type_vars ? merge_type_vars_in_terms
|> hd pairf tl
val original_max_potential = max_potential
val original_max_genuine = max_genuine
@@ -251,7 +263,8 @@
intro_table = intro_table, ground_thm_table = ground_thm_table,
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
special_funs = Unsynchronized.ref [],
- unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
+ unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
+ constr_cache = Unsynchronized.ref []}
val frees = Term.add_frees assms_t []
val _ = null (Term.add_tvars assms_t [])
orelse raise NOT_SUPPORTED "schematic type variables"
@@ -283,6 +296,21 @@
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
+ val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
+ val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
+ def_ts
+ val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) 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) =
+ List.partition (is_sel o nickname_of) const_names
+ val would_be_genuine = got_all_user_axioms andalso none_true wfs
+(*
+ val _ = List.app (priority o string_for_nut ctxt)
+ (core_u :: def_us @ nondef_us)
+*)
+
val unique_scope = forall (equal 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_free_type_monotonic T =
@@ -298,6 +326,8 @@
not (is_pure_typedef thy T) orelse is_univ_typedef thy T
orelse is_number_type thy T
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+ fun is_datatype_shallow T =
+ not (exists (equal T o domain_type o type_of) sel_names)
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
val (all_dataTs, all_free_Ts) =
@@ -326,7 +356,7 @@
()
val mono_Ts = mono_dataTs @ mono_free_Ts
val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
-
+ val shallow_dataTs = filter is_datatype_shallow mono_dataTs
(*
val _ = priority "Monotonic datatypes:"
val _ = List.app (priority o string_for_type ctxt) mono_dataTs
@@ -338,19 +368,6 @@
val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
*)
- val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
- val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
- def_ts
- val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
- nondef_ts
- val (free_names, const_names) =
- fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
- val nonsel_names = filter_out (is_sel o nickname_of) const_names
- val would_be_genuine = got_all_user_axioms andalso none_true wfs
-(*
- val _ = List.app (priority o string_for_nut ctxt)
- (core_u :: def_us @ nondef_us)
-*)
val need_incremental = Int.max (max_potential, max_genuine) >= 2
val effective_sat_solver =
if sat_solver <> "smart" then
@@ -627,15 +644,7 @@
case Kodkod.solve_any_problem overlord deadline max_threads
max_solutions (map fst problems) of
Kodkod.NotInstalled =>
- (print_m (fn () =>
- "Nitpick requires the external Java program Kodkodi. \
- \To install it, download the package from Isabelle's \
- \web page and add the \"kodkodi-x.y.z\" directory's \
- \full path to \"" ^
- Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME" ::
- (map Path.basic ["etc", "components"])))) ^
- "\".");
+ (print_m install_kodkodi_message;
(max_potential, max_genuine, donno + 1))
| Kodkod.Normal ([], unsat_js) =>
(update_checked_problems problems unsat_js;
@@ -778,11 +787,9 @@
case scope_count (do_filter (!generated_problems)) scope of
0 => I
| n =>
- if scope_count (do_filter (these (!checked_problems)))
- scope = n then
- Integer.add 1
- else
- I) (!generated_scopes) 0
+ scope_count (do_filter (these (!checked_problems)))
+ scope = n
+ ? Integer.add 1) (!generated_scopes) 0
in
"Nitpick " ^ did_so_and_so ^
(if is_some (!checked_problems) andalso total > 0 then
@@ -812,8 +819,19 @@
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
end
- val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
- iters_assigns bisim_depths mono_Ts nonmono_Ts
+ val (skipped, the_scopes) =
+ all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
+ bisim_depths mono_Ts nonmono_Ts shallow_dataTs
+ val _ = if skipped > 0 then
+ print_m (fn () => "Too many scopes. Dropping " ^
+ string_of_int skipped ^ " scope" ^
+ plural_s skipped ^
+ ". (Consider using \"mono\" or \
+ \\"merge_type_vars\" to prevent this.)")
+ else
+ ()
+ val _ = scopes := the_scopes
+
val batches = batch_list batch_size (!scopes)
val outcome_code =
(run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
@@ -839,16 +857,21 @@
(* Proof.state -> params -> bool -> term -> string * Proof.state *)
fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
auto orig_assm_ts orig_t =
- let
- val deadline = Option.map (curry Time.+ (Time.now ())) timeout
- val outcome as (outcome_code, _) =
- time_limit (if debug then NONE else timeout)
- (pick_them_nits_in_term deadline state params auto orig_assm_ts)
- orig_t
- in
- if expect = "" orelse outcome_code = expect then outcome
- else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
- end
+ if getenv "KODKODI" = "" then
+ (if auto then ()
+ else warning (Pretty.string_of (plazy install_kodkodi_message));
+ ("unknown", state))
+ else
+ let
+ val deadline = Option.map (curry Time.+ (Time.now ())) timeout
+ val outcome as (outcome_code, _) =
+ time_limit (if debug then NONE else timeout)
+ (pick_them_nits_in_term deadline state params auto orig_assm_ts)
+ orig_t
+ in
+ if expect = "" orelse outcome_code = expect then outcome
+ else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ end
(* Proof.state -> params -> thm -> int -> string * Proof.state *)
fun pick_nits_in_subgoal state params auto subgoal =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 10 06:48:26 2009 -0800
@@ -40,7 +40,8 @@
skolems: (string * string list) list Unsynchronized.ref,
special_funs: special_fun list Unsynchronized.ref,
unrolled_preds: unrolled list Unsynchronized.ref,
- wf_cache: wf_cache Unsynchronized.ref}
+ wf_cache: wf_cache Unsynchronized.ref,
+ constr_cache: (typ * styp list) list Unsynchronized.ref}
val name_sep : string
val numeral_prefix : string
@@ -86,6 +87,7 @@
val is_abs_fun : theory -> styp -> bool
val is_rep_fun : theory -> styp -> bool
val is_constr : theory -> styp -> bool
+ val is_stale_constr : theory -> styp -> bool
val is_sel : string -> bool
val discr_for_constr : styp -> styp
val num_sels_for_constr_type : typ -> int
@@ -100,16 +102,16 @@
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 : theory -> typ -> styp list
+ val datatype_constrs : extended_context -> typ -> styp list
val boxed_datatype_constrs : extended_context -> typ -> styp list
- val num_datatype_constrs : theory -> typ -> int
+ val num_datatype_constrs : extended_context -> typ -> int
val constr_name_for_sel_like : string -> string
val boxed_constr_for_sel : extended_context -> styp -> styp
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_precise_card_of_type :
- theory -> int -> int -> (typ * int) list -> typ -> int
- val is_finite_type : theory -> typ -> bool
+ extended_context -> int -> int -> (typ * int) list -> typ -> int
+ val is_finite_type : extended_context -> 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
@@ -125,7 +127,7 @@
val is_inductive_pred : extended_context -> styp -> bool
val is_constr_pattern_lhs : theory -> term -> bool
val is_constr_pattern_formula : theory -> term -> bool
- val coalesce_type_vars_in_terms : term list -> term list
+ 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 format_type : int list -> int list -> typ -> typ
@@ -177,9 +179,10 @@
skolems: (string * string list) list Unsynchronized.ref,
special_funs: special_fun list Unsynchronized.ref,
unrolled_preds: unrolled list Unsynchronized.ref,
- wf_cache: wf_cache Unsynchronized.ref}
+ wf_cache: wf_cache Unsynchronized.ref,
+ constr_cache: (typ * styp list) list Unsynchronized.ref}
-structure TheoryData = Theory_Data(
+structure Data = Theory_Data(
type T = {frac_types: (string * (string * string) list) list,
codatatypes: (string * (string * styp list)) list}
val empty = {frac_types = [], codatatypes = []}
@@ -312,7 +315,7 @@
(@{const_name times_int_inst.times_int}, 0),
(@{const_name div_int_inst.div_int}, 0),
(@{const_name div_int_inst.mod_int}, 0),
- (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
+ (@{const_name uminus_int_inst.uminus_int}, 0),
(@{const_name ord_int_inst.less_int}, 2),
(@{const_name ord_int_inst.less_eq_int}, 2),
(@{const_name Tha}, 1),
@@ -392,8 +395,7 @@
val is_record_type = not o null o Record.dest_recTs
(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
- not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy))
- s)))
+ not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
| is_frac_type _ _ = false
fun is_number_type thy = is_integer_type orf is_frac_type thy
@@ -469,16 +471,16 @@
(* string -> (string * string) list -> theory -> theory *)
fun register_frac_type frac_s ersaetze thy =
let
- val {frac_types, codatatypes} = TheoryData.get thy
+ val {frac_types, codatatypes} = Data.get thy
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
- in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
+ in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
(* string -> theory -> theory *)
fun unregister_frac_type frac_s = register_frac_type frac_s []
(* typ -> string -> styp list -> theory -> theory *)
fun register_codatatype co_T case_name constr_xs thy =
let
- val {frac_types, codatatypes} = TheoryData.get thy
+ val {frac_types, codatatypes} = Data.get thy
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
val (co_s, co_Ts) = dest_Type co_T
val _ =
@@ -486,7 +488,7 @@
else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
codatatypes
- in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
+ in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
(* typ -> theory -> theory *)
fun unregister_codatatype co_T = register_codatatype co_T "" []
@@ -520,7 +522,7 @@
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
fun is_codatatype thy (T as Type (s, _)) =
- not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s
+ not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
|> Option.map snd |> these))
| is_codatatype _ _ = false
fun is_pure_typedef thy (T as Type (s, _)) =
@@ -592,7 +594,7 @@
(* theory -> styp -> bool *)
fun is_coconstr thy (s, T) =
let
- val {codatatypes, ...} = TheoryData.get thy
+ val {codatatypes, ...} = Data.get thy
val co_T = body_type T
val co_s = dest_Type co_T |> fst
in
@@ -609,9 +611,13 @@
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
orelse is_coconstr thy x
end
+fun is_stale_constr thy (x as (_, T)) =
+ is_codatatype thy (body_type T) andalso is_constr_like thy x
+ andalso not (is_coconstr thy x)
fun is_constr thy (x as (_, T)) =
is_constr_like thy x
andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
+ andalso not (is_stale_constr thy x)
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
@@ -726,41 +732,51 @@
fun suc_const T = Const (@{const_name Suc}, T --> T)
(* theory -> typ -> styp list *)
-fun datatype_constrs thy (T as Type (s, Ts)) =
- if is_datatype thy T then
- case Datatype.get_info thy s of
- SOME {index, descr, ...} =>
- let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
- map (fn (s', Us) =>
- (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
- constrs
- end
- | NONE =>
- case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
- SOME (_, xs' as (_ :: _)) =>
- map (apsnd (repair_constr_type thy T)) xs'
- | _ =>
- if is_record_type T then
- let
- val s' = unsuffix Record.ext_typeN s ^ Record.extN
- val T' = (Record.get_extT_fields thy T
- |> apsnd single |> uncurry append |> map snd) ---> T
- in [(s', T')] end
- else case typedef_info thy s of
- SOME {abs_type, rep_type, Abs_name, ...} =>
- [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
- | NONE =>
- if T = @{typ ind} then
- [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
- else
- []
- else
- []
- | datatype_constrs _ _ = []
+fun uncached_datatype_constrs thy (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'
+ | _ =>
+ if is_datatype thy T then
+ case Datatype.get_info thy s of
+ SOME {index, descr, ...} =>
+ let
+ val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
+ in
+ map (fn (s', Us) =>
+ (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
+ ---> T)) constrs
+ end
+ | NONE =>
+ if is_record_type T then
+ let
+ val s' = unsuffix Record.ext_typeN s ^ Record.extN
+ val T' = (Record.get_extT_fields thy T
+ |> apsnd single |> uncurry append |> map snd) ---> T
+ in [(s', T')] end
+ else case typedef_info thy s of
+ SOME {abs_type, rep_type, Abs_name, ...} =>
+ [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
+ | NONE =>
+ if T = @{typ ind} then
+ [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
+ else
+ []
+ else
+ [])
+ | uncached_datatype_constrs _ _ = []
(* extended_context -> typ -> styp list *)
-fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) =
- map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy
-(* theory -> typ -> int *)
+fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
+ T =
+ case AList.lookup (op =) (!constr_cache) T of
+ SOME xs => xs
+ | NONE =>
+ let val xs = uncached_datatype_constrs thy 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 *)
val num_datatype_constrs = length oo datatype_constrs
(* string -> string *)
@@ -773,26 +789,26 @@
AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
|> the |> pair s
end
-(* theory -> styp -> term *)
-fun discr_term_for_constr thy (x as (s, T)) =
+(* extended_context -> styp -> term *)
+fun discr_term_for_constr ext_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 thy dataT >= 2 then
+ else if num_datatype_constrs ext_ctxt dataT >= 2 then
Const (discr_for_constr x)
else
Abs (Name.uu, dataT, @{const True})
end
-(* theory -> styp -> term -> term *)
-fun discriminate_value thy (x as (_, T)) t =
+(* extended_context -> styp -> term -> term *)
+fun discriminate_value (ext_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 thy x, t)
- | _ => betapply (discr_term_for_constr thy x, t)
+ else betapply (discr_term_for_constr ext_ctxt x, t)
+ | _ => betapply (discr_term_for_constr ext_ctxt x, t)
(* styp -> term -> term *)
fun nth_arg_sel_term_for_constr (x as (s, T)) n =
@@ -841,8 +857,8 @@
| _ => list_comb (Const x, args)
end
-(* theory -> typ -> term -> term *)
-fun constr_expand thy T t =
+(* 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 ())
@@ -854,7 +870,7 @@
(@{const_name Pair}, [T1, T2] ---> T)
end
else
- datatype_constrs thy T |> the_single
+ datatype_constrs ext_ctxt T |> the_single
val arg_Ts = binder_types T'
in
list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
@@ -896,8 +912,8 @@
card_of_type asgns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
-(* theory -> int -> (typ * int) list -> typ -> int *)
-fun bounded_precise_card_of_type thy max default_card asgns T =
+(* extended_context -> int -> (typ * int) list -> typ -> int *)
+fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
let
(* typ list -> typ -> int *)
fun aux avoid T =
@@ -927,12 +943,12 @@
| @{typ bool} => 2
| @{typ unit} => 1
| Type _ =>
- (case datatype_constrs thy T of
+ (case datatype_constrs ext_ctxt T of
[] => if is_integer_type T then 0 else raise SAME ()
| constrs =>
let
val constr_cards =
- datatype_constrs thy T
+ datatype_constrs ext_ctxt T
|> map (Integer.prod o map (aux (T :: avoid)) o binder_types
o snd)
in
@@ -943,8 +959,9 @@
handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
in Int.min (max, aux [] T) end
-(* theory -> typ -> bool *)
-fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 []
+(* extended_context -> typ -> bool *)
+fun is_finite_type ext_ctxt =
+ not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -965,6 +982,14 @@
(* indexname * typ -> term -> term *)
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
+(* theory -> string -> bool *)
+fun is_funky_typedef_name thy s =
+ s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
+ @{type_name int}]
+ orelse is_frac_type thy (Type (s, []))
+(* theory -> term -> bool *)
+fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
+ | is_funky_typedef _ _ = false
(* term -> bool *)
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
$ Const (@{const_name TYPE}, _)) = true
@@ -975,9 +1000,7 @@
| is_typedef_axiom thy boring
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
- boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
- orelse is_frac_type thy (Type (s, [])))
- andalso is_typedef thy s
+ boring <> is_funky_typedef_name thy s andalso is_typedef thy s
| is_typedef_axiom _ _ _ = false
(* Distinguishes between (1) constant definition axioms, (2) type arity and
@@ -1015,24 +1038,6 @@
| do_eq _ = false
in do_eq end
-(* This table is not pretty. A better approach would be to avoid expanding the
- operators to their low-level definitions, but this would require dealing with
- overloading. *)
-val built_in_built_in_defs =
- [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
- @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
- @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
- @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
- @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
- @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
- @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
- @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
- @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
- @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
- @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
- @{thm zero_nat_inst.zero_nat}]
- |> map prop_of
-
(* theory -> term list * term list * term list *)
fun all_axioms_of thy =
let
@@ -1053,8 +1058,7 @@
val (built_in_nondefs, user_nondefs) =
List.partition (is_typedef_axiom thy false) user_nondefs
|>> append built_in_nondefs
- val defs = built_in_built_in_defs @
- (thy |> PureThy.all_thms_of
+ val defs = (thy |> PureThy.all_thms_of
|> filter (equal Thm.definitionK o Thm.get_kind o snd)
|> map (prop_of o snd) |> filter is_plain_definition) @
user_defs @ built_in_defs
@@ -1185,7 +1189,7 @@
cons (case_name, AList.lookup (op =) descr index
|> the |> #3 |> length))
(Datatype.get_all thy) [] @
- map (apsnd length o snd) (#codatatypes (TheoryData.get thy))
+ map (apsnd length o snd) (#codatatypes (Data.get thy))
(* Proof.context -> term list -> const_table *)
fun const_def_table ctxt ts =
@@ -1221,7 +1225,7 @@
(* theory -> (string * string) list *)
fun ersatz_table thy =
- fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table
+ fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
(* const_table Unsynchronized.ref -> string -> term list -> unit *)
fun add_simps simp_table s eqs =
@@ -1238,7 +1242,7 @@
if s = s' then
ys |> (if AList.defined (op =) ys T' then
I
- else
+ else
cons (T', Refute.monomorphic_term
(Sign.typ_match thy (T', T) Vartab.empty) t)
handle Type.TYPE_MATCH => I
@@ -1292,29 +1296,26 @@
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-(* theory -> typ -> int * styp -> term -> term *)
-fun add_constr_case thy res_T (j, x) res_t =
+(* extended_context -> typ -> int * styp -> term -> term *)
+fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
- $ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t
-(* theory -> typ -> typ -> term *)
-fun optimized_case_def thy dataT res_T =
+ $ discriminate_value ext_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 =
let
- val xs = datatype_constrs thy dataT
+ val xs = datatype_constrs ext_ctxt dataT
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
val (xs', x) = split_last xs
in
constr_case_body thy (1, x)
- |> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')
+ |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-val redefined_in_Nitpick_thy =
- [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
- @{const_name list_size}]
-
-(* theory -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get thy s rec_T res_T t =
- let val constr_x = the_single (datatype_constrs thy rec_T) in
+(* 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 = the_single (datatype_constrs ext_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
Type (_, Ts as _ :: _) =>
@@ -1323,16 +1324,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 thy s rec_T' res_T
+ |> optimized_record_get ext_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
-(* theory -> string -> typ -> term -> term -> term *)
-fun optimized_record_update thy s rec_T fun_t rec_t =
+(* extended_context -> string -> typ -> term -> term -> term *)
+fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
let
- val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T)
+ val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
val Ts = binder_types constr_T
val n = length Ts
val special_j = no_of_record_field thy s rec_T
@@ -1343,7 +1344,7 @@
if j = special_j then
betapply (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
- optimized_record_update thy s
+ optimized_record_update ext_ctxt s
(rec_T |> dest_Type |> snd |> List.last) fun_t t
else
t
@@ -1381,7 +1382,6 @@
(is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
andf (not o has_trivial_definition thy def_table)
- andf (not o member (op =) redefined_in_Nitpick_thy o fst)
(* term * term -> term *)
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1488,7 +1488,7 @@
val (const, ts) =
if is_built_in_const fast_descrs x then
if s = @{const_name finite} then
- if is_finite_type thy (domain_type T) then
+ if is_finite_type ext_ctxt (domain_type T) then
(Abs ("A", domain_type T, @{const True}), ts)
else case ts of
[Const (@{const_name UNIV}, _)] => (@{const False}, [])
@@ -1501,24 +1501,26 @@
val (dataT, res_T) = nth_range_type n T
|> domain_type pairf range_type
in
- (optimized_case_def thy dataT res_T
+ (optimized_case_def ext_ctxt dataT res_T
|> do_term (depth + 1) Ts, ts)
end
| _ =>
if is_constr thy x then
(Const x, ts)
+ else if is_stale_constr thy x then
+ raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
+ \(\"" ^ s ^ "\")")
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 thy s (domain_type T)
+ | _ => (optimized_record_get ext_ctxt s (domain_type T)
(range_type T) (hd ts), tl ts)
else if is_record_update thy x then
case length ts of
- 2 => (optimized_record_update thy (unsuffix Record.updateN s)
- (nth_range_type 2 T)
- (do_term depth Ts (hd ts))
- (do_term depth Ts (nth ts 1)),
- [])
+ 2 => (optimized_record_update ext_ctxt
+ (unsuffix Record.updateN s) (nth_range_type 2 T)
+ (do_term depth Ts (hd ts))
+ (do_term depth Ts (nth ts 1)), [])
| n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
else if is_rep_fun thy x then
let val x' = mate_of_rep_fun thy x in
@@ -1545,10 +1547,10 @@
in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
in do_term 0 [] end
-(* theory -> typ -> term list *)
-fun codatatype_bisim_axioms thy T =
+(* extended_context -> typ -> term list *)
+fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
let
- val xs = datatype_constrs thy T
+ val xs = datatype_constrs ext_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)
@@ -1571,14 +1573,14 @@
let
val arg_Ts = binder_types T
val core_t =
- discriminate_value thy x y_var ::
+ discriminate_value ext_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 thy T bool_T,
+ $ (betapplys (optimized_case_def ext_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)
@@ -1629,6 +1631,7 @@
(tac ctxt (auto_tac (clasimpset_of ctxt))))
#> the #> Goal.finish ctxt) goal
+val max_cached_wfs = 100
val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
val cached_wf_props : (term * bool) list Unsynchronized.ref =
Unsynchronized.ref []
@@ -1637,11 +1640,11 @@
ScnpReconstruct.sizechange_tac]
(* extended_context -> const_table -> styp -> bool *)
-fun is_is_well_founded_inductive_pred
+fun uncached_is_well_founded_inductive_pred
({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
: extended_context) (x as (_, T)) =
case def_props_for_const thy fast_descrs intro_table x of
- [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
+ [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
| intro_ts =>
(case map (triple_for_intro_rule thy x) intro_ts
@@ -1662,8 +1665,11 @@
else
()
in
- if tac_timeout = (!cached_timeout) then ()
- else (cached_wf_props := []; cached_timeout := tac_timeout);
+ if tac_timeout = (!cached_timeout)
+ andalso length (!cached_wf_props) < max_cached_wfs then
+ ()
+ else
+ (cached_wf_props := []; cached_timeout := tac_timeout);
case AList.lookup (op =) (!cached_wf_props) prop of
SOME wf => wf
| NONE =>
@@ -1690,7 +1696,7 @@
| NONE =>
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val wf = is_is_well_founded_inductive_pred ext_ctxt x
+ val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
in
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
end
@@ -1878,9 +1884,7 @@
(* extended_context -> styp -> term list *)
fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
psimp_table, ...}) (x as (s, _)) =
- if s mem redefined_in_Nitpick_thy then
- []
- else case def_props_for_const thy fast_descrs (!simp_table) x of
+ 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]
| psimps => psimps)
@@ -1889,7 +1893,7 @@
val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
(* term list -> term list *)
-fun coalesce_type_vars_in_terms ts =
+fun merge_type_vars_in_terms ts =
let
(* typ -> (sort * string) list -> (sort * string) list *)
fun add_type (TFree (s, S)) table =
@@ -2002,8 +2006,8 @@
seen, concl)
end
-(* theory -> bool -> term -> term *)
-fun destroy_pulled_out_constrs thy axiom t =
+(* extended_context -> bool -> term -> term *)
+fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
let
(* styp -> int *)
val num_occs_of_var =
@@ -2037,7 +2041,7 @@
andalso (not careful orelse not (is_Var t1)
orelse String.isPrefix val_var_prefix
(fst (fst (dest_Var t1)))) then
- discriminate_value thy x t1 ::
+ discriminate_value ext_ctxt x t1 ::
map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
|> foldr1 s_conj
|> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
@@ -2564,7 +2568,6 @@
t
else
let
- (* FIXME: strong enough in the face of user-defined axioms? *)
val blacklist = if depth = 0 then []
else case term_under_def t of Const x => [x] | _ => []
(* term list -> typ list -> term -> term *)
@@ -2727,7 +2730,7 @@
| (Type (new_s, new_Ts as [new_T1, new_T2]),
Type (old_s, old_Ts as [old_T1, old_T2])) =>
if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
- case constr_expand thy old_T t of
+ 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
@@ -3030,14 +3033,16 @@
else if is_abs_fun thy x then
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> fold (add_def_axiom depth)
- (nondef_props_for_const thy true
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_def_axiom depth)
+ (nondef_props_for_const thy true
(extra_table def_table s) x)
else if is_rep_fun thy x then
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> fold (add_def_axiom depth)
- (nondef_props_for_const thy true
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_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))
@@ -3068,7 +3073,7 @@
#> (if is_pure_typedef thy T then
fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
else if max_bisim_depth >= 0 andalso is_codatatype thy T then
- fold (add_def_axiom depth) (codatatype_bisim_axioms thy T)
+ fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
else
I)
(* int -> typ -> sort -> accumulator -> accumulator *)
@@ -3312,7 +3317,7 @@
#> maybe_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 thy def)
+ #> destroy_pulled_out_constrs ext_ctxt def)
#> curry_assms
#> destroy_universal_equalities
#> destroy_existential_equalities thy
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 06:48:26 2009 -0800
@@ -10,7 +10,9 @@
sig
type params = Nitpick.params
+ val auto: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
+ val setup : theory -> theory
end
structure Nitpick_Isar : NITPICK_ISAR =
@@ -22,6 +24,14 @@
open Nitpick_Nut
open Nitpick
+val auto = Unsynchronized.ref false;
+
+val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
+ (setmp_CRITICAL auto false
+ (fn () => Preferences.bool_pref auto
+ "auto-nitpick"
+ "Whether to run Nitpick automatically.") ())
+
type raw_param = string * string list
val default_default_params =
@@ -33,12 +43,11 @@
("wf", ["smart"]),
("sat_solver", ["smart"]),
("batch_size", ["smart"]),
- ("auto", ["false"]),
("blocking", ["true"]),
("falsify", ["true"]),
("user_axioms", ["smart"]),
("assms", ["true"]),
- ("coalesce_type_vars", ["false"]),
+ ("merge_type_vars", ["false"]),
("destroy_constrs", ["true"]),
("specialize", ["true"]),
("skolemize", ["true"]),
@@ -47,7 +56,6 @@
("fast_descrs", ["true"]),
("peephole_optim", ["true"]),
("timeout", ["30 s"]),
- ("auto_timeout", ["5 s"]),
("tac_timeout", ["500 ms"]),
("sym_break", ["20"]),
("sharing_depth", ["3"]),
@@ -70,12 +78,11 @@
[("dont_box", "box"),
("non_mono", "mono"),
("non_wf", "wf"),
- ("no_auto", "auto"),
("non_blocking", "blocking"),
("satisfy", "falsify"),
("no_user_axioms", "user_axioms"),
("no_assms", "assms"),
- ("dont_coalesce_type_vars", "coalesce_type_vars"),
+ ("dont_merge_type_vars", "merge_type_vars"),
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_skolemize", "skolemize"),
@@ -125,30 +132,22 @@
| _ => value)
| NONE => (name, value)
-structure TheoryData = Theory_Data(
- type T = {params: raw_param list, registered_auto: bool}
- val empty = {params = rev default_default_params, registered_auto = false}
+structure Data = Theory_Data(
+ type T = {params: raw_param list}
+ val empty = {params = rev default_default_params}
+ val copy = I
val extend = I
- fun merge ({params = ps1, registered_auto = a1},
- {params = ps2, registered_auto = a2}) : T =
- {params = AList.merge (op =) (op =) (ps1, ps2),
- registered_auto = a1 orelse a2})
+ fun merge ({params = ps1}, {params = ps2}) =
+ {params = AList.merge (op =) (op =) (ps1, ps2)})
(* raw_param -> theory -> theory *)
fun set_default_raw_param param thy =
- let val {params, registered_auto} = TheoryData.get thy in
- TheoryData.put
- {params = AList.update (op =) (unnegate_raw_param param) params,
- registered_auto = registered_auto} thy
+ let val {params} = Data.get thy in
+ Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
+ thy
end
(* theory -> raw_param list *)
-val default_raw_params = #params o TheoryData.get
-
-(* theory -> theory *)
-fun set_registered_auto thy =
- TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
-(* theory -> bool *)
-val is_registered_auto = #registered_auto o TheoryData.get
+val default_raw_params = #params o Data.get
(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -304,7 +303,7 @@
val overlord = lookup_bool "overlord"
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
- val coalesce_type_vars = lookup_bool "coalesce_type_vars"
+ val merge_type_vars = lookup_bool "merge_type_vars"
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val skolemize = lookup_bool "skolemize"
@@ -312,8 +311,7 @@
val uncurry = lookup_bool "uncurry"
val fast_descrs = lookup_bool "fast_descrs"
val peephole_optim = lookup_bool "peephole_optim"
- val timeout = if auto then lookup_time "auto_timeout"
- else lookup_time "timeout"
+ val timeout = if auto then NONE else lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
val sym_break = Int.max (0, lookup_int "sym_break")
val sharing_depth = Int.max (1, lookup_int "sharing_depth")
@@ -325,8 +323,8 @@
val show_consts = show_all orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val evals = lookup_term_list "eval"
- val max_potential = if auto then 0
- else Int.max (0, lookup_int "max_potential")
+ val max_potential =
+ if auto then 0 else Int.max (0, lookup_int "max_potential")
val max_genuine = Int.max (0, lookup_int "max_genuine")
val check_potential = lookup_bool "check_potential"
val check_genuine = lookup_bool "check_genuine"
@@ -340,7 +338,7 @@
monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
user_axioms = user_axioms, assms = assms,
- coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
+ merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
star_linear_preds = star_linear_preds, uncurry = uncurry,
fast_descrs = fast_descrs, peephole_optim = peephole_optim,
@@ -411,7 +409,7 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
+(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
fun pick_nits override_params auto subgoal state =
let
val thy = Proof.theory_of state
@@ -420,70 +418,49 @@
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
- (* unit -> Proof.state *)
+ (* unit -> bool * Proof.state *)
fun go () =
- (if auto then perhaps o try
- else if debug then fn f => fn x => f x
- else handle_exceptions ctxt)
- (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
- state
+ (false, state)
+ |> (if auto then perhaps o try
+ else if debug then fn f => fn x => f x
+ else handle_exceptions ctxt)
+ (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
+ |>> equal "genuine")
in
- if auto orelse blocking then
- go ()
- else
- (SimpleThread.fork true (fn () => (go (); ()));
- state)
+ if auto orelse blocking then go ()
+ else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
end
(* (TableFun().key * string list) list option * int option
-> Toplevel.transition -> Toplevel.transition *)
fun nitpick_trans (opt_params, opt_subgoal) =
Toplevel.keep (K ()
- o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
+ o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
o Toplevel.proof_of)
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* bool -> Proof.state -> Proof.state *)
-fun pick_nits_auto interactive state =
- let val thy = Proof.theory_of state in
- ((interactive andalso not (!Toplevel.quiet)
- andalso the (general_lookup_bool false (default_raw_params thy)
- (SOME false) "auto"))
- ? pick_nits [] true 0) state
- end
-
-(* theory -> theory *)
-fun register_auto thy =
- (not (is_registered_auto thy)
- ? (set_registered_auto
- #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
- thy
-
(* (TableFun().key * string) list option -> Toplevel.transition
-> Toplevel.transition *)
fun nitpick_params_trans opt_params =
Toplevel.theory
- (fn thy =>
- let val thy = fold set_default_raw_param (these opt_params) thy in
- writeln ("Default parameters for Nitpick:\n" ^
- (case rev (default_raw_params thy) of
- [] => "none"
- | params =>
- (map check_raw_param params;
- params |> map string_for_raw_param |> sort_strings
- |> cat_lines)));
- register_auto thy
- end)
+ (fold set_default_raw_param (these opt_params)
+ #> tap (fn thy =>
+ writeln ("Default parameters for Nitpick:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
(* OuterParse.token list
-> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-fun scan_nitpick_command tokens =
- (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
-fun scan_nitpick_params_command tokens =
- scan_params tokens |>> nitpick_params_trans
+val scan_nitpick_command =
+ (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
+val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Kodkod"
@@ -492,4 +469,10 @@
"set and display the default parameters for Nitpick"
OuterKeyword.thy_decl scan_nitpick_params_command
+(* Proof.state -> bool * Proof.state *)
+fun auto_nitpick state =
+ if not (!auto) then (false, state) else pick_nits [] true 1 state
+
+val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
+
end;
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 10 06:48:26 2009 -0800
@@ -343,7 +343,6 @@
(* The type constraint below is a workaround for a Poly/ML bug. *)
-(* FIXME: clean up *)
(* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *)
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
R r =
@@ -371,7 +370,6 @@
Kodkod.True
end
fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
- (* FIXME: weird test *)
if not (is_opt_rep R) then
if r = suc_rel then
Kodkod.False
@@ -582,9 +580,9 @@
val schema = atom_schema_of_rep R1
val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
|> rel_expr_from_rel_expr kk R1' R1
+ val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
in
- #kk_comprehension kk (decls_for_atom_schema ~1 schema)
- (#kk_subset kk r1 r)
+ #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
end
| Func (Unit, (Atom (2, j0))) =>
#kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1)))
@@ -618,7 +616,7 @@
val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
in
#kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
- (#kk_rel_eq kk r2 r3)
+ (#kk_subset kk r2 r3)
end
end
| _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
@@ -643,10 +641,11 @@
(length ran_schema))
|> rel_expr_from_rel_expr kk R2' R2
val app = kk_n_fold_join kk true R1' R2' dom_prod r
+ val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk
in
#kk_comprehension kk (decls_for_atom_schema ~1
(dom_schema @ ran_schema))
- (#kk_subset kk ran_prod app)
+ (kk_xeq ran_prod app)
end
| _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
[old_R, Func (R1, R2)])
@@ -716,8 +715,8 @@
(* extended_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 ext_ctxt kk rel_table dtypes
- ({typ, constrs, ...} : dtype_spec) =
+ | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = 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
o #const) constrs)
@@ -884,12 +883,13 @@
(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> Kodkod.formula list *)
-fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
- let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
- partition_axioms_for_datatype j0 kk rel_table dtype
- end
+fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
+ | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
+ let val j0 = offset_of_type ofs typ in
+ sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
+ partition_axioms_for_datatype j0 kk rel_table dtype
+ end
(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
-> dtype_spec list -> Kodkod.formula list *)
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 10 06:48:26 2009 -0800
@@ -133,12 +133,14 @@
| aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
in apsnd (pairself rev) o aux end
-(* typ -> term -> term list * term *)
-fun break_in_two (Type ("*", [T1, T2]))
- (Const (@{const_name Pair}, _) $ t1 $ t2) =
- break_in_two T2 t2 |>> cons t1
- | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
- | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
+(* typ -> typ -> typ -> term -> term * term *)
+fun break_in_two T T1 T2 t =
+ let
+ val ps = HOLogic.flat_tupleT_paths T
+ val cut = length (HOLogic.strip_tupleT T1)
+ val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
+ val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
+ in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
(* typ -> term -> term -> term *)
fun pair_up (Type ("*", [T1', T2']))
(t1 as Const (@{const_name Pair},
@@ -153,12 +155,12 @@
(* typ -> typ -> typ -> term -> term *)
fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
let
- (* typ -> typ -> typ -> term -> term *)
- fun do_curry T1a T1b T2 t =
+ (* typ -> typ -> typ -> typ -> term -> term *)
+ fun do_curry T1 T1a T1b T2 t =
let
val (maybe_opt, ps) = dest_plain_fun t
val ps =
- ps |>> map (break_in_two T1a #>> mk_flat_tuple T1a)
+ ps |>> map (break_in_two T1 T1a T1b)
|> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
|> AList.coalesce (op =)
|> map (apsnd (make_plain_fun maybe_opt T1b T2))
@@ -185,7 +187,7 @@
case factor_out_types T1' T1 of
((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
| ((_, NONE), (T1a, SOME T1b)) =>
- t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
+ t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
| ((T1a', SOME T1b'), (_, NONE)) =>
t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
| _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
@@ -329,7 +331,8 @@
HOLogic.mk_number nat_T j
else case datatype_spec datatypes T of
NONE => atom for_auto T j
- | SOME {constrs, co, ...} =>
+ | SOME {shallow = true, ...} => atom for_auto T j
+ | SOME {co, constrs, ...} =>
let
(* styp -> int list *)
fun tuples_for_const (s, T) =
@@ -527,7 +530,7 @@
evals, case_names, def_table, nondef_table, user_nondefs,
simp_table, psimp_table, intro_table, ground_thm_table,
ersatz_table, skolems, special_funs, unrolled_preds,
- wf_cache},
+ wf_cache, constr_cache},
card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
free_names sel_names nonsel_names rel_table bounds =
let
@@ -545,7 +548,7 @@
intro_table = intro_table, ground_thm_table = ground_thm_table,
ersatz_table = ersatz_table, skolems = skolems,
special_funs = special_funs, unrolled_preds = unrolled_preds,
- wf_cache = wf_cache}
+ wf_cache = wf_cache, constr_cache = constr_cache}
val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
(* typ -> typ -> rep -> int list list -> term *)
@@ -585,8 +588,7 @@
|> term_for_rep T T' (rep_of name)
in
Pretty.block (Pretty.breaks
- [(setmp_CRITICAL show_question_marks false o setmp_show_all_types)
- (Syntax.pretty_term ctxt) t1,
+ [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
Pretty.str oper, Syntax.pretty_term ctxt t2])
end
(* dtype_spec -> Pretty.T *)
@@ -600,11 +602,12 @@
(* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- precise = false, constrs = []}]
+ precise = false, shallow = false, constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
- List.partition #co datatypes
- ||> append (integer_datatype nat_T @ integer_datatype int_T)
+ datatypes |> filter_out #shallow
+ |> List.partition #co
+ ||> append (integer_datatype nat_T @ integer_datatype int_T)
val block_of_datatypes =
if show_datatypes andalso not (null datatypes) then
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 10 06:48:26 2009 -0800
@@ -215,7 +215,7 @@
| NONE =>
let
val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
- val xs = datatype_constrs thy T
+ val xs = datatype_constrs ext_ctxt T
val (all_Cs, constr_Cs) =
fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
let
@@ -505,7 +505,7 @@
map prop_for_comp comps @
map prop_for_sign_expr sexps)
in
- case silence (SatSolver.invoke_solver "dpll") prop of
+ case SatSolver.invoke_solver "dpll" prop of
SatSolver.SATISFIABLE asgns =>
SOME (literals_from_assignments max_var asgns lits
|> tap print_solution)
@@ -708,7 +708,7 @@
(CFun (left_set_C, S Neg,
CFun (right_set_C, S Neg, left_set_C)),
(gamma, cset |> add_ctype_is_right_unique right_set_C
- (* FIXME: |> add_is_sub_ctype right_set_C left_set_C *)))
+ |> add_is_sub_ctype right_set_C left_set_C))
end
| @{const_name ord_fun_inst.less_eq_fun} =>
do_fragile_set_operation T accum
@@ -784,10 +784,8 @@
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
- (* term -> accumulator -> ctype * accumulator *)
- val do_term = consider_term cdata
(* term -> accumulator -> accumulator *)
- val do_boolean_term = snd oo do_term
+ val do_term = snd oo consider_term cdata
(* sign -> term -> accumulator -> accumulator *)
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
| do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
@@ -812,11 +810,8 @@
(* term -> term -> accumulator *)
fun do_equals t1 t2 =
case sn of
- Pos => do_boolean_term t accum
- | Neg => let
- val (C1, accum) = do_term t1 accum
- val (C2, accum) = do_term t2 accum
- in accum (* FIXME: ||> add_ctypes_equal C1 C2 *) end
+ Pos => do_term t accum
+ | Neg => fold do_term [t1, t2] accum
in
case t of
Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
@@ -844,10 +839,10 @@
| @{const "op -->"} $ t1 $ t2 =>
accum |> do_contra_formula t1 |> do_co_formula t2
| Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
- accum |> do_boolean_term t1 |> do_co_formula t2 |> do_co_formula t3
+ accum |> do_term t1 |> fold do_co_formula [t2, t3]
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_co_formula (betapply (t2, t1)) accum
- | _ => do_boolean_term t accum
+ | _ => do_term t accum
end
|> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
Syntax.string_of_term ctxt t ^
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 10 06:48:26 2009 -0800
@@ -749,8 +749,9 @@
(~1 upto num_sels_for_constr_type T - 1)
(* scope -> dtype_spec -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) =
- fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
+fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
+ | choose_rep_for_sels_of_datatype scope {constrs, ...} =
+ fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
(* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
@@ -1058,11 +1059,12 @@
Op2 (And, bool_T, Any,
case u2 of
Op2 (Lambda, _, _, u21, u22) =>
- if num_occs_in_nut u21 u22 = 0 then (* FIXME: move to s_op2 *)
+ if num_occs_in_nut u21 u22 = 0 then
u22
else
Op2 (Apply, bool_T, Any, u2, x_u)
| _ => Op2 (Apply, bool_T, Any, u2, x_u),
+
Op2 (Eq, bool_T, Any, y_u,
Op2 (Apply, ran_T, Any, u1, x_u)))))
|> sub
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Nov 10 06:48:26 2009 -0800
@@ -22,6 +22,7 @@
card: int,
co: bool,
precise: bool,
+ shallow: bool,
constrs: constr_spec list}
type scope = {
@@ -44,7 +45,7 @@
val all_scopes :
extended_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
- -> int list -> typ list -> typ list -> scope list
+ -> int list -> typ list -> typ list -> typ list -> int * scope list
end;
structure Nitpick_Scope : NITPICK_SCOPE =
@@ -66,6 +67,7 @@
card: int,
co: bool,
precise: bool,
+ shallow: bool,
constrs: constr_spec list}
type scope = {
@@ -126,7 +128,7 @@
card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
|> List.partition (is_fp_iterator_type o fst)
val (unimportant_card_asgns, important_card_asgns) =
- card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst)
+ card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
val cards =
map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
string_of_int k)
@@ -222,33 +224,31 @@
SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr)
handle TERM ("lookup_const_ints_assign", _) => NONE
-(* Proof.context -> (typ option * int list) list
+(* extended_context -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ -> block *)
-fun block_for_type ctxt cards_asgns maxes_asgns iters_asgns bisim_depths T =
- let val thy = ProofContext.theory_of ctxt in
- if T = @{typ bisim_iterator} then
- [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
- else if is_fp_iterator_type T then
- [(Card T, map (fn k => Int.max (0, k) + 1)
- (lookup_const_ints_assign thy iters_asgns
- (const_for_iterator_type T)))]
- else
- (Card T, lookup_type_ints_assign thy cards_asgns T) ::
- (case datatype_constrs thy T of
- [_] => []
- | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
- end
+fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns
+ bisim_depths T =
+ if T = @{typ bisim_iterator} then
+ [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
+ else if is_fp_iterator_type T then
+ [(Card T, map (fn k => Int.max (0, k) + 1)
+ (lookup_const_ints_assign thy iters_asgns
+ (const_for_iterator_type T)))]
+ else
+ (Card T, lookup_type_ints_assign thy cards_asgns T) ::
+ (case datatype_constrs ext_ctxt T of
+ [_] => []
+ | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
-(* Proof.context -> (typ option * int list) list
+(* extended_context -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> block list *)
-fun blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
+fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
mono_Ts nonmono_Ts =
let
- val thy = ProofContext.theory_of ctxt
(* typ -> block *)
- val block_for = block_for_type ctxt cards_asgns maxes_asgns iters_asgns
+ val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns
bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
@@ -289,15 +289,15 @@
type scope_desc = (typ * int) list * (styp * int) list
-(* theory -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign thy (card_asgns, max_asgns) (T, k) =
- case datatype_constrs thy T of
+(* extended_context -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) =
+ case datatype_constrs ext_ctxt T of
[] => false
| xs =>
let
val precise_cards =
map (Integer.prod
- o map (bounded_precise_card_of_type thy k 0 card_asgns)
+ o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns)
o binder_types o snd) xs
val maxes = map (constr_max max_asgns) xs
(* int -> int -> int *)
@@ -317,18 +317,19 @@
end
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
-(* theory -> scope_desc -> bool *)
-fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =
- exists (is_surely_inconsistent_card_assign thy desc) card_asgns
+(* extended_context -> scope_desc -> bool *)
+fun is_surely_inconsistent_scope_description ext_ctxt
+ (desc as (card_asgns, _)) =
+ exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns
-(* theory -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns thy (card_asgns, max_asgns) =
+(* extended_context -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) =
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) :: asgns) =
- (if is_surely_inconsistent_scope_description thy
+ (if is_surely_inconsistent_scope_description ext_ctxt
((T, k) :: seen, max_asgns) then
raise SAME ()
else
@@ -360,12 +361,12 @@
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* theory -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination thy blocks columns =
+(* extended_context -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
let
val (card_asgns, max_asgns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_asgns = repair_card_assigns thy (card_asgns, max_asgns) |> the
+ val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the
in
SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns)
end
@@ -431,16 +432,17 @@
explicit_max = max, total = total} :: constrs
end
-(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
+(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
(desc as (card_asgns, _)) (T, card) =
let
+ val shallow = T mem shallow_dataTs
val co = is_codatatype thy T
val xs = boxed_datatype_constrs ext_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition (equal true) self_recs |> pairself length
- val precise = (card = bounded_precise_card_of_type thy (card + 1) 0
+ val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
card_asgns T)
(* int -> int *)
fun sum_dom_cards max =
@@ -448,14 +450,18 @@
val constrs =
fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
num_non_self_recs) (self_recs ~~ xs) []
- in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
+ in
+ {typ = T, card = card, co = co, precise = precise, shallow = shallow,
+ constrs = constrs}
+ end
-(* extended_context -> int -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
+(* extended_context -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
(desc as (card_asgns, _)) =
let
- val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
- (filter (is_datatype thy o fst) card_asgns)
+ val datatypes =
+ map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
+ (filter (is_datatype thy o fst) card_asgns)
val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
in
{ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
@@ -476,23 +482,27 @@
| fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) =
(NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns
+val max_scopes = 4096
val distinct_threshold = 512
(* extended_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
- -> typ list -> typ list -> scope list *)
-fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
- iters_asgns bisim_depths mono_Ts nonmono_Ts =
+ -> typ list -> typ list -> typ list -> int * scope list *)
+fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns
+ iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
let
val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
- val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
+ val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns
bisim_depths mono_Ts nonmono_Ts
val ranks = map rank_of_block blocks
- val descs = all_combinations_ordered_smartly (map (rpair 0) ranks)
- |> map_filter (scope_descriptor_from_combination thy blocks)
+ val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
+ val head = Library.take (max_scopes, all)
+ val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
+ head
in
- descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor ext_ctxt sym_break)
+ (length all - length head,
+ descs |> length descs <= distinct_threshold ? distinct (op =)
+ |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs))
end
end;
--- a/src/HOL/Tools/inductive.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/inductive.ML Tue Nov 10 06:48:26 2009 -0800
@@ -665,7 +665,8 @@
|> LocalTheory.conceal
|> LocalTheory.define Thm.internalK
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- (Attrib.empty_binding, fold_rev lambda params
+ ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
+ fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
||> LocalTheory.restore_naming lthy;
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
--- a/src/HOL/Tools/sat_solver.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/Tools/sat_solver.ML Tue Nov 10 06:48:26 2009 -0800
@@ -546,7 +546,7 @@
(if name="dpll" orelse name="enumerate" then
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
else
- tracing ("Using SAT solver " ^ quote name ^ "."));
+ ());
(* apply 'solver' to 'fm' *)
solver fm
handle SatSolver.NOT_CONFIGURED => loop solvers
--- a/src/HOL/ex/ROOT.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/HOL/ex/ROOT.ML Tue Nov 10 06:48:26 2009 -0800
@@ -67,6 +67,9 @@
"Landau"
];
+HTML.with_charset "utf-8" (no_document use_thys)
+ ["Hebrew", "Chinese", "Serbian"];
+
(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
"Hilbert_Classical";
@@ -74,12 +77,10 @@
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";
-(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
-try use_thy "SAT_Examples";
-
(*requires zChaff (or some other reasonably fast SAT solver)*)
if getenv "ZCHAFF_HOME" = "" then ()
else use_thy "Sudoku";
-HTML.with_charset "utf-8" (no_document use_thys)
- ["Hebrew", "Chinese", "Serbian"];
+(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
+(*global side-effects ahead!*)
+try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)
--- a/src/Pure/IsaMakefile Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/IsaMakefile Tue Nov 10 06:48:26 2009 -0800
@@ -27,9 +27,10 @@
ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
- ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \
+ ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \
+ ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \
+ ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
ML-Systems/timing.ML ML-Systems/time_limit.ML \
ML-Systems/universal.ML ML-Systems/unsynchronized.ML
--- a/src/Pure/Isar/locale.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/Isar/locale.ML Tue Nov 10 06:48:26 2009 -0800
@@ -72,8 +72,6 @@
morphism -> theory -> theory
val amend_registration: string * morphism -> morphism * bool ->
morphism -> theory -> theory
- val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
- val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
val add_dependency: string -> string * morphism -> morphism -> theory -> theory
(* Diagnostic *)
@@ -239,7 +237,7 @@
in
-(* Note that while identifiers always have the external (exported) view, activate_dep is
+(* Note that while identifiers always have the external (exported) view, activate_dep
is presented with the internal view. *)
fun roundup thy activate_dep export (name, morph) (marked, input) =
@@ -481,36 +479,6 @@
end
end;
-fun amend_registration_legacy morph (name, base_morph) thy =
- (* legacy, never modify base morphism *)
- let
- val regs = Registrations.get thy |> fst |> map fst;
- val base = instance_of thy name base_morph;
- fun match (name', (morph', _)) =
- name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
- val i = find_index match (rev regs);
- val _ =
- if i = ~1 then error ("No registration of locale " ^
- quote (extern thy name) ^ " and parameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
- else ();
- in
- Registrations.map ((apfst o nth_map (length regs - 1 - i))
- (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
- end;
-
-fun add_registration_eqs (dep, proto_morph) eqns export thy =
- let
- val morph = if null eqns then proto_morph
- else proto_morph $> Element.eq_morphism thy eqns;
- in
- (get_idents (Context.Theory thy), thy)
- |> roundup thy (fn (dep', morph') =>
- Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
- |> snd
- |> Context.theory_map (activate_facts (dep, morph $> export))
- end;
-
(*** Dependencies ***)
--- a/src/Pure/Isar/proof_context.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/Isar/proof_context.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1032,7 +1032,10 @@
(Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
fun target_notation add mode args phi =
- let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
+ let
+ val args' = args |> map_filter (fn (t, mx) =>
+ let val t' = Morphism.term phi t
+ in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
end;
--- a/src/Pure/Isar/theory_target.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/Isar/theory_target.ML Tue Nov 10 06:48:26 2009 -0800
@@ -190,9 +190,7 @@
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
val arg = (b', Term.close_schematic_term rhs');
-(* val similar_body = Type.similar_types (rhs, rhs'); *)
- val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
- val similar_body = same_shape (rhs, rhs');
+ val same_shape = Term.aconv_untyped (rhs, rhs');
(* FIXME workaround based on educated guess *)
val prefix' = Binding.prefix_of b';
val class_global =
@@ -200,12 +198,12 @@
not (null prefix') andalso
fst (snd (split_last prefix')) = Class_Target.class_prefix target;
in
- not (is_class andalso (similar_body orelse class_global)) ?
+ not (is_class andalso (same_shape orelse class_global)) ?
(Context.mapping_result
(Sign.add_abbrev PrintMode.internal arg)
(ProofContext.add_abbrev PrintMode.internal arg)
#-> (fn (lhs' as Const (d, _), _) =>
- similar_body ?
+ same_shape ?
(Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
-Runtime compilation for Poly/ML 5.3.
+Runtime compilation for Poly/ML 5.3.0.
*)
local
--- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
-Extra toplevel pretty-printing for Poly/ML 5.3.
+Extra toplevel pretty-printing for Poly/ML 5.3.0.
*)
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
@@ -15,3 +15,29 @@
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
| SOME (Exn.Result y) => pretty (y, depth)));
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
+ let
+ open PolyML;
+ val from_ML = Pretty.from_ML o pretty_ml;
+ fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
+ fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
+ fun prt_term parens dp (t as _ $ _) =
+ op :: (strip_comb t)
+ |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+ |> Pretty.separate " $"
+ |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
+ | prt_term _ dp (Abs (x, T, body)) =
+ prt_apps "Abs"
+ [from_ML (prettyRepresentation (x, dp - 1)),
+ from_ML (prettyRepresentation (T, dp - 2)),
+ prt_term false (dp - 3) body]
+ | prt_term _ dp (Const const) =
+ prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
+ | prt_term _ dp (Free free) =
+ prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
+ | prt_term _ dp (Var var) =
+ prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
+ | prt_term _ dp (Bound i) =
+ prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
+ in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,28 @@
+(* Title: Pure/ML-Systems/polyml-5.2.1.ML
+
+Compatibility wrapper for Poly/ML 5.2.1.
+*)
+
+use "ML-Systems/unsynchronized.ML";
+
+open Thread;
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+end;
+
+fun reraise exn = raise exn;
+
+use "ML-Systems/polyml_common.ML";
+use "ML-Systems/multithreading_polyml.ML";
+
+val pointer_eq = PolyML.pointerEq;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
+use "ML-Systems/compiler_polyml-5.2.ML";
+use "ML-Systems/pp_polyml.ML";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.2.ML Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,30 @@
+(* Title: Pure/ML-Systems/polyml-5.2.ML
+
+Compatibility wrapper for Poly/ML 5.2.
+*)
+
+use "ML-Systems/unsynchronized.ML";
+
+open Thread;
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+end;
+
+fun reraise exn = raise exn;
+
+use "ML-Systems/polyml_common.ML";
+
+use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/multithreading.ML";
+
+val pointer_eq = PolyML.pointerEq;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
+use "ML-Systems/compiler_polyml-5.2.ML";
+use "ML-Systems/pp_polyml.ML";
+
--- a/src/Pure/ML-Systems/polyml-experimental.ML Tue Nov 10 06:47:55 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-experimental.ML
-
-Compatibility wrapper for Poly/ML 5.3.
-*)
-
-use "ML-Systems/unsynchronized.ML";
-
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn =
- (case PolyML.exceptionLocation exn of
- NONE => raise exn
- | SOME location => PolyML.raiseWithLocation (exn, location));
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/multithreading_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.3.ML";
-PolyML.Compiler.reportUnreferencedIds := true;
-
-
-(* toplevel pretty printing *)
-
-val pretty_ml =
- let
- fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
- let
- fun property name default =
- (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
- SOME (PolyML.ContextProperty (_, b)) => b
- | NONE => default);
- val bg = property "begin" "";
- val en = property "end" "";
- val len' = property "length" len;
- in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
- | convert len (PolyML.PrettyString s) =
- ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
- | convert _ (PolyML.PrettyBreak (wd, _)) =
- ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
- in convert "" end;
-
-fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
- let val context =
- (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
- (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
- in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
- | ml_pretty (ML_Pretty.String (s, len)) =
- if len = size s then PolyML.PrettyString s
- else PolyML.PrettyBlock
- (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
- | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
- | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
-
-fun toplevel_pp context (_: string list) pp =
- use_text context (1, "pp") false
- ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
-
--- a/src/Pure/ML-Systems/polyml.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/ML-Systems/polyml.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/polyml.ML
-Compatibility wrapper for Poly/ML 5.2 and 5.2.1.
+Compatibility wrapper for Poly/ML 5.3.0.
*)
use "ML-Systems/unsynchronized.ML";
@@ -14,18 +14,55 @@
val global = PolyML.globalNameSpace;
end;
-fun reraise exn = raise exn;
+fun reraise exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => raise exn
+ | SOME location => PolyML.raiseWithLocation (exn, location));
use "ML-Systems/polyml_common.ML";
-
-if ml_system = "polyml-5.2"
-then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML")
-else use "ML-Systems/multithreading_polyml.ML";
+use "ML-Systems/multithreading_polyml.ML";
val pointer_eq = PolyML.pointerEq;
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
+use "ML-Systems/compiler_polyml-5.3.ML";
+PolyML.Compiler.reportUnreferencedIds := true;
+
+
+(* toplevel pretty printing *)
+val pretty_ml =
+ let
+ fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
+ let
+ fun property name default =
+ (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+ SOME (PolyML.ContextProperty (_, b)) => b
+ | NONE => default);
+ val bg = property "begin" "";
+ val en = property "end" "";
+ val len' = property "length" len;
+ in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+ | convert len (PolyML.PrettyString s) =
+ ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+ | convert _ (PolyML.PrettyBreak (wd, _)) =
+ ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+ in convert "" end;
+
+fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+ let val context =
+ (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+ (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+ in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
+ | ml_pretty (ML_Pretty.String (s, len)) =
+ if len = size s then PolyML.PrettyString s
+ else PolyML.PrettyBlock
+ (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
+ | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
+ | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
+
+fun toplevel_pp context (_: string list) pp =
+ use_text context (1, "pp") false
+ ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Nov 10 06:48:26 2009 -0800
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_compiler_polyml-5.3.ML
Author: Makarius
-Advanced runtime compilation for Poly/ML 5.3 (SVN 839).
+Advanced runtime compilation for Poly/ML 5.3.0.
*)
signature ML_COMPILER =
--- a/src/Pure/ROOT.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/ROOT.ML Tue Nov 10 06:48:26 2009 -0800
@@ -169,7 +169,7 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "Isar/runtime.ML";
-if ml_system = "polyml-experimental"
+if ml_system = "polyml-5.3.0"
then use "ML/ml_compiler_polyml-5.3.ML"
else use "ML/ml_compiler.ML";
use "ML/ml_context.ML";
--- a/src/Pure/pure_setup.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/pure_setup.ML Tue Nov 10 06:48:26 2009 -0800
@@ -33,7 +33,7 @@
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
-if ml_system = "polyml-experimental"
+if ml_system = "polyml-5.3.0"
then use "ML-Systems/install_pp_polyml-5.3.ML"
else if String.isPrefix "polyml" ml_system
then use "ML-Systems/install_pp_polyml.ML"
--- a/src/Pure/term.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/term.ML Tue Nov 10 06:48:26 2009 -0800
@@ -146,6 +146,7 @@
val eq_ix: indexname * indexname -> bool
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
val eq_var: (indexname * typ) * (indexname * typ) -> bool
+ val aconv_untyped: term * term -> bool
val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
val match_bvars: (term * term) * (string * string) list -> (string * string) list
@@ -524,6 +525,17 @@
| (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
| (a1, a2) => a1 = a2);
+fun aconv_untyped (tm1, tm2) =
+ pointer_eq (tm1, tm2) orelse
+ (case (tm1, tm2) of
+ (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
+ | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
+ | (Const (a, _), Const (b, _)) => a = b
+ | (Free (x, _), Free (y, _)) => x = y
+ | (Var (xi, _), Var (yj, _)) => xi = yj
+ | (Bound i, Bound j) => i = j
+ | _ => false);
+
(*A fast unification filter: true unless the two terms cannot be unified.
Terms must be NORMAL. Treats all Vars as distinct. *)
--- a/src/Pure/type.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Pure/type.ML Tue Nov 10 06:48:26 2009 -0800
@@ -42,7 +42,6 @@
(*special treatment of type vars*)
val strip_sorts: typ -> typ
- val similar_types: term * term -> bool
val no_tvars: typ -> typ
val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
val freeze_thaw_type: typ -> typ * (typ -> typ)
@@ -236,23 +235,6 @@
| strip_sorts (TVar (xi, _)) = TVar (xi, []);
-(* equivalence up to renaming of atomic types *)
-
-local
-
-fun standard_types t =
- let
- val Ts = fold_types (fold_atyps (insert (op =))) t [];
- val Ts' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length Ts));
- in map_types (map_atyps (perhaps (AList.lookup (op =) (Ts ~~ Ts')))) t end;
-
-in
-
-val similar_types = op aconv o pairself (Term.map_types strip_sorts o standard_types);
-
-end;
-
-
(* no_tvars *)
fun no_tvars T =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Auto_Counterexample.thy Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,15 @@
+(* Title: Tools/Auto_Counterexample.thy
+ Author: Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+header {* Counterexample Search Unit *}
+
+theory Auto_Counterexample
+imports Pure
+uses
+ "~~/src/Tools/auto_counterexample.ML"
+begin
+
+end
--- a/src/Tools/Code_Generator.thy Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Tools/Code_Generator.thy Tue Nov 10 06:48:26 2009 -0800
@@ -5,7 +5,7 @@
header {* Loading the code generator modules *}
theory Code_Generator
-imports Pure
+imports Auto_Counterexample
uses
"~~/src/Tools/value.ML"
"~~/src/Tools/quickcheck.ML"
@@ -25,4 +25,4 @@
#> Nbe.setup
*}
-end
\ No newline at end of file
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_counterexample.ML Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,59 @@
+(* Title: Tools/auto_counterexample.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+signature AUTO_COUNTEREXAMPLE =
+sig
+ val time_limit: int Unsynchronized.ref
+
+ val register_tool :
+ string * (Proof.state -> bool * Proof.state) -> theory -> theory
+end;
+
+structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+struct
+
+(* preferences *)
+
+val time_limit = Unsynchronized.ref 2500
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.nat_pref time_limit
+ "auto-counterexample-time-limit"
+ "Time limit for automatic counterexample search (in milliseconds).")
+
+
+(* configuration *)
+
+structure Data = TheoryDataFun(
+ type T = (string * (Proof.state -> bool * Proof.state)) list
+ val empty = []
+ val copy = I
+ val extend = I
+ fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
+)
+
+val register_tool = Data.map o AList.update (op =)
+
+
+(* automatic testing *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
+ case !time_limit of
+ 0 => state
+ | ms =>
+ TimeLimit.timeLimit (Time.fromMilliseconds ms)
+ (fn () =>
+ if interact andalso not (!Toplevel.quiet) then
+ fold_rev (fn (_, tool) => fn (true, state) => (true, state)
+ | (false, state) => tool state)
+ (Data.get (Proof.theory_of state)) (false, state) |> snd
+ else
+ state) ()
+ handle TimeLimit.TimeOut =>
+ (warning "Automatic counterexample search timed out."; state)))
+
+end;
--- a/src/Tools/quickcheck.ML Tue Nov 10 06:47:55 2009 -0800
+++ b/src/Tools/quickcheck.ML Tue Nov 10 06:48:26 2009 -0800
@@ -7,10 +7,10 @@
signature QUICKCHECK =
sig
val auto: bool Unsynchronized.ref
- val auto_time_limit: int Unsynchronized.ref
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+ val setup: theory -> theory
val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
end;
@@ -20,20 +20,13 @@
(* preferences *)
val auto = Unsynchronized.ref false;
-val auto_time_limit = Unsynchronized.ref 2500;
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
(setmp_CRITICAL auto true (fn () =>
Preferences.bool_pref auto
"auto-quickcheck"
- "Whether to enable quickcheck automatically.") ());
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref auto_time_limit
- "auto-quickcheck-time-limit"
- "Time limit for automatic quickcheck (in milliseconds).");
+ "Whether to run Quickcheck automatically.") ());
(* quickcheck configuration -- default parameters, test generators *)
@@ -159,28 +152,26 @@
(* automatic testing *)
-val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
- let
- val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.all_assms_of ctxt);
- val Test_Params { size, iterations, default_type } =
- (snd o Data.get o Proof.theory_of) state;
- fun test () =
- let
- val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
- (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
- in
- case res of
- NONE => state
- | SOME NONE => state
- | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
- end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
- in
- if int andalso !auto andalso not (!Toplevel.quiet)
- then test ()
- else state
- end));
+fun auto_quickcheck state =
+ if not (!auto) then
+ (false, state)
+ else
+ let
+ val ctxt = Proof.context_of state;
+ val assms = map term_of (Assumption.all_assms_of ctxt);
+ val Test_Params { size, iterations, default_type } =
+ (snd o Data.get o Proof.theory_of) state;
+ val res =
+ try (test_goal true NONE size iterations default_type [] 1 assms) state;
+ in
+ case res of
+ NONE => (false, state)
+ | SOME NONE => (false, state)
+ | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
+ end
+
+val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
(* Isar commands *)
@@ -251,4 +242,3 @@
val auto_quickcheck = Quickcheck.auto;
-val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;