# HG changeset patch
# User blanchet
# Date 1267199386 -3600
# Node ID 45a4e19d3ebde35eae0e1d25929db2cccf08ad87
# Parent  29f81babefd74b4aa5d8919702b5ad1b1788deef
more work on the new monotonicity stuff in Nitpick

diff -r 29f81babefd7 -r 45a4e19d3ebd doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Feb 25 16:33:39 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 26 16:49:46 2010 +0100
@@ -2743,8 +2743,8 @@
 \item[$\bullet$] Although this has never been observed, arbitrary theorem
 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
 
-%\item[$\bullet$] All constants and types whose names start with
-%\textit{Nitpick}{.} are reserved for internal use.
+\item[$\bullet$] All constants, types, free variables, and schematic variables
+whose names start with \textit{Nitpick}{.} are reserved for internal use.
 \end{enum}
 
 \let\em=\sl
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
@@ -1000,7 +1000,7 @@
 oops
 
 lemma "(Q\<Colon>nat set) (Eps Q)"
-nitpick [expect = none]
+nitpick [expect = none] (* unfortunate *)
 oops
 
 lemma "\<not> Q (Eps Q)"
@@ -1053,11 +1053,11 @@
 
 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
 nitpick [expect = none]
-oops
+sorry
 
 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
 nitpick [expect = none]
-oops
+sorry
 
 subsection {* Destructors and Recursors *}
 
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
@@ -69,7 +69,7 @@
 oops
 
 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [card = 1\<midarrow>9, expect = none]
 sorry
 
 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
@@ -30,7 +30,7 @@
    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} [] []
+fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
 fun is_const t =
   let val T = fastype_of t in
     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
@@ -46,26 +46,26 @@
 ML {* const @{term "(A::'a set) = A"} *}
 ML {* const @{term "(A::'a set set) = A"} *}
 ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
-ML {* const @{term "{{a}} = C"} *}
+ML {* const @{term "{{a::'a}} = C"} *}
 ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
-ML {* const @{term "A \<union> B"} *}
+ML {* const @{term "A \<union> (B::'a set)"} *}
 ML {* const @{term "P (a::'a)"} *}
 ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
 ML {* const @{term "\<forall>A::'a set. A a"} *}
 ML {* const @{term "\<forall>A::'a set. P A"} *}
 ML {* const @{term "P \<or> Q"} *}
-ML {* const @{term "A \<union> B = C"} *}
+ML {* const @{term "A \<union> B = (C::'a set)"} *}
 ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
-ML {* const @{term "let A = C in A \<union> B"} *}
+ML {* const @{term "let A = (C::'a set) in A \<union> B"} *}
 ML {* const @{term "THE x::'b. P x"} *}
-ML {* const @{term "{}::'a set"} *}
+ML {* const @{term "(\<lambda>x::'a. False)"} *}
 ML {* const @{term "(\<lambda>x::'a. True)"} *}
-ML {* const @{term "Let a A"} *}
+ML {* const @{term "Let (a::'a) A"} *}
 ML {* const @{term "A (a::'a)"} *}
-ML {* const @{term "insert a A = B"} *}
+ML {* const @{term "insert (a::'a) A = B"} *}
 ML {* const @{term "- (A::'a set)"} *}
-ML {* const @{term "finite A"} *}
-ML {* const @{term "\<not> finite A"} *}
+ML {* const @{term "finite (A::'a set)"} *}
+ML {* const @{term "\<not> finite (A::'a set)"} *}
 ML {* const @{term "finite (A::'a set set)"} *}
 ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
 ML {* const @{term "A < (B::'a set)"} *}
@@ -74,27 +74,25 @@
 ML {* const @{term "[a::'a set]"} *}
 ML {* const @{term "[A \<union> (B::'a set)]"} *}
 ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
-ML {* const @{term "\<forall>P. P a"} *}
 
-ML {* nonconst @{term "{%x. True}"} *}
-ML {* nonconst @{term "{(%x. x = a)} = C"} *}
+ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *}
 ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
 ML {* nonconst @{term "\<forall>a::'a. P a"} *}
 ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
-ML {* nonconst @{term "THE x. P x"} *}
-ML {* nonconst @{term "SOME x. P x"} *}
+ML {* nonconst @{term "THE x::'a. P x"} *}
+ML {* nonconst @{term "SOME x::'a. P x"} *}
 
 ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
 ML {* mono @{prop "P (a::'a)"} *}
-ML {* mono @{prop "{a} = {b}"} *}
+ML {* mono @{prop "{a} = {b::'a}"} *}
 ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
 ML {* mono @{prop "\<forall>F::'a set set. P"} *}
 ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
 ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
-ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
+ML {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *}
 
-ML {* nonmono @{prop "\<forall>x. P x"} *}
+ML {* nonmono @{prop "\<forall>x::'a. P x"} *}
+ML {* nonmono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *}
 ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
-ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
 
 end
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
@@ -64,7 +64,7 @@
 oops
 
 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [expect = none]
+nitpick [fast_descrs (* ### FIXME *), expect = none]
 sorry
 
 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Fri Feb 26 16:49:46 2010 +0100
@@ -4,7 +4,9 @@
   * Added "std" option and implemented support for nonstandard models
   * Added support for quotient types
   * Added support for local definitions
-  * Optimized "Multiset.multiset"
+  * Disabled "fast_descrs" option by default
+  * Optimized "Multiset.multiset" and "FinFun.finfun"
+  * Improved efficiency of "destroy_constrs" optimization
   * Improved precision of infinite datatypes whose constructors don't appear
     in the formula to falsify based on a monotonicity analysis
   * Fixed soundness bugs related to "destroy_constrs" optimization and record
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 26 16:49:46 2010 +0100
@@ -131,9 +131,7 @@
   nonsel_names: nut list,
   rel_table: nut NameTable.table,
   unsound: bool,
-  scope: scope,
-  core: KK.formula,
-  defs: KK.formula list}
+  scope: scope}
 
 type rich_problem = KK.problem * problem_extension
 
@@ -195,7 +193,8 @@
     val timer = Timer.startRealTimer ()
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-(* FIXME: reintroduce code before new release
+(* FIXME: reintroduce code before new release:
+
     val nitpick_thy = ThyInfo.get_theory "Nitpick"
     val _ = Theory.subthy (nitpick_thy, thy) orelse
             error "You must import the theory \"Nitpick\" to use Nitpick"
@@ -289,8 +288,8 @@
     val frees = Term.add_frees assms_t []
     val _ = null (Term.add_tvars assms_t []) orelse
             raise NOT_SUPPORTED "schematic type variables"
-    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
-         core_t, binarize) = preprocess_term hol_ctxt assms_t
+    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
+         binarize) = preprocess_term hol_ctxt assms_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -307,28 +306,25 @@
                    \unroll it.")))
     val _ = if verbose then List.app print_wf (!wf_cache) else ()
     val _ =
-      pprint_d (fn () =>
-          Pretty.chunks
-              (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
-               pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
-               pretties_for_formulas ctxt "Relevant nondefinitional axiom"
-                                     nondef_ts))
-    val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
+      pprint_d (fn () => Pretty.chunks
+          (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
+           pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
+           pretties_for_formulas ctxt "Relevant nondefinitional axiom"
+                                 (tl nondef_ts)))
+    val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
             handle TYPE (_, Ts, ts) =>
                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
 
-    val core_u = nut_from_term hol_ctxt Eq core_t
+    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
     val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
-    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
     val (free_names, const_names) =
-      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
+      fold add_free_and_const_names (nondef_us @ def_us) ([], [])
     val (sel_names, nonsel_names) =
       List.partition (is_sel o nickname_of) const_names
     val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
     val standard = forall snd stds
 (*
-    val _ = List.app (priority o string_for_nut ctxt)
-                     (core_u :: def_us @ nondef_us)
+    val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
 *)
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
@@ -349,7 +345,7 @@
        (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
       is_number_type thy T orelse is_bit_type T
     fun is_type_actually_monotonic T =
-      formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
+      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     fun is_type_monotonic T =
       unique_scope orelse
       case triple_lookup (type_match thy) monos T of
@@ -362,14 +358,14 @@
     fun is_datatype_deep T =
       not standard orelse T = nat_T orelse is_word_type T orelse
       exists (curry (op =) T o domain_type o type_of) sel_names
-    val all_Ts = ground_types_in_terms hol_ctxt binarize
-                                       (core_t :: def_ts @ nondef_ts)
+    val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
                  |> sort TermOrd.typ_ord
     val _ = if verbose andalso binary_ints = SOME true andalso
                exists (member (op =) [nat_T, int_T]) all_Ts then
               print_v (K "The option \"binary_ints\" will be ignored because \
                          \of the presence of rationals, reals, \"Suc\", \
-                         \\"gcd\", or \"lcm\" in the problem.")
+                         \\"gcd\", or \"lcm\" in the problem or because of the \
+                         \\"non_std\" option.")
             else
               ()
     val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
@@ -480,7 +476,6 @@
                          (univ_card nat_card int_card main_j0 [] KK.True)
         val _ = check_arity min_univ_card min_highest_arity
 
-        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
         val def_us = map (choose_reps_in_nut scope unsound rep_table true)
                          def_us
         val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
@@ -488,7 +483,7 @@
 (*
         val _ = List.app (priority o string_for_nut ctxt)
                          (free_names @ sel_names @ nonsel_names @
-                          core_u :: def_us @ nondef_us)
+                          nondef_us @ def_us)
 *)
         val (free_rels, pool, rel_table) =
           rename_free_vars free_names initial_pool NameTable.empty
@@ -496,13 +491,11 @@
           rename_free_vars sel_names pool rel_table
         val (other_rels, pool, rel_table) =
           rename_free_vars nonsel_names pool rel_table
-        val core_u = rename_vars_in_nut pool rel_table core_u
+        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
         val def_us = map (rename_vars_in_nut pool rel_table) def_us
-        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
-        val core_f = kodkod_formula_from_nut ofs kk core_u
+        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
-        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
-        val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
+        val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       PrintMode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
@@ -550,8 +543,7 @@
                expr_assigns = [], formula = formula},
               {free_names = free_names, sel_names = sel_names,
                nonsel_names = nonsel_names, rel_table = rel_table,
-               unsound = unsound, scope = scope, core = core_f,
-               defs = nondef_fs @ def_fs @ declarative_axioms})
+               unsound = unsound, scope = scope})
       end
       handle TOO_LARGE (loc, msg) =>
              if loc = "Nitpick_Kodkod.check_arity" andalso
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 16:49:46 2010 +0100
@@ -154,6 +154,7 @@
     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   val is_finite_type : hol_context -> typ -> bool
   val special_bounds : term list -> (indexname * typ) list
+  val abs_var : indexname * typ -> term -> term
   val is_funky_typedef : theory -> typ -> bool
   val all_axioms_of :
     theory -> (term * term) list -> term list * term list * term list
@@ -631,8 +632,13 @@
        in
          case t_opt of
            SOME (Const (@{const_name top}, _)) => true
+           (* "Multiset.multiset" *)
          | SOME (Const (@{const_name Collect}, _)
                  $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
+           (* "FinFun.finfun" *)
+         | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
+                     Const (@{const_name Ex}, _) $ Abs (_, _,
+                         Const (@{const_name finite}, _) $ _))) => true
          | _ => false
        end
      | NONE => false)
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 26 16:49:46 2010 +0100
@@ -444,7 +444,7 @@
   single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
    -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
-fun tripl_rel_rel_let kk f r1 r2 r3 =
+fun triple_rel_rel_let kk f r1 r2 r3 =
   double_rel_rel_let kk
       (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
 
@@ -1615,7 +1615,7 @@
         kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
       | Op3 (If, _, R, u1, u2, u3) =>
         if is_opt_rep (rep_of u1) then
-          tripl_rel_rel_let kk
+          triple_rel_rel_let kk
               (fn r1 => fn r2 => fn r3 =>
                   let val empty_r = empty_rel_for_rep R in
                     fold1 kk_union
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Feb 26 16:49:46 2010 +0100
@@ -10,7 +10,7 @@
   type hol_context = Nitpick_HOL.hol_context
 
   val formulas_monotonic :
-    hol_context -> bool -> typ -> term list * term list * term -> bool
+    hol_context -> bool -> typ -> term list * term list -> bool
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -34,7 +34,7 @@
   MRec of string * typ list
 
 datatype mterm =
-  MAtom of term * mtyp |
+  MRaw of term * mtyp |
   MAbs of string * typ * mtyp * sign_atom * mterm |
   MApp of mterm * mterm
 
@@ -76,7 +76,7 @@
 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
 
 val bool_M = MType (@{type_name bool}, [])
-val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", [])
+val dummy_M = MType (nitpick_prefix ^ "dummy", [])
 
 (* mtyp -> bool *)
 fun is_MRec (MRec _) = true
@@ -102,16 +102,19 @@
         val need_parens = (prec < outer_prec)
       in
         (if need_parens then "(" else "") ^
-        (case M of
-           MAlpha => "\<alpha>"
-         | MFun (M1, a, M2) =>
-           aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
-           string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
-         | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
-         | MType (s, []) =>
-           if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
-         | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
-         | MRec (s, _) => "[" ^ s ^ "]") ^
+        (if M = dummy_M then
+           "_"
+         else case M of
+             MAlpha => "\<alpha>"
+           | MFun (M1, a, M2) =>
+             aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
+             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
+           | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
+           | MType (s, []) =>
+             if s = @{type_name prop} orelse s = @{type_name bool} then "o"
+             else s
+           | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
+           | MRec (s, _) => "[" ^ s ^ "]") ^
         (if need_parens then ")" else "")
       end
   in aux 0 end
@@ -122,7 +125,7 @@
   | flatten_mtype M = [M]
 
 (* mterm -> bool *)
-fun precedence_of_mterm (MAtom _) = no_prec
+fun precedence_of_mterm (MRaw _) = no_prec
   | precedence_of_mterm (MAbs _) = 1
   | precedence_of_mterm (MApp _) = 2
 
@@ -139,7 +142,7 @@
       in
         (if need_parens then "(" else "") ^
         (case m of
-           MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
+           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
          | MAbs (s, _, M, a, m) =>
            "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
            string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
@@ -149,7 +152,7 @@
   in aux 0 end
 
 (* mterm -> mtyp *)
-fun mtype_of_mterm (MAtom (_, M)) = M
+fun mtype_of_mterm (MRaw (_, M)) = M
   | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
   | mtype_of_mterm (MApp (m1, _)) =
     case mtype_of_mterm m1 of
@@ -545,19 +548,28 @@
 fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
   | solve max_var (CSet (lits, comps, sexps)) =
     let
+      (* (int -> bool option) -> literal list option *)
+      fun do_assigns assigns =
+        SOME (literals_from_assignments max_var assigns lits
+              |> tap print_solution)
       val _ = print_problem lits comps sexps
       val prop = PropLogic.all (map prop_for_literal lits @
                                 map prop_for_comp comps @
                                 map prop_for_sign_expr sexps)
-      (* use the first ML solver (to avoid startup overhead) *)
-      val solvers = !SatSolver.solvers
-                    |> filter (member (op =) ["dptsat", "dpll"] o fst)
+      val default_val = bool_from_sign Minus
     in
-      case snd (hd solvers) prop of
-        SatSolver.SATISFIABLE assigns =>
-        SOME (literals_from_assignments max_var assigns lits
-              |> tap print_solution)
-      | _ => NONE
+      if PropLogic.eval (K default_val) prop then
+        do_assigns (K (SOME default_val))
+      else
+        let
+          (* use the first ML solver (to avoid startup overhead) *)
+          val solvers = !SatSolver.solvers
+                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
+        in
+          case snd (hd solvers) prop of
+            SatSolver.SATISFIABLE assigns => do_assigns assigns
+          | _ => NONE
+        end
     end
 
 type mtype_schema = mtyp * constraint_set
@@ -580,7 +592,7 @@
   handle List.Empty => initial_gamma
 
 (* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
+fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
                                          def_table, ...},
                              alpha_T, max_fresh, ...}) =
   let
@@ -595,7 +607,7 @@
     fun do_all T (gamma, cset) =
       let
         val abs_M = mtype_for (domain_type (domain_type T))
-        val body_M = mtype_for (range_type T)
+        val body_M = mtype_for (body_type T)
       in
         (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
          (gamma, cset |> add_mtype_is_right_total abs_M))
@@ -641,9 +653,9 @@
         pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
     (* mtyp * accumulator *)
-    val mtype_unsolvable = (irrelevant_M, unsolvable_accum)
+    val mtype_unsolvable = (dummy_M, unsolvable_accum)
     (* term -> mterm * accumulator *)
-    fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum)
+    fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
     (* term -> string -> typ -> term -> term -> term -> accumulator
        -> mterm * accumulator *)
     fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
@@ -657,10 +669,11 @@
         val bound_M = mtype_of_mterm bound_m
         val (M1, a, M2) = dest_MFun bound_M
       in
-        (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)),
+        (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
                MAbs (abs_s, abs_T, M1, a,
-                     MApp (MApp (MAtom (connective_t, irrelevant_M),
-                                 MApp (bound_m, MAtom (Bound 0, M1))),
+                     MApp (MApp (MRaw (connective_t,
+                                       mtype_for (fastype_of connective_t)),
+                                 MApp (bound_m, MRaw (Bound 0, M1))),
                            body_m))), accum)
       end
     (* term -> accumulator -> mterm * accumulator *)
@@ -678,10 +691,14 @@
               | @{const_name "=="} => do_equals T accum
               | @{const_name All} => do_all T accum
               | @{const_name Ex} =>
-                do_term (@{const Not}
-                         $ (HOLogic.eq_const (domain_type T)
-                            $ Abs (Name.uu, T, @{const False}))) accum
-                |>> mtype_of_mterm
+                let val set_T = domain_type T in
+                  do_term (Abs (Name.uu, set_T,
+                                @{const Not} $ (HOLogic.mk_eq
+                                    (Abs (Name.uu, domain_type set_T,
+                                          @{const False}),
+                                     Bound 0)))) accum
+                  |>> mtype_of_mterm
+                end
               | @{const_name "op ="} => do_equals T accum
               | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
               | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
@@ -719,9 +736,12 @@
               | @{const_name rtrancl} =>
                 (print_g "*** rtrancl"; mtype_unsolvable)
               | @{const_name finite} =>
-                let val M1 = mtype_for (domain_type (domain_type T)) in
-                  (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
-                end
+                if is_finite_type hol_ctxt T then
+                  let val M1 = mtype_for (domain_type (domain_type T)) in
+                    (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
+                  end
+                else
+                  (print_g "*** finite"; mtype_unsolvable)
               | @{const_name rel_comp} =>
                 let
                   val x = Unsynchronized.inc max_fresh
@@ -807,7 +827,7 @@
                   let val M = mtype_for T in
                     (M, ({bounds = bounds, frees = frees,
                           consts = (x, M) :: consts}, cset))
-                  end) |>> curry MAtom t
+                  end) |>> curry MRaw t
          | Free (x as (_, T)) =>
            (case AList.lookup (op =) frees x of
               SOME M => (M, accum)
@@ -815,12 +835,12 @@
               let val M = mtype_for T in
                 (M, ({bounds = bounds, frees = (x, M) :: frees,
                       consts = consts}, cset))
-              end) |>> curry MAtom t
+              end) |>> curry MRaw t
          | Var _ => (print_g "*** Var"; mterm_unsolvable t)
-         | Bound j => (MAtom (t, nth bounds j), accum)
+         | Bound j => (MRaw (t, nth bounds j), accum)
          | Abs (s, T, t' as @{const False}) =>
            let val (M1, a, M2) = mfun_for T bool_T in
-             (MAbs (s, T, M1, a, MAtom (t', M2)), accum)
+             (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
            end
          | Abs (s, T, t') =>
            ((case t' of
@@ -850,88 +870,109 @@
            in
              case accum of
                (_, UnsolvableCSet) => mterm_unsolvable t
-             | _ => (MApp (m1, m2), accum)
+             | _ =>
+               let
+                 val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
+                 val M2 = mtype_of_mterm m2
+               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
            end)
         |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
                                       string_for_mterm ctxt m))
   in do_term end
 
-(* mdata -> sign -> term -> accumulator -> accumulator *)
+(* mdata -> styp -> term -> term -> mterm * accumulator *)
+fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
+  let
+    val (m1, accum) = consider_term mdata t1 accum
+    val (m2, accum) = consider_term mdata t2 accum
+    val M1 = mtype_of_mterm m1
+    val M2 = mtype_of_mterm m2
+    val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+  in
+    (MApp (MApp (MRaw (Const x,
+         MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
+     accum ||> add_mtypes_equal M1 M2)
+  end
+
+(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
 fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
   let
     (* typ -> mtyp *)
     val mtype_for = fresh_mtype_for_type mdata
-    (* term -> accumulator -> mtyp * accumulator *)
-    val do_term = apfst mtype_of_mterm oo consider_term mdata
-    (* sign -> term -> accumulator -> accumulator *)
-    fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
-      | do_formula sn t (accum as (gamma, cset)) =
+    (* term -> accumulator -> mterm * accumulator *)
+    val do_term = consider_term mdata
+    (* sign -> term -> accumulator -> mterm * accumulator *)
+    fun do_formula _ t (_, UnsolvableCSet) =
+        (MRaw (t, dummy_M), unsolvable_accum)
+      | do_formula sn t accum =
         let
-          (* term -> accumulator -> accumulator *)
-          val do_co_formula = do_formula sn
-          val do_contra_formula = do_formula (negate sn)
-          (* string -> typ -> term -> accumulator *)
-          fun do_quantifier quant_s abs_T body_t =
+          (* styp -> string -> typ -> term -> mterm * accumulator *)
+          fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
             let
               val abs_M = mtype_for abs_T
               val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
-              val cset = cset |> side_cond ? add_mtype_is_right_total abs_M
+              val (body_m, accum) =
+                accum ||> side_cond ? add_mtype_is_right_total abs_M
+                      |>> push_bound abs_M |> do_formula sn body_t
+              val body_M = mtype_of_mterm body_m
             in
-              (gamma |> push_bound abs_M, cset)
-              |> do_co_formula body_t |>> pop_bound
+              (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
+                     MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+               accum |>> pop_bound)
             end
-          (* typ -> term -> accumulator *)
-          fun do_bounded_quantifier abs_T body_t =
-            accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t
-                  |>> pop_bound
-          (* term -> term -> accumulator *)
-          fun do_equals t1 t2 =
+          (* styp -> term -> term -> mterm * accumulator *)
+          fun do_equals x t1 t2 =
             case sn of
-              Plus => do_term t accum |> snd
-            | Minus => let
-                         val (M1, accum) = do_term t1 accum
-                         val (M2, accum) = do_term t2 accum
-                       in accum ||> add_mtypes_equal M1 M2 end
+              Plus => do_term t accum
+            | Minus => consider_general_equals mdata x t1 t2 accum
         in
           case t of
-            Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
-            do_quantifier s0 T1 t1
-          | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
-          | @{const "==>"} $ t1 $ t2 =>
-            accum |> do_contra_formula t1 |> do_co_formula t2
-          | @{const Trueprop} $ t1 => do_co_formula t1 accum
-          | @{const Not} $ t1 => do_contra_formula t1 accum
-          | Const (@{const_name All}, _)
-            $ Abs (_, T1, t1 as @{const "op -->"} $ (_ $ Bound 0) $ _) =>
-            do_bounded_quantifier T1 t1
-          | Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>
-            do_quantifier s0 T1 t1
-          | Const (@{const_name Ex}, _)
-            $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
-            do_bounded_quantifier T1 t1
-          | Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
+            Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+            do_quantifier x s1 T1 t1
+          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+          | @{const Trueprop} $ t1 =>
+            let val (m1, accum) = do_formula sn t1 accum in
+              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+                     m1), accum)
+            end
+          | @{const Not} $ t1 =>
+            let val (m1, accum) = do_formula (negate sn) t1 accum in
+              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
+               accum)
+            end
+          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+            do_quantifier x s1 T1 t1
+          | Const (x0 as (s0 as @{const_name Ex}, T0))
+            $ (t1 as Abs (s1, T1, t1')) =>
             (case sn of
-               Plus => do_quantifier s0 T1 t1'
+               Plus => do_quantifier x0 s1 T1 t1'
              | Minus =>
+               (* ### do elsewhere *)
                do_term (@{const Not}
                         $ (HOLogic.eq_const (domain_type T0) $ t1
-                           $ Abs (Name.uu, T1, @{const False}))) accum |> snd)
-          | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
-          | @{const "op &"} $ t1 $ t2 =>
-            accum |> do_co_formula t1 |> do_co_formula t2
-          | @{const "op |"} $ t1 $ t2 =>
-            accum |> do_co_formula t1 |> do_co_formula t2
-          | @{const "op -->"} $ t1 $ t2 =>
-            accum |> do_contra_formula t1 |> do_co_formula t2
-          | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
-            accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
-          | Const (@{const_name Let}, _) $ t1 $ t2 =>
-            do_co_formula (betapply (t2, t1)) accum
-          | _ => do_term t accum |> snd
+                           $ Abs (Name.uu, T1, @{const False}))) accum)
+          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+            do_equals x t1 t2
+          | (t0 as Const (s0, _)) $ t1 $ t2 =>
+            if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+               s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
+              let
+                val impl = (s0 = @{const_name "==>"} orelse
+                           s0 = @{const_name "op -->"})
+                val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
+                val (m2, accum) = do_formula sn t2 accum
+              in
+                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
+                 accum)
+              end 
+            else
+              do_term t accum
+          | _ => do_term t accum
         end
-        |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
-                                 Syntax.string_of_term ctxt t ^
-                                 " : o\<^sup>" ^ string_for_sign sn))
+        |> tap (fn (m, _) =>
+                   print_g ("\<Gamma> \<turnstile> " ^
+                            string_for_mterm ctxt m ^ " : o\<^sup>" ^
+                            string_for_sign sn))
   in do_formula end
 
 (* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -947,46 +988,69 @@
   |> (forall (member (op =) harmless_consts o original_name o fst)
       orf exists (member (op =) bounteous_consts o fst))
 
-(* mdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t =
-  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t
+(* mdata -> term -> accumulator -> mterm * accumulator *)
+fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
+  if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
+  else consider_general_formula mdata Plus t
 
-(* mdata -> term -> accumulator -> accumulator *)
+(* mdata -> term -> accumulator -> mterm * accumulator *)
 fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
   if not (is_constr_pattern_formula thy t) then
-    consider_nondefinitional_axiom mdata Plus t
+    consider_nondefinitional_axiom mdata t
   else if is_harmless_axiom hol_ctxt t then
-    I
+    pair (MRaw (t, dummy_M))
   else
     let
-      (* term -> accumulator -> mtyp * accumulator *)
-      val do_term = apfst mtype_of_mterm oo consider_term mdata
-      (* typ -> term -> accumulator -> accumulator *)
-      fun do_all abs_T body_t accum =
-        let val abs_M = fresh_mtype_for_type mdata abs_T in
-          accum |>> push_bound abs_M |> do_formula body_t |>> pop_bound
+      (* typ -> mtyp *)
+      val mtype_for = fresh_mtype_for_type mdata
+      (* term -> accumulator -> mterm * accumulator *)
+      val do_term = consider_term mdata
+      (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
+      fun do_all quant_t abs_s abs_T body_t accum =
+        let
+          val abs_M = mtype_for abs_T
+          val (body_m, accum) =
+            accum |>> push_bound abs_M |> do_formula body_t
+          val body_M = mtype_of_mterm body_m
+        in
+          (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
+                 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+           accum |>> pop_bound)
         end
-      (* term -> term -> accumulator -> accumulator *)
-      and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
-      and do_equals t1 t2 accum =
+      (* term -> term -> term -> accumulator -> mterm * accumulator *)
+      and do_conjunction t0 t1 t2 accum =
         let
-          val (M1, accum) = do_term t1 accum
-          val (M2, accum) = do_term t2 accum
-        in accum ||> add_mtypes_equal M1 M2 end
+          val (m1, accum) = do_formula t1 accum
+          val (m2, accum) = do_formula t2 accum
+        in
+          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+        end
+      and do_implies t0 t1 t2 accum =
+        let
+          val (m1, accum) = do_term t1 accum
+          val (m2, accum) = do_formula t2 accum
+        in
+          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+        end
       (* term -> accumulator -> accumulator *)
-      and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
+      and do_formula t (_, UnsolvableCSet) =
+          (MRaw (t, dummy_M), unsolvable_accum)
         | do_formula t accum =
           case t of
-            Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+            (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+            do_all t0 s1 T1 t1 accum
           | @{const Trueprop} $ t1 => do_formula t1 accum
-          | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum
-          | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
-          | @{const Pure.conjunction} $ t1 $ t2 =>
-            accum |> do_formula t1 |> do_formula t2
-          | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
-          | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
-          | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
-          | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
+          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
+            consider_general_equals mdata x t1 t2 accum
+          | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+          | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
+            do_conjunction t0 t1 t2 accum
+          | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
+            do_all t0 s0 T1 t1 accum
+          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+            consider_general_equals mdata x t1 t2 accum
+          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                              \do_formula", [t])
     in do_formula t end
@@ -1002,20 +1066,27 @@
   map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   |> cat_lines |> print_g
 
-(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
+(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
+fun gather f t (ms, accum) =
+  let val (m, accum) = f t accum in (m :: ms, accum) end
+
+(* hol_context -> bool -> typ -> term list * term list -> bool *)
 fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
-                       (def_ts, nondef_ts, core_t) =
+                       (nondef_ts, def_ts) =
   let
     val _ = print_g ("****** Monotonicity analysis: " ^
                      string_for_mtype MAlpha ^ " is " ^
                      Syntax.string_of_typ ctxt alpha_T)
     val mdata as {max_fresh, constr_cache, ...} =
       initial_mdata hol_ctxt binarize alpha_T
-    val (gamma as {frees, consts, ...}, cset) =
-      (initial_gamma, slack)
-      |> fold (consider_definitional_axiom mdata) def_ts
-      |> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts
-      |> consider_general_formula mdata Plus core_t
+
+    val accum = (initial_gamma, slack)
+    val (nondef_ms, accum) =
+      ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
+                  |> fold (gather (consider_nondefinitional_axiom mdata))
+                          (tl nondef_ts)
+    val (def_ms, (gamma, cset)) =
+      ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
   in
     case solve (!max_fresh) cset of
       SOME lits => (print_mtype_context ctxt lits gamma; true)
diff -r 29f81babefd7 -r 45a4e19d3ebd src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Feb 26 16:49:46 2010 +0100
@@ -9,8 +9,7 @@
 sig
   type hol_context = Nitpick_HOL.hol_context
   val preprocess_term :
-    hol_context -> term
-    -> ((term list * term list) * (bool * bool)) * term * bool
+    hol_context -> term -> term list * term list * bool * bool * bool
 end
 
 structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -473,6 +472,19 @@
           (list_comb (t, args), seen)
   in aux [] 0 t [] [] |> fst end
 
+val let_var_prefix = nitpick_prefix ^ "l"
+val let_inline_threshold = 32
+
+(* int -> typ -> term -> (term -> term) -> term *)
+fun hol_let n abs_T body_T f t =
+  if n * size_of_term t <= let_inline_threshold then
+    f t
+  else
+    let val z = ((let_var_prefix, 0), abs_T) in
+      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
+      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
+    end
+
 (* hol_context -> bool -> term -> term *)
 fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
   let
@@ -507,14 +519,19 @@
           if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
           else raise SAME ()
         | (Const (x as (s, T)), args) =>
-          let val arg_Ts = binder_types T in
-            if length arg_Ts = length args andalso
-               (is_constr thy stds x orelse s = @{const_name Pair}) andalso
+          let
+            val (arg_Ts, dataT) = strip_type T
+            val n = length arg_Ts
+          in
+            if length args = n andalso
+               (is_constr thy stds x orelse s = @{const_name Pair} orelse
+                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
-              discriminate_value hol_ctxt x t1 ::
-              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
-              |> foldr1 s_conj
+                hol_let (n + 1) dataT bool_T
+                    (fn t1 => discriminate_value hol_ctxt x t1 ::
+                              map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
+                              |> foldr1 s_conj) t1
             else
               raise SAME ()
           end
@@ -1019,7 +1036,7 @@
 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
 val axioms_max_depth = 255
 
-(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+(* hol_context -> term -> term list * term list * bool * bool *)
 fun axioms_for_term
         (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
                       fast_descrs, evals, def_table, nondef_table, user_nondefs,
@@ -1169,10 +1186,9 @@
                      |> user_axioms = SOME true
                         ? fold (add_nondef_axiom 1) mono_user_nondefs
     val defs = defs @ special_congruence_axioms hol_ctxt xs
-  in
-    ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
-                       null poly_user_nondefs))
-  end
+    val got_all_mono_user_axioms =
+      (user_axioms = SOME true orelse null mono_user_nondefs)
+  in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
 
 (** Simplification of constructor/selector terms **)
 
@@ -1274,7 +1290,7 @@
 
 (* Maximum number of quantifiers in a cluster for which the exponential
    algorithm is used. Larger clusters use a heuristic inspired by Claessen &
-   Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+   Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
    paper). *)
 val quantifier_cluster_threshold = 7
 
@@ -1385,29 +1401,29 @@
 
 (** Preprocessor entry point **)
 
-(* hol_context -> term
-   -> ((term list * term list) * (bool * bool)) * term * bool *)
+(* hol_context -> term -> term list * term list * bool * bool * bool *)
 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
                                   boxes, skolemize, uncurry, ...}) t =
   let
     val skolem_depth = if skolemize then 4 else ~1
-    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
-         core_t) = t |> unfold_defs_in_term hol_ctxt
-                     |> close_form
-                     |> skolemize_term_and_more hol_ctxt skolem_depth
-                     |> specialize_consts_in_term hol_ctxt 0
-                     |> `(axioms_for_term hol_ctxt)
+    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
+      t |> unfold_defs_in_term hol_ctxt
+        |> close_form
+        |> skolemize_term_and_more hol_ctxt skolem_depth
+        |> specialize_consts_in_term hol_ctxt 0
+        |> axioms_for_term hol_ctxt
     val binarize =
       is_standard_datatype thy stds nat_T andalso
       case binary_ints of
         SOME false => false
-      | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+      | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso
              (binary_ints = SOME true orelse
-              exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+              exists should_use_binary_ints (nondef_ts @ def_ts))
     val box = exists (not_equal (SOME false) o snd) boxes
+    val uncurry = uncurry andalso box
     val table =
-      Termtab.empty |> uncurry
-        ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+      Termtab.empty
+      |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
     (* bool -> term -> term *)
     fun do_rest def =
       binarize ? binarize_nat_and_int_in_term
@@ -1424,12 +1440,10 @@
       #> push_quantifiers_inward
       #> close_form
       #> 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 = map (do_rest false) nondef_ts
-    val core_t = do_rest false core_t
   in
-    (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
-     core_t, binarize)
+    (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
   end
 
 end;