# HG changeset patch # User huffman # Date 1267023999 28800 # Node ID 0df9c8a37f64e0aa8c56cecf5197e9ebebefecb1 # Parent f9801fdeb7890e9630f3a8863c3438e238494d26# Parent 4dc65845eab3f426e7816a7807a1f55845387eaf merged diff -r f9801fdeb789 -r 0df9c8a37f64 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Feb 23 14:44:43 2010 -0800 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 07:06:39 2010 -0800 @@ -893,6 +893,9 @@ \item[iterations] sets how many sets of assignments are generated for each particular size. + \item[no\_assms] specifies whether assumptions in + structured proofs should be ignored. + \end{description} These option can be given within square brackets. diff -r f9801fdeb789 -r 0df9c8a37f64 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 14:44:43 2010 -0800 +++ b/doc-src/Nitpick/nitpick.tex Wed Feb 24 07:06:39 2010 -0800 @@ -1910,7 +1910,7 @@ (\S\ref{output-format}).} \optrue{assms}{no\_assms} -Specifies whether the relevant assumptions in structured proof should be +Specifies whether the relevant assumptions in structured proofs should be considered. The option is implicitly enabled for automatic runs. \nopagebreak @@ -2743,8 +2743,6 @@ \item[$\bullet$] Although this has never been observed, arbitrary theorem morphisms could possibly confuse Nitpick, resulting in spurious counterexamples. -\item[$\bullet$] Local definitions are not supported and result in an error. - %\item[$\bullet$] All constants and types whose names start with %\textit{Nitpick}{.} are reserved for internal use. \end{enum} diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Feb 24 07:06:39 2010 -0800 @@ -64,10 +64,8 @@ subsection {* Euclidean domains *} (* -axclass - euclidean < "domain" - - euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). +class euclidean = "domain" + + assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). a = b * q + r & e_size r < e_size b)" Nothing has been proved about Euclidean domains, yet. diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Feb 24 07:06:39 2010 -0800 @@ -14,8 +14,9 @@ ML {* exception FAIL -val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 -val def_table = Nitpick_HOL.const_def_table @{context} defs +val subst = [] +val defs = Nitpick_HOL.all_axioms_of @{theory} 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 = [], stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 24 07:06:39 2010 -0800 @@ -1381,25 +1381,16 @@ text {* A type class without axioms: *} -axclass classA +class classA lemma "P (x\'a\classA)" nitpick [expect = genuine] oops -text {* The axiom of this type class does not contain any type variables: *} - -axclass classB -classB_ax: "P \ \ P" - -lemma "P (x\'a\classB)" -nitpick [expect = genuine] -oops - text {* An axiom with a type variable (denoting types which have at least two elements): *} -axclass classC < type -classC_ax: "\x y. x \ y" +class classC = + assumes classC_ax: "\x y. x \ y" lemma "P (x\'a\classC)" nitpick [expect = genuine] @@ -1411,11 +1402,9 @@ text {* A type class for which a constant is defined: *} -consts -classD_const :: "'a \ 'a" - -axclass classD < type -classD_ax: "classD_const (classD_const x) = classD_const x" +class classD = + fixes classD_const :: "'a \ 'a" + assumes classD_ax: "classD_const (classD_const x) = classD_const x" lemma "P (x\'a\classD)" nitpick [expect = genuine] @@ -1423,16 +1412,12 @@ text {* A type class with multiple superclasses: *} -axclass classE < classC, classD +class classE = classC + classD lemma "P (x\'a\classE)" nitpick [expect = genuine] oops -lemma "P (x\'a\{classB, classE})" -nitpick [expect = genuine] -oops - text {* OFCLASS: *} lemma "OFCLASS('a\type, type_class)" @@ -1445,12 +1430,6 @@ apply intro_classes done -lemma "OFCLASS('a, classB_class)" -nitpick [expect = none] -apply intro_classes -apply simp -done - lemma "OFCLASS('a\type, classC_class)" nitpick [expect = genuine] oops diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/HISTORY Wed Feb 24 07:06:39 2010 -0800 @@ -2,6 +2,9 @@ * Added and implemented "binary_ints" and "bits" options * Added "std" option and implemented support for nonstandard models + * Added support for quotient types + * Added support for local definitions + * Optimized "Multiset.multiset" * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 24 07:06:39 2010 -0800 @@ -158,7 +158,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -304,7 +304,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -938,13 +938,13 @@ $$ "{" |-- scan_list scan_assignment --| $$ "}" (* string -> raw_bound list *) -fun parse_instance inst = - Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise SYNTAX ("Kodkod.parse_instance", - "ill-formed Kodkodi output")) - scan_instance)) - (strip_blanks (explode inst)) - |> fst +val parse_instance = + fst o Scan.finite Symbol.stopper + (Scan.error (!! (fn _ => + raise SYNTAX ("Kodkod.parse_instance", + "ill-formed Kodkodi output")) + scan_instance)) + o strip_blanks o explode val problem_marker = "*** PROBLEM " val outcome_marker = "---OUTCOME---\n" @@ -1029,7 +1029,7 @@ val reindex = fst o nth indexed_problems in if null indexed_problems then - Normal ([], triv_js) + Normal ([], triv_js, "") else let val (serial_str, temp_dir) = @@ -1089,6 +1089,8 @@ if null ps then if code = 2 then TimedOut js + else if code = 0 then + Normal ([], js, first_error) else if first_error |> Substring.full |> Substring.position "NoClassDefFoundError" |> snd |> Substring.isEmpty |> not then @@ -1098,12 +1100,10 @@ |> perhaps (try (unprefix "Error: ")), js) else if io_error then Error ("I/O error", js) - else if code <> 0 then + else Error ("Unknown error", js) - else - Normal ([], js) else - Normal (ps, js) + Normal (ps, js, first_error) end in remove_temporary_files (); outcome end handle Exn.Interrupt => diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 24 07:06:39 2010 -0800 @@ -321,7 +321,7 @@ in case solve_any_problem overlord NONE max_threads max_solutions problems of NotInstalled => "unknown" - | Normal ([], _) => "none" + | Normal ([], _, _) => "none" | Normal _ => "genuine" | TimedOut _ => "unknown" | Interrupted _ => "unknown" diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 24 07:06:39 2010 -0800 @@ -58,8 +58,8 @@ val register_codatatype : typ -> string -> styp list -> theory -> theory val unregister_codatatype : typ -> theory -> theory val pick_nits_in_term : - Proof.state -> params -> bool -> int -> int -> int -> term list -> term - -> string * Proof.state + Proof.state -> params -> bool -> int -> int -> int -> (term * term) list + -> term list -> term -> string * Proof.state val pick_nits_in_subgoal : Proof.state -> params -> bool -> int -> int -> string * Proof.state end; @@ -187,10 +187,10 @@ (* (unit -> string) -> Pretty.T *) fun plazy f = Pretty.blk (0, pstrs (f ())) -(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term - -> string * Proof.state *) +(* Time.time -> Proof.state -> params -> bool -> int -> int -> int + -> (term * term) list -> term list -> term -> string * Proof.state *) fun pick_them_nits_in_term deadline state (params : params) auto i n step - orig_assm_ts orig_t = + subst orig_assm_ts orig_t = let val timer = Timer.startRealTimer () val thy = Proof.theory_of state @@ -237,6 +237,7 @@ if passed_deadline deadline then raise TimeLimit.TimeOut else raise Interrupt + val orig_assm_ts = if assms orelse auto then orig_assm_ts else [] val _ = if step = 0 then print_m (fn () => "Nitpicking formula...") @@ -249,10 +250,7 @@ "goal")) [Logic.list_implies (orig_assm_ts, orig_t)])) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t - val assms_t = if assms orelse auto then - Logic.mk_conjunction_list (neg_t :: orig_assm_ts) - else - neg_t + val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts) val (assms_t, evals) = assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms |> pairf hd tl @@ -265,12 +263,12 @@ *) 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 - val def_table = const_def_table ctxt defs + val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy 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) - val psimp_table = const_psimp_table ctxt - val intro_table = inductive_intro_table ctxt def_table + val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) + val psimp_table = const_psimp_table ctxt subst + val intro_table = inductive_intro_table ctxt subst def_table val ground_thm_table = ground_theorem_table thy val ersatz_table = ersatz_table thy val (hol_ctxt as {wf_cache, ...}) = @@ -412,7 +410,7 @@ if sat_solver <> "smart" then if need_incremental andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) - sat_solver) then + sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") @@ -581,6 +579,9 @@ fun update_checked_problems problems = List.app (Unsynchronized.change checked_problems o Option.map o cons o nth problems) + (* string -> unit *) + fun show_kodkod_warning "" = () + | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") (* bool -> KK.raw_bound list -> problem_extension -> bool option *) fun print_and_check_model genuine bounds @@ -701,15 +702,16 @@ KK.NotInstalled => (print_m install_kodkodi_message; (max_potential, max_genuine, donno + 1)) - | KK.Normal ([], unsat_js) => - (update_checked_problems problems unsat_js; + | KK.Normal ([], unsat_js, s) => + (update_checked_problems problems unsat_js; show_kodkod_warning s; (max_potential, max_genuine, donno)) - | KK.Normal (sat_ps, unsat_js) => + | KK.Normal (sat_ps, unsat_js, s) => let val (lib_ps, con_ps) = List.partition (#unsound o snd o nth problems o fst) sat_ps in update_checked_problems problems (unsat_js @ map fst lib_ps); + show_kodkod_warning s; if null con_ps then let val num_genuine = take max_potential lib_ps @@ -937,10 +939,10 @@ else error "Nitpick was interrupted." -(* Proof.state -> params -> bool -> int -> int -> int -> term - -> string * Proof.state *) +(* Proof.state -> params -> bool -> int -> int -> int -> (term * term) list + -> term list -> term -> string * Proof.state *) fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n - step orig_assm_ts orig_t = + step subst orig_assm_ts orig_t = if getenv "KODKODI" = "" then (if auto then () else warning (Pretty.string_of (plazy install_kodkodi_message)); @@ -950,13 +952,27 @@ val deadline = Option.map (curry Time.+ (Time.now ())) timeout val outcome as (outcome_code, _) = time_limit (if debug then NONE else timeout) - (pick_them_nits_in_term deadline state params auto i n step + (pick_them_nits_in_term deadline state params auto i n step subst orig_assm_ts) orig_t in if expect = "" orelse outcome_code = expect then outcome else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") end +(* string list -> term -> bool *) +fun is_fixed_equation fixes + (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = + member (op =) fixes s + | is_fixed_equation _ _ = false +(* Proof.context -> term list * term -> (term * term) list * term list * term *) +fun extract_fixed_frees ctxt (assms, t) = + let + val fixes = Variable.fixes_of ctxt |> map snd + val (subst, other_assms) = + List.partition (is_fixed_equation fixes) assms + |>> map Logic.dest_equals + in (subst, other_assms, subst_atomic subst t) end + (* Proof.state -> params -> bool -> int -> int -> string * Proof.state *) fun pick_nits_in_subgoal state params auto i step = let @@ -967,12 +983,11 @@ 0 => (priority "No subgoal!"; ("none", state)) | n => let + val (t, frees) = Logic.goal_params t i + val t = subst_bounds (frees, t) val assms = map term_of (Assumption.all_assms_of ctxt) - val (t, frees) = Logic.goal_params t i - in - pick_nits_in_term state params auto i n step assms - (subst_bounds (frees, t)) - end + val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) + in pick_nits_in_term state params auto i n step subst assms t end end end; diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 24 07:06:39 2010 -0800 @@ -155,7 +155,8 @@ val is_finite_type : hol_context -> typ -> bool val special_bounds : term list -> (indexname * typ) list val is_funky_typedef : theory -> typ -> bool - val all_axioms_of : theory -> term list * term list * term list + val all_axioms_of : + theory -> (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 : @@ -163,11 +164,13 @@ val term_under_def : term -> term val case_const_names : theory -> (typ option * bool) list -> (string * int) list - val const_def_table : Proof.context -> term list -> const_table + val const_def_table : + Proof.context -> (term * term) list -> term list -> const_table val const_nondef_table : term list -> const_table - val const_simp_table : Proof.context -> const_table - val const_psimp_table : Proof.context -> const_table - val inductive_intro_table : Proof.context -> const_table -> const_table + val const_simp_table : Proof.context -> (term * term) list -> const_table + val const_psimp_table : Proof.context -> (term * term) list -> const_table + val inductive_intro_table : + Proof.context -> (term * term) list -> const_table -> const_table 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 @@ -619,12 +622,19 @@ fun is_univ_typedef thy (Type (s, _)) = (case typedef_info thy s of SOME {set_def, prop_of_Rep, ...} => - (case set_def of - SOME thm => - try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm - | NONE => - try (fst o dest_Const o snd o HOLogic.dest_mem - o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} + let + val t_opt = + case set_def of + SOME thm => try (snd o Logic.dest_equals o prop_of) thm + | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) + prop_of_Rep + in + case t_opt of + SOME (Const (@{const_name top}, _)) => true + | SOME (Const (@{const_name Collect}, _) + $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true + | _ => false + end | NONE => false) | is_univ_typedef _ _ = false (* theory -> (typ option * bool) list -> typ -> bool *) @@ -1166,11 +1176,12 @@ | do_eq _ = false in do_eq end -(* theory -> term list * term list * term list *) -fun all_axioms_of thy = +(* theory -> (term * term) list -> term list * term list * term list *) +fun all_axioms_of thy subst = let (* theory list -> term list *) - val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of) + val axioms_of_thys = + maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of)) val specs = Defs.all_specifications_of (Theory.defs_of thy) val def_names = specs |> maps snd |> map_filter #def |> OrdList.make fast_string_ord @@ -1317,12 +1328,13 @@ fun pair_for_prop t = case term_under_def t of Const (s, _) => (s, t) - | Free _ => raise NOT_SUPPORTED "local definitions" | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) -(* (Proof.context -> term list) -> Proof.context -> const_table *) -fun table_for get ctxt = - get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make +(* (Proof.context -> term list) -> Proof.context -> (term * term) list + -> const_table *) +fun table_for get ctxt subst = + ctxt |> get |> map (pair_for_prop o subst_atomic subst) + |> AList.group (op =) |> Symtab.make (* theory -> (typ option * bool) list -> (string * int) list *) fun case_const_names thy stds = @@ -1335,23 +1347,23 @@ (Datatype.get_all thy) [] @ map (apsnd length o snd) (#codatatypes (Data.get thy)) -(* Proof.context -> term list -> const_table *) -fun const_def_table ctxt ts = - table_for (map prop_of o Nitpick_Defs.get) ctxt +(* Proof.context -> (term * term) list -> term list -> const_table *) +fun const_def_table ctxt subst ts = + table_for (map prop_of o Nitpick_Defs.get) ctxt subst |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) (* term list -> const_table *) fun const_nondef_table ts = fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] |> AList.group (op =) |> Symtab.make -(* Proof.context -> const_table *) +(* Proof.context -> (term * term) list -> const_table *) val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) -(* Proof.context -> const_table -> const_table *) -fun inductive_intro_table ctxt def_table = +(* Proof.context -> (term * term) list -> const_table -> const_table *) +fun inductive_intro_table ctxt subst def_table = table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) def_table o prop_of) - o Nitpick_Intros.get) ctxt + o Nitpick_Intros.get) ctxt subst (* theory -> term list Inttab.table *) fun ground_theorem_table thy = fold ((fn @{const Trueprop} $ t1 => diff -r f9801fdeb789 -r 0df9c8a37f64 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 23 14:44:43 2010 -0800 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 24 07:06:39 2010 -0800 @@ -325,7 +325,7 @@ fun run_all_tests () = case Kodkod.solve_any_problem false NONE 0 1 (map (problem_for_nut @{context}) tests) of - Kodkod.Normal ([], _) => () + Kodkod.Normal ([], _, _) => () | _ => error "Tests failed" end;