--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 11:21:37 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 11:35:39 2010 +0100
@@ -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.
--- a/doc-src/Nitpick/nitpick.tex Wed Feb 24 11:21:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Feb 24 11:35:39 2010 +0100
@@ -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}
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Feb 24 11:35:39 2010 +0100
@@ -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,
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 24 11:35:39 2010 +0100
@@ -1381,25 +1381,16 @@
text {* A type class without axioms: *}
-axclass classA
+class classA
lemma "P (x\<Colon>'a\<Colon>classA)"
nitpick [expect = genuine]
oops
-text {* The axiom of this type class does not contain any type variables: *}
-
-axclass classB
-classB_ax: "P \<or> \<not> P"
-
-lemma "P (x\<Colon>'a\<Colon>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: "\<exists>x y. x \<noteq> y"
+class classC =
+ assumes classC_ax: "\<exists>x y. x \<noteq> y"
lemma "P (x\<Colon>'a\<Colon>classC)"
nitpick [expect = genuine]
@@ -1411,11 +1402,9 @@
text {* A type class for which a constant is defined: *}
-consts
-classD_const :: "'a \<Rightarrow> 'a"
-
-axclass classD < type
-classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+ fixes classD_const :: "'a \<Rightarrow> 'a"
+ assumes classD_ax: "classD_const (classD_const x) = classD_const x"
lemma "P (x\<Colon>'a\<Colon>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\<Colon>'a\<Colon>classE)"
nitpick [expect = genuine]
oops
-lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
-nitpick [expect = genuine]
-oops
-
text {* OFCLASS: *}
lemma "OFCLASS('a\<Colon>type, type_class)"
--- a/src/HOL/Tools/Nitpick/HISTORY Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Wed Feb 24 11:35:39 2010 +0100
@@ -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
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 24 11:35:39 2010 +0100
@@ -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 =>
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 24 11:35:39 2010 +0100
@@ -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"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 24 11:35:39 2010 +0100
@@ -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;
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 24 11:35:39 2010 +0100
@@ -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 =>
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 24 11:21:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 24 11:35:39 2010 +0100
@@ -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;