# HG changeset patch
# User blanchet
# Date 1281005937 -7200
# Node ID 927f919914ea34e44a270851bc71386148e71b0a
# Parent  2f531f620cb8cab47722642e262ff9652cdaccd2
make nitpick accept "==" for "nitpick_(p)simp"s

diff -r 2f531f620cb8 -r 927f919914ea doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Aug 05 12:40:12 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Thu Aug 05 12:58:57 2010 +0200
@@ -2585,7 +2585,11 @@
 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
 \textit{simps} rules. The equations must be of the form
 
-\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr].$
+\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr]$
+
+or
+
+\qquad $c~t_1~\ldots\ t_n \,\equiv\, u.$
 
 \flushitem{\textit{nitpick\_psimp}}
 
@@ -2595,7 +2599,11 @@
 corresponds to the \textit{psimps} rules. The conditional equations must be of
 the form
 
-\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$.
+\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$
+
+or
+
+\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,\equiv\, u$.
 
 \flushitem{\textit{nitpick\_choice\_spec}}
 
@@ -2633,7 +2641,7 @@
 
 or
 
-\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t)$
+\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t).$
 
 Nitpick assumes that the definition was made using a (co)inductive package
 based on the user-specified introduction rules registered in Isabelle's internal
diff -r 2f531f620cb8 -r 927f919914ea src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 12:40:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 12:58:57 2010 +0200
@@ -1727,7 +1727,7 @@
 
 (** Axiom extraction/generation **)
 
-fun equationalize t =
+fun equationalize ctxt tag t =
   let val (prems, concl) = Logic.strip_horn t in
     Logic.list_implies (prems,
         case concl of
@@ -1735,8 +1735,15 @@
           extensionalize_term concl
         | @{const Trueprop} $ t' =>
           @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
-        | _ => extensionalize_term concl)
+        | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+          extensionalize_term (Const (@{const_name "op ="}, T --> T --> bool_T)
+                               $ t1 $ t2)
+        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^
+                         quote (Syntax.string_of_term ctxt t) ^ ".");
+                raise SAME ()))
+    |> SOME
   end
+  handle SAME () => NONE
 
 fun pair_for_prop t =
   case term_under_def t of
@@ -1756,10 +1763,12 @@
 fun const_nondef_table ts =
   fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
 
-val const_simp_table =
-  def_table_for (map (equationalize o prop_of) o Nitpick_Simps.get)
-val const_psimp_table =
-  def_table_for (map (equationalize o prop_of) o Nitpick_Psimps.get)
+fun const_simp_table ctxt =
+  def_table_for (map_filter (equationalize ctxt "nitpick_simp" o prop_of)
+                 o Nitpick_Simps.get) ctxt
+fun const_psimp_table ctxt =
+  def_table_for (map_filter (equationalize ctxt "nitpick_psimp" o prop_of)
+                 o Nitpick_Psimps.get) ctxt
 
 fun const_choice_spec_table ctxt subst =
   map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)