Quelle nitpick_hol.ML Sprache: SML

(*  Title:      HOL/Tools/Nitpick/nitpick_hol.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2008, 2009, 2010

Auxiliary HOL-related functions used by Nitpick.
*)

signature NITPICK_HOL =
sig
  type const_table = term list Symtab.table
  type special_fun = ((string * typ) * int list * term list) * (string * typ)
  type unrolled = (string * typ) * (string * typ)
  type wf_cache = ((string * typ) * (bool * bool)) list

  type hol_context =
    {thy: theory,
     ctxt: Proof.context,
     max_bisim_depth: int,
     boxes: (typ option * bool option) list,
     wfs: ((string * typ) option * bool option) list,
     user_axioms: bool option,
     debug: bool,
     whacks: term list,
     binary_ints: bool option,
     destroy_constrs: bool,
     specialize: bool,
     star_linear_preds: bool,
     total_consts: bool option,
     needs: term list option,
     tac_timeout: Time.time,
     evals: term list,
     case_names: (string * int) list,
     def_tables: const_table * const_table,
     nondef_table: const_table,
     nondefs: term list,
     simp_table: const_table Unsynchronized.ref,
     psimp_table: const_table,
     choice_spec_table: const_table,
     intro_table: const_table,
     ground_thm_table: term list Inttab.table,
     ersatz_table: (string * string) list,
     skolems: (string * string list) list Unsynchronized.ref,
     special_funs: special_fun list Unsynchronized.ref,
     unrolled_preds: unrolled list Unsynchronized.ref,
     wf_cache: wf_cache Unsynchronized.ref,
     constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}

  datatype fixpoint_kind = Lfp | Gfp | NoFp
  datatype boxability =
    InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2

  val name_sep : string
  val numeral_prefix : string
  val base_prefix : string
  val step_prefix : string
  val unrolled_prefix : string
  val ubfp_prefix : string
  val lbfp_prefix : string
  val quot_normal_prefix : string
  val skolem_prefix : string
  val special_prefix : string
  val uncurry_prefix : string
  val eval_prefix : string
  val iter_var_prefix : string
  val strip_first_name_sep : string -> string * string
  val original_name : string -> string
  val abs_var : indexname * typ -> term -> term
  val s_conj : term * term -> term
  val s_disj : term * term -> term
  val strip_any_connective : term -> term list * term
  val conjuncts_of : term -> term list
  val disjuncts_of : term -> term list
  val unarize_unbox_etc_type : typ -> typ
  val uniterize_unarize_unbox_etc_type : typ -> typ
  val string_for_type : Proof.context -> typ -> string
  val pretty_for_type : Proof.context -> typ -> Pretty.T
  val prefix_name : string -> string -> string
  val shortest_name : string -> string
  val short_name : string -> string
  val shorten_names_in_term : term -> term
  val strict_type_match : theory -> typ * typ -> bool
  val type_match : theory -> typ * typ -> bool
  val const_match : theory -> (string * typ) * (string * typ) -> bool
  val term_match : theory -> term * term -> bool
  val frac_from_term_pair : typ -> term -> term -> term
  val is_fun_type : typ -> bool
  val is_set_type : typ -> bool
  val is_fun_or_set_type : typ -> bool
  val is_set_like_type : typ -> bool
  val is_pair_type : typ -> bool
  val is_lfp_iterator_type : typ -> bool
  val is_gfp_iterator_type : typ -> bool
  val is_fp_iterator_type : typ -> bool
  val is_iterator_type : typ -> bool
  val is_boolean_type : typ -> bool
  val is_integer_type : typ -> bool
  val is_bit_type : typ -> bool
  val is_word_type : typ -> bool
  val is_integer_like_type : typ -> bool
  val is_number_type : Proof.context -> typ -> bool
  val is_higher_order_type : typ -> bool
  val elem_type : typ -> typ
  val pseudo_domain_type : typ -> typ
  val pseudo_range_type : typ -> typ
  val const_for_iterator_type : typ -> string * typ
  val strip_n_binders : int -> typ -> typ list * typ
  val nth_range_type : int -> typ -> typ
  val num_factors_in_type : typ -> int
  val curried_binder_types : typ -> typ list
  val mk_flat_tuple : typ -> term list -> term
  val dest_n_tuple : int -> term -> term list
  val is_codatatype : Proof.context -> typ -> bool
  val is_quot_type : Proof.context -> typ -> bool
  val is_pure_typedef : Proof.context -> typ -> bool
  val is_univ_typedef : Proof.context -> typ -> bool
  val is_data_type : Proof.context -> typ -> bool
  val is_record_get : theory -> string * typ -> bool
  val is_record_update : theory -> string * typ -> bool
  val is_abs_fun : Proof.context -> string * typ -> bool
  val is_rep_fun : Proof.context -> string * typ -> bool
  val is_quot_abs_fun : Proof.context -> string * typ -> bool
  val is_quot_rep_fun : Proof.context -> string * typ -> bool
  val mate_of_rep_fun : Proof.context -> string * typ -> string * typ
  val is_nonfree_constr : Proof.context -> string * typ -> bool
  val is_free_constr : Proof.context -> string * typ -> bool
  val is_constr : Proof.context -> string * typ -> bool
  val is_sel : string -> bool
  val is_sel_like_and_no_discr : string -> bool
  val box_type : hol_context -> boxability -> typ -> typ
  val binarize_nat_and_int_in_type : typ -> typ
  val binarize_nat_and_int_in_term : term -> term
  val discr_for_constr : string * typ -> string * typ
  val num_sels_for_constr_type : typ -> int
  val nth_sel_name_for_constr_name : string -> int -> string
  val nth_sel_for_constr : string * typ -> int -> string * typ
  val binarized_and_boxed_nth_sel_for_constr :
    hol_context -> bool -> string * typ -> int -> string * typ
  val sel_no_from_name : string -> int
  val close_form : term -> term
  val distinctness_formula : typ -> term list -> term
  val register_frac_type :
    string -> (string * string) list -> morphism -> Context.generic
    -> Context.generic
  val register_frac_type_global :
    string -> (string * string) list -> theory -> theory
  val unregister_frac_type :
    string -> morphism -> Context.generic -> Context.generic
  val unregister_frac_type_global : string -> theory -> theory
  val register_ersatz :
    (string * string) list -> morphism -> Context.generic -> Context.generic
  val register_ersatz_global : (string * string) list -> theory -> theory
  val register_codatatype :
    typ -> string -> (string * typ) list -> morphism -> Context.generic ->
    Context.generic
  val register_codatatype_global :
    typ -> string -> (string * typ) list -> theory -> theory
  val unregister_codatatype :
    typ -> morphism -> Context.generic -> Context.generic
  val unregister_codatatype_global : typ -> theory -> theory
  val binarized_and_boxed_data_type_constrs :
    hol_context -> bool -> typ -> (string * typ) list
  val constr_name_for_sel_like : string -> string
  val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
    string * typ -> string * typ
  val card_of_type : (typ * int) list -> typ -> int
  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
  val bounded_exact_card_of_type :
    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
  val typical_card_of_type : typ -> int
  val is_finite_type : hol_context -> typ -> bool
  val is_special_eligible_arg : bool -> typ list -> term -> bool
  val s_let :
    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
  val s_betapply : typ list -> term * term -> term
  val s_betapplys : typ list -> term * term list -> term
  val discriminate_value : hol_context -> string * typ -> term -> term
  val select_nth_constr_arg :
    Proof.context -> string * typ -> term -> int -> typ -> term
  val construct_value : Proof.context -> string * typ -> term list -> term
  val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
  val special_bounds : term list -> (indexname * typ) list
  val is_funky_typedef : Proof.context -> typ -> bool
  val all_defs_of : theory -> (term * term) list -> term list
  val all_nondefs_of : Proof.context -> (term * term) list -> term list
  val arity_of_built_in_const : string * typ -> int option
  val is_built_in_const : string * typ -> bool
  val term_under_def : term -> term
  val case_const_names : Proof.context -> (string * int) list
  val unfold_defs_in_term : hol_context -> term -> term
  val const_def_tables :
    Proof.context -> (term * term) list -> term list
    -> const_table * const_table
  val const_nondef_table : term list -> const_table
  val const_simp_table : Proof.context -> (term * term) list -> const_table
  val const_psimp_table : Proof.context -> (term * term) list -> const_table
  val const_choice_spec_table :
    Proof.context -> (term * term) list -> const_table
  val inductive_intro_table :
    Proof.context -> (term * term) list -> const_table * const_table
    -> const_table
  val ground_theorem_table : theory -> term list Inttab.table
  val ersatz_table : Proof.context -> (string * string) list
  val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
  val inverse_axioms_for_rep_fun : Proof.context -> string * typ -> term list
  val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
  val optimized_quot_type_axioms :
    Proof.context -> string * typ list -> term list
  val def_of_const : theory -> const_table * const_table -> string * typ ->
    term option
  val fixpoint_kind_of_rhs : term -> fixpoint_kind
  val fixpoint_kind_of_const :
    theory -> const_table * const_table -> string * typ -> fixpoint_kind
  val is_raw_inductive_pred : hol_context -> string * typ -> bool
  val is_constr_pattern : Proof.context -> term -> bool
  val is_constr_pattern_lhs : Proof.context -> term -> bool
  val is_constr_pattern_formula : Proof.context -> term -> bool
  val nondef_props_for_const :
    theory -> bool -> const_table -> string * typ -> term list
  val is_choice_spec_fun : hol_context -> string * typ -> bool
  val is_choice_spec_axiom : Proof.context -> const_table -> term -> bool
  val is_raw_equational_fun : hol_context -> string * typ -> bool
  val is_equational_fun : hol_context -> string * typ -> bool
  val codatatype_bisim_axioms : hol_context -> typ -> term list
  val is_well_founded_inductive_pred : hol_context -> string * typ -> bool
  val unrolled_inductive_pred_const : hol_context -> bool -> string * typ ->
    term
  val equational_fun_axioms : hol_context -> string * typ -> term list
  val is_equational_fun_surely_complete : hol_context -> string * typ -> bool
  val merged_type_var_table_for_terms :
    theory -> term list -> (sort * string) list
  val merge_type_vars_in_term :
    theory -> bool -> (sort * string) list -> term -> term
  val ground_types_in_type : hol_context -> bool -> typ -> typ list
  val ground_types_in_terms : hol_context -> bool -> term list -> typ list
end;

structure Nitpick_HOL : NITPICK_HOL =
struct

open Nitpick_Util

type const_table = term list Symtab.table
type special_fun = ((string * typ) * int list * term list) * (string * typ)
type unrolled = (string * typ) * (string * typ)
type wf_cache = ((string * typ) * (bool * bool)) list

type hol_context =
  {thy: theory,
   ctxt: Proof.context,
   max_bisim_depth: int,
   boxes: (typ option * bool option) list,
   wfs: ((string * typ) option * bool option) list,
   user_axioms: bool option,
   debug: bool,
   whacks: term list,
   binary_ints: bool option,
   destroy_constrs: bool,
   specialize: bool,
   star_linear_preds: bool,
   total_consts: bool option,
   needs: term list option,
   tac_timeout: Time.time,
   evals: term list,
   case_names: (string * int) list,
   def_tables: const_table * const_table,
   nondef_table: const_table,
   nondefs: term list,
   simp_table: const_table Unsynchronized.ref,
   psimp_table: const_table,
   choice_spec_table: const_table,
   intro_table: const_table,
   ground_thm_table: term list Inttab.table,
   ersatz_table: (string * string) list,
   skolems: (string * string list) list Unsynchronized.ref,
   special_funs: special_fun list Unsynchronized.ref,
   unrolled_preds: unrolled list Unsynchronized.ref,
   wf_cache: wf_cache Unsynchronized.ref,
   constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}

datatype fixpoint_kind = Lfp | Gfp | NoFp
datatype boxability =
  InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2

(* FIXME: Get rid of 'codatatypes' and related functionality *)
structure Data = Generic_Data
(
  type T = {frac_types: (string * (string * string) list) list,
            ersatz_table: (string * string) list,
            codatatypes: (string * (string * (string * typ) list)) list}
  val empty = {frac_types = [], ersatz_table = [], codatatypes = []}
  fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1},
             {frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T =
    {frac_types = AList.merge (op =) (K true) (fs1, fs2),
     ersatz_table = AList.merge (op =) (K true) (et1, et2),
     codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
)

val name_sep = "$"
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
val sel_prefix = nitpick_prefix ^ "sel"
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
val base_prefix = nitpick_prefix ^ "base" ^ name_sep
val step_prefix = nitpick_prefix ^ "step" ^ name_sep
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
val skolem_prefix = nitpick_prefix ^ "sk"
val special_prefix = nitpick_prefix ^ "sp"
val uncurry_prefix = nitpick_prefix ^ "unc"
val eval_prefix = nitpick_prefix ^ "eval"
val iter_var_prefix = "i"

(** Constant/type information and term/type manipulation **)

fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep

fun quot_normal_name_for_type ctxt T =
  quot_normal_prefix ^ Pretty.pure_string_of (Syntax.pretty_typ ctxt T)

val strip_first_name_sep =
  Substring.full #> Substring.position name_sep ##> Substring.triml 1
  #> apply2 Substring.string

fun original_name s =
  if String.isPrefix nitpick_prefix s then
    case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
  else
    s

fun s_conj (t1, \<^Const_>\<open>True\<close>) = t1
  | s_conj (\<^Const_>\<open>True\<close>, t2) = t2
  | s_conj (t1, t2) =
    if t1 = \<^Const>\<open>False\<close> orelse t2 = \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
    else HOLogic.mk_conj (t1, t2)

fun s_disj (t1, \<^Const_>\<open>False\<close>) = t1
  | s_disj (\<^Const_>\<open>False\<close>, t2) = t2
  | s_disj (t1, t2) =
    if t1 = \<^Const>\<open>True\<close> orelse t2 = \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
    else HOLogic.mk_disj (t1, t2)

fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
    if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
  | strip_connective _ t = [t]

fun strip_any_connective (t as (t0 $ _ $ _)) =
    if t0 = \<^Const>\<open>conj\<close> orelse t0 = \<^Const>\<open>disj\<close> then
      (strip_connective t0 t, t0)
    else
      ([t], \<^Const>\<open>Not\<close>)
  | strip_any_connective t = ([t], \<^Const>\<open>Not\<close>)
val conjuncts_of = strip_connective \<^Const>\<open>conj\<close>
val disjuncts_of = strip_connective \<^Const>\<open>disj\<close>

(* When you add constants to these lists, make sure to handle them in
   "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   well. *)
val built_in_consts =
  [(\<^const_name>\<open>Pure.all\<close>, 1),
   (\<^const_name>\<open>Pure.eq\<close>, 2),
   (\<^const_name>\<open>Pure.imp\<close>, 2),
   (\<^const_name>\<open>Pure.conjunction\<close>, 2),
   (\<^const_name>\<open>Trueprop\<close>, 1),
   (\<^const_name>\<open>Not\<close>, 1),
   (\<^const_name>\<open>False\<close>, 0),
   (\<^const_name>\<open>True\<close>, 0),
   (\<^const_name>\<open>All\<close>, 1),
   (\<^const_name>\<open>Ex\<close>, 1),
   (\<^const_name>\<open>HOL.eq\<close>, 1),
   (\<^const_name>\<open>HOL.conj\<close>, 2),
   (\<^const_name>\<open>HOL.disj\<close>, 2),
   (\<^const_name>\<open>HOL.implies\<close>, 2),
   (\<^const_name>\<open>If\<close>, 3),
   (\<^const_name>\<open>Let\<close>, 2),
   (\<^const_name>\<open>Pair\<close>, 2),
   (\<^const_name>\<open>fst\<close>, 1),
   (\<^const_name>\<open>snd\<close>, 1),
   (\<^const_name>\<open>Set.member\<close>, 2),
   (\<^const_name>\<open>Collect\<close>, 1),
   (\<^const_name>\<open>Id\<close>, 0),
   (\<^const_name>\<open>converse\<close>, 1),
   (\<^const_name>\<open>trancl\<close>, 1),
   (\<^const_name>\<open>relcomp\<close>, 2),
   (\<^const_name>\<open>finite\<close>, 1),
   (\<^const_name>\<open>unknown\<close>, 0),
   (\<^const_name>\<open>is_unknown\<close>, 1),
   (\<^const_name>\<open>safe_The\<close>, 1),
   (\<^const_name>\<open>Frac\<close>, 0),
   (\<^const_name>\<open>norm_frac\<close>, 0),
   (\<^const_name>\<open>Suc\<close>, 0),
   (\<^const_name>\<open>nat\<close>, 0),
   (\<^const_name>\<open>nat_gcd\<close>, 0),
   (\<^const_name>\<open>nat_lcm\<close>, 0)]
val built_in_typed_consts =
  [((\<^const_name>\<open>zero_class.zero\<close>, nat_T), 0),
   ((\<^const_name>\<open>one_class.one\<close>, nat_T), 0),
   ((\<^const_name>\<open>plus_class.plus\<close>, nat_T --> nat_T --> nat_T), 0),
   ((\<^const_name>\<open>minus_class.minus\<close>, nat_T --> nat_T --> nat_T), 0),
   ((\<^const_name>\<open>times_class.times\<close>, nat_T --> nat_T --> nat_T), 0),
   ((\<^const_name>\<open>Rings.divide\<close>, nat_T --> nat_T --> nat_T), 0),
   ((\<^const_name>\<open>ord_class.less\<close>, nat_T --> nat_T --> bool_T), 2),
   ((\<^const_name>\<open>ord_class.less_eq\<close>, nat_T --> nat_T --> bool_T), 2),
   ((\<^const_name>\<open>of_nat\<close>, nat_T --> int_T), 0),
   ((\<^const_name>\<open>zero_class.zero\<close>, int_T), 0),
   ((\<^const_name>\<open>one_class.one\<close>, int_T), 0),
   ((\<^const_name>\<open>plus_class.plus\<close>, int_T --> int_T --> int_T), 0),
   ((\<^const_name>\<open>minus_class.minus\<close>, int_T --> int_T --> int_T), 0),
   ((\<^const_name>\<open>times_class.times\<close>, int_T --> int_T --> int_T), 0),
   ((\<^const_name>\<open>Rings.divide\<close>, int_T --> int_T --> int_T), 0),
   ((\<^const_name>\<open>uminus_class.uminus\<close>, int_T --> int_T), 0),
   ((\<^const_name>\<open>ord_class.less\<close>, int_T --> int_T --> bool_T), 2),
   ((\<^const_name>\<open>ord_class.less_eq\<close>, int_T --> int_T --> bool_T), 2)]

fun unarize_type \<^typ>\<open>unsigned_bit word\<close> = nat_T
  | unarize_type \<^typ>\<open>signed_bit word\<close> = int_T
  | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
  | unarize_type T = T

fun unarize_unbox_etc_type (Type (\<^type_name>\<open>fun_box\<close>, Ts)) =
    unarize_unbox_etc_type (Type (\<^type_name>\<open>fun\<close>, Ts))
  | unarize_unbox_etc_type (Type (\<^type_name>\<open>pair_box\<close>, Ts)) =
    Type (\<^type_name>\<open>prod\<close>, map unarize_unbox_etc_type Ts)
  | unarize_unbox_etc_type \<^typ>\<open>unsigned_bit word\<close> = nat_T
  | unarize_unbox_etc_type \<^typ>\<open>signed_bit word\<close> = int_T
  | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
    Type (s, map unarize_unbox_etc_type Ts)
  | unarize_unbox_etc_type T = T

fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
  | uniterize_type \<^typ>\<open>bisim_iterator\<close> = nat_T
  | uniterize_type T = T
val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type

fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type

val prefix_name = Long_Name.qualify o Long_Name.base_name
val shortest_name = Long_Name.base_name
val prefix_abs_vars = Term.map_abs_vars o prefix_name

fun short_name s =
  case space_explode name_sep s of
    [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
  | ss => map shortest_name ss |> space_implode "_"

fun shorten_names_in_type (Type (s, Ts)) =
    Type (short_name s, map shorten_names_in_type Ts)
  | shorten_names_in_type T = T

val shorten_names_in_term =
  map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
  #> map_types shorten_names_in_type

fun strict_type_match thy (T1, T2) =
  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
  handle Type.TYPE_MATCH => false

fun type_match thy = strict_type_match thy o apply2 unarize_unbox_etc_type

fun const_match thy ((s1, T1), (s2, T2)) =
  s1 = s2 andalso type_match thy (T1, T2)

fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
  | term_match thy (Free (s1, T1), Free (s2, T2)) =
    const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
  | term_match _ (t1, t2) = t1 aconv t2

fun frac_from_term_pair T t1 t2 =
  case snd (HOLogic.dest_number t1) of
    0 => HOLogic.mk_number T 0
  | n1 => case snd (HOLogic.dest_number t2) of
            1 => HOLogic.mk_number T n1
          | n2 => Const (\<^const_name>\<open>divide\<close>, T --> T --> T)
                  $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2

fun is_fun_type (Type (\<^type_name>\<open>fun\<close>, _)) = true
  | is_fun_type _ = false

fun is_set_type (Type (\<^type_name>\<open>set\<close>, _)) = true
  | is_set_type _ = false

val is_fun_or_set_type = is_fun_type orf is_set_type

fun is_set_like_type (Type (\<^type_name>\<open>fun\<close>, [_, T'])) =
    (body_type T' = bool_T)
  | is_set_like_type (Type (\<^type_name>\<open>set\<close>, _)) = true
  | is_set_like_type _ = false

fun is_pair_type (Type (\<^type_name>\<open>prod\<close>, _)) = true
  | is_pair_type _ = false

fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
  | is_lfp_iterator_type _ = false

fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
  | is_gfp_iterator_type _ = false

val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type

fun is_iterator_type T =
  (T = \<^typ>\<open>bisim_iterator\<close> orelse is_fp_iterator_type T)

fun is_boolean_type T = (T = prop_T orelse T = bool_T)

fun is_integer_type T = (T = nat_T orelse T = int_T)

fun is_bit_type T = (T = \<^typ>\<open>unsigned_bit\<close> orelse T = \<^typ>\<open>signed_bit\<close>)

fun is_word_type (Type (\<^type_name>\<open>word\<close>, _)) = true
  | is_word_type _ = false

val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type

fun is_frac_type ctxt (Type (s, [])) =
    s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt)))
  | is_frac_type _ _ = false

fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt

fun is_higher_order_type (Type (\<^type_name>\<open>fun\<close>, _)) = true
  | is_higher_order_type (Type (\<^type_name>\<open>set\<close>, _)) = true
  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
  | is_higher_order_type _ = false

fun elem_type (Type (\<^type_name>\<open>set\<close>, [T'])) = T'
  | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])

fun pseudo_domain_type (Type (\<^type_name>\<open>fun\<close>, [T1, _])) = T1
  | pseudo_domain_type T = elem_type T

fun pseudo_range_type (Type (\<^type_name>\<open>fun\<close>, [_, T2])) = T2
  | pseudo_range_type (Type (\<^type_name>\<open>set\<close>, _)) = bool_T
  | pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], [])

fun iterator_type_for_const gfp (s, T) =
  Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
        binder_types T)

fun const_for_iterator_type (Type (s, Ts)) =
    (strip_first_name_sep s |> snd, Ts ---> bool_T)
  | const_for_iterator_type T =
    raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])

fun strip_n_binders 0 T = ([], T)
  | strip_n_binders n (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
    strip_n_binders (n - 1) T2 |>> cons T1
  | strip_n_binders n (Type (\<^type_name>\<open>fun_box\<close>, Ts)) =
    strip_n_binders n (Type (\<^type_name>\<open>fun\<close>, Ts))
  | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])

val nth_range_type = snd oo strip_n_binders

fun num_factors_in_type (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) =
    fold (Integer.add o num_factors_in_type) [T1, T2] 0
  | num_factors_in_type _ = 1

val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types

fun maybe_curried_binder_types T =
  (if is_pair_type (body_type T) then binder_types else curried_binder_types) T

fun mk_flat_tuple _ [t] = t
  | mk_flat_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) (t :: ts) =
    HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
  | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)

fun dest_n_tuple 1 t = [t]
  | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::

fun typedef_info ctxt s =
  if is_frac_type ctxt (Type (s, [])) then
    SOME {abs_type = Type (s, []), rep_type = \<^typ>\<open>int * int\<close>,
          Abs_name = \<^const_name>\<open>Abs_Frac\<close>,
          Rep_name = \<^const_name>\<open>Rep_Frac\<close>,
          prop_of_Rep = \<^prop>\<open>Rep_Frac x \<in> Collect Frac\<close>
                        |> Logic.varify_global,
          Abs_inverse = NONE, Rep_inverse = NONE}
  else case Typedef.get_info ctxt s of
    (* When several entries are returned, it shouldn't matter much which one
       we take (according to Florian Haftmann). *)
    (* The "Logic.varifyT_global" calls are a temporary hack because these
       types's type variables sometimes clash with locally fixed type variables.
       Remove these calls once "Typedef" is fully localized. *)
    ({abs_type, rep_type, Abs_name, Rep_name, ...},
     {Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
    SOME {abs_type = Logic.varifyT_global abs_type,
          rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
          Rep_name = Rep_name, prop_of_Rep = Thm.prop_of Rep,
          Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse}
  | _ => NONE

val is_raw_typedef = is_some oo typedef_info
val is_raw_free_datatype = is_some oo Ctr_Sugar.ctr_sugar_of

val is_interpreted_type =
  member (op =) [\<^type_name>\<open>prod\<close>, \<^type_name>\<open>set\<close>, \<^type_name>\<open>bool\<close>,
                 \<^type_name>\<open>nat\<close>, \<^type_name>\<open>int\<close>, \<^type_name>\<open>natural\<close>,
                 \<^type_name>\<open>integer\<close>]

fun repair_constr_type (Type (_, Ts)) T =
  dest_Const_type (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T)))

fun register_frac_type_generic frac_s ersaetze generic =
  let
    val {frac_types, ersatz_table, codatatypes} = Data.get generic
    val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
               codatatypes = codatatypes} generic end

(* TODO: Consider morphism. *)
fun register_frac_type frac_s ersaetze (_ : morphism) =
  register_frac_type_generic frac_s ersaetze

val register_frac_type_global = Context.theory_map oo register_frac_type_generic

fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
(* TODO: Consider morphism. *)

fun unregister_frac_type frac_s (_ : morphism) =
  unregister_frac_type_generic frac_s

val unregister_frac_type_global =
  Context.theory_map o unregister_frac_type_generic

fun register_ersatz_generic ersatz generic =
  let
    val {frac_types, ersatz_table, codatatypes} = Data.get generic
    val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz)
  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
               codatatypes = codatatypes} generic end

(* TODO: Consider morphism. *)
fun register_ersatz ersatz (_ : morphism) =
  register_ersatz_generic ersatz

val register_ersatz_global = Context.theory_map o register_ersatz_generic

fun register_codatatype_generic coT case_name constr_xs generic =
  let
    val {frac_types, ersatz_table, codatatypes} = Data.get generic
    val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs
    val (co_s, coTs) = dest_Type coT
    val _ =
      if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
         co_s <> \<^type_name>\<open>fun\<close> andalso not (is_interpreted_type co_s) then
        ()
      else
        raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
    val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
                                   codatatypes
  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
               codatatypes = codatatypes} generic end

(* TODO: Consider morphism. *)
fun register_codatatype coT case_name constr_xs (_ : morphism) =
  register_codatatype_generic coT case_name constr_xs

val register_codatatype_global =
  Context.theory_map ooo register_codatatype_generic

fun unregister_codatatype_generic coT = register_codatatype_generic coT "" []
(* TODO: Consider morphism. *)

fun unregister_codatatype coT (_ : morphism) =
  unregister_codatatype_generic coT
val unregister_codatatype_global =
  Context.theory_map o unregister_codatatype_generic

fun is_raw_codatatype ctxt s =
  Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
  = SOME BNF_Util.Greatest_FP

fun is_registered_codatatype ctxt s =
  not (null (these (Option.map snd (AList.lookup (op =)
    (#codatatypes (Data.get (Context.Proof ctxt))) s))))

fun is_codatatype ctxt (Type (s, _)) =
    is_raw_codatatype ctxt s orelse is_registered_codatatype ctxt s
  | is_codatatype _ _ = false

fun is_registered_type ctxt (T as Type (s, _)) =
    is_frac_type ctxt T orelse is_registered_codatatype ctxt s
  | is_registered_type _ _ = false

fun is_raw_quot_type ctxt (Type (s, _)) =
    is_some (Quotient_Info.lookup_quotients ctxt s)
  | is_raw_quot_type _ _ = false

fun is_quot_type ctxt T =
  is_raw_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
  T <> \<^typ>\<open>int\<close>

fun is_pure_typedef ctxt (T as Type (s, _)) =
    is_frac_type ctxt T orelse
    (is_raw_typedef ctxt s andalso
     not (is_raw_free_datatype ctxt s orelse is_raw_quot_type ctxt T orelse
       is_codatatype ctxt T orelse is_integer_like_type T))
  | is_pure_typedef _ _ = false

fun is_univ_typedef ctxt (Type (s, _)) =
    (case typedef_info ctxt s of
       SOME {prop_of_Rep, ...} =>
       let
         val t_opt =
           try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep
       in
         case t_opt of
           SOME (Const (\<^const_name>\<open>top\<close>, _)) => true
           (* "Multiset.multiset" FIXME unchecked *)
         | SOME (Const (\<^const_name>\<open>Collect\<close>, _)
                 $ Abs (_, _, Const (\<^const_name>\<open>finite\<close>, _) $ _)) => true
           (* "FinFun.finfun" FIXME unchecked *)
         | SOME (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _,
                     Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _,
                         Const (\<^const_name>\<open>finite\<close>, _) $ _))) => true
         | _ => false
       end
     | NONE => false)
  | is_univ_typedef _ _ = false

fun is_data_type ctxt (T as Type (s, _)) =
    (is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse
     T = \<^typ>\<open>ind\<close> orelse is_raw_quot_type ctxt T) andalso
    not (is_interpreted_type s)
  | is_data_type _ _ = false

fun all_record_fields thy T =
  let val (recs, more) = Record.get_extT_fields thy T in
    recs @ more :: all_record_fields thy (snd more)
  end
  handle TYPE _ => []

val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields

fun no_of_record_field thy s T1 =
  find_index (curry (op =) s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)

fun is_record_get thy (s, Type (\<^type_name>\<open>fun\<close>, [T1, _])) =
    exists (curry (op =) s o fst) (all_record_fields thy T1)
  | is_record_get _ _ = false

fun is_record_update thy (s, T) =
  String.isSuffix Record.updateN s andalso
  exists (curry (op =) (unsuffix Record.updateN s) o fst) (all_record_fields thy (body_type T))
  handle TYPE _ => false

fun is_abs_fun ctxt (s, Type (\<^type_name>\<open>fun\<close>, [_, Type (s', _)])) =
    (case typedef_info ctxt s' of
       SOME {Abs_name, ...} => s = Abs_name
     | NONE => false)
  | is_abs_fun _ _ = false

fun is_rep_fun ctxt (s, Type (\<^type_name>\<open>fun\<close>, [Type (s', _), _])) =
    (case typedef_info ctxt s' of
       SOME {Rep_name, ...} => s = Rep_name
     | NONE => false)
  | is_rep_fun _ _ = false

fun is_quot_abs_fun ctxt (x as (_, Type (\<^type_name>\<open>fun\<close>,
                                         [_, abs_T as Type (s', _)]))) =
    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
    = SOME (Const x) andalso not (is_registered_type ctxt abs_T)
  | is_quot_abs_fun _ _ = false

fun is_quot_rep_fun ctxt (s, Type (\<^type_name>\<open>fun\<close>,
                                   [abs_T as Type (abs_s, _), _])) =
    (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
       SOME (Const (s', _)) =>
       s = s' andalso not (is_registered_type ctxt abs_T)
     | _ => false)
  | is_quot_rep_fun _ _ = false

fun mate_of_rep_fun ctxt (x as (_, Type (\<^type_name>\<open>fun\<close>,
                                         [T1 as Type (s', _), T2]))) =
    (case typedef_info ctxt s' of
       SOME {Abs_name, ...} => (Abs_name, Type (\<^type_name>\<open>fun\<close>, [T2, T1]))
     | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
  | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])

fun rep_type_for_quot_type ctxt (T as Type (s, _)) =
    let
      val thy = Proof_Context.theory_of ctxt
      val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients ctxt s)
    in
      instantiate_type thy qtyp T rtyp
    end
  | rep_type_for_quot_type _ T =
    raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])

fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
    let
      val {qtyp, equiv_rel, equiv_thm, ...} =
        the (Quotient_Info.lookup_quotients thy s)
      val partial =
        case Thm.prop_of equiv_thm of
          \<^Const_>\<open>Trueprop for \<^Const_>\<open>equivp _ for _\<close>\<close> => false
        | \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
        | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
                                   \relation theorem"
      val Ts' = dest_Type_args qtyp
    in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end
  | equiv_relation_for_quot_type _ T =
    raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])

fun is_raw_free_datatype_constr ctxt (s, T) =
  case body_type T of
    dtT as Type (dt_s, _) =>
    let
      val ctrs =
        case Ctr_Sugar.ctr_sugar_of ctxt dt_s of
          SOME {ctrs, ...} => map dest_Const ctrs
        | _ => []
    in
      exists (fn (s', T') => s = s' andalso repair_constr_type dtT T' = T) ctrs
    end
  | _  => false

fun is_registered_coconstr ctxt (s, T) =
  case body_type T of
    coT as Type (co_s, _) =>
    let
      val ctrs =
        co_s
        |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
        |> Option.map snd |> these
    in
      exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T) ctrs
    end
  | _ => false

fun is_nonfree_constr ctxt (s, T) =
  member (op =) [\<^const_name>\<open>FunBox\<close>, \<^const_name>\<open>PairBox\<close>,
                 \<^const_name>\<open>Quot\<close>, \<^const_name>\<open>Zero_Rep\<close>,
                 \<^const_name>\<open>Suc_Rep\<close>] s orelse
  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
    is_raw_free_datatype_constr ctxt x orelse
    (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
    is_registered_coconstr ctxt x
  end

fun is_free_constr ctxt (s, T) =
  is_nonfree_constr ctxt (s, T) andalso
  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
    not (is_abs_fun ctxt x) orelse is_univ_typedef ctxt (range_type T)
  end

fun is_stale_constr ctxt (x as (s, T)) =
  is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
  not (s = \<^const_name>\<open>Abs_Frac\<close> orelse is_registered_coconstr ctxt x)

fun is_constr ctxt (x as (_, T)) =
  is_nonfree_constr ctxt x andalso
  not (is_interpreted_type (dest_Type_name (unarize_type (body_type T)))) andalso
  not (is_stale_constr ctxt x)

val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
  String.isPrefix sel_prefix orf
  (member (op =) [\<^const_name>\<open>fst\<close>, \<^const_name>\<open>snd\<close>])

fun in_fun_lhs_for InConstr = InSel
  | in_fun_lhs_for _ = InFunLHS

fun in_fun_rhs_for InConstr = InConstr
  | in_fun_rhs_for InSel = InSel
  | in_fun_rhs_for InFunRHS1 = InFunRHS2
  | in_fun_rhs_for _ = InFunRHS1

fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
  case T of
    Type (\<^type_name>\<open>fun\<close>, _) =>
    (boxy = InPair orelse boxy = InFunLHS) andalso
    not (is_boolean_type (body_type T))
  | Type (\<^type_name>\<open>prod\<close>, Ts) =>
    boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
    ((boxy = InExpr orelse boxy = InFunLHS) andalso
     exists (is_boxing_worth_it hol_ctxt InPair)
            (map (box_type hol_ctxt InPair) Ts))
  | _ => false
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
  case triple_lookup (type_match thy) boxes (Type z) of
    SOME (SOME box_me) => box_me
  | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
and box_type hol_ctxt boxy T =
  case T of
    Type (z as (\<^type_name>\<open>fun\<close>, [T1, T2])) =>
    if boxy <> InConstr andalso boxy <> InSel andalso
       should_box_type hol_ctxt boxy z then
      Type (\<^type_name>\<open>fun_box\<close>,
            [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
    else
      box_type hol_ctxt (in_fun_lhs_for boxy) T1
      --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
  | Type (z as (\<^type_name>\<open>prod\<close>, Ts)) =>
    if boxy <> InConstr andalso boxy <> InSel
       andalso should_box_type hol_ctxt boxy z then
      Type (\<^type_name>\<open>pair_box\<close>, map (box_type hol_ctxt InSel) Ts)
    else
      Type (\<^type_name>\<open>prod\<close>,
            map (box_type hol_ctxt
                          (if boxy = InConstr orelse boxy = InSel then boxy
                           else InPair)) Ts)
  | _ => T

fun binarize_nat_and_int_in_type \<^typ>\<open>nat\<close> = \<^typ>\<open>unsigned_bit word\<close>
  | binarize_nat_and_int_in_type \<^typ>\<open>int\<close> = \<^typ>\<open>signed_bit word\<close>
  | binarize_nat_and_int_in_type (Type (s, Ts)) =
    Type (s, map binarize_nat_and_int_in_type Ts)
  | binarize_nat_and_int_in_type T = T
val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type

fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)

fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)

fun nth_sel_name_for_constr_name s n =
  if s = \<^const_name>\<open>Pair\<close> then
    if n = 0 then \<^const_name>\<open>fst\<close> else \<^const_name>\<open>snd\<close>
  else
    sel_prefix_for n ^ s

fun nth_sel_for_constr x ~1 = discr_for_constr x
  | nth_sel_for_constr (s, T) n =
    (nth_sel_name_for_constr_name s n,
     body_type T --> nth (maybe_curried_binder_types T) n)

fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
  apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
  oo nth_sel_for_constr

fun sel_no_from_name s =
  if String.isPrefix discr_prefix s then
    ~1
  else if String.isPrefix sel_prefix s then
    s |> unprefix sel_prefix |> Int.fromString |> the
  else if s = \<^const_name>\<open>snd\<close> then
    1
  else
    0

val close_form =
  let
    fun close_up zs zs' =
      fold (fn (z as ((s, _), T)) => fn t' =>
               Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
           (take (length zs' - length zs) zs')
    fun aux zs \<^Const>\<open>Pure.imp for t1 t2\<close> =
        let val zs' = Term.add_vars t1 zs in
          close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
        end
      | aux zs t = close_up zs (Term.add_vars t zs) t
  in aux [] end

fun distinctness_formula T =
  all_distinct_unordered_pairs_of
  #> map (fn (t1, t2) => \<^Const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
  #> List.foldr (s_conj o swap) \<^Const>\<open>True\<close>

fun zero_const T = Const (\<^const_name>\<open>zero_class.zero\<close>, T)
fun suc_const T = Const (\<^const_name>\<open>Suc\<close>, T --> T)

fun uncached_data_type_constrs ({ctxt, ...} : hol_context) (T as Type (s, _)) =
    if is_interpreted_type s then
      []
    else
      (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) s of
         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
       | _ =>
         if is_frac_type ctxt T then
           case typedef_info ctxt s of
             SOME {abs_type, rep_type, Abs_name, ...} =>
             [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
           | NONE => [] (* impossible *)
         else
           case Ctr_Sugar.ctr_sugar_of ctxt s of
             SOME {ctrs, ...} =>
             map (apsnd (repair_constr_type T) o dest_Const) ctrs
           | NONE =>
             if is_raw_quot_type ctxt T then
               [(\<^const_name>\<open>Quot\<close>, rep_type_for_quot_type ctxt T --> T)]
             else case typedef_info ctxt s of
               SOME {abs_type, rep_type, Abs_name, ...} =>
               [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
             | NONE =>
               if T = \<^typ>\<open>ind\<close> then [dest_Const \<^Const>\<open>Zero_Rep\<close>, dest_Const \<^Const>\<open>Suc_Rep\<close>]
               else [])
  | uncached_data_type_constrs _ _ = []

fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T =
  case AList.lookup (op =) (!constr_cache) T of
    SOME xs => xs
  | NONE =>
    let val xs = uncached_data_type_constrs hol_ctxt T in
      (Unsynchronized.change constr_cache (cons (T, xs)); xs)
    end

fun binarized_and_boxed_data_type_constrs hol_ctxt binarize =
  map (apsnd ((binarize ? binarize_nat_and_int_in_type)
              o box_type hol_ctxt InConstr)) o data_type_constrs hol_ctxt

fun constr_name_for_sel_like \<^const_name>\<open>fst\<close> = \<^const_name>\<open>Pair\<close>
  | constr_name_for_sel_like \<^const_name>\<open>snd\<close> = \<^const_name>\<open>Pair\<close>
  | constr_name_for_sel_like s' = original_name s'

fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
  let val s = constr_name_for_sel_like s' in
    AList.lookup (op =)
        (binarized_and_boxed_data_type_constrs hol_ctxt binarize (domain_type T'))
        s
    |> the |> pair s
  end

fun card_of_type assigns (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
  | card_of_type assigns (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) =
    card_of_type assigns T1 * card_of_type assigns T2
  | card_of_type assigns (Type (\<^type_name>\<open>set\<close>, [T'])) =
    reasonable_power 2 (card_of_type assigns T')
  | card_of_type _ (Type (\<^type_name>\<open>itself\<close>, _)) = 1
  | card_of_type _ \<^typ>\<open>prop\<close> = 2
  | card_of_type _ \<^typ>\<open>bool\<close> = 2
  | card_of_type assigns T =
    case AList.lookup (op =) assigns T of
      SOME k => k
    | NONE => if T = \<^typ>\<open>bisim_iterator\<close> then 0
              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])

fun bounded_card_of_type max default_card assigns
                         (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
    let
      val k1 = bounded_card_of_type max default_card assigns T1
      val k2 = bounded_card_of_type max default_card assigns T2
    in
      if k1 = max orelse k2 = max then max
      else Int.min (max, reasonable_power k2 k1)
      handle TOO_LARGE _ => max
    end
  | bounded_card_of_type max default_card assigns
                         (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) =
    let
      val k1 = bounded_card_of_type max default_card assigns T1
      val k2 = bounded_card_of_type max default_card assigns T2
    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
  | bounded_card_of_type max default_card assigns
                         (Type (\<^type_name>\<open>set\<close>, [T'])) =
    bounded_card_of_type max default_card assigns (T' --> bool_T)
  | bounded_card_of_type max default_card assigns T =
    Int.min (max, if default_card = ~1 then
                    card_of_type assigns T
                  else
                    card_of_type assigns T
                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                           default_card)

(* Similar to "ATP_Util.tiny_card_of_type". *)
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
                               assigns T =
  let
    fun aux avoid T =
      (if member (op =) avoid T then
         0
       else if member (op =) finitizable_dataTs T then
         raise SAME ()
       else case T of
         Type (\<^type_name>\<open>fun\<close>, [T1, T2]) =>
         (case (aux avoid T1, aux avoid T2) of
            (_, 1) => 1
          | (0, _) => 0
          | (_, 0) => 0
          | (k1, k2) =>
            if k1 >= max orelse k2 >= max then max
            else Int.min (max, reasonable_power k2 k1))
       | Type (\<^type_name>\<open>prod\<close>, [T1, T2]) =>
         (case (aux avoid T1, aux avoid T2) of
            (0, _) => 0
          | (_, 0) => 0
          | (k1, k2) =>
            if k1 >= max orelse k2 >= max then max
            else Int.min (max, k1 * k2))
       | Type (\<^type_name>\<open>set\<close>, [T']) => aux avoid (T' --> bool_T)
       | Type (\<^type_name>\<open>itself\<close>, _) => 1
       | \<^typ>\<open>prop\<close> => 2
       | \<^typ>\<open>bool\<close> => 2
       | Type _ =>
         (case data_type_constrs hol_ctxt T of
            [] => if is_integer_type T orelse is_bit_type T then 0
                  else raise SAME ()
          | constrs =>
            let
              val constr_cards =
                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
                    constrs
            in
              if exists (curry (op =) 0) constr_cards then 0
              else Int.min (max, Integer.sum constr_cards)
            end)
       | _ => raise SAME ())
      handle SAME () =>
             AList.lookup (op =) assigns T |> the_default default_card
  in Int.min (max, aux [] T) end

val typical_atomic_card = 4
val typical_card_of_type = bounded_card_of_type 16777217 typical_atomic_card []

fun is_finite_type hol_ctxt T =
  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0

fun is_special_eligible_arg strict Ts t =
  case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
    [] => true
  | bad_Ts =>
    let
      val bad_Ts_cost =
        if strict then fold (curry (op *) o typical_card_of_type) bad_Ts 1
        else fold (Integer.max o typical_card_of_type) bad_Ts 0
      val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
    in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end

fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))

fun let_var s = (nitpick_prefix ^ s, 999)
val let_inline_threshold = 20

fun s_let Ts s n abs_T body_T f t =
  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
     is_special_eligible_arg false Ts t then
    f t
  else
    let val z = (let_var s, abs_T) in
      Const (\<^const_name>\<open>Let\<close>, abs_T --> (abs_T --> body_T) --> body_T)
      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
    end

fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
  | loose_bvar1_count (t1 $ t2, k) =
    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
  | loose_bvar1_count _ = 0

fun s_betapply _ (t1 as Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1', t2) =
    if t1' aconv t2 then \<^prop>\True\ else t1 $ t2
  | s_betapply _ (t1 as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1', t2) =
    if t1' aconv t2 then \<^term>\True\ else t1 $ t2
  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>True\<close> $ t1', _) = t1'
  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>False\<close> $ _, t2) = t2
  | s_betapply Ts (Const (\<^const_name>\<open>Let\<close>,
                          Type (_, [bound_T, Type (_, [_, body_T])]))
                   $ t12 $ Abs (s, T, t13'), t2) =
    let val body_T' = range_type body_T in
      Const (\<^const_name>\<open>Let\<close>, bound_T --> (bound_T --> body_T') --> body_T')
      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
    end
  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
           (curry betapply t1) t2
     (* FIXME: fix all "s_betapply []" calls *)
     handle TERM _ => betapply (t1, t2)
          | General.Subscript => betapply (t1, t2))
  | s_betapply _ (t1, t2) = t1 $ t2

fun s_betapplys Ts = Library.foldl (s_betapply Ts)

fun s_beta_norm Ts t =
  let
    fun aux _ (Var _) = raise Same.SAME
      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
      | aux Ts ((t1 as Abs _) $ t2) =
        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
      | aux Ts (t1 $ t2) =
        ((case aux Ts t1 of
           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
         | t1 => t1 $ Same.commit (aux Ts) t2)
        handle Same.SAME => t1 $ aux Ts t2)
      | aux _ _ = raise Same.SAME
  in aux Ts t handle Same.SAME => t end

fun discr_term_for_constr hol_ctxt (x as (s, T)) =
  let val dataT = body_type T in
    if s = \<^const_name>\<open>Suc\<close> then
      Abs (Name.uu, dataT, \<^Const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
    else if length (data_type_constrs hol_ctxt dataT) >= 2 then
      Const (discr_for_constr x)
    else
      Abs (Name.uu, dataT, \<^Const>\<open>True\<close>)
  end

fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
  case head_of t of
    Const x' =>
    if x = x' then \<^Const>\True\
    else if is_nonfree_constr ctxt x' then \<^Const>\False\
    else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
  | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)

fun nth_arg_sel_term_for_constr (x as (s, T)) n =
  let val (arg_Ts, dataT) = strip_type T in
    if dataT = nat_T then
      \<^term>\<open>%n::nat. n - 1\<close>
    else if is_pair_type dataT then
      Const (nth_sel_for_constr x n)
    else
      let
        fun aux m (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) =
            let
              val (m, t1) = aux m T1
              val (m, t2) = aux m T2
            in (m, HOLogic.mk_prod (t1, t2)) end
          | aux m T =
            (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
                    $ Bound 0)
        val m = fold (Integer.add o num_factors_in_type)
                     (List.take (arg_Ts, n)) 0
      in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
  end

fun select_nth_constr_arg ctxt x t n res_T =
  (case strip_comb t of
     (Const x', args) =>
     if x = x' then
        if is_free_constr ctxt x then nth args n else raise SAME ()
     else if is_nonfree_constr ctxt x' then
       Const (\<^const_name>\<open>unknown\<close>, res_T)
     else
       raise SAME ()
   | _ => raise SAME())
  handle SAME () => s_betapply [] (nth_arg_sel_term_for_constr x n, t)

fun construct_value _ x [] = Const x
  | construct_value ctxt (x as (s, _)) args =
    let val args = map Envir.eta_contract args in
      case hd args of
        Const (s', _) $ t =>
        if is_sel_like_and_no_discr s' andalso
           constr_name_for_sel_like s' = s andalso
           forall (fn (n, t') => select_nth_constr_arg ctxt x t n dummyT = t')
                  (index_seq 0 (length args) ~~ args) then
          t
        else
          list_comb (Const x, args)
      | _ => list_comb (Const x, args)
    end

fun constr_expand (hol_ctxt as {ctxt, ...}) T t =
  (case head_of t of
     Const x => if is_nonfree_constr ctxt x then t else raise SAME ()
   | _ => raise SAME ())
  handle SAME () =>
         let
           val x' as (_, T') =
             if is_pair_type T then
               let val (T1, T2) = HOLogic.dest_prodT T in
                 (\<^const_name>\<open>Pair\<close>, T1 --> T2 --> T)
               end
             else
               data_type_constrs hol_ctxt T |> hd
           val arg_Ts = binder_types T'
         in
           list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t)
                                     (index_seq 0 (length arg_Ts)) arg_Ts)
         end

fun coerce_bound_no f j t =
  case t of
    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
  | Bound j' => if j' = j then f t else t
  | _ => t

fun coerce_bound_0_in_term hol_ctxt new_T old_T =
  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t =
  if old_T = new_T then
    t
  else
    case (new_T, old_T) of
      (Type (new_s, new_Ts as [new_T1, new_T2]),
       Type (\<^type_name>\<open>fun\<close>, [old_T1, old_T2])) =>
      (case eta_expand Ts t 1 of
         Abs (s, _, t') =>
         Abs (s, new_T1,
              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
         |> Envir.eta_contract
         |> new_s <> \<^type_name>\<open>fun\<close>
            ? construct_value ctxt
                  (\<^const_name>\<open>FunBox\<close>,
                   Type (\<^type_name>\<open>fun\<close>, new_Ts) --> new_T)
              o single
       | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
    | (Type (new_s, new_Ts as [new_T1, new_T2]),
       Type (old_s, old_Ts as [old_T1, old_T2])) =>
      if old_s = \<^type_name>\<open>fun_box\<close> orelse
         old_s = \<^type_name>\<open>pair_box\<close> orelse old_s = \<^type_name>\<open>prod\<close> then
        case constr_expand hol_ctxt old_T t of
          Const (old_s, _) $ t1 =>
          if new_s = \<^type_name>\<open>fun\<close> then
            coerce_term hol_ctxt Ts new_T (Type (\<^type_name>\<open>fun\<close>, old_Ts)) t1
          else
            construct_value ctxt
                (old_s, Type (\<^type_name>\<open>fun\<close>, new_Ts) --> new_T)
                [coerce_term hol_ctxt Ts (Type (\<^type_name>\<open>fun\<close>, new_Ts))
                             (Type (\<^type_name>\<open>fun\<close>, old_Ts)) t1]
        | Const _ $ t1 $ t2 =>
          construct_value ctxt
              (if new_s = \<^type_name>\<open>prod\<close> then \<^const_name>\<open>Pair\<close>
               else \<^const_name>\<open>PairBox\<close>, new_Ts ---> new_T)
              (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
                    [t1, t2])
        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
      else
        raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
    | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])

fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
  | is_ground_term (Const _) = true
  | is_ground_term _ = false

fun special_bounds ts =
  fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o apply2 fst)

fun is_funky_typedef_name ctxt s =
  member (op =) [\<^type_name>\<open>unit\<close>, \<^type_name>\<open>prod\<close>, \<^type_name>\<open>set\<close>,
                 \<^type_name>\<open>Sum_Type.sum\<close>, \<^type_name>\<open>int\<close>] s orelse
  is_frac_type ctxt (Type (s, []))

fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
  | is_funky_typedef _ _ = false

fun all_defs_of thy subst =
  let
    val def_names =
      thy |> Theory.defs_of
          |> Defs.all_specifications_of
          |> maps snd |> map_filter #def
          |> Ord_List.make fast_string_ord
  in
    Thm.all_axioms_of thy
    |> map (apsnd (subst_atomic subst o Thm.prop_of))
    |> sort (fast_string_ord o apply2 fst)
    |> Ord_List.inter (fast_string_ord o apsnd fst) def_names
    |> map snd
  end

(* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any
   theory will do as long as it contains all the "axioms" and "axiomatization"
   commands. *)
fun is_built_in_theory thy_id =
  Context.subthy_id (thy_id, Context.theory_id \<^theory>\<open>Hilbert_Choice\<close>)

fun all_nondefs_of ctxt subst =
  ctxt |> Spec_Rules.get
       |> filter (Spec_Rules.is_unknown o #rough_classification)
       |> maps #rules
       |> filter_out (is_built_in_theory o Thm.theory_id)
       |> map (subst_atomic subst o Thm.prop_of)

fun arity_of_built_in_const (s, T) =
  if s = \<^const_name>\<open>If\<close> then
    if nth_range_type 3 T = \<^typ>\<open>bool\<close> then NONE else SOME 3
  else
    case AList.lookup (op =) built_in_consts s of
      SOME n => SOME n
    | NONE =>
      case AList.lookup (op =) built_in_typed_consts (s, unarize_type T) of
        SOME n => SOME n
      | NONE =>
        case s of
          \<^const_name>\<open>zero_class.zero\<close> => if is_iterator_type T then SOME 0 else NONE
        | \<^const_name>\<open>Suc\<close> => if is_iterator_type (domain_type T) then SOME 0 else NONE
        | _ => NONE

val is_built_in_const = is_some o arity_of_built_in_const

(* This function is designed to work for both real definition axioms and
   simplification rules (equational specifications). *)
fun term_under_def t =
  case t of
    \<^Const_>\<open>Pure.imp for _ t2\<close> => term_under_def t2
  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => term_under_def t1
  | \<^Const_>\<open>Trueprop for t1\<close> => term_under_def t1
  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => term_under_def t1
  | Abs (_, _, t') => term_under_def t'
  | t1 $ _ => term_under_def t1
  | _ => t

(* Here we crucially rely on "specialize_type" performing a preorder traversal
   of the term, without which the wrong occurrence of a constant could be
   matched in the face of overloading. *)
fun def_props_for_const thy table (x as (s, _)) =
  if is_built_in_const x then
    []
  else
    these (Symtab.lookup table s)
    |> map_filter (try (specialize_type thy x))
    |> filter (curry (op =) (Const x) o term_under_def)

fun normalized_rhs_of t =
  let
    fun aux (v as Var _) (SOME t) = SOME (lambda v t)
      | aux (c as Const (\<^const_name>\<open>Pure.type\<close>, _)) (SOME t) = SOME (lambda c t)
      | aux _ _ = NONE
    val (lhs, rhs) =
      case t of
        \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => (t1, t2)
      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close> => (t1, t2)
      | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    val args = strip_comb lhs |> snd
  in fold_rev aux args (SOME rhs) end

fun get_def_of_const thy table (x as (s, _)) =
  x |> def_props_for_const thy table |> List.last
    |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
  handle List.Empty => NONE
       | TERM _ => NONE

fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
  if is_built_in_const x orelse original_name s <> s then
    NONE
  else case get_def_of_const thy unfold_table x of
    SOME def => SOME (true, def)
  | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false)

val def_of_const = Option.map snd ooo def_of_const_ext

fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
  | fixpoint_kind_of_rhs (Const (\<^const_name>\<open>lfp\<close>, _) $ Abs _) = Lfp
  | fixpoint_kind_of_rhs (Const (\<^const_name>\<open>gfp\<close>, _) $ Abs _) = Gfp
  | fixpoint_kind_of_rhs _ = NoFp

fun is_mutually_inductive_pred_def thy table t =
  let
    fun is_good_arg (Bound _) = true
      | is_good_arg (Const (s, _)) =
        s = \<^const_name>\<open>True\<close> orelse s = \<^const_name>\<open>False\<close> orelse
        s = \<^const_name>\<open>undefined\<close>
      | is_good_arg _ = false
  in
    case t |> strip_abs_body |> strip_comb of
      (Const x, ts as (_ :: _)) =>
      (case def_of_const thy table x of
         SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso
                    forall is_good_arg ts
       | NONE => false)
    | _ => false
  end

fun unfold_mutually_inductive_preds thy table =
  map_aterms (fn t as Const x =>
      (case def_of_const thy table x of
         SOME t' =>
         let val t' = Envir.eta_contract t' in
           if is_mutually_inductive_pred_def thy table t' then t' else t
         end
      | NONE => t)
    | t => t)

fun case_const_names ctxt =
  map_filter (fn {casex = Const (s, T), ...} =>
      (case rev (binder_types T) of
        [] => NONE
      | T :: Ts => if is_data_type ctxt T then SOME (s, length Ts) else NONE))
    (Ctr_Sugar.ctr_sugars_of ctxt) @
  map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt)))

fun fixpoint_kind_of_const thy table x =
  if is_built_in_const x then NoFp
  else fixpoint_kind_of_rhs (the (def_of_const thy table x))
  handle Option.Option => NoFp

fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context) x =
  fixpoint_kind_of_const thy def_tables x <> NoFp andalso
  not (null (def_props_for_const thy intro_table x))

fun is_inductive_pred hol_ctxt (x as (s, _)) =
  String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse
  is_raw_inductive_pred hol_ctxt x

fun lhs_of_equation t =
  case t of
    \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => SOME t1
  | \<^Const_>\<open>Pure.imp for _ t2\<close> => lhs_of_equation t2
  | \<^Const_>\<open>Trueprop for t1\<close> => lhs_of_equation t1
  | \<^Const_>\<open>All _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => SOME t1
  | \<^Const_>\<open>implies for _ t2\<close> => lhs_of_equation t2
  | _ => NONE

fun is_constr_pattern _ (Bound _) = true
  | is_constr_pattern _ (Var _) = true
  | is_constr_pattern ctxt t =
    case strip_comb t of
      (Const x, args) =>
      is_nonfree_constr ctxt x andalso forall (is_constr_pattern ctxt) args
    | _ => false

fun is_constr_pattern_lhs ctxt t =
  forall (is_constr_pattern ctxt) (snd (strip_comb t))

fun is_constr_pattern_formula ctxt t =
  case lhs_of_equation t of
    SOME t' => is_constr_pattern_lhs ctxt t'
  | NONE => false

(* Similar to "specialize_type" but returns all matches rather than only the
   first (preorder) match. *)
fun multi_specialize_type thy slack (s, T) t =
  let
    fun aux (Const (s', T')) ys =
        if s = s' then
          ys |> (if AList.defined (op =) ys T' then
                   I
                 else
                   cons (T', Envir.subst_term_types (Sign.typ_match thy (T', T)
                     Vartab.empty) t)
                   handle Type.TYPE_MATCH => I
                        | TERM _ =>
                          if slack then
                            I
                          else
                            raise NOT_SUPPORTED
                                      ("too much polymorphism in axiom \"" ^
                                       Syntax.string_of_term_global thy t ^
                                       "\" involving " ^ quote s))
        else
          ys
      | aux _ ys = ys
  in map snd (fold_aterms aux t []) end

fun nondef_props_for_const thy slack table (x as (s, _)) =
  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)

fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2
  | unvarify_term (Var ((s, 0), T)) = Free (s, T)
  | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
  | unvarify_term t = t

fun axiom_for_choice_spec ctxt =
  unvarify_term
  #> Object_Logic.atomize_term ctxt
  #> Choice_Specification.close_form
  #> HOLogic.mk_Trueprop

fun is_choice_spec_fun ({thy, ctxt, def_tables, nondef_table, choice_spec_table, ...}
                        : hol_context) x =
  case nondef_props_for_const thy true choice_spec_table x of
    [] => false
  | ts => case def_of_const thy def_tables x of
            SOME (Const (\<^const_name>\<open>Eps\<close>, _) $ _) => true
          | SOME _ => false
          | NONE =>
            let val ts' = nondef_props_for_const thy true nondef_table x in
              length ts' = length ts andalso
              forall (fn t =>
                         exists (curry (op aconv) (axiom_for_choice_spec ctxt t))
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.