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