wneuper/isa: src/HOL/Tools/Nitpick/nitpick_hol.ML@997aa3a3e4bb (annotated)

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

author	blanchet
	Tue, 23 Feb 2010 10:02:14 +0100
changeset 35309	997aa3a3e4bb
parent 35284	9edc2bd6d2bd
child 35311	8f9a66fc9f80
permissions	-rw-r--r--