# HG changeset patch # User blanchet # Date 1284463458 -7200 # Node ID 6f49c7fbb1b1abdbc3b5256d657fafd300ad5f5d # Parent 6bc2f7971df0edc53e9a4188ed3d0999c190b142 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Sep 14 12:52:50 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Tue Sep 14 13:24:18 2010 +0200 @@ -296,40 +296,18 @@ \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ \hbox{}\qquad\qquad $x = a_3$ \\ \hbox{}\qquad Constant: \nopagebreak \\ -\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$ +\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ \postw -We can see more clearly now. Since the predicate $P$ isn't true for a unique -value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even -$a_1$. Since $P~a_1$ is false, the entire formula is falsified. - -As an optimization, Nitpick's preprocessor introduced the special constant -``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e., -$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$ -satisfying $P~y$. We disable this optimization by passing the -\textit{full\_descrs} option: +As the result of an optimization, Nitpick directly assigned a value to the +subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we +disable this optimization by using the command \prew -\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount] -\slshape -Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] -\hbox{}\qquad Free variables: \nopagebreak \\ -\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ -\hbox{}\qquad\qquad $x = a_3$ \\ -\hbox{}\qquad Constant: \nopagebreak \\ -\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ +\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}] \postw -As the result of another optimization, Nitpick directly assigned a value to the -subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we -disable this second optimization by using the command - -\prew -\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\, -\textit{show\_consts}] -\postw - -we finally get \textit{The}: +we get \textit{The}: \prew \slshape Constant: \nopagebreak \\ @@ -2490,13 +2468,6 @@ {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug} (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).} -\optrue{fast\_descrs}{full\_descrs} -Specifies whether Nitpick should optimize the definite and indefinite -description operators (THE and SOME). The optimized versions usually help -Nitpick generate more counterexamples or at least find them faster, but only the -unoptimized versions are complete when all types occurring in the formula are -finite. - {\small See also \textit{debug} (\S\ref{output-format}).} \opnodefault{whack}{term\_list} diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Sep 14 13:24:18 2010 +0200 @@ -892,7 +892,7 @@ nitpick [expect = none] sorry -nitpick_params [full_descrs, max_potential = 1] +nitpick_params [max_potential = 1] lemma "(THE j. j > Suc 2 \ j \ 3) \ 0" nitpick [card nat = 2, expect = potential] @@ -940,7 +940,7 @@ nitpick [card nat = 6, expect = none] sorry -nitpick_params [fast_descrs, max_potential = 0] +nitpick_params [max_potential = 0] subsection {* Destructors and Recursors *} diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Sep 14 13:24:18 2010 +0200 @@ -21,8 +21,8 @@ {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false, destroy_constrs = false, - specialize = false, star_linear_preds = false, fast_descrs = false, - tac_timeout = NONE, evals = [], case_names = [], def_table = def_table, + specialize = false, star_linear_preds = false, tac_timeout = NONE, + evals = [], case_names = [], def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, choice_spec_table = Symtab.empty, intro_table = Symtab.empty, diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 13:24:18 2010 +0200 @@ -34,7 +34,6 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, - fast_descrs: bool, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -108,7 +107,6 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, - fast_descrs: bool, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -207,10 +205,10 @@ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, user_axioms, assms, whacks, merge_type_vars, binary_ints, destroy_constrs, specialize, star_linear_preds, - fast_descrs, peephole_optim, datatype_sym_break, kodkod_sym_break, - tac_timeout, max_threads, show_datatypes, show_consts, evals, formats, - atomss, max_potential, max_genuine, check_potential, check_genuine, - batch_size, ...} = params + peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout, + max_threads, show_datatypes, show_consts, evals, formats, atomss, + max_potential, max_genuine, check_potential, check_genuine, batch_size, + ...} = params val state_ref = Unsynchronized.ref state val pprint = if auto then @@ -280,14 +278,13 @@ 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, fast_descrs = fast_descrs, - tac_timeout = tac_timeout, evals = evals, case_names = case_names, - def_table = def_table, nondef_table = nondef_table, - user_nondefs = user_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 [], + star_linear_preds = star_linear_preds, tac_timeout = tac_timeout, + evals = evals, case_names = case_names, def_table = def_table, + nondef_table = nondef_table, user_nondefs = user_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 pseudo_frees = fold Term.add_frees assm_ts [] diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:24:18 2010 +0200 @@ -27,7 +27,6 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, - fast_descrs: bool, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, @@ -181,9 +180,9 @@ val all_axioms_of : Proof.context -> (term * term) list -> term list * term list * term list val arity_of_built_in_const : - theory -> (typ option * bool) list -> bool -> styp -> int option + theory -> (typ option * bool) list -> styp -> int option val is_built_in_const : - theory -> (typ option * bool) list -> bool -> styp -> bool + theory -> (typ option * bool) list -> styp -> bool val term_under_def : term -> term val case_const_names : Proof.context -> (typ option * bool) list -> (string * int) list @@ -254,7 +253,6 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, - fast_descrs: bool, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, @@ -434,9 +432,6 @@ (@{const_name nat}, 0), (@{const_name nat_gcd}, 0), (@{const_name nat_lcm}, 0)] -val built_in_descr_consts = - [(@{const_name The}, 1), - (@{const_name Eps}, 1)] val built_in_typed_consts = [((@{const_name zero_class.zero}, int_T), 0), ((@{const_name one_class.one}, int_T), 0), @@ -1317,15 +1312,14 @@ user_defs @ built_in_defs in (defs, built_in_nondefs, user_nondefs) end -fun arity_of_built_in_const thy stds fast_descrs (s, T) = +fun arity_of_built_in_const thy stds (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 - |> fast_descrs ? append built_in_descr_consts) s of + |> std_nats ? append built_in_nat_consts) s of SOME n => SOME n | NONE => case AList.lookup (op =) @@ -1344,7 +1338,7 @@ else NONE end -val is_built_in_const = is_some oooo arity_of_built_in_const +val is_built_in_const = is_some ooo arity_of_built_in_const (* This function is designed to work for both real definition axioms and simplification rules (equational specifications). *) @@ -1361,8 +1355,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 fast_descrs table (x as (s, _)) = - if is_built_in_const thy stds fast_descrs x then +fun def_props_for_const thy stds table (x as (s, _)) = + if is_built_in_const thy stds x then [] else these (Symtab.lookup table s) @@ -1384,12 +1378,11 @@ in fold_rev aux args (SOME rhs) end fun def_of_const thy table (x as (s, _)) = - if is_built_in_const thy [(NONE, false)] false x orelse + if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then NONE else - x |> def_props_for_const thy [(NONE, false)] false table - |> List.last + x |> def_props_for_const thy [(NONE, false)] table |> List.last |> normalized_rhs_of |> Option.map (prefix_abs_vars s) handle List.Empty => NONE @@ -1438,16 +1431,14 @@ end fun fixpoint_kind_of_const thy table x = - if is_built_in_const thy [(NONE, false)] false x then - NoFp - else - fixpoint_kind_of_rhs (the (def_of_const thy table x)) - handle Option.Option => NoFp + if is_built_in_const thy [(NONE, false)] 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, fast_descrs, def_table, intro_table, - ...} : hol_context) x = +fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...} + : hol_context) x = fixpoint_kind_of_const thy def_table x <> NoFp andalso - not (null (def_props_for_const thy stds fast_descrs intro_table x)) + not (null (def_props_for_const thy stds 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 @@ -1532,10 +1523,9 @@ exists (curry (op aconv) t o axiom_for_choice_spec thy) ts) choice_spec_table -fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table, - ...} : hol_context) x = - exists (fn table => not (null (def_props_for_const thy stds fast_descrs table - x))) +fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...} + : hol_context) x = + exists (fn table => not (null (def_props_for_const thy stds 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 @@ -1625,8 +1615,8 @@ val def_inline_threshold_for_non_booleans = 20 fun unfold_defs_in_term - (hol_ctxt as {thy, ctxt, stds, whacks, fast_descrs, case_names, - def_table, ground_thm_table, ersatz_table, ...}) = + (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table, + ground_thm_table, ersatz_table, ...}) = let fun do_term depth Ts t = case t of @@ -1702,7 +1692,7 @@ else def_inline_threshold_for_non_booleans val (const, ts) = - if is_built_in_const thy stds fast_descrs x then + if is_built_in_const thy stds x then (Const x, ts) else case AList.lookup (op =) case_names s of SOME n => @@ -2046,9 +2036,9 @@ ScnpReconstruct.sizechange_tac] fun uncached_is_well_founded_inductive_pred - ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...} - : hol_context) (x as (_, T)) = - case def_props_for_const thy stds fast_descrs intro_table x of + ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context) + (x as (_, T)) = + case def_props_for_const thy stds intro_table x of [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive", [Const x]) | intro_ts => @@ -2281,10 +2271,10 @@ else raw_inductive_pred_axiom hol_ctxt x -fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, fast_descrs, def_table, - simp_table, psimp_table, ...}) x = - case def_props_for_const thy stds fast_descrs (!simp_table) x of - [] => (case def_props_for_const thy stds fast_descrs psimp_table x of +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, 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 [] => (if is_inductive_pred hol_ctxt x then [inductive_pred_axiom hol_ctxt x] else case def_of_const thy def_table x of diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Sep 14 13:24:18 2010 +0200 @@ -58,7 +58,6 @@ ("destroy_constrs", "true"), ("specialize", "true"), ("star_linear_preds", "true"), - ("fast_descrs", "true"), ("peephole_optim", "true"), ("datatype_sym_break", "5"), ("kodkod_sym_break", "15"), @@ -91,7 +90,6 @@ ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), ("dont_star_linear_preds", "star_linear_preds"), - ("full_descrs", "fast_descrs"), ("no_peephole_optim", "peephole_optim"), ("no_debug", "debug"), ("quiet", "verbose"), @@ -251,7 +249,6 @@ val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" val star_linear_preds = lookup_bool "star_linear_preds" - val fast_descrs = lookup_bool "fast_descrs" val peephole_optim = lookup_bool "peephole_optim" val datatype_sym_break = lookup_int "datatype_sym_break" val kodkod_sym_break = lookup_int "kodkod_sym_break" @@ -282,8 +279,8 @@ 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, fast_descrs = fast_descrs, - peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, + star_linear_preds = star_linear_preds, 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_consts = show_consts, diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:24:18 2010 +0200 @@ -872,9 +872,9 @@ fun reconstruct_hol_model {show_datatypes, show_consts} ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, debug, whacks, binary_ints, destroy_constrs, specialize, - star_linear_preds, fast_descrs, tac_timeout, evals, - case_names, def_table, nondef_table, user_nondefs, - simp_table, psimp_table, choice_spec_table, intro_table, + star_linear_preds, tac_timeout, evals, case_names, + def_table, nondef_table, user_nondefs, simp_table, + psimp_table, choice_spec_table, intro_table, ground_thm_table, ersatz_table, skolems, special_funs, unrolled_preds, wf_cache, constr_cache}, binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope) @@ -889,15 +889,15 @@ 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, fast_descrs = fast_descrs, - tac_timeout = tac_timeout, evals = evals, case_names = case_names, - def_table = def_table, nondef_table = nondef_table, - user_nondefs = user_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 = skolems, - special_funs = special_funs, unrolled_preds = unrolled_preds, - wf_cache = wf_cache, constr_cache = constr_cache} + star_linear_preds = star_linear_preds, tac_timeout = tac_timeout, + evals = evals, case_names = case_names, def_table = def_table, + nondef_table = nondef_table, user_nondefs = user_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 = skolems, special_funs = special_funs, + unrolled_preds = unrolled_preds, wf_cache = wf_cache, + constr_cache = constr_cache} val scope = {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:24:18 2010 +0200 @@ -549,13 +549,12 @@ consts = consts} handle List.Empty => initial_gamma (* FIXME: needed? *) -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...}, - alpha_T, max_fresh, ...}) = +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, 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 fast_descrs x) + (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x) <= length ts | _ => true val mtype_for = fresh_mtype_for_type mdata false @@ -725,7 +724,7 @@ (mtype_for_sel mdata x, accum) else if is_constr ctxt stds x then (mtype_for_constr mdata x, accum) - else if is_built_in_const thy stds fast_descrs x then + else if is_built_in_const thy stds x then (fresh_mtype_for_type mdata true T, accum) else let val M = mtype_for T in @@ -908,9 +907,9 @@ val bounteous_consts = [@{const_name bisim}] fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false - | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t = + | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t = Term.add_consts t [] - |> filter_out (is_built_in_const thy stds fast_descrs) + |> 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)) @@ -1022,8 +1021,7 @@ fun fin_fun_constr T1 T2 = (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2])) -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache, - ...}) +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize finitizes alpha_T tsp = case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of SOME (lits, msp, constr_mtypes) => @@ -1074,7 +1072,7 @@ | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\ \term_from_mterm", [T, T'], []) in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end - else if is_built_in_const thy stds fast_descrs x then + else if is_built_in_const thy stds x then coerce_term hol_ctxt new_Ts T' T t else if is_constr ctxt stds x then Const (finitize_constr x) diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:24:18 2010 +0200 @@ -430,7 +430,7 @@ maps factorize [mk_fst z, mk_snd z] | factorize z = [z] -fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq = +fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq = let fun aux eq ss Ts t = let @@ -470,12 +470,6 @@ val t1 = list_comb (t0, ts') val T1 = fastype_of1 (Ts, t1) in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end - fun do_description_operator oper undef_s (x as (_, T)) t1 = - if fast_descrs then - Op2 (oper, range_type T, Any, sub t1, - sub (Const (undef_s, range_type T))) - else - do_apply (Const x) [t1] fun do_construct (x as (_, T)) ts = case num_binder_types T - length ts of 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any)) @@ -511,10 +505,6 @@ do_quantifier Exist s T t1 | (t0 as Const (@{const_name Ex}, _), [t1]) => sub' (t0 $ eta_expand Ts t1 1) - | (Const (x as (@{const_name The}, _)), [t1]) => - do_description_operator The @{const_name undefined_fast_The} x t1 - | (Const (x as (@{const_name Eps}, _)), [t1]) => - do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name HOL.eq}, T), [t1]) => Op1 (SingletonSet, range_type T, Any, sub t1) | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2 @@ -549,7 +539,7 @@ | (Const (@{const_name image}, T), [t1, t2]) => Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (x as (s as @{const_name Suc}, T)), []) => - if is_built_in_const thy stds false x then Cst (Suc, T, Any) + if is_built_in_const thy stds x then Cst (Suc, T, Any) else if is_constr ctxt stds x then do_construct x [] else ConstName (s, T, Any) | (Const (@{const_name finite}, T), [t1]) => @@ -560,27 +550,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 false x then Cst (Num 0, T, Any) + 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 [] else ConstName (s, T, Any) | (Const (x as (s as @{const_name one_class.one}, T)), []) => - if is_built_in_const thy stds false x then Cst (Num 1, T, Any) + if is_built_in_const thy stds 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 false x then Cst (Add, T, Any) + if is_built_in_const thy stds 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 false x then Cst (Subtract, T, Any) + if is_built_in_const thy stds 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 false x then Cst (Multiply, T, Any) + if is_built_in_const thy stds 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 false x then Cst (Divide, T, Any) + if is_built_in_const thy stds 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 false x then + if is_built_in_const thy stds x then Op2 (Less, bool_T, Any, sub t1, sub t2) else do_apply t0 ts @@ -592,14 +582,14 @@ (* FIXME: find out if this case is necessary *) | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)), ts as [t1, t2]) => - if is_built_in_const thy stds false x then + if is_built_in_const thy stds x then Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) else do_apply t0 ts | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any) | (Const (@{const_name 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 false x then + if is_built_in_const thy stds 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), @@ -613,8 +603,6 @@ | (Const (@{const_name safe_The}, Type (@{type_name fun}, [_, T2])), [t1]) => Op1 (SafeThe, T2, Any, sub t1) - | (Const (x as (@{const_name safe_Eps}, _)), [t1]) => - do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => @@ -628,7 +616,7 @@ 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 fast_descrs x of + (case arity_of_built_in_const thy stds x of SOME n => (case n - length ts of 0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t]) diff -r 6bc2f7971df0 -r 6f49c7fbb1b1 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 12:52:50 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:24:18 2010 +0200 @@ -76,7 +76,7 @@ let val table = aux t2 [] table in aux t1 (t2 :: args) table end | aux (Abs (_, _, t')) _ table = aux t' [] table | aux (t as Const (x as (s, _))) args table = - if is_built_in_const thy [(NONE, true)] true x orelse + if is_built_in_const thy [(NONE, true)] x orelse is_constr_like ctxt x orelse is_sel s orelse s = @{const_name Sigma} then table @@ -127,8 +127,7 @@ (** Boxing **) -fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...}) - def orig_t = +fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t = let fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = Type (@{type_name fun}, map box_relational_operator_type Ts) @@ -231,7 +230,7 @@ let val T' = box_type hol_ctxt InFunLHS (domain_type T) in T' --> T' end - else if is_built_in_const thy stds fast_descrs x orelse + else if is_built_in_const thy stds x orelse s = @{const_name Sigma} then T else if is_constr_like ctxt x then @@ -732,8 +731,8 @@ forall (op aconv) (ts1 ~~ ts2) fun specialize_consts_in_term - (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table, - simp_table, special_funs, ...}) def depth t = + (hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table, + special_funs, ...}) def depth t = if not specialize orelse depth > special_max_depth then t else @@ -743,7 +742,7 @@ 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 fast_descrs x) andalso + not (is_built_in_const thy stds x) andalso (is_equational_fun_but_no_plain_def hol_ctxt x orelse (is_some (def_of_const thy def_table x) andalso not (is_of_class_const thy x) andalso @@ -894,8 +893,8 @@ fun axioms_for_term (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, - fast_descrs, evals, def_table, nondef_table, - choice_spec_table, user_nondefs, ...}) assm_ts neg_t = + evals, def_table, nondef_table, choice_spec_table, + user_nondefs, ...}) assm_ts neg_t = let val (def_assm_ts, nondef_assm_ts) = List.partition (assumption_exclusively_defines_free assm_ts) assm_ts @@ -926,8 +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 fast_descrs x then + (if member (op aconv) seen t orelse is_built_in_const thy stds x then accum else let val accum = (t :: seen, axs) in