added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
authorblanchet
Thu Feb 18 18:48:07 2010 +0100 (2010-02-18)
changeset 352202bcdae5f4fdb
parent 35219 15a5f213ef5b
child 35221 5cb63cb4213f
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Feb 18 10:38:37 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Feb 18 18:48:07 2010 +0100
     1.3 @@ -472,7 +472,7 @@
     1.4  \prew
     1.5  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
     1.6  \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
     1.7 -\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
     1.8 +\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
     1.9  fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.10  Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.11  \hbox{}\qquad Free variable: \nopagebreak \\
    1.12 @@ -2083,7 +2083,6 @@
    1.13  Specifies whether the given (recursive) datatype should be given standard
    1.14  models. Nonstandard models are unsound but can help debug structural induction
    1.15  proofs, as explained in \S\ref{inductive-properties}.
    1.16 -%This option is not supported for the type \textit{nat}.
    1.17  
    1.18  \optrue{std}{non\_std}
    1.19  Specifies the default standardness to use. This can be overridden on a per-type
     2.1 --- a/src/HOL/Nitpick.thy	Thu Feb 18 10:38:37 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Thu Feb 18 18:48:07 2010 +0100
     2.3 @@ -217,21 +217,6 @@
     2.4  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
     2.5  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
     2.6  
     2.7 -(* While Nitpick normally avoids to unfold definitions for locales, it
     2.8 -   unfortunately needs to unfold them when dealing with the following built-in
     2.9 -   constants. A cleaner approach would be to change "Nitpick_HOL" and
    2.10 -   "Nitpick_Nut" so that they handle the unexpanded overloaded constants
    2.11 -   directly, but this is slightly more tricky to implement. *)
    2.12 -lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
    2.13 -    div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun
    2.14 -    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
    2.15 -    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
    2.16 -    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
    2.17 -    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
    2.18 -    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
    2.19 -    semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int
    2.20 -    zero_nat_inst.zero_nat
    2.21 -
    2.22  use "Tools/Nitpick/kodkod.ML"
    2.23  use "Tools/Nitpick/kodkod_sat.ML"
    2.24  use "Tools/Nitpick/nitpick_util.ML"
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 18 10:38:37 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 18 18:48:07 2010 +0100
     3.3 @@ -265,7 +265,7 @@
     3.4                       orig_assm_ts
     3.5  *)
     3.6      val max_bisim_depth = fold Integer.max bisim_depths ~1
     3.7 -    val case_names = case_const_names thy
     3.8 +    val case_names = case_const_names thy stds
     3.9      val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
    3.10      val def_table = const_def_table ctxt defs
    3.11      val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    3.12 @@ -337,7 +337,7 @@
    3.13      val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
    3.14      (* typ -> bool *)
    3.15      fun is_type_always_monotonic T =
    3.16 -      (is_datatype thy T andalso not (is_quot_type thy T) andalso
    3.17 +      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
    3.18         (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
    3.19        is_number_type thy T orelse is_bit_type T
    3.20      fun is_type_monotonic T =
    3.21 @@ -347,8 +347,8 @@
    3.22        | _ => is_type_always_monotonic T orelse
    3.23               formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
    3.24      fun is_deep_datatype T =
    3.25 -      is_datatype thy T andalso
    3.26 -      (not standard orelse is_word_type T orelse
    3.27 +      is_datatype thy stds T andalso
    3.28 +      (not standard orelse T = nat_T orelse is_word_type T orelse
    3.29         exists (curry (op =) T o domain_type o type_of) sel_names)
    3.30      val all_Ts = ground_types_in_terms hol_ctxt binarize
    3.31                                         (core_t :: def_ts @ nondef_ts)
    3.32 @@ -519,8 +519,9 @@
    3.33            declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
    3.34                                             rel_table datatypes
    3.35          val declarative_axioms = plain_axioms @ dtype_axioms
    3.36 -        val univ_card = univ_card nat_card int_card main_j0
    3.37 -                                  (plain_bounds @ sel_bounds) formula
    3.38 +        val univ_card = Int.max (univ_card nat_card int_card main_j0
    3.39 +                                     (plain_bounds @ sel_bounds) formula,
    3.40 +                                 main_j0 |> bits > 0 ? Integer.add (bits + 1))
    3.41          val built_in_bounds = bounds_for_built_in_rels_in_formula debug
    3.42                                    univ_card nat_card int_card main_j0 formula
    3.43          val bounds = built_in_bounds @ plain_bounds @ sel_bounds
    3.44 @@ -837,8 +838,9 @@
    3.45                   forall (KK.is_problem_trivially_false o fst)
    3.46                          sound_problems then
    3.47                  print_m (fn () =>
    3.48 -                    "Warning: The conjecture either trivially holds or (more \
    3.49 -                    \likely) lies outside Nitpick's supported fragment." ^
    3.50 +                    "Warning: The conjecture either trivially holds for the \
    3.51 +                    \given scopes or (more likely) lies outside Nitpick's \
    3.52 +                    \supported fragment." ^
    3.53                      (if exists (not o KK.is_problem_trivially_false o fst)
    3.54                                 unsound_problems then
    3.55                         " Only potential counterexamples may be found."
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 18 10:38:37 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 18 18:48:07 2010 +0100
     4.3 @@ -85,6 +85,7 @@
     4.4    val is_integer_type : typ -> bool
     4.5    val is_bit_type : typ -> bool
     4.6    val is_word_type : typ -> bool
     4.7 +  val is_integer_like_type : typ -> bool
     4.8    val is_record_type : typ -> bool
     4.9    val is_number_type : theory -> typ -> bool
    4.10    val const_for_iterator_type : typ -> styp
    4.11 @@ -95,14 +96,13 @@
    4.12    val curried_binder_types : typ -> typ list
    4.13    val mk_flat_tuple : typ -> term list -> term
    4.14    val dest_n_tuple : int -> term -> term list
    4.15 -  val instantiate_type : theory -> typ -> typ -> typ -> typ
    4.16    val is_real_datatype : theory -> string -> bool
    4.17 -  val is_standard_datatype : hol_context -> typ -> bool
    4.18 +  val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
    4.19    val is_quot_type : theory -> typ -> bool
    4.20    val is_codatatype : theory -> typ -> bool
    4.21    val is_pure_typedef : theory -> typ -> bool
    4.22    val is_univ_typedef : theory -> typ -> bool
    4.23 -  val is_datatype : theory -> typ -> bool
    4.24 +  val is_datatype : theory -> (typ option * bool) list -> typ -> bool
    4.25    val is_record_constr : styp -> bool
    4.26    val is_record_get : theory -> styp -> bool
    4.27    val is_record_update : theory -> styp -> bool
    4.28 @@ -113,7 +113,7 @@
    4.29    val mate_of_rep_fun : theory -> styp -> styp
    4.30    val is_constr_like : theory -> styp -> bool
    4.31    val is_stale_constr : theory -> styp -> bool
    4.32 -  val is_constr : theory -> styp -> bool
    4.33 +  val is_constr : theory -> (typ option * bool) list -> styp -> bool
    4.34    val is_sel : string -> bool
    4.35    val is_sel_like_and_no_discr : string -> bool
    4.36    val box_type : hol_context -> boxability -> typ -> typ
    4.37 @@ -141,8 +141,10 @@
    4.38    val constr_name_for_sel_like : string -> string
    4.39    val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
    4.40    val discriminate_value : hol_context -> styp -> term -> term
    4.41 -  val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
    4.42 -  val construct_value : theory -> styp -> term list -> term
    4.43 +  val select_nth_constr_arg :
    4.44 +    theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
    4.45 +  val construct_value :
    4.46 +    theory -> (typ option * bool) list -> styp -> term list -> term
    4.47    val card_of_type : (typ * int) list -> typ -> int
    4.48    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    4.49    val bounded_exact_card_of_type :
    4.50 @@ -151,10 +153,13 @@
    4.51    val special_bounds : term list -> (indexname * typ) list
    4.52    val is_funky_typedef : theory -> typ -> bool
    4.53    val all_axioms_of : theory -> term list * term list * term list
    4.54 -  val arity_of_built_in_const : bool -> styp -> int option
    4.55 -  val is_built_in_const : bool -> styp -> bool
    4.56 +  val arity_of_built_in_const :
    4.57 +    theory -> (typ option * bool) list -> bool -> styp -> int option
    4.58 +  val is_built_in_const :
    4.59 +    theory -> (typ option * bool) list -> bool -> styp -> bool
    4.60    val term_under_def : term -> term
    4.61 -  val case_const_names : theory -> (string * int) list
    4.62 +  val case_const_names :
    4.63 +    theory -> (typ option * bool) list -> (string * int) list
    4.64    val const_def_table : Proof.context -> term list -> const_table
    4.65    val const_nondef_table : term list -> const_table
    4.66    val const_simp_table : Proof.context -> const_table
    4.67 @@ -165,7 +170,8 @@
    4.68    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
    4.69    val inverse_axioms_for_rep_fun : theory -> styp -> term list
    4.70    val optimized_typedef_axioms : theory -> string * typ list -> term list
    4.71 -  val optimized_quot_type_axioms : theory -> string * typ list -> term list
    4.72 +  val optimized_quot_type_axioms :
    4.73 +    theory -> (typ option * bool) list -> string * typ list -> term list
    4.74    val def_of_const : theory -> const_table -> styp -> term option
    4.75    val fixpoint_kind_of_const :
    4.76      theory -> const_table -> string * typ -> fixpoint_kind
    4.77 @@ -340,44 +346,45 @@
    4.78     (@{const_name trancl}, 1),
    4.79     (@{const_name rel_comp}, 2),
    4.80     (@{const_name image}, 2),
    4.81 -   (@{const_name Suc}, 0),
    4.82     (@{const_name finite}, 1),
    4.83 -   (@{const_name nat}, 0),
    4.84 -   (@{const_name zero_nat_inst.zero_nat}, 0),
    4.85 -   (@{const_name one_nat_inst.one_nat}, 0),
    4.86 -   (@{const_name plus_nat_inst.plus_nat}, 0),
    4.87 -   (@{const_name minus_nat_inst.minus_nat}, 0),
    4.88 -   (@{const_name times_nat_inst.times_nat}, 0),
    4.89 -   (@{const_name div_nat_inst.div_nat}, 0),
    4.90 -   (@{const_name ord_nat_inst.less_nat}, 2),
    4.91 -   (@{const_name ord_nat_inst.less_eq_nat}, 2),
    4.92 -   (@{const_name nat_gcd}, 0),
    4.93 -   (@{const_name nat_lcm}, 0),
    4.94 -   (@{const_name zero_int_inst.zero_int}, 0),
    4.95 -   (@{const_name one_int_inst.one_int}, 0),
    4.96 -   (@{const_name plus_int_inst.plus_int}, 0),
    4.97 -   (@{const_name minus_int_inst.minus_int}, 0),
    4.98 -   (@{const_name times_int_inst.times_int}, 0),
    4.99 -   (@{const_name div_int_inst.div_int}, 0),
   4.100 -   (@{const_name uminus_int_inst.uminus_int}, 0),
   4.101 -   (@{const_name ord_int_inst.less_int}, 2),
   4.102 -   (@{const_name ord_int_inst.less_eq_int}, 2),
   4.103     (@{const_name unknown}, 0),
   4.104     (@{const_name is_unknown}, 1),
   4.105     (@{const_name Tha}, 1),
   4.106     (@{const_name Frac}, 0),
   4.107     (@{const_name norm_frac}, 0)]
   4.108 +val built_in_nat_consts =
   4.109 +  [(@{const_name Suc}, 0),
   4.110 +   (@{const_name nat}, 0),
   4.111 +   (@{const_name nat_gcd}, 0),
   4.112 +   (@{const_name nat_lcm}, 0)]
   4.113  val built_in_descr_consts =
   4.114    [(@{const_name The}, 1),
   4.115     (@{const_name Eps}, 1)]
   4.116  val built_in_typed_consts =
   4.117 -  [((@{const_name of_nat}, nat_T --> int_T), 0),
   4.118 -   ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
   4.119 +  [((@{const_name zero_class.zero}, int_T), 0),
   4.120 +   ((@{const_name one_class.one}, int_T), 0),
   4.121 +   ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
   4.122 +   ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
   4.123 +   ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
   4.124 +   ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
   4.125 +   ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
   4.126 +   ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
   4.127 +   ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
   4.128 +val built_in_typed_nat_consts =
   4.129 +  [((@{const_name zero_class.zero}, nat_T), 0),
   4.130 +   ((@{const_name one_class.one}, nat_T), 0),
   4.131 +   ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
   4.132 +   ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
   4.133 +   ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
   4.134 +   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
   4.135 +   ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   4.136 +   ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   4.137 +   ((@{const_name of_nat}, nat_T --> int_T), 0)]
   4.138  val built_in_set_consts =
   4.139 -  [(@{const_name semilattice_inf_fun_inst.inf_fun}, 2),
   4.140 -   (@{const_name semilattice_sup_fun_inst.sup_fun}, 2),
   4.141 -   (@{const_name minus_fun_inst.minus_fun}, 2),
   4.142 -   (@{const_name ord_fun_inst.less_eq_fun}, 2)]
   4.143 +  [(@{const_name semilattice_inf_class.inf}, 2),
   4.144 +   (@{const_name semilattice_sup_class.sup}, 2),
   4.145 +   (@{const_name minus_class.minus}, 2),
   4.146 +   (@{const_name ord_class.less_eq}, 2)]
   4.147  
   4.148  (* typ -> typ *)
   4.149  fun unarize_type @{typ "unsigned_bit word"} = nat_T
   4.150 @@ -449,17 +456,19 @@
   4.151    | is_gfp_iterator_type _ = false
   4.152  val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
   4.153  fun is_boolean_type T = (T = prop_T orelse T = bool_T)
   4.154 -val is_integer_type =
   4.155 -  member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
   4.156 +fun is_integer_type T = (T = nat_T orelse T = int_T)
   4.157  fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
   4.158  fun is_word_type (Type (@{type_name word}, _)) = true
   4.159    | is_word_type _ = false
   4.160 +fun is_integer_like_type T =
   4.161 +  is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
   4.162 +  T = @{typ bisim_iterator}
   4.163  val is_record_type = not o null o Record.dest_recTs
   4.164  (* theory -> typ -> bool *)
   4.165  fun is_frac_type thy (Type (s, [])) =
   4.166      not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
   4.167    | is_frac_type _ _ = false
   4.168 -fun is_number_type thy = is_integer_type orf is_frac_type thy
   4.169 +fun is_number_type thy = is_integer_like_type orf is_frac_type thy
   4.170  
   4.171  (* bool -> styp -> typ *)
   4.172  fun iterator_type_for_const gfp (s, T) =
   4.173 @@ -507,13 +516,41 @@
   4.174    | dest_n_tuple_type _ T =
   4.175      raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
   4.176  
   4.177 +type typedef_info =
   4.178 +  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   4.179 +   set_def: thm option, prop_of_Rep: thm, set_name: string,
   4.180 +   Abs_inverse: thm option, Rep_inverse: thm option}
   4.181 +
   4.182 +(* theory -> string -> typedef_info *)
   4.183 +fun typedef_info thy s =
   4.184 +  if is_frac_type thy (Type (s, [])) then
   4.185 +    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   4.186 +          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   4.187 +          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   4.188 +                          |> Logic.varify,
   4.189 +          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   4.190 +  else case Typedef.get_info thy s of
   4.191 +    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
   4.192 +          Rep_inverse, ...} =>
   4.193 +    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
   4.194 +          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   4.195 +          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
   4.196 +          Rep_inverse = SOME Rep_inverse}
   4.197 +  | NONE => NONE
   4.198 +
   4.199 +(* theory -> string -> bool *)
   4.200 +val is_typedef = is_some oo typedef_info
   4.201 +val is_real_datatype = is_some oo Datatype.get_info
   4.202 +(* theory -> (typ option * bool) list -> typ -> bool *)
   4.203 +fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
   4.204 +
   4.205  (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
   4.206     e.g., by adding a field to "Datatype_Aux.info". *)
   4.207 -(* string -> bool *)
   4.208 -val is_basic_datatype =
   4.209 -    member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   4.210 -                   @{type_name nat}, @{type_name int},
   4.211 -                   "Code_Numeral.code_numeral"]
   4.212 +(* theory -> (typ option * bool) list -> string -> bool *)
   4.213 +fun is_basic_datatype thy stds s =
   4.214 +  member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   4.215 +                 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
   4.216 +  (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
   4.217  
   4.218  (* theory -> typ -> typ -> typ -> typ *)
   4.219  fun instantiate_type thy T1 T1' T2 =
   4.220 @@ -544,7 +581,8 @@
   4.221      val (co_s, co_Ts) = dest_Type co_T
   4.222      val _ =
   4.223        if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
   4.224 -         co_s <> "fun" andalso not (is_basic_datatype co_s) then
   4.225 +         co_s <> "fun" andalso
   4.226 +         not (is_basic_datatype thy [(NONE, true)] co_s) then
   4.227          ()
   4.228        else
   4.229          raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   4.230 @@ -554,35 +592,6 @@
   4.231  (* typ -> theory -> theory *)
   4.232  fun unregister_codatatype co_T = register_codatatype co_T "" []
   4.233  
   4.234 -type typedef_info =
   4.235 -  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   4.236 -   set_def: thm option, prop_of_Rep: thm, set_name: string,
   4.237 -   Abs_inverse: thm option, Rep_inverse: thm option}
   4.238 -
   4.239 -(* theory -> string -> typedef_info *)
   4.240 -fun typedef_info thy s =
   4.241 -  if is_frac_type thy (Type (s, [])) then
   4.242 -    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   4.243 -          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   4.244 -          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   4.245 -                          |> Logic.varify,
   4.246 -          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   4.247 -  else case Typedef.get_info thy s of
   4.248 -    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
   4.249 -          Rep_inverse, ...} =>
   4.250 -    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
   4.251 -          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   4.252 -          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
   4.253 -          Rep_inverse = SOME Rep_inverse}
   4.254 -  | NONE => NONE
   4.255 -
   4.256 -(* theory -> string -> bool *)
   4.257 -val is_typedef = is_some oo typedef_info
   4.258 -val is_real_datatype = is_some oo Datatype.get_info
   4.259 -(* hol_context -> typ -> bool *)
   4.260 -fun is_standard_datatype ({thy, stds, ...} : hol_context) =
   4.261 -  the o triple_lookup (type_match thy) stds
   4.262 -
   4.263  (* theory -> typ -> bool *)
   4.264  fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
   4.265    | is_quot_type _ (Type ("FSet.fset", _)) = true
   4.266 @@ -594,7 +603,8 @@
   4.267  fun is_pure_typedef thy (T as Type (s, _)) =
   4.268      is_typedef thy s andalso
   4.269      not (is_real_datatype thy s orelse is_quot_type thy T orelse
   4.270 -         is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
   4.271 +         is_codatatype thy T orelse is_record_type T orelse
   4.272 +         is_integer_like_type T)
   4.273    | is_pure_typedef _ _ = false
   4.274  fun is_univ_typedef thy (Type (s, _)) =
   4.275      (case typedef_info thy s of
   4.276 @@ -607,11 +617,11 @@
   4.277                 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
   4.278       | NONE => false)
   4.279    | is_univ_typedef _ _ = false
   4.280 -fun is_datatype thy (T as Type (s, _)) =
   4.281 +(* theory -> (typ option * bool) list -> typ -> bool *)
   4.282 +fun is_datatype thy stds (T as Type (s, _)) =
   4.283      (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
   4.284 -     is_quot_type thy T) andalso
   4.285 -    not (is_basic_datatype s)
   4.286 -  | is_datatype _ _ = false
   4.287 +     is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
   4.288 +  | is_datatype _ _ _ = false
   4.289  
   4.290  (* theory -> typ -> (string * typ) list * (string * typ) *)
   4.291  fun all_record_fields thy T =
   4.292 @@ -699,15 +709,16 @@
   4.293    let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
   4.294      Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
   4.295      (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
   4.296 -    x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
   4.297      is_coconstr thy x
   4.298    end
   4.299  fun is_stale_constr thy (x as (_, T)) =
   4.300    is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
   4.301    not (is_coconstr thy x)
   4.302 -fun is_constr thy (x as (_, T)) =
   4.303 +(* theory -> (typ option * bool) list -> styp -> bool *)
   4.304 +fun is_constr thy stds (x as (_, T)) =
   4.305    is_constr_like thy x andalso
   4.306 -  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   4.307 +  not (is_basic_datatype thy stds
   4.308 +                         (fst (dest_Type (unarize_type (body_type T))))) andalso
   4.309    not (is_stale_constr thy x)
   4.310  (* string -> bool *)
   4.311  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   4.312 @@ -844,15 +855,16 @@
   4.313    #> List.foldr (s_conj o swap) @{const True}
   4.314  
   4.315  (* typ -> term *)
   4.316 -fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
   4.317 +fun zero_const T = Const (@{const_name zero_class.zero}, T)
   4.318  fun suc_const T = Const (@{const_name Suc}, T --> T)
   4.319  
   4.320 -(* theory -> typ -> styp list *)
   4.321 -fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
   4.322 +(* hol_context -> typ -> styp list *)
   4.323 +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
   4.324 +                              (T as Type (s, Ts)) =
   4.325      (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
   4.326         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
   4.327       | _ =>
   4.328 -       if is_datatype thy T then
   4.329 +       if is_datatype thy stds T then
   4.330           case Datatype.get_info thy s of
   4.331             SOME {index, descr, ...} =>
   4.332             let
   4.333 @@ -883,11 +895,11 @@
   4.334           [])
   4.335    | uncached_datatype_constrs _ _ = []
   4.336  (* hol_context -> typ -> styp list *)
   4.337 -fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
   4.338 +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   4.339    case AList.lookup (op =) (!constr_cache) T of
   4.340      SOME xs => xs
   4.341    | NONE =>
   4.342 -    let val xs = uncached_datatype_constrs thy T in
   4.343 +    let val xs = uncached_datatype_constrs hol_ctxt T in
   4.344        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   4.345      end
   4.346  (* hol_context -> bool -> typ -> styp list *)
   4.347 @@ -930,11 +942,11 @@
   4.348      else betapply (discr_term_for_constr hol_ctxt x, t)
   4.349    | _ => betapply (discr_term_for_constr hol_ctxt x, t)
   4.350  
   4.351 -(* styp -> term -> term *)
   4.352 -fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   4.353 +(* theory -> (typ option * bool) list -> styp -> term -> term *)
   4.354 +fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
   4.355    let val (arg_Ts, dataT) = strip_type T in
   4.356 -    if dataT = nat_T then
   4.357 -      @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
   4.358 +    if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
   4.359 +      @{term "%n::nat. n - 1"}
   4.360      else if is_pair_type dataT then
   4.361        Const (nth_sel_for_constr x n)
   4.362      else
   4.363 @@ -952,24 +964,26 @@
   4.364                       (List.take (arg_Ts, n)) 0
   4.365        in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   4.366    end
   4.367 -(* theory -> styp -> term -> int -> typ -> term *)
   4.368 -fun select_nth_constr_arg thy x t n res_T =
   4.369 -  case strip_comb t of
   4.370 -    (Const x', args) =>
   4.371 -    if x = x' then nth args n
   4.372 -    else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
   4.373 -    else betapply (nth_arg_sel_term_for_constr x n, t)
   4.374 -  | _ => betapply (nth_arg_sel_term_for_constr x n, t)
   4.375 +(* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
   4.376 +fun select_nth_constr_arg thy stds x t n res_T =
   4.377 +  (case strip_comb t of
   4.378 +     (Const x', args) =>
   4.379 +     if x = x' then nth args n
   4.380 +     else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
   4.381 +     else raise SAME ()
   4.382 +   | _ => raise SAME())
   4.383 +  handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
   4.384  
   4.385 -(* theory -> styp -> term list -> term *)
   4.386 -fun construct_value _ x [] = Const x
   4.387 -  | construct_value thy (x as (s, _)) args =
   4.388 +(* theory -> (typ option * bool) list -> styp -> term list -> term *)
   4.389 +fun construct_value _ _ x [] = Const x
   4.390 +  | construct_value thy stds (x as (s, _)) args =
   4.391      let val args = map Envir.eta_contract args in
   4.392        case hd args of
   4.393          Const (x' as (s', _)) $ t =>
   4.394          if is_sel_like_and_no_discr s' andalso
   4.395             constr_name_for_sel_like s' = s andalso
   4.396 -           forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
   4.397 +           forall (fn (n, t') =>
   4.398 +                      select_nth_constr_arg thy stds x t n dummyT = t')
   4.399                    (index_seq 0 (length args) ~~ args) then
   4.400            t
   4.401          else
   4.402 @@ -1167,24 +1181,31 @@
   4.403        user_defs @ built_in_defs
   4.404    in (defs, built_in_nondefs, user_nondefs) end
   4.405  
   4.406 -(* bool -> styp -> int option *)
   4.407 -fun arity_of_built_in_const fast_descrs (s, T) =
   4.408 +(* theory -> (typ option * bool) list -> bool -> styp -> int option *)
   4.409 +fun arity_of_built_in_const thy stds fast_descrs (s, T) =
   4.410    if s = @{const_name If} then
   4.411      if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
   4.412 -  else case AList.lookup (op =)
   4.413 -                (built_in_consts
   4.414 -                 |> fast_descrs ? append built_in_descr_consts) s of
   4.415 -    SOME n => SOME n
   4.416 -  | NONE =>
   4.417 -    case AList.lookup (op =) built_in_typed_consts (s, T) of
   4.418 -      SOME n => SOME n
   4.419 -    | NONE =>
   4.420 -      if is_fun_type T andalso is_set_type (domain_type T) then
   4.421 -        AList.lookup (op =) built_in_set_consts s
   4.422 -      else
   4.423 -        NONE
   4.424 -(* bool -> styp -> bool *)
   4.425 -val is_built_in_const = is_some oo arity_of_built_in_const
   4.426 +  else
   4.427 +    let val std_nats = is_standard_datatype thy stds nat_T in
   4.428 +      case AList.lookup (op =)
   4.429 +                    (built_in_consts
   4.430 +                     |> std_nats ? append built_in_nat_consts
   4.431 +                     |> fast_descrs ? append built_in_descr_consts) s of
   4.432 +        SOME n => SOME n
   4.433 +      | NONE =>
   4.434 +        case AList.lookup (op =)
   4.435 +                 (built_in_typed_consts
   4.436 +                  |> std_nats ? append built_in_typed_nat_consts)
   4.437 +                 (s, unarize_type T) of
   4.438 +          SOME n => SOME n
   4.439 +        | NONE =>
   4.440 +          if is_fun_type T andalso is_set_type (domain_type T) then
   4.441 +            AList.lookup (op =) built_in_set_consts s
   4.442 +          else
   4.443 +            NONE
   4.444 +    end
   4.445 +(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
   4.446 +val is_built_in_const = is_some oooo arity_of_built_in_const
   4.447  
   4.448  (* This function is designed to work for both real definition axioms and
   4.449     simplification rules (equational specifications). *)
   4.450 @@ -1202,9 +1223,10 @@
   4.451  (* Here we crucially rely on "Refute.specialize_type" performing a preorder
   4.452     traversal of the term, without which the wrong occurrence of a constant could
   4.453     be matched in the face of overloading. *)
   4.454 -(* theory -> bool -> const_table -> styp -> term list *)
   4.455 -fun def_props_for_const thy fast_descrs table (x as (s, _)) =
   4.456 -  if is_built_in_const fast_descrs x then
   4.457 +(* theory -> (typ option * bool) list -> bool -> const_table -> styp
   4.458 +   -> term list *)
   4.459 +fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
   4.460 +  if is_built_in_const thy stds fast_descrs x then
   4.461      []
   4.462    else
   4.463      these (Symtab.lookup table s)
   4.464 @@ -1229,10 +1251,11 @@
   4.465  
   4.466  (* theory -> const_table -> styp -> term option *)
   4.467  fun def_of_const thy table (x as (s, _)) =
   4.468 -  if is_built_in_const false x orelse original_name s <> s then
   4.469 +  if is_built_in_const thy [(NONE, false)] false x orelse
   4.470 +     original_name s <> s then
   4.471      NONE
   4.472    else
   4.473 -    x |> def_props_for_const thy false table |> List.last
   4.474 +    x |> def_props_for_const thy [(NONE, false)] false table |> List.last
   4.475        |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
   4.476      handle List.Empty => NONE
   4.477  
   4.478 @@ -1282,10 +1305,10 @@
   4.479  fun table_for get ctxt =
   4.480    get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
   4.481  
   4.482 -(* theory -> (string * int) list *)
   4.483 -fun case_const_names thy =
   4.484 +(* theory -> (typ option * bool) list -> (string * int) list *)
   4.485 +fun case_const_names thy stds =
   4.486    Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
   4.487 -                  if is_basic_datatype dtype_s then
   4.488 +                  if is_basic_datatype thy stds dtype_s then
   4.489                      I
   4.490                    else
   4.491                      cons (case_name, AList.lookup (op =) descr index
   4.492 @@ -1366,7 +1389,7 @@
   4.493        end
   4.494      | NONE => []
   4.495    end
   4.496 -fun optimized_quot_type_axioms thy abs_z =
   4.497 +fun optimized_quot_type_axioms thy stds abs_z =
   4.498    let
   4.499      val abs_T = Type abs_z
   4.500      val rep_T = rep_type_for_quot_type thy abs_T
   4.501 @@ -1375,7 +1398,7 @@
   4.502      val x_var = Var (("x", 0), rep_T)
   4.503      val y_var = Var (("y", 0), rep_T)
   4.504      val x = (@{const_name Quot}, rep_T --> abs_T)
   4.505 -    val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
   4.506 +    val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
   4.507      val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
   4.508      val normal_x = normal_t $ x_var
   4.509      val normal_y = normal_t $ y_var
   4.510 @@ -1392,31 +1415,31 @@
   4.511           $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
   4.512    end
   4.513  
   4.514 -(* theory -> int * styp -> term *)
   4.515 -fun constr_case_body thy (j, (x as (_, T))) =
   4.516 +(* theory -> (typ option * bool) list -> int * styp -> term *)
   4.517 +fun constr_case_body thy stds (j, (x as (_, T))) =
   4.518    let val arg_Ts = binder_types T in
   4.519 -    list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
   4.520 +    list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
   4.521                               (index_seq 0 (length arg_Ts)) arg_Ts)
   4.522    end
   4.523  (* hol_context -> typ -> int * styp -> term -> term *)
   4.524 -fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
   4.525 +fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
   4.526    Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   4.527 -  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
   4.528 +  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
   4.529    $ res_t
   4.530  (* hol_context -> typ -> typ -> term *)
   4.531 -fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
   4.532 +fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
   4.533    let
   4.534      val xs = datatype_constrs hol_ctxt dataT
   4.535      val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
   4.536      val (xs', x) = split_last xs
   4.537    in
   4.538 -    constr_case_body thy (1, x)
   4.539 +    constr_case_body thy stds (1, x)
   4.540      |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
   4.541      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   4.542    end
   4.543  
   4.544  (* hol_context -> string -> typ -> typ -> term -> term *)
   4.545 -fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
   4.546 +fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
   4.547    let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   4.548      case no_of_record_field thy s rec_T of
   4.549        ~1 => (case rec_T of
   4.550 @@ -1425,65 +1448,56 @@
   4.551                   val rec_T' = List.last Ts
   4.552                   val j = num_record_fields thy rec_T - 1
   4.553                 in
   4.554 -                 select_nth_constr_arg thy constr_x t j res_T
   4.555 +                 select_nth_constr_arg thy stds constr_x t j res_T
   4.556                   |> optimized_record_get hol_ctxt s rec_T' res_T
   4.557                 end
   4.558               | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
   4.559                                  []))
   4.560 -    | j => select_nth_constr_arg thy constr_x t j res_T
   4.561 +    | j => select_nth_constr_arg thy stds constr_x t j res_T
   4.562    end
   4.563  (* hol_context -> string -> typ -> term -> term -> term *)
   4.564 -fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
   4.565 +fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
   4.566    let
   4.567      val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
   4.568      val Ts = binder_types constr_T
   4.569      val n = length Ts
   4.570      val special_j = no_of_record_field thy s rec_T
   4.571 -    val ts = map2 (fn j => fn T =>
   4.572 -                      let
   4.573 -                        val t = select_nth_constr_arg thy constr_x rec_t j T
   4.574 -                      in
   4.575 -                        if j = special_j then
   4.576 -                          betapply (fun_t, t)
   4.577 -                        else if j = n - 1 andalso special_j = ~1 then
   4.578 -                          optimized_record_update hol_ctxt s
   4.579 -                              (rec_T |> dest_Type |> snd |> List.last) fun_t t
   4.580 -                        else
   4.581 -                          t
   4.582 -                      end) (index_seq 0 n) Ts
   4.583 +    val ts =
   4.584 +      map2 (fn j => fn T =>
   4.585 +               let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
   4.586 +                 if j = special_j then
   4.587 +                   betapply (fun_t, t)
   4.588 +                 else if j = n - 1 andalso special_j = ~1 then
   4.589 +                   optimized_record_update hol_ctxt s
   4.590 +                       (rec_T |> dest_Type |> snd |> List.last) fun_t t
   4.591 +                 else
   4.592 +                   t
   4.593 +               end) (index_seq 0 n) Ts
   4.594    in list_comb (Const constr_x, ts) end
   4.595  
   4.596 -(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
   4.597 -   constant, are said to be trivial. For those, we ignore the simplification
   4.598 -   rules and use the definition instead, to ensure that built-in symbols like
   4.599 -   "ord_nat_inst.less_eq_nat" are picked up correctly. *)
   4.600 -(* theory -> const_table -> styp -> bool *)
   4.601 -fun has_trivial_definition thy table x =
   4.602 -  case def_of_const thy table x of SOME (Const _) => true | _ => false
   4.603 -
   4.604  (* theory -> const_table -> string * typ -> fixpoint_kind *)
   4.605  fun fixpoint_kind_of_const thy table x =
   4.606 -  if is_built_in_const false x then
   4.607 +  if is_built_in_const thy [(NONE, false)] false x then
   4.608      NoFp
   4.609    else
   4.610      fixpoint_kind_of_rhs (the (def_of_const thy table x))
   4.611      handle Option.Option => NoFp
   4.612  
   4.613  (* hol_context -> styp -> bool *)
   4.614 -fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
   4.615 -                            : hol_context) x =
   4.616 -  not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
   4.617 -  fixpoint_kind_of_const thy def_table x <> NoFp
   4.618 -fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
   4.619 -                            : hol_context) x =
   4.620 -  exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
   4.621 +fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
   4.622 +                             ...} : hol_context) x =
   4.623 +  fixpoint_kind_of_const thy def_table x <> NoFp andalso
   4.624 +  not (null (def_props_for_const thy stds fast_descrs intro_table x))
   4.625 +fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
   4.626 +                             ...} : hol_context) x =
   4.627 +  exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
   4.628 +                                                     x)))
   4.629           [!simp_table, psimp_table]
   4.630  fun is_inductive_pred hol_ctxt =
   4.631    is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
   4.632  fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
   4.633    (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
   4.634     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   4.635 -  andf (not o has_trivial_definition thy def_table)
   4.636  
   4.637  (* term * term -> term *)
   4.638  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   4.639 @@ -1522,7 +1536,7 @@
   4.640  val unfold_max_depth = 255
   4.641  
   4.642  (* hol_context -> term -> term *)
   4.643 -fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
   4.644 +fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
   4.645                                        case_names, def_table, ground_thm_table,
   4.646                                        ersatz_table, ...}) =
   4.647    let
   4.648 @@ -1537,8 +1551,11 @@
   4.649                           |> ran_T = nat_T ? Integer.max 0
   4.650                val s = numeral_prefix ^ signed_string_of_int j
   4.651              in
   4.652 -              if is_integer_type ran_T then
   4.653 -                Const (s, ran_T)
   4.654 +              if is_integer_like_type ran_T then
   4.655 +                if is_standard_datatype thy stds ran_T then
   4.656 +                  Const (s, ran_T)
   4.657 +                else
   4.658 +                  funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
   4.659                else
   4.660                  do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
   4.661                                    $ Const (s, int_T))
   4.662 @@ -1577,9 +1594,9 @@
   4.663      (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
   4.664      and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
   4.665          (Abs (Name.uu, body_type T,
   4.666 -              select_nth_constr_arg thy x (Bound 0) n res_T), [])
   4.667 +              select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
   4.668        | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
   4.669 -        (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
   4.670 +        (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
   4.671      (* int -> typ list -> term -> styp -> term list -> term *)
   4.672      and do_const depth Ts t (x as (s, T)) ts =
   4.673        case AList.lookup (op =) ersatz_table s of
   4.674 @@ -1588,7 +1605,7 @@
   4.675        | NONE =>
   4.676          let
   4.677            val (const, ts) =
   4.678 -            if is_built_in_const fast_descrs x then
   4.679 +            if is_built_in_const thy stds fast_descrs x then
   4.680                (Const x, ts)
   4.681              else case AList.lookup (op =) case_names s of
   4.682                SOME n =>
   4.683 @@ -1600,7 +1617,7 @@
   4.684                   |> do_term (depth + 1) Ts, ts)
   4.685                end
   4.686              | _ =>
   4.687 -              if is_constr thy x then
   4.688 +              if is_constr thy stds x then
   4.689                  (Const x, ts)
   4.690                else if is_stale_constr thy x then
   4.691                  raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
   4.692 @@ -1635,7 +1652,7 @@
   4.693                  | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
   4.694                else if is_rep_fun thy x then
   4.695                  let val x' = mate_of_rep_fun thy x in
   4.696 -                  if is_constr thy x' then
   4.697 +                  if is_constr thy stds x' then
   4.698                      select_nth_constr_arg_with_args depth Ts x' ts 0
   4.699                                                      (range_type T)
   4.700                    else
   4.701 @@ -1659,7 +1676,7 @@
   4.702    in do_term 0 [] end
   4.703  
   4.704  (* hol_context -> typ -> term list *)
   4.705 -fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
   4.706 +fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
   4.707    let
   4.708      val xs = datatype_constrs hol_ctxt T
   4.709      val set_T = T --> bool_T
   4.710 @@ -1677,8 +1694,8 @@
   4.711      fun nth_sub_bisim x n nth_T =
   4.712        (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
   4.713         else HOLogic.eq_const nth_T)
   4.714 -      $ select_nth_constr_arg thy x x_var n nth_T
   4.715 -      $ select_nth_constr_arg thy x y_var n nth_T
   4.716 +      $ select_nth_constr_arg thy stds x x_var n nth_T
   4.717 +      $ select_nth_constr_arg thy stds x y_var n nth_T
   4.718      (* styp -> term *)
   4.719      fun case_func (x as (_, T)) =
   4.720        let
   4.721 @@ -1695,7 +1712,7 @@
   4.722                        map case_func xs @ [x_var]))),
   4.723       HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
   4.724       $ (Const (@{const_name insert}, T --> set_T --> set_T)
   4.725 -        $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
   4.726 +        $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
   4.727      |> map HOLogic.mk_Trueprop
   4.728    end
   4.729  
   4.730 @@ -1753,9 +1770,9 @@
   4.731  
   4.732  (* hol_context -> const_table -> styp -> bool *)
   4.733  fun uncached_is_well_founded_inductive_pred
   4.734 -        ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
   4.735 +        ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
   4.736           : hol_context) (x as (_, T)) =
   4.737 -  case def_props_for_const thy fast_descrs intro_table x of
   4.738 +  case def_props_for_const thy stds fast_descrs intro_table x of
   4.739      [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   4.740                        [Const x])
   4.741    | intro_ts =>
   4.742 @@ -1999,10 +2016,10 @@
   4.743      raw_inductive_pred_axiom hol_ctxt x
   4.744  
   4.745  (* hol_context -> styp -> term list *)
   4.746 -fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
   4.747 +fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
   4.748                                              psimp_table, ...}) (x as (s, _)) =
   4.749 -  case def_props_for_const thy fast_descrs (!simp_table) x of
   4.750 -    [] => (case def_props_for_const thy fast_descrs psimp_table x of
   4.751 +  case def_props_for_const thy stds fast_descrs (!simp_table) x of
   4.752 +    [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
   4.753               [] => [inductive_pred_axiom hol_ctxt x]
   4.754             | psimps => psimps)
   4.755    | simps => simps
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 18 10:38:37 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 18 18:48:07 2010 +0100
     5.3 @@ -131,8 +131,7 @@
     5.4    let
     5.5      (* int -> int -> int -> KK.int_bound list *)
     5.6      fun aux 0  _ _ = []
     5.7 -      | aux 1 pow_of_two j =
     5.8 -        if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
     5.9 +      | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
    5.10        | aux iter pow_of_two j =
    5.11          (SOME pow_of_two, [single_atom j]) ::
    5.12          aux (iter - 1) (2 * pow_of_two) (j + 1)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 10:38:37 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 18:48:07 2010 +0100
     6.3 @@ -264,8 +264,8 @@
     6.4     -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
     6.5     -> typ -> rep -> int list list -> term *)
     6.6  fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
     6.7 -        ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
     6.8 -          ofs, ...} : scope) sel_names rel_table bounds =
     6.9 +        ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
    6.10 +          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
    6.11    let
    6.12      val for_auto = (maybe_name = "")
    6.13      (* int list list -> int *)
    6.14 @@ -388,7 +388,7 @@
    6.15          if j = 0 then @{const False} else @{const True}
    6.16        | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
    6.17        | term_for_atom seen T _ j k =
    6.18 -        if T = nat_T then
    6.19 +        if T = nat_T andalso is_standard_datatype thy stds nat_T then
    6.20            HOLogic.mk_number nat_T j
    6.21          else if T = int_T then
    6.22            HOLogic.mk_number int_T (int_for_atom (k, 0) j)
    6.23 @@ -713,7 +713,9 @@
    6.24        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    6.25      val (codatatypes, datatypes) =
    6.26        datatypes |> filter #deep |> List.partition #co
    6.27 -                ||> append (integer_datatype nat_T @ integer_datatype int_T)
    6.28 +                ||> append (integer_datatype int_T
    6.29 +                            |> is_standard_datatype thy stds nat_T
    6.30 +                               ? append (integer_datatype nat_T))
    6.31      val block_of_datatypes =
    6.32        if show_datatypes andalso not (null datatypes) then
    6.33          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 10:38:37 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 18:48:07 2010 +0100
     7.3 @@ -130,7 +130,7 @@
     7.4  fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
     7.5      could_exist_alpha_subtype alpha_T T
     7.6    | could_exist_alpha_sub_ctype thy alpha_T T =
     7.7 -    (T = alpha_T orelse is_datatype thy T)
     7.8 +    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
     7.9  
    7.10  (* ctype -> bool *)
    7.11  fun exists_alpha_sub_ctype CAlpha = true
    7.12 @@ -545,8 +545,9 @@
    7.13    handle List.Empty => initial_gamma
    7.14  
    7.15  (* cdata -> term -> accumulator -> ctype * accumulator *)
    7.16 -fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    7.17 -                             max_fresh, ...}) =
    7.18 +fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
    7.19 +                                          def_table, ...},
    7.20 +                             alpha_T, max_fresh, ...}) =
    7.21    let
    7.22      (* typ -> ctype *)
    7.23      val ctype_for = fresh_ctype_for_type cdata
    7.24 @@ -663,10 +664,6 @@
    7.25                  in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
    7.26                | @{const_name trancl} => do_fragile_set_operation T accum
    7.27                | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
    7.28 -              | @{const_name semilattice_inf_fun_inst.inf_fun} =>
    7.29 -                do_robust_set_operation T accum
    7.30 -              | @{const_name semilattice_sup_fun_inst.sup_fun} =>
    7.31 -                do_robust_set_operation T accum
    7.32                | @{const_name finite} =>
    7.33                  let val C1 = ctype_for (domain_type (domain_type T)) in
    7.34                    (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
    7.35 @@ -710,19 +707,6 @@
    7.36                    (CFun (a_set_C, S Minus,
    7.37                           CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
    7.38                  end
    7.39 -              | @{const_name minus_fun_inst.minus_fun} =>
    7.40 -                let
    7.41 -                  val set_T = domain_type T
    7.42 -                  val left_set_C = ctype_for set_T
    7.43 -                  val right_set_C = ctype_for set_T
    7.44 -                in
    7.45 -                  (CFun (left_set_C, S Minus,
    7.46 -                         CFun (right_set_C, S Minus, left_set_C)),
    7.47 -                   (gamma, cset |> add_ctype_is_right_unique right_set_C
    7.48 -                                |> add_is_sub_ctype right_set_C left_set_C))
    7.49 -                end
    7.50 -              | @{const_name ord_fun_inst.less_eq_fun} =>
    7.51 -                do_fragile_set_operation T accum
    7.52                | @{const_name Tha} =>
    7.53                  let
    7.54                    val a_C = ctype_for (domain_type (domain_type T))
    7.55 @@ -732,24 +716,44 @@
    7.56                  let val dom_C = ctype_for (domain_type T) in
    7.57                    (CFun (dom_C, S Minus, dom_C), accum)
    7.58                  end
    7.59 -              | _ => if is_sel s then
    7.60 -                       if constr_name_for_sel_like s = @{const_name FunBox} then
    7.61 -                         let val dom_C = ctype_for (domain_type T) in
    7.62 -                           (CFun (dom_C, S Minus, dom_C), accum)
    7.63 -                         end
    7.64 -                       else
    7.65 -                         (ctype_for_sel cdata x, accum)
    7.66 -                     else if is_constr thy x then
    7.67 -                       (ctype_for_constr cdata x, accum)
    7.68 -                     else if is_built_in_const true x then
    7.69 -                       case def_of_const thy def_table x of
    7.70 -                         SOME t' => do_term t' accum
    7.71 -                       | NONE => (print_g ("*** built-in " ^ s); unsolvable)
    7.72 -                     else
    7.73 -                       let val C = ctype_for T in
    7.74 -                         (C, ({bounds = bounds, frees = frees,
    7.75 -                               consts = (x, C) :: consts}, cset))
    7.76 -                       end)
    7.77 +              | _ =>
    7.78 +                if s = @{const_name minus_class.minus} andalso
    7.79 +                   is_set_type (domain_type T) then
    7.80 +                  let
    7.81 +                    val set_T = domain_type T
    7.82 +                    val left_set_C = ctype_for set_T
    7.83 +                    val right_set_C = ctype_for set_T
    7.84 +                  in
    7.85 +                    (CFun (left_set_C, S Minus,
    7.86 +                           CFun (right_set_C, S Minus, left_set_C)),
    7.87 +                     (gamma, cset |> add_ctype_is_right_unique right_set_C
    7.88 +                                  |> add_is_sub_ctype right_set_C left_set_C))
    7.89 +                  end
    7.90 +                else if s = @{const_name ord_class.less_eq} andalso
    7.91 +                        is_set_type (domain_type T) then
    7.92 +                  do_fragile_set_operation T accum
    7.93 +                else if (s = @{const_name semilattice_inf_class.inf} orelse
    7.94 +                         s = @{const_name semilattice_sup_class.sup}) andalso
    7.95 +                        is_set_type (domain_type T) then
    7.96 +                  do_robust_set_operation T accum
    7.97 +                else if is_sel s then
    7.98 +                  if constr_name_for_sel_like s = @{const_name FunBox} then
    7.99 +                    let val dom_C = ctype_for (domain_type T) in
   7.100 +                      (CFun (dom_C, S Minus, dom_C), accum)
   7.101 +                    end
   7.102 +                  else
   7.103 +                    (ctype_for_sel cdata x, accum)
   7.104 +                else if is_constr thy stds x then
   7.105 +                  (ctype_for_constr cdata x, accum)
   7.106 +                else if is_built_in_const thy stds fast_descrs x then
   7.107 +                  case def_of_const thy def_table x of
   7.108 +                    SOME t' => do_term t' accum
   7.109 +                  | NONE => (print_g ("*** built-in " ^ s); unsolvable)
   7.110 +                else
   7.111 +                  let val C = ctype_for T in
   7.112 +                    (C, ({bounds = bounds, frees = frees,
   7.113 +                          consts = (x, C) :: consts}, cset))
   7.114 +                  end)
   7.115           | Free (x as (_, T)) =>
   7.116             (case AList.lookup (op =) frees x of
   7.117                SOME C => (C, accum)
   7.118 @@ -881,20 +885,21 @@
   7.119  val bounteous_consts = [@{const_name bisim}]
   7.120  
   7.121  (* term -> bool *)
   7.122 -fun is_harmless_axiom t =
   7.123 -  Term.add_consts t [] |> filter_out (is_built_in_const true)
   7.124 +fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
   7.125 +  Term.add_consts t []
   7.126 +  |> filter_out (is_built_in_const thy stds fast_descrs)
   7.127    |> (forall (member (op =) harmless_consts o original_name o fst)
   7.128        orf exists (member (op =) bounteous_consts o fst))
   7.129  
   7.130  (* cdata -> sign -> term -> accumulator -> accumulator *)
   7.131 -fun consider_nondefinitional_axiom cdata sn t =
   7.132 -  not (is_harmless_axiom t) ? consider_general_formula cdata sn t
   7.133 +fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
   7.134 +  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
   7.135  
   7.136  (* cdata -> term -> accumulator -> accumulator *)
   7.137  fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
   7.138    if not (is_constr_pattern_formula thy t) then
   7.139      consider_nondefinitional_axiom cdata Plus t
   7.140 -  else if is_harmless_axiom t then
   7.141 +  else if is_harmless_axiom hol_ctxt t then
   7.142      I
   7.143    else
   7.144      let
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 18 10:38:37 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 18 18:48:07 2010 +0100
     8.3 @@ -467,7 +467,7 @@
     8.4    | factorize z = [z]
     8.5  
     8.6  (* hol_context -> op2 -> term -> nut *)
     8.7 -fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
     8.8 +fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
     8.9    let
    8.10      (* string list -> typ list -> term -> nut *)
    8.11      fun aux eq ss Ts t =
    8.12 @@ -603,46 +603,62 @@
    8.13               Const (@{const_name top}, _) => Cst (False, bool_T, Any)
    8.14             | _ => Op1 (Finite, bool_T, Any, sub t1))
    8.15          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    8.16 -        | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
    8.17 -          Cst (Num 0, T, Any)
    8.18 -        | (Const (@{const_name one_nat_inst.one_nat}, T), []) =>
    8.19 -          Cst (Num 1, T, Any)
    8.20 -        | (Const (@{const_name plus_nat_inst.plus_nat}, T), []) =>
    8.21 -          Cst (Add, T, Any)
    8.22 -        | (Const (@{const_name minus_nat_inst.minus_nat}, T), []) =>
    8.23 -          Cst (Subtract, T, Any)
    8.24 -        | (Const (@{const_name times_nat_inst.times_nat}, T), []) =>
    8.25 -          Cst (Multiply, T, Any)
    8.26 -        | (Const (@{const_name div_nat_inst.div_nat}, T), []) =>
    8.27 -          Cst (Divide, T, Any)
    8.28 -        | (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) =>
    8.29 -          Op2 (Less, bool_T, Any, sub t1, sub t2)
    8.30 -        | (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) =>
    8.31 -          Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
    8.32 +        | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
    8.33 +          if is_built_in_const thy stds false x then
    8.34 +            Cst (Num 0, T, Any)
    8.35 +          else if is_constr thy stds x then
    8.36 +            let val (s', T') = discr_for_constr x in
    8.37 +              Construct ([ConstName (s', T', Any)], T, Any, [])
    8.38 +            end
    8.39 +          else
    8.40 +            ConstName (s, T, Any)
    8.41 +        | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
    8.42 +          if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
    8.43 +          else ConstName (s, T, Any)
    8.44 +        | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
    8.45 +          if is_built_in_const thy stds false x then Cst (Add, T, Any)
    8.46 +          else ConstName (s, T, Any)
    8.47 +        | (Const (@{const_name minus_class.minus},
    8.48 +                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
    8.49 +           [t1, t2]) =>
    8.50 +          Op2 (SetDifference, T1, Any, sub t1, sub t2)
    8.51 +        | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
    8.52 +          if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
    8.53 +          else ConstName (s, T, Any)
    8.54 +        | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
    8.55 +          if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
    8.56 +          else ConstName (s, T, Any)
    8.57 +        | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
    8.58 +          if is_built_in_const thy stds false x then Cst (Divide, T, Any)
    8.59 +          else ConstName (s, T, Any)
    8.60 +        | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
    8.61 +           ts as [t1, t2]) =>
    8.62 +          if is_built_in_const thy stds false x then
    8.63 +            Op2 (Less, bool_T, Any, sub t1, sub t2)
    8.64 +          else
    8.65 +            do_apply t0 ts
    8.66 +        | (Const (@{const_name ord_class.less_eq},
    8.67 +                  Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
    8.68 +           [t1, t2]) =>
    8.69 +          Op2 (Subset, bool_T, Any, sub t1, sub t2)
    8.70 +        (* FIXME: find out if this case is necessary *)
    8.71 +        | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
    8.72 +           ts as [t1, t2]) =>
    8.73 +          if is_built_in_const thy stds false x then
    8.74 +            Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
    8.75 +          else
    8.76 +            do_apply t0 ts
    8.77          | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
    8.78          | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
    8.79 -        | (Const (@{const_name zero_int_inst.zero_int}, T), []) =>
    8.80 -          Cst (Num 0, T, Any)
    8.81 -        | (Const (@{const_name one_int_inst.one_int}, T), []) =>
    8.82 -          Cst (Num 1, T, Any)
    8.83 -        | (Const (@{const_name plus_int_inst.plus_int}, T), []) =>
    8.84 -          Cst (Add, T, Any)
    8.85 -        | (Const (@{const_name minus_int_inst.minus_int}, T), []) =>
    8.86 -          Cst (Subtract, T, Any)
    8.87 -        | (Const (@{const_name times_int_inst.times_int}, T), []) =>
    8.88 -          Cst (Multiply, T, Any)
    8.89 -        | (Const (@{const_name div_int_inst.div_int}, T), []) =>
    8.90 -          Cst (Divide, T, Any)
    8.91 -        | (Const (@{const_name uminus_int_inst.uminus_int}, T), []) =>
    8.92 -          let val num_T = domain_type T in
    8.93 -            Op2 (Apply, num_T --> num_T, Any,
    8.94 -                 Cst (Subtract, num_T --> num_T --> num_T, Any),
    8.95 -                 Cst (Num 0, num_T, Any))
    8.96 -          end
    8.97 -        | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
    8.98 -          Op2 (Less, bool_T, Any, sub t1, sub t2)
    8.99 -        | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
   8.100 -          Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
   8.101 +        | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
   8.102 +          if is_built_in_const thy stds false x then
   8.103 +            let val num_T = domain_type T in
   8.104 +              Op2 (Apply, num_T --> num_T, Any,
   8.105 +                   Cst (Subtract, num_T --> num_T --> num_T, Any),
   8.106 +                   Cst (Num 0, num_T, Any))
   8.107 +            end
   8.108 +          else
   8.109 +            ConstName (s, T, Any)
   8.110          | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
   8.111          | (Const (@{const_name is_unknown}, T), [t1]) =>
   8.112            Op1 (IsUnknown, bool_T, Any, sub t1)
   8.113 @@ -655,18 +671,16 @@
   8.114          | (Const (@{const_name of_nat},
   8.115                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
   8.116            Cst (NatToInt, T, Any)
   8.117 -        | (Const (@{const_name semilattice_inf_fun_inst.inf_fun}, T),
   8.118 -                  [t1, t2]) =>
   8.119 -          Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2)
   8.120 -        | (Const (@{const_name semilattice_sup_fun_inst.sup_fun}, T),
   8.121 -                  [t1, t2]) =>
   8.122 -          Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2)
   8.123 -        | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) =>
   8.124 -          Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2)
   8.125 -        | (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) =>
   8.126 -          Op2 (Subset, bool_T, Any, sub t1, sub t2)
   8.127 +        | (Const (@{const_name semilattice_inf_class.inf},
   8.128 +                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
   8.129 +           [t1, t2]) =>
   8.130 +          Op2 (Intersect, T1, Any, sub t1, sub t2)
   8.131 +        | (Const (@{const_name semilattice_sup_class.sup},
   8.132 +                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
   8.133 +           [t1, t2]) =>
   8.134 +          Op2 (Union, T1, Any, sub t1, sub t2)
   8.135          | (t0 as Const (x as (s, T)), ts) =>
   8.136 -          if is_constr thy x then
   8.137 +          if is_constr thy stds x then
   8.138              case num_binder_types T - length ts of
   8.139                0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
   8.140                                      o nth_sel_for_constr x)
   8.141 @@ -678,7 +692,7 @@
   8.142            else if String.isPrefix numeral_prefix s then
   8.143              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   8.144            else
   8.145 -            (case arity_of_built_in_const fast_descrs x of
   8.146 +            (case arity_of_built_in_const thy stds fast_descrs x of
   8.147                 SOME n =>
   8.148                 (case n - length ts of
   8.149                    0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 18 10:38:37 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 18 18:48:07 2010 +0100
     9.3 @@ -43,11 +43,9 @@
     9.4    | may_use_binary_ints _ = true
     9.5  fun should_use_binary_ints (t1 $ t2) =
     9.6      should_use_binary_ints t1 orelse should_use_binary_ints t2
     9.7 -  | should_use_binary_ints (Const (s, _)) =
     9.8 -    member (op =) [@{const_name times_nat_inst.times_nat},
     9.9 -                   @{const_name div_nat_inst.div_nat},
    9.10 -                   @{const_name times_int_inst.times_int},
    9.11 -                   @{const_name div_int_inst.div_int}] s orelse
    9.12 +  | should_use_binary_ints (Const (s, T)) =
    9.13 +    ((s = @{const_name times} orelse s = @{const_name div}) andalso
    9.14 +     is_integer_type (body_type T)) orelse
    9.15      (String.isPrefix numeral_prefix s andalso
    9.16       let val n = the (Int.fromString (unprefix numeral_prefix s)) in
    9.17         n < ~ binary_int_threshold orelse n > binary_int_threshold
    9.18 @@ -65,7 +63,8 @@
    9.19          let val table = aux t2 [] table in aux t1 (t2 :: args) table end
    9.20        | aux (Abs (_, _, t')) _ table = aux t' [] table
    9.21        | aux (t as Const (x as (s, _))) args table =
    9.22 -        if is_built_in_const true x orelse is_constr_like thy x orelse
    9.23 +        if is_built_in_const thy [(NONE, true)] true x orelse
    9.24 +           is_constr_like thy x orelse
    9.25             is_sel s orelse s = @{const_name Sigma} then
    9.26            table
    9.27          else
    9.28 @@ -119,7 +118,7 @@
    9.29  (** Boxing **)
    9.30  
    9.31  (* hol_context -> typ -> term -> term *)
    9.32 -fun constr_expand (hol_ctxt as {thy, ...}) T t =
    9.33 +fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
    9.34    (case head_of t of
    9.35       Const x => if is_constr_like thy x then t else raise SAME ()
    9.36     | _ => raise SAME ())
    9.37 @@ -134,12 +133,13 @@
    9.38                 datatype_constrs hol_ctxt T |> hd
    9.39             val arg_Ts = binder_types T'
    9.40           in
    9.41 -           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
    9.42 +           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
    9.43                                       (index_seq 0 (length arg_Ts)) arg_Ts)
    9.44           end
    9.45  
    9.46  (* hol_context -> bool -> term -> term *)
    9.47 -fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
    9.48 +fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
    9.49 +                             orig_t =
    9.50    let
    9.51      (* typ -> typ *)
    9.52      fun box_relational_operator_type (Type ("fun", Ts)) =
    9.53 @@ -172,8 +172,9 @@
    9.54                       |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
    9.55               |> Envir.eta_contract
    9.56               |> new_s <> "fun"
    9.57 -                ? construct_value thy (@{const_name FunBox},
    9.58 -                                       Type ("fun", new_Ts) --> new_T) o single
    9.59 +                ? construct_value thy stds
    9.60 +                      (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
    9.61 +                      o single
    9.62             | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
    9.63                                 \coerce_term", [t']))
    9.64          | (Type (new_s, new_Ts as [new_T1, new_T2]),
    9.65 @@ -185,12 +186,12 @@
    9.66                if new_s = "fun" then
    9.67                  coerce_term Ts new_T (Type ("fun", old_Ts)) t1
    9.68                else
    9.69 -                construct_value thy
    9.70 +                construct_value thy stds
    9.71                      (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
    9.72 -                     [coerce_term Ts (Type ("fun", new_Ts))
    9.73 -                                  (Type ("fun", old_Ts)) t1]
    9.74 +                    [coerce_term Ts (Type ("fun", new_Ts))
    9.75 +                                 (Type ("fun", old_Ts)) t1]
    9.76              | Const _ $ t1 $ t2 =>
    9.77 -              construct_value thy
    9.78 +              construct_value thy stds
    9.79                    (if new_s = "*" then @{const_name Pair}
    9.80                     else @{const_name PairBox}, new_Ts ---> new_T)
    9.81                    [coerce_term Ts new_T1 old_T1 t1,
    9.82 @@ -302,7 +303,7 @@
    9.83          Const (s, if s = @{const_name converse} orelse
    9.84                       s = @{const_name trancl} then
    9.85                      box_relational_operator_type T
    9.86 -                  else if is_built_in_const fast_descrs x orelse
    9.87 +                  else if is_built_in_const thy stds fast_descrs x orelse
    9.88                            s = @{const_name Sigma} then
    9.89                      T
    9.90                    else if is_constr_like thy x then
    9.91 @@ -325,7 +326,7 @@
    9.92            betapply (if s1 = "fun" then
    9.93                        t1
    9.94                      else
    9.95 -                      select_nth_constr_arg thy
    9.96 +                      select_nth_constr_arg thy stds
    9.97                            (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
    9.98                            (Type ("fun", Ts1)), t2)
    9.99          end
   9.100 @@ -341,7 +342,7 @@
   9.101            betapply (if s1 = "fun" then
   9.102                        t1
   9.103                      else
   9.104 -                      select_nth_constr_arg thy
   9.105 +                      select_nth_constr_arg thy stds
   9.106                            (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
   9.107                            (Type ("fun", Ts1)), t2)
   9.108          end
   9.109 @@ -371,13 +372,14 @@
   9.110        | aux _ = true
   9.111    in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
   9.112  
   9.113 -(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
   9.114 -   -> term * term list *)
   9.115 -fun pull_out_constr_comb thy Ts relax k level t args seen =
   9.116 +(* hol_context -> typ list -> bool -> int -> int -> term -> term list
   9.117 +   -> term list -> term * term list *)
   9.118 +fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
   9.119 +                         args seen =
   9.120    let val t_comb = list_comb (t, args) in
   9.121      case t of
   9.122        Const x =>
   9.123 -      if not relax andalso is_constr thy x andalso
   9.124 +      if not relax andalso is_constr thy stds x andalso
   9.125           not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
   9.126           has_heavy_bounds_or_vars Ts level t_comb andalso
   9.127           not (loose_bvar (t_comb, level)) then
   9.128 @@ -398,8 +400,8 @@
   9.129           (index_seq 0 n) seen
   9.130    end
   9.131  
   9.132 -(* theory -> bool -> term -> term *)
   9.133 -fun pull_out_universal_constrs thy def t =
   9.134 +(* hol_context -> bool -> term -> term *)
   9.135 +fun pull_out_universal_constrs hol_ctxt def t =
   9.136    let
   9.137      val k = maxidx_of_term t + 1
   9.138      (* typ list -> bool -> term -> term list -> term list -> term * term list *)
   9.139 @@ -421,7 +423,7 @@
   9.140          let val (t2, seen) = do_term Ts def t2 [] seen in
   9.141            do_term Ts def t1 (t2 :: args) seen
   9.142          end
   9.143 -      | _ => pull_out_constr_comb thy Ts def k 0 t args seen
   9.144 +      | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
   9.145      (* typ list -> bool -> bool -> term -> term -> term -> term list
   9.146         -> term * term list *)
   9.147      and do_eq_or_imp Ts eq def t0 t1 t2 seen =
   9.148 @@ -440,8 +442,8 @@
   9.149  fun mk_exists v t =
   9.150    HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
   9.151  
   9.152 -(* theory -> term -> term *)
   9.153 -fun pull_out_existential_constrs thy t =
   9.154 +(* hol_context -> term -> term *)
   9.155 +fun pull_out_existential_constrs hol_ctxt t =
   9.156    let
   9.157      val k = maxidx_of_term t + 1
   9.158      (* typ list -> int -> term -> term list -> term list -> term * term list *)
   9.159 @@ -468,13 +470,13 @@
   9.160          in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
   9.161        | _ =>
   9.162          if num_exists > 0 then
   9.163 -          pull_out_constr_comb thy Ts false k num_exists t args seen
   9.164 +          pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen
   9.165          else
   9.166            (list_comb (t, args), seen)
   9.167    in aux [] 0 t [] [] |> fst end
   9.168  
   9.169  (* hol_context -> bool -> term -> term *)
   9.170 -fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
   9.171 +fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
   9.172    let
   9.173      (* styp -> int *)
   9.174      val num_occs_of_var =
   9.175 @@ -509,7 +511,7 @@
   9.176          | (Const (x as (s, T)), args) =>
   9.177            let val arg_Ts = binder_types T in
   9.178              if length arg_Ts = length args andalso
   9.179 -               (is_constr thy x orelse s = @{const_name Pair}) andalso
   9.180 +               (is_constr thy stds x orelse s = @{const_name Pair}) andalso
   9.181                 (not careful orelse not (is_Var t1) orelse
   9.182                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   9.183                discriminate_value hol_ctxt x t1 ::
   9.184 @@ -524,7 +526,8 @@
   9.185                          else t0 $ aux false t2 $ aux false t1
   9.186      (* styp -> term -> int -> typ -> term -> term *)
   9.187      and sel_eq x t n nth_T nth_t =
   9.188 -      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
   9.189 +      HOLogic.eq_const nth_T $ nth_t
   9.190 +                             $ select_nth_constr_arg thy stds x t n nth_T
   9.191        |> aux false
   9.192    in aux axiom t end
   9.193  
   9.194 @@ -565,34 +568,40 @@
   9.195          aux (t1 :: prems) (Term.add_vars t1 zs) t2
   9.196    in aux [] [] end
   9.197  
   9.198 -(* theory -> int -> term list -> term list -> (term * term list) option *)
   9.199 -fun find_bound_assign _ _ _ [] = NONE
   9.200 -  | find_bound_assign thy j seen (t :: ts) =
   9.201 -    let
   9.202 -      (* bool -> term -> term -> (term * term list) option *)
   9.203 -      fun aux pass1 t1 t2 =
   9.204 -        (if loose_bvar1 (t2, j) then
   9.205 -           if pass1 then aux false t2 t1 else raise SAME ()
   9.206 -         else case t1 of
   9.207 -           Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
   9.208 -         | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
   9.209 -           if j' = j andalso
   9.210 -              s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
   9.211 -             SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
   9.212 -                   ts @ seen)
   9.213 -           else
   9.214 -             raise SAME ()
   9.215 -         | _ => raise SAME ())
   9.216 -        handle SAME () => find_bound_assign thy j (t :: seen) ts
   9.217 -    in
   9.218 -      case t of
   9.219 -        Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
   9.220 -      | _ => find_bound_assign thy j (t :: seen) ts
   9.221 -    end
   9.222 +(* theory -> (typ option * bool) list -> int -> term list -> term list
   9.223 +   -> (term * term list) option *)
   9.224 +fun find_bound_assign thy stds j =
   9.225 +  let
   9.226 +    (* term list -> term list -> (term * term list) option *)
   9.227 +    fun do_term _ [] = NONE
   9.228 +      | do_term seen (t :: ts) =
   9.229 +        let
   9.230 +          (* bool -> term -> term -> (term * term list) option *)
   9.231 +          fun do_eq pass1 t1 t2 =
   9.232 +            (if loose_bvar1 (t2, j) then
   9.233 +               if pass1 then do_eq false t2 t1 else raise SAME ()
   9.234 +             else case t1 of
   9.235 +               Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
   9.236 +             | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
   9.237 +               if j' = j andalso
   9.238 +                  s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
   9.239 +                 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
   9.240 +                                       [t2], ts @ seen)
   9.241 +               else
   9.242 +                 raise SAME ()
   9.243 +             | _ => raise SAME ())
   9.244 +            handle SAME () => do_term (t :: seen) ts
   9.245 +        in
   9.246 +          case t of
   9.247 +            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
   9.248 +          | _ => do_term (t :: seen) ts
   9.249 +        end
   9.250 +  in do_term end
   9.251  
   9.252  (* int -> term -> term -> term *)
   9.253  fun subst_one_bound j arg t =
   9.254    let
   9.255 +    (* term * int -> term *)
   9.256      fun aux (Bound i, lev) =
   9.257          if i < lev then raise SAME ()
   9.258          else if i = lev then incr_boundvars (lev - j) arg
   9.259 @@ -604,13 +613,13 @@
   9.260        | aux _ = raise SAME ()
   9.261    in aux (t, j) handle SAME () => t end
   9.262  
   9.263 -(* theory -> term -> term *)
   9.264 -fun destroy_existential_equalities thy =
   9.265 +(* hol_context -> term -> term *)
   9.266 +fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
   9.267    let
   9.268      (* string list -> typ list -> term list -> term *)
   9.269      fun kill [] [] ts = foldr1 s_conj ts
   9.270        | kill (s :: ss) (T :: Ts) ts =
   9.271 -        (case find_bound_assign thy (length ss) [] ts of
   9.272 +        (case find_bound_assign thy stds (length ss) [] ts of
   9.273             SOME (_, []) => @{const True}
   9.274           | SOME (arg_t, ts) =>
   9.275             kill ss Ts (map (subst_one_bound (length ss)
   9.276 @@ -704,13 +713,11 @@
   9.277                val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   9.278                val (pref, connective, set_oper) =
   9.279                  if gfp then
   9.280 -                  (lbfp_prefix,
   9.281 -                   @{const "op |"},
   9.282 -                   @{const_name semilattice_sup_fun_inst.sup_fun})
   9.283 +                  (lbfp_prefix, @{const "op |"},
   9.284 +                   @{const_name semilattice_sup_class.sup})
   9.285                  else
   9.286 -                  (ubfp_prefix,
   9.287 -                   @{const "op &"},
   9.288 -                   @{const_name semilattice_inf_fun_inst.inf_fun})
   9.289 +                  (ubfp_prefix, @{const "op &"},
   9.290 +                   @{const_name semilattice_inf_class.inf})
   9.291                (* unit -> term *)
   9.292                fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
   9.293                             |> aux ss Ts js depth polar
   9.294 @@ -854,7 +861,7 @@
   9.295                                             (index_seq 0 (length args) ~~ args)
   9.296                  val _ = not (null eligible_args) orelse raise SAME ()
   9.297                  val old_axs = equational_fun_axioms hol_ctxt x
   9.298 -                              |> map (destroy_existential_equalities thy)
   9.299 +                              |> map (destroy_existential_equalities hol_ctxt)
   9.300                  val static_params = static_args_in_terms hol_ctxt x old_axs
   9.301                  val fixed_js = overlapping_indices static_params eligible_args
   9.302                  val _ = not (null fixed_js) orelse raise SAME ()
   9.303 @@ -1016,8 +1023,8 @@
   9.304  
   9.305  (* hol_context -> term -> (term list * term list) * (bool * bool) *)
   9.306  fun axioms_for_term
   9.307 -        (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
   9.308 -                      def_table, nondef_table, user_nondefs, ...}) t =
   9.309 +        (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
   9.310 +                      evals, def_table, nondef_table, user_nondefs, ...}) t =
   9.311    let
   9.312      type accumulator = styp list * (term list * term list)
   9.313      (* (term list * term list -> term list)
   9.314 @@ -1051,7 +1058,8 @@
   9.315        case t of
   9.316          t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
   9.317        | Const (x as (s, T)) =>
   9.318 -        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
   9.319 +        (if member (op =) xs x orelse
   9.320 +            is_built_in_const thy stds fast_descrs x then
   9.321             accum
   9.322           else
   9.323             let val accum as (xs, _) = (x :: xs, axs) in
   9.324 @@ -1072,7 +1080,7 @@
   9.325                   fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
   9.326                        accum
   9.327                 end
   9.328 -             else if is_constr thy x then
   9.329 +             else if is_constr thy stds x then
   9.330                 accum
   9.331               else if is_equational_fun hol_ctxt x then
   9.332                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
   9.333 @@ -1127,7 +1135,7 @@
   9.334          #> (if is_pure_typedef thy T then
   9.335                fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
   9.336              else if is_quot_type thy T then
   9.337 -              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
   9.338 +              fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
   9.339              else if max_bisim_depth >= 0 andalso is_codatatype thy T then
   9.340                fold (add_maybe_def_axiom depth)
   9.341                     (codatatype_bisim_axioms hol_ctxt T)
   9.342 @@ -1377,8 +1385,8 @@
   9.343  
   9.344  (* hol_context -> term
   9.345     -> ((term list * term list) * (bool * bool)) * term * bool *)
   9.346 -fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
   9.347 -                                  skolemize, uncurry, ...}) t =
   9.348 +fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
   9.349 +                                  boxes, skolemize, uncurry, ...}) t =
   9.350    let
   9.351      val skolem_depth = if skolemize then 4 else ~1
   9.352      val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
   9.353 @@ -1388,12 +1396,12 @@
   9.354                       |> specialize_consts_in_term hol_ctxt 0
   9.355                       |> `(axioms_for_term hol_ctxt)
   9.356      val binarize =
   9.357 +      is_standard_datatype thy stds nat_T andalso
   9.358        case binary_ints of
   9.359          SOME false => false
   9.360 -      | _ =>
   9.361 -        forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
   9.362 -        (binary_ints = SOME true orelse
   9.363 -         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
   9.364 +      | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
   9.365 +             (binary_ints = SOME true orelse
   9.366 +              exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
   9.367      val box = exists (not_equal (SOME false) o snd) boxes
   9.368      val table =
   9.369        Termtab.empty |> uncurry
   9.370 @@ -1403,12 +1411,12 @@
   9.371        binarize ? binarize_nat_and_int_in_term
   9.372        #> uncurry ? uncurry_term table
   9.373        #> box ? box_fun_and_pair_in_term hol_ctxt def
   9.374 -      #> destroy_constrs ? (pull_out_universal_constrs thy def
   9.375 -                            #> pull_out_existential_constrs thy
   9.376 +      #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
   9.377 +                            #> pull_out_existential_constrs hol_ctxt
   9.378                              #> destroy_pulled_out_constrs hol_ctxt def)
   9.379        #> curry_assms
   9.380        #> destroy_universal_equalities
   9.381 -      #> destroy_existential_equalities thy
   9.382 +      #> destroy_existential_equalities hol_ctxt
   9.383        #> simplify_constrs_and_sels thy
   9.384        #> distribute_quantifiers
   9.385        #> push_quantifiers_inward thy
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 18 10:38:37 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 18 18:48:07 2010 +0100
    10.3 @@ -111,7 +111,7 @@
    10.4    | is_complete_type dtypes (Type ("*", Ts)) =
    10.5      forall (is_complete_type dtypes) Ts
    10.6    | is_complete_type dtypes T =
    10.7 -    not (is_integer_type T) andalso not (is_bit_type T) andalso
    10.8 +    not (is_integer_like_type T) andalso not (is_bit_type T) andalso
    10.9      #complete (the (datatype_spec dtypes T))
   10.10      handle Option.Option => true
   10.11  and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
   10.12 @@ -135,8 +135,9 @@
   10.13  
   10.14  (* (string -> string) -> scope
   10.15     -> string list * string list * string list * string list * string list *)
   10.16 -fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
   10.17 -                                bits, bisim_depth, datatypes, ...} : scope) =
   10.18 +fun quintuple_for_scope quote
   10.19 +        ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
   10.20 +         datatypes, ...} : scope) =
   10.21    let
   10.22      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
   10.23                       @{typ bisim_iterator}]
   10.24 @@ -144,7 +145,7 @@
   10.25        card_assigns |> filter_out (member (op =) boring_Ts o fst)
   10.26                     |> List.partition (is_fp_iterator_type o fst)
   10.27      val (secondary_card_assigns, primary_card_assigns) =
   10.28 -      card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
   10.29 +      card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
   10.30                                        o fst)
   10.31      val cards =
   10.32        map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
   10.33 @@ -400,7 +401,8 @@
   10.34         -> int Typtab.table *)
   10.35      fun aux next _ [] = Typtab.update_new (dummyT, next)
   10.36        | aux next reusable ((T, k) :: assigns) =
   10.37 -        if k = 1 orelse is_integer_type T orelse is_bit_type T then
   10.38 +        if k = 1 orelse is_fp_iterator_type T orelse is_integer_type T
   10.39 +           orelse T = @{typ bisim_iterator} orelse is_bit_type T then
   10.40            aux next reusable assigns
   10.41          else if length (these (Option.map #constrs (datatype_spec dtypes T)))
   10.42                  > 1 then
   10.43 @@ -468,19 +470,20 @@
   10.44    end
   10.45  
   10.46  (* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   10.47 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
   10.48 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
   10.49          deep_dataTs (desc as (card_assigns, _)) (T, card) =
   10.50    let
   10.51      val deep = member (op =) deep_dataTs T
   10.52      val co = is_codatatype thy T
   10.53 -    val standard = is_standard_datatype hol_ctxt T
   10.54 +    val standard = is_standard_datatype thy stds T
   10.55      val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   10.56      val self_recs = map (is_self_recursive_constr_type o snd) xs
   10.57      val (num_self_recs, num_non_self_recs) =
   10.58        List.partition I self_recs |> pairself length
   10.59      val complete = has_exact_card hol_ctxt card_assigns T
   10.60 -    val concrete = xs |> maps (binder_types o snd) |> maps binder_types
   10.61 -                      |> forall (has_exact_card hol_ctxt card_assigns)
   10.62 +    val concrete = is_word_type T orelse
   10.63 +                   (xs |> maps (binder_types o snd) |> maps binder_types
   10.64 +                       |> forall (has_exact_card hol_ctxt card_assigns))
   10.65      (* int -> int *)
   10.66      fun sum_dom_cards max =
   10.67        map (domain_card max card_assigns o snd) xs |> Integer.sum
   10.68 @@ -502,12 +505,12 @@
   10.69          (map snd card_assigns @ map snd max_assigns) 0)
   10.70  
   10.71  (* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
   10.72 -fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
   10.73 +fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
   10.74                            deep_dataTs (desc as (card_assigns, _)) =
   10.75    let
   10.76      val datatypes =
   10.77        map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   10.78 -               desc) (filter (is_datatype thy o fst) card_assigns)
   10.79 +               desc) (filter (is_datatype thy stds o fst) card_assigns)
   10.80      val bits = card_of_type card_assigns @{typ signed_bit} - 1
   10.81                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   10.82                        card_of_type card_assigns @{typ unsigned_bit}
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 18 10:38:37 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 18 18:48:07 2010 +0100
    11.3 @@ -215,10 +215,11 @@
    11.4      SOME z => SOME z
    11.5    | NONE => ps |> find_first (is_none o fst) |> Option.map snd
    11.6  (* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
    11.7 -fun triple_lookup eq ps key =
    11.8 -  case AList.lookup (op =) ps (SOME key) of
    11.9 -    SOME z => SOME z
   11.10 -  | NONE => double_lookup eq ps key
   11.11 +fun triple_lookup _ [(NONE, z)] _ = SOME z
   11.12 +  | triple_lookup eq ps key =
   11.13 +    case AList.lookup (op =) ps (SOME key) of
   11.14 +      SOME z => SOME z
   11.15 +    | NONE => double_lookup eq ps key
   11.16  
   11.17  (* string -> string -> bool *)
   11.18  fun is_substring_of needle stack =