--- a/Admin/linktest Wed Jun 02 13:18:21 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-#!/usr/bin/env bash
-#
-# leightweight link checker for the isabelle website
-
-
-PRG=`basename "$0"`
-
-usage()
-{
- echo
- echo "Usage: $PRG URL"
- echo
- exit 1
-}
-
-fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-url="$1"
-if [ -z "$url" ]
-then
- usage;
-fi
-
-type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
-
-mkdir -p /tmp/isa_linktest
-dir=$(pwd)
-cd /tmp/isa_linktest
-exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
- --delete-after \
- "$url" \
- 2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
-cd "$dir"
-rm -rf /tmp/isa_linktest
--- a/NEWS Wed Jun 02 13:18:21 2010 +0200
+++ b/NEWS Wed Jun 02 13:18:48 2010 +0200
@@ -425,8 +425,10 @@
- Improved efficiency of "destroy_constrs" optimization.
- Fixed soundness bugs related to "destroy_constrs" optimization and
record getters.
- - Fixed soundness bug related to higher-order constructors
+ - Fixed soundness bug related to higher-order constructors.
+ - Fixed soundness bug when "full_descrs" is enabled.
- Improved precision of set constructs.
+ - Added "atoms" option.
- Added cache to speed up repeated Kodkod invocations on the same
problems.
- Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
@@ -434,6 +436,7 @@
"SAT4J_Light". INCOMPATIBILITY.
- Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
+ - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
* Moved the SMT binding into the HOL image.
--- a/doc-src/Nitpick/nitpick.tex Wed Jun 02 13:18:21 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Wed Jun 02 13:18:48 2010 +0200
@@ -1897,6 +1897,8 @@
\begin{enum}
\item[$\bullet$] \qtybf{string}: A string.
+\item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
+(e.g., ``\textit{ichi ni san}'').
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
@@ -2256,6 +2258,19 @@
counterexamples. This option suffers from an ``observer effect'': Nitpick might
find different counterexamples for different values of this option.
+\oparg{atoms}{type}{string\_list}
+Specifies the names to use to refer to the atoms of the given type. By default,
+Nitpick generates names of the form $a_1, \ldots, a_n$, where $a$ is the first
+letter of the type's name.
+
+\opnodefault{atoms}{string\_list}
+Specifies the default names to use to refer to atoms of any type. For example,
+to call the three atoms of type ${'}a$ \textit{ichi}, \textit{ni}, and
+\textit{san} instead of $a_1$, $a_2$, $a_3$, specify the option
+``\textit{atoms}~${'}a$ = \textit{ichi~ni~san}''. The default names can be
+overridden on a per-type basis using the \textit{atoms}~\qty{type} option
+described above.
+
\oparg{format}{term}{int\_seq}
Specifies how to uncurry the value displayed for a variable or constant.
Uncurrying sometimes increases the readability of the output for high-arity
@@ -2563,21 +2578,6 @@
\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
-\flushitem{\textit{nitpick\_intro}}
-
-\nopagebreak
-This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
-For predicates defined using the \textbf{inductive} or \textbf{coinductive}
-command, this corresponds to the \textit{intros} rules. The introduction rules
-must be of the form
-
-\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
-\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
-\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
-
-where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
-optional monotonic operator. The order of the assumptions is irrelevant.
-
\flushitem{\textit{nitpick\_choice\_spec}}
\nopagebreak
@@ -2626,9 +2626,8 @@
``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
\postw
-Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
-the above rules. Nitpick then uses the \textit{lfp}-based definition in
-conjunction with these rules. To override this, we can specify an alternative
+By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
+the introduction rules. To override this, we can specify an alternative
definition as follows:
\prew
--- a/src/HOL/HOL.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/HOL.thy Wed Jun 02 13:18:48 2010 +0200
@@ -2033,11 +2033,6 @@
val name = "nitpick_psimp"
val description = "partial equational specification of constants as needed by Nitpick"
)
-structure Nitpick_Intros = Named_Thms
-(
- val name = "nitpick_intro"
- val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
-)
structure Nitpick_Choice_Specs = Named_Thms
(
val name = "nitpick_choice_spec"
@@ -2049,7 +2044,6 @@
Nitpick_Defs.setup
#> Nitpick_Simps.setup
#> Nitpick_Psimps.setup
- #> Nitpick_Intros.setup
#> Nitpick_Choice_Specs.setup
*}
--- a/src/HOL/Library/Multiset.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 02 13:18:48 2010 +0200
@@ -1711,7 +1711,8 @@
| NONE => [Const (maybe_name, elem_T --> elem_T) $ t]
in
case maps elems_for (all_values elem_T) @
- (if maybe_opt then [Const (Nitpick_Model.unrep, elem_T)] else []) of
+ (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)]
+ else []) of
[] => Const (@{const_name zero_class.zero}, T)
| ts => foldl1 (fn (t1, t2) =>
Const (@{const_name plus_class.plus}, T --> T --> T)
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Jun 02 13:18:48 2010 +0200
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+nitpick_params [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI,
+ max_threads = 1, timeout = 60 s]
subsection {* Curry in a Hurry *}
@@ -1051,6 +1051,56 @@
nitpick [expect = none]
sorry
+nitpick_params [full_descrs, max_potential = 1]
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = potential] (* unfortunate *)
+oops
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
+sorry
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
+sorry
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 14, expect = genuine]
+oops
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
+nitpick [card nat = 14, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
+sorry
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 14, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
+nitpick [card nat = 14, expect = none]
+sorry
+
+nitpick_params [fast_descrs, max_potential = 0]
+
subsection {* Destructors and Recursors *}
lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Jun 02 13:18:48 2010 +0200
@@ -15,7 +15,7 @@
exception FAIL
val subst = []
-val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1
+val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1
val def_table = Nitpick_HOL.const_def_table @{context} subst defs
val hol_ctxt : Nitpick_HOL.hol_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Jun 02 13:18:48 2010 +0200
@@ -64,7 +64,7 @@
oops
lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [fast_descrs (* ### FIXME *), expect = none]
+nitpick [expect = none]
sorry
lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
--- a/src/HOL/Product_Type.thy Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Product_Type.thy Wed Jun 02 13:18:48 2010 +0200
@@ -856,8 +856,22 @@
lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
by (simp add: prod_fun_def)
-lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
- by (rule ext) auto
+lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
+by (cases x, auto)
+
+lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
+by (cases x, auto)
+
+lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
+by (rule ext) auto
+
+lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
+by (rule ext) auto
+
+
+lemma prod_fun_compose:
+ "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
+by (rule ext) auto
lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
by (rule ext) auto
@@ -878,6 +892,7 @@
apply blast
done
+
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
"apfst f = prod_fun f id"
@@ -1098,6 +1113,66 @@
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
by (auto, case_tac "f x", auto)
+text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
+
+lemma prod_fun_inj_on:
+ assumes "inj_on f A" and "inj_on g B"
+ shows "inj_on (prod_fun f g) (A \<times> B)"
+proof (rule inj_onI)
+ fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
+ assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
+ assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
+ assume "prod_fun f g x = prod_fun f g y"
+ hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
+ hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
+ with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
+ have "fst x = fst y" by (auto dest:dest:inj_onD)
+ moreover from `prod_fun f g x = prod_fun f g y`
+ have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
+ hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
+ with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
+ have "snd x = snd y" by (auto dest:dest:inj_onD)
+ ultimately show "x = y" by(rule prod_eqI)
+qed
+
+lemma prod_fun_surj:
+ assumes "surj f" and "surj g"
+ shows "surj (prod_fun f g)"
+unfolding surj_def
+proof
+ fix y :: "'b \<times> 'd"
+ from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
+ moreover
+ from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
+ ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
+ thus "\<exists>x. y = prod_fun f g x" by auto
+qed
+
+lemma prod_fun_surj_on:
+ assumes "f ` A = A'" and "g ` B = B'"
+ shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
+unfolding image_def
+proof(rule set_ext,rule iffI)
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
+ then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
+ from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
+ moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
+ ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
+ with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
+next
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
+ from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
+ then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
+ moreover from `image g B = B'` and `snd x \<in> B'`
+ obtain b where "b \<in> B" and "snd x = g b" by auto
+ ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
+ moreover from `a \<in> A` and `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
+ ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
+ thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
+qed
+
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
by (auto intro!: inj_onI)
--- a/src/HOL/Tools/Nitpick/HISTORY Wed Jun 02 13:18:21 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-Version 2010
-
- * Added and implemented "binary_ints" and "bits" options
- * Added "std" option and implemented support for nonstandard models
- * Added and implemented "finitize" option to improve the precision of infinite
- datatypes based on a monotonicity analysis
- * Added support for quotient types
- * Added support for "specification" and "ax_specification" constructs
- * Added support for local definitions (for "function" and "termination"
- proofs)
- * Added support for term postprocessors
- * Optimized "Multiset.multiset" and "FinFun.finfun"
- * Improved efficiency of "destroy_constrs" optimization
- * Fixed soundness bugs related to "destroy_constrs" optimization and record
- getters
- * Fixed soundness bug related to higher-order constructors
- * Improved precision of set constructs
- * Added cache to speed up repeated Kodkod invocations on the same problems
- * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
- "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
- * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
- "sharing_depth", and "show_skolems" options
-
-Version 2009-1
-
- * Moved into Isabelle/HOL "Main"
- * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
- "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
- "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 in the "uncurry" optimization
- * Fixed soundness bugs related to sets, sets of sets, (co)inductive
- predicates, typedefs, "finite", "rel_comp", and negative literals
- * Fixed monotonicity check
- * Fixed error when processing definitions
- * Fixed error in "star_linear_preds" optimization
- * Fixed error in Kodkod encoding of "The" and "Eps"
- * Fixed error in display of uncurried constants
- * Speeded up scope enumeration
-
-Version 1.2.2 (16 Oct 2009)
-
- * Added and implemented "star_linear_preds" option
- * Added and implemented "format" option
- * Added and implemented "coalesce_type_vars" option
- * Added and implemented "max_genuine" option
- * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
- "-1::nat", subset, constructors, sort axioms, and partially applied
- interpreted constants
- * Fixed error in "show_consts" for boxed specialized constants
- * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
- * Fixed display of Skolem constants
- * Fixed error in "check_potential" and "check_genuine"
- * Added boxing support for higher-order constructor parameters
- * Changed notation used for coinductive datatypes
- * Optimized Kodkod encoding of "If", "card", and "setsum"
- * Improved the monotonicity check
-
-Version 1.2.1 (25 Sep 2009)
-
- * Added explicit support for coinductive datatypes
- * Added and implemented "box" option
- * Added and implemented "fast_descrs" option
- * Added and implemented "uncurry" option
- * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
- * Fixed soundness issue related to nullary constructors
- * Fixed soundness issue related to higher-order quantifiers
- * Fixed soundness issue related to the "destroy_constrs" optimization
- * Fixed soundness issues related to the "special_depth" optimization
- * Added support for PicoSAT and incorporated it with the Nitpick package
- * Added automatic detection of installed SAT solvers based on naming
- convention
- * Optimized handling of quantifiers by moving them inward whenever possible
- * Optimized and improved precision of "wf" and "wfrec"
- * Improved handling of definitions made in locales
- * Fixed checked scope count in message shown upon interruption and timeout
- * Added minimalistic Nitpick-like tool called Minipick
-
-Version 1.2.0 (27 Jul 2009)
-
- * Optimized Kodkod encoding of datatypes and records
- * Optimized coinductive definitions
- * Fixed soundness issues related to pairs of functions
- * Fixed soundness issue in the peephole optimizer
- * Improved precision of non-well-founded predicates occurring positively in
- the formula to falsify
- * Added and implemented "destroy_constrs" option
- * Changed semantics of "inductive_mood" option to ensure soundness
- * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
- "sync_cards"
- * Improved precision of "trancl" and "rtrancl"
- * Optimized Kodkod encoding of "tranclp" and "rtranclp"
- * Made detection of inconsistent scope specifications more robust
- * Fixed a few Kodkod generation bugs
-
-Version 1.1.1 (24 Jun 2009)
-
- * Added "show_all" option
- * Fixed soundness issues related to type classes
- * Improved precision of some set constructs
- * Fiddled with the automatic monotonicity check
- * Fixed performance issues related to scope enumeration
- * Fixed a few Kodkod generation bugs
-
-Version 1.1.0 (16 Jun 2009)
-
- * Redesigned handling of datatypes to provide an interface baded on "card" and
- "max", obsoleting "mult"
- * Redesigned handling of typedefs, "rat", and "real"
- * Made "lockstep" option a three-state option and added an automatic
- monotonicity check
- * Made "batch_size" a (n + 1)-state option whose default depends on whether
- "debug" is enabled
- * Made "debug" automatically enable "verbose"
- * Added "destroy_equals" option
- * Added "no_assms" option
- * Fixed bug in computation of ground type
- * Fixed performance issue related to datatype acyclicity constraint generation
- * Fixed performance issue related to axiom selection
- * Improved precision of some well-founded inductive predicates
- * Added more checks to guard against very large cardinalities
- * Improved hit rate of potential counterexamples
- * Fixed several soundness issues
- * Optimized the Kodkod encoding to benefit more from symmetry breaking
- * Optimized relational composition, cartesian product, and converse
- * Added support for HaifaSat
-
-Version 1.0.3 (17 Mar 2009)
-
- * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
- * Added "overlord" option to assist debugging
- * Increased default value of "special_depth" option
- * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
- * Ensured that no scopes are skipped when multithreading is enabled
- * Fixed soundness issue in handling of "The", "Eps", and partial functions
- defined using Isabelle's function package
- * Fixed soundness issue in handling of non-definitional axioms
- * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
- "nat", "int", and "*"
- * Fixed a few Kodkod generation bugs
- * Optimized "div", "mod", and "dvd" on "nat" and "int"
-
-Version 1.0.2 (12 Mar 2009)
-
- * Added support for non-definitional axioms
- * Improved Isar integration
- * Added support for multiplicities of 0
- * Added "max_threads" option and support for multithreaded Kodkodi
- * Added "blocking" option to control whether Nitpick should be run
- synchronously or asynchronously
- * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
- * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
- * Introduced "auto_timeout" to specify Auto Nitpick's time limit
- * Renamed the possible values for the "expect" option
- * Renamed the "peephole" option to "peephole_optim"
- * Added negative versions of all Boolean options and made "= true" optional
- * Altered order of automatic SAT solver selection
-
-Version 1.0.1 (6 Mar 2009)
-
- * Eliminated the need to import "Nitpick" to use "nitpick"
- * Added "debug" option
- * Replaced "specialize_funs" with the more general "special_depth" option
- * Renamed "watch" option to "eval"
- * Improved parsing of "card", "mult", and "iter" options
- * Fixed a soundness bug in the "specialize_funs" optimization
- * Increased the scope of the "specialize_funs" optimization
- * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
- * Fixed a soundness bug in the "subterm property" optimization for types of
- cardinality 1
- * Improved the axiom selection for overloaded constants, which led to an
- infinite loop for "Nominal.perm"
- * Added support for multiple instantiations of non-well-founded inductive
- predicates, which previously raised an exception
- * Fixed a Kodkod generation bug
- * Altered order of scope enumeration and automatic SAT solver selection
- * Optimized "Eps", "nat_case", and "list_case"
- * Improved output formatting
- * Added checks to prevent infinite loops in axiom selector and constant
- unfolding
-
-Version 1.0.0 (27 Feb 2009)
-
- * First release
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 02 13:18:48 2010 +0200
@@ -42,6 +42,7 @@
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
+ atomss: (typ option * string list) list,
max_potential: int,
max_genuine: int,
check_potential: bool,
@@ -112,6 +113,7 @@
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
+ atomss: (typ option * string list) list,
max_potential: int,
max_genuine: int,
check_potential: bool,
@@ -190,7 +192,7 @@
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
destroy_constrs, specialize, star_linear_preds, fast_descrs,
peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
- evals, formats, max_potential, max_genuine, check_potential,
+ evals, formats, atomss, max_potential, max_genuine, check_potential,
check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
@@ -235,14 +237,9 @@
|> pairf hd tl
val original_max_potential = max_potential
val original_max_genuine = max_genuine
-(*
- val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
- val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
- orig_assm_ts
-*)
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names thy stds
- val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
+ val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
val def_table = const_def_table ctxt subst defs
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
@@ -322,8 +319,8 @@
". " ^ extra
end
fun is_type_fundamentally_monotonic T =
- (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
- (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
+ (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
+ (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_actually_monotonic T =
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
@@ -369,7 +366,8 @@
else
()
val (deep_dataTs, shallow_dataTs) =
- all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
+ all_Ts |> filter (is_datatype ctxt stds)
+ |> List.partition is_datatype_deep
val finitizable_dataTs =
shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
|> filter is_shallow_datatype_finitizable
@@ -579,8 +577,8 @@
val (reconstructed_model, codatatypes_ok) =
reconstruct_hol_model {show_datatypes = show_datatypes,
show_consts = show_consts}
- scope formats frees free_names sel_names nonsel_names rel_table
- bounds
+ scope formats atomss frees free_names sel_names nonsel_names
+ rel_table bounds
val genuine_means_genuine =
got_all_user_axioms andalso none_true wfs andalso
sound_finitizes andalso codatatypes_ok
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Jun 02 13:18:48 2010 +0200
@@ -109,20 +109,19 @@
val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
val is_quot_type : theory -> typ -> bool
val is_codatatype : theory -> typ -> bool
- val is_pure_typedef : theory -> typ -> bool
- val is_univ_typedef : theory -> typ -> bool
- val is_datatype : theory -> (typ option * bool) list -> typ -> bool
+ val is_pure_typedef : Proof.context -> typ -> bool
+ val is_univ_typedef : Proof.context -> typ -> bool
+ val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
val is_record_constr : styp -> bool
val is_record_get : theory -> styp -> bool
val is_record_update : theory -> styp -> bool
- val is_abs_fun : theory -> styp -> bool
- val is_rep_fun : theory -> styp -> bool
+ val is_abs_fun : Proof.context -> styp -> bool
+ val is_rep_fun : Proof.context -> styp -> bool
val is_quot_abs_fun : Proof.context -> styp -> bool
val is_quot_rep_fun : Proof.context -> styp -> bool
- val mate_of_rep_fun : theory -> styp -> styp
- val is_constr_like : theory -> styp -> bool
- val is_stale_constr : theory -> styp -> bool
- val is_constr : theory -> (typ option * bool) list -> styp -> bool
+ val mate_of_rep_fun : Proof.context -> styp -> styp
+ val is_constr_like : Proof.context -> styp -> bool
+ val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
@@ -151,9 +150,10 @@
val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
val discriminate_value : hol_context -> styp -> term -> term
val select_nth_constr_arg :
- theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
+ Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
+ -> term
val construct_value :
- theory -> (typ option * bool) list -> styp -> term list -> term
+ Proof.context -> (typ option * bool) list -> styp -> term list -> term
val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
@@ -165,7 +165,7 @@
val abs_var : indexname * typ -> term -> term
val is_funky_typedef : theory -> typ -> bool
val all_axioms_of :
- theory -> (term * term) list -> term list * term list * term list
+ Proof.context -> (term * term) list -> term list * term list * term list
val arity_of_built_in_const :
theory -> (typ option * bool) list -> bool -> styp -> int option
val is_built_in_const :
@@ -186,8 +186,8 @@
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : theory -> (string * string) list
val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
- val inverse_axioms_for_rep_fun : theory -> styp -> term list
- val optimized_typedef_axioms : theory -> string * typ list -> term list
+ val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
+ val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
val optimized_quot_type_axioms :
Proof.context -> (typ option * bool) list -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
@@ -196,8 +196,8 @@
theory -> const_table -> string * typ -> fixpoint_kind
val is_inductive_pred : hol_context -> styp -> bool
val is_equational_fun : hol_context -> styp -> bool
- val is_constr_pattern_lhs : theory -> term -> bool
- val is_constr_pattern_formula : theory -> term -> bool
+ val is_constr_pattern_lhs : Proof.context -> term -> bool
+ val is_constr_pattern_formula : Proof.context -> term -> bool
val nondef_props_for_const :
theory -> bool -> const_table -> styp -> term list
val is_choice_spec_fun : hol_context -> styp -> bool
@@ -524,22 +524,25 @@
set_def: thm option, prop_of_Rep: thm, set_name: string,
Abs_inverse: thm option, Rep_inverse: thm option}
-fun typedef_info thy s =
- if is_frac_type thy (Type (s, [])) then
- SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
- Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
- set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
- |> Logic.varify_global,
- set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
- else case Typedef.get_info_global thy s of
- (* FIXME handle multiple typedef interpretations (!??) *)
- [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
- Rep_inverse, ...})] =>
- SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
- Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
- set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
- Rep_inverse = SOME Rep_inverse}
- | _ => NONE
+fun typedef_info ctxt s =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_frac_type thy (Type (s, [])) then
+ SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
+ Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
+ set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+ |> Logic.varify_global,
+ set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+ else case Typedef.get_info ctxt s of
+ (* When several entries are returned, it shouldn't matter much which one
+ we take (according to Florian Haftmann). *)
+ ({abs_type, rep_type, Abs_name, Rep_name, ...},
+ {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
+ SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+ Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+ set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+ Rep_inverse = SOME Rep_inverse}
+ | _ => NONE
+ end
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
@@ -594,14 +597,16 @@
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, _)) =
- is_typedef thy s andalso
- not (is_real_datatype thy s orelse is_quot_type thy T orelse
- is_codatatype thy T orelse is_record_type T orelse
- is_integer_like_type T)
+fun is_pure_typedef ctxt (T as Type (s, _)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_typedef ctxt s andalso
+ not (is_real_datatype thy s orelse is_quot_type thy T orelse
+ is_codatatype thy T orelse is_record_type T orelse
+ is_integer_like_type T)
+ end
| is_pure_typedef _ _ = false
-fun is_univ_typedef thy (Type (s, _)) =
- (case typedef_info thy s of
+fun is_univ_typedef ctxt (Type (s, _)) =
+ (case typedef_info ctxt s of
SOME {set_def, prop_of_Rep, ...} =>
let
val t_opt =
@@ -623,9 +628,11 @@
end
| NONE => false)
| is_univ_typedef _ _ = false
-fun is_datatype thy stds (T as Type (s, _)) =
- (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
- is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+fun is_datatype ctxt stds (T as Type (s, _)) =
+ let val thy = ProofContext.theory_of ctxt in
+ (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
+ is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+ end
| is_datatype _ _ _ = false
fun all_record_fields thy T =
@@ -651,13 +658,13 @@
exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
-fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
- (case typedef_info thy s' of
+fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
+ (case typedef_info ctxt s' of
SOME {Abs_name, ...} => s = Abs_name
| NONE => false)
| is_abs_fun _ _ = false
-fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
- (case typedef_info thy s' of
+fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
+ (case typedef_info ctxt s' of
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
@@ -672,9 +679,9 @@
= SOME (Const x))
| is_quot_rep_fun _ _ = false
-fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
- [T1 as Type (s', _), T2]))) =
- (case typedef_info thy s' of
+fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
+ [T1 as Type (s', _), T2]))) =
+ (case typedef_info ctxt s' of
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
@@ -700,23 +707,30 @@
(AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
end
handle TYPE ("dest_Type", _, _) => false
-fun is_constr_like thy (s, T) =
+fun is_constr_like ctxt (s, T) =
member (op =) [@{const_name FinFun}, @{const_name FunBox},
@{const_name PairBox}, @{const_name Quot},
@{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
- let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
- Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
- (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (x as (_, T)) = (s, unarize_unbox_etc_type T)
+ in
+ is_real_constr thy x orelse is_record_constr x orelse
+ (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type 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 stds (x as (_, T)) =
- is_constr_like thy x andalso
- not (is_basic_datatype thy stds
+fun is_stale_constr ctxt (x as (_, T)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_codatatype thy (body_type T) andalso is_constr_like ctxt x andalso
+ not (is_coconstr thy x)
+ end
+fun is_constr ctxt stds (x as (_, T)) =
+ let val thy = ProofContext.theory_of ctxt in
+ is_constr_like ctxt x andalso
+ not (is_basic_datatype thy stds
(fst (dest_Type (unarize_type (body_type T))))) andalso
- not (is_stale_constr thy x)
+ not (is_stale_constr ctxt x)
+ end
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
String.isPrefix sel_prefix orf
@@ -815,7 +829,7 @@
| eta_expand Ts (Abs (s, T, t')) n =
Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
| eta_expand Ts t n =
- fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
+ fold_rev (curry3 Abs ("x" ^ nat_subscript n))
(List.take (binder_types (fastype_of1 (Ts, t)), n))
(list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
@@ -836,20 +850,20 @@
fun zero_const T = Const (@{const_name zero_class.zero}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
+fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
| _ =>
- if is_datatype thy stds T then
+ if is_datatype ctxt stds 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
+ map (apsnd (fn Us =>
+ map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
end
| NONE =>
if is_record_type T then
@@ -860,7 +874,7 @@
in [(s', T')] end
else if is_quot_type thy T then
[(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
- else case typedef_info thy s of
+ else case typedef_info ctxt s of
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name,
varify_and_instantiate_type thy abs_type T rep_type --> T)]
@@ -905,11 +919,11 @@
else
Abs (Name.uu, dataT, @{const True})
end
-fun discriminate_value (hol_ctxt as {thy, ...}) x t =
+fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
case head_of t of
Const x' =>
if x = x' then @{const True}
- else if is_constr_like thy x' then @{const False}
+ else if is_constr_like ctxt x' then @{const False}
else betapply (discr_term_for_constr hol_ctxt x, t)
| _ => betapply (discr_term_for_constr hol_ctxt x, t)
@@ -933,24 +947,26 @@
(List.take (arg_Ts, n)) 0
in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
end
-fun select_nth_constr_arg thy stds x t n res_T =
- (case strip_comb t of
- (Const x', args) =>
- if x = x' then nth args n
- else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
- else raise SAME ()
- | _ => raise SAME())
- handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+fun select_nth_constr_arg ctxt stds x t n res_T =
+ let val thy = ProofContext.theory_of ctxt in
+ (case strip_comb t of
+ (Const x', args) =>
+ if x = x' then nth args n
+ else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
+ else raise SAME ()
+ | _ => raise SAME())
+ handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+ end
fun construct_value _ _ x [] = Const x
- | construct_value thy stds (x as (s, _)) args =
+ | construct_value ctxt stds (x as (s, _)) args =
let val args = map Envir.eta_contract args in
case hd args of
Const (s', _) $ t =>
if is_sel_like_and_no_discr s' andalso
constr_name_for_sel_like s' = s andalso
forall (fn (n, t') =>
- select_nth_constr_arg thy stds x t n dummyT = t')
+ select_nth_constr_arg ctxt stds x t n dummyT = t')
(index_seq 0 (length args) ~~ args) then
t
else
@@ -958,9 +974,9 @@
| _ => list_comb (Const x, args)
end
-fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
+fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
(case head_of t of
- Const x => if is_constr_like thy x then t else raise SAME ()
+ Const x => if is_constr_like ctxt x then t else raise SAME ()
| _ => raise SAME ())
handle SAME () =>
let
@@ -973,7 +989,7 @@
datatype_constrs hol_ctxt T |> hd
val arg_Ts = binder_types T'
in
- list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
+ list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
(index_seq 0 (length arg_Ts)) arg_Ts)
end
@@ -985,7 +1001,7 @@
| _ => t
fun coerce_bound_0_in_term hol_ctxt new_T old_T =
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
if old_T = new_T then
t
else
@@ -999,7 +1015,7 @@
|> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
|> Envir.eta_contract
|> new_s <> @{type_name fun}
- ? construct_value thy stds
+ ? construct_value ctxt stds
(if new_s = @{type_name fin_fun} then @{const_name FinFun}
else @{const_name FunBox},
Type (@{type_name fun}, new_Ts) --> new_T)
@@ -1014,12 +1030,12 @@
if new_s = @{type_name fun} then
coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
else
- construct_value thy stds
+ construct_value ctxt stds
(old_s, Type (@{type_name fun}, new_Ts) --> new_T)
[coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
(Type (@{type_name fun}, old_Ts)) t1]
| Const _ $ t1 $ t2 =>
- construct_value thy stds
+ construct_value ctxt stds
(if new_s = @{type_name "*"} then @{const_name Pair}
else @{const_name PairBox}, new_Ts ---> new_T)
(map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
@@ -1145,13 +1161,15 @@
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
$ Const (@{const_name TYPE}, _)) = true
| is_arity_type_axiom _ = false
-fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
- is_typedef_axiom thy boring t2
- | is_typedef_axiom thy boring
+fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
+ is_typedef_axiom ctxt boring t2
+ | is_typedef_axiom ctxt boring
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
$ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
$ Const _ $ _)) =
- boring <> is_funky_typedef_name thy s andalso is_typedef thy s
+ let val thy = ProofContext.theory_of ctxt in
+ boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s
+ end
| is_typedef_axiom _ _ _ = false
val is_class_axiom =
Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
@@ -1160,13 +1178,13 @@
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
Typedef axioms are uninteresting to Nitpick, because it can retrieve them
using "typedef_info". *)
-fun partition_axioms_by_definitionality thy axioms def_names =
+fun partition_axioms_by_definitionality ctxt axioms def_names =
let
val axioms = sort (fast_string_ord o pairself fst) axioms
val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
val nondefs =
OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
- |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
+ |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
in pairself (map snd) (defs, nondefs) end
(* Ideally we would check against "Complex_Main", not "Refute", but any theory
@@ -1189,8 +1207,9 @@
| do_eq _ = false
in do_eq end
-fun all_axioms_of thy subst =
+fun all_axioms_of ctxt subst =
let
+ val thy = ProofContext.theory_of ctxt
val axioms_of_thys =
maps Thm.axioms_of
#> map (apsnd (subst_atomic subst o prop_of))
@@ -1203,12 +1222,12 @@
val built_in_axioms = axioms_of_thys built_in_thys
val user_axioms = axioms_of_thys user_thys
val (built_in_defs, built_in_nondefs) =
- partition_axioms_by_definitionality thy built_in_axioms def_names
- ||> filter (is_typedef_axiom thy false)
+ partition_axioms_by_definitionality ctxt built_in_axioms def_names
+ ||> filter (is_typedef_axiom ctxt false)
val (user_defs, user_nondefs) =
- partition_axioms_by_definitionality thy user_axioms def_names
+ partition_axioms_by_definitionality ctxt user_axioms def_names
val (built_in_nondefs, user_nondefs) =
- List.partition (is_typedef_axiom thy false) user_nondefs
+ List.partition (is_typedef_axiom ctxt false) user_nondefs
|>> append built_in_nondefs
val defs =
(thy |> PureThy.all_thms_of
@@ -1369,16 +1388,16 @@
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
- | is_constr_pattern thy t =
+ | is_constr_pattern ctxt t =
case strip_comb t of
(Const x, args) =>
- is_constr_like thy x andalso forall (is_constr_pattern thy) args
+ is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
| _ => false
-fun is_constr_pattern_lhs thy t =
- forall (is_constr_pattern thy) (snd (strip_comb t))
-fun is_constr_pattern_formula thy t =
+fun is_constr_pattern_lhs ctxt t =
+ forall (is_constr_pattern ctxt) (snd (strip_comb t))
+fun is_constr_pattern_formula ctxt t =
case lhs_of_equation t of
- SOME t' => is_constr_pattern_lhs thy t'
+ SOME t' => is_constr_pattern_lhs ctxt t'
| NONE => false
(* Similar to "specialize_type" but returns all matches rather than only the
@@ -1397,8 +1416,10 @@
if slack then
I
else
- raise NOT_SUPPORTED ("too much polymorphism in \
- \axiom involving " ^ quote s))
+ raise NOT_SUPPORTED
+ ("too much polymorphism in axiom \"" ^
+ Syntax.string_of_term_global thy t ^
+ "\" involving " ^ quote s))
else
ys
| aux _ ys = ys
@@ -1437,26 +1458,26 @@
(** Constant unfolding **)
-fun constr_case_body thy stds (j, (x as (_, T))) =
+fun constr_case_body ctxt stds (j, (x as (_, T))) =
let val arg_Ts = binder_types T in
- list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
+ list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
+fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
+ $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
$ res_t
-fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
+fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
let
val xs = datatype_constrs hol_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 stds (1, x)
+ constr_case_body ctxt stds (1, x)
|> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
@@ -1465,14 +1486,15 @@
val rec_T' = List.last Ts
val j = num_record_fields thy rec_T - 1
in
- select_nth_constr_arg thy stds constr_x t j res_T
+ select_nth_constr_arg ctxt stds constr_x t j res_T
|> optimized_record_get hol_ctxt s rec_T' res_T
end
| _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
[]))
- | j => select_nth_constr_arg thy stds constr_x t j res_T
+ | j => select_nth_constr_arg ctxt stds constr_x t j res_T
end
-fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
+fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
+ rec_t =
let
val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
val Ts = binder_types constr_T
@@ -1480,7 +1502,7 @@
val special_j = no_of_record_field thy s rec_T
val ts =
map2 (fn j => fn T =>
- let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
+ let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
if j = special_j then
betapply (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
@@ -1549,9 +1571,9 @@
| Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
- select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
+ select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
- (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
+ (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
and do_const depth Ts t (x as (s, T)) ts =
case AList.lookup (op =) ersatz_table s of
SOME s' =>
@@ -1571,9 +1593,9 @@
|> do_term (depth + 1) Ts, ts)
end
| _ =>
- if is_constr thy stds x then
+ if is_constr ctxt stds x then
(Const x, ts)
- else if is_stale_constr thy x then
+ else if is_stale_constr ctxt x then
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
\(\"" ^ s ^ "\")")
else if is_quot_abs_fun ctxt x then
@@ -1604,9 +1626,9 @@
(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
- if is_constr thy stds x' then
+ else if is_rep_fun ctxt x then
+ let val x' = mate_of_rep_fun ctxt x in
+ if is_constr ctxt stds x' then
select_nth_constr_arg_with_args depth Ts x' ts 0
(range_type T)
else
@@ -1652,10 +1674,14 @@
map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
|> const_nondef_table
fun inductive_intro_table ctxt subst def_table =
- def_table_for
- (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
- def_table o prop_of)
- o Nitpick_Intros.get) ctxt subst
+ let val thy = ProofContext.theory_of ctxt in
+ def_table_for
+ (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
+ o snd o snd)
+ o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
+ cat = Spec_Rules.Co_Inductive)
+ o Spec_Rules.get) ctxt subst
+ end
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
@@ -1677,18 +1703,24 @@
Unsynchronized.change simp_table
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
-fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
- let val abs_T = domain_type T in
- typedef_info thy (fst (dest_Type abs_T)) |> the
+fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val abs_T = domain_type T
+ in
+ typedef_info ctxt (fst (dest_Type abs_T)) |> the
|> pairf #Abs_inverse #Rep_inverse
|> pairself (specialize_type thy x o prop_of o the)
||> single |> op ::
end
-fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
- let val abs_T = Type abs_z in
- if is_univ_typedef thy abs_T then
+fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val abs_T = Type abs_z
+ in
+ if is_univ_typedef ctxt abs_T then
[]
- else case typedef_info thy abs_s of
+ else case typedef_info ctxt abs_s of
SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
let
val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
@@ -1716,7 +1748,7 @@
val x_var = Var (("x", 0), rep_T)
val y_var = Var (("y", 0), rep_T)
val x = (@{const_name Quot}, rep_T --> abs_T)
- val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
+ val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
val normal_x = normal_t $ x_var
val normal_y = normal_t $ y_var
@@ -1734,7 +1766,7 @@
HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
end
-fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
@@ -1751,8 +1783,8 @@
fun nth_sub_bisim x n nth_T =
(if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
else HOLogic.eq_const nth_T)
- $ select_nth_constr_arg thy stds x x_var n nth_T
- $ select_nth_constr_arg thy stds x y_var n nth_T
+ $ select_nth_constr_arg ctxt stds x x_var n nth_T
+ $ select_nth_constr_arg ctxt stds x y_var n nth_T
fun case_func (x as (_, T)) =
let
val arg_Ts = binder_types T
@@ -1785,20 +1817,18 @@
end
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
-
fun wf_constraint_for rel side concl main =
let
- val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
- tuple_for_args concl), Var rel)
+ val core = HOLogic.mk_mem (HOLogic.mk_prod
+ (pairself tuple_for_args (main, concl)), Var rel)
val t = List.foldl HOLogic.mk_imp core side
- val vars = filter (not_equal rel) (Term.add_vars t [])
+ val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
in
Library.foldl (fn (t', ((x, j), T)) =>
HOLogic.all_const T
$ Abs (x, T, abstract_over (Var ((x, j), T), t')))
(t, vars)
end
-
fun wf_constraint_for_triple rel (side, main, concl) =
map (wf_constraint_for rel side concl) main |> foldr1 s_conj
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Jun 02 13:18:48 2010 +0200
@@ -65,6 +65,7 @@
("show_datatypes", "false"),
("show_consts", "false"),
("format", "1"),
+ ("atoms", ""),
("max_potential", "1"),
("max_genuine", "1"),
("check_potential", "false"),
@@ -98,10 +99,11 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
AList.defined (op =) negated_params s orelse
- s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
+ member (op =) ["max", "show_all", "eval", "expect"] s orelse
exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
- "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
+ "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -149,8 +151,8 @@
let
val override_params = maps normalize_raw_param override_params
val raw_params = rev override_params @ rev default_params
- val lookup =
- Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
+ val raw_lookup = AList.lookup (op =) raw_params
+ val lookup = Option.map stringify_raw_param_value o raw_lookup
val lookup_string = the_default "" o lookup
fun general_lookup_bool option default_value name =
case lookup name of
@@ -191,27 +193,21 @@
[] => [min_int]
| value => value)
| NONE => [min_int]
- fun lookup_ints_assigns read prefix min_int =
- (NONE, lookup_int_seq prefix min_int)
- :: map (fn (name, value) =>
- (SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> int_seq_from_string name min_int))
- (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
- fun lookup_bool_assigns read prefix =
- (NONE, lookup_bool prefix)
+ fun lookup_assigns read prefix default convert =
+ (NONE, convert (the_default default (lookup prefix)))
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> parse_bool_option false name |> the))
+ convert (stringify_raw_param_value value)))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
+ fun lookup_ints_assigns read prefix min_int =
+ lookup_assigns read prefix (signed_string_of_int min_int)
+ (int_seq_from_string prefix min_int)
+ fun lookup_bool_assigns read prefix =
+ lookup_assigns read prefix "" (the o parse_bool_option false prefix)
fun lookup_bool_option_assigns read prefix =
- (NONE, lookup_bool_option prefix)
- :: map (fn (name, value) =>
- (SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> parse_bool_option true name))
- (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
+ lookup_assigns read prefix "" (parse_bool_option true prefix)
+ fun lookup_strings_assigns read prefix =
+ lookup_assigns read prefix "" (space_explode " ")
fun lookup_time name =
case lookup name of
NONE => NONE
@@ -255,6 +251,7 @@
val show_datatypes = debug orelse lookup_bool "show_datatypes"
val show_consts = debug orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
+ val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
val evals = lookup_term_list "eval"
val max_potential =
if auto then 0 else Int.max (0, lookup_int "max_potential")
@@ -279,9 +276,10 @@
peephole_optim = peephole_optim, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
show_datatypes = show_datatypes, show_consts = show_consts,
- formats = formats, evals = evals, max_potential = max_potential,
- max_genuine = max_genuine, check_potential = check_potential,
- check_genuine = check_genuine, batch_size = batch_size, expect = expect}
+ formats = formats, atomss = atomss, evals = evals,
+ max_potential = max_potential, max_genuine = max_genuine,
+ check_potential = check_potential, check_genuine = check_genuine,
+ batch_size = batch_size, expect = expect}
end
fun default_params thy =
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Jun 02 13:18:48 2010 +0200
@@ -23,7 +23,7 @@
val irrelevant : string
val unknown : string
- val unrep : string
+ val unrep : unit -> string
val register_term_postprocessor :
typ -> term_postprocessor -> theory -> theory
val unregister_term_postprocessor : typ -> theory -> theory
@@ -31,8 +31,9 @@
nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
val dest_plain_fun : term -> bool * (term list * term list)
val reconstruct_hol_model :
- params -> scope -> (term option * int list) list -> styp list -> nut list
- -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
+ params -> scope -> (term option * int list) list
+ -> (typ option * string list) list -> styp list -> nut list -> nut list
+ -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
-> Pretty.T * bool
val prove_hol_model :
scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
@@ -64,17 +65,19 @@
val extend = I
fun merge (x, y) = AList.merge (op =) (K true) (x, y))
+fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
+
val irrelevant = "_"
val unknown = "?"
-val unrep = "\<dots>"
-val maybe_mixfix = "_\<^sup>?"
-val base_mixfix = "_\<^bsub>base\<^esub>"
-val step_mixfix = "_\<^bsub>step\<^esub>"
-val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
+val unrep = xsym "\<dots>" "..."
+val maybe_mixfix = xsym "_\<^sup>?" "_?"
+val base_mixfix = xsym "_\<^bsub>base\<^esub>" "_.base"
+val step_mixfix = xsym "_\<^bsub>step\<^esub>" "_.step"
+val abs_mixfix = xsym "\<guillemotleft>_\<guillemotright>" "\"_\""
val arg_var_prefix = "x"
-val cyclic_co_val_name = "\<omega>"
-val cyclic_const_prefix = "\<xi>"
-val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
+val cyclic_co_val_name = xsym "\<omega>" "w"
+val cyclic_const_prefix = xsym "\<xi>" "X"
+fun cyclic_type_name () = nitpick_prefix ^ cyclic_const_prefix ()
val opt_flag = nitpick_prefix ^ "opt"
val non_opt_flag = nitpick_prefix ^ "non_opt"
@@ -86,16 +89,16 @@
val thy = ProofContext.theory_of ctxt |> Context.reject_draft
val (maybe_t, thy) =
Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
- Mixfix (maybe_mixfix, [1000], 1000)) thy
+ Mixfix (maybe_mixfix (), [1000], 1000)) thy
val (abs_t, thy) =
Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
- Mixfix (abs_mixfix, [40], 40)) thy
+ Mixfix (abs_mixfix (), [40], 40)) thy
val (base_t, thy) =
Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
- Mixfix (base_mixfix, [1000], 1000)) thy
+ Mixfix (base_mixfix (), [1000], 1000)) thy
val (step_t, thy) =
Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
- Mixfix (step_mixfix, [1000], 1000)) thy
+ Mixfix (step_mixfix (), [1000], 1000)) thy
in
(pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
ProofContext.transfer_syntax thy ctxt)
@@ -103,31 +106,41 @@
(** Term reconstruction **)
-fun nth_atom_suffix pool s j k =
- (case AList.lookup (op =) (!pool) (s, k) of
- SOME js =>
- (case find_index (curry (op =) j) js of
- ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
- length js + 1)
- | n => length js - n)
- | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
- |> nat_subscript
- |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
+fun nth_atom_number pool T j =
+ case AList.lookup (op =) (!pool) T of
+ SOME js =>
+ (case find_index (curry (op =) j) js of
+ ~1 => (Unsynchronized.change pool (cons (T, j :: js));
+ length js + 1)
+ | n => length js - n)
+ | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
+fun atom_suffix s =
+ nat_subscript
+ #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
? prefix "\<^isub>,"
-fun nth_atom_name pool prefix (Type (s, _)) j k =
- let val s' = shortest_name s in
- prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
- nth_atom_suffix pool s j k
- end
- | nth_atom_name pool prefix (TFree (s, _)) j k =
- prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
- | nth_atom_name _ _ T _ _ =
- raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
-fun nth_atom pool for_auto T j k =
+fun nth_atom_name thy atomss pool prefix T j =
+ let
+ val ss = these (triple_lookup (type_match thy) atomss T)
+ val m = nth_atom_number pool T j
+ in
+ if m <= length ss then
+ nth ss (m - 1)
+ else case T of
+ Type (s, _) =>
+ let val s' = shortest_name s in
+ prefix ^
+ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
+ atom_suffix s m
+ end
+ | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
+ | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
+ end
+fun nth_atom thy atomss pool for_auto T j =
if for_auto then
- Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
+ Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
+ T j, T)
else
- Const (nth_atom_name pool "" T j k, T)
+ Const (nth_atom_name thy atomss pool "" T j, T)
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
@@ -300,27 +313,29 @@
strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
- sel_names rel_table bounds card T =
+ atomss sel_names rel_table bounds card T =
let
val card = if card = 0 then card_of_type card_assigns T else card
fun nth_value_of_type n =
let
fun term unfold =
- reconstruct_term unfold pool wacky_names scope sel_names rel_table
- bounds T T (Atom (card, 0)) [[n]]
+ reconstruct_term true unfold pool wacky_names scope atomss sel_names
+ rel_table bounds T T (Atom (card, 0)) [[n]]
in
case term false of
t as Const (s, _) =>
- if String.isPrefix cyclic_const_prefix s then
+ if String.isPrefix (cyclic_const_prefix ()) s then
HOLogic.mk_eq (t, term true)
else
t
| t => t
end
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
-and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
- (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
- bits, datatypes, ofs, ...}) sel_names rel_table bounds =
+and reconstruct_term maybe_opt unfold pool
+ (wacky_names as ((maybe_name, abs_name), _))
+ (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
+ bits, datatypes, ofs, ...})
+ atomss sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
fun value_of_bits jss =
@@ -332,7 +347,8 @@
js 0
end
val all_values =
- all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
+ all_values_of_type pool wacky_names scope atomss sel_names rel_table
+ bounds 0
fun postprocess_term (Type (@{type_name fun}, _)) = I
| postprocess_term T =
if null (Data.get thy) then
@@ -354,7 +370,7 @@
T1 --> (T1 --> T2) --> T1 --> T2)
fun aux [] =
if maybe_opt andalso not (is_complete_type datatypes false T1) then
- insert_const $ Const (unrep, T1) $ empty_const
+ insert_const $ Const (unrep (), T1) $ empty_const
else
empty_const
| aux ((t1, t2) :: zs) =
@@ -383,7 +399,7 @@
| _ => update_const $ aux' tps $ t1 $ t2)
fun aux tps =
if maybe_opt andalso not (is_complete_type datatypes false T1) then
- update_const $ aux' tps $ Const (unrep, T1)
+ update_const $ aux' tps $ Const (unrep (), T1)
$ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
else
aux' tps
@@ -471,16 +487,17 @@
else if T = @{typ bisim_iterator} then
HOLogic.mk_number nat_T j
else case datatype_spec datatypes T of
- NONE => nth_atom pool for_auto T j k
- | SOME {deep = false, ...} => nth_atom pool for_auto T j k
+ NONE => nth_atom thy atomss pool for_auto T j
+ | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
| SOME {co, standard, constrs, ...} =>
let
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
fun cyclic_atom () =
- nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
- fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
-
+ nth_atom thy atomss pool for_auto (Type (cyclic_type_name (), []))
+ j
+ fun cyclic_var () =
+ Var ((nth_atom_name thy atomss pool "" T j, 0), T)
val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
constrs
val real_j = j + offset_of_type ofs T
@@ -536,7 +553,7 @@
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
\term_for_atom (Abs_Frac)", ts)
else if not for_auto andalso
- (is_abs_fun thy constr_x orelse
+ (is_abs_fun ctxt constr_x orelse
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
else
@@ -546,14 +563,15 @@
let val var = cyclic_var () in
if unfold andalso not standard andalso
length seen = 1 andalso
- exists_subterm (fn Const (s, _) =>
- String.isPrefix cyclic_const_prefix s
- | t' => t' = var) t then
+ exists_subterm
+ (fn Const (s, _) =>
+ String.isPrefix (cyclic_const_prefix ()) s
+ | t' => t' = var) t then
subst_atomic [(var, cyclic_atom ())] t
else if exists_subterm (curry (op =) var) t then
if co then
Const (@{const_name The}, (T --> bool_T) --> T)
- $ Abs (cyclic_co_val_name, T,
+ $ Abs (cyclic_co_val_name (), T,
Const (@{const_name "op ="}, T --> T --> bool_T)
$ Bound 0 $ abstract_over (var, t))
else
@@ -612,11 +630,11 @@
else term_for_rep true seen T T' R jss
| term_for_rep _ _ T _ R jss =
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
- Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
+ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
in
postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
- oooo term_for_rep true []
+ oooo term_for_rep maybe_opt []
end
(** Constant postprocessing **)
@@ -801,9 +819,11 @@
fun assign_operator_for_const (s, T) =
if String.isPrefix ubfp_prefix s then
- if is_fun_type T then "\<subseteq>" else "\<le>"
+ if is_fun_type T then xsym "\<subseteq>" "<=" ()
+ else xsym "\<le>" "<=" ()
else if String.isPrefix lbfp_prefix s then
- if is_fun_type T then "\<supseteq>" else "\<ge>"
+ if is_fun_type T then xsym "\<supseteq>" ">=" ()
+ else xsym "\<ge>" ">=" ()
else if original_name s <> s then
assign_operator_for_const (strip_first_name_sep s |> snd, T)
else
@@ -811,13 +831,6 @@
(** Model reconstruction **)
-fun term_for_name pool scope sel_names rel_table bounds name =
- let val T = type_of name in
- tuple_list_for_name rel_table bounds name
- |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
- rel_table bounds T T (rep_of name)
- end
-
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
$ Abs (s, T, Const (@{const_name "op ="}, _)
$ Bound 0 $ t')) =
@@ -848,7 +861,8 @@
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache},
binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
- formats all_frees free_names sel_names nonsel_names rel_table bounds =
+ formats atomss all_frees free_names sel_names nonsel_names rel_table
+ bounds =
let
val pool = Unsynchronized.ref []
val (wacky_names as (_, base_step_names), ctxt) =
@@ -870,22 +884,24 @@
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
- fun term_for_rep unfold =
- reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
+ fun term_for_rep maybe_opt unfold =
+ reconstruct_term maybe_opt unfold pool wacky_names scope atomss
+ sel_names rel_table bounds
fun nth_value_of_type card T n =
let
- fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
+ fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
in
case aux false of
t as Const (s, _) =>
- if String.isPrefix cyclic_const_prefix s then
+ if String.isPrefix (cyclic_const_prefix ()) s then
HOLogic.mk_eq (t, aux true)
else
t
| t => t
end
val all_values =
- all_values_of_type pool wacky_names scope sel_names rel_table bounds
+ all_values_of_type pool wacky_names scope atomss sel_names rel_table
+ bounds
fun is_codatatype_wellformed (cos : dtype_spec list)
({typ, card, ...} : dtype_spec) =
let
@@ -912,7 +928,8 @@
Const (@{const_name undefined}, T')
else
tuple_list_for_name rel_table bounds name
- |> term_for_rep false T T' (rep_of name)
+ |> term_for_rep (not (is_fully_representable_set name)) false
+ T T' (rep_of name)
in
Pretty.block (Pretty.breaks
[setmp_show_all_types (Syntax.pretty_term ctxt) t1,
@@ -930,7 +947,7 @@
Pretty.enum "," "{" "}"
(map (Syntax.pretty_term ctxt) (all_values card typ) @
(if fun_from_pair complete false then []
- else [Pretty.str unrep]))]))
+ else [Pretty.str (unrep ())]))]))
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
standard = true, complete = (false, false), concrete = (true, true),
@@ -991,14 +1008,23 @@
forall (is_codatatype_wellformed codatatypes) codatatypes)
end
+fun term_for_name pool scope atomss sel_names rel_table bounds name =
+ let val T = type_of name in
+ tuple_list_for_name rel_table bounds name
+ |> reconstruct_term (not (is_fully_representable_set name)) false pool
+ (("", ""), ("", "")) scope atomss sel_names rel_table
+ bounds T T (rep_of name)
+ end
+
fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
val pool = Unsynchronized.ref []
+ val atomss = [(NONE, [])]
fun free_type_assm (T, k) =
let
- fun atom j = nth_atom pool true T j k
+ fun atom j = nth_atom thy atomss pool true T j
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
val eqs = map equation_for_atom (index_seq 0 k)
val compreh_assm =
@@ -1008,7 +1034,8 @@
in s_conj (compreh_assm, distinct_assm) end
fun free_name_assm name =
HOLogic.mk_eq (Free (nickname_of name, type_of name),
- term_for_name pool scope sel_names rel_table bounds name)
+ term_for_name pool scope atomss sel_names rel_table bounds
+ name)
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
val model_assms = map free_name_assm free_names
val assm = foldr1 s_conj (freeT_assms @ model_assms)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Jun 02 13:18:48 2010 +0200
@@ -162,8 +162,8 @@
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
- | could_exist_alpha_sub_mtype thy alpha_T T =
- (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
+ | could_exist_alpha_sub_mtype ctxt alpha_T T =
+ (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
fun exists_alpha_sub_mtype MAlpha = true
| exists_alpha_sub_mtype (MFun (M1, _, M2)) =
@@ -243,7 +243,7 @@
else
S Minus
in (M1, a, M2) end
-and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
+and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
datatype_mcache, constr_mcache, ...})
all_minus =
let
@@ -255,7 +255,7 @@
MFun (fresh_mfun_for_fun_type mdata false T1 T2)
| Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
- if could_exist_alpha_sub_mtype thy alpha_T T then
+ if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!datatype_mcache) z of
SOME M => M
| NONE =>
@@ -290,7 +290,7 @@
end
else
MType (s, [])
- | _ => MType (Refute.string_of_typ T, [])
+ | _ => MType (simple_string_of_typ T, [])
in do_type end
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
@@ -304,9 +304,9 @@
case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
end
-fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
+fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
...}) (x as (_, T)) =
- if could_exist_alpha_sub_mtype thy alpha_T T then
+ if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!constr_mcache) x of
SOME M => M
| NONE => if T = alpha_T then
@@ -741,7 +741,7 @@
do_robust_set_operation T accum
else if is_sel s then
(mtype_for_sel mdata x, accum)
- else if is_constr thy stds x then
+ else if is_constr ctxt stds x then
(mtype_for_constr mdata x, accum)
else if is_built_in_const thy stds fast_descrs x then
(fresh_mtype_for_type mdata true T, accum)
@@ -924,8 +924,8 @@
if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
else consider_general_formula mdata Plus t
-fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
- if not (is_constr_pattern_formula thy t) then
+fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
+ if not (is_constr_pattern_formula ctxt t) then
consider_nondefinitional_axiom mdata t
else if is_harmless_axiom mdata t then
pair (MRaw (t, dummy_M))
@@ -1027,7 +1027,8 @@
fun fin_fun_constr T1 T2 =
(@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
+fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
+ ...})
binarize finitizes alpha_T tsp =
case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
SOME (lits, msp, constr_mtypes) =>
@@ -1054,11 +1055,11 @@
(s, case AList.lookup (op =) constr_mtypes x of
SOME M => type_from_mtype T M
| NONE => T)
- fun term_from_mterm Ts m =
+ fun term_from_mterm new_Ts old_Ts m =
case m of
MRaw (t, M) =>
let
- val T = fastype_of1 (Ts, t)
+ val T = fastype_of1 (old_Ts, t)
val T' = type_from_mtype T M
in
case t of
@@ -1072,7 +1073,7 @@
$ (Const (@{const_name is_unknown},
elem_T' --> bool_T) $ Bound 1)
$ (Const (@{const_name unknown}, set_T'))
- $ (coerce_term hol_ctxt Ts T' T (Const x)
+ $ (coerce_term hol_ctxt new_Ts T' T (Const x)
$ Bound 1 $ Bound 0)))
| _ => Const (s, T')
else if s = @{const_name finite} then
@@ -1084,8 +1085,8 @@
s = @{const_name "op ="} then
Const (s, T')
else if is_built_in_const thy stds fast_descrs x then
- coerce_term hol_ctxt Ts T' T t
- else if is_constr thy stds x then
+ coerce_term hol_ctxt new_Ts T' T t
+ else if is_constr ctxt stds x then
Const (finitize_constr x)
else if is_sel s then
let
@@ -1106,32 +1107,32 @@
end
| MApp (m1, m2) =>
let
- val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
- val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
+ val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
+ val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
val (t1', T2') =
case T1 of
Type (s, [T11, T12]) =>
(if s = @{type_name fin_fun} then
- select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
+ select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
0 (T11 --> T12)
else
t1, T11)
| _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
[T1], [])
- in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
- | MAbs (s, T, M, a, m') =>
+ in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
+ | MAbs (s, old_T, M, a, m') =>
let
- val T = type_from_mtype T M
- val t' = term_from_mterm (T :: Ts) m'
- val T' = fastype_of1 (T :: Ts, t')
+ val new_T = type_from_mtype old_T M
+ val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
+ val T' = fastype_of1 (new_T :: new_Ts, t')
in
- Abs (s, T, t')
- |> should_finitize (T --> T') a
- ? construct_value thy stds (fin_fun_constr T T') o single
+ Abs (s, new_T, t')
+ |> should_finitize (new_T --> T') a
+ ? construct_value ctxt stds (fin_fun_constr new_T T') o single
end
in
Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
- pairself (map (term_from_mterm [])) msp
+ pairself (map (term_from_mterm [] [])) msp
end
| NONE => tsp
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Jun 02 13:18:48 2010 +0200
@@ -105,6 +105,7 @@
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
val nut_from_term : hol_context -> op2 -> term -> nut
+ val is_fully_representable_set : nut -> bool
val choose_reps_for_free_vars :
scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
val choose_reps_for_consts :
@@ -439,7 +440,7 @@
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
let
fun aux eq ss Ts t =
let
@@ -565,7 +566,7 @@
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (x as (s as @{const_name Suc}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Suc, T, Any)
- else if is_constr thy stds x then do_construct x []
+ else if is_constr ctxt stds x then do_construct x []
else ConstName (s, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
(if is_finite_type hol_ctxt (domain_type T) then
@@ -576,7 +577,7 @@
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
| (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
- else if is_constr thy stds x then do_construct x []
+ else if is_constr ctxt stds x then do_construct x []
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name one_class.one}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
@@ -653,7 +654,7 @@
[t1, t2]) =>
Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
- if is_constr thy stds x then
+ if is_constr ctxt stds x then
do_construct x ts
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
@@ -677,6 +678,24 @@
end
in aux eq [] [] end
+fun is_fully_representable_set u =
+ not (is_opt_rep (rep_of u)) andalso
+ case u of
+ FreeName _ => true
+ | Op1 (SingletonSet, _, _, _) => true
+ | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
+ | Op2 (oper, _, _, u1, u2) =>
+ if oper = Union orelse oper = SetDifference orelse oper = Intersect then
+ forall is_fully_representable_set [u1, u2]
+ else if oper = Apply then
+ case u1 of
+ ConstName (s, _, _) =>
+ is_sel_like_and_no_discr s orelse s = @{const_name set}
+ | _ => false
+ else
+ false
+ | _ => false
+
fun rep_for_abs_fun scope T =
let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
@@ -687,13 +706,13 @@
val R = best_non_opt_set_rep_for_type scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
(vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
- val R = (if is_abs_fun thy x then
+ val R = (if is_abs_fun ctxt x then
rep_for_abs_fun
- else if is_rep_fun thy x then
+ else if is_rep_fun ctxt x then
Func oo best_non_opt_symmetric_reps_for_fun_type
else if all_exact orelse is_skolem_name v orelse
member (op =) [@{const_name undefined_fast_The},
@@ -766,22 +785,6 @@
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
-fun is_fully_representable_set u =
- not (is_opt_rep (rep_of u)) andalso
- case u of
- FreeName _ => true
- | Op1 (SingletonSet, _, _, _) => true
- | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
- | Op2 (oper, _, _, u1, u2) =>
- if oper = Union orelse oper = SetDifference orelse oper = Intersect then
- forall is_fully_representable_set [u1, u2]
- else if oper = Apply then
- case u1 of
- ConstName (s, _, _) => is_sel_like_and_no_discr s
- | _ => false
- else
- false
- | _ => false
fun s_op1 oper T R u1 =
((if oper = Not then
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jun 02 13:18:48 2010 +0200
@@ -25,6 +25,10 @@
(polar = Pos andalso quant_s = @{const_name Ex}) orelse
(polar = Neg andalso quant_s <> @{const_name Ex})
+val is_descr =
+ member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
+ @{const_name safe_Eps}]
+
(** Binary coding of integers **)
(* If a formula contains a numeral whose absolute value is more than this
@@ -65,14 +69,15 @@
(** Uncurrying **)
-fun add_to_uncurry_table thy t =
+fun add_to_uncurry_table ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
fun aux (t1 $ t2) args table =
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
| aux (t as Const (x as (s, _))) args table =
if is_built_in_const thy [(NONE, true)] true x orelse
- is_constr_like thy x orelse
+ is_constr_like ctxt x orelse
is_sel s orelse s = @{const_name Sigma} then
table
else
@@ -121,8 +126,8 @@
(** Boxing **)
-fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
- orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
+ def orig_t =
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
@@ -178,7 +183,7 @@
list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
end
- and do_description_operator s T =
+ and do_descr s T =
let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
Const (s, (T1 --> bool_T) --> T1)
end
@@ -213,28 +218,26 @@
| @{const "op -->"} $ t1 $ t2 =>
@{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
$ do_term new_Ts old_Ts polar t2
- | Const (s as @{const_name The}, T) => do_description_operator s T
- | Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (s as @{const_name safe_The}, T) => do_description_operator s T
- | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T
| Const (x as (s, T)) =>
- Const (s, if s = @{const_name converse} orelse
- s = @{const_name trancl} then
- box_relational_operator_type T
- else if String.isPrefix quot_normal_prefix s then
- let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
- T' --> T'
- end
- else if is_built_in_const thy stds fast_descrs x orelse
- s = @{const_name Sigma} then
- T
- else if is_constr_like thy x then
- box_type hol_ctxt InConstr T
- else if is_sel s
- orelse is_rep_fun thy x then
- box_type hol_ctxt InSel T
- else
- box_type hol_ctxt InExpr T)
+ if is_descr s then
+ do_descr s T
+ else
+ Const (s, if s = @{const_name converse} orelse
+ s = @{const_name trancl} then
+ box_relational_operator_type T
+ else if String.isPrefix quot_normal_prefix s then
+ let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
+ T' --> T'
+ end
+ else if is_built_in_const thy stds fast_descrs x orelse
+ s = @{const_name Sigma} then
+ T
+ else if is_constr_like ctxt x then
+ box_type hol_ctxt InConstr T
+ else if is_sel s orelse is_rep_fun ctxt x then
+ box_type hol_ctxt InSel T
+ else
+ box_type hol_ctxt InExpr T)
| t1 $ Abs (s, T, t2') =>
let
val t1 = do_term new_Ts old_Ts Neut t1
@@ -248,7 +251,7 @@
betapply (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg thy stds
+ select_nth_constr_arg ctxt stds
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -265,7 +268,7 @@
betapply (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg thy stds
+ select_nth_constr_arg ctxt stds
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -293,12 +296,12 @@
| aux _ = true
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
+fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
args seen =
let val t_comb = list_comb (t, args) in
case t of
Const x =>
- if not relax andalso is_constr thy stds x andalso
+ if not relax andalso is_constr ctxt stds x andalso
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
has_heavy_bounds_or_vars Ts t_comb andalso
not (loose_bvar (t_comb, level)) then
@@ -397,7 +400,7 @@
$ t $ abs_var z (incr_boundvars 1 (f (Var z)))
end
-fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
let
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
@@ -432,7 +435,7 @@
val n = length arg_Ts
in
if length args = n andalso
- (is_constr thy stds x orelse s = @{const_name Pair} orelse
+ (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
@@ -449,7 +452,7 @@
else t0 $ aux false t2 $ aux false t1
and sel_eq x t n nth_T nth_t =
HOLogic.eq_const nth_T $ nth_t
- $ select_nth_constr_arg thy stds x t n nth_T
+ $ select_nth_constr_arg ctxt stds x t n nth_T
|> aux false
in aux axiom t end
@@ -484,7 +487,7 @@
aux (t1 :: prems) (Term.add_vars t1 zs) t2
in aux [] [] end
-fun find_bound_assign thy stds j =
+fun find_bound_assign ctxt stds j =
let
fun do_term _ [] = NONE
| do_term seen (t :: ts) =
@@ -497,8 +500,9 @@
| Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
if j' = j andalso
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
- SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
- [t2], ts @ seen)
+ SOME (construct_value ctxt stds
+ (@{const_name FunBox}, T2 --> T1) [t2],
+ ts @ seen)
else
raise SAME ()
| _ => raise SAME ())
@@ -523,11 +527,11 @@
| aux _ = raise SAME ()
in aux (t, j) handle SAME () => t end
-fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
+fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
let
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign thy stds (length ss) [] ts of
+ (case find_bound_assign ctxt stds (length ss) [] ts of
SOME (_, []) => @{const True}
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
@@ -893,7 +897,7 @@
(if head_of t <> @{const "==>"} then add_def_axiom
else add_nondef_axiom) depth t
and add_eq_axiom depth t =
- (if is_constr_pattern_formula thy t then add_def_axiom
+ (if is_constr_pattern_formula ctxt t then add_def_axiom
else add_nondef_axiom) depth t
and add_axioms_for_term depth t (accum as (xs, axs)) =
case t of
@@ -909,27 +913,30 @@
\add_axioms_for_term",
"too many nested axioms (" ^
string_of_int depth ^ ")")
- else if Refute.is_const_of_class thy x then
+ else if is_of_class_const thy x then
let
val class = Logic.class_of_const s
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
class)
val ax1 = try (specialize_type thy x) of_class
val ax2 = Option.map (specialize_type thy x o snd)
- (Refute.get_classdef thy class)
+ (get_class_def thy class)
in
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
accum
end
- else if is_constr thy stds x then
+ else if is_constr ctxt stds x then
accum
+ else if is_descr (original_name s) then
+ fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
+ accum
else if is_equational_fun hol_ctxt x then
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
accum
else if is_choice_spec_fun hol_ctxt x then
fold (add_nondef_axiom depth)
(nondef_props_for_const thy true choice_spec_table x) accum
- else if is_abs_fun thy x then
+ else if is_abs_fun ctxt x then
if is_quot_type thy (range_type T) then
raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
else
@@ -940,7 +947,7 @@
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
- else if is_rep_fun thy x then
+ else if is_rep_fun ctxt x then
if is_quot_type thy (domain_type T) then
raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
else
@@ -952,9 +959,11 @@
(nondef_props_for_const thy true
(extra_table def_table s) x)
|> add_axioms_for_term depth
- (Const (mate_of_rep_fun thy x))
+ (Const (mate_of_rep_fun ctxt x))
|> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun thy x)
+ (inverse_axioms_for_rep_fun ctxt x)
+ else if s = @{const_name TYPE} then
+ accum
else
accum |> user_axioms <> SOME false
? fold (add_nondef_axiom depth)
@@ -977,8 +986,8 @@
| TVar (_, S) => add_axioms_for_sort depth T S
| Type (z as (_, Ts)) =>
fold (add_axioms_for_type depth) Ts
- #> (if is_pure_typedef thy T then
- fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+ #> (if is_pure_typedef ctxt T then
+ fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
else if is_quot_type thy T then
fold (add_def_axiom depth)
(optimized_quot_type_axioms ctxt stds z)
@@ -1018,7 +1027,7 @@
(** Simplification of constructor/selector terms **)
-fun simplify_constrs_and_sels thy t =
+fun simplify_constrs_and_sels ctxt t =
let
fun is_nth_sel_on t' n (Const (s, _) $ t) =
(t = t' andalso is_sel_like_and_no_discr s andalso
@@ -1030,7 +1039,7 @@
$ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
| do_term (t as Const (x as (s, T))) (args as _ :: _) =
- ((if is_constr_like thy x then
+ ((if is_constr_like ctxt x then
if length args = num_binder_types T then
case hd args of
Const (_, T') $ t' =>
@@ -1046,7 +1055,7 @@
else if is_sel_like_and_no_discr s then
case strip_comb (hd args) of
(Const (x' as (s', T')), ts') =>
- if is_constr_like thy x' andalso
+ if is_constr_like ctxt x' andalso
constr_name_for_sel_like s = s' andalso
not (exists is_pair_type (binder_types T')) then
list_comb (nth ts' (sel_no_from_name s), tl args)
@@ -1228,7 +1237,7 @@
val max_skolem_depth = 4
-fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
+fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
boxes, ...}) finitizes monos t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1248,7 +1257,7 @@
val box = exists (not_equal (SOME false) o snd) boxes
val table =
Termtab.empty
- |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
+ |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
#> box ? uncurry_term table
@@ -1259,7 +1268,7 @@
#> curry_assms
#> destroy_universal_equalities
#> destroy_existential_equalities hol_ctxt
- #> simplify_constrs_and_sels thy
+ #> simplify_constrs_and_sels ctxt
#> distribute_quantifiers
#> push_quantifiers_inward
#> close_form
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Jun 02 13:18:48 2010 +0200
@@ -135,7 +135,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
fun quintuple_for_scope quote
- ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -144,8 +144,8 @@
card_assigns |> filter_out (member (op =) boring_Ts o fst)
|> List.partition (is_fp_iterator_type o fst)
val (secondary_card_assigns, primary_card_assigns) =
- card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
- o fst)
+ card_assigns
+ |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
val cards =
map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
string_of_int k)
@@ -458,13 +458,13 @@
concrete = concrete, deep = deep, constrs = constrs}
end
-fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
+fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
finitizable_dataTs (desc as (card_assigns, _)) =
let
val datatypes =
map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
finitizable_dataTs desc)
- (filter (is_datatype thy stds o fst) card_assigns)
+ (filter (is_datatype ctxt stds o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
card_of_type card_assigns @{typ unsigned_bit}
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Jun 02 13:18:48 2010 +0200
@@ -57,8 +57,15 @@
val bool_T : typ
val nat_T : typ
val int_T : typ
+ val simple_string_of_typ : typ -> string
+ val is_real_constr : theory -> string * typ -> bool
+ val typ_of_dtyp :
+ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
+ -> typ
+ val is_of_class_const : theory -> string * typ -> bool
+ val get_class_def : theory -> string -> (string * term) option
val monomorphic_term : Type.tyenv -> term -> term
- val specialize_type : theory -> (string * typ) -> term -> term
+ val specialize_type : theory -> string * typ -> term -> term
val nat_subscript : int -> string
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -229,15 +236,25 @@
val nat_T = @{typ nat}
val int_T = @{typ int}
+val simple_string_of_typ = Refute.string_of_typ
+val is_real_constr = Refute.is_IDT_constructor
+val typ_of_dtyp = Refute.typ_of_dtyp
+val is_of_class_const = Refute.is_const_of_class
+val get_class_def = Refute.get_classdef
val monomorphic_term = Sledgehammer_Util.monomorphic_term
val specialize_type = Sledgehammer_Util.specialize_type
-val subscript = implode o map (prefix "\<^isub>") o explode
+val i_subscript = implode o map (prefix "\<^isub>") o explode
+fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
fun nat_subscript n =
- (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
- numbers *)
- if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
- else subscript (string_of_int n)
+ let val s = signed_string_of_int n in
+ if print_mode_active Symbol.xsymbolsN then
+ (* cheap trick to ensure proper alphanumeric ordering for one- and
+ two-digit numbers *)
+ (if n <= 9 then be_subscript else i_subscript) s
+ else
+ s
+ end
fun time_limit NONE = I
| time_limit (SOME delay) = TimeLimit.timeLimit delay
--- a/src/HOL/Tools/inductive.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Jun 02 13:18:48 2010 +0200
@@ -719,8 +719,7 @@
Local_Theory.notes
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
map (fn th => [([th],
- [Attrib.internal (K (Context_Rules.intro_query NONE)),
- Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
+ [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), lthy2) =
lthy1 |>
--- a/src/HOL/Tools/refute.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/refute.ML Wed Jun 02 13:18:48 2010 +0200
@@ -1165,6 +1165,13 @@
val fm_u = (if negate then toFalse else toTrue) (hd intrs)
val fm_ax = PropLogic.all (map toTrue (tl intrs))
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
+ val _ =
+ (if satsolver = "dpll" orelse satsolver = "enumerate" then
+ warning ("Using SAT solver " ^ quote satsolver ^
+ "; for better performance, consider installing an \
+ \external solver.")
+ else
+ ());
val solver =
SatSolver.invoke_solver satsolver
handle Option.Option =>
--- a/src/HOL/Tools/sat_solver.ML Wed Jun 02 13:18:21 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML Wed Jun 02 13:18:48 2010 +0200
@@ -543,10 +543,6 @@
(* do not call solver "auto" from within "auto" *)
loop solvers
else (
- (if name="dpll" orelse name="enumerate" then
- warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
- else
- ());
(* apply 'solver' to 'fm' *)
solver fm
handle SatSolver.NOT_CONFIGURED => loop solvers