1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Feb 23 16:53:13 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 23 19:10:25 2010 +0100
     1.3 @@ -2743,8 +2743,6 @@
     1.4  \item[$\bullet$] Although this has never been observed, arbitrary theorem
     1.5  morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
     1.6  
     1.7 -\item[$\bullet$] Local definitions are not supported and result in an error.
     1.8 -
     1.9  %\item[$\bullet$] All constants and types whose names start with
    1.10  %\textit{Nitpick}{.} are reserved for internal use.
    1.11  \end{enum}

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 16:53:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 19:10:25 2010 +0100
     2.3 @@ -58,8 +58,8 @@
     2.4    val register_codatatype : typ -> string -> styp list -> theory -> theory
     2.5    val unregister_codatatype : typ -> theory -> theory
     2.6    val pick_nits_in_term :
     2.7 -    Proof.state -> params -> bool -> int -> int -> int -> term list -> term
     2.8 -    -> string * Proof.state
     2.9 +    Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
    2.10 +    -> term list -> term -> string * Proof.state
    2.11    val pick_nits_in_subgoal :
    2.12      Proof.state -> params -> bool -> int -> int -> string * Proof.state
    2.13  end;
    2.14 @@ -187,10 +187,10 @@
    2.15  (* (unit -> string) -> Pretty.T *)
    2.16  fun plazy f = Pretty.blk (0, pstrs (f ()))
    2.17  
    2.18 -(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term
    2.19 -   -> string * Proof.state *)
    2.20 +(* Time.time -> Proof.state -> params -> bool -> int -> int -> int
    2.21 +   -> (term * term) list -> term list -> term -> string * Proof.state *)
    2.22  fun pick_them_nits_in_term deadline state (params : params) auto i n step
    2.23 -                           orig_assm_ts orig_t =
    2.24 +                           subst orig_assm_ts orig_t =
    2.25    let
    2.26      val timer = Timer.startRealTimer ()
    2.27      val thy = Proof.theory_of state
    2.28 @@ -237,6 +237,7 @@
    2.29        if passed_deadline deadline then raise TimeLimit.TimeOut
    2.30        else raise Interrupt
    2.31  
    2.32 +    val orig_assm_ts = if assms orelse auto then orig_assm_ts else []
    2.33      val _ =
    2.34        if step = 0 then
    2.35          print_m (fn () => "Nitpicking formula...")
    2.36 @@ -249,10 +250,7 @@
    2.37                     "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
    2.38      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    2.39                  else orig_t
    2.40 -    val assms_t = if assms orelse auto then
    2.41 -                    Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
    2.42 -                  else
    2.43 -                    neg_t
    2.44 +    val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
    2.45      val (assms_t, evals) =
    2.46        assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
    2.47                         |> pairf hd tl
    2.48 @@ -265,12 +263,12 @@
    2.49  *)
    2.50      val max_bisim_depth = fold Integer.max bisim_depths ~1
    2.51      val case_names = case_const_names thy stds
    2.52 -    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
    2.53 -    val def_table = const_def_table ctxt defs
    2.54 +    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
    2.55 +    val def_table = const_def_table ctxt subst defs
    2.56      val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    2.57 -    val simp_table = Unsynchronized.ref (const_simp_table ctxt)
    2.58 -    val psimp_table = const_psimp_table ctxt
    2.59 -    val intro_table = inductive_intro_table ctxt def_table
    2.60 +    val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    2.61 +    val psimp_table = const_psimp_table ctxt subst
    2.62 +    val intro_table = inductive_intro_table ctxt subst def_table
    2.63      val ground_thm_table = ground_theorem_table thy
    2.64      val ersatz_table = ersatz_table thy
    2.65      val (hol_ctxt as {wf_cache, ...}) =
    2.66 @@ -941,10 +939,10 @@
    2.67             else
    2.68               error "Nitpick was interrupted."
    2.69  
    2.70 -(* Proof.state -> params -> bool -> int -> int -> int -> term
    2.71 -   -> string * Proof.state *)
    2.72 +(* Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
    2.73 +   -> term list -> term -> string * Proof.state *)
    2.74  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
    2.75 -                      step orig_assm_ts orig_t =
    2.76 +                      step subst orig_assm_ts orig_t =
    2.77    if getenv "KODKODI" = "" then
    2.78      (if auto then ()
    2.79       else warning (Pretty.string_of (plazy install_kodkodi_message));
    2.80 @@ -954,13 +952,27 @@
    2.81        val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    2.82        val outcome as (outcome_code, _) =
    2.83          time_limit (if debug then NONE else timeout)
    2.84 -            (pick_them_nits_in_term deadline state params auto i n step
    2.85 +            (pick_them_nits_in_term deadline state params auto i n step subst
    2.86                                      orig_assm_ts) orig_t
    2.87      in
    2.88        if expect = "" orelse outcome_code = expect then outcome
    2.89        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    2.90      end
    2.91  
    2.92 +(* string list -> term -> bool *)
    2.93 +fun is_fixed_equation fixes
    2.94 +                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
    2.95 +    member (op =) fixes s
    2.96 +  | is_fixed_equation _ _ = false
    2.97 +(* Proof.context -> term list * term -> (term * term) list * term list * term *)
    2.98 +fun extract_fixed_frees ctxt (assms, t) =
    2.99 +  let
   2.100 +    val fixes = Variable.fixes_of ctxt |> map snd
   2.101 +    val (subst, other_assms) =
   2.102 +      List.partition (is_fixed_equation fixes) assms
   2.103 +      |>> map Logic.dest_equals
   2.104 +  in (subst, other_assms, subst_atomic subst t) end
   2.105 +
   2.106  (* Proof.state -> params -> bool -> int -> int -> string * Proof.state *)
   2.107  fun pick_nits_in_subgoal state params auto i step =
   2.108    let
   2.109 @@ -971,12 +983,11 @@
   2.110        0 => (priority "No subgoal!"; ("none", state))
   2.111      | n =>
   2.112        let
   2.113 +        val (t, frees) = Logic.goal_params t i
   2.114 +        val t = subst_bounds (frees, t)
   2.115          val assms = map term_of (Assumption.all_assms_of ctxt)
   2.116 -        val (t, frees) = Logic.goal_params t i
   2.117 -      in
   2.118 -        pick_nits_in_term state params auto i n step assms
   2.119 -                          (subst_bounds (frees, t))
   2.120 -      end
   2.121 +        val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
   2.122 +      in pick_nits_in_term state params auto i n step subst assms t end
   2.123    end
   2.124  
   2.125  end;

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 16:53:13 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 19:10:25 2010 +0100
     3.3 @@ -155,7 +155,8 @@
     3.4    val is_finite_type : hol_context -> typ -> bool
     3.5    val special_bounds : term list -> (indexname * typ) list
     3.6    val is_funky_typedef : theory -> typ -> bool
     3.7 -  val all_axioms_of : theory -> term list * term list * term list
     3.8 +  val all_axioms_of :
     3.9 +    theory -> (term * term) list -> term list * term list * term list
    3.10    val arity_of_built_in_const :
    3.11      theory -> (typ option * bool) list -> bool -> styp -> int option
    3.12    val is_built_in_const :
    3.13 @@ -163,11 +164,13 @@
    3.14    val term_under_def : term -> term
    3.15    val case_const_names :
    3.16      theory -> (typ option * bool) list -> (string * int) list
    3.17 -  val const_def_table : Proof.context -> term list -> const_table
    3.18 +  val const_def_table :
    3.19 +    Proof.context -> (term * term) list -> term list -> const_table
    3.20    val const_nondef_table : term list -> const_table
    3.21 -  val const_simp_table : Proof.context -> const_table
    3.22 -  val const_psimp_table : Proof.context -> const_table
    3.23 -  val inductive_intro_table : Proof.context -> const_table -> const_table
    3.24 +  val const_simp_table : Proof.context -> (term * term) list -> const_table
    3.25 +  val const_psimp_table : Proof.context -> (term * term) list -> const_table
    3.26 +  val inductive_intro_table :
    3.27 +    Proof.context -> (term * term) list -> const_table -> const_table
    3.28    val ground_theorem_table : theory -> term list Inttab.table
    3.29    val ersatz_table : theory -> (string * string) list
    3.30    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
    3.31 @@ -1173,11 +1176,12 @@
    3.32        | do_eq _ = false
    3.33    in do_eq end
    3.34  
    3.35 -(* theory -> term list * term list * term list *)
    3.36 -fun all_axioms_of thy =
    3.37 +(* theory -> (term * term) list -> term list * term list * term list *)
    3.38 +fun all_axioms_of thy subst =
    3.39    let
    3.40      (* theory list -> term list *)
    3.41 -    val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
    3.42 +    val axioms_of_thys =
    3.43 +      maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of))
    3.44      val specs = Defs.all_specifications_of (Theory.defs_of thy)
    3.45      val def_names = specs |> maps snd |> map_filter #def
    3.46                      |> OrdList.make fast_string_ord
    3.47 @@ -1324,12 +1328,13 @@
    3.48  fun pair_for_prop t =
    3.49    case term_under_def t of
    3.50      Const (s, _) => (s, t)
    3.51 -  | Free _ => raise NOT_SUPPORTED "local definitions"
    3.52    | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
    3.53  
    3.54 -(* (Proof.context -> term list) -> Proof.context -> const_table *)
    3.55 -fun table_for get ctxt =
    3.56 -  get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
    3.57 +(* (Proof.context -> term list) -> Proof.context -> (term * term) list
    3.58 +   -> const_table *)
    3.59 +fun table_for get ctxt subst =
    3.60 +  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
    3.61 +       |> AList.group (op =) |> Symtab.make
    3.62  
    3.63  (* theory -> (typ option * bool) list -> (string * int) list *)
    3.64  fun case_const_names thy stds =
    3.65 @@ -1342,23 +1347,23 @@
    3.66                (Datatype.get_all thy) [] @
    3.67    map (apsnd length o snd) (#codatatypes (Data.get thy))
    3.68  
    3.69 -(* Proof.context -> term list -> const_table *)
    3.70 -fun const_def_table ctxt ts =
    3.71 -  table_for (map prop_of o Nitpick_Defs.get) ctxt
    3.72 +(* Proof.context -> (term * term) list -> term list -> const_table *)
    3.73 +fun const_def_table ctxt subst ts =
    3.74 +  table_for (map prop_of o Nitpick_Defs.get) ctxt subst
    3.75    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
    3.76            (map pair_for_prop ts)
    3.77  (* term list -> const_table *)
    3.78  fun const_nondef_table ts =
    3.79    fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
    3.80    |> AList.group (op =) |> Symtab.make
    3.81 -(* Proof.context -> const_table *)
    3.82 +(* Proof.context -> (term * term) list -> const_table *)
    3.83  val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
    3.84  val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
    3.85 -(* Proof.context -> const_table -> const_table *)
    3.86 -fun inductive_intro_table ctxt def_table =
    3.87 +(* Proof.context -> (term * term) list -> const_table -> const_table *)
    3.88 +fun inductive_intro_table ctxt subst def_table =
    3.89    table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
    3.90                                                    def_table o prop_of)
    3.91 -             o Nitpick_Intros.get) ctxt
    3.92 +             o Nitpick_Intros.get) ctxt subst
    3.93  (* theory -> term list Inttab.table *)
    3.94  fun ground_theorem_table thy =
    3.95    fold ((fn @{const Trueprop} $ t1 =>