src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33583 b5e0909cd5ea
parent 33522 737589bb9bb8
parent 33581 e1e77265fb1d
child 33699 f33b036ef318
child 33705 947184dc75c9
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 10 13:17:50 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 10 13:54:00 2009 +0100
     1.3 @@ -40,7 +40,8 @@
     1.4      skolems: (string * string list) list Unsynchronized.ref,
     1.5      special_funs: special_fun list Unsynchronized.ref,
     1.6      unrolled_preds: unrolled list Unsynchronized.ref,
     1.7 -    wf_cache: wf_cache Unsynchronized.ref}
     1.8 +    wf_cache: wf_cache Unsynchronized.ref,
     1.9 +    constr_cache: (typ * styp list) list Unsynchronized.ref}
    1.10  
    1.11    val name_sep : string
    1.12    val numeral_prefix : string
    1.13 @@ -86,6 +87,7 @@
    1.14    val is_abs_fun : theory -> styp -> bool
    1.15    val is_rep_fun : theory -> styp -> bool
    1.16    val is_constr : theory -> styp -> bool
    1.17 +  val is_stale_constr : theory -> styp -> bool
    1.18    val is_sel : string -> bool
    1.19    val discr_for_constr : styp -> styp
    1.20    val num_sels_for_constr_type : typ -> int
    1.21 @@ -100,16 +102,16 @@
    1.22    val unregister_frac_type : string -> theory -> theory
    1.23    val register_codatatype : typ -> string -> styp list -> theory -> theory
    1.24    val unregister_codatatype : typ -> theory -> theory
    1.25 -  val datatype_constrs : theory -> typ -> styp list
    1.26 +  val datatype_constrs : extended_context -> typ -> styp list
    1.27    val boxed_datatype_constrs : extended_context -> typ -> styp list
    1.28 -  val num_datatype_constrs : theory -> typ -> int
    1.29 +  val num_datatype_constrs : extended_context -> typ -> int
    1.30    val constr_name_for_sel_like : string -> string
    1.31    val boxed_constr_for_sel : extended_context -> styp -> styp
    1.32    val card_of_type : (typ * int) list -> typ -> int
    1.33    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    1.34    val bounded_precise_card_of_type :
    1.35 -    theory -> int -> int -> (typ * int) list -> typ -> int
    1.36 -  val is_finite_type : theory -> typ -> bool
    1.37 +    extended_context -> int -> int -> (typ * int) list -> typ -> int
    1.38 +  val is_finite_type : extended_context -> typ -> bool
    1.39    val all_axioms_of : theory -> term list * term list * term list
    1.40    val arity_of_built_in_const : bool -> styp -> int option
    1.41    val is_built_in_const : bool -> styp -> bool
    1.42 @@ -125,7 +127,7 @@
    1.43    val is_inductive_pred : extended_context -> styp -> bool
    1.44    val is_constr_pattern_lhs : theory -> term -> bool
    1.45    val is_constr_pattern_formula : theory -> term -> bool
    1.46 -  val coalesce_type_vars_in_terms : term list -> term list
    1.47 +  val merge_type_vars_in_terms : term list -> term list
    1.48    val ground_types_in_type : extended_context -> typ -> typ list
    1.49    val ground_types_in_terms : extended_context -> term list -> typ list
    1.50    val format_type : int list -> int list -> typ -> typ
    1.51 @@ -177,9 +179,10 @@
    1.52    skolems: (string * string list) list Unsynchronized.ref,
    1.53    special_funs: special_fun list Unsynchronized.ref,
    1.54    unrolled_preds: unrolled list Unsynchronized.ref,
    1.55 -  wf_cache: wf_cache Unsynchronized.ref}
    1.56 +  wf_cache: wf_cache Unsynchronized.ref,
    1.57 +  constr_cache: (typ * styp list) list Unsynchronized.ref}
    1.58  
    1.59 -structure TheoryData = Theory_Data(
    1.60 +structure Data = Theory_Data(
    1.61    type T = {frac_types: (string * (string * string) list) list,
    1.62              codatatypes: (string * (string * styp list)) list}
    1.63    val empty = {frac_types = [], codatatypes = []}
    1.64 @@ -312,7 +315,7 @@
    1.65     (@{const_name times_int_inst.times_int}, 0),
    1.66     (@{const_name div_int_inst.div_int}, 0),
    1.67     (@{const_name div_int_inst.mod_int}, 0),
    1.68 -   (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
    1.69 +   (@{const_name uminus_int_inst.uminus_int}, 0),
    1.70     (@{const_name ord_int_inst.less_int}, 2),
    1.71     (@{const_name ord_int_inst.less_eq_int}, 2),
    1.72     (@{const_name Tha}, 1),
    1.73 @@ -392,8 +395,7 @@
    1.74  val is_record_type = not o null o Record.dest_recTs
    1.75  (* theory -> typ -> bool *)
    1.76  fun is_frac_type thy (Type (s, [])) =
    1.77 -    not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy))
    1.78 -                                          s)))
    1.79 +    not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
    1.80    | is_frac_type _ _ = false
    1.81  fun is_number_type thy = is_integer_type orf is_frac_type thy
    1.82  
    1.83 @@ -469,16 +471,16 @@
    1.84  (* string -> (string * string) list -> theory -> theory *)
    1.85  fun register_frac_type frac_s ersaetze thy =
    1.86    let
    1.87 -    val {frac_types, codatatypes} = TheoryData.get thy
    1.88 +    val {frac_types, codatatypes} = Data.get thy
    1.89      val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
    1.90 -  in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
    1.91 +  in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
    1.92  (* string -> theory -> theory *)
    1.93  fun unregister_frac_type frac_s = register_frac_type frac_s []
    1.94  
    1.95  (* typ -> string -> styp list -> theory -> theory *)
    1.96  fun register_codatatype co_T case_name constr_xs thy =
    1.97    let
    1.98 -    val {frac_types, codatatypes} = TheoryData.get thy
    1.99 +    val {frac_types, codatatypes} = Data.get thy
   1.100      val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
   1.101      val (co_s, co_Ts) = dest_Type co_T
   1.102      val _ =
   1.103 @@ -486,7 +488,7 @@
   1.104        else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   1.105      val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
   1.106                                     codatatypes
   1.107 -  in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   1.108 +  in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   1.109  (* typ -> theory -> theory *)
   1.110  fun unregister_codatatype co_T = register_codatatype co_T "" []
   1.111  
   1.112 @@ -520,7 +522,7 @@
   1.113  val is_real_datatype = is_some oo Datatype.get_info
   1.114  (* theory -> typ -> bool *)
   1.115  fun is_codatatype thy (T as Type (s, _)) =
   1.116 -    not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s
   1.117 +    not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
   1.118                 |> Option.map snd |> these))
   1.119    | is_codatatype _ _ = false
   1.120  fun is_pure_typedef thy (T as Type (s, _)) =
   1.121 @@ -592,7 +594,7 @@
   1.122  (* theory -> styp -> bool *)
   1.123  fun is_coconstr thy (s, T) =
   1.124    let
   1.125 -    val {codatatypes, ...} = TheoryData.get thy
   1.126 +    val {codatatypes, ...} = Data.get thy
   1.127      val co_T = body_type T
   1.128      val co_s = dest_Type co_T |> fst
   1.129    in
   1.130 @@ -609,9 +611,13 @@
   1.131      orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
   1.132      orelse is_coconstr thy x
   1.133    end
   1.134 +fun is_stale_constr thy (x as (_, T)) =
   1.135 +  is_codatatype thy (body_type T) andalso is_constr_like thy x
   1.136 +  andalso not (is_coconstr thy x)
   1.137  fun is_constr thy (x as (_, T)) =
   1.138    is_constr_like thy x
   1.139    andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
   1.140 +  andalso not (is_stale_constr thy x)
   1.141  (* string -> bool *)
   1.142  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   1.143  val is_sel_like_and_no_discr =
   1.144 @@ -726,41 +732,51 @@
   1.145  fun suc_const T = Const (@{const_name Suc}, T --> T)
   1.146  
   1.147  (* theory -> typ -> styp list *)
   1.148 -fun datatype_constrs thy (T as Type (s, Ts)) =
   1.149 -    if is_datatype thy T then
   1.150 -      case Datatype.get_info thy s of
   1.151 -        SOME {index, descr, ...} =>
   1.152 -        let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
   1.153 -          map (fn (s', Us) =>
   1.154 -                  (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   1.155 -              constrs
   1.156 -         end
   1.157 -      | NONE =>
   1.158 -        case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
   1.159 -          SOME (_, xs' as (_ :: _)) =>
   1.160 -          map (apsnd (repair_constr_type thy T)) xs'
   1.161 -        | _ =>
   1.162 -          if is_record_type T then
   1.163 -            let
   1.164 -              val s' = unsuffix Record.ext_typeN s ^ Record.extN
   1.165 -              val T' = (Record.get_extT_fields thy T
   1.166 -                       |> apsnd single |> uncurry append |> map snd) ---> T
   1.167 -            in [(s', T')] end
   1.168 -          else case typedef_info thy s of
   1.169 -            SOME {abs_type, rep_type, Abs_name, ...} =>
   1.170 -            [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
   1.171 -          | NONE =>
   1.172 -            if T = @{typ ind} then
   1.173 -              [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   1.174 -            else
   1.175 -              []
   1.176 -    else
   1.177 -      []
   1.178 -  | datatype_constrs _ _ = []
   1.179 +fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
   1.180 +    (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
   1.181 +       SOME (_, xs' as (_ :: _)) =>
   1.182 +       map (apsnd (repair_constr_type thy T)) xs'
   1.183 +     | _ =>
   1.184 +       if is_datatype thy T then
   1.185 +         case Datatype.get_info thy s of
   1.186 +           SOME {index, descr, ...} =>
   1.187 +           let
   1.188 +             val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   1.189 +           in
   1.190 +             map (fn (s', Us) =>
   1.191 +                     (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
   1.192 +                          ---> T)) constrs
   1.193 +           end
   1.194 +         | NONE =>
   1.195 +           if is_record_type T then
   1.196 +             let
   1.197 +               val s' = unsuffix Record.ext_typeN s ^ Record.extN
   1.198 +               val T' = (Record.get_extT_fields thy T
   1.199 +                        |> apsnd single |> uncurry append |> map snd) ---> T
   1.200 +             in [(s', T')] end
   1.201 +           else case typedef_info thy s of
   1.202 +             SOME {abs_type, rep_type, Abs_name, ...} =>
   1.203 +             [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
   1.204 +           | NONE =>
   1.205 +             if T = @{typ ind} then
   1.206 +               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   1.207 +             else
   1.208 +               []
   1.209 +       else
   1.210 +         [])
   1.211 +  | uncached_datatype_constrs _ _ = []
   1.212  (* extended_context -> typ -> styp list *)
   1.213 -fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) =
   1.214 -  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy
   1.215 -(* theory -> typ -> int *)
   1.216 +fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
   1.217 +                     T =
   1.218 +  case AList.lookup (op =) (!constr_cache) T of
   1.219 +    SOME xs => xs
   1.220 +  | NONE =>
   1.221 +    let val xs = uncached_datatype_constrs thy T in
   1.222 +      (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   1.223 +    end
   1.224 +fun boxed_datatype_constrs ext_ctxt =
   1.225 +  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
   1.226 +(* extended_context -> typ -> int *)
   1.227  val num_datatype_constrs = length oo datatype_constrs
   1.228  
   1.229  (* string -> string *)
   1.230 @@ -773,26 +789,26 @@
   1.231      AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
   1.232      |> the |> pair s
   1.233    end
   1.234 -(* theory -> styp -> term *)
   1.235 -fun discr_term_for_constr thy (x as (s, T)) =
   1.236 +(* extended_context -> styp -> term *)
   1.237 +fun discr_term_for_constr ext_ctxt (x as (s, T)) =
   1.238    let val dataT = body_type T in
   1.239      if s = @{const_name Suc} then
   1.240        Abs (Name.uu, dataT,
   1.241             @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
   1.242 -    else if num_datatype_constrs thy dataT >= 2 then
   1.243 +    else if num_datatype_constrs ext_ctxt dataT >= 2 then
   1.244        Const (discr_for_constr x)
   1.245      else
   1.246        Abs (Name.uu, dataT, @{const True})
   1.247    end
   1.248  
   1.249 -(* theory -> styp -> term -> term *)
   1.250 -fun discriminate_value thy (x as (_, T)) t =
   1.251 +(* extended_context -> styp -> term -> term *)
   1.252 +fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
   1.253    case strip_comb t of
   1.254      (Const x', args) =>
   1.255      if x = x' then @{const True}
   1.256      else if is_constr_like thy x' then @{const False}
   1.257 -    else betapply (discr_term_for_constr thy x, t)
   1.258 -  | _ => betapply (discr_term_for_constr thy x, t)
   1.259 +    else betapply (discr_term_for_constr ext_ctxt x, t)
   1.260 +  | _ => betapply (discr_term_for_constr ext_ctxt x, t)
   1.261  
   1.262  (* styp -> term -> term *)
   1.263  fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   1.264 @@ -841,8 +857,8 @@
   1.265        | _ => list_comb (Const x, args)
   1.266      end
   1.267  
   1.268 -(* theory -> typ -> term -> term *)
   1.269 -fun constr_expand thy T t =
   1.270 +(* extended_context -> typ -> term -> term *)
   1.271 +fun constr_expand (ext_ctxt as {thy, ...}) T t =
   1.272    (case head_of t of
   1.273       Const x => if is_constr_like thy x then t else raise SAME ()
   1.274     | _ => raise SAME ())
   1.275 @@ -854,7 +870,7 @@
   1.276                   (@{const_name Pair}, [T1, T2] ---> T)
   1.277                 end
   1.278               else
   1.279 -               datatype_constrs thy T |> the_single
   1.280 +               datatype_constrs ext_ctxt T |> the_single
   1.281             val arg_Ts = binder_types T'
   1.282           in
   1.283             list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
   1.284 @@ -896,8 +912,8 @@
   1.285                      card_of_type asgns T
   1.286                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   1.287                             default_card)
   1.288 -(* theory -> int -> (typ * int) list -> typ -> int *)
   1.289 -fun bounded_precise_card_of_type thy max default_card asgns T =
   1.290 +(* extended_context -> int -> (typ * int) list -> typ -> int *)
   1.291 +fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
   1.292    let
   1.293      (* typ list -> typ -> int *)
   1.294      fun aux avoid T =
   1.295 @@ -927,12 +943,12 @@
   1.296         | @{typ bool} => 2
   1.297         | @{typ unit} => 1
   1.298         | Type _ =>
   1.299 -         (case datatype_constrs thy T of
   1.300 +         (case datatype_constrs ext_ctxt T of
   1.301              [] => if is_integer_type T then 0 else raise SAME ()
   1.302            | constrs =>
   1.303              let
   1.304                val constr_cards =
   1.305 -                datatype_constrs thy T
   1.306 +                datatype_constrs ext_ctxt T
   1.307                  |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
   1.308                          o snd)
   1.309              in
   1.310 @@ -943,8 +959,9 @@
   1.311        handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
   1.312    in Int.min (max, aux [] T) end
   1.313  
   1.314 -(* theory -> typ -> bool *)
   1.315 -fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 []
   1.316 +(* extended_context -> typ -> bool *)
   1.317 +fun is_finite_type ext_ctxt =
   1.318 +  not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
   1.319  
   1.320  (* term -> bool *)
   1.321  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   1.322 @@ -965,6 +982,14 @@
   1.323  (* indexname * typ -> term -> term *)
   1.324  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   1.325  
   1.326 +(* theory -> string -> bool *)
   1.327 +fun is_funky_typedef_name thy s =
   1.328 +  s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   1.329 +         @{type_name int}]
   1.330 +  orelse is_frac_type thy (Type (s, []))
   1.331 +(* theory -> term -> bool *)
   1.332 +fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   1.333 +  | is_funky_typedef _ _ = false
   1.334  (* term -> bool *)
   1.335  fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
   1.336                           $ Const (@{const_name TYPE}, _)) = true
   1.337 @@ -975,9 +1000,7 @@
   1.338    | is_typedef_axiom thy boring
   1.339          (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
   1.340           $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
   1.341 -    boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
   1.342 -               orelse is_frac_type thy (Type (s, [])))
   1.343 -    andalso is_typedef thy s
   1.344 +    boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   1.345    | is_typedef_axiom _ _ _ = false
   1.346  
   1.347  (* Distinguishes between (1) constant definition axioms, (2) type arity and
   1.348 @@ -1015,24 +1038,6 @@
   1.349        | do_eq _ = false
   1.350    in do_eq end
   1.351  
   1.352 -(* This table is not pretty. A better approach would be to avoid expanding the
   1.353 -   operators to their low-level definitions, but this would require dealing with
   1.354 -   overloading. *)
   1.355 -val built_in_built_in_defs =
   1.356 -  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
   1.357 -   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
   1.358 -   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
   1.359 -   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
   1.360 -   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
   1.361 -   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
   1.362 -   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
   1.363 -   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
   1.364 -   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
   1.365 -   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
   1.366 -   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
   1.367 -   @{thm zero_nat_inst.zero_nat}]
   1.368 -  |> map prop_of
   1.369 -
   1.370  (* theory -> term list * term list * term list *)
   1.371  fun all_axioms_of thy =
   1.372    let
   1.373 @@ -1053,8 +1058,7 @@
   1.374      val (built_in_nondefs, user_nondefs) =
   1.375        List.partition (is_typedef_axiom thy false) user_nondefs
   1.376        |>> append built_in_nondefs
   1.377 -    val defs = built_in_built_in_defs @
   1.378 -               (thy |> PureThy.all_thms_of
   1.379 +    val defs = (thy |> PureThy.all_thms_of
   1.380                      |> filter (equal Thm.definitionK o Thm.get_kind o snd)
   1.381                      |> map (prop_of o snd) |> filter is_plain_definition) @
   1.382                 user_defs @ built_in_defs
   1.383 @@ -1185,7 +1189,7 @@
   1.384                      cons (case_name, AList.lookup (op =) descr index
   1.385                                       |> the |> #3 |> length))
   1.386                (Datatype.get_all thy) [] @
   1.387 -  map (apsnd length o snd) (#codatatypes (TheoryData.get thy))
   1.388 +  map (apsnd length o snd) (#codatatypes (Data.get thy))
   1.389  
   1.390  (* Proof.context -> term list -> const_table *)
   1.391  fun const_def_table ctxt ts =
   1.392 @@ -1221,7 +1225,7 @@
   1.393  
   1.394  (* theory -> (string * string) list *)
   1.395  fun ersatz_table thy =
   1.396 -  fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table
   1.397 +  fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
   1.398  
   1.399  (* const_table Unsynchronized.ref -> string -> term list -> unit *)
   1.400  fun add_simps simp_table s eqs =
   1.401 @@ -1238,7 +1242,7 @@
   1.402          if s = s' then
   1.403            ys |> (if AList.defined (op =) ys T' then
   1.404                     I
   1.405 -                else
   1.406 +                 else
   1.407                    cons (T', Refute.monomorphic_term
   1.408                                  (Sign.typ_match thy (T', T) Vartab.empty) t)
   1.409                    handle Type.TYPE_MATCH => I
   1.410 @@ -1292,29 +1296,26 @@
   1.411      list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
   1.412                               (index_seq 0 (length arg_Ts)) arg_Ts)
   1.413    end
   1.414 -(* theory -> typ -> int * styp -> term -> term *)
   1.415 -fun add_constr_case thy res_T (j, x) res_t =
   1.416 +(* extended_context -> typ -> int * styp -> term -> term *)
   1.417 +fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
   1.418    Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
   1.419 -  $ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t
   1.420 -(* theory -> typ -> typ -> term *)
   1.421 -fun optimized_case_def thy dataT res_T =
   1.422 +  $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
   1.423 +  $ res_t
   1.424 +(* extended_context -> typ -> typ -> term *)
   1.425 +fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
   1.426    let
   1.427 -    val xs = datatype_constrs thy dataT
   1.428 +    val xs = datatype_constrs ext_ctxt dataT
   1.429      val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
   1.430      val (xs', x) = split_last xs
   1.431    in
   1.432      constr_case_body thy (1, x)
   1.433 -    |> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')
   1.434 +    |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
   1.435      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   1.436    end
   1.437  
   1.438 -val redefined_in_Nitpick_thy =
   1.439 -  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
   1.440 -   @{const_name list_size}]
   1.441 -
   1.442 -(* theory -> string -> typ -> typ -> term -> term *)
   1.443 -fun optimized_record_get thy s rec_T res_T t =
   1.444 -  let val constr_x = the_single (datatype_constrs thy rec_T) in
   1.445 +(* extended_context -> string -> typ -> typ -> term -> term *)
   1.446 +fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
   1.447 +  let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
   1.448      case no_of_record_field thy s rec_T of
   1.449        ~1 => (case rec_T of
   1.450                 Type (_, Ts as _ :: _) =>
   1.451 @@ -1323,16 +1324,16 @@
   1.452                   val j = num_record_fields thy rec_T - 1
   1.453                 in
   1.454                   select_nth_constr_arg thy constr_x t j res_T
   1.455 -                 |> optimized_record_get thy s rec_T' res_T
   1.456 +                 |> optimized_record_get ext_ctxt s rec_T' res_T
   1.457                 end
   1.458               | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
   1.459                                  []))
   1.460      | j => select_nth_constr_arg thy constr_x t j res_T
   1.461    end
   1.462 -(* theory -> string -> typ -> term -> term -> term *)
   1.463 -fun optimized_record_update thy s rec_T fun_t rec_t =
   1.464 +(* extended_context -> string -> typ -> term -> term -> term *)
   1.465 +fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
   1.466    let
   1.467 -    val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T)
   1.468 +    val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
   1.469      val Ts = binder_types constr_T
   1.470      val n = length Ts
   1.471      val special_j = no_of_record_field thy s rec_T
   1.472 @@ -1343,7 +1344,7 @@
   1.473                          if j = special_j then
   1.474                            betapply (fun_t, t)
   1.475                          else if j = n - 1 andalso special_j = ~1 then
   1.476 -                          optimized_record_update thy s
   1.477 +                          optimized_record_update ext_ctxt s
   1.478                                (rec_T |> dest_Type |> snd |> List.last) fun_t t
   1.479                          else
   1.480                            t
   1.481 @@ -1381,7 +1382,6 @@
   1.482    (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
   1.483     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   1.484    andf (not o has_trivial_definition thy def_table)
   1.485 -  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
   1.486  
   1.487  (* term * term -> term *)
   1.488  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   1.489 @@ -1488,7 +1488,7 @@
   1.490            val (const, ts) =
   1.491              if is_built_in_const fast_descrs x then
   1.492                if s = @{const_name finite} then
   1.493 -                if is_finite_type thy (domain_type T) then
   1.494 +                if is_finite_type ext_ctxt (domain_type T) then
   1.495                    (Abs ("A", domain_type T, @{const True}), ts)
   1.496                  else case ts of
   1.497                    [Const (@{const_name UNIV}, _)] => (@{const False}, [])
   1.498 @@ -1501,24 +1501,26 @@
   1.499                  val (dataT, res_T) = nth_range_type n T
   1.500                                       |> domain_type pairf range_type
   1.501                in
   1.502 -                (optimized_case_def thy dataT res_T
   1.503 +                (optimized_case_def ext_ctxt dataT res_T
   1.504                   |> do_term (depth + 1) Ts, ts)
   1.505                end
   1.506              | _ =>
   1.507                if is_constr thy x then
   1.508                  (Const x, ts)
   1.509 +              else if is_stale_constr thy x then
   1.510 +                raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
   1.511 +                                     \(\"" ^ s ^ "\")")
   1.512                else if is_record_get thy x then
   1.513                  case length ts of
   1.514                    0 => (do_term depth Ts (eta_expand Ts t 1), [])
   1.515 -                | _ => (optimized_record_get thy s (domain_type T)
   1.516 +                | _ => (optimized_record_get ext_ctxt s (domain_type T)
   1.517                                               (range_type T) (hd ts), tl ts)
   1.518                else if is_record_update thy x then
   1.519                  case length ts of
   1.520 -                  2 => (optimized_record_update thy (unsuffix Record.updateN s)
   1.521 -                                                (nth_range_type 2 T)
   1.522 -                                                (do_term depth Ts (hd ts))
   1.523 -                                                (do_term depth Ts (nth ts 1)),
   1.524 -                        [])
   1.525 +                  2 => (optimized_record_update ext_ctxt
   1.526 +                            (unsuffix Record.updateN s) (nth_range_type 2 T)
   1.527 +                            (do_term depth Ts (hd ts))
   1.528 +                            (do_term depth Ts (nth ts 1)), [])
   1.529                  | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
   1.530                else if is_rep_fun thy x then
   1.531                  let val x' = mate_of_rep_fun thy x in
   1.532 @@ -1545,10 +1547,10 @@
   1.533          in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
   1.534    in do_term 0 [] end
   1.535  
   1.536 -(* theory -> typ -> term list *)
   1.537 -fun codatatype_bisim_axioms thy T =
   1.538 +(* extended_context -> typ -> term list *)
   1.539 +fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
   1.540    let
   1.541 -    val xs = datatype_constrs thy T
   1.542 +    val xs = datatype_constrs ext_ctxt T
   1.543      val set_T = T --> bool_T
   1.544      val iter_T = @{typ bisim_iterator}
   1.545      val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
   1.546 @@ -1571,14 +1573,14 @@
   1.547        let
   1.548          val arg_Ts = binder_types T
   1.549          val core_t =
   1.550 -          discriminate_value thy x y_var ::
   1.551 +          discriminate_value ext_ctxt x y_var ::
   1.552            map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
   1.553            |> foldr1 s_conj
   1.554        in List.foldr absdummy core_t arg_Ts end
   1.555    in
   1.556      [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
   1.557       $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
   1.558 -        $ (betapplys (optimized_case_def thy T bool_T,
   1.559 +        $ (betapplys (optimized_case_def ext_ctxt T bool_T,
   1.560                        map case_func xs @ [x_var]))),
   1.561       HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
   1.562       $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
   1.563 @@ -1629,6 +1631,7 @@
   1.564                                   (tac ctxt (auto_tac (clasimpset_of ctxt))))
   1.565         #> the #> Goal.finish ctxt) goal
   1.566  
   1.567 +val max_cached_wfs = 100
   1.568  val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
   1.569  val cached_wf_props : (term * bool) list Unsynchronized.ref =
   1.570    Unsynchronized.ref []
   1.571 @@ -1637,11 +1640,11 @@
   1.572                          ScnpReconstruct.sizechange_tac]
   1.573  
   1.574  (* extended_context -> const_table -> styp -> bool *)
   1.575 -fun is_is_well_founded_inductive_pred
   1.576 +fun uncached_is_well_founded_inductive_pred
   1.577          ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
   1.578           : extended_context) (x as (_, T)) =
   1.579    case def_props_for_const thy fast_descrs intro_table x of
   1.580 -    [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
   1.581 +    [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   1.582                        [Const x])
   1.583    | intro_ts =>
   1.584      (case map (triple_for_intro_rule thy x) intro_ts
   1.585 @@ -1662,8 +1665,11 @@
   1.586                   else
   1.587                     ()
   1.588         in
   1.589 -         if tac_timeout = (!cached_timeout) then ()
   1.590 -         else (cached_wf_props := []; cached_timeout := tac_timeout);
   1.591 +         if tac_timeout = (!cached_timeout)
   1.592 +            andalso length (!cached_wf_props) < max_cached_wfs then
   1.593 +           ()
   1.594 +         else
   1.595 +           (cached_wf_props := []; cached_timeout := tac_timeout);
   1.596           case AList.lookup (op =) (!cached_wf_props) prop of
   1.597             SOME wf => wf
   1.598           | NONE =>
   1.599 @@ -1690,7 +1696,7 @@
   1.600                  | NONE =>
   1.601                    let
   1.602                      val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   1.603 -                    val wf = is_is_well_founded_inductive_pred ext_ctxt x
   1.604 +                    val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
   1.605                    in
   1.606                      Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   1.607                    end
   1.608 @@ -1878,9 +1884,7 @@
   1.609  (* extended_context -> styp -> term list *)
   1.610  fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
   1.611                                              psimp_table, ...}) (x as (s, _)) =
   1.612 -  if s mem redefined_in_Nitpick_thy then
   1.613 -    []
   1.614 -  else case def_props_for_const thy fast_descrs (!simp_table) x of
   1.615 +  case def_props_for_const thy fast_descrs (!simp_table) x of
   1.616      [] => (case def_props_for_const thy fast_descrs psimp_table x of
   1.617               [] => [inductive_pred_axiom ext_ctxt x]
   1.618             | psimps => psimps)
   1.619 @@ -1889,7 +1893,7 @@
   1.620  val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
   1.621  
   1.622  (* term list -> term list *)
   1.623 -fun coalesce_type_vars_in_terms ts =
   1.624 +fun merge_type_vars_in_terms ts =
   1.625    let
   1.626      (* typ -> (sort * string) list -> (sort * string) list *)
   1.627      fun add_type (TFree (s, S)) table =
   1.628 @@ -2002,8 +2006,8 @@
   1.629                                                           seen, concl)
   1.630    end
   1.631  
   1.632 -(* theory -> bool -> term -> term *)
   1.633 -fun destroy_pulled_out_constrs thy axiom t =
   1.634 +(* extended_context -> bool -> term -> term *)
   1.635 +fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
   1.636    let
   1.637      (* styp -> int *)
   1.638      val num_occs_of_var =
   1.639 @@ -2037,7 +2041,7 @@
   1.640                andalso (not careful orelse not (is_Var t1)
   1.641                         orelse String.isPrefix val_var_prefix
   1.642                                                (fst (fst (dest_Var t1)))) then
   1.643 -             discriminate_value thy x t1 ::
   1.644 +             discriminate_value ext_ctxt x t1 ::
   1.645               map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
   1.646               |> foldr1 s_conj
   1.647               |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
   1.648 @@ -2564,7 +2568,6 @@
   1.649      t
   1.650    else
   1.651      let
   1.652 -      (* FIXME: strong enough in the face of user-defined axioms? *)
   1.653        val blacklist = if depth = 0 then []
   1.654                        else case term_under_def t of Const x => [x] | _ => []
   1.655        (* term list -> typ list -> term -> term *)
   1.656 @@ -2727,7 +2730,7 @@
   1.657          | (Type (new_s, new_Ts as [new_T1, new_T2]),
   1.658             Type (old_s, old_Ts as [old_T1, old_T2])) =>
   1.659            if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
   1.660 -            case constr_expand thy old_T t of
   1.661 +            case constr_expand ext_ctxt old_T t of
   1.662                Const (@{const_name FunBox}, _) $ t1 =>
   1.663                if new_s = "fun" then
   1.664                  coerce_term Ts new_T (Type ("fun", old_Ts)) t1
   1.665 @@ -3030,14 +3033,16 @@
   1.666               else if is_abs_fun thy x then
   1.667                 accum |> fold (add_nondef_axiom depth)
   1.668                               (nondef_props_for_const thy false nondef_table x)
   1.669 -                     |> fold (add_def_axiom depth)
   1.670 -                             (nondef_props_for_const thy true
   1.671 +                     |> is_funky_typedef thy (range_type T)
   1.672 +                        ? fold (add_def_axiom depth)
   1.673 +                               (nondef_props_for_const thy true
   1.674                                                      (extra_table def_table s) x)
   1.675               else if is_rep_fun thy x then
   1.676                 accum |> fold (add_nondef_axiom depth)
   1.677                               (nondef_props_for_const thy false nondef_table x)
   1.678 -                     |> fold (add_def_axiom depth)
   1.679 -                             (nondef_props_for_const thy true
   1.680 +                     |> is_funky_typedef thy (range_type T)
   1.681 +                        ? fold (add_def_axiom depth)
   1.682 +                               (nondef_props_for_const thy true
   1.683                                                      (extra_table def_table s) x)
   1.684                       |> add_axioms_for_term depth
   1.685                                              (Const (mate_of_rep_fun thy x))
   1.686 @@ -3068,7 +3073,7 @@
   1.687          #> (if is_pure_typedef thy T then
   1.688                fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
   1.689              else if max_bisim_depth >= 0 andalso is_codatatype thy T then
   1.690 -              fold (add_def_axiom depth) (codatatype_bisim_axioms thy T)
   1.691 +              fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
   1.692              else
   1.693                I)
   1.694      (* int -> typ -> sort -> accumulator -> accumulator *)
   1.695 @@ -3312,7 +3317,7 @@
   1.696        #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
   1.697        #> destroy_constrs ? (pull_out_universal_constrs thy def
   1.698                              #> pull_out_existential_constrs thy
   1.699 -                            #> destroy_pulled_out_constrs thy def)
   1.700 +                            #> destroy_pulled_out_constrs ext_ctxt def)
   1.701        #> curry_assms
   1.702        #> destroy_universal_equalities
   1.703        #> destroy_existential_equalities thy