blanchet@33978: (* Title: HOL/Tools/Nitpick/nitpick_hol.ML blanchet@33192: Author: Jasmin Blanchette, TU Muenchen blanchet@34969: Copyright 2008, 2009, 2010 blanchet@33192: blanchet@33192: Auxiliary HOL-related functions used by Nitpick. blanchet@33192: *) blanchet@33192: blanchet@33192: signature NITPICK_HOL = blanchet@33192: sig blanchet@33705: type styp = Nitpick_Util.styp blanchet@33192: type const_table = term list Symtab.table blanchet@33192: type special_fun = (styp * int list * term list) * styp blanchet@33192: type unrolled = styp * styp blanchet@33192: type wf_cache = (styp * (bool * bool)) list blanchet@33192: blanchet@35067: type hol_context = { blanchet@33192: thy: theory, blanchet@33192: ctxt: Proof.context, blanchet@33192: max_bisim_depth: int, blanchet@33192: boxes: (typ option * bool option) list, blanchet@34969: stds: (typ option * bool) list, blanchet@33192: wfs: (styp option * bool option) list, blanchet@33192: user_axioms: bool option, blanchet@33192: debug: bool, blanchet@34121: binary_ints: bool option, blanchet@33192: destroy_constrs: bool, blanchet@33192: specialize: bool, blanchet@33192: skolemize: bool, blanchet@33192: star_linear_preds: bool, blanchet@33192: uncurry: bool, blanchet@33192: fast_descrs: bool, blanchet@33192: tac_timeout: Time.time option, blanchet@33192: evals: term list, blanchet@33192: case_names: (string * int) list, blanchet@33192: def_table: const_table, blanchet@33192: nondef_table: const_table, blanchet@33192: user_nondefs: term list, blanchet@33192: simp_table: const_table Unsynchronized.ref, blanchet@33192: psimp_table: const_table, blanchet@33192: intro_table: const_table, blanchet@33192: ground_thm_table: term list Inttab.table, blanchet@33192: ersatz_table: (string * string) list, blanchet@33192: skolems: (string * string list) list Unsynchronized.ref, blanchet@33192: special_funs: special_fun list Unsynchronized.ref, blanchet@33192: unrolled_preds: unrolled list Unsynchronized.ref, blanchet@33571: wf_cache: wf_cache Unsynchronized.ref, blanchet@33571: constr_cache: (typ * styp list) list Unsynchronized.ref} blanchet@33192: blanchet@35067: datatype fixpoint_kind = Lfp | Gfp | NoFp blanchet@35067: datatype boxability = blanchet@35067: InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 blanchet@35067: blanchet@33192: val name_sep : string blanchet@33192: val numeral_prefix : string blanchet@35067: val ubfp_prefix : string blanchet@35067: val lbfp_prefix : string blanchet@35311: val quot_normal_prefix : string blanchet@33192: val skolem_prefix : string blanchet@35067: val special_prefix : string blanchet@35067: val uncurry_prefix : string blanchet@33192: val eval_prefix : string blanchet@33192: val original_name : string -> string blanchet@34985: val s_conj : term * term -> term blanchet@35067: val s_disj : term * term -> term blanchet@35067: val strip_any_connective : term -> term list * term blanchet@35067: val conjuncts_of : term -> term list blanchet@35067: val disjuncts_of : term -> term list blanchet@35665: val unarize_unbox_etc_type : typ -> typ blanchet@35665: val uniterize_unarize_unbox_etc_type : typ -> typ blanchet@33192: val string_for_type : Proof.context -> typ -> string blanchet@33192: val prefix_name : string -> string -> string blanchet@34118: val shortest_name : string -> string blanchet@33192: val short_name : string -> string blanchet@34118: val shorten_names_in_term : term -> term blanchet@33192: val type_match : theory -> typ * typ -> bool blanchet@33192: val const_match : theory -> styp * styp -> bool blanchet@33192: val term_match : theory -> term * term -> bool blanchet@33192: val is_TFree : typ -> bool blanchet@33192: val is_higher_order_type : typ -> bool blanchet@33192: val is_fun_type : typ -> bool blanchet@33192: val is_set_type : typ -> bool blanchet@33192: val is_pair_type : typ -> bool blanchet@33192: val is_lfp_iterator_type : typ -> bool blanchet@33192: val is_gfp_iterator_type : typ -> bool blanchet@33192: val is_fp_iterator_type : typ -> bool blanchet@35280: val is_iterator_type : typ -> bool blanchet@33192: val is_boolean_type : typ -> bool blanchet@33192: val is_integer_type : typ -> bool blanchet@34121: val is_bit_type : typ -> bool blanchet@34121: val is_word_type : typ -> bool blanchet@35220: val is_integer_like_type : typ -> bool blanchet@33192: val is_record_type : typ -> bool blanchet@33192: val is_number_type : theory -> typ -> bool blanchet@33192: val const_for_iterator_type : typ -> styp blanchet@35067: val strip_n_binders : int -> typ -> typ list * typ blanchet@33192: val nth_range_type : int -> typ -> typ blanchet@33192: val num_factors_in_type : typ -> int blanchet@33192: val num_binder_types : typ -> int blanchet@33192: val curried_binder_types : typ -> typ list blanchet@33192: val mk_flat_tuple : typ -> term list -> term blanchet@33192: val dest_n_tuple : int -> term -> term list blanchet@33978: val is_real_datatype : theory -> string -> bool blanchet@35220: val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool blanchet@34923: val is_quot_type : theory -> typ -> bool blanchet@33192: val is_codatatype : theory -> typ -> bool blanchet@33192: val is_pure_typedef : theory -> typ -> bool blanchet@33192: val is_univ_typedef : theory -> typ -> bool blanchet@35220: val is_datatype : theory -> (typ option * bool) list -> typ -> bool blanchet@33192: val is_record_constr : styp -> bool blanchet@33192: val is_record_get : theory -> styp -> bool blanchet@33192: val is_record_update : theory -> styp -> bool blanchet@33192: val is_abs_fun : theory -> styp -> bool blanchet@33192: val is_rep_fun : theory -> styp -> bool blanchet@34923: val is_quot_abs_fun : Proof.context -> styp -> bool blanchet@34923: val is_quot_rep_fun : Proof.context -> styp -> bool blanchet@35067: val mate_of_rep_fun : theory -> styp -> styp blanchet@35067: val is_constr_like : theory -> styp -> bool blanchet@35067: val is_stale_constr : theory -> styp -> bool blanchet@35220: val is_constr : theory -> (typ option * bool) list -> styp -> bool blanchet@33192: val is_sel : string -> bool blanchet@34121: val is_sel_like_and_no_discr : string -> bool blanchet@35067: val box_type : hol_context -> boxability -> typ -> typ blanchet@35190: val binarize_nat_and_int_in_type : typ -> typ blanchet@35190: val binarize_nat_and_int_in_term : term -> term blanchet@33192: val discr_for_constr : styp -> styp blanchet@33192: val num_sels_for_constr_type : typ -> int blanchet@33192: val nth_sel_name_for_constr_name : string -> int -> string blanchet@33192: val nth_sel_for_constr : styp -> int -> styp blanchet@35190: val binarized_and_boxed_nth_sel_for_constr : blanchet@35190: hol_context -> bool -> styp -> int -> styp blanchet@33192: val sel_no_from_name : string -> int blanchet@35075: val close_form : term -> term blanchet@33192: val eta_expand : typ list -> term -> int -> term blanchet@33192: val extensionalize : term -> term blanchet@33192: val distinctness_formula : typ -> term list -> term blanchet@33192: val register_frac_type : string -> (string * string) list -> theory -> theory blanchet@33192: val unregister_frac_type : string -> theory -> theory blanchet@33192: val register_codatatype : typ -> string -> styp list -> theory -> theory blanchet@33192: val unregister_codatatype : typ -> theory -> theory blanchet@35067: val datatype_constrs : hol_context -> typ -> styp list blanchet@35190: val binarized_and_boxed_datatype_constrs : blanchet@35190: hol_context -> bool -> typ -> styp list blanchet@35067: val num_datatype_constrs : hol_context -> typ -> int blanchet@33192: val constr_name_for_sel_like : string -> string blanchet@35190: val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp blanchet@35067: val discriminate_value : hol_context -> styp -> term -> term blanchet@35220: val select_nth_constr_arg : blanchet@35220: theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term blanchet@35220: val construct_value : blanchet@35220: theory -> (typ option * bool) list -> styp -> term list -> term blanchet@35665: val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term blanchet@33192: val card_of_type : (typ * int) list -> typ -> int blanchet@33192: val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int blanchet@34120: val bounded_exact_card_of_type : blanchet@35385: hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int blanchet@35067: val is_finite_type : hol_context -> typ -> bool blanchet@35665: val is_small_finite_type : hol_context -> typ -> bool blanchet@35067: val special_bounds : term list -> (indexname * typ) list blanchet@35386: val abs_var : indexname * typ -> term -> term blanchet@35067: val is_funky_typedef : theory -> typ -> bool blanchet@35335: val all_axioms_of : blanchet@35335: theory -> (term * term) list -> term list * term list * term list blanchet@35220: val arity_of_built_in_const : blanchet@35220: theory -> (typ option * bool) list -> bool -> styp -> int option blanchet@35220: val is_built_in_const : blanchet@35220: theory -> (typ option * bool) list -> bool -> styp -> bool blanchet@35067: val term_under_def : term -> term blanchet@35220: val case_const_names : blanchet@35220: theory -> (typ option * bool) list -> (string * int) list blanchet@35335: val const_def_table : blanchet@35335: Proof.context -> (term * term) list -> term list -> const_table blanchet@33192: val const_nondef_table : term list -> const_table blanchet@35335: val const_simp_table : Proof.context -> (term * term) list -> const_table blanchet@35335: val const_psimp_table : Proof.context -> (term * term) list -> const_table blanchet@35335: val inductive_intro_table : blanchet@35335: Proof.context -> (term * term) list -> const_table -> const_table blanchet@33192: val ground_theorem_table : theory -> term list Inttab.table blanchet@33192: val ersatz_table : theory -> (string * string) list blanchet@35067: val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit blanchet@35067: val inverse_axioms_for_rep_fun : theory -> styp -> term list blanchet@35067: val optimized_typedef_axioms : theory -> string * typ list -> term list blanchet@35220: val optimized_quot_type_axioms : blanchet@35311: Proof.context -> (typ option * bool) list -> string * typ list -> term list blanchet@33192: val def_of_const : theory -> const_table -> styp -> term option blanchet@35067: val fixpoint_kind_of_const : blanchet@35067: theory -> const_table -> string * typ -> fixpoint_kind blanchet@35067: val is_inductive_pred : hol_context -> styp -> bool blanchet@35067: val is_equational_fun : hol_context -> styp -> bool blanchet@33192: val is_constr_pattern_lhs : theory -> term -> bool blanchet@33192: val is_constr_pattern_formula : theory -> term -> bool blanchet@35067: val unfold_defs_in_term : hol_context -> term -> term blanchet@35067: val codatatype_bisim_axioms : hol_context -> typ -> term list blanchet@35067: val is_well_founded_inductive_pred : hol_context -> styp -> bool blanchet@35067: val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term blanchet@35067: val equational_fun_axioms : hol_context -> styp -> term list blanchet@35067: val is_equational_fun_surely_complete : hol_context -> styp -> bool blanchet@33547: val merge_type_vars_in_terms : term list -> term list blanchet@35190: val ground_types_in_type : hol_context -> bool -> typ -> typ list blanchet@35190: val ground_types_in_terms : hol_context -> bool -> term list -> typ list blanchet@33192: val format_type : int list -> int list -> typ -> typ blanchet@33192: val format_term_type : blanchet@33192: theory -> const_table -> (term option * int list) list -> term -> typ blanchet@33192: val user_friendly_const : blanchet@35067: hol_context -> string * string -> (term option * int list) list blanchet@33192: -> styp -> term * typ blanchet@33192: val assign_operator_for_const : styp -> string blanchet@33192: end; blanchet@33192: blanchet@33224: structure Nitpick_HOL : NITPICK_HOL = blanchet@33192: struct blanchet@33192: blanchet@33224: open Nitpick_Util blanchet@33192: blanchet@33192: type const_table = term list Symtab.table blanchet@33192: type special_fun = (styp * int list * term list) * styp blanchet@33192: type unrolled = styp * styp blanchet@33192: type wf_cache = (styp * (bool * bool)) list blanchet@33192: blanchet@35067: type hol_context = { blanchet@33192: thy: theory, blanchet@33192: ctxt: Proof.context, blanchet@33192: max_bisim_depth: int, blanchet@33192: boxes: (typ option * bool option) list, blanchet@34969: stds: (typ option * bool) list, blanchet@33192: wfs: (styp option * bool option) list, blanchet@33192: user_axioms: bool option, blanchet@33192: debug: bool, blanchet@34121: binary_ints: bool option, blanchet@33192: destroy_constrs: bool, blanchet@33192: specialize: bool, blanchet@33192: skolemize: bool, blanchet@33192: star_linear_preds: bool, blanchet@33192: uncurry: bool, blanchet@33192: fast_descrs: bool, blanchet@33192: tac_timeout: Time.time option, blanchet@33192: evals: term list, blanchet@33192: case_names: (string * int) list, blanchet@33192: def_table: const_table, blanchet@33192: nondef_table: const_table, blanchet@33192: user_nondefs: term list, blanchet@33192: simp_table: const_table Unsynchronized.ref, blanchet@33192: psimp_table: const_table, blanchet@33192: intro_table: const_table, blanchet@33192: ground_thm_table: term list Inttab.table, blanchet@33192: ersatz_table: (string * string) list, blanchet@33192: skolems: (string * string list) list Unsynchronized.ref, blanchet@33192: special_funs: special_fun list Unsynchronized.ref, blanchet@33192: unrolled_preds: unrolled list Unsynchronized.ref, blanchet@33571: wf_cache: wf_cache Unsynchronized.ref, blanchet@33571: constr_cache: (typ * styp list) list Unsynchronized.ref} blanchet@33192: blanchet@35067: datatype fixpoint_kind = Lfp | Gfp | NoFp blanchet@35067: datatype boxability = blanchet@35067: InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 blanchet@35067: blanchet@33574: structure Data = Theory_Data( blanchet@33192: type T = {frac_types: (string * (string * string) list) list, blanchet@33192: codatatypes: (string * (string * styp list)) list} blanchet@33192: val empty = {frac_types = [], codatatypes = []} blanchet@33192: val extend = I wenzelm@33522: fun merge ({frac_types = fs1, codatatypes = cs1}, wenzelm@33522: {frac_types = fs2, codatatypes = cs2}) : T = wenzelm@33699: {frac_types = AList.merge (op =) (K true) (fs1, fs2), wenzelm@33699: codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) blanchet@33192: blanchet@33192: val name_sep = "$" blanchet@33192: val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep blanchet@33192: val sel_prefix = nitpick_prefix ^ "sel" blanchet@33192: val discr_prefix = nitpick_prefix ^ "is" ^ name_sep blanchet@33192: val set_prefix = nitpick_prefix ^ "set" ^ name_sep blanchet@33192: val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep blanchet@33192: val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep blanchet@33192: val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep blanchet@33192: val base_prefix = nitpick_prefix ^ "base" ^ name_sep blanchet@33192: val step_prefix = nitpick_prefix ^ "step" ^ name_sep blanchet@33192: val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep blanchet@33192: val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep blanchet@35311: val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep blanchet@33192: val skolem_prefix = nitpick_prefix ^ "sk" blanchet@33192: val special_prefix = nitpick_prefix ^ "sp" blanchet@33192: val uncurry_prefix = nitpick_prefix ^ "unc" blanchet@33192: val eval_prefix = nitpick_prefix ^ "eval" blanchet@33192: val iter_var_prefix = "i" blanchet@33192: val arg_var_prefix = "x" blanchet@33192: blanchet@33192: (* int -> string *) blanchet@33192: fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep blanchet@35311: (* Proof.context -> typ -> string *) blanchet@35311: fun quot_normal_name_for_type ctxt T = blanchet@35311: quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) blanchet@33192: blanchet@33192: (* string -> string * string *) blanchet@33192: val strip_first_name_sep = blanchet@33192: Substring.full #> Substring.position name_sep ##> Substring.triml 1 blanchet@33192: #> pairself Substring.string blanchet@33192: (* string -> string *) blanchet@33192: fun original_name s = blanchet@33192: if String.isPrefix nitpick_prefix s then blanchet@33192: case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 blanchet@33192: else blanchet@33192: s blanchet@33192: val after_name_sep = snd o strip_first_name_sep blanchet@33192: blanchet@34985: (* term * term -> term *) blanchet@34985: fun s_conj (t1, @{const True}) = t1 blanchet@34985: | s_conj (@{const True}, t2) = t2 blanchet@34985: | s_conj (t1, t2) = blanchet@34985: if t1 = @{const False} orelse t2 = @{const False} then @{const False} blanchet@34985: else HOLogic.mk_conj (t1, t2) blanchet@34985: fun s_disj (t1, @{const False}) = t1 blanchet@34985: | s_disj (@{const False}, t2) = t2 blanchet@34985: | s_disj (t1, t2) = blanchet@34985: if t1 = @{const True} orelse t2 = @{const True} then @{const True} blanchet@34985: else HOLogic.mk_disj (t1, t2) blanchet@34985: blanchet@34985: (* term -> term -> term list *) blanchet@34985: fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = blanchet@34985: if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t] blanchet@34985: | strip_connective _ t = [t] blanchet@34985: (* term -> term list * term *) blanchet@35280: fun strip_any_connective (t as (t0 $ _ $ _)) = blanchet@34985: if t0 = @{const "op &"} orelse t0 = @{const "op |"} then blanchet@34985: (strip_connective t0 t, t0) blanchet@34985: else blanchet@34985: ([t], @{const Not}) blanchet@34985: | strip_any_connective t = ([t], @{const Not}) blanchet@34985: (* term -> term list *) blanchet@35067: val conjuncts_of = strip_connective @{const "op &"} blanchet@35067: val disjuncts_of = strip_connective @{const "op |"} blanchet@34985: blanchet@33192: (* When you add constants to these lists, make sure to handle them in blanchet@33224: "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as blanchet@33192: well. *) blanchet@33192: val built_in_consts = blanchet@33192: [(@{const_name all}, 1), blanchet@33192: (@{const_name "=="}, 2), blanchet@33192: (@{const_name "==>"}, 2), blanchet@33192: (@{const_name Pure.conjunction}, 2), blanchet@33192: (@{const_name Trueprop}, 1), blanchet@33192: (@{const_name Not}, 1), blanchet@33192: (@{const_name False}, 0), blanchet@33192: (@{const_name True}, 0), blanchet@33192: (@{const_name All}, 1), blanchet@33192: (@{const_name Ex}, 1), blanchet@33192: (@{const_name "op ="}, 2), blanchet@33192: (@{const_name "op &"}, 2), blanchet@33192: (@{const_name "op |"}, 2), blanchet@33192: (@{const_name "op -->"}, 2), blanchet@33192: (@{const_name If}, 3), blanchet@33192: (@{const_name Let}, 2), blanchet@33192: (@{const_name Unity}, 0), blanchet@33192: (@{const_name Pair}, 2), blanchet@33192: (@{const_name fst}, 1), blanchet@33192: (@{const_name snd}, 1), blanchet@33192: (@{const_name Id}, 0), blanchet@33192: (@{const_name insert}, 2), blanchet@33192: (@{const_name converse}, 1), blanchet@33192: (@{const_name trancl}, 1), blanchet@33192: (@{const_name rel_comp}, 2), blanchet@33192: (@{const_name image}, 2), blanchet@33192: (@{const_name finite}, 1), blanchet@34923: (@{const_name unknown}, 0), blanchet@34923: (@{const_name is_unknown}, 1), blanchet@33192: (@{const_name Tha}, 1), blanchet@33192: (@{const_name Frac}, 0), blanchet@33192: (@{const_name norm_frac}, 0)] blanchet@35220: val built_in_nat_consts = blanchet@35220: [(@{const_name Suc}, 0), blanchet@35220: (@{const_name nat}, 0), blanchet@35220: (@{const_name nat_gcd}, 0), blanchet@35220: (@{const_name nat_lcm}, 0)] blanchet@33192: val built_in_descr_consts = blanchet@33192: [(@{const_name The}, 1), blanchet@33192: (@{const_name Eps}, 1)] blanchet@33192: val built_in_typed_consts = blanchet@35220: [((@{const_name zero_class.zero}, int_T), 0), blanchet@35220: ((@{const_name one_class.one}, int_T), 0), blanchet@35220: ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0), blanchet@35220: ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0), blanchet@35220: ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0), blanchet@35220: ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0), blanchet@35220: ((@{const_name uminus_class.uminus}, int_T --> int_T), 0), blanchet@35220: ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2), blanchet@35220: ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)] blanchet@35220: val built_in_typed_nat_consts = blanchet@35220: [((@{const_name zero_class.zero}, nat_T), 0), blanchet@35220: ((@{const_name one_class.one}, nat_T), 0), blanchet@35220: ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0), blanchet@35220: ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0), blanchet@35220: ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0), blanchet@35220: ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0), blanchet@35220: ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2), blanchet@35220: ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2), blanchet@35220: ((@{const_name of_nat}, nat_T --> int_T), 0)] blanchet@33192: val built_in_set_consts = blanchet@35220: [(@{const_name semilattice_inf_class.inf}, 2), blanchet@35220: (@{const_name semilattice_sup_class.sup}, 2), blanchet@35220: (@{const_name minus_class.minus}, 2), blanchet@35220: (@{const_name ord_class.less_eq}, 2)] blanchet@33192: blanchet@33192: (* typ -> typ *) blanchet@35190: fun unarize_type @{typ "unsigned_bit word"} = nat_T blanchet@35190: | unarize_type @{typ "signed_bit word"} = int_T blanchet@35190: | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) blanchet@35190: | unarize_type T = T blanchet@35665: fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) = blanchet@35665: unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) blanchet@35665: | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = blanchet@35665: unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) blanchet@35665: | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = blanchet@35665: Type (@{type_name "*"}, map unarize_unbox_etc_type Ts) blanchet@35665: | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T blanchet@35665: | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T blanchet@35665: | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = blanchet@35665: Type (s, map unarize_unbox_etc_type Ts) blanchet@35665: | unarize_unbox_etc_type T = T blanchet@35280: fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts) blanchet@35280: | uniterize_type @{typ bisim_iterator} = nat_T blanchet@35280: | uniterize_type T = T blanchet@35665: val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type blanchet@35280: blanchet@33192: (* Proof.context -> typ -> string *) blanchet@35665: fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type blanchet@33192: blanchet@33192: (* string -> string -> string *) blanchet@33192: val prefix_name = Long_Name.qualify o Long_Name.base_name blanchet@33192: (* string -> string *) blanchet@34118: fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" blanchet@33192: (* string -> term -> term *) blanchet@33192: val prefix_abs_vars = Term.map_abs_vars o prefix_name blanchet@33192: (* string -> string *) blanchet@34118: fun short_name s = blanchet@33192: case space_explode name_sep s of blanchet@33192: [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix blanchet@34118: | ss => map shortest_name ss |> space_implode "_" blanchet@34118: (* typ -> typ *) blanchet@34118: fun shorten_names_in_type (Type (s, Ts)) = blanchet@34118: Type (short_name s, map shorten_names_in_type Ts) blanchet@34118: | shorten_names_in_type T = T blanchet@33192: (* term -> term *) blanchet@34118: val shorten_names_in_term = blanchet@34118: map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t) blanchet@34118: #> map_types shorten_names_in_type blanchet@33192: blanchet@33192: (* theory -> typ * typ -> bool *) blanchet@35665: fun strict_type_match thy (T1, T2) = blanchet@33192: (Sign.typ_match thy (T2, T1) Vartab.empty; true) blanchet@33192: handle Type.TYPE_MATCH => false blanchet@35665: fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type blanchet@33192: (* theory -> styp * styp -> bool *) blanchet@33192: fun const_match thy ((s1, T1), (s2, T2)) = blanchet@33192: s1 = s2 andalso type_match thy (T1, T2) blanchet@33192: (* theory -> term * term -> bool *) blanchet@33192: fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) blanchet@33192: | term_match thy (Free (s1, T1), Free (s2, T2)) = blanchet@34118: const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) blanchet@35280: | term_match _ (t1, t2) = t1 aconv t2 blanchet@33192: blanchet@33192: (* typ -> bool *) blanchet@33192: fun is_TFree (TFree _) = true blanchet@33192: | is_TFree _ = false blanchet@35665: fun is_higher_order_type (Type (@{type_name fun}, _)) = true blanchet@33192: | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts blanchet@33192: | is_higher_order_type _ = false blanchet@35665: fun is_fun_type (Type (@{type_name fun}, _)) = true blanchet@33192: | is_fun_type _ = false blanchet@35665: fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true blanchet@33192: | is_set_type _ = false blanchet@35665: fun is_pair_type (Type (@{type_name "*"}, _)) = true blanchet@33192: | is_pair_type _ = false blanchet@33192: fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s blanchet@33192: | is_lfp_iterator_type _ = false blanchet@33192: fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s blanchet@33192: | is_gfp_iterator_type _ = false blanchet@33192: val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type blanchet@35280: fun is_iterator_type T = blanchet@35280: (T = @{typ bisim_iterator} orelse is_fp_iterator_type T) blanchet@34118: fun is_boolean_type T = (T = prop_T orelse T = bool_T) blanchet@35220: fun is_integer_type T = (T = nat_T orelse T = int_T) blanchet@34121: fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit}) blanchet@34121: fun is_word_type (Type (@{type_name word}, _)) = true blanchet@34121: | is_word_type _ = false blanchet@35280: val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type blanchet@33192: val is_record_type = not o null o Record.dest_recTs blanchet@33192: (* theory -> typ -> bool *) blanchet@33192: fun is_frac_type thy (Type (s, [])) = blanchet@33574: not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) blanchet@33192: | is_frac_type _ _ = false blanchet@35220: fun is_number_type thy = is_integer_like_type orf is_frac_type thy blanchet@33192: blanchet@33192: (* bool -> styp -> typ *) blanchet@33192: fun iterator_type_for_const gfp (s, T) = blanchet@33192: Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, blanchet@33192: binder_types T) blanchet@33192: (* typ -> styp *) blanchet@33192: fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T) blanchet@33192: | const_for_iterator_type T = blanchet@33224: raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) blanchet@33192: blanchet@35067: (* int -> typ -> typ list * typ *) blanchet@33192: fun strip_n_binders 0 T = ([], T) blanchet@35665: | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) = blanchet@33192: strip_n_binders (n - 1) T2 |>> cons T1 blanchet@33192: | strip_n_binders n (Type (@{type_name fun_box}, Ts)) = blanchet@35665: strip_n_binders n (Type (@{type_name fun}, Ts)) blanchet@33224: | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) blanchet@33192: (* typ -> typ *) blanchet@33192: val nth_range_type = snd oo strip_n_binders blanchet@33192: blanchet@33192: (* typ -> int *) blanchet@35665: fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) = blanchet@33192: fold (Integer.add o num_factors_in_type) [T1, T2] 0 blanchet@33192: | num_factors_in_type _ = 1 blanchet@35665: fun num_binder_types (Type (@{type_name fun}, [_, T2])) = blanchet@35665: 1 + num_binder_types T2 blanchet@33192: | num_binder_types _ = 0 blanchet@33192: (* typ -> typ list *) blanchet@33192: val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types blanchet@33192: fun maybe_curried_binder_types T = blanchet@33192: (if is_pair_type (body_type T) then binder_types else curried_binder_types) T blanchet@33192: blanchet@33192: (* typ -> term list -> term *) blanchet@33192: fun mk_flat_tuple _ [t] = t blanchet@35665: | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) = blanchet@33192: HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) blanchet@33224: | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) blanchet@33192: (* int -> term -> term list *) blanchet@33192: fun dest_n_tuple 1 t = [t] blanchet@33192: | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: blanchet@33192: blanchet@33192: (* int -> typ -> typ list *) blanchet@33192: fun dest_n_tuple_type 1 T = [T] blanchet@33192: | dest_n_tuple_type n (Type (_, [T1, T2])) = blanchet@33192: T1 :: dest_n_tuple_type (n - 1) T2 blanchet@33224: | dest_n_tuple_type _ T = blanchet@33224: raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) blanchet@33192: blanchet@35220: type typedef_info = blanchet@35220: {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, blanchet@35220: set_def: thm option, prop_of_Rep: thm, set_name: string, blanchet@35220: Abs_inverse: thm option, Rep_inverse: thm option} blanchet@35220: blanchet@35220: (* theory -> string -> typedef_info *) blanchet@35220: fun typedef_info thy s = blanchet@35220: if is_frac_type thy (Type (s, [])) then blanchet@35220: SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, blanchet@35220: Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, blanchet@35220: set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \ Frac"} blanchet@35220: |> Logic.varify, blanchet@35220: set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} blanchet@35220: else case Typedef.get_info thy s of blanchet@35220: SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, blanchet@35220: Rep_inverse, ...} => blanchet@35220: SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, blanchet@35220: Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, blanchet@35220: set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, blanchet@35220: Rep_inverse = SOME Rep_inverse} blanchet@35220: | NONE => NONE blanchet@35220: blanchet@35220: (* theory -> string -> bool *) blanchet@35220: val is_typedef = is_some oo typedef_info blanchet@35220: val is_real_datatype = is_some oo Datatype.get_info blanchet@35220: (* theory -> (typ option * bool) list -> typ -> bool *) blanchet@35220: fun is_standard_datatype thy = the oo triple_lookup (type_match thy) blanchet@35220: blanchet@34118: (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", blanchet@34118: e.g., by adding a field to "Datatype_Aux.info". *) blanchet@35220: (* theory -> (typ option * bool) list -> string -> bool *) blanchet@35220: fun is_basic_datatype thy stds s = blanchet@35220: member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit}, blanchet@35220: @{type_name int}, "Code_Numeral.code_numeral"] s orelse blanchet@35220: (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) blanchet@34118: blanchet@33192: (* theory -> typ -> typ -> typ -> typ *) blanchet@33192: fun instantiate_type thy T1 T1' T2 = blanchet@33192: Same.commit (Envir.subst_type_same blanchet@35311: (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 blanchet@33192: handle Type.TYPE_MATCH => blanchet@33224: raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) blanchet@35311: fun varify_and_instantiate_type thy T1 T1' T2 = blanchet@35311: instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) blanchet@33192: blanchet@33192: (* theory -> typ -> typ -> styp *) blanchet@33192: fun repair_constr_type thy body_T' T = blanchet@35311: varify_and_instantiate_type thy (body_type T) body_T' T blanchet@33192: blanchet@33192: (* string -> (string * string) list -> theory -> theory *) blanchet@33192: fun register_frac_type frac_s ersaetze thy = blanchet@33192: let blanchet@33574: val {frac_types, codatatypes} = Data.get thy blanchet@33192: val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types blanchet@33574: in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end blanchet@33192: (* string -> theory -> theory *) blanchet@33192: fun unregister_frac_type frac_s = register_frac_type frac_s [] blanchet@33192: blanchet@33192: (* typ -> string -> styp list -> theory -> theory *) blanchet@33192: fun register_codatatype co_T case_name constr_xs thy = blanchet@33192: let blanchet@33574: val {frac_types, codatatypes} = Data.get thy blanchet@33192: val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs blanchet@33192: val (co_s, co_Ts) = dest_Type co_T blanchet@33192: val _ = blanchet@34923: if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso blanchet@35665: co_s <> @{type_name fun} andalso blanchet@35220: not (is_basic_datatype thy [(NONE, true)] co_s) then blanchet@34118: () blanchet@34118: else blanchet@34118: raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) blanchet@33192: val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) blanchet@33192: codatatypes blanchet@33574: in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end blanchet@33192: (* typ -> theory -> theory *) blanchet@33192: fun unregister_codatatype co_T = register_codatatype co_T "" [] blanchet@33192: blanchet@33192: (* theory -> typ -> bool *) blanchet@35284: fun is_quot_type thy (Type (s, _)) = blanchet@35284: is_some (Quotient_Info.quotdata_lookup_raw thy s) blanchet@34923: | is_quot_type _ _ = false blanchet@35280: fun is_codatatype thy (Type (s, _)) = blanchet@33574: not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s blanchet@33192: |> Option.map snd |> these)) blanchet@33192: | is_codatatype _ _ = false blanchet@33192: fun is_pure_typedef thy (T as Type (s, _)) = blanchet@33192: is_typedef thy s andalso blanchet@34923: not (is_real_datatype thy s orelse is_quot_type thy T orelse blanchet@35220: is_codatatype thy T orelse is_record_type T orelse blanchet@35220: is_integer_like_type T) blanchet@33192: | is_pure_typedef _ _ = false blanchet@33192: fun is_univ_typedef thy (Type (s, _)) = blanchet@33192: (case typedef_info thy s of blanchet@33192: SOME {set_def, prop_of_Rep, ...} => blanchet@35332: let blanchet@35332: val t_opt = blanchet@35332: case set_def of blanchet@35332: SOME thm => try (snd o Logic.dest_equals o prop_of) thm blanchet@35332: | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) blanchet@35332: prop_of_Rep blanchet@35332: in blanchet@35332: case t_opt of blanchet@35332: SOME (Const (@{const_name top}, _)) => true blanchet@35386: (* "Multiset.multiset" *) blanchet@35332: | SOME (Const (@{const_name Collect}, _) blanchet@35332: $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true blanchet@35386: (* "FinFun.finfun" *) blanchet@35386: | SOME (Const (@{const_name Collect}, _) $ Abs (_, _, blanchet@35386: Const (@{const_name Ex}, _) $ Abs (_, _, blanchet@35386: Const (@{const_name finite}, _) $ _))) => true blanchet@35332: | _ => false blanchet@35332: end blanchet@33192: | NONE => false) blanchet@33192: | is_univ_typedef _ _ = false blanchet@35220: (* theory -> (typ option * bool) list -> typ -> bool *) blanchet@35220: fun is_datatype thy stds (T as Type (s, _)) = blanchet@34923: (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse blanchet@35220: is_quot_type thy T) andalso not (is_basic_datatype thy stds s) blanchet@35220: | is_datatype _ _ _ = false blanchet@33192: blanchet@33192: (* theory -> typ -> (string * typ) list * (string * typ) *) blanchet@33192: fun all_record_fields thy T = blanchet@33192: let val (recs, more) = Record.get_extT_fields thy T in blanchet@33192: recs @ more :: all_record_fields thy (snd more) blanchet@33192: end blanchet@33192: handle TYPE _ => [] blanchet@33192: (* styp -> bool *) blanchet@35280: fun is_record_constr (s, T) = blanchet@33192: String.isSuffix Record.extN s andalso blanchet@33192: let val dataT = body_type T in blanchet@33192: is_record_type dataT andalso blanchet@33192: s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN blanchet@33192: end blanchet@33192: (* theory -> typ -> int *) blanchet@33192: val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields blanchet@33192: (* theory -> string -> typ -> int *) blanchet@33192: fun no_of_record_field thy s T1 = blanchet@34118: find_index (curry (op =) s o fst) blanchet@34118: (Record.get_extT_fields thy T1 ||> single |> op @) blanchet@33192: (* theory -> styp -> bool *) blanchet@35665: fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) = blanchet@34118: exists (curry (op =) s o fst) (all_record_fields thy T1) blanchet@33192: | is_record_get _ _ = false blanchet@33192: fun is_record_update thy (s, T) = blanchet@33192: String.isSuffix Record.updateN s andalso blanchet@34118: exists (curry (op =) (unsuffix Record.updateN s) o fst) blanchet@33192: (all_record_fields thy (body_type T)) blanchet@33192: handle TYPE _ => false blanchet@35665: fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) = blanchet@33192: (case typedef_info thy s' of blanchet@33192: SOME {Abs_name, ...} => s = Abs_name blanchet@33192: | NONE => false) blanchet@33192: | is_abs_fun _ _ = false blanchet@35665: fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) = blanchet@33192: (case typedef_info thy s' of blanchet@33192: SOME {Rep_name, ...} => s = Rep_name blanchet@33192: | NONE => false) blanchet@33192: | is_rep_fun _ _ = false blanchet@34923: (* Proof.context -> styp -> bool *) blanchet@35665: fun is_quot_abs_fun ctxt blanchet@35665: (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) = blanchet@35284: (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' blanchet@35284: = SOME (Const x)) blanchet@34923: | is_quot_abs_fun _ _ = false blanchet@35665: fun is_quot_rep_fun ctxt blanchet@35665: (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) = blanchet@35284: (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' blanchet@35284: = SOME (Const x)) blanchet@34923: | is_quot_rep_fun _ _ = false blanchet@33192: blanchet@33192: (* theory -> styp -> styp *) blanchet@35665: fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun}, blanchet@35665: [T1 as Type (s', _), T2]))) = blanchet@33192: (case typedef_info thy s' of blanchet@35665: SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1])) blanchet@33224: | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) blanchet@33224: | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) blanchet@34923: (* theory -> typ -> typ *) blanchet@35284: fun rep_type_for_quot_type thy (T as Type (s, _)) = blanchet@35284: let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in blanchet@35284: instantiate_type thy qtyp T rtyp blanchet@35284: end blanchet@34923: (* theory -> typ -> term *) blanchet@35284: fun equiv_relation_for_quot_type thy (Type (s, Ts)) = blanchet@35284: let blanchet@35284: val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s blanchet@35284: val Ts' = qtyp |> dest_Type |> snd blanchet@35284: in subst_atomic_types (Ts' ~~ Ts) equiv_rel end blanchet@34923: | equiv_relation_for_quot_type _ T = blanchet@34923: raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) blanchet@33192: blanchet@33192: (* theory -> styp -> bool *) blanchet@33192: fun is_coconstr thy (s, T) = blanchet@33192: let blanchet@33574: val {codatatypes, ...} = Data.get thy blanchet@33192: val co_T = body_type T blanchet@33192: val co_s = dest_Type co_T |> fst blanchet@33192: in blanchet@33192: exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T) blanchet@33192: (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) blanchet@33192: end blanchet@33192: handle TYPE ("dest_Type", _, _) => false blanchet@33192: fun is_constr_like thy (s, T) = blanchet@35665: member (op =) [@{const_name FinFun}, @{const_name FunBox}, blanchet@35665: @{const_name PairBox}, @{const_name Quot}, blanchet@35665: @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse blanchet@35665: let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in blanchet@34923: Refute.is_IDT_constructor thy x orelse is_record_constr x orelse blanchet@34923: (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse blanchet@34923: is_coconstr thy x blanchet@33192: end blanchet@33572: fun is_stale_constr thy (x as (_, T)) = blanchet@34923: is_codatatype thy (body_type T) andalso is_constr_like thy x andalso blanchet@34923: not (is_coconstr thy x) blanchet@35220: (* theory -> (typ option * bool) list -> styp -> bool *) blanchet@35220: fun is_constr thy stds (x as (_, T)) = blanchet@34923: is_constr_like thy x andalso blanchet@35220: not (is_basic_datatype thy stds blanchet@35220: (fst (dest_Type (unarize_type (body_type T))))) andalso blanchet@34923: not (is_stale_constr thy x) blanchet@33192: (* string -> bool *) blanchet@33192: val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix blanchet@33192: val is_sel_like_and_no_discr = blanchet@35665: String.isPrefix sel_prefix orf blanchet@35665: (member (op =) [@{const_name fst}, @{const_name snd}]) blanchet@33192: blanchet@33192: (* boxability -> boxability *) blanchet@33192: fun in_fun_lhs_for InConstr = InSel blanchet@33192: | in_fun_lhs_for _ = InFunLHS blanchet@33192: fun in_fun_rhs_for InConstr = InConstr blanchet@33192: | in_fun_rhs_for InSel = InSel blanchet@33192: | in_fun_rhs_for InFunRHS1 = InFunRHS2 blanchet@33192: | in_fun_rhs_for _ = InFunRHS1 blanchet@33192: blanchet@35067: (* hol_context -> boxability -> typ -> bool *) blanchet@35067: fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = blanchet@33192: case T of blanchet@35665: Type (@{type_name fun}, _) => blanchet@34923: (boxy = InPair orelse boxy = InFunLHS) andalso blanchet@34923: not (is_boolean_type (body_type T)) blanchet@35665: | Type (@{type_name "*"}, Ts) => blanchet@34923: boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse blanchet@34923: ((boxy = InExpr orelse boxy = InFunLHS) andalso blanchet@35067: exists (is_boxing_worth_it hol_ctxt InPair) blanchet@35067: (map (box_type hol_ctxt InPair) Ts)) blanchet@33192: | _ => false blanchet@35067: (* hol_context -> boxability -> string * typ list -> string *) blanchet@35280: and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z = blanchet@33192: case triple_lookup (type_match thy) boxes (Type z) of blanchet@33192: SOME (SOME box_me) => box_me blanchet@35067: | _ => is_boxing_worth_it hol_ctxt boxy (Type z) blanchet@35067: (* hol_context -> boxability -> typ -> typ *) blanchet@35067: and box_type hol_ctxt boxy T = blanchet@33192: case T of blanchet@35665: Type (z as (@{type_name fun}, [T1, T2])) => blanchet@34923: if boxy <> InConstr andalso boxy <> InSel andalso blanchet@35067: should_box_type hol_ctxt boxy z then blanchet@33192: Type (@{type_name fun_box}, blanchet@35067: [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2]) blanchet@33192: else blanchet@35067: box_type hol_ctxt (in_fun_lhs_for boxy) T1 blanchet@35067: --> box_type hol_ctxt (in_fun_rhs_for boxy) T2 blanchet@35665: | Type (z as (@{type_name "*"}, Ts)) => blanchet@34969: if boxy <> InConstr andalso boxy <> InSel blanchet@35067: andalso should_box_type hol_ctxt boxy z then blanchet@35067: Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) blanchet@33192: else blanchet@35665: Type (@{type_name "*"}, blanchet@35665: map (box_type hol_ctxt blanchet@34118: (if boxy = InConstr orelse boxy = InSel then boxy blanchet@34118: else InPair)) Ts) blanchet@33192: | _ => T blanchet@33192: blanchet@35190: (* typ -> typ *) blanchet@35190: fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} blanchet@35190: | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} blanchet@35190: | binarize_nat_and_int_in_type (Type (s, Ts)) = blanchet@35190: Type (s, map binarize_nat_and_int_in_type Ts) blanchet@35190: | binarize_nat_and_int_in_type T = T blanchet@35190: (* term -> term *) blanchet@35190: val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type blanchet@35190: blanchet@33192: (* styp -> styp *) blanchet@33192: fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T) blanchet@33192: blanchet@33192: (* typ -> int *) blanchet@33192: fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) blanchet@33192: (* string -> int -> string *) blanchet@33192: fun nth_sel_name_for_constr_name s n = blanchet@33192: if s = @{const_name Pair} then blanchet@33192: if n = 0 then @{const_name fst} else @{const_name snd} blanchet@33192: else blanchet@33192: sel_prefix_for n ^ s blanchet@33192: (* styp -> int -> styp *) blanchet@33192: fun nth_sel_for_constr x ~1 = discr_for_constr x blanchet@33192: | nth_sel_for_constr (s, T) n = blanchet@33192: (nth_sel_name_for_constr_name s n, blanchet@33192: body_type T --> nth (maybe_curried_binder_types T) n) blanchet@35190: (* hol_context -> bool -> styp -> int -> styp *) blanchet@35190: fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize = blanchet@35190: apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel) blanchet@35190: oo nth_sel_for_constr blanchet@33192: blanchet@33192: (* string -> int *) blanchet@33192: fun sel_no_from_name s = blanchet@33192: if String.isPrefix discr_prefix s then blanchet@33192: ~1 blanchet@33192: else if String.isPrefix sel_prefix s then blanchet@33192: s |> unprefix sel_prefix |> Int.fromString |> the blanchet@33192: else if s = @{const_name snd} then blanchet@33192: 1 blanchet@33192: else blanchet@33192: 0 blanchet@33192: blanchet@35075: (* term -> term *) blanchet@35075: val close_form = blanchet@35075: let blanchet@35075: (* (indexname * typ) list -> (indexname * typ) list -> term -> term *) blanchet@35075: fun close_up zs zs' = blanchet@35075: fold (fn (z as ((s, _), T)) => fn t' => blanchet@35075: Term.all T $ Abs (s, T, abstract_over (Var z, t'))) blanchet@35075: (take (length zs' - length zs) zs') blanchet@35075: (* (indexname * typ) list -> term -> term *) blanchet@35075: fun aux zs (@{const "==>"} $ t1 $ t2) = blanchet@35075: let val zs' = Term.add_vars t1 zs in blanchet@35075: close_up zs zs' (Logic.mk_implies (t1, aux zs' t2)) blanchet@35075: end blanchet@35075: | aux zs t = close_up zs (Term.add_vars t zs) t blanchet@35075: in aux [] end blanchet@35075: blanchet@33192: (* typ list -> term -> int -> term *) blanchet@33192: fun eta_expand _ t 0 = t blanchet@33192: | eta_expand Ts (Abs (s, T, t')) n = blanchet@33192: Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) blanchet@33192: | eta_expand Ts t n = blanchet@33192: fold_rev (curry3 Abs ("x\<^isub>\" ^ nat_subscript n)) blanchet@33192: (List.take (binder_types (fastype_of1 (Ts, t)), n)) blanchet@33192: (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) blanchet@33192: blanchet@33192: (* term -> term *) blanchet@33192: fun extensionalize t = blanchet@33192: case t of blanchet@33192: (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1 blanchet@33192: | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) => blanchet@33192: let val v = Var ((s, maxidx_of_term t + 1), T) in blanchet@33192: extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2))) blanchet@33192: end blanchet@33192: | _ => t blanchet@33192: blanchet@33192: (* typ -> term list -> term *) blanchet@33192: fun distinctness_formula T = blanchet@33192: all_distinct_unordered_pairs_of blanchet@33192: #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) blanchet@33192: #> List.foldr (s_conj o swap) @{const True} blanchet@33192: blanchet@33192: (* typ -> term *) blanchet@35220: fun zero_const T = Const (@{const_name zero_class.zero}, T) blanchet@33192: fun suc_const T = Const (@{const_name Suc}, T --> T) blanchet@33192: blanchet@35220: (* hol_context -> typ -> styp list *) blanchet@35220: fun uncached_datatype_constrs ({thy, stds, ...} : hol_context) blanchet@35220: (T as Type (s, Ts)) = blanchet@33574: (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of blanchet@34969: SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' blanchet@33572: | _ => blanchet@35220: if is_datatype thy stds T then blanchet@33572: case Datatype.get_info thy s of blanchet@33572: SOME {index, descr, ...} => blanchet@33572: let blanchet@33572: val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the blanchet@33572: in blanchet@33572: map (fn (s', Us) => blanchet@33572: (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us blanchet@33572: ---> T)) constrs blanchet@33572: end blanchet@33572: | NONE => blanchet@33572: if is_record_type T then blanchet@33572: let blanchet@33572: val s' = unsuffix Record.ext_typeN s ^ Record.extN blanchet@33572: val T' = (Record.get_extT_fields thy T blanchet@33572: |> apsnd single |> uncurry append |> map snd) ---> T blanchet@33572: in [(s', T')] end blanchet@34923: else if is_quot_type thy T then blanchet@34923: [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)] blanchet@33572: else case typedef_info thy s of blanchet@33572: SOME {abs_type, rep_type, Abs_name, ...} => blanchet@35311: [(Abs_name, blanchet@35311: varify_and_instantiate_type thy abs_type T rep_type --> T)] blanchet@33572: | NONE => blanchet@33572: if T = @{typ ind} then blanchet@33572: [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] blanchet@33572: else blanchet@33572: [] blanchet@33572: else blanchet@33572: []) blanchet@33571: | uncached_datatype_constrs _ _ = [] blanchet@35067: (* hol_context -> typ -> styp list *) blanchet@35220: fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T = blanchet@33571: case AList.lookup (op =) (!constr_cache) T of blanchet@33571: SOME xs => xs blanchet@33571: | NONE => blanchet@35220: let val xs = uncached_datatype_constrs hol_ctxt T in blanchet@33571: (Unsynchronized.change constr_cache (cons (T, xs)); xs) blanchet@33571: end blanchet@35190: (* hol_context -> bool -> typ -> styp list *) blanchet@35190: fun binarized_and_boxed_datatype_constrs hol_ctxt binarize = blanchet@35190: map (apsnd ((binarize ? binarize_nat_and_int_in_type) blanchet@35190: o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt blanchet@35067: (* hol_context -> typ -> int *) blanchet@33192: val num_datatype_constrs = length oo datatype_constrs blanchet@33192: blanchet@33192: (* string -> string *) blanchet@33192: fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair} blanchet@33192: | constr_name_for_sel_like @{const_name snd} = @{const_name Pair} blanchet@33192: | constr_name_for_sel_like s' = original_name s' blanchet@35190: (* hol_context -> bool -> styp -> styp *) blanchet@35190: fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') = blanchet@33192: let val s = constr_name_for_sel_like s' in blanchet@35190: AList.lookup (op =) blanchet@35190: (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T')) blanchet@35190: s blanchet@33192: |> the |> pair s blanchet@33192: end blanchet@34969: blanchet@35067: (* hol_context -> styp -> term *) blanchet@35067: fun discr_term_for_constr hol_ctxt (x as (s, T)) = blanchet@33192: let val dataT = body_type T in blanchet@33192: if s = @{const_name Suc} then blanchet@33192: Abs (Name.uu, dataT, blanchet@33192: @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) blanchet@35067: else if num_datatype_constrs hol_ctxt dataT >= 2 then blanchet@33192: Const (discr_for_constr x) blanchet@33192: else blanchet@33192: Abs (Name.uu, dataT, @{const True}) blanchet@33192: end blanchet@35067: (* hol_context -> styp -> term -> term *) blanchet@35280: fun discriminate_value (hol_ctxt as {thy, ...}) x t = blanchet@35280: case head_of t of blanchet@35280: Const x' => blanchet@33192: if x = x' then @{const True} blanchet@33192: else if is_constr_like thy x' then @{const False} blanchet@35067: else betapply (discr_term_for_constr hol_ctxt x, t) blanchet@35067: | _ => betapply (discr_term_for_constr hol_ctxt x, t) blanchet@33192: blanchet@35220: (* theory -> (typ option * bool) list -> styp -> term -> term *) blanchet@35220: fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n = blanchet@33192: let val (arg_Ts, dataT) = strip_type T in blanchet@35220: if dataT = nat_T andalso is_standard_datatype thy stds nat_T then blanchet@35220: @{term "%n::nat. n - 1"} blanchet@33192: else if is_pair_type dataT then blanchet@33192: Const (nth_sel_for_constr x n) blanchet@33192: else blanchet@33192: let blanchet@33192: (* int -> typ -> int * term *) blanchet@35665: fun aux m (Type (@{type_name "*"}, [T1, T2])) = blanchet@33192: let blanchet@33192: val (m, t1) = aux m T1 blanchet@33192: val (m, t2) = aux m T2 blanchet@33192: in (m, HOLogic.mk_prod (t1, t2)) end blanchet@33192: | aux m T = blanchet@33192: (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T) blanchet@33192: $ Bound 0) blanchet@33192: val m = fold (Integer.add o num_factors_in_type) blanchet@33192: (List.take (arg_Ts, n)) 0 blanchet@33192: in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end blanchet@33192: end blanchet@35220: (* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *) blanchet@35220: fun select_nth_constr_arg thy stds x t n res_T = blanchet@35220: (case strip_comb t of blanchet@35220: (Const x', args) => blanchet@35220: if x = x' then nth args n blanchet@35220: else if is_constr_like thy x' then Const (@{const_name unknown}, res_T) blanchet@35220: else raise SAME () blanchet@35220: | _ => raise SAME()) blanchet@35220: handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) blanchet@33192: blanchet@35220: (* theory -> (typ option * bool) list -> styp -> term list -> term *) blanchet@35220: fun construct_value _ _ x [] = Const x blanchet@35220: | construct_value thy stds (x as (s, _)) args = blanchet@33192: let val args = map Envir.eta_contract args in blanchet@33192: case hd args of blanchet@35280: Const (s', _) $ t => blanchet@34923: if is_sel_like_and_no_discr s' andalso blanchet@34923: constr_name_for_sel_like s' = s andalso blanchet@35220: forall (fn (n, t') => blanchet@35220: select_nth_constr_arg thy stds x t n dummyT = t') blanchet@34923: (index_seq 0 (length args) ~~ args) then blanchet@33192: t blanchet@33192: else blanchet@33192: list_comb (Const x, args) blanchet@33192: | _ => list_comb (Const x, args) blanchet@33192: end blanchet@33192: blanchet@35665: (* hol_context -> typ -> term -> term *) blanchet@35665: fun constr_expand (hol_ctxt as {thy, stds, ...}) T t = blanchet@35665: (case head_of t of blanchet@35665: Const x => if is_constr_like thy x then t else raise SAME () blanchet@35665: | _ => raise SAME ()) blanchet@35665: handle SAME () => blanchet@35665: let blanchet@35665: val x' as (_, T') = blanchet@35665: if is_pair_type T then blanchet@35665: let val (T1, T2) = HOLogic.dest_prodT T in blanchet@35665: (@{const_name Pair}, T1 --> T2 --> T) blanchet@35665: end blanchet@35665: else blanchet@35665: datatype_constrs hol_ctxt T |> hd blanchet@35665: val arg_Ts = binder_types T' blanchet@35665: in blanchet@35665: list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t) blanchet@35665: (index_seq 0 (length arg_Ts)) arg_Ts) blanchet@35665: end blanchet@35665: blanchet@35665: (* (term -> term) -> int -> term -> term *) blanchet@35665: fun coerce_bound_no f j t = blanchet@35665: case t of blanchet@35665: t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 blanchet@35665: | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') blanchet@35665: | Bound j' => if j' = j then f t else t blanchet@35665: | _ => t blanchet@35665: (* hol_context -> typ -> typ -> term -> term *) blanchet@35665: fun coerce_bound_0_in_term hol_ctxt new_T old_T = blanchet@35665: old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0 blanchet@35665: (* hol_context -> typ list -> typ -> typ -> term -> term *) blanchet@35665: and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t = blanchet@35665: if old_T = new_T then blanchet@35665: t blanchet@35665: else blanchet@35665: case (new_T, old_T) of blanchet@35665: (Type (new_s, new_Ts as [new_T1, new_T2]), blanchet@35665: Type (@{type_name fun}, [old_T1, old_T2])) => blanchet@35665: (case eta_expand Ts t 1 of blanchet@35665: Abs (s, _, t') => blanchet@35665: Abs (s, new_T1, blanchet@35665: t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 blanchet@35665: |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) blanchet@35665: |> Envir.eta_contract blanchet@35665: |> new_s <> @{type_name fun} blanchet@35665: ? construct_value thy stds blanchet@35665: (if new_s = @{type_name fin_fun} then @{const_name FinFun} blanchet@35665: else @{const_name FunBox}, blanchet@35665: Type (@{type_name fun}, new_Ts) --> new_T) blanchet@35665: o single blanchet@35665: | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) blanchet@35665: | (Type (new_s, new_Ts as [new_T1, new_T2]), blanchet@35665: Type (old_s, old_Ts as [old_T1, old_T2])) => blanchet@35665: if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse blanchet@35665: old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then blanchet@35665: case constr_expand hol_ctxt old_T t of blanchet@35665: Const (old_s, _) $ t1 => blanchet@35665: if new_s = @{type_name fun} then blanchet@35665: coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1 blanchet@35665: else blanchet@35665: construct_value thy stds blanchet@35665: (old_s, Type (@{type_name fun}, new_Ts) --> new_T) blanchet@35665: [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts)) blanchet@35665: (Type (@{type_name fun}, old_Ts)) t1] blanchet@35665: | Const _ $ t1 $ t2 => blanchet@35665: construct_value thy stds blanchet@35665: (if new_s = @{type_name "*"} then @{const_name Pair} blanchet@35665: else @{const_name PairBox}, new_Ts ---> new_T) blanchet@35665: (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] blanchet@35665: [t1, t2]) blanchet@35665: | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) blanchet@35665: else blanchet@35665: raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) blanchet@35665: | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) blanchet@35665: blanchet@33192: (* (typ * int) list -> typ -> int *) blanchet@35665: fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = blanchet@34120: reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) blanchet@35665: | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) = blanchet@34120: card_of_type assigns T1 * card_of_type assigns T2 blanchet@33192: | card_of_type _ (Type (@{type_name itself}, _)) = 1 blanchet@33192: | card_of_type _ @{typ prop} = 2 blanchet@33192: | card_of_type _ @{typ bool} = 2 blanchet@33192: | card_of_type _ @{typ unit} = 1 blanchet@34120: | card_of_type assigns T = blanchet@34120: case AList.lookup (op =) assigns T of blanchet@33192: SOME k => k blanchet@33192: | NONE => if T = @{typ bisim_iterator} then 0 blanchet@33224: else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) blanchet@33192: (* int -> (typ * int) list -> typ -> int *) blanchet@35665: fun bounded_card_of_type max default_card assigns blanchet@35665: (Type (@{type_name fun}, [T1, T2])) = blanchet@33192: let blanchet@34120: val k1 = bounded_card_of_type max default_card assigns T1 blanchet@34120: val k2 = bounded_card_of_type max default_card assigns T2 blanchet@33192: in blanchet@33192: if k1 = max orelse k2 = max then max blanchet@33192: else Int.min (max, reasonable_power k2 k1) blanchet@33192: end blanchet@35665: | bounded_card_of_type max default_card assigns blanchet@35665: (Type (@{type_name "*"}, [T1, T2])) = blanchet@33192: let blanchet@34120: val k1 = bounded_card_of_type max default_card assigns T1 blanchet@34120: val k2 = bounded_card_of_type max default_card assigns T2 blanchet@33192: in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end blanchet@34120: | bounded_card_of_type max default_card assigns T = blanchet@33192: Int.min (max, if default_card = ~1 then blanchet@34120: card_of_type assigns T blanchet@33192: else blanchet@34120: card_of_type assigns T blanchet@33224: handle TYPE ("Nitpick_HOL.card_of_type", _, _) => blanchet@33192: default_card) blanchet@35385: (* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *) blanchet@35385: fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card blanchet@35385: assigns T = blanchet@33192: let blanchet@33192: (* typ list -> typ -> int *) blanchet@33192: fun aux avoid T = blanchet@34118: (if member (op =) avoid T then blanchet@33192: 0 blanchet@35385: else if member (op =) finitizable_dataTs T then blanchet@35385: raise SAME () blanchet@33192: else case T of blanchet@35665: Type (@{type_name fun}, [T1, T2]) => blanchet@33192: let blanchet@33192: val k1 = aux avoid T1 blanchet@33192: val k2 = aux avoid T2 blanchet@33192: in blanchet@33192: if k1 = 0 orelse k2 = 0 then 0 blanchet@33192: else if k1 >= max orelse k2 >= max then max blanchet@33192: else Int.min (max, reasonable_power k2 k1) blanchet@33192: end blanchet@35665: | Type (@{type_name "*"}, [T1, T2]) => blanchet@33192: let blanchet@33192: val k1 = aux avoid T1 blanchet@33192: val k2 = aux avoid T2 blanchet@33192: in blanchet@33192: if k1 = 0 orelse k2 = 0 then 0 blanchet@33192: else if k1 >= max orelse k2 >= max then max blanchet@33192: else Int.min (max, k1 * k2) blanchet@33192: end blanchet@33192: | Type (@{type_name itself}, _) => 1 blanchet@33192: | @{typ prop} => 2 blanchet@33192: | @{typ bool} => 2 blanchet@33192: | @{typ unit} => 1 blanchet@33192: | Type _ => blanchet@35067: (case datatype_constrs hol_ctxt T of blanchet@34123: [] => if is_integer_type T orelse is_bit_type T then 0 blanchet@34123: else raise SAME () blanchet@33192: | constrs => blanchet@33192: let blanchet@33192: val constr_cards = blanchet@35280: map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) blanchet@35280: constrs blanchet@33192: in blanchet@34118: if exists (curry (op =) 0) constr_cards then 0 blanchet@33192: else Integer.sum constr_cards blanchet@33192: end) blanchet@33192: | _ => raise SAME ()) blanchet@34120: handle SAME () => blanchet@34120: AList.lookup (op =) assigns T |> the_default default_card blanchet@33192: in Int.min (max, aux [] T) end blanchet@33192: blanchet@35665: val small_type_max_card = 5 blanchet@35665: blanchet@35067: (* hol_context -> typ -> bool *) blanchet@35384: fun is_finite_type hol_ctxt T = blanchet@35665: bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 blanchet@35665: (* hol_context -> typ -> bool *) blanchet@35665: fun is_small_finite_type hol_ctxt T = blanchet@35665: let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in blanchet@35665: n > 0 andalso n <= small_type_max_card blanchet@35665: end blanchet@33192: blanchet@33192: (* term -> bool *) blanchet@33192: fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 blanchet@33192: | is_ground_term (Const _) = true blanchet@33192: | is_ground_term _ = false blanchet@33192: blanchet@33192: (* term -> word -> word *) blanchet@33192: fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2) blanchet@33192: | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0) blanchet@33192: | hashw_term _ = 0w0 blanchet@33192: (* term -> int *) blanchet@33192: val hash_term = Word.toInt o hashw_term blanchet@33192: blanchet@33192: (* term list -> (indexname * typ) list *) blanchet@33192: fun special_bounds ts = wenzelm@35408: fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) blanchet@33192: blanchet@33192: (* indexname * typ -> term -> term *) blanchet@33192: fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) blanchet@33192: blanchet@33562: (* theory -> string -> bool *) blanchet@33562: fun is_funky_typedef_name thy s = blanchet@34118: member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, blanchet@34923: @{type_name int}] s orelse blanchet@34923: is_frac_type thy (Type (s, [])) blanchet@35067: (* theory -> typ -> bool *) blanchet@33562: fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s blanchet@33562: | is_funky_typedef _ _ = false blanchet@33192: (* term -> bool *) blanchet@33192: fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _) blanchet@33192: $ Const (@{const_name TYPE}, _)) = true blanchet@33192: | is_arity_type_axiom _ = false blanchet@33192: (* theory -> bool -> term -> bool *) blanchet@33197: fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) = blanchet@33197: is_typedef_axiom thy boring t2 blanchet@33197: | is_typedef_axiom thy boring blanchet@33192: (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) blanchet@35665: $ Const (_, Type (@{type_name fun}, [Type (s, _), _])) blanchet@35665: $ Const _ $ _)) = blanchet@33562: boring <> is_funky_typedef_name thy s andalso is_typedef thy s blanchet@33192: | is_typedef_axiom _ _ _ = false blanchet@33192: blanchet@33192: (* Distinguishes between (1) constant definition axioms, (2) type arity and blanchet@33192: typedef axioms, and (3) other axioms, and returns the pair ((1), (3)). blanchet@33192: Typedef axioms are uninteresting to Nitpick, because it can retrieve them blanchet@33192: using "typedef_info". *) blanchet@33192: (* theory -> (string * term) list -> string list -> term list * term list *) blanchet@33192: fun partition_axioms_by_definitionality thy axioms def_names = blanchet@33192: let blanchet@33192: val axioms = sort (fast_string_ord o pairself fst) axioms blanchet@33192: val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms blanchet@33192: val nondefs = blanchet@33192: OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms blanchet@33192: |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd) blanchet@33192: in pairself (map snd) (defs, nondefs) end blanchet@33192: blanchet@33197: (* Ideally we would check against "Complex_Main", not "Refute", but any theory blanchet@33197: will do as long as it contains all the "axioms" and "axiomatization" blanchet@33192: commands. *) blanchet@33192: (* theory -> bool *) blanchet@33192: fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute}) blanchet@33192: blanchet@33192: (* term -> bool *) blanchet@35283: val is_trivial_definition = blanchet@35283: the_default false o try (op aconv o Logic.dest_equals) blanchet@33192: val is_plain_definition = blanchet@33192: let blanchet@33192: (* term -> bool *) blanchet@33192: fun do_lhs t1 = blanchet@33192: case strip_comb t1 of blanchet@34923: (Const _, args) => blanchet@34923: forall is_Var args andalso not (has_duplicates (op =) args) blanchet@33192: | _ => false blanchet@33192: fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 blanchet@33192: | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) = blanchet@33192: do_lhs t1 blanchet@33192: | do_eq _ = false blanchet@33192: in do_eq end blanchet@33192: blanchet@35335: (* theory -> (term * term) list -> term list * term list * term list *) blanchet@35335: fun all_axioms_of thy subst = blanchet@33192: let blanchet@33192: (* theory list -> term list *) blanchet@35335: val axioms_of_thys = blanchet@35335: maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of)) blanchet@33192: val specs = Defs.all_specifications_of (Theory.defs_of thy) wenzelm@33701: val def_names = specs |> maps snd |> map_filter #def blanchet@33197: |> OrdList.make fast_string_ord blanchet@33192: val thys = thy :: Theory.ancestors_of thy blanchet@33192: val (built_in_thys, user_thys) = List.partition is_built_in_theory thys blanchet@33192: val built_in_axioms = axioms_of_thys built_in_thys blanchet@33192: val user_axioms = axioms_of_thys user_thys blanchet@33192: val (built_in_defs, built_in_nondefs) = blanchet@33192: partition_axioms_by_definitionality thy built_in_axioms def_names blanchet@33197: ||> filter (is_typedef_axiom thy false) blanchet@33192: val (user_defs, user_nondefs) = blanchet@33192: partition_axioms_by_definitionality thy user_axioms def_names blanchet@33197: val (built_in_nondefs, user_nondefs) = blanchet@33197: List.partition (is_typedef_axiom thy false) user_nondefs blanchet@33197: |>> append built_in_nondefs blanchet@34118: val defs = blanchet@34118: (thy |> PureThy.all_thms_of blanchet@34118: |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) blanchet@35283: |> map (prop_of o snd) blanchet@35283: |> filter_out is_trivial_definition blanchet@35283: |> filter is_plain_definition) @ blanchet@34118: user_defs @ built_in_defs blanchet@33192: in (defs, built_in_nondefs, user_nondefs) end blanchet@33192: blanchet@35220: (* theory -> (typ option * bool) list -> bool -> styp -> int option *) blanchet@35220: fun arity_of_built_in_const thy stds fast_descrs (s, T) = blanchet@33192: if s = @{const_name If} then blanchet@33192: if nth_range_type 3 T = @{typ bool} then NONE else SOME 3 blanchet@35220: else blanchet@35220: let val std_nats = is_standard_datatype thy stds nat_T in blanchet@35220: case AList.lookup (op =) blanchet@35220: (built_in_consts blanchet@35220: |> std_nats ? append built_in_nat_consts blanchet@35220: |> fast_descrs ? append built_in_descr_consts) s of blanchet@35220: SOME n => SOME n blanchet@35220: | NONE => blanchet@35220: case AList.lookup (op =) blanchet@35220: (built_in_typed_consts blanchet@35220: |> std_nats ? append built_in_typed_nat_consts) blanchet@35220: (s, unarize_type T) of blanchet@35220: SOME n => SOME n blanchet@35220: | NONE => blanchet@35280: case s of blanchet@35280: @{const_name zero_class.zero} => blanchet@35280: if is_iterator_type T then SOME 0 else NONE blanchet@35280: | @{const_name Suc} => blanchet@35280: if is_iterator_type (domain_type T) then SOME 0 else NONE blanchet@35280: | _ => if is_fun_type T andalso is_set_type (domain_type T) then blanchet@35280: AList.lookup (op =) built_in_set_consts s blanchet@35280: else blanchet@35280: NONE blanchet@35220: end blanchet@35220: (* theory -> (typ option * bool) list -> bool -> styp -> bool *) blanchet@35220: val is_built_in_const = is_some oooo arity_of_built_in_const blanchet@33192: blanchet@33192: (* This function is designed to work for both real definition axioms and blanchet@33192: simplification rules (equational specifications). *) blanchet@33192: (* term -> term *) blanchet@33192: fun term_under_def t = blanchet@33192: case t of blanchet@33192: @{const "==>"} $ _ $ t2 => term_under_def t2 blanchet@33192: | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1 blanchet@33192: | @{const Trueprop} $ t1 => term_under_def t1 blanchet@33192: | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1 blanchet@33192: | Abs (_, _, t') => term_under_def t' blanchet@33192: | t1 $ _ => term_under_def t1 blanchet@33192: | _ => t blanchet@33192: blanchet@33192: (* Here we crucially rely on "Refute.specialize_type" performing a preorder blanchet@33192: traversal of the term, without which the wrong occurrence of a constant could blanchet@33192: be matched in the face of overloading. *) blanchet@35220: (* theory -> (typ option * bool) list -> bool -> const_table -> styp blanchet@35220: -> term list *) blanchet@35220: fun def_props_for_const thy stds fast_descrs table (x as (s, _)) = blanchet@35220: if is_built_in_const thy stds fast_descrs x then blanchet@33192: [] blanchet@33192: else blanchet@33192: these (Symtab.lookup table s) blanchet@33192: |> map_filter (try (Refute.specialize_type thy x)) blanchet@34118: |> filter (curry (op =) (Const x) o term_under_def) blanchet@33192: blanchet@35280: (* term -> term option *) blanchet@35280: fun normalized_rhs_of t = blanchet@33192: let blanchet@33743: (* term option -> term option *) blanchet@33743: fun aux (v as Var _) (SOME t) = SOME (lambda v t) blanchet@35280: | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t) blanchet@33743: | aux _ _ = NONE blanchet@33192: val (lhs, rhs) = blanchet@33192: case t of blanchet@33192: Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2) blanchet@33192: | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) => blanchet@33192: (t1, t2) blanchet@33224: | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) blanchet@33192: val args = strip_comb lhs |> snd blanchet@33743: in fold_rev aux args (SOME rhs) end blanchet@33192: blanchet@33192: (* theory -> const_table -> styp -> term option *) blanchet@33192: fun def_of_const thy table (x as (s, _)) = blanchet@35220: if is_built_in_const thy [(NONE, false)] false x orelse blanchet@35220: original_name s <> s then blanchet@33192: NONE blanchet@33192: else blanchet@35220: x |> def_props_for_const thy [(NONE, false)] false table |> List.last blanchet@35280: |> normalized_rhs_of |> Option.map (prefix_abs_vars s) blanchet@33192: handle List.Empty => NONE blanchet@33192: blanchet@33192: (* term -> fixpoint_kind *) blanchet@33192: fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t blanchet@33192: | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp blanchet@33192: | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp blanchet@33192: | fixpoint_kind_of_rhs _ = NoFp blanchet@33192: blanchet@33192: (* theory -> const_table -> term -> bool *) blanchet@33192: fun is_mutually_inductive_pred_def thy table t = blanchet@33192: let blanchet@33192: (* term -> bool *) blanchet@33192: fun is_good_arg (Bound _) = true blanchet@33192: | is_good_arg (Const (s, _)) = blanchet@34923: s = @{const_name True} orelse s = @{const_name False} orelse blanchet@34923: s = @{const_name undefined} blanchet@33192: | is_good_arg _ = false blanchet@33192: in blanchet@33192: case t |> strip_abs_body |> strip_comb of blanchet@33192: (Const x, ts as (_ :: _)) => blanchet@33192: (case def_of_const thy table x of blanchet@33192: SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts blanchet@33192: | NONE => false) blanchet@33192: | _ => false blanchet@33192: end blanchet@33192: (* theory -> const_table -> term -> term *) blanchet@33192: fun unfold_mutually_inductive_preds thy table = blanchet@33192: map_aterms (fn t as Const x => blanchet@33192: (case def_of_const thy table x of blanchet@33192: SOME t' => blanchet@33192: let val t' = Envir.eta_contract t' in blanchet@33192: if is_mutually_inductive_pred_def thy table t' then t' blanchet@33192: else t blanchet@33192: end blanchet@33192: | NONE => t) blanchet@33192: | t => t) blanchet@33192: blanchet@33192: (* term -> string * term *) blanchet@33192: fun pair_for_prop t = blanchet@33192: case term_under_def t of blanchet@33192: Const (s, _) => (s, t) blanchet@33224: | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) blanchet@33192: blanchet@35335: (* (Proof.context -> term list) -> Proof.context -> (term * term) list blanchet@35335: -> const_table *) blanchet@35335: fun table_for get ctxt subst = blanchet@35335: ctxt |> get |> map (pair_for_prop o subst_atomic subst) blanchet@35335: |> AList.group (op =) |> Symtab.make blanchet@33192: blanchet@35220: (* theory -> (typ option * bool) list -> (string * int) list *) blanchet@35220: fun case_const_names thy stds = blanchet@33192: Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => blanchet@35220: if is_basic_datatype thy stds dtype_s then blanchet@33192: I blanchet@33192: else blanchet@33192: cons (case_name, AList.lookup (op =) descr index blanchet@33192: |> the |> #3 |> length)) blanchet@33192: (Datatype.get_all thy) [] @ blanchet@33574: map (apsnd length o snd) (#codatatypes (Data.get thy)) blanchet@33192: blanchet@35335: (* Proof.context -> (term * term) list -> term list -> const_table *) blanchet@35335: fun const_def_table ctxt subst ts = blanchet@35335: table_for (map prop_of o Nitpick_Defs.get) ctxt subst blanchet@33192: |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) blanchet@33192: (map pair_for_prop ts) blanchet@33192: (* term list -> const_table *) blanchet@33192: fun const_nondef_table ts = blanchet@33192: fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] blanchet@33192: |> AList.group (op =) |> Symtab.make blanchet@35335: (* Proof.context -> (term * term) list -> const_table *) blanchet@33192: val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) blanchet@33192: val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) blanchet@35335: (* Proof.context -> (term * term) list -> const_table -> const_table *) blanchet@35335: fun inductive_intro_table ctxt subst def_table = blanchet@33192: table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) blanchet@33192: def_table o prop_of) blanchet@35335: o Nitpick_Intros.get) ctxt subst blanchet@33192: (* theory -> term list Inttab.table *) blanchet@33192: fun ground_theorem_table thy = blanchet@33192: fold ((fn @{const Trueprop} $ t1 => blanchet@33192: is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) blanchet@33192: | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty blanchet@33192: blanchet@33192: val basic_ersatz_table = blanchet@33192: [(@{const_name prod_case}, @{const_name split}), blanchet@33192: (@{const_name card}, @{const_name card'}), blanchet@33192: (@{const_name setsum}, @{const_name setsum'}), blanchet@33192: (@{const_name fold_graph}, @{const_name fold_graph'}), blanchet@33192: (@{const_name wf}, @{const_name wf'}), blanchet@33192: (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), blanchet@33192: (@{const_name wfrec}, @{const_name wfrec'})] blanchet@33192: blanchet@33192: (* theory -> (string * string) list *) blanchet@33192: fun ersatz_table thy = blanchet@33574: fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table blanchet@33192: blanchet@33192: (* const_table Unsynchronized.ref -> string -> term list -> unit *) blanchet@33192: fun add_simps simp_table s eqs = blanchet@33192: Unsynchronized.change simp_table blanchet@33192: (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) blanchet@33192: blanchet@34923: (* theory -> styp -> term list *) blanchet@34923: fun inverse_axioms_for_rep_fun thy (x as (_, T)) = blanchet@34923: let val abs_T = domain_type T in blanchet@34923: typedef_info thy (fst (dest_Type abs_T)) |> the blanchet@34923: |> pairf #Abs_inverse #Rep_inverse blanchet@34923: |> pairself (Refute.specialize_type thy x o prop_of o the) blanchet@34923: ||> single |> op :: blanchet@34923: end blanchet@35067: (* theory -> string * typ list -> term list *) blanchet@35280: fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) = blanchet@34923: let val abs_T = Type abs_z in blanchet@33192: if is_univ_typedef thy abs_T then blanchet@33192: [] blanchet@33192: else case typedef_info thy abs_s of blanchet@35280: SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} => blanchet@33192: let blanchet@35311: val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type blanchet@33192: val rep_t = Const (Rep_name, abs_T --> rep_T) blanchet@33192: val set_t = Const (set_name, rep_T --> bool_T) blanchet@33192: val set_t' = blanchet@33192: prop_of_Rep |> HOLogic.dest_Trueprop blanchet@33192: |> Refute.specialize_type thy (dest_Const rep_t) blanchet@33192: |> HOLogic.dest_mem |> snd blanchet@33192: in blanchet@33192: [HOLogic.all_const abs_T blanchet@33192: $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))] blanchet@33192: |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t')) blanchet@33192: |> map HOLogic.mk_Trueprop blanchet@33192: end blanchet@33192: | NONE => [] blanchet@33192: end blanchet@35311: (* Proof.context -> string * typ list -> term list *) blanchet@35311: fun optimized_quot_type_axioms ctxt stds abs_z = blanchet@34923: let blanchet@35311: val thy = ProofContext.theory_of ctxt blanchet@34923: val abs_T = Type abs_z blanchet@34923: val rep_T = rep_type_for_quot_type thy abs_T blanchet@34923: val equiv_rel = equiv_relation_for_quot_type thy abs_T blanchet@34923: val a_var = Var (("a", 0), abs_T) blanchet@34923: val x_var = Var (("x", 0), rep_T) blanchet@34923: val y_var = Var (("y", 0), rep_T) blanchet@34923: val x = (@{const_name Quot}, rep_T --> abs_T) blanchet@35220: val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T blanchet@35311: val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) blanchet@34923: val normal_x = normal_t $ x_var blanchet@34923: val normal_y = normal_t $ y_var blanchet@34923: val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T) blanchet@34923: in blanchet@34969: [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t), blanchet@34923: Logic.list_implies blanchet@34969: ([@{const Not} $ (is_unknown_t $ normal_x), blanchet@34923: @{const Not} $ (is_unknown_t $ normal_y), blanchet@34923: equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop, blanchet@34923: Logic.mk_equals (normal_x, normal_y)), blanchet@35388: Logic.list_implies blanchet@35388: ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)), blanchet@35388: HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))], blanchet@35388: HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] blanchet@33864: end blanchet@33192: blanchet@35220: (* theory -> (typ option * bool) list -> int * styp -> term *) blanchet@35220: fun constr_case_body thy stds (j, (x as (_, T))) = blanchet@33192: let val arg_Ts = binder_types T in blanchet@35220: list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0)) blanchet@33192: (index_seq 0 (length arg_Ts)) arg_Ts) blanchet@33192: end blanchet@35067: (* hol_context -> typ -> int * styp -> term -> term *) blanchet@35220: fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t = blanchet@34121: Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T) blanchet@35220: $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x) blanchet@33571: $ res_t blanchet@35067: (* hol_context -> typ -> typ -> term *) blanchet@35220: fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T = blanchet@33192: let blanchet@35067: val xs = datatype_constrs hol_ctxt dataT blanchet@35179: val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs blanchet@35179: val (xs', x) = split_last xs blanchet@33192: in blanchet@35220: constr_case_body thy stds (1, x) blanchet@35179: |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs') blanchet@33192: |> fold_rev (curry absdummy) (func_Ts @ [dataT]) blanchet@33192: end blanchet@33192: blanchet@35067: (* hol_context -> string -> typ -> typ -> term -> term *) blanchet@35220: fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t = blanchet@35067: let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in blanchet@33192: case no_of_record_field thy s rec_T of blanchet@33192: ~1 => (case rec_T of blanchet@33192: Type (_, Ts as _ :: _) => blanchet@33192: let blanchet@33192: val rec_T' = List.last Ts blanchet@33192: val j = num_record_fields thy rec_T - 1 blanchet@33192: in blanchet@35220: select_nth_constr_arg thy stds constr_x t j res_T blanchet@35067: |> optimized_record_get hol_ctxt s rec_T' res_T blanchet@33192: end blanchet@33224: | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], blanchet@33224: [])) blanchet@35220: | j => select_nth_constr_arg thy stds constr_x t j res_T blanchet@33192: end blanchet@35067: (* hol_context -> string -> typ -> term -> term -> term *) blanchet@35220: fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t = blanchet@33192: let blanchet@35067: val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T) blanchet@33192: val Ts = binder_types constr_T blanchet@33192: val n = length Ts blanchet@33192: val special_j = no_of_record_field thy s rec_T blanchet@35220: val ts = blanchet@35220: map2 (fn j => fn T => blanchet@35220: let val t = select_nth_constr_arg thy stds constr_x rec_t j T in blanchet@35220: if j = special_j then blanchet@35220: betapply (fun_t, t) blanchet@35220: else if j = n - 1 andalso special_j = ~1 then blanchet@35220: optimized_record_update hol_ctxt s blanchet@35220: (rec_T |> dest_Type |> snd |> List.last) fun_t t blanchet@35220: else blanchet@35220: t blanchet@35220: end) (index_seq 0 n) Ts blanchet@33192: in list_comb (Const constr_x, ts) end blanchet@33192: blanchet@33192: (* theory -> const_table -> string * typ -> fixpoint_kind *) blanchet@33192: fun fixpoint_kind_of_const thy table x = blanchet@35220: if is_built_in_const thy [(NONE, false)] false x then blanchet@33192: NoFp blanchet@33192: else blanchet@33192: fixpoint_kind_of_rhs (the (def_of_const thy table x)) blanchet@33192: handle Option.Option => NoFp blanchet@33192: blanchet@35067: (* hol_context -> styp -> bool *) blanchet@35220: fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table, blanchet@35220: ...} : hol_context) x = blanchet@35220: fixpoint_kind_of_const thy def_table x <> NoFp andalso blanchet@35220: not (null (def_props_for_const thy stds fast_descrs intro_table x)) blanchet@35220: fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table, blanchet@35220: ...} : hol_context) x = blanchet@35220: exists (fn table => not (null (def_props_for_const thy stds fast_descrs table blanchet@35220: x))) blanchet@33192: [!simp_table, psimp_table] blanchet@35067: fun is_inductive_pred hol_ctxt = blanchet@35067: is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt) blanchet@35280: fun is_equational_fun hol_ctxt = blanchet@35665: (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf blanchet@35665: (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) blanchet@33192: blanchet@33192: (* term * term -> term *) blanchet@33192: fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t blanchet@33192: | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t blanchet@33192: | s_betapply p = betapply p blanchet@33192: (* term * term list -> term *) blanchet@33192: val s_betapplys = Library.foldl s_betapply blanchet@33192: blanchet@33192: (* term -> term *) blanchet@33192: fun lhs_of_equation t = blanchet@33192: case t of blanchet@33192: Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 blanchet@33192: | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1 blanchet@33192: | @{const "==>"} $ _ $ t2 => lhs_of_equation t2 blanchet@33192: | @{const Trueprop} $ t1 => lhs_of_equation t1 blanchet@33192: | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1 blanchet@33192: | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1 blanchet@33192: | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2 blanchet@33192: | _ => NONE blanchet@33192: (* theory -> term -> bool *) blanchet@33192: fun is_constr_pattern _ (Bound _) = true blanchet@33864: | is_constr_pattern _ (Var _) = true blanchet@33192: | is_constr_pattern thy t = blanchet@33192: case strip_comb t of blanchet@35280: (Const x, args) => blanchet@33192: is_constr_like thy x andalso forall (is_constr_pattern thy) args blanchet@33192: | _ => false blanchet@33192: fun is_constr_pattern_lhs thy t = blanchet@33192: forall (is_constr_pattern thy) (snd (strip_comb t)) blanchet@33192: fun is_constr_pattern_formula thy t = blanchet@33192: case lhs_of_equation t of blanchet@33192: SOME t' => is_constr_pattern_lhs thy t' blanchet@33192: | NONE => false blanchet@33192: blanchet@35067: (* Prevents divergence in case of cyclic or infinite definition dependencies. *) blanchet@33747: val unfold_max_depth = 255 blanchet@33192: blanchet@35067: (* hol_context -> term -> term *) blanchet@35284: fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names, blanchet@35280: def_table, ground_thm_table, ersatz_table, blanchet@35280: ...}) = blanchet@33192: let blanchet@33192: (* int -> typ list -> term -> term *) blanchet@33192: fun do_term depth Ts t = blanchet@33192: case t of blanchet@33192: (t0 as Const (@{const_name Int.number_class.number_of}, blanchet@35665: Type (@{type_name fun}, [_, ran_T]))) $ t1 => blanchet@33192: ((if is_number_type thy ran_T then blanchet@33192: let blanchet@33192: val j = t1 |> HOLogic.dest_numeral blanchet@33882: |> ran_T = nat_T ? Integer.max 0 blanchet@33192: val s = numeral_prefix ^ signed_string_of_int j blanchet@33192: in blanchet@35220: if is_integer_like_type ran_T then blanchet@35220: if is_standard_datatype thy stds ran_T then blanchet@35220: Const (s, ran_T) blanchet@35220: else blanchet@35220: funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T) blanchet@33192: else blanchet@33192: do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T) blanchet@33192: $ Const (s, int_T)) blanchet@33192: end blanchet@33192: handle TERM _ => raise SAME () blanchet@33192: else blanchet@33192: raise SAME ()) blanchet@33192: handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1)) blanchet@33864: | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 => blanchet@33192: do_const depth Ts t (@{const_name refl'}, range_type T) [t2] blanchet@35280: | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) => blanchet@33192: betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts, blanchet@33192: map (do_term depth Ts) [t1, t2]) blanchet@33192: | Const (x as (@{const_name distinct}, blanchet@35665: Type (@{type_name fun}, [Type (@{type_name list}, [T']), _]))) blanchet@33192: $ (t1 as _ $ _) => blanchet@33192: (t1 |> HOLogic.dest_list |> distinctness_formula T' blanchet@33192: handle TERM _ => do_const depth Ts t x [t1]) blanchet@35280: | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 => blanchet@34923: if is_ground_term t1 andalso blanchet@34923: exists (Pattern.matches thy o rpair t1) blanchet@34923: (Inttab.lookup_list ground_thm_table (hash_term t1)) then blanchet@33192: do_term depth Ts t2 blanchet@33192: else blanchet@33192: do_const depth Ts t x [t1, t2, t3] blanchet@33192: | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3] blanchet@33192: | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2] blanchet@33192: | Const x $ t1 => do_const depth Ts t x [t1] blanchet@33192: | Const x => do_const depth Ts t x [] blanchet@33192: | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2) blanchet@33192: | Free _ => t blanchet@33192: | Var _ => t blanchet@33192: | Bound _ => t blanchet@33192: | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body) blanchet@33192: (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *) blanchet@33192: and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T = blanchet@33192: (Abs (Name.uu, body_type T, blanchet@35220: select_nth_constr_arg thy stds x (Bound 0) n res_T), []) blanchet@33192: | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T = blanchet@35220: (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts) blanchet@33192: (* int -> typ list -> term -> styp -> term list -> term *) blanchet@33192: and do_const depth Ts t (x as (s, T)) ts = blanchet@33192: case AList.lookup (op =) ersatz_table s of blanchet@33192: SOME s' => blanchet@33192: do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts blanchet@33192: | NONE => blanchet@33192: let blanchet@33192: val (const, ts) = blanchet@35220: if is_built_in_const thy stds fast_descrs x then blanchet@33877: (Const x, ts) blanchet@33192: else case AList.lookup (op =) case_names s of blanchet@33192: SOME n => blanchet@33192: let blanchet@33192: val (dataT, res_T) = nth_range_type n T blanchet@33705: |> pairf domain_type range_type blanchet@33192: in blanchet@35067: (optimized_case_def hol_ctxt dataT res_T blanchet@33192: |> do_term (depth + 1) Ts, ts) blanchet@33192: end blanchet@33192: | _ => blanchet@35220: if is_constr thy stds x then blanchet@33192: (Const x, ts) blanchet@33572: else if is_stale_constr thy x then blanchet@34923: raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \ blanchet@33572: \(\"" ^ s ^ "\")") blanchet@35284: else if is_quot_abs_fun ctxt x then blanchet@34923: let blanchet@34923: val rep_T = domain_type T blanchet@34923: val abs_T = range_type T blanchet@34923: in blanchet@34923: (Abs (Name.uu, rep_T, blanchet@34923: Const (@{const_name Quot}, rep_T --> abs_T) blanchet@35311: $ (Const (quot_normal_name_for_type ctxt abs_T, blanchet@34923: rep_T --> rep_T) $ Bound 0)), ts) blanchet@34923: end blanchet@35284: else if is_quot_rep_fun ctxt x then blanchet@34923: let blanchet@34923: val abs_T = domain_type T blanchet@34923: val rep_T = range_type T blanchet@34923: val x' = (@{const_name Quot}, rep_T --> abs_T) blanchet@34923: in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end blanchet@33192: else if is_record_get thy x then blanchet@33192: case length ts of blanchet@33192: 0 => (do_term depth Ts (eta_expand Ts t 1), []) blanchet@35067: | _ => (optimized_record_get hol_ctxt s (domain_type T) blanchet@34969: (range_type T) (do_term depth Ts (hd ts)), tl ts) blanchet@33192: else if is_record_update thy x then blanchet@33192: case length ts of blanchet@35067: 2 => (optimized_record_update hol_ctxt blanchet@33571: (unsuffix Record.updateN s) (nth_range_type 2 T) blanchet@33571: (do_term depth Ts (hd ts)) blanchet@33571: (do_term depth Ts (nth ts 1)), []) blanchet@33192: | n => (do_term depth Ts (eta_expand Ts t (2 - n)), []) blanchet@33192: else if is_rep_fun thy x then blanchet@33192: let val x' = mate_of_rep_fun thy x in blanchet@35220: if is_constr thy stds x' then blanchet@33192: select_nth_constr_arg_with_args depth Ts x' ts 0 blanchet@33192: (range_type T) blanchet@33192: else blanchet@33192: (Const x, ts) blanchet@33192: end blanchet@35067: else if is_equational_fun hol_ctxt x then blanchet@33192: (Const x, ts) blanchet@33192: else case def_of_const thy def_table x of blanchet@33192: SOME def => blanchet@33192: if depth > unfold_max_depth then blanchet@34121: raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term", blanchet@34121: "too many nested definitions (" ^ blanchet@34121: string_of_int depth ^ ") while expanding " ^ blanchet@34121: quote s) blanchet@33192: else if s = @{const_name wfrec'} then blanchet@33192: (do_term (depth + 1) Ts (betapplys (def, ts)), []) blanchet@33192: else blanchet@33192: (do_term (depth + 1) Ts def, ts) blanchet@33192: | NONE => (Const x, ts) blanchet@33192: in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end blanchet@33192: in do_term 0 [] end blanchet@33192: blanchet@35067: (* hol_context -> typ -> term list *) blanchet@35220: fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T = blanchet@33192: let blanchet@35067: val xs = datatype_constrs hol_ctxt T blanchet@33192: val set_T = T --> bool_T blanchet@33192: val iter_T = @{typ bisim_iterator} blanchet@34121: val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T) blanchet@33192: val bisim_max = @{const bisim_iterator_max} blanchet@33192: val n_var = Var (("n", 0), iter_T) blanchet@33192: val n_var_minus_1 = blanchet@33192: Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T) blanchet@33192: $ Abs ("m", iter_T, HOLogic.eq_const iter_T blanchet@33192: $ (suc_const iter_T $ Bound 0) $ n_var) blanchet@33192: val x_var = Var (("x", 0), T) blanchet@33192: val y_var = Var (("y", 0), T) blanchet@33192: (* styp -> int -> typ -> term *) blanchet@33192: fun nth_sub_bisim x n nth_T = blanchet@33192: (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1 blanchet@33192: else HOLogic.eq_const nth_T) blanchet@35220: $ select_nth_constr_arg thy stds x x_var n nth_T blanchet@35220: $ select_nth_constr_arg thy stds x y_var n nth_T blanchet@33192: (* styp -> term *) blanchet@33192: fun case_func (x as (_, T)) = blanchet@33192: let blanchet@33192: val arg_Ts = binder_types T blanchet@33192: val core_t = blanchet@35067: discriminate_value hol_ctxt x y_var :: blanchet@33192: map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts blanchet@33192: |> foldr1 s_conj blanchet@33192: in List.foldr absdummy core_t arg_Ts end blanchet@33192: in blanchet@33192: [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var) blanchet@33192: $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T) blanchet@35067: $ (betapplys (optimized_case_def hol_ctxt T bool_T, blanchet@33192: map case_func xs @ [x_var]))), blanchet@33192: HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var) blanchet@34121: $ (Const (@{const_name insert}, T --> set_T --> set_T) blanchet@35220: $ x_var $ Const (@{const_name bot_class.bot}, set_T))] blanchet@33192: |> map HOLogic.mk_Trueprop blanchet@33192: end blanchet@33192: blanchet@33192: exception NO_TRIPLE of unit blanchet@33192: blanchet@33192: (* theory -> styp -> term -> term list * term list * term *) blanchet@33192: fun triple_for_intro_rule thy x t = blanchet@33192: let wenzelm@35625: val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy) wenzelm@35625: val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy blanchet@34118: val (main, side) = List.partition (exists_Const (curry (op =) x)) prems blanchet@33192: (* term -> bool *) blanchet@34118: val is_good_head = curry (op =) (Const x) o head_of blanchet@33192: in blanchet@33192: if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE () blanchet@33192: end blanchet@33192: blanchet@33192: (* term -> term *) blanchet@33192: val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb blanchet@33192: blanchet@33192: (* indexname * typ -> term list -> term -> term -> term *) blanchet@33192: fun wf_constraint_for rel side concl main = blanchet@33192: let blanchet@33192: val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main, blanchet@33192: tuple_for_args concl), Var rel) blanchet@33192: val t = List.foldl HOLogic.mk_imp core side blanchet@33192: val vars = filter (not_equal rel) (Term.add_vars t []) blanchet@33192: in blanchet@33192: Library.foldl (fn (t', ((x, j), T)) => blanchet@33192: HOLogic.all_const T blanchet@33192: $ Abs (x, T, abstract_over (Var ((x, j), T), t'))) blanchet@33192: (t, vars) blanchet@33192: end blanchet@33192: blanchet@33192: (* indexname * typ -> term list * term list * term -> term *) blanchet@33192: fun wf_constraint_for_triple rel (side, main, concl) = blanchet@33192: map (wf_constraint_for rel side concl) main |> foldr1 s_conj blanchet@33192: blanchet@33192: (* Proof.context -> Time.time option -> thm blanchet@33192: -> (Proof.context -> tactic -> tactic) -> bool *) blanchet@33192: fun terminates_by ctxt timeout goal tac = blanchet@33192: can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the blanchet@33192: #> SINGLE (DETERM_TIMEOUT timeout blanchet@33192: (tac ctxt (auto_tac (clasimpset_of ctxt)))) blanchet@33192: #> the #> Goal.finish ctxt) goal blanchet@33192: blanchet@35181: val max_cached_wfs = 50 blanchet@35181: val cached_timeout = blanchet@35181: Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime) blanchet@35181: val cached_wf_props = blanchet@35181: Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) blanchet@33192: krauss@33351: val termination_tacs = [Lexicographic_Order.lex_order_tac true, blanchet@33192: ScnpReconstruct.sizechange_tac] blanchet@33192: blanchet@35067: (* hol_context -> const_table -> styp -> bool *) blanchet@33571: fun uncached_is_well_founded_inductive_pred blanchet@35220: ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...} blanchet@35067: : hol_context) (x as (_, T)) = blanchet@35220: case def_props_for_const thy stds fast_descrs intro_table x of blanchet@33571: [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive", blanchet@33224: [Const x]) blanchet@33192: | intro_ts => blanchet@33192: (case map (triple_for_intro_rule thy x) intro_ts blanchet@33192: |> filter_out (null o #2) of blanchet@33192: [] => true blanchet@33192: | triples => blanchet@33192: let blanchet@33192: val binders_T = HOLogic.mk_tupleT (binder_types T) blanchet@33192: val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T blanchet@33882: val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1 blanchet@33192: val rel = (("R", j), rel_T) blanchet@33192: val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel :: blanchet@33192: map (wf_constraint_for_triple rel) triples blanchet@33192: |> foldr1 s_conj |> HOLogic.mk_Trueprop blanchet@33192: val _ = if debug then blanchet@33192: priority ("Wellfoundedness goal: " ^ blanchet@33192: Syntax.string_of_term ctxt prop ^ ".") blanchet@33192: else blanchet@33192: () blanchet@33192: in blanchet@35181: if tac_timeout = Synchronized.value cached_timeout andalso blanchet@35181: length (Synchronized.value cached_wf_props) < max_cached_wfs then blanchet@33548: () blanchet@33548: else blanchet@35181: (Synchronized.change cached_wf_props (K []); blanchet@35181: Synchronized.change cached_timeout (K tac_timeout)); blanchet@35181: case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of blanchet@33192: SOME wf => wf blanchet@33192: | NONE => blanchet@33192: let blanchet@33192: val goal = prop |> cterm_of thy |> Goal.init blanchet@33705: val wf = exists (terminates_by ctxt tac_timeout goal) blanchet@33705: termination_tacs blanchet@35181: in Synchronized.change cached_wf_props (cons (prop, wf)); wf end blanchet@33192: end) blanchet@35309: handle List.Empty => false | NO_TRIPLE () => false blanchet@33192: blanchet@35067: (* The type constraint below is a workaround for a Poly/ML crash. *) blanchet@33192: blanchet@35067: (* hol_context -> styp -> bool *) blanchet@33192: fun is_well_founded_inductive_pred blanchet@35067: (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context) blanchet@33192: (x as (s, _)) = blanchet@33192: case triple_lookup (const_match thy) wfs x of blanchet@33192: SOME (SOME b) => b blanchet@34923: | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse blanchet@34923: case AList.lookup (op =) (!wf_cache) x of blanchet@35181: SOME (_, wf) => wf blanchet@35181: | NONE => blanchet@35181: let blanchet@35181: val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) blanchet@35181: val wf = uncached_is_well_founded_inductive_pred hol_ctxt x blanchet@35181: in blanchet@35181: Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf blanchet@35181: end blanchet@33192: blanchet@35280: (* typ list -> typ -> term -> term *) blanchet@35280: fun ap_curry [_] _ t = t blanchet@35280: | ap_curry arg_Ts tuple_T t = blanchet@33192: let val n = length arg_Ts in blanchet@33192: list_abs (map (pair "c") arg_Ts, blanchet@33192: incr_boundvars n t blanchet@33192: $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0))) blanchet@33192: end blanchet@33192: blanchet@33192: (* int -> term -> int *) blanchet@33192: fun num_occs_of_bound_in_term j (t1 $ t2) = blanchet@33192: op + (pairself (num_occs_of_bound_in_term j) (t1, t2)) blanchet@35280: | num_occs_of_bound_in_term j (Abs (_, _, t')) = blanchet@33192: num_occs_of_bound_in_term (j + 1) t' blanchet@33192: | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0 blanchet@33192: | num_occs_of_bound_in_term _ _ = 0 blanchet@33192: blanchet@33192: (* term -> bool *) blanchet@33192: val is_linear_inductive_pred_def = blanchet@33192: let blanchet@33192: (* int -> term -> bool *) blanchet@33192: fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) = blanchet@33192: do_disjunct (j + 1) t2 blanchet@33192: | do_disjunct j t = blanchet@33192: case num_occs_of_bound_in_term j t of blanchet@33192: 0 => true blanchet@35067: | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t) blanchet@33192: | _ => false blanchet@33192: (* term -> bool *) blanchet@33192: fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) = blanchet@33192: let val (xs, body) = strip_abs t2 in blanchet@33192: case length xs of blanchet@33192: 1 => false blanchet@35067: | n => forall (do_disjunct (n - 1)) (disjuncts_of body) blanchet@33192: end blanchet@33192: | do_lfp_def _ = false blanchet@33192: in do_lfp_def o strip_abs_body end blanchet@33192: blanchet@33851: (* int -> int list list *) blanchet@33851: fun n_ptuple_paths 0 = [] blanchet@33851: | n_ptuple_paths 1 = [] blanchet@33851: | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1)) blanchet@33851: (* int -> typ -> typ -> term -> term *) blanchet@33851: val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths blanchet@33192: blanchet@33192: (* term -> term * term *) blanchet@33192: val linear_pred_base_and_step_rhss = blanchet@33192: let blanchet@33192: (* term -> term *) blanchet@33192: fun aux (Const (@{const_name lfp}, _) $ t2) = blanchet@33192: let blanchet@33192: val (xs, body) = strip_abs t2 blanchet@33192: val arg_Ts = map snd (tl xs) blanchet@33192: val tuple_T = HOLogic.mk_tupleT arg_Ts blanchet@33192: val j = length arg_Ts blanchet@33192: (* int -> term -> term *) blanchet@33192: fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) = blanchet@33192: Const (@{const_name Ex}, T1) blanchet@33192: $ Abs (s2, T2, repair_rec (j + 1) t2') blanchet@33192: | repair_rec j (@{const "op &"} $ t1 $ t2) = blanchet@33192: @{const "op &"} $ repair_rec j t1 $ repair_rec j t2 blanchet@33192: | repair_rec j t = blanchet@33192: let val (head, args) = strip_comb t in blanchet@33192: if head = Bound j then blanchet@33192: HOLogic.eq_const tuple_T $ Bound j blanchet@33192: $ mk_flat_tuple tuple_T args blanchet@33192: else blanchet@33192: t blanchet@33192: end blanchet@33192: val (nonrecs, recs) = blanchet@34118: List.partition (curry (op =) 0 o num_occs_of_bound_in_term j) blanchet@35067: (disjuncts_of body) blanchet@33192: val base_body = nonrecs |> List.foldl s_disj @{const False} blanchet@33192: val step_body = recs |> map (repair_rec j) blanchet@33192: |> List.foldl s_disj @{const False} blanchet@33192: in blanchet@33192: (list_abs (tl xs, incr_bv (~1, j, base_body)) blanchet@33851: |> ap_n_split (length arg_Ts) tuple_T bool_T, blanchet@33192: Abs ("y", tuple_T, list_abs (tl xs, step_body) blanchet@33851: |> ap_n_split (length arg_Ts) tuple_T bool_T)) blanchet@33192: end blanchet@33192: | aux t = blanchet@33224: raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t]) blanchet@33192: in aux end blanchet@33192: blanchet@35067: (* hol_context -> styp -> term -> term *) blanchet@35280: fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def = blanchet@33192: let blanchet@33192: val j = maxidx_of_term def + 1 blanchet@33192: val (outer, fp_app) = strip_abs def blanchet@33192: val outer_bounds = map Bound (length outer - 1 downto 0) blanchet@33192: val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer blanchet@33192: val fp_app = subst_bounds (rev outer_vars, fp_app) blanchet@33192: val (outer_Ts, rest_T) = strip_n_binders (length outer) T blanchet@33192: val tuple_arg_Ts = strip_type rest_T |> fst blanchet@33192: val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts blanchet@33192: val set_T = tuple_T --> bool_T blanchet@33192: val curried_T = tuple_T --> set_T blanchet@35665: val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T blanchet@33192: val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app blanchet@33192: val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T) blanchet@33192: val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs) blanchet@33192: |> HOLogic.mk_Trueprop blanchet@33192: val _ = add_simps simp_table base_s [base_eq] blanchet@33192: val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T) blanchet@33192: val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs) blanchet@33192: |> HOLogic.mk_Trueprop blanchet@33192: val _ = add_simps simp_table step_s [step_eq] blanchet@33192: in blanchet@33192: list_abs (outer, blanchet@33192: Const (@{const_name Image}, uncurried_T --> set_T --> set_T) blanchet@33192: $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T) blanchet@33192: $ (Const (@{const_name split}, curried_T --> uncurried_T) blanchet@33192: $ list_comb (Const step_x, outer_bounds))) blanchet@33192: $ list_comb (Const base_x, outer_bounds) blanchet@35280: |> ap_curry tuple_arg_Ts tuple_T) blanchet@35067: |> unfold_defs_in_term hol_ctxt blanchet@33192: end blanchet@33192: blanchet@35067: (* hol_context -> bool -> styp -> term *) blanchet@35067: fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds, blanchet@33192: def_table, simp_table, ...}) blanchet@33192: gfp (x as (s, T)) = blanchet@33192: let blanchet@33192: val iter_T = iterator_type_for_const gfp x blanchet@33192: val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T) blanchet@33192: val unrolled_const = Const x' $ zero_const iter_T blanchet@33192: val def = the (def_of_const thy def_table x) blanchet@33192: in blanchet@35067: if is_equational_fun hol_ctxt x' then blanchet@33192: unrolled_const (* already done *) blanchet@34923: else if not gfp andalso is_linear_inductive_pred_def def andalso blanchet@34923: star_linear_preds then blanchet@35067: starred_linear_pred_const hol_ctxt x def blanchet@33192: else blanchet@33192: let blanchet@33192: val j = maxidx_of_term def + 1 blanchet@33192: val (outer, fp_app) = strip_abs def blanchet@33192: val outer_bounds = map Bound (length outer - 1 downto 0) blanchet@33192: val cur = Var ((iter_var_prefix, j + 1), iter_T) blanchet@33192: val next = suc_const iter_T $ cur blanchet@33192: val rhs = case fp_app of blanchet@33192: Const _ $ t => blanchet@33192: betapply (t, list_comb (Const x', next :: outer_bounds)) blanchet@33224: | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\ blanchet@33224: \const", [fp_app]) blanchet@33192: val (inner, naked_rhs) = strip_abs rhs blanchet@33192: val all = outer @ inner blanchet@33192: val bounds = map Bound (length all - 1 downto 0) blanchet@33192: val vars = map (fn (s, T) => Var ((s, j), T)) all blanchet@33192: val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs) blanchet@33192: |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars) blanchet@33192: val _ = add_simps simp_table s' [eq] blanchet@33192: in unrolled_const end blanchet@33192: end blanchet@33192: blanchet@35067: (* hol_context -> styp -> term *) blanchet@35067: fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x = blanchet@33192: let blanchet@33192: val def = the (def_of_const thy def_table x) blanchet@33192: val (outer, fp_app) = strip_abs def blanchet@33192: val outer_bounds = map Bound (length outer - 1 downto 0) blanchet@33192: val rhs = case fp_app of blanchet@33192: Const _ $ t => betapply (t, list_comb (Const x, outer_bounds)) blanchet@33224: | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", blanchet@33192: [fp_app]) blanchet@33192: val (inner, naked_rhs) = strip_abs rhs blanchet@33192: val all = outer @ inner blanchet@33192: val bounds = map Bound (length all - 1 downto 0) blanchet@33192: val j = maxidx_of_term def + 1 blanchet@33192: val vars = map (fn (s, T) => Var ((s, j), T)) all blanchet@33192: in blanchet@33192: HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs) blanchet@33192: |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars) blanchet@33192: end blanchet@35067: fun inductive_pred_axiom hol_ctxt (x as (s, T)) = blanchet@33192: if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then blanchet@33192: let val x' = (after_name_sep s, T) in blanchet@35067: raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)] blanchet@33192: end blanchet@33192: else blanchet@35067: raw_inductive_pred_axiom hol_ctxt x blanchet@33192: blanchet@35067: (* hol_context -> styp -> term list *) blanchet@35220: fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table, blanchet@35280: psimp_table, ...}) x = blanchet@35220: case def_props_for_const thy stds fast_descrs (!simp_table) x of blanchet@35220: [] => (case def_props_for_const thy stds fast_descrs psimp_table x of blanchet@35067: [] => [inductive_pred_axiom hol_ctxt x] blanchet@33192: | psimps => psimps) blanchet@33192: | simps => simps blanchet@33192: val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms blanchet@35067: (* hol_context -> styp -> bool *) blanchet@35067: fun is_equational_fun_surely_complete hol_ctxt x = blanchet@35067: case raw_equational_fun_axioms hol_ctxt x of blanchet@35067: [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] => blanchet@35067: strip_comb t1 |> snd |> forall is_Var blanchet@35067: | _ => false blanchet@33192: blanchet@33192: (* term list -> term list *) blanchet@33547: fun merge_type_vars_in_terms ts = blanchet@33192: let blanchet@33192: (* typ -> (sort * string) list -> (sort * string) list *) blanchet@33192: fun add_type (TFree (s, S)) table = blanchet@33192: (case AList.lookup (op =) table S of blanchet@33192: SOME s' => blanchet@33192: if string_ord (s', s) = LESS then AList.update (op =) (S, s') table blanchet@33192: else table blanchet@33192: | NONE => (S, s) :: table) blanchet@33192: | add_type _ table = table blanchet@33192: val table = fold (fold_types (fold_atyps add_type)) ts [] blanchet@33192: (* typ -> typ *) blanchet@35280: fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S) blanchet@33192: | coalesce T = T blanchet@33192: in map (map_types (map_atyps coalesce)) ts end blanchet@33192: blanchet@35190: (* hol_context -> bool -> typ -> typ list -> typ list *) blanchet@35190: fun add_ground_types hol_ctxt binarize = blanchet@35190: let blanchet@35190: fun aux T accum = blanchet@35190: case T of blanchet@35665: Type (@{type_name fun}, Ts) => fold aux Ts accum blanchet@35665: | Type (@{type_name "*"}, Ts) => fold aux Ts accum blanchet@35190: | Type (@{type_name itself}, [T1]) => aux T1 accum blanchet@35190: | Type (_, Ts) => blanchet@35190: if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) blanchet@35190: T then blanchet@35190: accum blanchet@35190: else blanchet@35190: T :: accum blanchet@35190: |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt blanchet@35190: binarize T of blanchet@35190: [] => Ts blanchet@35190: | xs => map snd xs) blanchet@35190: | _ => insert (op =) T accum blanchet@35190: in aux end blanchet@34985: blanchet@35190: (* hol_context -> bool -> typ -> typ list *) blanchet@35190: fun ground_types_in_type hol_ctxt binarize T = blanchet@35190: add_ground_types hol_ctxt binarize T [] blanchet@35067: (* hol_context -> term list -> typ list *) blanchet@35190: fun ground_types_in_terms hol_ctxt binarize ts = blanchet@35190: fold (fold_types (add_ground_types hol_ctxt binarize)) ts [] blanchet@33192: blanchet@33192: (* theory -> const_table -> styp -> int list *) blanchet@33192: fun const_format thy def_table (x as (s, T)) = blanchet@33192: if String.isPrefix unrolled_prefix s then blanchet@33192: const_format thy def_table (original_name s, range_type T) blanchet@33192: else if String.isPrefix skolem_prefix s then blanchet@33192: let blanchet@33192: val k = unprefix skolem_prefix s blanchet@33192: |> strip_first_name_sep |> fst |> space_explode "@" blanchet@33192: |> hd |> Int.fromString |> the blanchet@33192: in [k, num_binder_types T - k] end blanchet@33192: else if original_name s <> s then blanchet@33192: [num_binder_types T] blanchet@33192: else case def_of_const thy def_table x of blanchet@33192: SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then blanchet@33192: let val k = length (strip_abs_vars t') in blanchet@33192: [k, num_binder_types T - k] blanchet@33192: end blanchet@33192: else blanchet@33192: [num_binder_types T] blanchet@33192: | NONE => [num_binder_types T] blanchet@33192: (* int list -> int list -> int list *) blanchet@33192: fun intersect_formats _ [] = [] blanchet@33192: | intersect_formats [] _ = [] blanchet@33192: | intersect_formats ks1 ks2 = blanchet@33192: let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in blanchet@33192: intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else [])) blanchet@33192: (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @ blanchet@33192: [Int.min (k1, k2)] blanchet@33192: end blanchet@33192: blanchet@33192: (* theory -> const_table -> (term option * int list) list -> term -> int list *) blanchet@33192: fun lookup_format thy def_table formats t = blanchet@33192: case AList.lookup (fn (SOME x, SOME y) => blanchet@33192: (term_match thy) (x, y) | _ => false) blanchet@33192: formats (SOME t) of blanchet@33192: SOME format => format blanchet@33192: | NONE => let val format = the (AList.lookup (op =) formats NONE) in blanchet@33192: case t of blanchet@33192: Const x => intersect_formats format blanchet@33192: (const_format thy def_table x) blanchet@33192: | _ => format blanchet@33192: end blanchet@33192: blanchet@33192: (* int list -> int list -> typ -> typ *) blanchet@33192: fun format_type default_format format T = blanchet@33192: let blanchet@35665: val T = uniterize_unarize_unbox_etc_type T blanchet@33192: val format = format |> filter (curry (op <) 0) blanchet@33192: in blanchet@34118: if forall (curry (op =) 1) format then blanchet@33192: T blanchet@33192: else blanchet@33192: let blanchet@33192: val (binder_Ts, body_T) = strip_type T blanchet@33192: val batched = blanchet@33192: binder_Ts blanchet@33192: |> map (format_type default_format default_format) blanchet@33192: |> rev |> chunk_list_unevenly (rev format) blanchet@33192: |> map (HOLogic.mk_tupleT o rev) blanchet@33192: in List.foldl (op -->) body_T batched end blanchet@33192: end blanchet@33192: (* theory -> const_table -> (term option * int list) list -> term -> typ *) blanchet@33192: fun format_term_type thy def_table formats t = blanchet@33192: format_type (the (AList.lookup (op =) formats NONE)) blanchet@33192: (lookup_format thy def_table formats t) (fastype_of t) blanchet@33192: blanchet@33192: (* int list -> int -> int list -> int list *) blanchet@33192: fun repair_special_format js m format = blanchet@33192: m - 1 downto 0 |> chunk_list_unevenly (rev format) blanchet@33192: |> map (rev o filter_out (member (op =) js)) blanchet@33192: |> filter_out null |> map length |> rev blanchet@33192: blanchet@35067: (* hol_context -> string * string -> (term option * int list) list blanchet@33192: -> styp -> term * typ *) blanchet@33192: fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...} blanchet@35067: : hol_context) (base_name, step_name) formats = blanchet@33192: let blanchet@33192: val default_format = the (AList.lookup (op =) formats NONE) blanchet@33192: (* styp -> term * typ *) blanchet@33192: fun do_const (x as (s, T)) = blanchet@33192: (if String.isPrefix special_prefix s then blanchet@33192: let blanchet@33192: (* term -> term *) blanchet@33192: val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t') blanchet@33192: val (x' as (_, T'), js, ts) = blanchet@35665: AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T) blanchet@34121: |> the_single blanchet@33192: val max_j = List.last js blanchet@33192: val Ts = List.take (binder_types T', max_j + 1) blanchet@33192: val missing_js = filter_out (member (op =) js) (0 upto max_j) blanchet@33192: val missing_Ts = filter_indices missing_js Ts blanchet@33192: (* int -> indexname *) blanchet@33192: fun nth_missing_var n = blanchet@33192: ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n) blanchet@33192: val missing_vars = map nth_missing_var (0 upto length missing_js - 1) blanchet@33192: val vars = special_bounds ts @ missing_vars blanchet@35280: val ts' = blanchet@35280: map (fn j => blanchet@35280: case AList.lookup (op =) (js ~~ ts) j of blanchet@35280: SOME t => do_term t blanchet@35280: | NONE => blanchet@35280: Var (nth missing_vars blanchet@35280: (find_index (curry (op =) j) missing_js))) blanchet@35280: (0 upto max_j) blanchet@33192: val t = do_const x' |> fst blanchet@33192: val format = blanchet@33192: case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2) blanchet@33192: | _ => false) formats (SOME t) of blanchet@33192: SOME format => blanchet@33192: repair_special_format js (num_binder_types T') format blanchet@33192: | NONE => blanchet@33192: const_format thy def_table x' blanchet@33192: |> repair_special_format js (num_binder_types T') blanchet@33192: |> intersect_formats default_format blanchet@33192: in blanchet@33192: (list_comb (t, ts') |> fold_rev abs_var vars, blanchet@33192: format_type default_format format T) blanchet@33192: end blanchet@33192: else if String.isPrefix uncurry_prefix s then blanchet@33192: let blanchet@33192: val (ss, s') = unprefix uncurry_prefix s blanchet@33192: |> strip_first_name_sep |>> space_explode "@" blanchet@33192: in blanchet@33192: if String.isPrefix step_prefix s' then blanchet@33192: do_const (s', T) blanchet@33192: else blanchet@33192: let blanchet@33192: val k = the (Int.fromString (hd ss)) blanchet@33192: val j = the (Int.fromString (List.last ss)) blanchet@33192: val (before_Ts, (tuple_T, rest_T)) = blanchet@33192: strip_n_binders j T ||> (strip_n_binders 1 #>> hd) blanchet@33192: val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T blanchet@33192: in do_const (s', T') end blanchet@33192: end blanchet@33192: else if String.isPrefix unrolled_prefix s then blanchet@33192: let val t = Const (original_name s, range_type T) in blanchet@33192: (lambda (Free (iter_var_prefix, nat_T)) t, blanchet@33192: format_type default_format blanchet@33192: (lookup_format thy def_table formats t) T) blanchet@33192: end blanchet@33192: else if String.isPrefix base_prefix s then blanchet@33192: (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T), blanchet@33192: format_type default_format default_format T) blanchet@33192: else if String.isPrefix step_prefix s then blanchet@33192: (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T), blanchet@33192: format_type default_format default_format T) blanchet@35311: else if String.isPrefix quot_normal_prefix s then blanchet@35311: let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in blanchet@35311: (t, format_term_type thy def_table formats t) blanchet@35311: end blanchet@33192: else if String.isPrefix skolem_prefix s then blanchet@33192: let blanchet@33192: val ss = the (AList.lookup (op =) (!skolems) s) blanchet@33192: val (Ts, Ts') = chop (length ss) (binder_types T) blanchet@33192: val frees = map Free (ss ~~ Ts) blanchet@33192: val s' = original_name s blanchet@33192: in blanchet@33192: (fold lambda frees (Const (s', Ts' ---> T)), blanchet@33192: format_type default_format blanchet@33192: (lookup_format thy def_table formats (Const x)) T) blanchet@33192: end blanchet@33192: else if String.isPrefix eval_prefix s then blanchet@33192: let blanchet@33192: val t = nth evals (the (Int.fromString (unprefix eval_prefix s))) blanchet@33192: in (t, format_term_type thy def_table formats t) end blanchet@33192: else if s = @{const_name undefined_fast_The} then blanchet@33192: (Const (nitpick_prefix ^ "The fallback", T), blanchet@33192: format_type default_format blanchet@33192: (lookup_format thy def_table formats blanchet@33192: (Const (@{const_name The}, (T --> bool_T) --> T))) T) blanchet@33192: else if s = @{const_name undefined_fast_Eps} then blanchet@33192: (Const (nitpick_prefix ^ "Eps fallback", T), blanchet@33192: format_type default_format blanchet@33192: (lookup_format thy def_table formats blanchet@33192: (Const (@{const_name Eps}, (T --> bool_T) --> T))) T) blanchet@33192: else blanchet@33192: let val t = Const (original_name s, T) in blanchet@33192: (t, format_term_type thy def_table formats t) blanchet@33192: end) blanchet@35665: |>> map_types uniterize_unarize_unbox_etc_type blanchet@35067: |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name blanchet@33192: in do_const end blanchet@33192: blanchet@33192: (* styp -> string *) blanchet@33192: fun assign_operator_for_const (s, T) = blanchet@33192: if String.isPrefix ubfp_prefix s then blanchet@33192: if is_fun_type T then "\" else "\" blanchet@33192: else if String.isPrefix lbfp_prefix s then blanchet@33192: if is_fun_type T then "\" else "\" blanchet@33192: else if original_name s <> s then blanchet@33192: assign_operator_for_const (after_name_sep s, T) blanchet@33192: else blanchet@33192: "=" blanchet@33192: blanchet@33192: end;