# HG changeset patch
# User blanchet
# Date 1258997340 -3600
# Node ID e779bea3d3375dc3a29a44160b60c32f6900c27c
# Parent  62bcf6a52493205cb0607ba9321ea9190f9c2b65
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite

diff -r 62bcf6a52493 -r e779bea3d337 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:59:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 18:29:00 2009 +0100
@@ -11,7 +11,7 @@
     the formula to falsify
   * Added support for codatatype view of datatypes
   * Fixed soundness bugs related to sets, sets of sets, (co)inductive
-    predicates, and typedefs
+    predicates, typedefs, and "finite"
   * Fixed monotonicity check
   * Fixed error when processing definitions
   * Fixed error in "star_linear_preds" optimization
diff -r 62bcf6a52493 -r e779bea3d337 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 23 17:59:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 23 18:29:00 2009 +0100
@@ -251,7 +251,7 @@
     val intro_table = inductive_intro_table ctxt def_table
     val ground_thm_table = ground_theorem_table thy
     val ersatz_table = ersatz_table thy
-    val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =
+    val (ext_ctxt as {wf_cache, ...}) =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        user_axioms = user_axioms, debug = debug, wfs = wfs,
        destroy_constrs = destroy_constrs, specialize = specialize,
@@ -296,11 +296,9 @@
             handle TYPE (_, Ts, ts) =>
                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
 
-    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
-    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
-                     def_ts
-    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
-                        nondef_ts
+    val core_u = nut_from_term ext_ctxt Eq core_t
+    val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
+    val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
     val (free_names, const_names) =
       fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
     val (sel_names, nonsel_names) =
diff -r 62bcf6a52493 -r e779bea3d337 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:59:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 18:29:00 2009 +0100
@@ -1496,14 +1496,7 @@
         let
           val (const, ts) =
             if is_built_in_const fast_descrs x then
-              if s = @{const_name finite} then
-                if is_finite_type ext_ctxt (domain_type T) then
-                  (Abs ("A", domain_type T, @{const True}), ts)
-                else case ts of
-                  [Const (@{const_name top}, _)] => (@{const False}, [])
-                | _ => (Const x, ts)
-              else
-                (Const x, ts)
+              (Const x, ts)
             else case AList.lookup (op =) case_names s of
               SOME n =>
               let
diff -r 62bcf6a52493 -r e779bea3d337 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 17:59:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 18:29:00 2009 +0100
@@ -106,7 +106,7 @@
   val name_ord : (nut * nut) -> order
   val the_name : 'a NameTable.table -> nut -> 'a
   val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
-  val nut_from_term : theory -> bool -> special_fun list -> op2 -> term -> nut
+  val nut_from_term : extended_context -> op2 -> term -> nut
   val choose_reps_for_free_vars :
     scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
   val choose_reps_for_consts :
@@ -464,8 +464,8 @@
 fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
   | factorize z = [z]
 
-(* theory -> bool -> special_fun list -> op2 -> term -> nut *)
-fun nut_from_term thy fast_descrs special_funs eq =
+(* extended_context -> op2 -> term -> nut *)
+fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
   let
     (* string list -> typ list -> term -> nut *)
     fun aux eq ss Ts t =
@@ -596,7 +596,11 @@
           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
         | (Const (@{const_name finite}, T), [t1]) =>
-          Op1 (Finite, bool_T, Any, sub t1)
+          (if is_finite_type ext_ctxt (domain_type T) then
+             Cst (True, bool_T, Any)
+           else case t1 of
+             Const (@{const_name top}, _) => Cst (False, bool_T, Any)
+           | _ => Op1 (Finite, bool_T, Any, sub t1))
         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
         | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
           Cst (Num 0, T, Any)
@@ -678,7 +682,7 @@
              | NONE => if null ts then ConstName (s, T, Any)
                        else do_apply t0 ts)
         | (Free (s, T), []) => FreeName (s, T, Any)
-        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
+        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
         | (Bound j, []) =>
           BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
         | (Abs (s, T, t1), []) =>