--- 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
--- 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)