# HG changeset patch
# User blanchet
# Date 1266948625 -3600
# Node ID f715cfde056a369a0e38074c13500a495fd60a48
# Parent  b83b9f2a4b923ae680d381e2226c782b6309b591
support local definitions in Nitpick

diff -r b83b9f2a4b92 -r f715cfde056a doc-src/Nitpick/nitpick.tex
--- 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}
diff -r b83b9f2a4b92 -r f715cfde056a src/HOL/Tools/Nitpick/nitpick.ML
--- 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;
diff -r b83b9f2a4b92 -r f715cfde056a src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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 =>