--- a/src/Doc/Nitpick/document/root.tex Mon Mar 03 16:44:46 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex Mon Mar 03 22:33:22 2014 +0100
@@ -1384,121 +1384,6 @@
and this time \textit{arith} can finish off the subgoals.
-A similar technique can be employed for structural induction. The
-following mini formalization of full binary trees will serve as illustration:
-
-\prew
-\textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
-\textbf{primrec}~\textit{labels}~\textbf{where} \\
-``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
-``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
-\textbf{primrec}~\textit{swap}~\textbf{where} \\
-``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
-\phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
-``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
-\postw
-
-The \textit{labels} function returns the set of labels occurring on leaves of a
-tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
-labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
-obtained by swapping $a$ and $b$:
-
-\prew
-\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
-\postw
-
-Nitpick can't find any counterexample, so we proceed with induction
-(this time favoring a more structured style):
-
-\prew
-\textbf{proof}~(\textit{induct}~$t$) \\
-\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
-\textbf{next} \\
-\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
-\postw
-
-Nitpick can't find any counterexample at this point either, but it makes the
-following suggestion:
-
-\prew
-\slshape
-Hint: To check that the induction hypothesis is general enough, try this command:
-\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
-\postw
-
-If we follow the hint, we get a ``nonstandard'' counterexample for the step:
-
-\prew
-\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
-\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $a = a_1$ \\
-\hbox{}\qquad\qquad $b = a_2$ \\
-\hbox{}\qquad\qquad $t = \xi_1$ \\
-\hbox{}\qquad\qquad $u = \xi_2$ \\
-\hbox{}\qquad Datatype: \nopagebreak \\
-\hbox{}\qquad\qquad $'a~\textit{bin\_tree} =
-\{\!\begin{aligned}[t]
-& \xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \\[-2pt]
-& \textit{Branch}~\xi_1~\xi_2,\> \unr\}\end{aligned}$ \\
-\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{labels} = \unkef
- (\!\begin{aligned}[t]%
- & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
- & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
-\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \unkef
- (\!\begin{aligned}[t]%
- & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
- & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
-The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
-be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
-\postw
-
-Reading the Nitpick manual is a most excellent idea.
-But what's going on? The \textit{non\_std} option told the tool to look for
-nonstandard models of binary trees, which means that new ``nonstandard'' trees
-$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
-generated by the \textit{Leaf} and \textit{Branch} constructors.%
-\footnote{Notice the similarity between allowing nonstandard trees here and
-allowing unreachable states in the preceding example (by removing the ``$n \in
-\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
-set of objects over which the induction is performed while doing the step
-in order to test the induction hypothesis's strength.}
-Unlike standard trees, these new trees contain cycles. We will see later that
-every property of acyclic trees that can be proved without using induction also
-holds for cyclic trees. Hence,
-%
-\begin{quote}
-\textsl{If the induction
-hypothesis is strong enough, the induction step will hold even for nonstandard
-objects, and Nitpick won't find any nonstandard counterexample.}
-\end{quote}
-%
-But here the tool find some nonstandard trees $t = \xi_1$
-and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
-\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
-Because neither tree contains both $a$ and $b$, the induction hypothesis tells
-us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
-and as a result we know nothing about the labels of the tree
-$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
-$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
-labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
-\textit{labels}$ $(\textit{swap}~u~a~b)$.
-
-The solution is to ensure that we always know what the labels of the subtrees
-are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
-$t$ in the statement of the lemma:
-
-\prew
-\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
-\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
-\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
-\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
-\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
-\postw
-
-This time, Nitpick won't find any nonstandard counterexample, and we can perform
-the induction step using \textit{auto}.
-
\section{Case Studies}
\label{case-studies}
@@ -2172,15 +2057,6 @@
theoretical chance of finding a counterexample.
{\small See also \textit{mono} (\S\ref{scope-of-search}).}
-
-\opargbool{std}{type}{non\_std}
-Specifies whether the given (recursive) datatype should be given standard
-models. Nonstandard models are unsound but can help debug structural induction
-proofs, as explained in \S\ref{inductive-properties}.
-
-\optrue{std}{non\_std}
-Specifies the default standardness to use. This can be overridden on a per-type
-basis using the \textit{std}~\qty{type} option described above.
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 22:33:22 2014 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009-2013
+ Copyright 2009-2014
Examples from the Nitpick manual.
*)
@@ -15,10 +15,12 @@
imports Main Real "~~/src/HOL/Library/Quotient_Product"
begin
-chapter {* 2. First Steps *}
+
+section {* 2. First Steps *}
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+
subsection {* 2.1. Propositional Logic *}
lemma "P \<longleftrightarrow> Q"
@@ -28,12 +30,14 @@
nitpick [expect = genuine] 2
oops
+
subsection {* 2.2. Type Variables *}
lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
nitpick [verbose, expect = genuine]
oops
+
subsection {* 2.3. Constants *}
lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
@@ -47,6 +51,7 @@
(* sledgehammer *)
by (metis the_equality)
+
subsection {* 2.4. Skolemization *}
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
@@ -61,6 +66,7 @@
nitpick [expect = genuine]
oops
+
subsection {* 2.5. Natural Numbers and Integers *}
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
@@ -81,6 +87,7 @@
nitpick [card nat = 2, expect = none]
oops
+
subsection {* 2.6. Inductive Datatypes *}
lemma "hd (xs @ [y, y]) = hd xs"
@@ -92,6 +99,7 @@
nitpick [show_datatypes, expect = genuine]
oops
+
subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
definition "three = {0\<Colon>nat, 1, 2}"
@@ -149,6 +157,7 @@
nitpick [show_datatypes, expect = genuine]
oops
+
subsection {* 2.8. Inductive and Coinductive Predicates *}
inductive even where
@@ -191,6 +200,7 @@
nitpick [card nat = 4, show_consts, expect = genuine]
oops
+
subsection {* 2.9. Coinductive Datatypes *}
codatatype 'a llist = LNil | LCons 'a "'a llist"
@@ -211,6 +221,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry
+
subsection {* 2.10. Boxing *}
datatype tm = Var nat | Lam tm | App tm tm
@@ -247,6 +258,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry
+
subsection {* 2.11. Scope Monotonicity *}
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
@@ -258,6 +270,7 @@
nitpick [expect = genuine]
oops
+
subsection {* 2.12. Inductive Properties *}
inductive_set reach where
@@ -286,45 +299,12 @@
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
by (induct set: reach) arith+
-datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
-
-primrec labels where
-"labels (Leaf a) = {a}" |
-"labels (Branch t u) = labels t \<union> labels u"
-
-primrec swap where
-"swap (Leaf c) a b =
- (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
-"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
-
-lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
-(* nitpick *)
-proof (induct t)
- case Leaf thus ?case by simp
-next
- case (Branch t u) thus ?case
- (* nitpick *)
- nitpick [non_std, show_all, expect = genuine]
-oops
-
-lemma "labels (swap t a b) =
- (if a \<in> labels t then
- if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
- else
- if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
-(* nitpick *)
-proof (induct t)
- case Leaf thus ?case by simp
-next
- case (Branch t u) thus ?case
- nitpick [non_std, card = 1\<emdash>4, expect = none]
- by auto
-qed
section {* 3. Case Studies *}
nitpick_params [max_potential = 0]
+
subsection {* 3.1. A Context-Free Grammar *}
datatype alphabet = a | b
@@ -399,6 +379,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry
+
subsection {* 3.2. AA Trees *}
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Mar 03 22:33:22 2014 +0100
@@ -22,10 +22,9 @@
val thy = @{theory}
val ctxt = @{context}
-val stds = [(NONE, true)]
val subst = []
val tac_timeout = seconds 1.0
-val case_names = case_const_names ctxt stds
+val case_names = case_const_names ctxt
val defs = all_defs_of thy subst
val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
@@ -37,18 +36,17 @@
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {thy, ...} : hol_context =
- {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
- stds = stds, wfs = [], user_axioms = NONE, debug = false,
- whacks = [], binary_ints = SOME false, destroy_constrs = true,
- specialize = false, star_linear_preds = false, total_consts = NONE,
- needs = NONE, tac_timeout = tac_timeout, evals = [], case_names = case_names,
- def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
- unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
- constr_cache = Unsynchronized.ref []}
+ {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
+ user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
+ destroy_constrs = true, specialize = false, star_linear_preds = false,
+ total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
+ case_names = case_names, def_tables = def_tables,
+ nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
+ wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
val binarize = false
fun is_mono t =
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 03 22:33:22 2014 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/kodkod.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009, 2010
+ Copyright 2008-2014
ML interface for Kodkod.
*)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
@@ -21,7 +21,6 @@
boxes: (typ option * bool option) list,
finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
- stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
sat_solver: string,
blocking: bool,
@@ -107,7 +106,6 @@
boxes: (typ option * bool option) list,
finitizes: (typ option * bool option) list,
monos: (typ option * bool option) list,
- stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
sat_solver: string,
blocking: bool,
@@ -227,8 +225,8 @@
error "You must import the theory \"Nitpick\" to use Nitpick"
*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
- boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
- verbose, overlord, spy, user_axioms, assms, whacks, merge_type_vars,
+ boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
+ overlord, spy, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
total_consts, needs, peephole_optim, datatype_sym_break,
kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
@@ -291,7 +289,7 @@
val original_max_potential = max_potential
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
- val case_names = case_const_names ctxt stds
+ val case_names = case_const_names ctxt
val defs = def_assm_ts @ all_defs_of thy subst
val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
@@ -306,12 +304,11 @@
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {wf_cache, ...} =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
- stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
- whacks = whacks, binary_ints = binary_ints,
- destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, total_consts = total_consts,
- needs = needs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_tables = def_tables,
+ wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
+ binary_ints = binary_ints, destroy_constrs = destroy_constrs,
+ specialize = specialize, star_linear_preds = star_linear_preds,
+ total_consts = total_consts, needs = needs, tac_timeout = tac_timeout,
+ evals = evals, case_names = case_names, def_tables = def_tables,
nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
psimp_table = psimp_table, choice_spec_table = choice_spec_table,
intro_table = intro_table, ground_thm_table = ground_thm_table,
@@ -359,7 +356,6 @@
val (sel_names, nonsel_names) =
List.partition (is_sel o nickname_of) const_names
val sound_finitizes = none_true finitizes
- val standard = forall snd stds
(*
val _ =
List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
@@ -380,7 +376,7 @@
". " ^ extra))
end
fun is_type_fundamentally_monotonic T =
- (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
+ (is_datatype ctxt T andalso not (is_quot_type ctxt T) andalso
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type ctxt T orelse is_bit_type T
fun is_type_actually_monotonic T =
@@ -406,8 +402,7 @@
SOME (SOME b) => b
| _ => is_type_kind_of_monotonic T
fun is_datatype_deep T =
- not standard orelse T = @{typ unit} orelse T = nat_T orelse
- is_word_type T orelse
+ T = @{typ unit} orelse T = nat_T orelse is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
|> sort Term_Ord.typ_ord
@@ -416,7 +411,7 @@
exists (member (op =) [nat_T, int_T]) all_Ts then
print_v (K "The option \"binary_ints\" will be ignored because of the \
\presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
- \in the problem or because of the \"non_std\" option.")
+ \in the problem.")
else
()
val _ =
@@ -441,7 +436,7 @@
else
()
val (deep_dataTs, shallow_dataTs) =
- all_Ts |> filter (is_datatype ctxt stds)
+ all_Ts |> filter (is_datatype ctxt)
|> List.partition is_datatype_deep
val finitizable_dataTs =
(deep_dataTs |> filter_out (is_finite_type hol_ctxt)
@@ -454,26 +449,6 @@
"Nitpick can use a more precise finite encoding."))
else
()
- (* This detection code is an ugly hack. Fortunately, it is used only to
- provide a hint to the user. *)
- fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
- not (null fixes) andalso
- exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso
- exists (exists (curry (op =) name o shortest_name o fst)
- o datatype_constrs hol_ctxt) deep_dataTs
- val likely_in_struct_induct_step =
- exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
- val _ = if standard andalso likely_in_struct_induct_step then
- pprint_nt (fn () => Pretty.blk (0,
- pstrs "Hint: To check that the induction hypothesis is \
- \general enough, try this command: " @
- [Pretty.mark
- (Active.make_markup Markup.sendbackN
- {implicit = false, properties = [Markup.padding_command]})
- (Pretty.blk (0,
- pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
- else
- ()
(*
val _ = print_g "Monotonic types:"
val _ = List.app (print_g o string_for_type ctxt) mono_Ts
@@ -649,9 +624,7 @@
"scope.");
NONE)
- val das_wort_model =
- (if falsify then "counterexample" else "model")
- |> not standard ? prefix "nonstandard "
+ val das_wort_model = if falsify then "counterexample" else "model"
val scopes = Unsynchronized.ref []
val generated_scopes = Unsynchronized.ref []
@@ -704,7 +677,7 @@
Pretty.indent indent_size reconstructed_model]);
print_t (K "% SZS output end FiniteModel");
if genuine then
- (if check_genuine andalso standard then
+ (if check_genuine then
case prove_hol_model scope tac_timeout free_names sel_names
rel_table bounds (assms_prop ()) of
SOME true =>
@@ -722,13 +695,6 @@
| NONE => print "No confirmation by \"auto\"."
else
();
- if not standard andalso likely_in_struct_induct_step then
- print "The existence of a nonstandard model suggests that the \
- \induction hypothesis is not general enough or may even be \
- \wrong. See the Nitpick manual's \"Inductive Properties\" \
- \section for details (\"isabelle doc nitpick\")."
- else
- ();
if has_lonely_bool_var orig_t then
print "Hint: Maybe you forgot a colon after the lemma's name?"
else if has_syntactic_sorts orig_t then
@@ -1018,13 +984,8 @@
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_t (K "% SZS status Unknown");
- print_nt (fn () =>
- "Nitpick found no " ^ das_wort_model ^ "." ^
- (if not standard andalso likely_in_struct_induct_step then
- " This suggests that the induction hypothesis might be \
- \general enough to prove this subgoal."
- else
- "")); if skipped > 0 then unknownN else noneN)
+ print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
+ if skipped > 0 then unknownN else noneN)
else
(print_nt (fn () =>
excipit ("could not find a" ^
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 22:33:22 2014 +0100
@@ -48,7 +48,6 @@
("box", "smart"),
("finitize", "smart"),
("mono", "smart"),
- ("std", "true"),
("wf", "smart"),
("sat_solver", "smart"),
("batch_size", "smart"),
@@ -85,7 +84,6 @@
[("dont_box", "box"),
("dont_finitize", "finitize"),
("non_mono", "mono"),
- ("non_std", "std"),
("non_wf", "wf"),
("non_blocking", "blocking"),
("satisfy", "falsify"),
@@ -115,8 +113,7 @@
"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",
- "atoms"]
+ "mono", "non_mono", "wf", "non_wf", "format", "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -218,8 +215,6 @@
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 =
lookup_assigns read prefix "" (parse_bool_option true prefix)
fun lookup_strings_assigns read prefix =
@@ -247,7 +242,6 @@
val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
val monos = if mode = Auto_Try then [(NONE, SOME true)]
else lookup_bool_option_assigns read_type_polymorphic "mono"
- val stds = lookup_bool_assigns read_type_polymorphic "std"
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
val sat_solver = lookup_string "sat_solver"
val blocking = mode <> Normal orelse lookup_bool "blocking"
@@ -290,19 +284,24 @@
| NONE => if debug then 1 else 50
val expect = lookup_string "expect"
in
- {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns,
- bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes,
- monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
- falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy,
- user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars,
- binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, total_consts = total_consts, needs = needs,
- peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
- kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout,
- max_threads = max_threads, show_datatypes = show_datatypes, show_skolems = show_skolems,
- show_consts = show_consts, evals = evals, formats = formats, atomss = atomss,
- max_potential = max_potential, max_genuine = max_genuine, check_potential = check_potential,
- check_genuine = check_genuine, batch_size = batch_size, expect = expect}
+ {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
+ iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
+ boxes = boxes, finitizes = finitizes, monos = monos, wfs = wfs,
+ sat_solver = sat_solver, blocking = blocking, falsify = falsify,
+ debug = debug, verbose = verbose, overlord = overlord, spy = spy,
+ user_axioms = user_axioms, assms = assms, whacks = whacks,
+ merge_type_vars = merge_type_vars, binary_ints = binary_ints,
+ destroy_constrs = destroy_constrs, specialize = specialize,
+ star_linear_preds = star_linear_preds, total_consts = total_consts,
+ needs = needs, peephole_optim = peephole_optim,
+ datatype_sym_break = datatype_sym_break,
+ kodkod_sym_break = kodkod_sym_break, timeout = timeout,
+ tac_timeout = tac_timeout, max_threads = max_threads,
+ show_datatypes = show_datatypes, show_skolems = show_skolems,
+ show_consts = show_consts, evals = evals, formats = formats,
+ atomss = atomss, 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_hol.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 22:33:22 2014 +0100
@@ -18,7 +18,6 @@
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
- stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
@@ -114,12 +113,11 @@
val mk_flat_tuple : typ -> term list -> term
val dest_n_tuple : int -> term -> term list
val is_real_datatype : theory -> string -> bool
- val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
val is_codatatype : Proof.context -> typ -> bool
val is_quot_type : Proof.context -> 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_datatype : Proof.context -> typ -> bool
val is_record_constr : styp -> bool
val is_record_get : theory -> styp -> bool
val is_record_update : theory -> styp -> bool
@@ -130,7 +128,7 @@
val mate_of_rep_fun : Proof.context -> styp -> styp
val is_constr_like : Proof.context -> styp -> bool
val is_constr_like_injective : Proof.context -> styp -> bool
- val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
+ val is_constr : Proof.context -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
@@ -182,22 +180,17 @@
val s_betapplys : typ list -> term * term list -> term
val discriminate_value : hol_context -> styp -> term -> term
val select_nth_constr_arg :
- Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
- -> term
- val construct_value :
- Proof.context -> (typ option * bool) list -> styp -> term list -> term
+ Proof.context -> styp -> term -> int -> typ -> term
+ val construct_value : Proof.context -> styp -> term list -> term
val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
val special_bounds : term list -> (indexname * typ) list
val is_funky_typedef : Proof.context -> typ -> bool
val all_defs_of : theory -> (term * term) list -> term list
val all_nondefs_of : Proof.context -> (term * term) list -> term list
- val arity_of_built_in_const :
- theory -> (typ option * bool) list -> styp -> int option
- val is_built_in_const :
- theory -> (typ option * bool) list -> styp -> bool
+ val arity_of_built_in_const : styp -> int option
+ val is_built_in_const : styp -> bool
val term_under_def : term -> term
- val case_const_names :
- Proof.context -> (typ option * bool) list -> (string * int) list
+ val case_const_names : Proof.context -> (string * int) list
val unfold_defs_in_term : hol_context -> term -> term
val const_def_tables :
Proof.context -> (term * term) list -> term list
@@ -216,7 +209,7 @@
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
+ Proof.context -> string * typ list -> term list
val def_of_const : theory -> const_table * const_table -> styp -> term option
val fixpoint_kind_of_rhs : term -> fixpoint_kind
val fixpoint_kind_of_const :
@@ -259,7 +252,6 @@
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
- stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
@@ -397,14 +389,22 @@
(@{const_name is_unknown}, 1),
(@{const_name safe_The}, 1),
(@{const_name Nitpick.Frac}, 0),
- (@{const_name Nitpick.norm_frac}, 0)]
-val built_in_nat_consts =
- [(@{const_name Suc}, 0),
+ (@{const_name Nitpick.norm_frac}, 0),
+ (@{const_name Suc}, 0),
(@{const_name nat}, 0),
(@{const_name Nitpick.nat_gcd}, 0),
(@{const_name Nitpick.nat_lcm}, 0)]
val built_in_typed_consts =
- [((@{const_name zero_class.zero}, int_T), 0),
+ [((@{const_name zero_class.zero}, nat_T), 0),
+ ((@{const_name one_class.one}, nat_T), 0),
+ ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
+ ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
+ ((@{const_name of_nat}, nat_T --> int_T), 0),
+ ((@{const_name zero_class.zero}, int_T), 0),
((@{const_name one_class.one}, int_T), 0),
((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
@@ -413,16 +413,6 @@
((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
-val built_in_typed_nat_consts =
- [((@{const_name zero_class.zero}, nat_T), 0),
- ((@{const_name one_class.one}, nat_T), 0),
- ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
- ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
- ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
- ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
- ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
- ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
- ((@{const_name of_nat}, nat_T --> int_T), 0)]
val built_in_set_like_consts =
[(@{const_name ord_class.less_eq}, 2)]
@@ -583,14 +573,13 @@
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
-fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
(* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
-fun is_basic_datatype thy stds s =
+val is_basic_datatype =
member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
- @{type_name int}, @{type_name natural}, @{type_name integer}] s orelse
- (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
+ @{type_name nat}, @{type_name int}, @{type_name natural},
+ @{type_name integer}]
fun repair_constr_type (Type (_, Ts)) T =
snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T))))
@@ -626,14 +615,12 @@
fun register_codatatype_generic coT case_name constr_xs generic =
let
- val thy = Context.theory_of generic
val {frac_types, ersatz_table, codatatypes} = Data.get generic
val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs
val (co_s, coTs) = dest_Type coT
val _ =
if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
- co_s <> @{type_name fun} andalso
- not (is_basic_datatype thy [(NONE, true)] co_s) then
+ co_s <> @{type_name fun} andalso not (is_basic_datatype co_s) then
()
else
raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
@@ -696,13 +683,11 @@
end
| NONE => false)
| is_univ_typedef _ _ = false
-fun is_datatype ctxt stds (T as Type (s, _)) =
- let val thy = Proof_Context.theory_of ctxt in
- (is_typedef ctxt s orelse is_registered_type ctxt T orelse
- T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
- not (is_basic_datatype thy stds s)
- end
- | is_datatype _ _ _ = false
+fun is_datatype ctxt (T as Type (s, _)) =
+ (is_typedef ctxt s orelse is_registered_type ctxt T orelse
+ T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
+ not (is_basic_datatype s)
+ | is_datatype _ _ = false
fun all_record_fields thy T =
let val (recs, more) = Record.get_extT_fields thy T in
@@ -818,13 +803,10 @@
fun is_stale_constr ctxt (x as (s, T)) =
is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
-fun is_constr ctxt stds (x as (_, T)) =
- let val thy = Proof_Context.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 ctxt x)
- end
+fun is_constr ctxt (x as (_, T)) =
+ is_constr_like ctxt x andalso
+ not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
+ not (is_stale_constr ctxt x)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
String.isPrefix sel_prefix orf
@@ -927,7 +909,7 @@
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, ctxt, stds, ...} : hol_context)
+fun uncached_datatype_constrs ({thy, ctxt, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
s of
@@ -944,7 +926,7 @@
[(Abs_name,
varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
| NONE => [] (* impossible *)
- else if is_datatype ctxt stds T then
+ else if is_datatype ctxt T then
case Datatype.get_info thy s of
SOME {index, descr, ...} =>
let
@@ -1179,9 +1161,9 @@
else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
| _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
-fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
+fun nth_arg_sel_term_for_constr (x as (s, T)) n =
let val (arg_Ts, dataT) = strip_type T in
- if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
+ if dataT = nat_T then
@{term "%n::nat. n - 1"}
else if is_pair_type dataT then
Const (nth_sel_for_constr x n)
@@ -1199,30 +1181,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 ctxt stds x t n res_T =
- let val thy = Proof_Context.theory_of ctxt in
- (case strip_comb t of
- (Const x', args) =>
- if x = x' then
- if is_constr_like_injective ctxt x then nth args n else raise SAME ()
- else if is_constr_like ctxt x' then
- Const (@{const_name unknown}, res_T)
- else
- raise SAME ()
- | _ => raise SAME())
- handle SAME () =>
- s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
- end
+fun select_nth_constr_arg ctxt x t n res_T =
+ (case strip_comb t of
+ (Const x', args) =>
+ if x = x' then
+ if is_constr_like_injective ctxt x then nth args n else raise SAME ()
+ else if is_constr_like ctxt x' then
+ Const (@{const_name unknown}, res_T)
+ else
+ raise SAME ()
+ | _ => raise SAME())
+ handle SAME () => s_betapply [] (nth_arg_sel_term_for_constr x n, t)
-fun construct_value _ _ x [] = Const x
- | construct_value ctxt stds (x as (s, _)) args =
+fun construct_value _ x [] = Const x
+ | construct_value ctxt (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 ctxt stds x t n dummyT = t')
+ forall (fn (n, t') => select_nth_constr_arg ctxt x t n dummyT = t')
(index_seq 0 (length args) ~~ args) then
t
else
@@ -1230,7 +1208,7 @@
| _ => list_comb (Const x, args)
end
-fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
+fun constr_expand (hol_ctxt as {ctxt, ...}) T t =
(case head_of t of
Const x => if is_constr_like ctxt x then t else raise SAME ()
| _ => raise SAME ())
@@ -1245,7 +1223,7 @@
datatype_constrs hol_ctxt T |> hd
val arg_Ts = binder_types T'
in
- list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
+ list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t)
(index_seq 0 (length arg_Ts)) arg_Ts)
end
@@ -1257,7 +1235,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 {ctxt, stds, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t =
if old_T = new_T then
t
else
@@ -1271,7 +1249,7 @@
|> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
|> Envir.eta_contract
|> new_s <> @{type_name fun}
- ? construct_value ctxt stds
+ ? construct_value ctxt
(@{const_name FunBox},
Type (@{type_name fun}, new_Ts) --> new_T)
o single
@@ -1285,12 +1263,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 ctxt stds
+ construct_value ctxt
(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 ctxt stds
+ construct_value ctxt
(if new_s = @{type_name prod} 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]
@@ -1343,33 +1321,27 @@
|> filter_out (is_built_in_theory o theory_of_thm)
|> map (subst_atomic subst o prop_of)
-fun arity_of_built_in_const thy stds (s, T) =
+fun arity_of_built_in_const (s, T) =
if s = @{const_name If} then
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
else
- let val std_nats = is_standard_datatype thy stds nat_T in
- case AList.lookup (op =)
- (built_in_consts
- |> std_nats ? append built_in_nat_consts) s of
+ case AList.lookup (op =) built_in_consts s of
+ SOME n => SOME n
+ | NONE =>
+ case AList.lookup (op =) built_in_typed_consts (s, unarize_type T) of
SOME n => SOME n
| NONE =>
- case AList.lookup (op =)
- (built_in_typed_consts
- |> std_nats ? append built_in_typed_nat_consts)
- (s, unarize_type T) of
- SOME n => SOME n
- | NONE =>
- case s of
- @{const_name zero_class.zero} =>
- if is_iterator_type T then SOME 0 else NONE
- | @{const_name Suc} =>
- if is_iterator_type (domain_type T) then SOME 0 else NONE
- | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
- AList.lookup (op =) built_in_set_like_consts s
- else
- NONE
- end
-val is_built_in_const = is_some ooo arity_of_built_in_const
+ case s of
+ @{const_name zero_class.zero} =>
+ if is_iterator_type T then SOME 0 else NONE
+ | @{const_name Suc} =>
+ if is_iterator_type (domain_type T) then SOME 0 else NONE
+ | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
+ AList.lookup (op =) built_in_set_like_consts s
+ else
+ NONE
+
+val is_built_in_const = is_some o arity_of_built_in_const
(* This function is designed to work for both real definition axioms and
simplification rules (equational specifications). *)
@@ -1386,8 +1358,8 @@
(* Here we crucially rely on "specialize_type" performing a preorder traversal
of the term, without which the wrong occurrence of a constant could be
matched in the face of overloading. *)
-fun def_props_for_const thy stds table (x as (s, _)) =
- if is_built_in_const thy stds x then
+fun def_props_for_const thy table (x as (s, _)) =
+ if is_built_in_const x then
[]
else
these (Symtab.lookup table s)
@@ -1409,12 +1381,12 @@
in fold_rev aux args (SOME rhs) end
fun get_def_of_const thy table (x as (s, _)) =
- x |> def_props_for_const thy [(NONE, false)] table |> List.last
+ x |> def_props_for_const thy table |> List.last
|> normalized_rhs_of |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
- if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
+ if is_built_in_const x orelse original_name s <> s then
NONE
else case get_def_of_const thy unfold_table x of
SOME def => SOME (true, def)
@@ -1454,10 +1426,10 @@
| NONE => t)
| t => t)
-fun case_const_names ctxt stds =
+fun case_const_names ctxt =
let val thy = Proof_Context.theory_of ctxt in
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
- if is_basic_datatype thy stds dtype_s then
+ if is_basic_datatype dtype_s then
I
else
cons (case_name, AList.lookup (op =) descr index
@@ -1473,14 +1445,14 @@
end
fun fixpoint_kind_of_const thy table x =
- if is_built_in_const thy [(NONE, false)] x then NoFp
+ if is_built_in_const x then NoFp
else fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
- : hol_context) x =
+fun is_real_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
+ x =
fixpoint_kind_of_const thy def_tables x <> NoFp andalso
- not (null (def_props_for_const thy stds intro_table x))
+ not (null (def_props_for_const thy intro_table x))
fun is_inductive_pred hol_ctxt (x as (s, _)) =
is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
String.isPrefix lbfp_prefix s
@@ -1565,18 +1537,18 @@
exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
choice_spec_table
-fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...}
+fun is_real_equational_fun ({thy, simp_table, psimp_table, ...}
: hol_context) x =
- exists (fn table => not (null (def_props_for_const thy stds table x)))
+ exists (fn table => not (null (def_props_for_const thy table x)))
[!simp_table, psimp_table]
fun is_equational_fun_but_no_plain_def hol_ctxt =
is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
(** Constant unfolding **)
-fun constr_case_body ctxt stds Ts (func_t, (x as (_, T))) =
+fun constr_case_body ctxt Ts (func_t, (x as (_, T))) =
let val arg_Ts = binder_types T in
- s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
+ s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
fun add_constr_case res_T (body_t, guard_t) res_t =
@@ -1585,13 +1557,13 @@
else
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
$ guard_t $ body_t $ res_t
-fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) Ts dataT res_T func_ts =
+fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
let
val xs = datatype_constrs hol_ctxt dataT
val cases =
func_ts ~~ xs
|> map (fn (func_t, x) =>
- (constr_case_body ctxt stds (dataT :: Ts)
+ (constr_case_body ctxt (dataT :: Ts)
(incr_boundvars 1 func_t, x),
discriminate_value hol_ctxt x (Bound 0)))
|> AList.group (op aconv)
@@ -1613,7 +1585,7 @@
end
|> absdummy dataT
-fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, ctxt, ...}) 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
@@ -1622,14 +1594,14 @@
val rec_T' = List.last Ts
val j = num_record_fields thy rec_T - 1
in
- select_nth_constr_arg ctxt stds constr_x t j res_T
+ select_nth_constr_arg ctxt 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 ctxt stds constr_x t j res_T
+ | j => select_nth_constr_arg ctxt constr_x t j res_T
end
-fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
+fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
rec_t =
let
val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
@@ -1638,7 +1610,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 ctxt stds constr_x rec_t j T in
+ let val t = select_nth_constr_arg ctxt constr_x rec_t j T in
if j = special_j then
s_betapply [] (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
@@ -1660,7 +1632,7 @@
val def_inline_threshold_for_non_booleans = 20
fun unfold_defs_in_term
- (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
+ (hol_ctxt as {thy, ctxt, whacks, total_consts, case_names,
def_tables, ground_thm_table, ersatz_table, ...}) =
let
fun do_numeral depth Ts mult T some_t0 t1 t2 =
@@ -1675,8 +1647,7 @@
val s = numeral_prefix ^ signed_string_of_int j
in
if is_integer_like_type T then
- if is_standard_datatype thy stds T then Const (s, T)
- else funpow j (curry (op $) (suc_const T)) (zero_const T)
+ Const (s, T)
else
do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
$ Const (s, int_T))
@@ -1732,9 +1703,9 @@
t
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
- select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
+ select_nth_constr_arg ctxt x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
- (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
+ (select_nth_constr_arg ctxt x (do_term depth Ts t) n res_T, ts)
and quot_rep_of depth Ts abs_T rep_T ts =
select_nth_constr_arg_with_args depth Ts
(@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
@@ -1753,7 +1724,7 @@
else
def_inline_threshold_for_non_booleans
val (const, ts) =
- if is_built_in_const thy stds x then
+ if is_built_in_const x then
(Const x, ts)
else case AList.lookup (op =) case_names s of
SOME n =>
@@ -1769,7 +1740,7 @@
drop n ts)
end
| _ =>
- if is_constr ctxt stds x then
+ if is_constr ctxt x then
(Const x, ts)
else if is_stale_constr ctxt x then
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
@@ -1777,7 +1748,7 @@
else if is_quot_abs_fun ctxt x then
case T of
Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
- if is_basic_datatype thy [(NONE, true)] abs_s then
+ if is_basic_datatype abs_s then
raise NOT_SUPPORTED ("abstraction function on " ^
quote abs_s)
else
@@ -1788,7 +1759,7 @@
else if is_quot_rep_fun ctxt x then
case T of
Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
- if is_basic_datatype thy [(NONE, true)] abs_s then
+ if is_basic_datatype abs_s then
raise NOT_SUPPORTED ("representation function on " ^
quote abs_s)
else
@@ -1828,7 +1799,7 @@
end
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
+ if is_constr ctxt x' then
select_nth_constr_arg_with_args depth Ts x' ts 0
(range_type T)
else if is_quot_type ctxt (domain_type T) then
@@ -1993,7 +1964,7 @@
end
| NONE => []
end
-fun optimized_quot_type_axioms ctxt stds abs_z =
+fun optimized_quot_type_axioms ctxt abs_z =
let
val abs_T = Type abs_z
val rep_T = rep_type_for_quot_type ctxt abs_T
@@ -2002,7 +1973,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 ctxt stds x a_var 0 rep_T
+ val sel_a_t = select_nth_constr_arg ctxt x a_var 0 rep_T
val normal_fun =
Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
val normal_x = normal_fun $ x_var
@@ -2022,7 +1993,7 @@
|> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
end
-fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
val pred_T = T --> bool_T
@@ -2039,8 +2010,8 @@
fun nth_sub_bisim x n nth_T =
(if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
else HOLogic.eq_const 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
+ $ select_nth_constr_arg ctxt x x_var n nth_T
+ $ select_nth_constr_arg ctxt x y_var n nth_T
fun case_func (x as (_, T)) =
let
val arg_Ts = binder_types T
@@ -2102,9 +2073,9 @@
ScnpReconstruct.sizechange_tac]
fun uncached_is_well_founded_inductive_pred
- ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context)
+ ({thy, ctxt, debug, tac_timeout, intro_table, ...} : hol_context)
(x as (_, T)) =
- case def_props_for_const thy stds intro_table x of
+ case def_props_for_const thy intro_table x of
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
| intro_ts =>
@@ -2351,10 +2322,10 @@
else
raw_inductive_pred_axiom hol_ctxt x
-fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
+fun equational_fun_axioms (hol_ctxt as {thy, ctxt, def_tables, simp_table,
psimp_table, ...}) x =
- case def_props_for_const thy stds (!simp_table) x of
- [] => (case def_props_for_const thy stds psimp_table x of
+ case def_props_for_const thy (!simp_table) x of
+ [] => (case def_props_for_const thy psimp_table x of
[] => (if is_inductive_pred hol_ctxt x then
[inductive_pred_axiom hol_ctxt x]
else case def_of_const thy def_tables x of
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 22:33:22 2014 +0100
@@ -55,8 +55,7 @@
fun pull x xs = x :: filter_out (curry (op =) x) xs
-fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
- : datatype_spec) = true
+fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
| is_datatype_acyclic _ = false
fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
@@ -1499,7 +1498,6 @@
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
| nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
| nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
{typ, constrs, ...} =
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 22:33:22 2014 +0100
@@ -356,8 +356,8 @@
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
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, ...})
+ (scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
+ datatypes, ofs, ...})
atomss sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
@@ -507,7 +507,7 @@
| term_for_atom _ @{typ bool} _ j _ =
if j = 0 then @{const False} else @{const True}
| term_for_atom seen T _ j k =
- if T = nat_T andalso is_standard_datatype thy stds nat_T then
+ if T = nat_T then
HOLogic.mk_number nat_T j
else if T = int_T then
HOLogic.mk_number int_T (int_for_atom (k, 0) j)
@@ -518,7 +518,7 @@
else case datatype_spec datatypes T of
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, ...} =>
+ | SOME {co, constrs, ...} =>
let
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
@@ -553,9 +553,8 @@
map (map_filter (fn js => if hd js = real_j then SOME (tl js)
else NONE)) sel_jsss
val uncur_arg_Ts = binder_types constr_T
- val maybe_cyclic = co orelse not standard
in
- if maybe_cyclic andalso not (null seen) andalso
+ if co andalso not (null seen) andalso
member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
cyclic_var ()
else if constr_s = @{const_name Word} then
@@ -564,7 +563,7 @@
(value_of_bits (the_single arg_jsss))
else
let
- val seen = seen |> maybe_cyclic ? cons (T, j)
+ val seen = seen |> co ? cons (T, j)
val ts =
if length arg_Ts = 0 then
[]
@@ -587,16 +586,9 @@
else
list_comb (Const constr_x, ts)
in
- if maybe_cyclic then
+ if co then
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
- subst_atomic [(var, cyclic_atom ())] t
- else if exists_subterm (curry (op =) var) t then
+ 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,
@@ -876,7 +868,7 @@
end
fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
- ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
+ ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
star_linear_preds, total_consts, needs, tac_timeout,
evals, case_names, def_tables, nondef_table, nondefs,
@@ -892,12 +884,11 @@
add_wacky_syntax ctxt
val hol_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
- stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
- whacks = whacks, binary_ints = binary_ints,
- destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, total_consts = total_consts,
- needs = needs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_tables = def_tables,
+ wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
+ binary_ints = binary_ints, destroy_constrs = destroy_constrs,
+ specialize = specialize, star_linear_preds = star_linear_preds,
+ total_consts = total_consts, needs = needs, tac_timeout = tac_timeout,
+ evals = evals, case_names = case_names, def_tables = def_tables,
nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
psimp_table = psimp_table, choice_spec_table = choice_spec_table,
intro_table = intro_table, ground_thm_table = ground_thm_table,
@@ -960,14 +951,12 @@
else [Pretty.str (unrep ())]))]))
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- standard = true, self_rec = true, complete = (false, false),
- concrete = (true, true), deep = true, constrs = []}]
+ self_rec = true, complete = (false, false), concrete = (true, true),
+ deep = true, constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
datatypes |> filter #deep |> List.partition #co
- ||> append (integer_datatype int_T
- |> is_standard_datatype thy stds nat_T
- ? append (integer_datatype nat_T))
+ ||> append (integer_datatype nat_T @ integer_datatype int_T)
val block_of_datatypes =
if show_datatypes andalso not (null datatypes) then
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 22:33:22 2014 +0100
@@ -129,7 +129,7 @@
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
| could_exist_alpha_sub_mtype ctxt alpha_T T =
- (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
+ (T = alpha_T orelse is_datatype ctxt T)
fun exists_alpha_sub_mtype MAlpha = true
| exists_alpha_sub_mtype (MFun (M1, _, M2)) =
@@ -737,13 +737,11 @@
frame2)
end
-fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
- max_fresh, ...}) =
+fun consider_term (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, max_fresh, ...}) =
let
fun is_enough_eta_expanded t =
case strip_comb t of
- (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
- <= length ts
+ (Const x, ts) => the_default 0 (arity_of_built_in_const x) <= length ts
| _ => true
val mtype_for = fresh_mtype_for_type mdata false
fun mtype_for_set x T = MFun (mtype_for (pseudo_domain_type T), V x, bool_M)
@@ -894,9 +892,9 @@
do_fragile_set_operation T accum
else if is_sel s then
(mtype_for_sel mdata x, accum)
- else if is_constr ctxt stds x then
+ else if is_constr ctxt x then
(mtype_for_constr mdata x, accum)
- else if is_built_in_const thy stds x then
+ else if is_built_in_const x then
(fresh_mtype_for_type mdata true T, accum)
else
let val M = mtype_for T in
@@ -1074,20 +1072,20 @@
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
val bounteous_consts = [@{const_name bisim}]
-fun is_harmless_axiom ({hol_ctxt = {thy, stds, ...}, ...} : mdata) t =
- Term.add_consts t []
- |> filter_out (is_built_in_const thy stds)
- |> (forall (member (op =) harmless_consts o original_name o fst) orf
- exists (member (op =) bounteous_consts o fst))
+fun is_harmless_axiom t =
+ Term.add_consts t []
+ |> filter_out is_built_in_const
+ |> (forall (member (op =) harmless_consts o original_name o fst) orf
+ exists (member (op =) bounteous_consts o fst))
fun consider_nondefinitional_axiom mdata t =
- if is_harmless_axiom mdata t then I
+ if is_harmless_axiom t then I
else consider_general_formula mdata Plus t
fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...} : mdata) t =
if not (is_constr_pattern_formula ctxt t) then
consider_nondefinitional_axiom mdata t
- else if is_harmless_axiom mdata t then
+ else if is_harmless_axiom t then
I
else
let
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 22:33:22 2014 +0100
@@ -418,7 +418,7 @@
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq =
+fun nut_from_term (hol_ctxt as {ctxt, ...}) eq =
let
fun aux eq ss Ts t =
let
@@ -525,8 +525,8 @@
| (Const (@{const_name relcomp}, T), [t1, t2]) =>
Op2 (Composition, 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 x then Cst (Suc, T, Any)
- else if is_constr ctxt stds x then do_construct x []
+ if is_built_in_const x then Cst (Suc, T, Any)
+ else if is_constr ctxt 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
@@ -536,27 +536,27 @@
| _ => Op1 (Finite, bool_T, Any, sub t1))
| (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 x then Cst (Num 0, T, Any)
- else if is_constr ctxt stds x then do_construct x []
+ if is_built_in_const x then Cst (Num 0, T, Any)
+ else if is_constr ctxt 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 x then Cst (Num 1, T, Any)
+ if is_built_in_const x then Cst (Num 1, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
- if is_built_in_const thy stds x then Cst (Add, T, Any)
+ if is_built_in_const x then Cst (Add, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
- if is_built_in_const thy stds x then Cst (Subtract, T, Any)
+ if is_built_in_const x then Cst (Subtract, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name times_class.times}, T)), []) =>
- if is_built_in_const thy stds x then Cst (Multiply, T, Any)
+ if is_built_in_const x then Cst (Multiply, T, Any)
else ConstName (s, T, Any)
| (Const (x as (s as @{const_name div_class.div}, T)), []) =>
- if is_built_in_const thy stds x then Cst (Divide, T, Any)
+ if is_built_in_const x then Cst (Divide, T, Any)
else ConstName (s, T, Any)
| (t0 as Const (x as (@{const_name ord_class.less}, _)),
ts as [t1, t2]) =>
- if is_built_in_const thy stds x then
+ if is_built_in_const x then
Op2 (Less, bool_T, Any, sub t1, sub t2)
else
do_apply t0 ts
@@ -564,7 +564,7 @@
ts as [t1, t2]) =>
if is_set_like_type (domain_type T) then
Op2 (Subset, bool_T, Any, sub t1, sub t2)
- else if is_built_in_const thy stds x then
+ else if is_built_in_const x then
(* FIXME: find out if this case is necessary *)
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
else
@@ -572,7 +572,7 @@
| (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
| (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
| (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
- if is_built_in_const thy stds x then
+ if is_built_in_const x then
let val num_T = domain_type T in
Op2 (Apply, num_T --> num_T, Any,
Cst (Subtract, num_T --> num_T --> num_T, Any),
@@ -595,12 +595,12 @@
T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
Cst (NatToInt, T, Any)
| (t0 as Const (x as (s, T)), ts) =>
- if is_constr ctxt stds x then
+ if is_constr ctxt 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)
else
- (case arity_of_built_in_const thy stds x of
+ (case arity_of_built_in_const x of
SOME n =>
(case n - length ts of
0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 03 22:33:22 2014 +0100
@@ -70,13 +70,11 @@
fun add_to_uncurry_table ctxt t =
let
- val thy = Proof_Context.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)] x orelse
- is_constr_like ctxt x orelse
+ if is_built_in_const x orelse is_constr_like ctxt x orelse
is_sel s orelse s = @{const_name Sigma} then
table
else
@@ -126,7 +124,7 @@
(** Boxing **)
-fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, ...}) def orig_t =
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
@@ -229,7 +227,7 @@
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
T' --> T'
end
- else if is_built_in_const thy stds x orelse
+ else if is_built_in_const x orelse
s = @{const_name Sigma} then
T
else if is_constr_like ctxt x then
@@ -251,7 +249,7 @@
s_betapply new_Ts (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg ctxt stds
+ select_nth_constr_arg ctxt
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -268,7 +266,7 @@
s_betapply new_Ts (if s1 = @{type_name fun} then
t1
else
- select_nth_constr_arg ctxt stds
+ select_nth_constr_arg ctxt
(@{const_name FunBox},
Type (@{type_name fun}, Ts1) --> T1) t1 0
(Type (@{type_name fun}, Ts1)), t2)
@@ -306,12 +304,12 @@
| aux _ = true
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
- args seen =
+fun pull_out_constr_comb ({ctxt, ...} : 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 ctxt stds x andalso
+ if not relax andalso is_constr ctxt x andalso
not (is_fun_or_set_type (fastype_of1 (Ts, t_comb))) andalso
has_heavy_bounds_or_vars Ts t_comb andalso
not (loose_bvar (t_comb, level)) then
@@ -398,7 +396,7 @@
(list_comb (t, args), seen)
in aux [] 0 t [] [] |> fst end
-fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom strong t =
+fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, ...}) axiom strong t =
let
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
@@ -434,7 +432,7 @@
val n = length arg_Ts
in
if length args = n andalso
- (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
+ (is_constr ctxt 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
@@ -451,8 +449,7 @@
handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
else t0 $ aux Ts false t2 $ aux Ts false t1
and sel_eq Ts x t n nth_T nth_t =
- HOLogic.eq_const nth_T $ nth_t
- $ select_nth_constr_arg ctxt stds x t n nth_T
+ HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg ctxt x t n nth_T
|> aux Ts false
in aux [] axiom t end
@@ -487,7 +484,7 @@
aux (t1 :: prems) (Term.add_vars t1 zs) t2
in aux [] [] end
-fun find_bound_assign ctxt stds j =
+fun find_bound_assign ctxt j =
let
fun do_term _ [] = NONE
| do_term seen (t :: ts) =
@@ -500,7 +497,7 @@
| 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 ctxt stds
+ SOME (construct_value ctxt
(@{const_name FunBox}, T2 --> T1) [t2],
ts @ seen)
else
@@ -527,11 +524,11 @@
| aux _ = raise SAME ()
in aux (t, j) handle SAME () => t end
-fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
+fun destroy_existential_equalities ({ctxt, ...} : hol_context) =
let
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign ctxt stds (length ss) [] ts of
+ (case find_bound_assign ctxt (length ss) [] ts of
SOME (_, []) => @{const True}
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
@@ -731,7 +728,7 @@
forall (op aconv) (ts1 ~~ ts2)
fun specialize_consts_in_term
- (hol_ctxt as {ctxt, thy, stds, specialize, def_tables, simp_table,
+ (hol_ctxt as {ctxt, thy, specialize, def_tables, simp_table,
special_funs, ...}) def depth t =
if not specialize orelse depth > special_max_depth then
t
@@ -742,11 +739,11 @@
fun aux args Ts (Const (x as (s, T))) =
((if not (member (op =) blacklist x) andalso not (null args) andalso
not (String.isPrefix special_prefix s) andalso
- not (is_built_in_const thy stds x) andalso
+ not (is_built_in_const x) andalso
(is_equational_fun_but_no_plain_def hol_ctxt x orelse
(is_some (def_of_const thy def_tables x) andalso
not (is_of_class_const thy x) andalso
- not (is_constr ctxt stds x) andalso
+ not (is_constr ctxt x) andalso
not (is_choice_spec_fun hol_ctxt x))) then
let
val eligible_args =
@@ -895,9 +892,9 @@
val axioms_max_depth = 255
fun axioms_for_term
- (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
- evals, def_tables, nondef_table, choice_spec_table,
- nondefs, ...}) assm_ts neg_t =
+ (hol_ctxt as {thy, ctxt, max_bisim_depth, user_axioms, evals,
+ def_tables, nondef_table, choice_spec_table, nondefs,
+ ...}) assm_ts neg_t =
let
val (def_assm_ts, nondef_assm_ts) =
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
@@ -928,7 +925,7 @@
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if member (op aconv) seen t orelse is_built_in_const thy stds x then
+ (if member (op aconv) seen t orelse is_built_in_const x then
accum
else
let val accum = (t :: seen, axs) in
@@ -949,7 +946,7 @@
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
accum
end
- else if is_constr ctxt stds x then
+ else if is_constr ctxt x then
accum
else if is_descr (original_name s) then
fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
@@ -1017,8 +1014,7 @@
#> (if is_pure_typedef ctxt T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
else if is_quot_type ctxt T then
- fold (add_def_axiom depth)
- (optimized_quot_type_axioms ctxt stds z)
+ fold (add_def_axiom depth) (optimized_quot_type_axioms ctxt z)
else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then
fold (add_maybe_def_axiom depth)
(codatatype_bisim_axioms hol_ctxt T)
@@ -1253,8 +1249,8 @@
val max_skolem_depth = 3
fun preprocess_formulas
- (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
- needs, ...}) assm_ts neg_t =
+ (hol_ctxt as {ctxt, binary_ints, destroy_constrs, boxes, needs, ...})
+ assm_ts neg_t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
neg_t |> unfold_defs_in_term hol_ctxt
@@ -1263,7 +1259,6 @@
|> specialize_consts_in_term hol_ctxt false 0
|> axioms_for_term hol_ctxt assm_ts
val binarize =
- is_standard_datatype thy stds nat_T andalso
case binary_ints of
SOME false => false
| _ => forall (may_use_binary_ints false) nondef_ts andalso
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 22:33:22 2014 +0100
@@ -22,7 +22,6 @@
{typ: typ,
card: int,
co: bool,
- standard: bool,
self_rec: bool,
complete: bool * bool,
concrete: bool * bool,
@@ -76,7 +75,6 @@
{typ: typ,
card: int,
co: bool,
- standard: bool,
self_rec: bool,
complete: bool * bool,
concrete: bool * bool,
@@ -142,7 +140,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
fun quintuple_for_scope code_type code_term code_string
- ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -152,7 +150,7 @@
|> 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 ctxt stds) o fst)
+ |> List.partition ((is_integer_type orf is_datatype ctxt) o fst)
val cards =
map (fn (T, k) =>
[code_type ctxt T, code_string (" = " ^ string_of_int k)])
@@ -433,13 +431,12 @@
card_assigns T
end
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ctxt, stds, ...})
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
(T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype ctxt T
- val standard = is_standard_datatype thy stds T
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
@@ -459,21 +456,21 @@
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
- fold_rev (add_constr_spec desc (not co andalso standard) card
- sum_dom_cards num_self_recs num_non_self_recs)
+ fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs
+ num_non_self_recs)
(sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
- {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
- complete = complete, concrete = concrete, deep = deep, constrs = constrs}
+ {typ = T, card = card, co = co, self_rec = self_rec, complete = complete,
+ concrete = concrete, deep = deep, constrs = constrs}
end
-fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
+fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) 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 ctxt stds o fst) card_assigns)
+ (filter (is_datatype ctxt 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}