src/HOL/Tools/Nitpick/nitpick_hol.ML
author blanchet
Mon Mar 29 15:50:18 2010 +0200 (2010-03-29)
changeset 36062 194cb6e3c13f
parent 35994 9cc3df9a606e
child 36126 00d550b6cfd4
permissions -rw-r--r--
get rid of Polyhash, since it's no longer used
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_hol.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Auxiliary HOL-related functions used by Nitpick.
     6 *)
     7 
     8 signature NITPICK_HOL =
     9 sig
    10   type styp = Nitpick_Util.styp
    11   type const_table = term list Symtab.table
    12   type special_fun = (styp * int list * term list) * styp
    13   type unrolled = styp * styp
    14   type wf_cache = (styp * (bool * bool)) list
    15 
    16   type hol_context = {
    17     thy: theory,
    18     ctxt: Proof.context,
    19     max_bisim_depth: int,
    20     boxes: (typ option * bool option) list,
    21     stds: (typ option * bool) list,
    22     wfs: (styp option * bool option) list,
    23     user_axioms: bool option,
    24     debug: bool,
    25     binary_ints: bool option,
    26     destroy_constrs: bool,
    27     specialize: bool,
    28     skolemize: bool,
    29     star_linear_preds: bool,
    30     uncurry: bool,
    31     fast_descrs: bool,
    32     tac_timeout: Time.time option,
    33     evals: term list,
    34     case_names: (string * int) list,
    35     def_table: const_table,
    36     nondef_table: const_table,
    37     user_nondefs: term list,
    38     simp_table: const_table Unsynchronized.ref,
    39     psimp_table: const_table,
    40     choice_spec_table: const_table,
    41     intro_table: const_table,
    42     ground_thm_table: term list Inttab.table,
    43     ersatz_table: (string * string) list,
    44     skolems: (string * string list) list Unsynchronized.ref,
    45     special_funs: special_fun list Unsynchronized.ref,
    46     unrolled_preds: unrolled list Unsynchronized.ref,
    47     wf_cache: wf_cache Unsynchronized.ref,
    48     constr_cache: (typ * styp list) list Unsynchronized.ref}
    49 
    50   datatype fixpoint_kind = Lfp | Gfp | NoFp
    51   datatype boxability =
    52     InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
    53 
    54   val name_sep : string
    55   val numeral_prefix : string
    56   val base_prefix : string
    57   val step_prefix : string
    58   val unrolled_prefix : string
    59   val ubfp_prefix : string
    60   val lbfp_prefix : string
    61   val quot_normal_prefix : string
    62   val skolem_prefix : string
    63   val special_prefix : string
    64   val uncurry_prefix : string
    65   val eval_prefix : string
    66   val iter_var_prefix : string
    67   val strip_first_name_sep : string -> string * string
    68   val original_name : string -> string
    69   val s_conj : term * term -> term
    70   val s_disj : term * term -> term
    71   val strip_any_connective : term -> term list * term
    72   val conjuncts_of : term -> term list
    73   val disjuncts_of : term -> term list
    74   val unarize_unbox_etc_type : typ -> typ
    75   val uniterize_unarize_unbox_etc_type : typ -> typ
    76   val string_for_type : Proof.context -> typ -> string
    77   val prefix_name : string -> string -> string
    78   val shortest_name : string -> string
    79   val short_name : string -> string
    80   val shorten_names_in_term : term -> term
    81   val strict_type_match : theory -> typ * typ -> bool
    82   val type_match : theory -> typ * typ -> bool
    83   val const_match : theory -> styp * styp -> bool
    84   val term_match : theory -> term * term -> bool
    85   val frac_from_term_pair : typ -> term -> term -> term
    86   val is_TFree : typ -> bool
    87   val is_higher_order_type : typ -> bool
    88   val is_fun_type : typ -> bool
    89   val is_set_type : typ -> bool
    90   val is_pair_type : typ -> bool
    91   val is_lfp_iterator_type : typ -> bool
    92   val is_gfp_iterator_type : typ -> bool
    93   val is_fp_iterator_type : typ -> bool
    94   val is_iterator_type : typ -> bool
    95   val is_boolean_type : typ -> bool
    96   val is_integer_type : typ -> bool
    97   val is_bit_type : typ -> bool
    98   val is_word_type : typ -> bool
    99   val is_integer_like_type : typ -> bool
   100   val is_record_type : typ -> bool
   101   val is_number_type : theory -> typ -> bool
   102   val const_for_iterator_type : typ -> styp
   103   val strip_n_binders : int -> typ -> typ list * typ
   104   val nth_range_type : int -> typ -> typ
   105   val num_factors_in_type : typ -> int
   106   val num_binder_types : typ -> int
   107   val curried_binder_types : typ -> typ list
   108   val mk_flat_tuple : typ -> term list -> term
   109   val dest_n_tuple : int -> term -> term list
   110   val is_real_datatype : theory -> string -> bool
   111   val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
   112   val is_quot_type : theory -> typ -> bool
   113   val is_codatatype : theory -> typ -> bool
   114   val is_pure_typedef : theory -> typ -> bool
   115   val is_univ_typedef : theory -> typ -> bool
   116   val is_datatype : theory -> (typ option * bool) list -> typ -> bool
   117   val is_record_constr : styp -> bool
   118   val is_record_get : theory -> styp -> bool
   119   val is_record_update : theory -> styp -> bool
   120   val is_abs_fun : theory -> styp -> bool
   121   val is_rep_fun : theory -> styp -> bool
   122   val is_quot_abs_fun : Proof.context -> styp -> bool
   123   val is_quot_rep_fun : Proof.context -> styp -> bool
   124   val mate_of_rep_fun : theory -> styp -> styp
   125   val is_constr_like : theory -> styp -> bool
   126   val is_stale_constr : theory -> styp -> bool
   127   val is_constr : theory -> (typ option * bool) list -> styp -> bool
   128   val is_sel : string -> bool
   129   val is_sel_like_and_no_discr : string -> bool
   130   val box_type : hol_context -> boxability -> typ -> typ
   131   val binarize_nat_and_int_in_type : typ -> typ
   132   val binarize_nat_and_int_in_term : term -> term
   133   val discr_for_constr : styp -> styp
   134   val num_sels_for_constr_type : typ -> int
   135   val nth_sel_name_for_constr_name : string -> int -> string
   136   val nth_sel_for_constr : styp -> int -> styp
   137   val binarized_and_boxed_nth_sel_for_constr :
   138     hol_context -> bool -> styp -> int -> styp
   139   val sel_no_from_name : string -> int
   140   val close_form : term -> term
   141   val eta_expand : typ list -> term -> int -> term
   142   val extensionalize : term -> term
   143   val distinctness_formula : typ -> term list -> term
   144   val register_frac_type : string -> (string * string) list -> theory -> theory
   145   val unregister_frac_type : string -> theory -> theory
   146   val register_codatatype : typ -> string -> styp list -> theory -> theory
   147   val unregister_codatatype : typ -> theory -> theory
   148   val datatype_constrs : hol_context -> typ -> styp list
   149   val binarized_and_boxed_datatype_constrs :
   150     hol_context -> bool -> typ -> styp list
   151   val num_datatype_constrs : hol_context -> typ -> int
   152   val constr_name_for_sel_like : string -> string
   153   val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   154   val discriminate_value : hol_context -> styp -> term -> term
   155   val select_nth_constr_arg :
   156     theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
   157   val construct_value :
   158     theory -> (typ option * bool) list -> styp -> term list -> term
   159   val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
   160   val card_of_type : (typ * int) list -> typ -> int
   161   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   162   val bounded_exact_card_of_type :
   163     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   164   val is_finite_type : hol_context -> typ -> bool
   165   val is_small_finite_type : hol_context -> typ -> bool
   166   val special_bounds : term list -> (indexname * typ) list
   167   val abs_var : indexname * typ -> term -> term
   168   val is_funky_typedef : theory -> typ -> bool
   169   val all_axioms_of :
   170     theory -> (term * term) list -> term list * term list * term list
   171   val arity_of_built_in_const :
   172     theory -> (typ option * bool) list -> bool -> styp -> int option
   173   val is_built_in_const :
   174     theory -> (typ option * bool) list -> bool -> styp -> bool
   175   val term_under_def : term -> term
   176   val case_const_names :
   177     theory -> (typ option * bool) list -> (string * int) list
   178   val unfold_defs_in_term : hol_context -> term -> term
   179   val const_def_table :
   180     Proof.context -> (term * term) list -> term list -> const_table
   181   val const_nondef_table : term list -> const_table
   182   val const_simp_table : Proof.context -> (term * term) list -> const_table
   183   val const_psimp_table : Proof.context -> (term * term) list -> const_table
   184   val const_choice_spec_table :
   185     Proof.context -> (term * term) list -> const_table
   186   val inductive_intro_table :
   187     Proof.context -> (term * term) list -> const_table -> const_table
   188   val ground_theorem_table : theory -> term list Inttab.table
   189   val ersatz_table : theory -> (string * string) list
   190   val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
   191   val inverse_axioms_for_rep_fun : theory -> styp -> term list
   192   val optimized_typedef_axioms : theory -> string * typ list -> term list
   193   val optimized_quot_type_axioms :
   194     Proof.context -> (typ option * bool) list -> string * typ list -> term list
   195   val def_of_const : theory -> const_table -> styp -> term option
   196   val fixpoint_kind_of_rhs : term -> fixpoint_kind
   197   val fixpoint_kind_of_const :
   198     theory -> const_table -> string * typ -> fixpoint_kind
   199   val is_inductive_pred : hol_context -> styp -> bool
   200   val is_equational_fun : hol_context -> styp -> bool
   201   val is_constr_pattern_lhs : theory -> term -> bool
   202   val is_constr_pattern_formula : theory -> term -> bool
   203   val nondef_props_for_const :
   204     theory -> bool -> const_table -> styp -> term list
   205   val is_choice_spec_fun : hol_context -> styp -> bool
   206   val is_choice_spec_axiom : theory -> const_table -> term -> bool
   207   val codatatype_bisim_axioms : hol_context -> typ -> term list
   208   val is_well_founded_inductive_pred : hol_context -> styp -> bool
   209   val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   210   val equational_fun_axioms : hol_context -> styp -> term list
   211   val is_equational_fun_surely_complete : hol_context -> styp -> bool
   212   val merge_type_vars_in_terms : term list -> term list
   213   val ground_types_in_type : hol_context -> bool -> typ -> typ list
   214   val ground_types_in_terms : hol_context -> bool -> term list -> typ list
   215 end;
   216 
   217 structure Nitpick_HOL : NITPICK_HOL =
   218 struct
   219 
   220 open Sledgehammer_Util
   221 open Nitpick_Util
   222 
   223 type const_table = term list Symtab.table
   224 type special_fun = (styp * int list * term list) * styp
   225 type unrolled = styp * styp
   226 type wf_cache = (styp * (bool * bool)) list
   227 
   228 type hol_context = {
   229   thy: theory,
   230   ctxt: Proof.context,
   231   max_bisim_depth: int,
   232   boxes: (typ option * bool option) list,
   233   stds: (typ option * bool) list,
   234   wfs: (styp option * bool option) list,
   235   user_axioms: bool option,
   236   debug: bool,
   237   binary_ints: bool option,
   238   destroy_constrs: bool,
   239   specialize: bool,
   240   skolemize: bool,
   241   star_linear_preds: bool,
   242   uncurry: bool,
   243   fast_descrs: bool,
   244   tac_timeout: Time.time option,
   245   evals: term list,
   246   case_names: (string * int) list,
   247   def_table: const_table,
   248   nondef_table: const_table,
   249   user_nondefs: term list,
   250   simp_table: const_table Unsynchronized.ref,
   251   psimp_table: const_table,
   252   choice_spec_table: const_table,
   253   intro_table: const_table,
   254   ground_thm_table: term list Inttab.table,
   255   ersatz_table: (string * string) list,
   256   skolems: (string * string list) list Unsynchronized.ref,
   257   special_funs: special_fun list Unsynchronized.ref,
   258   unrolled_preds: unrolled list Unsynchronized.ref,
   259   wf_cache: wf_cache Unsynchronized.ref,
   260   constr_cache: (typ * styp list) list Unsynchronized.ref}
   261 
   262 datatype fixpoint_kind = Lfp | Gfp | NoFp
   263 datatype boxability =
   264   InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
   265 
   266 structure Data = Theory_Data(
   267   type T = {frac_types: (string * (string * string) list) list,
   268             codatatypes: (string * (string * styp list)) list}
   269   val empty = {frac_types = [], codatatypes = []}
   270   val extend = I
   271   fun merge ({frac_types = fs1, codatatypes = cs1},
   272                {frac_types = fs2, codatatypes = cs2}) : T =
   273     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
   274      codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
   275 
   276 val name_sep = "$"
   277 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
   278 val sel_prefix = nitpick_prefix ^ "sel"
   279 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
   280 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
   281 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
   282 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
   283 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
   284 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
   285 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
   286 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
   287 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
   288 val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
   289 val skolem_prefix = nitpick_prefix ^ "sk"
   290 val special_prefix = nitpick_prefix ^ "sp"
   291 val uncurry_prefix = nitpick_prefix ^ "unc"
   292 val eval_prefix = nitpick_prefix ^ "eval"
   293 val iter_var_prefix = "i"
   294 
   295 (** Constant/type information and term/type manipulation **)
   296 
   297 (* int -> string *)
   298 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
   299 (* Proof.context -> typ -> string *)
   300 fun quot_normal_name_for_type ctxt T =
   301   quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
   302 
   303 (* string -> string * string *)
   304 val strip_first_name_sep =
   305   Substring.full #> Substring.position name_sep ##> Substring.triml 1
   306   #> pairself Substring.string
   307 (* string -> string *)
   308 fun original_name s =
   309   if String.isPrefix nitpick_prefix s then
   310     case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
   311   else
   312     s
   313 
   314 (* term * term -> term *)
   315 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   316   | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
   317   | s_betapply p = betapply p
   318 (* term * term list -> term *)
   319 val s_betapplys = Library.foldl s_betapply
   320 
   321 (* term * term -> term *)
   322 fun s_conj (t1, @{const True}) = t1
   323   | s_conj (@{const True}, t2) = t2
   324   | s_conj (t1, t2) =
   325     if t1 = @{const False} orelse t2 = @{const False} then @{const False}
   326     else HOLogic.mk_conj (t1, t2)
   327 fun s_disj (t1, @{const False}) = t1
   328   | s_disj (@{const False}, t2) = t2
   329   | s_disj (t1, t2) =
   330     if t1 = @{const True} orelse t2 = @{const True} then @{const True}
   331     else HOLogic.mk_disj (t1, t2)
   332 
   333 (* term -> term -> term list *)
   334 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
   335     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   336   | strip_connective _ t = [t]
   337 (* term -> term list * term *)
   338 fun strip_any_connective (t as (t0 $ _ $ _)) =
   339     if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
   340       (strip_connective t0 t, t0)
   341     else
   342       ([t], @{const Not})
   343   | strip_any_connective t = ([t], @{const Not})
   344 (* term -> term list *)
   345 val conjuncts_of = strip_connective @{const "op &"}
   346 val disjuncts_of = strip_connective @{const "op |"}
   347 
   348 (* When you add constants to these lists, make sure to handle them in
   349    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   350    well. *)
   351 val built_in_consts =
   352   [(@{const_name all}, 1),
   353    (@{const_name "=="}, 2),
   354    (@{const_name "==>"}, 2),
   355    (@{const_name Pure.conjunction}, 2),
   356    (@{const_name Trueprop}, 1),
   357    (@{const_name Not}, 1),
   358    (@{const_name False}, 0),
   359    (@{const_name True}, 0),
   360    (@{const_name All}, 1),
   361    (@{const_name Ex}, 1),
   362    (@{const_name "op ="}, 2),
   363    (@{const_name "op &"}, 2),
   364    (@{const_name "op |"}, 2),
   365    (@{const_name "op -->"}, 2),
   366    (@{const_name If}, 3),
   367    (@{const_name Let}, 2),
   368    (@{const_name Unity}, 0),
   369    (@{const_name Pair}, 2),
   370    (@{const_name fst}, 1),
   371    (@{const_name snd}, 1),
   372    (@{const_name Id}, 0),
   373    (@{const_name insert}, 2),
   374    (@{const_name converse}, 1),
   375    (@{const_name trancl}, 1),
   376    (@{const_name rel_comp}, 2),
   377    (@{const_name image}, 2),
   378    (@{const_name finite}, 1),
   379    (@{const_name unknown}, 0),
   380    (@{const_name is_unknown}, 1),
   381    (@{const_name safe_The}, 1),
   382    (@{const_name safe_Eps}, 1),
   383    (@{const_name Frac}, 0),
   384    (@{const_name norm_frac}, 0)]
   385 val built_in_nat_consts =
   386   [(@{const_name Suc}, 0),
   387    (@{const_name nat}, 0),
   388    (@{const_name nat_gcd}, 0),
   389    (@{const_name nat_lcm}, 0)]
   390 val built_in_descr_consts =
   391   [(@{const_name The}, 1),
   392    (@{const_name Eps}, 1)]
   393 val built_in_typed_consts =
   394   [((@{const_name zero_class.zero}, int_T), 0),
   395    ((@{const_name one_class.one}, int_T), 0),
   396    ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
   397    ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
   398    ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
   399    ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
   400    ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
   401    ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
   402    ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
   403 val built_in_typed_nat_consts =
   404   [((@{const_name zero_class.zero}, nat_T), 0),
   405    ((@{const_name one_class.one}, nat_T), 0),
   406    ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
   407    ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
   408    ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
   409    ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
   410    ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   411    ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   412    ((@{const_name of_nat}, nat_T --> int_T), 0)]
   413 val built_in_set_consts =
   414   [(@{const_name semilattice_inf_class.inf}, 2),
   415    (@{const_name semilattice_sup_class.sup}, 2),
   416    (@{const_name minus_class.minus}, 2),
   417    (@{const_name ord_class.less_eq}, 2)]
   418 
   419 (* typ -> typ *)
   420 fun unarize_type @{typ "unsigned_bit word"} = nat_T
   421   | unarize_type @{typ "signed_bit word"} = int_T
   422   | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
   423   | unarize_type T = T
   424 fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
   425     unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
   426   | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
   427     unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
   428   | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
   429     Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
   430   | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
   431   | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
   432   | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
   433     Type (s, map unarize_unbox_etc_type Ts)
   434   | unarize_unbox_etc_type T = T
   435 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
   436   | uniterize_type @{typ bisim_iterator} = nat_T
   437   | uniterize_type T = T
   438 val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
   439 
   440 (* Proof.context -> typ -> string *)
   441 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
   442 
   443 (* string -> string -> string *)
   444 val prefix_name = Long_Name.qualify o Long_Name.base_name
   445 (* string -> string *)
   446 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
   447 (* string -> term -> term *)
   448 val prefix_abs_vars = Term.map_abs_vars o prefix_name
   449 (* string -> string *)
   450 fun short_name s =
   451   case space_explode name_sep s of
   452     [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
   453   | ss => map shortest_name ss |> space_implode "_"
   454 (* typ -> typ *)
   455 fun shorten_names_in_type (Type (s, Ts)) =
   456     Type (short_name s, map shorten_names_in_type Ts)
   457   | shorten_names_in_type T = T
   458 (* term -> term *)
   459 val shorten_names_in_term =
   460   map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
   461   #> map_types shorten_names_in_type
   462 
   463 (* theory -> typ * typ -> bool *)
   464 fun strict_type_match thy (T1, T2) =
   465   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   466   handle Type.TYPE_MATCH => false
   467 fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
   468 (* theory -> styp * styp -> bool *)
   469 fun const_match thy ((s1, T1), (s2, T2)) =
   470   s1 = s2 andalso type_match thy (T1, T2)
   471 (* theory -> term * term -> bool *)
   472 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
   473   | term_match thy (Free (s1, T1), Free (s2, T2)) =
   474     const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
   475   | term_match _ (t1, t2) = t1 aconv t2
   476 
   477 (* typ -> term -> term -> term *)
   478 fun frac_from_term_pair T t1 t2 =
   479   case snd (HOLogic.dest_number t1) of
   480     0 => HOLogic.mk_number T 0
   481   | n1 => case snd (HOLogic.dest_number t2) of
   482             1 => HOLogic.mk_number T n1
   483           | n2 => Const (@{const_name divide}, T --> T --> T)
   484                   $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
   485 
   486 (* typ -> bool *)
   487 fun is_TFree (TFree _) = true
   488   | is_TFree _ = false
   489 fun is_higher_order_type (Type (@{type_name fun}, _)) = true
   490   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   491   | is_higher_order_type _ = false
   492 fun is_fun_type (Type (@{type_name fun}, _)) = true
   493   | is_fun_type _ = false
   494 fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
   495   | is_set_type _ = false
   496 fun is_pair_type (Type (@{type_name "*"}, _)) = true
   497   | is_pair_type _ = false
   498 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   499   | is_lfp_iterator_type _ = false
   500 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
   501   | is_gfp_iterator_type _ = false
   502 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
   503 fun is_iterator_type T =
   504   (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
   505 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
   506 fun is_integer_type T = (T = nat_T orelse T = int_T)
   507 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
   508 fun is_word_type (Type (@{type_name word}, _)) = true
   509   | is_word_type _ = false
   510 val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
   511 val is_record_type = not o null o Record.dest_recTs
   512 (* theory -> typ -> bool *)
   513 fun is_frac_type thy (Type (s, [])) =
   514     not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
   515   | is_frac_type _ _ = false
   516 fun is_number_type thy = is_integer_like_type orf is_frac_type thy
   517 
   518 (* bool -> styp -> typ *)
   519 fun iterator_type_for_const gfp (s, T) =
   520   Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
   521         binder_types T)
   522 (* typ -> styp *)
   523 fun const_for_iterator_type (Type (s, Ts)) =
   524     (strip_first_name_sep s |> snd, Ts ---> bool_T)
   525   | const_for_iterator_type T =
   526     raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
   527 
   528 (* int -> typ -> typ list * typ *)
   529 fun strip_n_binders 0 T = ([], T)
   530   | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
   531     strip_n_binders (n - 1) T2 |>> cons T1
   532   | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
   533     strip_n_binders n (Type (@{type_name fun}, Ts))
   534   | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   535 (* typ -> typ *)
   536 val nth_range_type = snd oo strip_n_binders
   537 
   538 (* typ -> int *)
   539 fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
   540     fold (Integer.add o num_factors_in_type) [T1, T2] 0
   541   | num_factors_in_type _ = 1
   542 fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
   543     1 + num_binder_types T2
   544   | num_binder_types _ = 0
   545 (* typ -> typ list *)
   546 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
   547 fun maybe_curried_binder_types T =
   548   (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
   549 
   550 (* typ -> term list -> term *)
   551 fun mk_flat_tuple _ [t] = t
   552   | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
   553     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   554   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   555 (* int -> term -> term list *)
   556 fun dest_n_tuple 1 t = [t]
   557   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   558 
   559 type typedef_info =
   560   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   561    set_def: thm option, prop_of_Rep: thm, set_name: string,
   562    Abs_inverse: thm option, Rep_inverse: thm option}
   563 
   564 (* theory -> string -> typedef_info *)
   565 fun typedef_info thy s =
   566   if is_frac_type thy (Type (s, [])) then
   567     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   568           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   569           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   570                           |> Logic.varify_global,
   571           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   572   else case Typedef.get_info_global thy s of
   573     (* FIXME handle multiple typedef interpretations (!??) *)
   574     [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
   575           Rep_inverse, ...})] =>
   576     SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
   577           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   578           set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
   579           Rep_inverse = SOME Rep_inverse}
   580   | _ => NONE
   581 
   582 (* theory -> string -> bool *)
   583 val is_typedef = is_some oo typedef_info
   584 val is_real_datatype = is_some oo Datatype.get_info
   585 (* theory -> (typ option * bool) list -> typ -> bool *)
   586 fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
   587 
   588 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
   589    e.g., by adding a field to "Datatype_Aux.info". *)
   590 (* theory -> (typ option * bool) list -> string -> bool *)
   591 fun is_basic_datatype thy stds s =
   592   member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   593                  @{type_name int}, "Code_Numeral.code_numeral"] s orelse
   594   (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
   595 
   596 (* theory -> typ -> typ -> typ -> typ *)
   597 fun instantiate_type thy T1 T1' T2 =
   598   Same.commit (Envir.subst_type_same
   599                    (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
   600   handle Type.TYPE_MATCH =>
   601          raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
   602 fun varify_and_instantiate_type thy T1 T1' T2 =
   603   instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
   604 
   605 (* theory -> typ -> typ -> styp *)
   606 fun repair_constr_type thy body_T' T =
   607   varify_and_instantiate_type thy (body_type T) body_T' T
   608 
   609 (* string -> (string * string) list -> theory -> theory *)
   610 fun register_frac_type frac_s ersaetze thy =
   611   let
   612     val {frac_types, codatatypes} = Data.get thy
   613     val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
   614   in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   615 (* string -> theory -> theory *)
   616 fun unregister_frac_type frac_s = register_frac_type frac_s []
   617 
   618 (* typ -> string -> styp list -> theory -> theory *)
   619 fun register_codatatype co_T case_name constr_xs thy =
   620   let
   621     val {frac_types, codatatypes} = Data.get thy
   622     val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
   623     val (co_s, co_Ts) = dest_Type co_T
   624     val _ =
   625       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
   626          co_s <> @{type_name fun} andalso
   627          not (is_basic_datatype thy [(NONE, true)] co_s) then
   628         ()
   629       else
   630         raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   631     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
   632                                    codatatypes
   633   in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   634 (* typ -> theory -> theory *)
   635 fun unregister_codatatype co_T = register_codatatype co_T "" []
   636 
   637 (* theory -> typ -> bool *)
   638 fun is_quot_type thy (Type (s, _)) =
   639     is_some (Quotient_Info.quotdata_lookup_raw thy s)
   640   | is_quot_type _ _ = false
   641 fun is_codatatype thy (Type (s, _)) =
   642     not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
   643                |> Option.map snd |> these))
   644   | is_codatatype _ _ = false
   645 fun is_pure_typedef thy (T as Type (s, _)) =
   646     is_typedef thy s andalso
   647     not (is_real_datatype thy s orelse is_quot_type thy T orelse
   648          is_codatatype thy T orelse is_record_type T orelse
   649          is_integer_like_type T)
   650   | is_pure_typedef _ _ = false
   651 fun is_univ_typedef thy (Type (s, _)) =
   652     (case typedef_info thy s of
   653        SOME {set_def, prop_of_Rep, ...} =>
   654        let
   655          val t_opt =
   656            case set_def of
   657              SOME thm => try (snd o Logic.dest_equals o prop_of) thm
   658            | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
   659                          prop_of_Rep
   660        in
   661          case t_opt of
   662            SOME (Const (@{const_name top}, _)) => true
   663            (* "Multiset.multiset" *)
   664          | SOME (Const (@{const_name Collect}, _)
   665                  $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
   666            (* "FinFun.finfun" *)
   667          | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
   668                      Const (@{const_name Ex}, _) $ Abs (_, _,
   669                          Const (@{const_name finite}, _) $ _))) => true
   670          | _ => false
   671        end
   672      | NONE => false)
   673   | is_univ_typedef _ _ = false
   674 (* theory -> (typ option * bool) list -> typ -> bool *)
   675 fun is_datatype thy stds (T as Type (s, _)) =
   676     (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
   677      is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
   678   | is_datatype _ _ _ = false
   679 
   680 (* theory -> typ -> (string * typ) list * (string * typ) *)
   681 fun all_record_fields thy T =
   682   let val (recs, more) = Record.get_extT_fields thy T in
   683     recs @ more :: all_record_fields thy (snd more)
   684   end
   685   handle TYPE _ => []
   686 (* styp -> bool *)
   687 fun is_record_constr (s, T) =
   688   String.isSuffix Record.extN s andalso
   689   let val dataT = body_type T in
   690     is_record_type dataT andalso
   691     s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
   692   end
   693 (* theory -> typ -> int *)
   694 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
   695 (* theory -> string -> typ -> int *)
   696 fun no_of_record_field thy s T1 =
   697   find_index (curry (op =) s o fst)
   698              (Record.get_extT_fields thy T1 ||> single |> op @)
   699 (* theory -> styp -> bool *)
   700 fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
   701     exists (curry (op =) s o fst) (all_record_fields thy T1)
   702   | is_record_get _ _ = false
   703 fun is_record_update thy (s, T) =
   704   String.isSuffix Record.updateN s andalso
   705   exists (curry (op =) (unsuffix Record.updateN s) o fst)
   706          (all_record_fields thy (body_type T))
   707   handle TYPE _ => false
   708 fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
   709     (case typedef_info thy s' of
   710        SOME {Abs_name, ...} => s = Abs_name
   711      | NONE => false)
   712   | is_abs_fun _ _ = false
   713 fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
   714     (case typedef_info thy s' of
   715        SOME {Rep_name, ...} => s = Rep_name
   716      | NONE => false)
   717   | is_rep_fun _ _ = false
   718 (* Proof.context -> styp -> bool *)
   719 fun is_quot_abs_fun ctxt
   720                     (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
   721     (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
   722      = SOME (Const x))
   723   | is_quot_abs_fun _ _ = false
   724 fun is_quot_rep_fun ctxt
   725                     (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
   726     (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
   727      = SOME (Const x))
   728   | is_quot_rep_fun _ _ = false
   729 
   730 (* theory -> styp -> styp *)
   731 fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
   732                                         [T1 as Type (s', _), T2]))) =
   733     (case typedef_info thy s' of
   734        SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
   735      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   736   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   737 (* theory -> typ -> typ *)
   738 fun rep_type_for_quot_type thy (T as Type (s, _)) =
   739   let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
   740     instantiate_type thy qtyp T rtyp
   741   end
   742 (* theory -> typ -> term *)
   743 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
   744     let
   745       val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
   746       val Ts' = qtyp |> dest_Type |> snd
   747     in subst_atomic_types (Ts' ~~ Ts) equiv_rel end
   748   | equiv_relation_for_quot_type _ T =
   749     raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
   750 
   751 (* theory -> styp -> bool *)
   752 fun is_coconstr thy (s, T) =
   753   let
   754     val {codatatypes, ...} = Data.get thy
   755     val co_T = body_type T
   756     val co_s = dest_Type co_T |> fst
   757   in
   758     exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
   759            (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
   760   end
   761   handle TYPE ("dest_Type", _, _) => false
   762 fun is_constr_like thy (s, T) =
   763   member (op =) [@{const_name FinFun}, @{const_name FunBox},
   764                  @{const_name PairBox}, @{const_name Quot},
   765                  @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
   766   let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
   767     Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
   768     (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
   769     is_coconstr thy x
   770   end
   771 fun is_stale_constr thy (x as (_, T)) =
   772   is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
   773   not (is_coconstr thy x)
   774 (* theory -> (typ option * bool) list -> styp -> bool *)
   775 fun is_constr thy stds (x as (_, T)) =
   776   is_constr_like thy x andalso
   777   not (is_basic_datatype thy stds
   778                          (fst (dest_Type (unarize_type (body_type T))))) andalso
   779   not (is_stale_constr thy x)
   780 (* string -> bool *)
   781 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   782 val is_sel_like_and_no_discr =
   783   String.isPrefix sel_prefix orf
   784   (member (op =) [@{const_name fst}, @{const_name snd}])
   785 
   786 (* boxability -> boxability *)
   787 fun in_fun_lhs_for InConstr = InSel
   788   | in_fun_lhs_for _ = InFunLHS
   789 fun in_fun_rhs_for InConstr = InConstr
   790   | in_fun_rhs_for InSel = InSel
   791   | in_fun_rhs_for InFunRHS1 = InFunRHS2
   792   | in_fun_rhs_for _ = InFunRHS1
   793 
   794 (* hol_context -> boxability -> typ -> bool *)
   795 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
   796   case T of
   797     Type (@{type_name fun}, _) =>
   798     (boxy = InPair orelse boxy = InFunLHS) andalso
   799     not (is_boolean_type (body_type T))
   800   | Type (@{type_name "*"}, Ts) =>
   801     boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
   802     ((boxy = InExpr orelse boxy = InFunLHS) andalso
   803      exists (is_boxing_worth_it hol_ctxt InPair)
   804             (map (box_type hol_ctxt InPair) Ts))
   805   | _ => false
   806 (* hol_context -> boxability -> string * typ list -> string *)
   807 and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
   808   case triple_lookup (type_match thy) boxes (Type z) of
   809     SOME (SOME box_me) => box_me
   810   | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
   811 (* hol_context -> boxability -> typ -> typ *)
   812 and box_type hol_ctxt boxy T =
   813   case T of
   814     Type (z as (@{type_name fun}, [T1, T2])) =>
   815     if boxy <> InConstr andalso boxy <> InSel andalso
   816        should_box_type hol_ctxt boxy z then
   817       Type (@{type_name fun_box},
   818             [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
   819     else
   820       box_type hol_ctxt (in_fun_lhs_for boxy) T1
   821       --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
   822   | Type (z as (@{type_name "*"}, Ts)) =>
   823     if boxy <> InConstr andalso boxy <> InSel
   824        andalso should_box_type hol_ctxt boxy z then
   825       Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
   826     else
   827       Type (@{type_name "*"},
   828             map (box_type hol_ctxt
   829                           (if boxy = InConstr orelse boxy = InSel then boxy
   830                            else InPair)) Ts)
   831   | _ => T
   832 
   833 (* typ -> typ *)
   834 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
   835   | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
   836   | binarize_nat_and_int_in_type (Type (s, Ts)) =
   837     Type (s, map binarize_nat_and_int_in_type Ts)
   838   | binarize_nat_and_int_in_type T = T
   839 (* term -> term *)
   840 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
   841 
   842 (* styp -> styp *)
   843 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   844 
   845 (* typ -> int *)
   846 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
   847 (* string -> int -> string *)
   848 fun nth_sel_name_for_constr_name s n =
   849   if s = @{const_name Pair} then
   850     if n = 0 then @{const_name fst} else @{const_name snd}
   851   else
   852     sel_prefix_for n ^ s
   853 (* styp -> int -> styp *)
   854 fun nth_sel_for_constr x ~1 = discr_for_constr x
   855   | nth_sel_for_constr (s, T) n =
   856     (nth_sel_name_for_constr_name s n,
   857      body_type T --> nth (maybe_curried_binder_types T) n)
   858 (* hol_context -> bool -> styp -> int -> styp *)
   859 fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
   860   apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
   861   oo nth_sel_for_constr
   862 
   863 (* string -> int *)
   864 fun sel_no_from_name s =
   865   if String.isPrefix discr_prefix s then
   866     ~1
   867   else if String.isPrefix sel_prefix s then
   868     s |> unprefix sel_prefix |> Int.fromString |> the
   869   else if s = @{const_name snd} then
   870     1
   871   else
   872     0
   873 
   874 (* term -> term *)
   875 val close_form =
   876   let
   877     (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
   878     fun close_up zs zs' =
   879       fold (fn (z as ((s, _), T)) => fn t' =>
   880                Term.all T $ Abs (s, T, abstract_over (Var z, t')))
   881            (take (length zs' - length zs) zs')
   882     (* (indexname * typ) list -> term -> term *)
   883     fun aux zs (@{const "==>"} $ t1 $ t2) =
   884         let val zs' = Term.add_vars t1 zs in
   885           close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
   886         end
   887       | aux zs t = close_up zs (Term.add_vars t zs) t
   888   in aux [] end
   889 
   890 (* typ list -> term -> int -> term *)
   891 fun eta_expand _ t 0 = t
   892   | eta_expand Ts (Abs (s, T, t')) n =
   893     Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
   894   | eta_expand Ts t n =
   895     fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
   896              (List.take (binder_types (fastype_of1 (Ts, t)), n))
   897              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
   898 
   899 (* term -> term *)
   900 fun extensionalize t =
   901   case t of
   902     (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
   903   | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
   904     let val v = Var ((s, maxidx_of_term t + 1), T) in
   905       extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
   906     end
   907   | _ => t
   908 
   909 (* typ -> term list -> term *)
   910 fun distinctness_formula T =
   911   all_distinct_unordered_pairs_of
   912   #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
   913   #> List.foldr (s_conj o swap) @{const True}
   914 
   915 (* typ -> term *)
   916 fun zero_const T = Const (@{const_name zero_class.zero}, T)
   917 fun suc_const T = Const (@{const_name Suc}, T --> T)
   918 
   919 (* hol_context -> typ -> styp list *)
   920 fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
   921                               (T as Type (s, Ts)) =
   922     (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
   923        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
   924      | _ =>
   925        if is_datatype thy stds T then
   926          case Datatype.get_info thy s of
   927            SOME {index, descr, ...} =>
   928            let
   929              val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   930            in
   931              map (fn (s', Us) =>
   932                      (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
   933                           ---> T)) constrs
   934            end
   935          | NONE =>
   936            if is_record_type T then
   937              let
   938                val s' = unsuffix Record.ext_typeN s ^ Record.extN
   939                val T' = (Record.get_extT_fields thy T
   940                         |> apsnd single |> uncurry append |> map snd) ---> T
   941              in [(s', T')] end
   942            else if is_quot_type thy T then
   943              [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
   944            else case typedef_info thy s of
   945              SOME {abs_type, rep_type, Abs_name, ...} =>
   946              [(Abs_name,
   947                varify_and_instantiate_type thy abs_type T rep_type --> T)]
   948            | NONE =>
   949              if T = @{typ ind} then
   950                [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   951              else
   952                []
   953        else
   954          [])
   955   | uncached_datatype_constrs _ _ = []
   956 (* hol_context -> typ -> styp list *)
   957 fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   958   case AList.lookup (op =) (!constr_cache) T of
   959     SOME xs => xs
   960   | NONE =>
   961     let val xs = uncached_datatype_constrs hol_ctxt T in
   962       (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   963     end
   964 (* hol_context -> bool -> typ -> styp list *)
   965 fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
   966   map (apsnd ((binarize ? binarize_nat_and_int_in_type)
   967               o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   968 (* hol_context -> typ -> int *)
   969 val num_datatype_constrs = length oo datatype_constrs
   970 
   971 (* string -> string *)
   972 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   973   | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   974   | constr_name_for_sel_like s' = original_name s'
   975 (* hol_context -> bool -> styp -> styp *)
   976 fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   977   let val s = constr_name_for_sel_like s' in
   978     AList.lookup (op =)
   979         (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
   980         s
   981     |> the |> pair s
   982   end
   983 
   984 (* hol_context -> styp -> term *)
   985 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   986   let val dataT = body_type T in
   987     if s = @{const_name Suc} then
   988       Abs (Name.uu, dataT,
   989            @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
   990     else if num_datatype_constrs hol_ctxt dataT >= 2 then
   991       Const (discr_for_constr x)
   992     else
   993       Abs (Name.uu, dataT, @{const True})
   994   end
   995 (* hol_context -> styp -> term -> term *)
   996 fun discriminate_value (hol_ctxt as {thy, ...}) x t =
   997   case head_of t of
   998     Const x' =>
   999     if x = x' then @{const True}
  1000     else if is_constr_like thy x' then @{const False}
  1001     else betapply (discr_term_for_constr hol_ctxt x, t)
  1002   | _ => betapply (discr_term_for_constr hol_ctxt x, t)
  1003 
  1004 (* theory -> (typ option * bool) list -> styp -> term -> term *)
  1005 fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
  1006   let val (arg_Ts, dataT) = strip_type T in
  1007     if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
  1008       @{term "%n::nat. n - 1"}
  1009     else if is_pair_type dataT then
  1010       Const (nth_sel_for_constr x n)
  1011     else
  1012       let
  1013         (* int -> typ -> int * term *)
  1014         fun aux m (Type (@{type_name "*"}, [T1, T2])) =
  1015             let
  1016               val (m, t1) = aux m T1
  1017               val (m, t2) = aux m T2
  1018             in (m, HOLogic.mk_prod (t1, t2)) end
  1019           | aux m T =
  1020             (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
  1021                     $ Bound 0)
  1022         val m = fold (Integer.add o num_factors_in_type)
  1023                      (List.take (arg_Ts, n)) 0
  1024       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
  1025   end
  1026 (* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
  1027 fun select_nth_constr_arg thy stds x t n res_T =
  1028   (case strip_comb t of
  1029      (Const x', args) =>
  1030      if x = x' then nth args n
  1031      else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
  1032      else raise SAME ()
  1033    | _ => raise SAME())
  1034   handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
  1035 
  1036 (* theory -> (typ option * bool) list -> styp -> term list -> term *)
  1037 fun construct_value _ _ x [] = Const x
  1038   | construct_value thy stds (x as (s, _)) args =
  1039     let val args = map Envir.eta_contract args in
  1040       case hd args of
  1041         Const (s', _) $ t =>
  1042         if is_sel_like_and_no_discr s' andalso
  1043            constr_name_for_sel_like s' = s andalso
  1044            forall (fn (n, t') =>
  1045                       select_nth_constr_arg thy stds x t n dummyT = t')
  1046                   (index_seq 0 (length args) ~~ args) then
  1047           t
  1048         else
  1049           list_comb (Const x, args)
  1050       | _ => list_comb (Const x, args)
  1051     end
  1052 
  1053 (* hol_context -> typ -> term -> term *)
  1054 fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
  1055   (case head_of t of
  1056      Const x => if is_constr_like thy x then t else raise SAME ()
  1057    | _ => raise SAME ())
  1058   handle SAME () =>
  1059          let
  1060            val x' as (_, T') =
  1061              if is_pair_type T then
  1062                let val (T1, T2) = HOLogic.dest_prodT T in
  1063                  (@{const_name Pair}, T1 --> T2 --> T)
  1064                end
  1065              else
  1066                datatype_constrs hol_ctxt T |> hd
  1067            val arg_Ts = binder_types T'
  1068          in
  1069            list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
  1070                                      (index_seq 0 (length arg_Ts)) arg_Ts)
  1071          end
  1072 
  1073 (* (term -> term) -> int -> term -> term *)
  1074 fun coerce_bound_no f j t =
  1075   case t of
  1076     t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
  1077   | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
  1078   | Bound j' => if j' = j then f t else t
  1079   | _ => t
  1080 (* hol_context -> typ -> typ -> term -> term *)
  1081 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
  1082   old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
  1083 (* hol_context -> typ list -> typ -> typ -> term -> term *)
  1084 and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
  1085   if old_T = new_T then
  1086     t
  1087   else
  1088     case (new_T, old_T) of
  1089       (Type (new_s, new_Ts as [new_T1, new_T2]),
  1090        Type (@{type_name fun}, [old_T1, old_T2])) =>
  1091       (case eta_expand Ts t 1 of
  1092          Abs (s, _, t') =>
  1093          Abs (s, new_T1,
  1094               t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
  1095                  |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
  1096          |> Envir.eta_contract
  1097          |> new_s <> @{type_name fun}
  1098             ? construct_value thy stds
  1099                   (if new_s = @{type_name fin_fun} then @{const_name FinFun}
  1100                    else @{const_name FunBox},
  1101                    Type (@{type_name fun}, new_Ts) --> new_T)
  1102               o single
  1103        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
  1104     | (Type (new_s, new_Ts as [new_T1, new_T2]),
  1105        Type (old_s, old_Ts as [old_T1, old_T2])) =>
  1106       if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
  1107          old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
  1108         case constr_expand hol_ctxt old_T t of
  1109           Const (old_s, _) $ t1 =>
  1110           if new_s = @{type_name fun} then
  1111             coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
  1112           else
  1113             construct_value thy stds
  1114                 (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
  1115                 [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
  1116                              (Type (@{type_name fun}, old_Ts)) t1]
  1117         | Const _ $ t1 $ t2 =>
  1118           construct_value thy stds
  1119               (if new_s = @{type_name "*"} then @{const_name Pair}
  1120                else @{const_name PairBox}, new_Ts ---> new_T)
  1121               (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
  1122                     [t1, t2])
  1123         | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
  1124       else
  1125         raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
  1126     | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
  1127 
  1128 (* (typ * int) list -> typ -> int *)
  1129 fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
  1130     reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
  1131   | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
  1132     card_of_type assigns T1 * card_of_type assigns T2
  1133   | card_of_type _ (Type (@{type_name itself}, _)) = 1
  1134   | card_of_type _ @{typ prop} = 2
  1135   | card_of_type _ @{typ bool} = 2
  1136   | card_of_type _ @{typ unit} = 1
  1137   | card_of_type assigns T =
  1138     case AList.lookup (op =) assigns T of
  1139       SOME k => k
  1140     | NONE => if T = @{typ bisim_iterator} then 0
  1141               else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
  1142 (* int -> (typ * int) list -> typ -> int *)
  1143 fun bounded_card_of_type max default_card assigns
  1144                          (Type (@{type_name fun}, [T1, T2])) =
  1145     let
  1146       val k1 = bounded_card_of_type max default_card assigns T1
  1147       val k2 = bounded_card_of_type max default_card assigns T2
  1148     in
  1149       if k1 = max orelse k2 = max then max
  1150       else Int.min (max, reasonable_power k2 k1)
  1151     end
  1152   | bounded_card_of_type max default_card assigns
  1153                          (Type (@{type_name "*"}, [T1, T2])) =
  1154     let
  1155       val k1 = bounded_card_of_type max default_card assigns T1
  1156       val k2 = bounded_card_of_type max default_card assigns T2
  1157     in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
  1158   | bounded_card_of_type max default_card assigns T =
  1159     Int.min (max, if default_card = ~1 then
  1160                     card_of_type assigns T
  1161                   else
  1162                     card_of_type assigns T
  1163                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  1164                            default_card)
  1165 (* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
  1166 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
  1167                                assigns T =
  1168   let
  1169     (* typ list -> typ -> int *)
  1170     fun aux avoid T =
  1171       (if member (op =) avoid T then
  1172          0
  1173        else if member (op =) finitizable_dataTs T then
  1174          raise SAME ()
  1175        else case T of
  1176          Type (@{type_name fun}, [T1, T2]) =>
  1177          let
  1178            val k1 = aux avoid T1
  1179            val k2 = aux avoid T2
  1180          in
  1181            if k1 = 0 orelse k2 = 0 then 0
  1182            else if k1 >= max orelse k2 >= max then max
  1183            else Int.min (max, reasonable_power k2 k1)
  1184          end
  1185        | Type (@{type_name "*"}, [T1, T2]) =>
  1186          let
  1187            val k1 = aux avoid T1
  1188            val k2 = aux avoid T2
  1189          in
  1190            if k1 = 0 orelse k2 = 0 then 0
  1191            else if k1 >= max orelse k2 >= max then max
  1192            else Int.min (max, k1 * k2)
  1193          end
  1194        | Type (@{type_name itself}, _) => 1
  1195        | @{typ prop} => 2
  1196        | @{typ bool} => 2
  1197        | @{typ unit} => 1
  1198        | Type _ =>
  1199          (case datatype_constrs hol_ctxt T of
  1200             [] => if is_integer_type T orelse is_bit_type T then 0
  1201                   else raise SAME ()
  1202           | constrs =>
  1203             let
  1204               val constr_cards =
  1205                 map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
  1206                     constrs
  1207             in
  1208               if exists (curry (op =) 0) constr_cards then 0
  1209               else Integer.sum constr_cards
  1210             end)
  1211        | _ => raise SAME ())
  1212       handle SAME () =>
  1213              AList.lookup (op =) assigns T |> the_default default_card
  1214   in Int.min (max, aux [] T) end
  1215 
  1216 val small_type_max_card = 5
  1217 
  1218 (* hol_context -> typ -> bool *)
  1219 fun is_finite_type hol_ctxt T =
  1220   bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
  1221 (* hol_context -> typ -> bool *)
  1222 fun is_small_finite_type hol_ctxt T =
  1223   let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
  1224     n > 0 andalso n <= small_type_max_card
  1225   end
  1226 
  1227 (* term -> bool *)
  1228 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
  1229   | is_ground_term (Const _) = true
  1230   | is_ground_term _ = false
  1231 
  1232 (* term -> word -> word *)
  1233 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
  1234   | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
  1235   | hashw_term _ = 0w0
  1236 (* term -> int *)
  1237 val hash_term = Word.toInt o hashw_term
  1238 
  1239 (* term list -> (indexname * typ) list *)
  1240 fun special_bounds ts =
  1241   fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
  1242 
  1243 (* indexname * typ -> term -> term *)
  1244 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
  1245 
  1246 (* theory -> string -> bool *)
  1247 fun is_funky_typedef_name thy s =
  1248   member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
  1249                  @{type_name int}] s orelse
  1250   is_frac_type thy (Type (s, []))
  1251 (* theory -> typ -> bool *)
  1252 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
  1253   | is_funky_typedef _ _ = false
  1254 (* term -> bool *)
  1255 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
  1256                          $ Const (@{const_name TYPE}, _)) = true
  1257   | is_arity_type_axiom _ = false
  1258 (* theory -> bool -> term -> bool *)
  1259 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
  1260     is_typedef_axiom thy boring t2
  1261   | is_typedef_axiom thy boring
  1262         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
  1263          $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
  1264          $ Const _ $ _)) =
  1265     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
  1266   | is_typedef_axiom _ _ _ = false
  1267 (* term -> bool *)
  1268 fun is_class_axiom t =
  1269   (t |> Logic.strip_horn |> swap |> op :: |> map Logic.dest_of_class; true)
  1270   handle TERM _ => false
  1271 
  1272 (* Distinguishes between (1) constant definition axioms, (2) type arity and
  1273    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
  1274    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
  1275    using "typedef_info". *)
  1276 (* theory -> (string * term) list -> string list -> term list * term list *)
  1277 fun partition_axioms_by_definitionality thy axioms def_names =
  1278   let
  1279     val axioms = sort (fast_string_ord o pairself fst) axioms
  1280     val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
  1281     val nondefs =
  1282       OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
  1283       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
  1284   in pairself (map snd) (defs, nondefs) end
  1285 
  1286 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
  1287    will do as long as it contains all the "axioms" and "axiomatization"
  1288    commands. *)
  1289 (* theory -> bool *)
  1290 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
  1291 
  1292 (* term -> bool *)
  1293 val is_trivial_definition =
  1294   the_default false o try (op aconv o Logic.dest_equals)
  1295 val is_plain_definition =
  1296   let
  1297     (* term -> bool *)
  1298     fun do_lhs t1 =
  1299       case strip_comb t1 of
  1300         (Const _, args) =>
  1301         forall is_Var args andalso not (has_duplicates (op =) args)
  1302       | _ => false
  1303     fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
  1304       | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
  1305         do_lhs t1
  1306       | do_eq _ = false
  1307   in do_eq end
  1308 
  1309 (* theory -> (term * term) list -> term list * term list * term list *)
  1310 fun all_axioms_of thy subst =
  1311   let
  1312     (* theory list -> term list *)
  1313     val axioms_of_thys =
  1314       maps Thm.axioms_of
  1315       #> map (apsnd (subst_atomic subst o prop_of))
  1316       #> filter_out (is_class_axiom o snd)
  1317     val specs = Defs.all_specifications_of (Theory.defs_of thy)
  1318     val def_names = specs |> maps snd |> map_filter #def
  1319                     |> OrdList.make fast_string_ord
  1320     val thys = thy :: Theory.ancestors_of thy
  1321     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
  1322     val built_in_axioms = axioms_of_thys built_in_thys
  1323     val user_axioms = axioms_of_thys user_thys
  1324     val (built_in_defs, built_in_nondefs) =
  1325       partition_axioms_by_definitionality thy built_in_axioms def_names
  1326       ||> filter (is_typedef_axiom thy false)
  1327     val (user_defs, user_nondefs) =
  1328       partition_axioms_by_definitionality thy user_axioms def_names
  1329     val (built_in_nondefs, user_nondefs) =
  1330       List.partition (is_typedef_axiom thy false) user_nondefs
  1331       |>> append built_in_nondefs
  1332     val defs =
  1333       (thy |> PureThy.all_thms_of
  1334            |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
  1335            |> map (prop_of o snd)
  1336            |> filter_out is_trivial_definition
  1337            |> filter is_plain_definition) @
  1338       user_defs @ built_in_defs
  1339   in (defs, built_in_nondefs, user_nondefs) end
  1340 
  1341 (* theory -> (typ option * bool) list -> bool -> styp -> int option *)
  1342 fun arity_of_built_in_const thy stds fast_descrs (s, T) =
  1343   if s = @{const_name If} then
  1344     if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
  1345   else
  1346     let val std_nats = is_standard_datatype thy stds nat_T in
  1347       case AList.lookup (op =)
  1348                     (built_in_consts
  1349                      |> std_nats ? append built_in_nat_consts
  1350                      |> fast_descrs ? append built_in_descr_consts) s of
  1351         SOME n => SOME n
  1352       | NONE =>
  1353         case AList.lookup (op =)
  1354                  (built_in_typed_consts
  1355                   |> std_nats ? append built_in_typed_nat_consts)
  1356                  (s, unarize_type T) of
  1357           SOME n => SOME n
  1358         | NONE =>
  1359           case s of
  1360             @{const_name zero_class.zero} =>
  1361             if is_iterator_type T then SOME 0 else NONE
  1362           | @{const_name Suc} =>
  1363             if is_iterator_type (domain_type T) then SOME 0 else NONE
  1364           | _ => if is_fun_type T andalso is_set_type (domain_type T) then
  1365                    AList.lookup (op =) built_in_set_consts s
  1366                  else
  1367                    NONE
  1368     end
  1369 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
  1370 val is_built_in_const = is_some oooo arity_of_built_in_const
  1371 
  1372 (* This function is designed to work for both real definition axioms and
  1373    simplification rules (equational specifications). *)
  1374 (* term -> term *)
  1375 fun term_under_def t =
  1376   case t of
  1377     @{const "==>"} $ _ $ t2 => term_under_def t2
  1378   | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
  1379   | @{const Trueprop} $ t1 => term_under_def t1
  1380   | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
  1381   | Abs (_, _, t') => term_under_def t'
  1382   | t1 $ _ => term_under_def t1
  1383   | _ => t
  1384 
  1385 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
  1386    traversal of the term, without which the wrong occurrence of a constant could
  1387    be matched in the face of overloading. *)
  1388 (* theory -> (typ option * bool) list -> bool -> const_table -> styp
  1389    -> term list *)
  1390 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
  1391   if is_built_in_const thy stds fast_descrs x then
  1392     []
  1393   else
  1394     these (Symtab.lookup table s)
  1395     |> map_filter (try (Refute.specialize_type thy x))
  1396     |> filter (curry (op =) (Const x) o term_under_def)
  1397 
  1398 (* term -> term option *)
  1399 fun normalized_rhs_of t =
  1400   let
  1401     (* term option -> term option *)
  1402     fun aux (v as Var _) (SOME t) = SOME (lambda v t)
  1403       | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
  1404       | aux _ _ = NONE
  1405     val (lhs, rhs) =
  1406       case t of
  1407         Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
  1408       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
  1409         (t1, t2)
  1410       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
  1411     val args = strip_comb lhs |> snd
  1412   in fold_rev aux args (SOME rhs) end
  1413 
  1414 (* theory -> const_table -> styp -> term option *)
  1415 fun def_of_const thy table (x as (s, _)) =
  1416   if is_built_in_const thy [(NONE, false)] false x orelse
  1417      original_name s <> s then
  1418     NONE
  1419   else
  1420     x |> def_props_for_const thy [(NONE, false)] false table |> List.last
  1421       |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
  1422     handle List.Empty => NONE
  1423 
  1424 (* term -> fixpoint_kind *)
  1425 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
  1426   | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
  1427   | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
  1428   | fixpoint_kind_of_rhs _ = NoFp
  1429 
  1430 (* theory -> const_table -> term -> bool *)
  1431 fun is_mutually_inductive_pred_def thy table t =
  1432   let
  1433     (* term -> bool *)
  1434     fun is_good_arg (Bound _) = true
  1435       | is_good_arg (Const (s, _)) =
  1436         s = @{const_name True} orelse s = @{const_name False} orelse
  1437         s = @{const_name undefined}
  1438       | is_good_arg _ = false
  1439   in
  1440     case t |> strip_abs_body |> strip_comb of
  1441       (Const x, ts as (_ :: _)) =>
  1442       (case def_of_const thy table x of
  1443          SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
  1444        | NONE => false)
  1445     | _ => false
  1446   end
  1447 (* theory -> const_table -> term -> term *)
  1448 fun unfold_mutually_inductive_preds thy table =
  1449   map_aterms (fn t as Const x =>
  1450                  (case def_of_const thy table x of
  1451                     SOME t' =>
  1452                     let val t' = Envir.eta_contract t' in
  1453                       if is_mutually_inductive_pred_def thy table t' then t'
  1454                       else t
  1455                     end
  1456                  | NONE => t)
  1457                | t => t)
  1458 
  1459 (* theory -> (typ option * bool) list -> (string * int) list *)
  1460 fun case_const_names thy stds =
  1461   Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
  1462                   if is_basic_datatype thy stds dtype_s then
  1463                     I
  1464                   else
  1465                     cons (case_name, AList.lookup (op =) descr index
  1466                                      |> the |> #3 |> length))
  1467               (Datatype.get_all thy) [] @
  1468   map (apsnd length o snd) (#codatatypes (Data.get thy))
  1469 
  1470 (* theory -> const_table -> string * typ -> fixpoint_kind *)
  1471 fun fixpoint_kind_of_const thy table x =
  1472   if is_built_in_const thy [(NONE, false)] false x then
  1473     NoFp
  1474   else
  1475     fixpoint_kind_of_rhs (the (def_of_const thy table x))
  1476     handle Option.Option => NoFp
  1477 
  1478 (* hol_context -> styp -> bool *)
  1479 fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
  1480                              ...} : hol_context) x =
  1481   fixpoint_kind_of_const thy def_table x <> NoFp andalso
  1482   not (null (def_props_for_const thy stds fast_descrs intro_table x))
  1483 fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
  1484                              ...} : hol_context) x =
  1485   exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
  1486                                                      x)))
  1487          [!simp_table, psimp_table]
  1488 fun is_inductive_pred hol_ctxt =
  1489   is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
  1490 fun is_equational_fun hol_ctxt =
  1491   (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
  1492    (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
  1493 
  1494 (* term -> term *)
  1495 fun lhs_of_equation t =
  1496   case t of
  1497     Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1498   | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
  1499   | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
  1500   | @{const Trueprop} $ t1 => lhs_of_equation t1
  1501   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1502   | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
  1503   | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
  1504   | _ => NONE
  1505 (* theory -> term -> bool *)
  1506 fun is_constr_pattern _ (Bound _) = true
  1507   | is_constr_pattern _ (Var _) = true
  1508   | is_constr_pattern thy t =
  1509     case strip_comb t of
  1510       (Const x, args) =>
  1511       is_constr_like thy x andalso forall (is_constr_pattern thy) args
  1512     | _ => false
  1513 fun is_constr_pattern_lhs thy t =
  1514   forall (is_constr_pattern thy) (snd (strip_comb t))
  1515 fun is_constr_pattern_formula thy t =
  1516   case lhs_of_equation t of
  1517     SOME t' => is_constr_pattern_lhs thy t'
  1518   | NONE => false
  1519 
  1520 (* Similar to "Refute.specialize_type" but returns all matches rather than only
  1521    the first (preorder) match. *)
  1522 (* theory -> styp -> term -> term list *)
  1523 fun multi_specialize_type thy slack (s, T) t =
  1524   let
  1525     (* term -> (typ * term) list -> (typ * term) list *)
  1526     fun aux (Const (s', T')) ys =
  1527         if s = s' then
  1528           ys |> (if AList.defined (op =) ys T' then
  1529                    I
  1530                  else
  1531                    cons (T', Refute.monomorphic_term
  1532                                  (Sign.typ_match thy (T', T) Vartab.empty) t)
  1533                    handle Type.TYPE_MATCH => I
  1534                         | Refute.REFUTE _ =>
  1535                           if slack then
  1536                             I
  1537                           else
  1538                             raise NOT_SUPPORTED ("too much polymorphism in \
  1539                                                  \axiom involving " ^ quote s))
  1540         else
  1541           ys
  1542       | aux _ ys = ys
  1543   in map snd (fold_aterms aux t []) end
  1544 (* theory -> bool -> const_table -> styp -> term list *)
  1545 fun nondef_props_for_const thy slack table (x as (s, _)) =
  1546   these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
  1547 
  1548 (* term -> term *)
  1549 fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2
  1550   | unvarify_term (Var ((s, 0), T)) = Free (s, T)
  1551   | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
  1552   | unvarify_term t = t
  1553 (* theory -> term -> term *)
  1554 fun axiom_for_choice_spec thy =
  1555   unvarify_term
  1556   #> Object_Logic.atomize_term thy
  1557   #> Choice_Specification.close_form
  1558   #> HOLogic.mk_Trueprop
  1559 (* hol_context -> styp -> bool *)
  1560 fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
  1561                         : hol_context) x =
  1562   case nondef_props_for_const thy true choice_spec_table x of
  1563     [] => false
  1564   | ts => case def_of_const thy def_table x of
  1565             SOME (Const (@{const_name Eps}, _) $ _) => true
  1566           | SOME _ => false
  1567           | NONE =>
  1568             let val ts' = nondef_props_for_const thy true nondef_table x in
  1569               length ts' = length ts andalso
  1570               forall (fn t =>
  1571                          exists (curry (op aconv) (axiom_for_choice_spec thy t))
  1572                                 ts') ts
  1573             end
  1574 
  1575 (* theory -> const_table -> term -> bool *)
  1576 fun is_choice_spec_axiom thy choice_spec_table t =
  1577   Symtab.exists (fn (_, ts) =>
  1578                     exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
  1579                 choice_spec_table
  1580 
  1581 (** Constant unfolding **)
  1582 
  1583 (* theory -> (typ option * bool) list -> int * styp -> term *)
  1584 fun constr_case_body thy stds (j, (x as (_, T))) =
  1585   let val arg_Ts = binder_types T in
  1586     list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
  1587                              (index_seq 0 (length arg_Ts)) arg_Ts)
  1588   end
  1589 (* hol_context -> typ -> int * styp -> term -> term *)
  1590 fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
  1591   Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
  1592   $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
  1593   $ res_t
  1594 (* hol_context -> typ -> typ -> term *)
  1595 fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
  1596   let
  1597     val xs = datatype_constrs hol_ctxt dataT
  1598     val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
  1599     val (xs', x) = split_last xs
  1600   in
  1601     constr_case_body thy stds (1, x)
  1602     |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
  1603     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
  1604   end
  1605 (* hol_context -> string -> typ -> typ -> term -> term *)
  1606 fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
  1607   let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
  1608     case no_of_record_field thy s rec_T of
  1609       ~1 => (case rec_T of
  1610                Type (_, Ts as _ :: _) =>
  1611                let
  1612                  val rec_T' = List.last Ts
  1613                  val j = num_record_fields thy rec_T - 1
  1614                in
  1615                  select_nth_constr_arg thy stds constr_x t j res_T
  1616                  |> optimized_record_get hol_ctxt s rec_T' res_T
  1617                end
  1618              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
  1619                                 []))
  1620     | j => select_nth_constr_arg thy stds constr_x t j res_T
  1621   end
  1622 (* hol_context -> string -> typ -> term -> term -> term *)
  1623 fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
  1624   let
  1625     val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
  1626     val Ts = binder_types constr_T
  1627     val n = length Ts
  1628     val special_j = no_of_record_field thy s rec_T
  1629     val ts =
  1630       map2 (fn j => fn T =>
  1631                let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
  1632                  if j = special_j then
  1633                    betapply (fun_t, t)
  1634                  else if j = n - 1 andalso special_j = ~1 then
  1635                    optimized_record_update hol_ctxt s
  1636                        (rec_T |> dest_Type |> snd |> List.last) fun_t t
  1637                  else
  1638                    t
  1639                end) (index_seq 0 n) Ts
  1640   in list_comb (Const constr_x, ts) end
  1641 
  1642 (* Prevents divergence in case of cyclic or infinite definition dependencies. *)
  1643 val unfold_max_depth = 255
  1644 
  1645 (* hol_context -> term -> term *)
  1646 fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
  1647                                       def_table, ground_thm_table, ersatz_table,
  1648                                       ...}) =
  1649   let
  1650     (* int -> typ list -> term -> term *)
  1651     fun do_term depth Ts t =
  1652       case t of
  1653         (t0 as Const (@{const_name Int.number_class.number_of},
  1654                       Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
  1655         ((if is_number_type thy ran_T then
  1656             let
  1657               val j = t1 |> HOLogic.dest_numeral
  1658                          |> ran_T = nat_T ? Integer.max 0
  1659               val s = numeral_prefix ^ signed_string_of_int j
  1660             in
  1661               if is_integer_like_type ran_T then
  1662                 if is_standard_datatype thy stds ran_T then
  1663                   Const (s, ran_T)
  1664                 else
  1665                   funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
  1666               else
  1667                 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
  1668                                   $ Const (s, int_T))
  1669             end
  1670             handle TERM _ => raise SAME ()
  1671           else
  1672             raise SAME ())
  1673          handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
  1674       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
  1675         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
  1676       | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
  1677         betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
  1678                    map (do_term depth Ts) [t1, t2])
  1679       | Const (x as (@{const_name distinct},
  1680                Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
  1681         $ (t1 as _ $ _) =>
  1682         (t1 |> HOLogic.dest_list |> distinctness_formula T'
  1683          handle TERM _ => do_const depth Ts t x [t1])
  1684       | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
  1685         if is_ground_term t1 andalso
  1686            exists (Pattern.matches thy o rpair t1)
  1687                   (Inttab.lookup_list ground_thm_table (hash_term t1)) then
  1688           do_term depth Ts t2
  1689         else
  1690           do_const depth Ts t x [t1, t2, t3]
  1691       | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
  1692       | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
  1693       | Const x $ t1 => do_const depth Ts t x [t1]
  1694       | Const x => do_const depth Ts t x []
  1695       | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
  1696       | Free _ => t
  1697       | Var _ => t
  1698       | Bound _ => t
  1699       | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
  1700     (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
  1701     and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
  1702         (Abs (Name.uu, body_type T,
  1703               select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
  1704       | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
  1705         (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
  1706     (* int -> typ list -> term -> styp -> term list -> term *)
  1707     and do_const depth Ts t (x as (s, T)) ts =
  1708       case AList.lookup (op =) ersatz_table s of
  1709         SOME s' =>
  1710         do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
  1711       | NONE =>
  1712         let
  1713           val (const, ts) =
  1714             if is_built_in_const thy stds fast_descrs x then
  1715               (Const x, ts)
  1716             else case AList.lookup (op =) case_names s of
  1717               SOME n =>
  1718               let
  1719                 val (dataT, res_T) = nth_range_type n T
  1720                                      |> pairf domain_type range_type
  1721               in
  1722                 (optimized_case_def hol_ctxt dataT res_T
  1723                  |> do_term (depth + 1) Ts, ts)
  1724               end
  1725             | _ =>
  1726               if is_constr thy stds x then
  1727                 (Const x, ts)
  1728               else if is_stale_constr thy x then
  1729                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
  1730                                      \(\"" ^ s ^ "\")")
  1731               else if is_quot_abs_fun ctxt x then
  1732                 let
  1733                   val rep_T = domain_type T
  1734                   val abs_T = range_type T
  1735                 in
  1736                   (Abs (Name.uu, rep_T,
  1737                         Const (@{const_name Quot}, rep_T --> abs_T)
  1738                                $ (Const (quot_normal_name_for_type ctxt abs_T,
  1739                                          rep_T --> rep_T) $ Bound 0)), ts)
  1740                 end
  1741               else if is_quot_rep_fun ctxt x then
  1742                 let
  1743                   val abs_T = domain_type T
  1744                   val rep_T = range_type T
  1745                   val x' = (@{const_name Quot}, rep_T --> abs_T)
  1746                 in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
  1747               else if is_record_get thy x then
  1748                 case length ts of
  1749                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
  1750                 | _ => (optimized_record_get hol_ctxt s (domain_type T)
  1751                             (range_type T) (do_term depth Ts (hd ts)), tl ts)
  1752               else if is_record_update thy x then
  1753                 case length ts of
  1754                   2 => (optimized_record_update hol_ctxt
  1755                             (unsuffix Record.updateN s) (nth_range_type 2 T)
  1756                             (do_term depth Ts (hd ts))
  1757                             (do_term depth Ts (nth ts 1)), [])
  1758                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
  1759               else if is_rep_fun thy x then
  1760                 let val x' = mate_of_rep_fun thy x in
  1761                   if is_constr thy stds x' then
  1762                     select_nth_constr_arg_with_args depth Ts x' ts 0
  1763                                                     (range_type T)
  1764                   else
  1765                     (Const x, ts)
  1766                 end
  1767               else if is_equational_fun hol_ctxt x orelse
  1768                       is_choice_spec_fun hol_ctxt x then
  1769                 (Const x, ts)
  1770               else case def_of_const thy def_table x of
  1771                 SOME def =>
  1772                 if depth > unfold_max_depth then
  1773                   raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
  1774                                    "too many nested definitions (" ^
  1775                                    string_of_int depth ^ ") while expanding " ^
  1776                                    quote s)
  1777                 else if s = @{const_name wfrec'} then
  1778                   (do_term (depth + 1) Ts (betapplys (def, ts)), [])
  1779                 else
  1780                   (do_term (depth + 1) Ts def, ts)
  1781               | NONE => (Const x, ts)
  1782         in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
  1783   in do_term 0 [] end
  1784 
  1785 (** Axiom extraction/generation **)
  1786 
  1787 (* term -> string * term *)
  1788 fun pair_for_prop t =
  1789   case term_under_def t of
  1790     Const (s, _) => (s, t)
  1791   | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
  1792 (* (Proof.context -> term list) -> Proof.context -> (term * term) list
  1793    -> const_table *)
  1794 fun def_table_for get ctxt subst =
  1795   ctxt |> get |> map (pair_for_prop o subst_atomic subst)
  1796        |> AList.group (op =) |> Symtab.make
  1797 (* term -> string * term *)
  1798 fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
  1799 (* Proof.context -> (term * term) list -> term list -> const_table *)
  1800 fun const_def_table ctxt subst ts =
  1801   def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
  1802   |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
  1803           (map pair_for_prop ts)
  1804 (* term list -> const_table *)
  1805 fun const_nondef_table ts =
  1806   fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
  1807 (* Proof.context -> (term * term) list -> const_table *)
  1808 val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
  1809 val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
  1810 fun const_choice_spec_table ctxt subst =
  1811   map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
  1812   |> const_nondef_table
  1813 (* Proof.context -> (term * term) list -> const_table -> const_table *)
  1814 fun inductive_intro_table ctxt subst def_table =
  1815   def_table_for
  1816       (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
  1817                                             def_table o prop_of)
  1818            o Nitpick_Intros.get) ctxt subst
  1819 (* theory -> term list Inttab.table *)
  1820 fun ground_theorem_table thy =
  1821   fold ((fn @{const Trueprop} $ t1 =>
  1822             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
  1823           | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
  1824 
  1825 (* TODO: Move to "Nitpick.thy" *)
  1826 val basic_ersatz_table =
  1827   [(@{const_name prod_case}, @{const_name split}),
  1828    (@{const_name card}, @{const_name card'}),
  1829    (@{const_name setsum}, @{const_name setsum'}),
  1830    (@{const_name fold_graph}, @{const_name fold_graph'}),
  1831    (@{const_name wf}, @{const_name wf'}),
  1832    (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
  1833    (@{const_name wfrec}, @{const_name wfrec'})]
  1834 
  1835 (* theory -> (string * string) list *)
  1836 fun ersatz_table thy =
  1837   fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
  1838 
  1839 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
  1840 fun add_simps simp_table s eqs =
  1841   Unsynchronized.change simp_table
  1842       (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
  1843 
  1844 (* theory -> styp -> term list *)
  1845 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
  1846   let val abs_T = domain_type T in
  1847     typedef_info thy (fst (dest_Type abs_T)) |> the
  1848     |> pairf #Abs_inverse #Rep_inverse
  1849     |> pairself (Refute.specialize_type thy x o prop_of o the)
  1850     ||> single |> op ::
  1851   end
  1852 (* theory -> string * typ list -> term list *)
  1853 fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
  1854   let val abs_T = Type abs_z in
  1855     if is_univ_typedef thy abs_T then
  1856       []
  1857     else case typedef_info thy abs_s of
  1858       SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
  1859       let
  1860         val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
  1861         val rep_t = Const (Rep_name, abs_T --> rep_T)
  1862         val set_t = Const (set_name, rep_T --> bool_T)
  1863         val set_t' =
  1864           prop_of_Rep |> HOLogic.dest_Trueprop
  1865                       |> Refute.specialize_type thy (dest_Const rep_t)
  1866                       |> HOLogic.dest_mem |> snd
  1867       in
  1868         [HOLogic.all_const abs_T
  1869          $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
  1870         |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
  1871         |> map HOLogic.mk_Trueprop
  1872       end
  1873     | NONE => []
  1874   end
  1875 (* Proof.context -> string * typ list -> term list *)
  1876 fun optimized_quot_type_axioms ctxt stds abs_z =
  1877   let
  1878     val thy = ProofContext.theory_of ctxt
  1879     val abs_T = Type abs_z
  1880     val rep_T = rep_type_for_quot_type thy abs_T
  1881     val equiv_rel = equiv_relation_for_quot_type thy abs_T
  1882     val a_var = Var (("a", 0), abs_T)
  1883     val x_var = Var (("x", 0), rep_T)
  1884     val y_var = Var (("y", 0), rep_T)
  1885     val x = (@{const_name Quot}, rep_T --> abs_T)
  1886     val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
  1887     val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
  1888     val normal_x = normal_t $ x_var
  1889     val normal_y = normal_t $ y_var
  1890     val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
  1891   in
  1892     [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
  1893      Logic.list_implies
  1894          ([@{const Not} $ (is_unknown_t $ normal_x),
  1895            @{const Not} $ (is_unknown_t $ normal_y),
  1896            equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
  1897            Logic.mk_equals (normal_x, normal_y)),
  1898      Logic.list_implies
  1899          ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)),
  1900            HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))],
  1901           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
  1902   end
  1903 
  1904 (* hol_context -> typ -> term list *)
  1905 fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
  1906   let
  1907     val xs = datatype_constrs hol_ctxt T
  1908     val set_T = T --> bool_T
  1909     val iter_T = @{typ bisim_iterator}
  1910     val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
  1911     val bisim_max = @{const bisim_iterator_max}
  1912     val n_var = Var (("n", 0), iter_T)
  1913     val n_var_minus_1 =
  1914       Const (@{const_name safe_The}, (iter_T --> bool_T) --> iter_T)
  1915       $ Abs ("m", iter_T, HOLogic.eq_const iter_T
  1916                           $ (suc_const iter_T $ Bound 0) $ n_var)
  1917     val x_var = Var (("x", 0), T)
  1918     val y_var = Var (("y", 0), T)
  1919     (* styp -> int -> typ -> term *)
  1920     fun nth_sub_bisim x n nth_T =
  1921       (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
  1922        else HOLogic.eq_const nth_T)
  1923       $ select_nth_constr_arg thy stds x x_var n nth_T
  1924       $ select_nth_constr_arg thy stds x y_var n nth_T
  1925     (* styp -> term *)
  1926     fun case_func (x as (_, T)) =
  1927       let
  1928         val arg_Ts = binder_types T
  1929         val core_t =
  1930           discriminate_value hol_ctxt x y_var ::
  1931           map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
  1932           |> foldr1 s_conj
  1933       in List.foldr absdummy core_t arg_Ts end
  1934   in
  1935     [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
  1936      $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
  1937         $ (betapplys (optimized_case_def hol_ctxt T bool_T,
  1938                       map case_func xs @ [x_var]))),
  1939      HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
  1940      $ (Const (@{const_name insert}, T --> set_T --> set_T)
  1941         $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
  1942     |> map HOLogic.mk_Trueprop
  1943   end
  1944 
  1945 exception NO_TRIPLE of unit
  1946 
  1947 (* theory -> styp -> term -> term list * term list * term *)
  1948 fun triple_for_intro_rule thy x t =
  1949   let
  1950     val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
  1951     val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
  1952     val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
  1953     (* term -> bool *)
  1954      val is_good_head = curry (op =) (Const x) o head_of
  1955   in
  1956     if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
  1957   end
  1958 
  1959 (* term -> term *)
  1960 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
  1961 
  1962 (* indexname * typ -> term list -> term -> term -> term *)
  1963 fun wf_constraint_for rel side concl main =
  1964   let
  1965     val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
  1966                                                 tuple_for_args concl), Var rel)
  1967     val t = List.foldl HOLogic.mk_imp core side
  1968     val vars = filter (not_equal rel) (Term.add_vars t [])
  1969   in
  1970     Library.foldl (fn (t', ((x, j), T)) =>
  1971                       HOLogic.all_const T
  1972                       $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
  1973                   (t, vars)
  1974   end
  1975 
  1976 (* indexname * typ -> term list * term list * term -> term *)
  1977 fun wf_constraint_for_triple rel (side, main, concl) =
  1978   map (wf_constraint_for rel side concl) main |> foldr1 s_conj
  1979 
  1980 (* Proof.context -> Time.time option -> thm
  1981    -> (Proof.context -> tactic -> tactic) -> bool *)
  1982 fun terminates_by ctxt timeout goal tac =
  1983   can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
  1984        #> SINGLE (DETERM_TIMEOUT timeout
  1985                                  (tac ctxt (auto_tac (clasimpset_of ctxt))))
  1986        #> the #> Goal.finish ctxt) goal
  1987 
  1988 val max_cached_wfs = 50
  1989 val cached_timeout =
  1990   Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
  1991 val cached_wf_props =
  1992   Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
  1993 
  1994 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
  1995                         ScnpReconstruct.sizechange_tac]
  1996 
  1997 (* hol_context -> const_table -> styp -> bool *)
  1998 fun uncached_is_well_founded_inductive_pred
  1999         ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
  2000          : hol_context) (x as (_, T)) =
  2001   case def_props_for_const thy stds fast_descrs intro_table x of
  2002     [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
  2003                       [Const x])
  2004   | intro_ts =>
  2005     (case map (triple_for_intro_rule thy x) intro_ts
  2006           |> filter_out (null o #2) of
  2007        [] => true
  2008      | triples =>
  2009        let
  2010          val binders_T = HOLogic.mk_tupleT (binder_types T)
  2011          val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
  2012          val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
  2013          val rel = (("R", j), rel_T)
  2014          val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
  2015                     map (wf_constraint_for_triple rel) triples
  2016                     |> foldr1 s_conj |> HOLogic.mk_Trueprop
  2017          val _ = if debug then
  2018                    priority ("Wellfoundedness goal: " ^
  2019                              Syntax.string_of_term ctxt prop ^ ".")
  2020                  else
  2021                    ()
  2022        in
  2023          if tac_timeout = Synchronized.value cached_timeout andalso
  2024             length (Synchronized.value cached_wf_props) < max_cached_wfs then
  2025            ()
  2026          else
  2027            (Synchronized.change cached_wf_props (K []);
  2028             Synchronized.change cached_timeout (K tac_timeout));
  2029          case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
  2030            SOME wf => wf
  2031          | NONE =>
  2032            let
  2033              val goal = prop |> cterm_of thy |> Goal.init
  2034              val wf = exists (terminates_by ctxt tac_timeout goal)
  2035                              termination_tacs
  2036            in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
  2037        end)
  2038     handle List.Empty => false | NO_TRIPLE () => false
  2039 
  2040 (* The type constraint below is a workaround for a Poly/ML crash. *)
  2041 
  2042 (* hol_context -> styp -> bool *)
  2043 fun is_well_founded_inductive_pred
  2044         (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
  2045         (x as (s, _)) =
  2046   case triple_lookup (const_match thy) wfs x of
  2047     SOME (SOME b) => b
  2048   | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
  2049          case AList.lookup (op =) (!wf_cache) x of
  2050            SOME (_, wf) => wf
  2051          | NONE =>
  2052            let
  2053              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
  2054              val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
  2055            in
  2056              Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
  2057            end
  2058 
  2059 (* typ list -> typ -> term -> term *)
  2060 fun ap_curry [_] _ t = t
  2061   | ap_curry arg_Ts tuple_T t =
  2062     let val n = length arg_Ts in
  2063       list_abs (map (pair "c") arg_Ts,
  2064                 incr_boundvars n t
  2065                 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
  2066     end
  2067 
  2068 (* int -> term -> int *)
  2069 fun num_occs_of_bound_in_term j (t1 $ t2) =
  2070     op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
  2071   | num_occs_of_bound_in_term j (Abs (_, _, t')) =
  2072     num_occs_of_bound_in_term (j + 1) t'
  2073   | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
  2074   | num_occs_of_bound_in_term _ _ = 0
  2075 
  2076 (* term -> bool *)
  2077 val is_linear_inductive_pred_def =
  2078   let
  2079     (* int -> term -> bool *)
  2080     fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
  2081         do_disjunct (j + 1) t2
  2082       | do_disjunct j t =
  2083         case num_occs_of_bound_in_term j t of
  2084           0 => true
  2085         | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
  2086         | _ => false
  2087     (* term -> bool *)
  2088     fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
  2089         let val (xs, body) = strip_abs t2 in
  2090           case length xs of
  2091             1 => false
  2092           | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
  2093         end
  2094       | do_lfp_def _ = false
  2095   in do_lfp_def o strip_abs_body end
  2096 
  2097 (* int -> int list list *)
  2098 fun n_ptuple_paths 0 = []
  2099   | n_ptuple_paths 1 = []
  2100   | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
  2101 (* int -> typ -> typ -> term -> term *)
  2102 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
  2103 
  2104 (* term -> term * term *)
  2105 val linear_pred_base_and_step_rhss =
  2106   let
  2107     (* term -> term *)
  2108     fun aux (Const (@{const_name lfp}, _) $ t2) =
  2109         let
  2110           val (xs, body) = strip_abs t2
  2111           val arg_Ts = map snd (tl xs)
  2112           val tuple_T = HOLogic.mk_tupleT arg_Ts
  2113           val j = length arg_Ts
  2114           (* int -> term -> term *)
  2115           fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
  2116               Const (@{const_name Ex}, T1)
  2117               $ Abs (s2, T2, repair_rec (j + 1) t2')
  2118             | repair_rec j (@{const "op &"} $ t1 $ t2) =
  2119               @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
  2120             | repair_rec j t =
  2121               let val (head, args) = strip_comb t in
  2122                 if head = Bound j then
  2123                   HOLogic.eq_const tuple_T $ Bound j
  2124                   $ mk_flat_tuple tuple_T args
  2125                 else
  2126                   t
  2127               end
  2128           val (nonrecs, recs) =
  2129             List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
  2130                            (disjuncts_of body)
  2131           val base_body = nonrecs |> List.foldl s_disj @{const False}
  2132           val step_body = recs |> map (repair_rec j)
  2133                                |> List.foldl s_disj @{const False} 
  2134         in
  2135           (list_abs (tl xs, incr_bv (~1, j, base_body))
  2136            |> ap_n_split (length arg_Ts) tuple_T bool_T,
  2137            Abs ("y", tuple_T, list_abs (tl xs, step_body)
  2138                               |> ap_n_split (length arg_Ts) tuple_T bool_T))
  2139         end
  2140       | aux t =
  2141         raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
  2142   in aux end
  2143 
  2144 (* hol_context -> styp -> term -> term *)
  2145 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
  2146   let
  2147     val j = maxidx_of_term def + 1
  2148     val (outer, fp_app) = strip_abs def
  2149     val outer_bounds = map Bound (length outer - 1 downto 0)
  2150     val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
  2151     val fp_app = subst_bounds (rev outer_vars, fp_app)
  2152     val (outer_Ts, rest_T) = strip_n_binders (length outer) T
  2153     val tuple_arg_Ts = strip_type rest_T |> fst
  2154     val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  2155     val set_T = tuple_T --> bool_T
  2156     val curried_T = tuple_T --> set_T
  2157     val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
  2158     val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
  2159     val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
  2160     val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
  2161                   |> HOLogic.mk_Trueprop
  2162     val _ = add_simps simp_table base_s [base_eq]
  2163     val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
  2164     val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
  2165                   |> HOLogic.mk_Trueprop
  2166     val _ = add_simps simp_table step_s [step_eq]
  2167   in
  2168     list_abs (outer,
  2169               Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
  2170               $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
  2171                  $ (Const (@{const_name split}, curried_T --> uncurried_T)
  2172                     $ list_comb (Const step_x, outer_bounds)))
  2173               $ list_comb (Const base_x, outer_bounds)
  2174               |> ap_curry tuple_arg_Ts tuple_T)
  2175     |> unfold_defs_in_term hol_ctxt
  2176   end
  2177 
  2178 (* hol_context -> bool -> styp -> term *)
  2179 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
  2180                                                 def_table, simp_table, ...})
  2181                                   gfp (x as (s, T)) =
  2182   let
  2183     val iter_T = iterator_type_for_const gfp x
  2184     val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
  2185     val unrolled_const = Const x' $ zero_const iter_T
  2186     val def = the (def_of_const thy def_table x)
  2187   in
  2188     if is_equational_fun hol_ctxt x' then
  2189       unrolled_const (* already done *)
  2190     else if not gfp andalso is_linear_inductive_pred_def def andalso
  2191          star_linear_preds then
  2192       starred_linear_pred_const hol_ctxt x def
  2193     else
  2194       let
  2195         val j = maxidx_of_term def + 1
  2196         val (outer, fp_app) = strip_abs def
  2197         val outer_bounds = map Bound (length outer - 1 downto 0)
  2198         val cur = Var ((iter_var_prefix, j + 1), iter_T)
  2199         val next = suc_const iter_T $ cur
  2200         val rhs = case fp_app of
  2201                     Const _ $ t =>
  2202                     betapply (t, list_comb (Const x', next :: outer_bounds))
  2203                   | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
  2204                                      \const", [fp_app])
  2205         val (inner, naked_rhs) = strip_abs rhs
  2206         val all = outer @ inner
  2207         val bounds = map Bound (length all - 1 downto 0)
  2208         val vars = map (fn (s, T) => Var ((s, j), T)) all
  2209         val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
  2210                  |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  2211         val _ = add_simps simp_table s' [eq]
  2212       in unrolled_const end
  2213   end
  2214 
  2215 (* hol_context -> styp -> term *)
  2216 fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
  2217   let
  2218     val def = the (def_of_const thy def_table x)
  2219     val (outer, fp_app) = strip_abs def
  2220     val outer_bounds = map Bound (length outer - 1 downto 0)
  2221     val rhs = case fp_app of
  2222                 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
  2223               | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
  2224                                  [fp_app])
  2225     val (inner, naked_rhs) = strip_abs rhs
  2226     val all = outer @ inner
  2227     val bounds = map Bound (length all - 1 downto 0)
  2228     val j = maxidx_of_term def + 1
  2229     val vars = map (fn (s, T) => Var ((s, j), T)) all
  2230   in
  2231     HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
  2232     |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  2233   end
  2234 fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
  2235   if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
  2236     let val x' = (strip_first_name_sep s |> snd, T) in
  2237       raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
  2238     end
  2239   else
  2240     raw_inductive_pred_axiom hol_ctxt x
  2241 
  2242 (* hol_context -> styp -> term list *)
  2243 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
  2244                                             psimp_table, ...}) x =
  2245   case def_props_for_const thy stds fast_descrs (!simp_table) x of
  2246     [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
  2247              [] => [inductive_pred_axiom hol_ctxt x]
  2248            | psimps => psimps)
  2249   | simps => simps
  2250 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
  2251 (* hol_context -> styp -> bool *)
  2252 fun is_equational_fun_surely_complete hol_ctxt x =
  2253   case raw_equational_fun_axioms hol_ctxt x of
  2254     [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
  2255     strip_comb t1 |> snd |> forall is_Var
  2256   | _ => false
  2257 
  2258 (** Type preprocessing **)
  2259 
  2260 (* term list -> term list *)
  2261 fun merge_type_vars_in_terms ts =
  2262   let
  2263     (* typ -> (sort * string) list -> (sort * string) list *)
  2264     fun add_type (TFree (s, S)) table =
  2265         (case AList.lookup (op =) table S of
  2266            SOME s' =>
  2267            if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
  2268            else table
  2269          | NONE => (S, s) :: table)
  2270       | add_type _ table = table
  2271     val table = fold (fold_types (fold_atyps add_type)) ts []
  2272     (* typ -> typ *)
  2273     fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
  2274       | coalesce T = T
  2275   in map (map_types (map_atyps coalesce)) ts end
  2276 
  2277 (* hol_context -> bool -> typ -> typ list -> typ list *)
  2278 fun add_ground_types hol_ctxt binarize =
  2279   let
  2280     fun aux T accum =
  2281       case T of
  2282         Type (@{type_name fun}, Ts) => fold aux Ts accum
  2283       | Type (@{type_name "*"}, Ts) => fold aux Ts accum
  2284       | Type (@{type_name itself}, [T1]) => aux T1 accum
  2285       | Type (_, Ts) =>
  2286         if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
  2287                   T then
  2288           accum
  2289         else
  2290           T :: accum
  2291           |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
  2292                                                                  binarize T of
  2293                          [] => Ts
  2294                        | xs => map snd xs)
  2295       | _ => insert (op =) T accum
  2296   in aux end
  2297 
  2298 (* hol_context -> bool -> typ -> typ list *)
  2299 fun ground_types_in_type hol_ctxt binarize T =
  2300   add_ground_types hol_ctxt binarize T []
  2301 (* hol_context -> term list -> typ list *)
  2302 fun ground_types_in_terms hol_ctxt binarize ts =
  2303   fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
  2304 
  2305 end;