remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much

--- a/src/HOL/Nitpick.thy	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Nitpick.thy	Tue Dec 07 11:56:53 2010 +0100
@@ -35,7 +35,6 @@
            and Quot :: "'a \<Rightarrow> 'b"
            and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
-datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
 datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
 datatype ('a, 'b) pair_box = PairBox 'a 'b
 
@@ -240,12 +239,11 @@
 setup {* Nitpick_Isar.setup *}
 
 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
-    FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card'
-    setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
-    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
+    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
+    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
+    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
     number_of_frac inverse_frac less_frac less_eq_frac of_frac
-hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
-    word
+hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
 hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
     refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
     fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -292,7 +292,7 @@
     val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
-         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
+         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -361,9 +361,7 @@
         SOME (SOME b) => b
       | _ => is_type_fundamentally_monotonic T orelse
              is_type_actually_monotonic T
-    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
-        is_type_kind_of_monotonic T
-      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
+    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
         is_type_kind_of_monotonic T
       | is_shallow_datatype_finitizable T =
         case triple_lookup (type_match thy) finitizes T of

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -462,9 +462,7 @@
   | unarize_type @{typ "signed_bit word"} = int_T
   | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
   | unarize_type T = T
-fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
-    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
-  | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
+fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
     unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
   | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
     Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
@@ -804,9 +802,9 @@
     end
   | _ => false
 fun is_constr_like ctxt (s, T) =
-  member (op =) [@{const_name FinFun}, @{const_name FunBox},
-                 @{const_name PairBox}, @{const_name Quot},
-                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
+  member (op =) [@{const_name FunBox}, @{const_name PairBox},
+                 @{const_name Quot}, @{const_name Zero_Rep},
+                 @{const_name Suc_Rep}] s orelse
   let
     val thy = ProofContext.theory_of ctxt
     val (x as (_, T)) = (s, unarize_unbox_etc_type T)
@@ -1095,14 +1093,13 @@
          |> Envir.eta_contract
          |> new_s <> @{type_name fun}
             ? construct_value ctxt stds
-                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
-                   else @{const_name FunBox},
+                  (@{const_name FunBox},
                    Type (@{type_name fun}, new_Ts) --> new_T)
               o single
        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
     | (Type (new_s, new_Ts as [new_T1, new_T2]),
        Type (old_s, old_Ts as [old_T1, old_T2])) =>
-      if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
+      if old_s = @{type_name fun_box} orelse
          old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
         case constr_expand hol_ctxt old_T t of
           Const (old_s, _) $ t1 =>

--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -178,9 +178,7 @@
 fun tuple_list_for_name rel_table bounds name =
   the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
 
-fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
-    unarize_unbox_etc_term t1
-  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
+fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
     unarize_unbox_etc_term t1
   | unarize_unbox_etc_term
         (Const (@{const_name PairBox},
@@ -559,9 +557,8 @@
                   if length arg_Ts = 0 then
                     []
                   else
-                    map3 (fn Ts =>
-                             term_for_rep (constr_s <> @{const_name FinFun})
-                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
+                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
+                         arg_jsss
                     |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
                     |> dest_n_tuple (length uncur_arg_Ts)
                 val t =
@@ -935,8 +932,7 @@
       Pretty.block (Pretty.breaks
           (pretty_for_type ctxt typ ::
            (case typ of
-              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
-            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
+              Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
             | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
             | _ => []) @
            [Pretty.str "=",

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -12,9 +12,6 @@
   val trace : bool Unsynchronized.ref
   val formulas_monotonic :
     hol_context -> bool -> typ -> term list * term list -> bool
-  val finitize_funs :
-    hol_context -> bool -> (typ option * bool option) list -> typ
-    -> term list * term list -> term list * term list
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -1249,110 +1246,4 @@
 
 val formulas_monotonic = is_some oooo infer "Monotonicity" false
 
-fun fin_fun_constr T1 T2 =
-  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-
-fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
-                  finitizes alpha_T tsp =
-  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
-    SOME (asgs, msp, constr_mtypes) =>
-    if forall (curry (op =) Gen o snd) asgs then
-      tsp
-    else
-      let
-        fun should_finitize T aa =
-          case triple_lookup (type_match thy) finitizes T of
-            SOME (SOME false) => false
-          | _ => resolve_annotation_atom asgs aa = A Fls
-        fun type_from_mtype T M =
-          case (M, T) of
-            (MAlpha, _) => T
-          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
-            Type (if should_finitize T aa then @{type_name fin_fun}
-                  else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
-          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
-            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
-          | (MType _, _) => T
-          | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
-                              [M], [T])
-        fun finitize_constr (x as (s, T)) =
-          (s, case AList.lookup (op =) constr_mtypes x of
-                SOME M => type_from_mtype T M
-              | NONE => T)
-        fun term_from_mterm new_Ts old_Ts m =
-          case m of
-            MRaw (t, M) =>
-            let
-              val T = fastype_of1 (old_Ts, t)
-              val T' = type_from_mtype T M
-            in
-              case t of
-                Const (x as (s, _)) =>
-                if s = @{const_name finite} then
-                  case domain_type T' of
-                    set_T' as Type (@{type_name fin_fun}, _) =>
-                    Abs (Name.uu, set_T', @{const True})
-                  | _ => Const (s, T')
-                else if s = @{const_name "=="} orelse
-                        s = @{const_name HOL.eq} then
-                  let
-                    val T =
-                      case T' of
-                        Type (_, [T1, Type (_, [T2, T3])]) =>
-                        T1 --> T2 --> T3
-                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
-                                         \term_from_mterm", [T, T'], [])
-                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
-                else if is_built_in_const thy stds x then
-                  coerce_term hol_ctxt new_Ts T' T t
-                else if is_constr ctxt stds x then
-                  Const (finitize_constr x)
-                else if is_sel s then
-                  let
-                    val n = sel_no_from_name s
-                    val x' =
-                      x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
-                        |> finitize_constr
-                    val x'' =
-                      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
-                                                             x' n
-                  in Const x'' end
-                else
-                  Const (s, T')
-              | Free (s, T) => Free (s, type_from_mtype T M)
-              | Bound _ => t
-              | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
-                                  [m])
-            end
-          | MApp (m1, m2) =>
-            let
-              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
-              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
-              val (t1', T2') =
-                case T1 of
-                  Type (s, [T11, T12]) =>
-                  (if s = @{type_name fin_fun} then
-                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
-                                           0 (T11 --> T12)
-                   else
-                     t1, T11)
-                | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
-                                   [T1], [])
-            in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
-          | MAbs (s, old_T, M, aa, m') =>
-            let
-              val new_T = type_from_mtype old_T M
-              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
-              val T' = fastype_of1 (new_T :: new_Ts, t')
-            in
-              Abs (s, new_T, t')
-              |> should_finitize (new_T --> T') aa
-                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
-            end
-      in
-        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
-        pairself (map (term_from_mterm [] [])) msp
-      end
-  | NONE => tsp
-
 end;

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -9,8 +9,7 @@
 sig
   type hol_context = Nitpick_HOL.hol_context
   val preprocess_formulas :
-    hol_context -> (typ option * bool option) list
-    -> (typ option * bool option) list -> term list -> term
+    hol_context -> term list -> term
     -> term list * term list * bool * bool * bool
 end;
 
@@ -1245,32 +1244,13 @@
              | _ => t
   in aux "" [] [] end
 
-(** Inference of finite functions **)
-
-fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
-                               (nondef_ts, def_ts) =
-  if forall (curry (op =) (SOME false) o snd) finitizes then
-    (nondef_ts, def_ts)
-  else
-    let
-      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
-               |> filter_out (fn Type (@{type_name fun_box}, _) => true
-                               | @{typ signed_bit} => true
-                               | @{typ unsigned_bit} => true
-                               | T => is_small_finite_type hol_ctxt T orelse
-                                      triple_lookup (type_match thy) monos T
-                                      = SOME (SOME false))
-    in
-      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
-    end
-
 (** Preprocessor entry point **)
 
 val max_skolem_depth = 3
 
 fun preprocess_formulas
         (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
-                      ...}) finitizes monos assm_ts neg_t =
+                      ...}) assm_ts neg_t =
   let
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
       neg_t |> unfold_defs_in_term hol_ctxt
@@ -1307,9 +1287,6 @@
       #> Term.map_abs_vars shortest_name
     val nondef_ts = map (do_rest false) nondef_ts
     val def_ts = map (do_rest true) def_ts
-    val (nondef_ts, def_ts) =
-      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
-                                 (nondef_ts, def_ts)
   in
     (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
   end

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:53 2010 +0100
@@ -112,8 +112,6 @@
 
 fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
-  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
-    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
   | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
     forall (is_complete_type dtypes facto) Ts
   | is_complete_type dtypes facto T =
@@ -122,8 +120,6 @@
     handle Option.Option => true
 and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
-  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
-    is_concrete_type dtypes facto T2
   | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
     forall (is_concrete_type dtypes facto) Ts
   | is_concrete_type dtypes facto T =