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