merged
authorblanchet
Tue Dec 07 12:10:13 2010 +0100 (2010-12-07)
changeset 41055d6f45159ae84
parent 41044 1c0eefa8d02a
parent 41054 e58d1cdda832
child 41056 dcec9bc71ee9
merged
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:50:16 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Dec 07 12:10:13 2010 +0100
     1.3 @@ -2108,14 +2108,9 @@
     1.4  per-type basis using the \textit{box}~\qty{type} option described above.
     1.5  
     1.6  \opargboolorsmart{finitize}{type}{dont\_finitize}
     1.7 -Specifies whether Nitpick should attempt to finitize a given type, which can be
     1.8 -a function type or an infinite ``shallow datatype'' (an infinite datatype whose
     1.9 -constructors don't appear in the problem).
    1.10 -
    1.11 -For function types, Nitpick performs a monotonicity analysis to detect functions
    1.12 -that are constant at all but finitely many points (e.g., finite sets) and treats
    1.13 -such occurrences specially, thereby increasing the precision. The option can
    1.14 -then take the following values:
    1.15 +Specifies whether Nitpick should attempt to finitize an infinite ``shallow
    1.16 +datatype'' (an infinite datatype whose constructors don't appear in the
    1.17 +problem). The option can then take the following values:
    1.18  
    1.19  \begin{enum}
    1.20  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
    1.21 @@ -2132,12 +2127,9 @@
    1.22  genuine.''
    1.23  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
    1.24  \item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
    1.25 -detect whether the datatype can be safely finitized before finitizing it.
    1.26 +detect whether the datatype can be soundly finitized before finitizing it.
    1.27  \end{enum}
    1.28  
    1.29 -Like other drastic optimizations, finitization can sometimes prevent the
    1.30 -discovery of counterexamples.
    1.31 -
    1.32  \nopagebreak
    1.33  {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
    1.34  (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
     2.1 --- a/src/HOL/Nitpick.thy	Tue Dec 07 11:50:16 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Tue Dec 07 12:10:13 2010 +0100
     2.3 @@ -35,7 +35,6 @@
     2.4             and Quot :: "'a \<Rightarrow> 'b"
     2.5             and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     2.6  
     2.7 -datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
     2.8  datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
     2.9  datatype ('a, 'b) pair_box = PairBox 'a 'b
    2.10  
    2.11 @@ -76,6 +75,9 @@
    2.12  "tranclp r a b \<equiv> trancl (split r) (a, b)"
    2.13  by (simp add: trancl_def Collect_def mem_def)
    2.14  
    2.15 +definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    2.16 +"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    2.17 +
    2.18  definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
    2.19  "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
    2.20  
    2.21 @@ -237,18 +239,17 @@
    2.22  setup {* Nitpick_Isar.setup *}
    2.23  
    2.24  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    2.25 -    FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    2.26 +    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    2.27      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    2.28      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    2.29      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    2.30 -hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    2.31 -    word
    2.32 -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    2.33 -    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    2.34 -    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    2.35 -    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    2.36 -    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    2.37 -    uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
    2.38 -    less_eq_frac_def of_frac_def
    2.39 +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    2.40 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
    2.41 +    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    2.42 +    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    2.43 +    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    2.44 +    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    2.45 +    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    2.46 +    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    2.47  
    2.48  end
     3.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:50:16 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 12:10:13 2010 +0100
     3.3 @@ -67,7 +67,6 @@
     3.4  ML {* Nitpick_Mono.trace := false *}
     3.5  
     3.6  ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
     3.7 -(*
     3.8  ML {* const @{term "(A\<Colon>'a set) = A"} *}
     3.9  ML {* const @{term "(A\<Colon>'a set set) = A"} *}
    3.10  ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
    3.11 @@ -138,7 +137,6 @@
    3.12  
    3.13  ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
    3.14  ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
    3.15 -*)
    3.16  
    3.17  ML {*
    3.18  val preproc_timeout = SOME (seconds 5.0)
    3.19 @@ -184,8 +182,6 @@
    3.20  
    3.21  fun check_theory thy =
    3.22    let
    3.23 -    val finitizes = [(NONE, SOME false)]
    3.24 -    val monos = [(NONE, SOME false)]
    3.25      val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
    3.26      val _ = File.write path ""
    3.27      fun check_theorem (name, th) =
    3.28 @@ -193,8 +189,7 @@
    3.29          val t = th |> prop_of |> Type.legacy_freeze |> close_form
    3.30          val neg_t = Logic.mk_implies (t, @{prop False})
    3.31          val (nondef_ts, def_ts, _, _, _) =
    3.32 -          time_limit preproc_timeout
    3.33 -              (preprocess_formulas hol_ctxt finitizes monos []) neg_t
    3.34 +          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
    3.35          val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
    3.36        in File.append path (res ^ "\n"); writeln res end
    3.37        handle TimeLimit.TimeOut => ()
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:50:16 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 12:10:13 2010 +0100
     4.3 @@ -179,6 +179,10 @@
     4.4  
     4.5  fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
     4.6  
     4.7 +fun has_lonely_bool_var (@{const Pure.conjunction}
     4.8 +                         $ (@{const Trueprop} $ Free _) $ _) = true
     4.9 +  | has_lonely_bool_var _ = false
    4.10 +
    4.11  val syntactic_sorts =
    4.12    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
    4.13    @{sort number}
    4.14 @@ -229,8 +233,7 @@
    4.15      val print_v = pprint_v o K o plazy
    4.16  
    4.17      fun check_deadline () =
    4.18 -      if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
    4.19 -      else ()
    4.20 +      if passed_deadline deadline then raise TimeLimit.TimeOut else ()
    4.21  
    4.22      val assm_ts = if assms orelse auto then assm_ts else []
    4.23      val _ =
    4.24 @@ -289,7 +292,7 @@
    4.25      val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
    4.26              raise NOT_SUPPORTED "schematic type variables"
    4.27      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
    4.28 -         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
    4.29 +         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
    4.30      val got_all_user_axioms =
    4.31        got_all_mono_user_axioms andalso no_poly_user_axioms
    4.32  
    4.33 @@ -358,9 +361,7 @@
    4.34          SOME (SOME b) => b
    4.35        | _ => is_type_fundamentally_monotonic T orelse
    4.36               is_type_actually_monotonic T
    4.37 -    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
    4.38 -        is_type_kind_of_monotonic T
    4.39 -      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    4.40 +    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    4.41          is_type_kind_of_monotonic T
    4.42        | is_shallow_datatype_finitizable T =
    4.43          case triple_lookup (type_match thy) finitizes T of
    4.44 @@ -661,7 +662,9 @@
    4.45                      \section for details (\"isabelle doc nitpick\")."
    4.46              else
    4.47                ();
    4.48 -            if has_syntactic_sorts orig_t then
    4.49 +            if has_lonely_bool_var orig_t then
    4.50 +              print "Hint: Maybe you forgot a colon after the lemma's name?"
    4.51 +            else if has_syntactic_sorts orig_t then
    4.52                print "Hint: Maybe you forgot a type constraint?"
    4.53              else
    4.54                ();
    4.55 @@ -975,6 +978,9 @@
    4.56                  ".")
    4.57    in (outcome_code, !state_ref) end
    4.58  
    4.59 +(* Give the inner timeout a chance. *)
    4.60 +val timeout_bonus = seconds 0.25
    4.61 +
    4.62  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
    4.63                        step subst assm_ts orig_t =
    4.64    let val warning_m = if auto then K () else warning in
    4.65 @@ -988,7 +994,8 @@
    4.66          val unknown_outcome = ("unknown", state)
    4.67          val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    4.68          val outcome as (outcome_code, _) =
    4.69 -          time_limit (if debug then NONE else timeout)
    4.70 +          time_limit (if debug orelse is_none timeout then NONE
    4.71 +                      else SOME (Time.+ (the timeout, timeout_bonus)))
    4.72                (pick_them_nits_in_term deadline state params auto i n step subst
    4.73                                        assm_ts) orig_t
    4.74            handle TOO_LARGE (_, details) =>
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:50:16 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 12:10:13 2010 +0100
     5.3 @@ -65,6 +65,7 @@
     5.4    val strip_first_name_sep : string -> string * string
     5.5    val original_name : string -> string
     5.6    val abs_var : indexname * typ -> term -> term
     5.7 +  val is_higher_order_type : typ -> bool
     5.8    val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
     5.9    val s_betapply : typ list -> term * term -> term
    5.10    val s_betapplys : typ list -> term * term list -> term
    5.11 @@ -87,7 +88,6 @@
    5.12    val term_match : theory -> term * term -> bool
    5.13    val frac_from_term_pair : typ -> term -> term -> term
    5.14    val is_TFree : typ -> bool
    5.15 -  val is_higher_order_type : typ -> bool
    5.16    val is_fun_type : typ -> bool
    5.17    val is_set_type : typ -> bool
    5.18    val is_pair_type : typ -> bool
    5.19 @@ -319,13 +319,18 @@
    5.20    else
    5.21      s
    5.22  
    5.23 +fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    5.24 +  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    5.25 +  | is_higher_order_type _ = false
    5.26 +
    5.27  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    5.28  
    5.29  fun let_var s = (nitpick_prefix ^ s, 999)
    5.30  val let_inline_threshold = 20
    5.31  
    5.32  fun s_let s n abs_T body_T f t =
    5.33 -  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold then
    5.34 +  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
    5.35 +     is_higher_order_type abs_T then
    5.36      f t
    5.37    else
    5.38      let val z = (let_var s, abs_T) in
    5.39 @@ -419,7 +424,6 @@
    5.40     (@{const_name converse}, 1),
    5.41     (@{const_name trancl}, 1),
    5.42     (@{const_name rel_comp}, 2),
    5.43 -   (@{const_name image}, 2),
    5.44     (@{const_name finite}, 1),
    5.45     (@{const_name unknown}, 0),
    5.46     (@{const_name is_unknown}, 1),
    5.47 @@ -458,9 +462,7 @@
    5.48    | unarize_type @{typ "signed_bit word"} = int_T
    5.49    | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
    5.50    | unarize_type T = T
    5.51 -fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
    5.52 -    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    5.53 -  | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    5.54 +fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    5.55      unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    5.56    | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
    5.57      Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
    5.58 @@ -512,9 +514,6 @@
    5.59  
    5.60  fun is_TFree (TFree _) = true
    5.61    | is_TFree _ = false
    5.62 -fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    5.63 -  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    5.64 -  | is_higher_order_type _ = false
    5.65  fun is_fun_type (Type (@{type_name fun}, _)) = true
    5.66    | is_fun_type _ = false
    5.67  fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    5.68 @@ -803,9 +802,9 @@
    5.69      end
    5.70    | _ => false
    5.71  fun is_constr_like ctxt (s, T) =
    5.72 -  member (op =) [@{const_name FinFun}, @{const_name FunBox},
    5.73 -                 @{const_name PairBox}, @{const_name Quot},
    5.74 -                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
    5.75 +  member (op =) [@{const_name FunBox}, @{const_name PairBox},
    5.76 +                 @{const_name Quot}, @{const_name Zero_Rep},
    5.77 +                 @{const_name Suc_Rep}] s orelse
    5.78    let
    5.79      val thy = ProofContext.theory_of ctxt
    5.80      val (x as (_, T)) = (s, unarize_unbox_etc_type T)
    5.81 @@ -1094,14 +1093,13 @@
    5.82           |> Envir.eta_contract
    5.83           |> new_s <> @{type_name fun}
    5.84              ? construct_value ctxt stds
    5.85 -                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
    5.86 -                   else @{const_name FunBox},
    5.87 +                  (@{const_name FunBox},
    5.88                     Type (@{type_name fun}, new_Ts) --> new_T)
    5.89                o single
    5.90         | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
    5.91      | (Type (new_s, new_Ts as [new_T1, new_T2]),
    5.92         Type (old_s, old_Ts as [old_T1, old_T2])) =>
    5.93 -      if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
    5.94 +      if old_s = @{type_name fun_box} orelse
    5.95           old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
    5.96          case constr_expand hol_ctxt old_T t of
    5.97            Const (old_s, _) $ t1 =>
    5.98 @@ -1643,9 +1641,14 @@
    5.99                  s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
   5.100        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
   5.101          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
   5.102 -      | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
   5.103 -        s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
   5.104 -                        map (do_term depth Ts) [t1, t2])
   5.105 +      | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
   5.106 +        $ t1 $ (t2 as Abs (_, _, t2')) =>
   5.107 +        if loose_bvar1 (t2', 0) then
   5.108 +          s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
   5.109 +        else
   5.110 +          do_term depth Ts
   5.111 +                  (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
   5.112 +                   $ t1 $ incr_boundvars ~1 t2')
   5.113        | Const (x as (@{const_name distinct},
   5.114                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
   5.115          $ (t1 as _ $ _) =>
   5.116 @@ -1658,6 +1661,8 @@
   5.117            do_term depth Ts t2
   5.118          else
   5.119            do_const depth Ts t x [t1, t2, t3]
   5.120 +      | Const (@{const_name Let}, _) $ t1 $ t2 =>
   5.121 +        s_betapply Ts (pairself (do_term depth Ts) (t2, t1))
   5.122        | Const x => do_const depth Ts t x []
   5.123        | t1 $ t2 =>
   5.124          (case strip_comb t of
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:50:16 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 12:10:13 2010 +0100
     6.3 @@ -99,7 +99,7 @@
     6.4                          ""
     6.5                        else
     6.6                          " of Kodkod relation associated with " ^
     6.7 -                        quote guilty_party) ^
     6.8 +                        quote (original_name guilty_party)) ^
     6.9                       " too large for universe of cardinality " ^
    6.10                       string_of_int univ_card)
    6.11    else
    6.12 @@ -1510,55 +1510,6 @@
    6.13             | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
    6.14            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
    6.15          end
    6.16 -      | Op2 (Product, T, R, u1, u2) =>
    6.17 -        let
    6.18 -          val (a_T, b_T) = HOLogic.dest_prodT (domain_type T)
    6.19 -          val a_k = card_of_domain_from_rep 2 (rep_of u1)
    6.20 -          val b_k = card_of_domain_from_rep 2 (rep_of u2)
    6.21 -          val a_R = Atom (a_k, offset_of_type ofs a_T)
    6.22 -          val b_R = Atom (b_k, offset_of_type ofs b_T)
    6.23 -          val body_R = body_rep R
    6.24 -        in
    6.25 -          (case body_R of
    6.26 -             Formula Neut =>
    6.27 -             kk_product (to_rep (Func (a_R, Formula Neut)) u1)
    6.28 -                        (to_rep (Func (b_R, Formula Neut)) u2)
    6.29 -           | Opt (Atom (2, _)) =>
    6.30 -             let
    6.31 -               fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
    6.32 -               fun do_term r =
    6.33 -                 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
    6.34 -             in kk_union (do_term true_atom) (do_term false_atom) end
    6.35 -           | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
    6.36 -          |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
    6.37 -        end
    6.38 -      | Op2 (Image, T, R, u1, u2) =>
    6.39 -        (case (rep_of u1, rep_of u2) of
    6.40 -           (Func (R11, R12), Func (R21, Formula Neut)) =>
    6.41 -           if R21 = R11 andalso is_lone_rep R12 then
    6.42 -             let
    6.43 -               fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
    6.44 -               val core_r = big_join (to_r u2)
    6.45 -               val core_R = Func (R12, Formula Neut)
    6.46 -             in
    6.47 -               if is_opt_rep R12 then
    6.48 -                 let
    6.49 -                   val schema = atom_schema_of_rep R21
    6.50 -                   val decls = decls_for_atom_schema ~1 schema
    6.51 -                   val vars = unary_var_seq ~1 (length decls)
    6.52 -                   val f = kk_some (big_join (fold1 kk_product vars))
    6.53 -                 in
    6.54 -                   kk_rel_if (kk_all decls f)
    6.55 -                             (rel_expr_from_rel_expr kk R core_R core_r)
    6.56 -                             (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)
    6.57 -                                              (kk_product core_r true_atom))
    6.58 -                 end
    6.59 -               else
    6.60 -                 rel_expr_from_rel_expr kk R core_R core_r
    6.61 -             end
    6.62 -           else
    6.63 -             raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
    6.64 -         | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
    6.65        | Op2 (Apply, @{typ nat}, _,
    6.66               Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
    6.67          if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:50:16 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 12:10:13 2010 +0100
     7.3 @@ -178,9 +178,7 @@
     7.4  fun tuple_list_for_name rel_table bounds name =
     7.5    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
     7.6  
     7.7 -fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
     7.8 -    unarize_unbox_etc_term t1
     7.9 -  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    7.10 +fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    7.11      unarize_unbox_etc_term t1
    7.12    | unarize_unbox_etc_term
    7.13          (Const (@{const_name PairBox},
    7.14 @@ -559,9 +557,8 @@
    7.15                    if length arg_Ts = 0 then
    7.16                      []
    7.17                    else
    7.18 -                    map3 (fn Ts =>
    7.19 -                             term_for_rep (constr_s <> @{const_name FinFun})
    7.20 -                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
    7.21 +                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
    7.22 +                         arg_jsss
    7.23                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
    7.24                      |> dest_n_tuple (length uncur_arg_Ts)
    7.25                  val t =
    7.26 @@ -935,8 +932,7 @@
    7.27        Pretty.block (Pretty.breaks
    7.28            (pretty_for_type ctxt typ ::
    7.29             (case typ of
    7.30 -              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
    7.31 -            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    7.32 +              Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    7.33              | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
    7.34              | _ => []) @
    7.35             [Pretty.str "=",
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:50:16 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 12:10:13 2010 +0100
     8.3 @@ -12,9 +12,6 @@
     8.4    val trace : bool Unsynchronized.ref
     8.5    val formulas_monotonic :
     8.6      hol_context -> bool -> typ -> term list * term list -> bool
     8.7 -  val finitize_funs :
     8.8 -    hol_context -> bool -> (typ option * bool option) list -> typ
     8.9 -    -> term list * term list -> term list * term list
    8.10  end;
    8.11  
    8.12  structure Nitpick_Mono : NITPICK_MONO =
    8.13 @@ -41,23 +38,16 @@
    8.14    MType of string * mtyp list |
    8.15    MRec of string * typ list
    8.16  
    8.17 -datatype mterm =
    8.18 -  MRaw of term * mtyp |
    8.19 -  MAbs of string * typ * mtyp * annotation_atom * mterm |
    8.20 -  MApp of mterm * mterm
    8.21 -
    8.22  type mdata =
    8.23    {hol_ctxt: hol_context,
    8.24     binarize: bool,
    8.25     alpha_T: typ,
    8.26 -   no_harmless: bool,
    8.27     max_fresh: int Unsynchronized.ref,
    8.28     datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    8.29     constr_mcache: (styp * mtyp) list Unsynchronized.ref}
    8.30  
    8.31  exception UNSOLVABLE of unit
    8.32  exception MTYPE of string * mtyp list * typ list
    8.33 -exception MTERM of string * mterm list
    8.34  
    8.35  val trace = Unsynchronized.ref false
    8.36  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    8.37 @@ -129,43 +119,9 @@
    8.38    | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
    8.39    | flatten_mtype M = [M]
    8.40  
    8.41 -fun precedence_of_mterm (MRaw _) = no_prec
    8.42 -  | precedence_of_mterm (MAbs _) = 1
    8.43 -  | precedence_of_mterm (MApp _) = 2
    8.44 -
    8.45 -fun string_for_mterm ctxt =
    8.46 -  let
    8.47 -    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
    8.48 -    fun aux outer_prec m =
    8.49 -      let
    8.50 -        val prec = precedence_of_mterm m
    8.51 -        val need_parens = (prec < outer_prec)
    8.52 -      in
    8.53 -        (if need_parens then "(" else "") ^
    8.54 -        (case m of
    8.55 -           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
    8.56 -         | MAbs (s, _, M, aa, m) =>
    8.57 -           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
    8.58 -           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
    8.59 -         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
    8.60 -        (if need_parens then ")" else "")
    8.61 -      end
    8.62 -  in aux 0 end
    8.63 -
    8.64 -fun mtype_of_mterm (MRaw (_, M)) = M
    8.65 -  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
    8.66 -  | mtype_of_mterm (MApp (m1, _)) =
    8.67 -    case mtype_of_mterm m1 of
    8.68 -      MFun (_, _, M12) => M12
    8.69 -    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
    8.70 -
    8.71 -fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
    8.72 -  | strip_mcomb m = (m, [])
    8.73 -
    8.74 -fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
    8.75 +fun initial_mdata hol_ctxt binarize alpha_T =
    8.76    ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    8.77 -    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
    8.78 -    datatype_mcache = Unsynchronized.ref [],
    8.79 +    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
    8.80      constr_mcache = Unsynchronized.ref []} : mdata)
    8.81  
    8.82  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
    8.83 @@ -246,7 +202,7 @@
    8.84                  $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
    8.85    | fin_fun_body _ _ _ = NONE
    8.86  
    8.87 -(* ### FIXME: make sure well-annotated! *)
    8.88 +(* FIXME: make sure well-annotated *)
    8.89  
    8.90  fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
    8.91                              T1 T2 =
    8.92 @@ -309,7 +265,8 @@
    8.93        | _ => MType (simple_string_of_typ T, [])
    8.94    in do_type end
    8.95  
    8.96 -val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
    8.97 +val ground_and_sole_base_constrs = []
    8.98 +(* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
    8.99  
   8.100  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   8.101    | prodM_factors M = [M]
   8.102 @@ -647,8 +604,6 @@
   8.103    {bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame, frees = frees,
   8.104     consts = consts}
   8.105  
   8.106 -(* FIXME: make sure tracing messages are complete *)
   8.107 -
   8.108  fun add_comp_frame aa cmp = fold (add_annotation_atom_comp cmp [] aa o snd)
   8.109  
   8.110  fun add_bound_frame j frame =
   8.111 @@ -694,11 +649,11 @@
   8.112     [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
   8.113     [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
   8.114  
   8.115 -val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
   8.116 -val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
   8.117 -val conj_triple = ("\<and>", conj_clauses, @{const conj})
   8.118 -val disj_triple = ("\<or>", disj_clauses, @{const disj})
   8.119 -val imp_triple = ("\<implies>", imp_clauses, @{const implies})
   8.120 +val meta_conj_spec = ("\<and>", conj_clauses)
   8.121 +val meta_imp_spec = ("\<implies>", imp_clauses)
   8.122 +val conj_spec = ("\<and>", conj_clauses)
   8.123 +val disj_spec = ("\<or>", disj_clauses)
   8.124 +val imp_spec = ("\<implies>", imp_clauses)
   8.125  
   8.126  fun add_annotation_clause_from_quasi_clause _ NONE = NONE
   8.127    | add_annotation_clause_from_quasi_clause [] accum = accum
   8.128 @@ -764,19 +719,17 @@
   8.129      #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
   8.130      #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
   8.131  
   8.132 -fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
   8.133 +fun consider_connective mdata (conn, mk_quasi_clauses) do_t1 do_t2
   8.134                          (accum as ({frame, ...}, _)) =
   8.135    let
   8.136 -    val mtype_for = fresh_mtype_for_type mdata false
   8.137      val frame1 = fresh_frame mdata (SOME Tru) NONE frame
   8.138      val frame2 = fresh_frame mdata (SOME Fls) NONE frame
   8.139 -    val (m1, accum) = accum |>> set_frame frame1 |> do_t1
   8.140 -    val (m2, accum) = accum |>> set_frame frame2 |> do_t2
   8.141    in
   8.142 -    (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   8.143 -     accum |>> set_frame frame
   8.144 -           ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
   8.145 -                                            frame2))
   8.146 +    accum |>> set_frame frame1 |> do_t1
   8.147 +          |>> set_frame frame2 |> do_t2
   8.148 +          |>> set_frame frame
   8.149 +          ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
   8.150 +                                           frame2)
   8.151    end
   8.152  
   8.153  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   8.154 @@ -837,8 +790,9 @@
   8.155          M as MPair (a_M, b_M) =>
   8.156          pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   8.157        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   8.158 -    and do_connect triple t1 t2 =
   8.159 -      consider_connective mdata triple (do_term t1) (do_term t2)
   8.160 +    and do_connect spec t1 t2 accum =
   8.161 +      (bool_M, consider_connective mdata spec (snd o do_term t1)
   8.162 +                                   (snd o do_term t2) accum)
   8.163      and do_term t
   8.164              (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
   8.165                         cset)) =
   8.166 @@ -846,12 +800,10 @@
   8.167                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   8.168                             " : _?");
   8.169         case t of
   8.170 -         @{const False} =>
   8.171 -         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
   8.172 +         @{const False} => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
   8.173         | Const (@{const_name None}, T) =>
   8.174 -         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
   8.175 -       | @{const True} =>
   8.176 -         (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
   8.177 +         (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
   8.178 +       | @{const True} => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
   8.179         | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
   8.180           (* hack to exploit symmetry of equality when typing "insert" *)
   8.181           (if t2 = Bound 0 then do_term @{term True}
   8.182 @@ -873,7 +825,6 @@
   8.183                                    (Abs (Name.uu, domain_type set_T,
   8.184                                          @{const False}),
   8.185                                     Bound 0)))) accum
   8.186 -                |>> mtype_of_mterm
   8.187                end
   8.188              | @{const_name HOL.eq} => do_equals T accum
   8.189              | @{const_name The} =>
   8.190 @@ -912,36 +863,22 @@
   8.191                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
   8.192                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
   8.193                end
   8.194 -            | @{const_name image} =>
   8.195 -              let
   8.196 -                val x = Unsynchronized.inc max_fresh
   8.197 -                val a_M = mtype_for (domain_type (domain_type T))
   8.198 -                val b_M = mtype_for (range_type (domain_type T))
   8.199 -              in
   8.200 -                (MFun (MFun (a_M, A Gen, b_M), A Gen,
   8.201 -                       MFun (MFun (a_M, V x, bool_M), A Gen,
   8.202 -                             MFun (b_M, V x, bool_M))),
   8.203 -                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
   8.204 -              end
   8.205              | @{const_name finite} =>
   8.206                let
   8.207                  val M1 = mtype_for (domain_type (domain_type T))
   8.208                  val a = if exists_alpha_sub_mtype M1 then Fls else Gen
   8.209                in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
   8.210 -            | @{const_name Sigma} =>
   8.211 +            | @{const_name prod} =>
   8.212                let
   8.213                  val x = Unsynchronized.inc max_fresh
   8.214                  fun mtype_for_set T =
   8.215                    MFun (mtype_for (domain_type T), V x, bool_M)
   8.216 -                val a_set_T = domain_type T
   8.217 -                val a_M = mtype_for (domain_type a_set_T)
   8.218 +                val a_set_M = mtype_for_set (domain_type T)
   8.219                  val b_set_M =
   8.220                    mtype_for_set (range_type (domain_type (range_type T)))
   8.221 -                val a_set_M = mtype_for_set a_set_T
   8.222 -                val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
   8.223                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
   8.224                in
   8.225 -                (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
   8.226 +                (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
   8.227                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
   8.228                end
   8.229              | _ =>
   8.230 @@ -964,7 +901,6 @@
   8.231                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   8.232                          frees = frees, consts = (x, M) :: consts}, cset))
   8.233                  end)
   8.234 -           |>> curry MRaw t
   8.235             ||> apsnd (add_comp_frame (A Gen) Eq frame)
   8.236           | Free (x as (_, T)) =>
   8.237             (case AList.lookup (op =) frees x of
   8.238 @@ -974,20 +910,20 @@
   8.239                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   8.240                        frees = (x, M) :: frees, consts = consts}, cset))
   8.241                end)
   8.242 -           |>> curry MRaw t ||> apsnd (add_comp_frame (A Gen) Eq frame)
   8.243 +           ||> apsnd (add_comp_frame (A Gen) Eq frame)
   8.244           | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
   8.245           | Bound j =>
   8.246 -           (MRaw (t, nth bound_Ms j),
   8.247 +           (nth bound_Ms j,
   8.248              accum ||> add_bound_frame (length bound_Ts - j - 1) frame)
   8.249 -         | Abs (s, T, t') =>
   8.250 +         | Abs (_, T, t') =>
   8.251             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   8.252                SOME t' =>
   8.253                let
   8.254                  val M = mtype_for T
   8.255                  val x = Unsynchronized.inc max_fresh
   8.256 -                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
   8.257 +                val (M', accum) = do_term t' (accum |>> push_bound (V x) T M)
   8.258                in
   8.259 -                (MAbs (s, T, M, V x, m'),
   8.260 +                (MFun (M, V x, M'),
   8.261                   accum |>> pop_bound
   8.262                         ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
   8.263                end
   8.264 @@ -1009,13 +945,13 @@
   8.265                        let
   8.266                          val M = mtype_for T
   8.267                          val x = Unsynchronized.inc max_fresh
   8.268 -                        val (m', accum) =
   8.269 +                        val (M', accum) =
   8.270                            do_term t' (accum |>> push_bound (V x) T M)
   8.271 -                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
   8.272 -         | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
   8.273 -         | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
   8.274 -         | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
   8.275 -         | @{const implies} $ t1 $ t2 => do_connect imp_triple t1 t2 accum
   8.276 +                      in (MFun (M, V x, M'), accum |>> pop_bound) end))
   8.277 +         | @{const Not} $ t1 => do_connect imp_spec t1 @{const False} accum
   8.278 +         | @{const conj} $ t1 $ t2 => do_connect conj_spec t1 t2 accum
   8.279 +         | @{const disj} $ t1 $ t2 => do_connect disj_spec t1 t2 accum
   8.280 +         | @{const implies} $ t1 $ t2 => do_connect imp_spec t1 t2 accum
   8.281           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   8.282             do_term (betapply (t2, t1)) accum
   8.283           | t1 $ t2 =>
   8.284 @@ -1028,121 +964,106 @@
   8.285               val frame2b =
   8.286                 frame1b |> map (apsnd (fn _ => V (Unsynchronized.inc max_fresh)))
   8.287               val frame2 = frame2a @ frame2b
   8.288 -             val (m1, accum) = accum |>> set_frame frame1a |> do_term t1
   8.289 -             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   8.290 +             val (M1, accum) = accum |>> set_frame frame1a |> do_term t1
   8.291 +             val (M2, accum) = accum |>> set_frame frame2 |> do_term t2
   8.292             in
   8.293               let
   8.294 -               val (M11, aa, _) = mtype_of_mterm m1 |> dest_MFun
   8.295 -               val M2 = mtype_of_mterm m2
   8.296 +               val (M11, aa, M12) = M1 |> dest_MFun
   8.297               in
   8.298 -               (MApp (m1, m2),
   8.299 -                accum |>> set_frame frame
   8.300 -                      ||> add_is_sub_mtype M2 M11
   8.301 -                      ||> add_app aa frame1b frame2b)
   8.302 +               (M12, accum |>> set_frame frame
   8.303 +                           ||> add_is_sub_mtype M2 M11
   8.304 +                           ||> add_app aa frame1b frame2b)
   8.305               end
   8.306             end)
   8.307 -        |> tap (fn (m, (gamma, _)) =>
   8.308 +        |> tap (fn (M, (gamma, _)) =>
   8.309                     trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   8.310                                         " \<turnstile> " ^
   8.311 -                                       string_for_mterm ctxt m))
   8.312 +                                       Syntax.string_of_term ctxt t ^ " : " ^
   8.313 +                                       string_for_mtype M))
   8.314    in do_term end
   8.315  
   8.316  fun force_gen_funs 0 _ = I
   8.317    | force_gen_funs n (M as MFun (M1, _, M2)) =
   8.318      add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
   8.319    | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
   8.320 -fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   8.321 +fun consider_general_equals mdata def t1 t2 accum =
   8.322    let
   8.323 -    val (m1, accum) = consider_term mdata t1 accum
   8.324 -    val (m2, accum) = consider_term mdata t2 accum
   8.325 -    val M1 = mtype_of_mterm m1
   8.326 -    val M2 = mtype_of_mterm m2
   8.327 +    val (M1, accum) = consider_term mdata t1 accum
   8.328 +    val (M2, accum) = consider_term mdata t2 accum
   8.329      val accum = accum ||> add_mtypes_equal M1 M2
   8.330 -    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   8.331 -    val m = MApp (MApp (MRaw (Const x,
   8.332 -                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
   8.333    in
   8.334 -    (m, (if def then
   8.335 -           let val (head_m, arg_ms) = strip_mcomb m1 in
   8.336 -             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
   8.337 -           end
   8.338 -         else
   8.339 -           accum))
   8.340 +    if def then
   8.341 +      let
   8.342 +        val (head1, args1) = strip_comb t1
   8.343 +        val (head_M1, accum) = consider_term mdata head1 accum
   8.344 +      in accum ||> force_gen_funs (length args1) head_M1 end
   8.345 +    else
   8.346 +      accum
   8.347    end
   8.348  
   8.349  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,
   8.350                                          ...}) =
   8.351    let
   8.352      val mtype_for = fresh_mtype_for_type mdata false
   8.353 -    val do_term = consider_term mdata
   8.354 +    val do_term = snd oo consider_term mdata
   8.355      fun do_formula sn t (accum as (gamma, _)) =
   8.356        let
   8.357 -        fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   8.358 +        fun do_quantifier quant_s abs_T body_t =
   8.359            let
   8.360              val abs_M = mtype_for abs_T
   8.361              val x = Unsynchronized.inc max_fresh
   8.362              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   8.363              fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
   8.364 -            val (body_m, accum) =
   8.365 -              accum ||> side_cond
   8.366 -                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
   8.367 -                    |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
   8.368 -            val body_M = mtype_of_mterm body_m
   8.369            in
   8.370 -            (MApp (MRaw (Const quant_x,
   8.371 -                         MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
   8.372 -                   MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   8.373 -             accum |>> pop_bound)
   8.374 +            accum ||> side_cond
   8.375 +                      ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
   8.376 +                  |>> push_bound (V x) abs_T abs_M
   8.377 +                  |> do_formula sn body_t
   8.378 +                  |>> pop_bound
   8.379            end
   8.380 -        fun do_connect triple neg1 t1 t2 =
   8.381 -          consider_connective mdata triple
   8.382 +        fun do_connect spec neg1 t1 t2 =
   8.383 +          consider_connective mdata spec
   8.384                (do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
   8.385 -        fun do_equals x t1 t2 =
   8.386 +        fun do_equals t1 t2 =
   8.387            case sn of
   8.388              Plus => do_term t accum
   8.389 -          | Minus => consider_general_equals mdata false x t1 t2 accum
   8.390 +          | Minus => consider_general_equals mdata false t1 t2 accum
   8.391        in
   8.392          trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   8.393                              " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   8.394                              " : o\<^sup>" ^ string_for_sign sn ^ "?");
   8.395          case t of
   8.396 -          Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   8.397 -          do_quantifier x s1 T1 t1
   8.398 -        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
   8.399 -        | @{const Trueprop} $ t1 =>
   8.400 -          let val (m1, accum) = do_formula sn t1 accum in
   8.401 -            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
   8.402 -             accum)
   8.403 -          end
   8.404 -        | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   8.405 -          do_quantifier x s1 T1 t1
   8.406 -        | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
   8.407 +          Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
   8.408 +          do_quantifier s T1 t1
   8.409 +        | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
   8.410 +        | @{const Trueprop} $ t1 => do_formula sn t1 accum
   8.411 +        | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
   8.412 +          do_quantifier s T1 t1
   8.413 +        | Const (s as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
   8.414            (case sn of
   8.415 -             Plus => do_quantifier x0 s1 T1 t1'
   8.416 +             Plus => do_quantifier s T1 t1'
   8.417             | Minus =>
   8.418 -             (* FIXME: Move elsewhere *)
   8.419 +             (* FIXME: Needed? *)
   8.420               do_term (@{const Not}
   8.421                        $ (HOLogic.eq_const (domain_type T0) $ t1
   8.422                           $ Abs (Name.uu, T1, @{const False}))) accum)
   8.423 -        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_equals x t1 t2
   8.424 +        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_equals t1 t2
   8.425          | Const (@{const_name Let}, _) $ t1 $ t2 =>
   8.426            do_formula sn (betapply (t2, t1)) accum
   8.427          | @{const Pure.conjunction} $ t1 $ t2 =>
   8.428 -          do_connect meta_conj_triple false t1 t2 accum
   8.429 -        | @{const "==>"} $ t1 $ t2 =>
   8.430 -          do_connect meta_imp_triple true t1 t2 accum
   8.431 -        | @{const Not} $ t1 =>
   8.432 -          do_connect imp_triple true t1 @{const False} accum
   8.433 -        | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
   8.434 -        | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
   8.435 -        | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
   8.436 +          do_connect meta_conj_spec false t1 t2 accum
   8.437 +        | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   8.438 +        | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
   8.439 +        | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
   8.440 +        | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
   8.441 +        | @{const implies} $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
   8.442          | _ => do_term t accum
   8.443        end
   8.444 -      |> tap (fn (m, (gamma, _)) =>
   8.445 +      |> tap (fn (gamma, _) =>
   8.446                   trace_msg (fn () => string_for_mcontext ctxt t gamma ^
   8.447                                       " \<turnstile> " ^
   8.448 -                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   8.449 -                                     string_for_sign sn))
   8.450 +                                     Syntax.string_of_term ctxt t ^
   8.451 +                                     " : o\<^sup>" ^ string_for_sign sn))
   8.452    in do_formula end
   8.453  
   8.454  (* The harmless axiom optimization below is somewhat too aggressive in the face
   8.455 @@ -1151,72 +1072,44 @@
   8.456    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
   8.457  val bounteous_consts = [@{const_name bisim}]
   8.458  
   8.459 -fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
   8.460 -  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
   8.461 +fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
   8.462      Term.add_consts t []
   8.463      |> filter_out (is_built_in_const thy stds)
   8.464      |> (forall (member (op =) harmless_consts o original_name o fst) orf
   8.465          exists (member (op =) bounteous_consts o fst))
   8.466  
   8.467  fun consider_nondefinitional_axiom mdata t =
   8.468 -  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
   8.469 +  if is_harmless_axiom mdata t then I
   8.470    else consider_general_formula mdata Plus t
   8.471  
   8.472  fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
   8.473    if not (is_constr_pattern_formula ctxt t) then
   8.474      consider_nondefinitional_axiom mdata t
   8.475    else if is_harmless_axiom mdata t then
   8.476 -    pair (MRaw (t, dummy_M))
   8.477 +    I
   8.478    else
   8.479      let
   8.480        val mtype_for = fresh_mtype_for_type mdata false
   8.481 -      val do_term = consider_term mdata
   8.482 -      fun do_all quant_t abs_s abs_T body_t accum =
   8.483 -        let
   8.484 -          val abs_M = mtype_for abs_T
   8.485 -          val (body_m, accum) =
   8.486 -            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
   8.487 -          val body_M = mtype_of_mterm body_m
   8.488 -        in
   8.489 -          (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
   8.490 -                       body_M)),
   8.491 -                 MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   8.492 -           accum |>> pop_bound)
   8.493 -        end
   8.494 -      and do_conjunction t0 t1 t2 accum =
   8.495 -        let
   8.496 -          val (m1, accum) = do_formula t1 accum
   8.497 -          val (m2, accum) = do_formula t2 accum
   8.498 -        in
   8.499 -          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   8.500 -        end
   8.501 -      and do_implies t0 t1 t2 accum =
   8.502 -        let
   8.503 -          val (m1, accum) = do_term t1 accum
   8.504 -          val (m2, accum) = do_formula t2 accum
   8.505 -        in
   8.506 -          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   8.507 -        end
   8.508 +      val do_term = snd oo consider_term mdata
   8.509 +      fun do_all abs_T body_t accum =
   8.510 +        accum |>> push_bound (A Gen) abs_T (mtype_for abs_T)
   8.511 +              |> do_formula body_t
   8.512 +              |>> pop_bound
   8.513 +      and do_implies t1 t2 = do_term t1 #> do_formula t2
   8.514        and do_formula t accum =
   8.515          case t of
   8.516 -          (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   8.517 -          do_all t0 s1 T1 t1 accum
   8.518 -        | @{const Trueprop} $ t1 =>
   8.519 -          let val (m1, accum) = do_formula t1 accum in
   8.520 -            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
   8.521 -             accum)
   8.522 -          end
   8.523 -        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
   8.524 -          consider_general_equals mdata true x t1 t2 accum
   8.525 -        | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   8.526 -        | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
   8.527 -          do_conjunction t0 t1 t2 accum
   8.528 -        | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
   8.529 -          do_all t0 s0 T1 t1 accum
   8.530 -        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   8.531 -          consider_general_equals mdata true x t1 t2 accum
   8.532 -        | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   8.533 -        | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   8.534 +          Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   8.535 +        | @{const Trueprop} $ t1 => do_formula t1 accum
   8.536 +        | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   8.537 +          consider_general_equals mdata true t1 t2 accum
   8.538 +        | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
   8.539 +        | @{const Pure.conjunction} $ t1 $ t2 =>
   8.540 +          fold (do_formula) [t1, t2] accum
   8.541 +        | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   8.542 +        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   8.543 +          consider_general_equals mdata true t1 t2 accum
   8.544 +        | @{const conj} $ t1 $ t2 => fold (do_formula) [t1, t2] accum
   8.545 +        | @{const implies} $ t1 $ t2 => do_implies t1 t2 accum
   8.546          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   8.547                             \do_formula", [t])
   8.548      in do_formula t end
   8.549 @@ -1230,143 +1123,26 @@
   8.550        map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
   8.551        |> cat_lines)
   8.552  
   8.553 -fun amass f t (ms, accum) =
   8.554 -  let val (m, accum) = f t accum in (m :: ms, accum) end
   8.555 -
   8.556 -fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
   8.557 -          alpha_T (nondef_ts, def_ts) =
   8.558 +fun formulas_monotonic (hol_ctxt as {ctxt, tac_timeout, ...}) binarize alpha_T
   8.559 +                       (nondef_ts, def_ts) =
   8.560    let
   8.561 -    val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   8.562 +    val _ = trace_msg (fn () => "****** Monotonicity analysis: " ^
   8.563                                  string_for_mtype MAlpha ^ " is " ^
   8.564                                  Syntax.string_of_typ ctxt alpha_T)
   8.565 -    val mdata as {max_fresh, constr_mcache, ...} =
   8.566 -      initial_mdata hol_ctxt binarize no_harmless alpha_T
   8.567 -    val accum = (initial_gamma, ([], []))
   8.568 -    val (nondef_ms, accum) =
   8.569 -      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
   8.570 -                  |> fold (amass (consider_nondefinitional_axiom mdata))
   8.571 -                          (tl nondef_ts)
   8.572 -    val (def_ms, (gamma, cset)) =
   8.573 -      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   8.574 +    val mdata as {max_fresh, ...} = initial_mdata hol_ctxt binarize alpha_T
   8.575 +    val (gamma, cset) =
   8.576 +      (initial_gamma, ([], []))
   8.577 +      |> consider_general_formula mdata Plus (hd nondef_ts)
   8.578 +      |> fold (consider_nondefinitional_axiom mdata) (tl nondef_ts)
   8.579 +      |> fold (consider_definitional_axiom mdata) def_ts
   8.580    in
   8.581      case solve tac_timeout (!max_fresh) cset of
   8.582 -      SOME asgs => (print_mcontext ctxt asgs gamma;
   8.583 -                    SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   8.584 -    | _ => NONE
   8.585 +      SOME asgs => (print_mcontext ctxt asgs gamma; true)
   8.586 +    | _ => false
   8.587    end
   8.588 -  handle UNSOLVABLE () => NONE
   8.589 +  handle UNSOLVABLE () => false
   8.590         | MTYPE (loc, Ms, Ts) =>
   8.591           raise BAD (loc, commas (map string_for_mtype Ms @
   8.592                                   map (Syntax.string_of_typ ctxt) Ts))
   8.593 -       | MTERM (loc, ms) =>
   8.594 -         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
   8.595 -
   8.596 -val formulas_monotonic = is_some oooo infer "Monotonicity" false
   8.597 -
   8.598 -fun fin_fun_constr T1 T2 =
   8.599 -  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
   8.600 -
   8.601 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
   8.602 -                  finitizes alpha_T tsp =
   8.603 -  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   8.604 -    SOME (asgs, msp, constr_mtypes) =>
   8.605 -    if forall (curry (op =) Gen o snd) asgs then
   8.606 -      tsp
   8.607 -    else
   8.608 -      let
   8.609 -        fun should_finitize T aa =
   8.610 -          case triple_lookup (type_match thy) finitizes T of
   8.611 -            SOME (SOME false) => false
   8.612 -          | _ => resolve_annotation_atom asgs aa = A Fls
   8.613 -        fun type_from_mtype T M =
   8.614 -          case (M, T) of
   8.615 -            (MAlpha, _) => T
   8.616 -          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
   8.617 -            Type (if should_finitize T aa then @{type_name fin_fun}
   8.618 -                  else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
   8.619 -          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
   8.620 -            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
   8.621 -          | (MType _, _) => T
   8.622 -          | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
   8.623 -                              [M], [T])
   8.624 -        fun finitize_constr (x as (s, T)) =
   8.625 -          (s, case AList.lookup (op =) constr_mtypes x of
   8.626 -                SOME M => type_from_mtype T M
   8.627 -              | NONE => T)
   8.628 -        fun term_from_mterm new_Ts old_Ts m =
   8.629 -          case m of
   8.630 -            MRaw (t, M) =>
   8.631 -            let
   8.632 -              val T = fastype_of1 (old_Ts, t)
   8.633 -              val T' = type_from_mtype T M
   8.634 -            in
   8.635 -              case t of
   8.636 -                Const (x as (s, _)) =>
   8.637 -                if s = @{const_name finite} then
   8.638 -                  case domain_type T' of
   8.639 -                    set_T' as Type (@{type_name fin_fun}, _) =>
   8.640 -                    Abs (Name.uu, set_T', @{const True})
   8.641 -                  | _ => Const (s, T')
   8.642 -                else if s = @{const_name "=="} orelse
   8.643 -                        s = @{const_name HOL.eq} then
   8.644 -                  let
   8.645 -                    val T =
   8.646 -                      case T' of
   8.647 -                        Type (_, [T1, Type (_, [T2, T3])]) =>
   8.648 -                        T1 --> T2 --> T3
   8.649 -                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
   8.650 -                                         \term_from_mterm", [T, T'], [])
   8.651 -                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
   8.652 -                else if is_built_in_const thy stds x then
   8.653 -                  coerce_term hol_ctxt new_Ts T' T t
   8.654 -                else if is_constr ctxt stds x then
   8.655 -                  Const (finitize_constr x)
   8.656 -                else if is_sel s then
   8.657 -                  let
   8.658 -                    val n = sel_no_from_name s
   8.659 -                    val x' =
   8.660 -                      x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
   8.661 -                        |> finitize_constr
   8.662 -                    val x'' =
   8.663 -                      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
   8.664 -                                                             x' n
   8.665 -                  in Const x'' end
   8.666 -                else
   8.667 -                  Const (s, T')
   8.668 -              | Free (s, T) => Free (s, type_from_mtype T M)
   8.669 -              | Bound _ => t
   8.670 -              | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
   8.671 -                                  [m])
   8.672 -            end
   8.673 -          | MApp (m1, m2) =>
   8.674 -            let
   8.675 -              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
   8.676 -              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
   8.677 -              val (t1', T2') =
   8.678 -                case T1 of
   8.679 -                  Type (s, [T11, T12]) =>
   8.680 -                  (if s = @{type_name fin_fun} then
   8.681 -                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
   8.682 -                                           0 (T11 --> T12)
   8.683 -                   else
   8.684 -                     t1, T11)
   8.685 -                | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
   8.686 -                                   [T1], [])
   8.687 -            in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
   8.688 -          | MAbs (s, old_T, M, aa, m') =>
   8.689 -            let
   8.690 -              val new_T = type_from_mtype old_T M
   8.691 -              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
   8.692 -              val T' = fastype_of1 (new_T :: new_Ts, t')
   8.693 -            in
   8.694 -              Abs (s, new_T, t')
   8.695 -              |> should_finitize (new_T --> T') aa
   8.696 -                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
   8.697 -            end
   8.698 -      in
   8.699 -        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
   8.700 -        pairself (map (term_from_mterm [] [])) msp
   8.701 -      end
   8.702 -  | NONE => tsp
   8.703  
   8.704  end;
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:50:16 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 12:10:13 2010 +0100
     9.3 @@ -55,8 +55,6 @@
     9.4      Eq |
     9.5      Triad |
     9.6      Composition |
     9.7 -    Product |
     9.8 -    Image |
     9.9      Apply |
    9.10      Lambda
    9.11  
    9.12 @@ -170,8 +168,6 @@
    9.13    Eq |
    9.14    Triad |
    9.15    Composition |
    9.16 -  Product |
    9.17 -  Image |
    9.18    Apply |
    9.19    Lambda
    9.20  
    9.21 @@ -235,8 +231,6 @@
    9.22    | string_for_op2 Eq = "Eq"
    9.23    | string_for_op2 Triad = "Triad"
    9.24    | string_for_op2 Composition = "Composition"
    9.25 -  | string_for_op2 Product = "Product"
    9.26 -  | string_for_op2 Image = "Image"
    9.27    | string_for_op2 Apply = "Apply"
    9.28    | string_for_op2 Lambda = "Lambda"
    9.29  
    9.30 @@ -528,10 +522,6 @@
    9.31            Op1 (Closure, range_type T, Any, sub t1)
    9.32          | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
    9.33            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    9.34 -        | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
    9.35 -          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
    9.36 -        | (Const (@{const_name image}, T), [t1, t2]) =>
    9.37 -          Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    9.38          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    9.39            if is_built_in_const thy stds x then Cst (Suc, T, Any)
    9.40            else if is_constr ctxt stds x then do_construct x []
    9.41 @@ -941,46 +931,6 @@
    9.42                Cst (False, T, Formula Pos)
    9.43                |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
    9.44            end
    9.45 -        | Op2 (Image, T, _, u1, u2) =>
    9.46 -          let
    9.47 -            val u1' = sub u1
    9.48 -            val u2' = sub u2
    9.49 -          in
    9.50 -            (case (rep_of u1', rep_of u2') of
    9.51 -               (Func (R11, R12), Func (R21, Formula Neut)) =>
    9.52 -               if R21 = R11 andalso is_lone_rep R12 then
    9.53 -                 let
    9.54 -                   val R =
    9.55 -                     best_non_opt_set_rep_for_type scope T
    9.56 -                     |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
    9.57 -                 in s_op2 Image T R u1' u2' end
    9.58 -               else
    9.59 -                 raise SAME ()
    9.60 -             | _ => raise SAME ())
    9.61 -            handle SAME () =>
    9.62 -                   let
    9.63 -                     val T1 = type_of u1
    9.64 -                     val dom_T = domain_type T1
    9.65 -                     val ran_T = range_type T1
    9.66 -                     val x_u = BoundName (~1, dom_T, Any, "image.x")
    9.67 -                     val y_u = BoundName (~2, ran_T, Any, "image.y")
    9.68 -                   in
    9.69 -                     Op2 (Lambda, T, Any, y_u,
    9.70 -                          Op2 (Exist, bool_T, Any, x_u,
    9.71 -                               Op2 (And, bool_T, Any,
    9.72 -                                    case u2 of
    9.73 -                                      Op2 (Lambda, _, _, u21, u22) =>
    9.74 -                                      if num_occurrences_in_nut u21 u22 = 0 then
    9.75 -                                        u22
    9.76 -                                      else
    9.77 -                                        Op2 (Apply, bool_T, Any, u2, x_u)
    9.78 -                                    | _ => Op2 (Apply, bool_T, Any, u2, x_u),
    9.79 -
    9.80 -                                    Op2 (Eq, bool_T, Any, y_u,
    9.81 -                                         Op2 (Apply, ran_T, Any, u1, x_u)))))
    9.82 -                     |> sub
    9.83 -                   end
    9.84 -          end
    9.85          | Op2 (Apply, T, _, u1, u2) =>
    9.86            let
    9.87              val u1 = sub u1
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:50:16 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 12:10:13 2010 +0100
    10.3 @@ -9,8 +9,7 @@
    10.4  sig
    10.5    type hol_context = Nitpick_HOL.hol_context
    10.6    val preprocess_formulas :
    10.7 -    hol_context -> (typ option * bool option) list
    10.8 -    -> (typ option * bool option) list -> term list -> term
    10.9 +    hol_context -> term list -> term
   10.10      -> term list * term list * bool * bool * bool
   10.11  end;
   10.12  
   10.13 @@ -1245,32 +1244,13 @@
   10.14               | _ => t
   10.15    in aux "" [] [] end
   10.16  
   10.17 -(** Inference of finite functions **)
   10.18 -
   10.19 -fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
   10.20 -                               (nondef_ts, def_ts) =
   10.21 -  if forall (curry (op =) (SOME false) o snd) finitizes then
   10.22 -    (nondef_ts, def_ts)
   10.23 -  else
   10.24 -    let
   10.25 -      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
   10.26 -               |> filter_out (fn Type (@{type_name fun_box}, _) => true
   10.27 -                               | @{typ signed_bit} => true
   10.28 -                               | @{typ unsigned_bit} => true
   10.29 -                               | T => is_small_finite_type hol_ctxt T orelse
   10.30 -                                      triple_lookup (type_match thy) monos T
   10.31 -                                      = SOME (SOME false))
   10.32 -    in
   10.33 -      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
   10.34 -    end
   10.35 -
   10.36  (** Preprocessor entry point **)
   10.37  
   10.38  val max_skolem_depth = 3
   10.39  
   10.40  fun preprocess_formulas
   10.41          (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
   10.42 -                      ...}) finitizes monos assm_ts neg_t =
   10.43 +                      ...}) assm_ts neg_t =
   10.44    let
   10.45      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
   10.46        neg_t |> unfold_defs_in_term hol_ctxt
   10.47 @@ -1307,9 +1287,6 @@
   10.48        #> Term.map_abs_vars shortest_name
   10.49      val nondef_ts = map (do_rest false) nondef_ts
   10.50      val def_ts = map (do_rest true) def_ts
   10.51 -    val (nondef_ts, def_ts) =
   10.52 -      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
   10.53 -                                 (nondef_ts, def_ts)
   10.54    in
   10.55      (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
   10.56    end
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:50:16 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 12:10:13 2010 +0100
    11.3 @@ -112,8 +112,6 @@
    11.4  
    11.5  fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
    11.6      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
    11.7 -  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
    11.8 -    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
    11.9    | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
   11.10      forall (is_complete_type dtypes facto) Ts
   11.11    | is_complete_type dtypes facto T =
   11.12 @@ -122,8 +120,6 @@
   11.13      handle Option.Option => true
   11.14  and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
   11.15      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
   11.16 -  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
   11.17 -    is_concrete_type dtypes facto T2
   11.18    | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
   11.19      forall (is_concrete_type dtypes facto) Ts
   11.20    | is_concrete_type dtypes facto T =