# HG changeset patch
# User blanchet
# Date 1281012327 -7200
# Node ID 37a7272cb453f7ac205d7b00822803d8772c4dd9
# Parent  38339c0558697945adf4ada74e1321b4b5a36afa
handle inductive predicates correctly after change in "def" semantics

diff -r 38339c055869 -r 37a7272cb453 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 14:32:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 14:45:27 2010 +0200
@@ -197,13 +197,14 @@
   val fixpoint_kind_of_rhs : term -> fixpoint_kind
   val fixpoint_kind_of_const :
     theory -> const_table -> string * typ -> fixpoint_kind
-  val is_inductive_pred : hol_context -> styp -> bool
+  val is_real_inductive_pred : hol_context -> styp -> bool
   val is_constr_pattern_lhs : Proof.context -> term -> bool
   val is_constr_pattern_formula : Proof.context -> term -> bool
   val nondef_props_for_const :
     theory -> bool -> const_table -> styp -> term list
   val is_choice_spec_fun : hol_context -> styp -> bool
   val is_choice_spec_axiom : theory -> const_table -> term -> bool
+  val is_real_equational_fun : hol_context -> styp -> bool
   val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool
   val codatatype_bisim_axioms : hol_context -> typ -> term list
   val is_well_founded_inductive_pred : hol_context -> styp -> bool
@@ -1401,13 +1402,9 @@
                              ...} : hol_context) x =
   fixpoint_kind_of_const thy def_table x <> NoFp andalso
   not (null (def_props_for_const thy stds fast_descrs intro_table x))
-fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
-                             ...} : hol_context) x =
-  exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
-                                                     x)))
-         [!simp_table, psimp_table]
-fun is_inductive_pred hol_ctxt =
-  is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
+fun is_inductive_pred hol_ctxt (x as (s, _)) =
+  is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
+  String.isPrefix lbfp_prefix s
 
 fun lhs_of_equation t =
   case t of
@@ -1489,9 +1486,13 @@
                     exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
                 choice_spec_table
 
+fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
+                             ...} : hol_context) x =
+  exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
+                                                     x)))
+         [!simp_table, psimp_table]
 fun is_equational_fun_but_no_plain_def hol_ctxt =
-  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
-   (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
+  is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
 
 (** Constant unfolding **)
 
diff -r 38339c055869 -r 37a7272cb453 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 05 14:32:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 05 14:45:27 2010 +0200
@@ -614,7 +614,8 @@
         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js skolemizable polar t2
         | Const (x as (s, T)) =>
-          if is_inductive_pred hol_ctxt x andalso
+          if is_real_inductive_pred hol_ctxt x andalso
+             not (is_real_equational_fun hol_ctxt x) andalso
              not (is_well_founded_inductive_pred hol_ctxt x) then
             let
               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)