--- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 16:53:13 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 19:10:25 2010 +0100
@@ -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/Tools/Nitpick/nitpick.ML Tue Feb 23 16:53:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 19:10:25 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, ...}) =
@@ -941,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));
@@ -954,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
@@ -971,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 Tue Feb 23 16:53:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 19:10:25 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
@@ -1173,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
@@ -1324,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 =
@@ -1342,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 =>