# HG changeset patch # User blanchet # Date 1393882402 -3600 # Node ID cac1add157e8cb82b36612bcbceb8c7af81dd37c # Parent 25bd4745ee38ace9fa2388aabece6769f0636d72 removed nonstandard models from Nitpick diff -r 25bd4745ee38 -r cac1add157e8 src/Doc/Nitpick/document/root.tex --- 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} diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 \ Q" @@ -28,12 +30,14 @@ nitpick [expect = genuine] 2 oops + subsection {* 2.2. Type Variables *} lemma "x \ A \ (THE y. y \ A) \ A" nitpick [verbose, expect = genuine] oops + subsection {* 2.3. Constants *} lemma "x \ A \ (THE y. y \ A) \ A" @@ -47,6 +51,7 @@ (* sledgehammer *) by (metis the_equality) + subsection {* 2.4. Skolemization *} lemma "\g. \x. g (f x) = x \ \y. \x. y = f x" @@ -61,6 +66,7 @@ nitpick [expect = genuine] oops + subsection {* 2.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ 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\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\5, expect = none] sorry + subsection {* 2.10. Boxing *} datatype tm = Var nat | Lam tm | App tm tm @@ -247,6 +258,7 @@ nitpick [card = 1\5, expect = none] sorry + subsection {* 2.11. Scope Monotonicity *} lemma "length xs = length ys \ 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 \ reach \ 2 dvd n \ n \ 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 \ 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} \ labels t \ 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 \ labels t then - if b \ labels t then labels t else (labels t - {a}) \ {b} - else - if b \ labels t then (labels t - {b}) \ {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\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\5, expect = none] sorry + subsection {* 3.2. AA Trees *} datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 = diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/kodkod.ML --- 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. *) diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick.ML --- 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" ^ diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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 = diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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, ...} = diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 ^ ":") diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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]) diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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}