33192

1 
(* Title: HOL/Nitpick/Tools/nitpick_hol.ML


2 
Author: Jasmin Blanchette, TU Muenchen


3 
Copyright 2008, 2009


4 


5 
Auxiliary HOLrelated functions used by Nitpick.


6 
*)


7 


8 
signature NITPICK_HOL =


9 
sig


10 
type const_table = term list Symtab.table


11 
type special_fun = (styp * int list * term list) * styp


12 
type unrolled = styp * styp


13 
type wf_cache = (styp * (bool * bool)) list


14 


15 
type extended_context = {


16 
thy: theory,


17 
ctxt: Proof.context,


18 
max_bisim_depth: int,


19 
boxes: (typ option * bool option) list,


20 
wfs: (styp option * bool option) list,


21 
user_axioms: bool option,


22 
debug: bool,


23 
destroy_constrs: bool,


24 
specialize: bool,


25 
skolemize: bool,


26 
star_linear_preds: bool,


27 
uncurry: bool,


28 
fast_descrs: bool,


29 
tac_timeout: Time.time option,


30 
evals: term list,


31 
case_names: (string * int) list,


32 
def_table: const_table,


33 
nondef_table: const_table,


34 
user_nondefs: term list,


35 
simp_table: const_table Unsynchronized.ref,


36 
psimp_table: const_table,


37 
intro_table: const_table,


38 
ground_thm_table: term list Inttab.table,


39 
ersatz_table: (string * string) list,


40 
skolems: (string * string list) list Unsynchronized.ref,


41 
special_funs: special_fun list Unsynchronized.ref,


42 
unrolled_preds: unrolled list Unsynchronized.ref,


43 
wf_cache: wf_cache Unsynchronized.ref}


44 


45 
val name_sep : string


46 
val numeral_prefix : string


47 
val skolem_prefix : string


48 
val eval_prefix : string


49 
val original_name : string > string


50 
val unbox_type : typ > typ


51 
val string_for_type : Proof.context > typ > string


52 
val prefix_name : string > string > string


53 
val short_name : string > string


54 
val short_const_name : string > string


55 
val shorten_const_names_in_term : term > term


56 
val type_match : theory > typ * typ > bool


57 
val const_match : theory > styp * styp > bool


58 
val term_match : theory > term * term > bool


59 
val is_TFree : typ > bool


60 
val is_higher_order_type : typ > bool


61 
val is_fun_type : typ > bool


62 
val is_set_type : typ > bool


63 
val is_pair_type : typ > bool


64 
val is_lfp_iterator_type : typ > bool


65 
val is_gfp_iterator_type : typ > bool


66 
val is_fp_iterator_type : typ > bool


67 
val is_boolean_type : typ > bool


68 
val is_integer_type : typ > bool


69 
val is_record_type : typ > bool


70 
val is_number_type : theory > typ > bool


71 
val const_for_iterator_type : typ > styp


72 
val nth_range_type : int > typ > typ


73 
val num_factors_in_type : typ > int


74 
val num_binder_types : typ > int


75 
val curried_binder_types : typ > typ list


76 
val mk_flat_tuple : typ > term list > term


77 
val dest_n_tuple : int > term > term list


78 
val instantiate_type : theory > typ > typ > typ > typ


79 
val is_codatatype : theory > typ > bool


80 
val is_pure_typedef : theory > typ > bool


81 
val is_univ_typedef : theory > typ > bool


82 
val is_datatype : theory > typ > bool


83 
val is_record_constr : styp > bool


84 
val is_record_get : theory > styp > bool


85 
val is_record_update : theory > styp > bool


86 
val is_abs_fun : theory > styp > bool


87 
val is_rep_fun : theory > styp > bool


88 
val is_constr : theory > styp > bool


89 
val is_sel : string > bool


90 
val discr_for_constr : styp > styp


91 
val num_sels_for_constr_type : typ > int


92 
val nth_sel_name_for_constr_name : string > int > string


93 
val nth_sel_for_constr : styp > int > styp


94 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp


95 
val sel_no_from_name : string > int


96 
val eta_expand : typ list > term > int > term


97 
val extensionalize : term > term


98 
val distinctness_formula : typ > term list > term


99 
val register_frac_type : string > (string * string) list > theory > theory


100 
val unregister_frac_type : string > theory > theory


101 
val register_codatatype : typ > string > styp list > theory > theory


102 
val unregister_codatatype : typ > theory > theory


103 
val datatype_constrs : theory > typ > styp list


104 
val boxed_datatype_constrs : extended_context > typ > styp list


105 
val num_datatype_constrs : theory > typ > int


106 
val constr_name_for_sel_like : string > string


107 
val boxed_constr_for_sel : extended_context > styp > styp


108 
val card_of_type : (typ * int) list > typ > int


109 
val bounded_card_of_type : int > int > (typ * int) list > typ > int


110 
val bounded_precise_card_of_type :


111 
theory > int > int > (typ * int) list > typ > int


112 
val is_finite_type : theory > typ > bool


113 
val all_axioms_of : theory > term list * term list * term list


114 
val arity_of_built_in_const : bool > styp > int option


115 
val is_built_in_const : bool > styp > bool


116 
val case_const_names : theory > (string * int) list


117 
val const_def_table : Proof.context > term list > const_table


118 
val const_nondef_table : term list > const_table


119 
val const_simp_table : Proof.context > const_table


120 
val const_psimp_table : Proof.context > const_table


121 
val inductive_intro_table : Proof.context > const_table > const_table


122 
val ground_theorem_table : theory > term list Inttab.table


123 
val ersatz_table : theory > (string * string) list


124 
val def_of_const : theory > const_table > styp > term option


125 
val is_inductive_pred : extended_context > styp > bool


126 
val is_constr_pattern_lhs : theory > term > bool


127 
val is_constr_pattern_formula : theory > term > bool


128 
val coalesce_type_vars_in_terms : term list > term list


129 
val ground_types_in_type : extended_context > typ > typ list


130 
val ground_types_in_terms : extended_context > term list > typ list


131 
val format_type : int list > int list > typ > typ


132 
val format_term_type :


133 
theory > const_table > (term option * int list) list > term > typ


134 
val user_friendly_const :


135 
extended_context > string * string > (term option * int list) list


136 
> styp > term * typ


137 
val assign_operator_for_const : styp > string


138 
val preprocess_term :


139 
extended_context > term > ((term list * term list) * (bool * bool)) * term


140 
end;


141 


142 
structure NitpickHOL : NITPICK_HOL =


143 
struct


144 


145 
open NitpickUtil


146 


147 
type const_table = term list Symtab.table


148 
type special_fun = (styp * int list * term list) * styp


149 
type unrolled = styp * styp


150 
type wf_cache = (styp * (bool * bool)) list


151 


152 
type extended_context = {


153 
thy: theory,


154 
ctxt: Proof.context,


155 
max_bisim_depth: int,


156 
boxes: (typ option * bool option) list,


157 
wfs: (styp option * bool option) list,


158 
user_axioms: bool option,


159 
debug: bool,


160 
destroy_constrs: bool,


161 
specialize: bool,


162 
skolemize: bool,


163 
star_linear_preds: bool,


164 
uncurry: bool,


165 
fast_descrs: bool,


166 
tac_timeout: Time.time option,


167 
evals: term list,


168 
case_names: (string * int) list,


169 
def_table: const_table,


170 
nondef_table: const_table,


171 
user_nondefs: term list,


172 
simp_table: const_table Unsynchronized.ref,


173 
psimp_table: const_table,


174 
intro_table: const_table,


175 
ground_thm_table: term list Inttab.table,


176 
ersatz_table: (string * string) list,


177 
skolems: (string * string list) list Unsynchronized.ref,


178 
special_funs: special_fun list Unsynchronized.ref,


179 
unrolled_preds: unrolled list Unsynchronized.ref,


180 
wf_cache: wf_cache Unsynchronized.ref}


181 


182 
structure TheoryData = TheoryDataFun(


183 
type T = {frac_types: (string * (string * string) list) list,


184 
codatatypes: (string * (string * styp list)) list}


185 
val empty = {frac_types = [], codatatypes = []}


186 
val copy = I


187 
val extend = I


188 
fun merge _ ({frac_types = fs1, codatatypes = cs1},


189 
{frac_types = fs2, codatatypes = cs2}) =


190 
{frac_types = AList.merge (op =) (op =) (fs1, fs2),


191 
codatatypes = AList.merge (op =) (op =) (cs1, cs2)})


192 


193 
(* term * term > term *)


194 
fun s_conj (t1, @{const True}) = t1


195 
 s_conj (@{const True}, t2) = t2


196 
 s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}


197 
else HOLogic.mk_conj (t1, t2)


198 
fun s_disj (t1, @{const False}) = t1


199 
 s_disj (@{const False}, t2) = t2


200 
 s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}


201 
else HOLogic.mk_disj (t1, t2)


202 
(* term > term > term *)


203 
fun mk_exists v t =


204 
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)


205 


206 
(* term > term > term list *)


207 
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =


208 
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]


209 
 strip_connective _ t = [t]


210 
(* term > term list * term *)


211 
fun strip_any_connective (t as (t0 $ t1 $ t2)) =


212 
if t0 mem [@{const "op &"}, @{const "op "}] then


213 
(strip_connective t0 t, t0)


214 
else


215 
([t], @{const Not})


216 
 strip_any_connective t = ([t], @{const Not})


217 
(* term > term list *)


218 
val conjuncts = strip_connective @{const "op &"}


219 
val disjuncts = strip_connective @{const "op "}


220 


221 
val name_sep = "$"


222 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep


223 
val sel_prefix = nitpick_prefix ^ "sel"


224 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep


225 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep


226 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep


227 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep


228 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep


229 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep


230 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep


231 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep


232 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep


233 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep


234 
val skolem_prefix = nitpick_prefix ^ "sk"


235 
val special_prefix = nitpick_prefix ^ "sp"


236 
val uncurry_prefix = nitpick_prefix ^ "unc"


237 
val eval_prefix = nitpick_prefix ^ "eval"


238 
val bound_var_prefix = "b"


239 
val cong_var_prefix = "c"


240 
val iter_var_prefix = "i"


241 
val val_var_prefix = nitpick_prefix ^ "v"


242 
val arg_var_prefix = "x"


243 


244 
(* int > string *)


245 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep


246 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep


247 
(* int > int > string *)


248 
fun skolem_prefix_for k j =


249 
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep


250 
fun uncurry_prefix_for k j =


251 
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep


252 


253 
(* string > string * string *)


254 
val strip_first_name_sep =


255 
Substring.full #> Substring.position name_sep ##> Substring.triml 1


256 
#> pairself Substring.string


257 
(* string > string *)


258 
fun original_name s =


259 
if String.isPrefix nitpick_prefix s then


260 
case strip_first_name_sep s of (s1, "") => s1  (_, s2) => original_name s2


261 
else


262 
s


263 
val after_name_sep = snd o strip_first_name_sep


264 


265 
(* When you add constants to these lists, make sure to handle them in


266 
"NitpickNut.nut_from_term", and perhaps in "NitpickMono.consider_term" as


267 
well. *)


268 
val built_in_consts =


269 
[(@{const_name all}, 1),


270 
(@{const_name "=="}, 2),


271 
(@{const_name "==>"}, 2),


272 
(@{const_name Pure.conjunction}, 2),


273 
(@{const_name Trueprop}, 1),


274 
(@{const_name Not}, 1),


275 
(@{const_name False}, 0),


276 
(@{const_name True}, 0),


277 
(@{const_name All}, 1),


278 
(@{const_name Ex}, 1),


279 
(@{const_name "op ="}, 2),


280 
(@{const_name "op &"}, 2),


281 
(@{const_name "op "}, 2),


282 
(@{const_name "op >"}, 2),


283 
(@{const_name If}, 3),


284 
(@{const_name Let}, 2),


285 
(@{const_name Unity}, 0),


286 
(@{const_name Pair}, 2),


287 
(@{const_name fst}, 1),


288 
(@{const_name snd}, 1),


289 
(@{const_name Id}, 0),


290 
(@{const_name insert}, 2),


291 
(@{const_name converse}, 1),


292 
(@{const_name trancl}, 1),


293 
(@{const_name rel_comp}, 2),


294 
(@{const_name image}, 2),


295 
(@{const_name Suc}, 0),


296 
(@{const_name finite}, 1),


297 
(@{const_name nat}, 0),


298 
(@{const_name zero_nat_inst.zero_nat}, 0),


299 
(@{const_name one_nat_inst.one_nat}, 0),


300 
(@{const_name plus_nat_inst.plus_nat}, 0),


301 
(@{const_name minus_nat_inst.minus_nat}, 0),


302 
(@{const_name times_nat_inst.times_nat}, 0),


303 
(@{const_name div_nat_inst.div_nat}, 0),


304 
(@{const_name div_nat_inst.mod_nat}, 0),


305 
(@{const_name ord_nat_inst.less_nat}, 2),


306 
(@{const_name ord_nat_inst.less_eq_nat}, 2),


307 
(@{const_name nat_gcd}, 0),


308 
(@{const_name nat_lcm}, 0),


309 
(@{const_name zero_int_inst.zero_int}, 0),


310 
(@{const_name one_int_inst.one_int}, 0),


311 
(@{const_name plus_int_inst.plus_int}, 0),


312 
(@{const_name minus_int_inst.minus_int}, 0),


313 
(@{const_name times_int_inst.times_int}, 0),


314 
(@{const_name div_int_inst.div_int}, 0),


315 
(@{const_name div_int_inst.mod_int}, 0),


316 
(@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)


317 
(@{const_name ord_int_inst.less_int}, 2),


318 
(@{const_name ord_int_inst.less_eq_int}, 2),


319 
(@{const_name Tha}, 1),


320 
(@{const_name Frac}, 0),


321 
(@{const_name norm_frac}, 0)]


322 
val built_in_descr_consts =


323 
[(@{const_name The}, 1),


324 
(@{const_name Eps}, 1)]


325 
val built_in_typed_consts =


326 
[((@{const_name of_nat}, nat_T > int_T), 0)]


327 
val built_in_set_consts =


328 
[(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),


329 
(@{const_name upper_semilattice_fun_inst.sup_fun}, 2),


330 
(@{const_name minus_fun_inst.minus_fun}, 2),


331 
(@{const_name ord_fun_inst.less_eq_fun}, 2)]


332 


333 
(* typ > typ *)


334 
fun unbox_type (Type (@{type_name fun_box}, Ts)) =


335 
Type ("fun", map unbox_type Ts)


336 
 unbox_type (Type (@{type_name pair_box}, Ts)) =


337 
Type ("*", map unbox_type Ts)


338 
 unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)


339 
 unbox_type T = T


340 
(* Proof.context > typ > string *)


341 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type


342 


343 
(* string > string > string *)


344 
val prefix_name = Long_Name.qualify o Long_Name.base_name


345 
(* string > string *)


346 
fun short_name s = List.last (space_explode "." s) handle List.Empty => ""


347 
(* string > term > term *)


348 
val prefix_abs_vars = Term.map_abs_vars o prefix_name


349 
(* term > term *)


350 
val shorten_abs_vars = Term.map_abs_vars short_name


351 
(* string > string *)


352 
fun short_const_name s =


353 
case space_explode name_sep s of


354 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix


355 
 ss => map short_name ss > space_implode "_"


356 
(* term > term *)


357 
val shorten_const_names_in_term =


358 
map_aterms (fn Const (s, T) => Const (short_const_name s, T)  t => t)


359 


360 
(* theory > typ * typ > bool *)


361 
fun type_match thy (T1, T2) =


362 
(Sign.typ_match thy (T2, T1) Vartab.empty; true)


363 
handle Type.TYPE_MATCH => false


364 
(* theory > styp * styp > bool *)


365 
fun const_match thy ((s1, T1), (s2, T2)) =


366 
s1 = s2 andalso type_match thy (T1, T2)


367 
(* theory > term * term > bool *)


368 
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)


369 
 term_match thy (Free (s1, T1), Free (s2, T2)) =


370 
const_match thy ((short_name s1, T1), (short_name s2, T2))


371 
 term_match thy (t1, t2) = t1 aconv t2


372 


373 
(* typ > bool *)


374 
fun is_TFree (TFree _) = true


375 
 is_TFree _ = false


376 
fun is_higher_order_type (Type ("fun", _)) = true


377 
 is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts


378 
 is_higher_order_type _ = false


379 
fun is_fun_type (Type ("fun", _)) = true


380 
 is_fun_type _ = false


381 
fun is_set_type (Type ("fun", [_, @{typ bool}])) = true


382 
 is_set_type _ = false


383 
fun is_pair_type (Type ("*", _)) = true


384 
 is_pair_type _ = false


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


386 
 is_lfp_iterator_type _ = false


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


388 
 is_gfp_iterator_type _ = false


389 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type


390 
val is_boolean_type = equal prop_T orf equal bool_T


391 
val is_integer_type =


392 
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type


393 
val is_record_type = not o null o Record.dest_recTs


394 
(* theory > typ > bool *)


395 
fun is_frac_type thy (Type (s, [])) =


396 
not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy))


397 
s)))


398 
 is_frac_type _ _ = false


399 
fun is_number_type thy = is_integer_type orf is_frac_type thy


400 


401 
(* bool > styp > typ *)


402 
fun iterator_type_for_const gfp (s, T) =


403 
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,


404 
binder_types T)


405 
(* typ > styp *)


406 
fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts > bool_T)


407 
 const_for_iterator_type T =


408 
raise TYPE ("NitpickHOL.const_for_iterator_type", [T], [])


409 


410 
(* int > typ > typ * typ *)


411 
fun strip_n_binders 0 T = ([], T)


412 
 strip_n_binders n (Type ("fun", [T1, T2])) =


413 
strip_n_binders (n  1) T2 >> cons T1


414 
 strip_n_binders n (Type (@{type_name fun_box}, Ts)) =


415 
strip_n_binders n (Type ("fun", Ts))


416 
 strip_n_binders _ T = raise TYPE ("NitpickHOL.strip_n_binders", [T], [])


417 
(* typ > typ *)


418 
val nth_range_type = snd oo strip_n_binders


419 


420 
(* typ > int *)


421 
fun num_factors_in_type (Type ("*", [T1, T2])) =


422 
fold (Integer.add o num_factors_in_type) [T1, T2] 0


423 
 num_factors_in_type _ = 1


424 
fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2


425 
 num_binder_types _ = 0


426 
(* typ > typ list *)


427 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types


428 
fun maybe_curried_binder_types T =


429 
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T


430 


431 
(* typ > term list > term *)


432 
fun mk_flat_tuple _ [t] = t


433 
 mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =


434 
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)


435 
 mk_flat_tuple T ts = raise TYPE ("NitpickHOL.mk_flat_tuple", [T], ts)


436 
(* int > term > term list *)


437 
fun dest_n_tuple 1 t = [t]


438 
 dest_n_tuple n t = HOLogic.dest_prod t > dest_n_tuple (n  1) > op ::


439 


440 
(* int > typ > typ list *)


441 
fun dest_n_tuple_type 1 T = [T]


442 
 dest_n_tuple_type n (Type (_, [T1, T2])) =


443 
T1 :: dest_n_tuple_type (n  1) T2


444 
 dest_n_tuple_type _ T = raise TYPE ("NitpickHOL.dest_n_tuple_type", [T], [])


445 


446 
(* (typ * typ) list > typ > typ *)


447 
fun typ_subst [] T = T


448 
 typ_subst ps T =


449 
let


450 
(* typ > typ *)


451 
fun subst T =


452 
case AList.lookup (op =) ps T of


453 
SOME T' => T'


454 
 NONE => case T of Type (s, Ts) => Type (s, map subst Ts)  _ => T


455 
in subst T end


456 


457 
(* theory > typ > typ > typ > typ *)


458 
fun instantiate_type thy T1 T1' T2 =


459 
Same.commit (Envir.subst_type_same


460 
(Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))


461 
(Logic.varifyT T2)


462 
handle Type.TYPE_MATCH =>


463 
raise TYPE ("NitpickHOL.instantiate_type", [T1, T1'], [])


464 


465 
(* theory > typ > typ > styp *)


466 
fun repair_constr_type thy body_T' T =


467 
instantiate_type thy (body_type T) body_T' T


468 


469 
(* string > (string * string) list > theory > theory *)


470 
fun register_frac_type frac_s ersaetze thy =


471 
let


472 
val {frac_types, codatatypes} = TheoryData.get thy


473 
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types


474 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end


475 
(* string > theory > theory *)


476 
fun unregister_frac_type frac_s = register_frac_type frac_s []


477 


478 
(* typ > string > styp list > theory > theory *)


479 
fun register_codatatype co_T case_name constr_xs thy =


480 
let


481 
val {frac_types, codatatypes} = TheoryData.get thy


482 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs


483 
val (co_s, co_Ts) = dest_Type co_T


484 
val _ =


485 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()


486 
else raise TYPE ("NitpickHOL.register_codatatype", [co_T], [])


487 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))


488 
codatatypes


489 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end


490 
(* typ > theory > theory *)


491 
fun unregister_codatatype co_T = register_codatatype co_T "" []


492 


493 
type typedef_info =


494 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,


495 
set_def: thm option, prop_of_Rep: thm, set_name: string,


496 
Rep_inverse: thm option}


497 


498 
(* theory > string > typedef_info *)


499 
fun typedef_info thy s =


500 
if is_frac_type thy (Type (s, [])) then


501 
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},


502 
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},


503 
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}


504 
> Logic.varify,


505 
set_name = @{const_name Frac}, Rep_inverse = NONE}


506 
else case Typedef.get_info thy s of


507 
SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,


508 
...} =>


509 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,


510 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,


511 
set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}


512 
 NONE => NONE


513 


514 
(* string > bool *)


515 
fun is_basic_datatype s =


516 
s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},


517 
@{type_name nat}, @{type_name int}]


518 
(* theory > string > bool *)


519 
val is_typedef = is_some oo typedef_info


520 
val is_real_datatype = is_some oo Datatype.get_info


521 
(* theory > typ > bool *)


522 
fun is_codatatype thy (T as Type (s, _)) =


523 
not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s


524 
> Option.map snd > these))


525 
 is_codatatype _ _ = false


526 
fun is_pure_typedef thy (T as Type (s, _)) =


527 
is_typedef thy s andalso


528 
not (is_real_datatype thy s orelse is_codatatype thy T


529 
orelse is_record_type T orelse is_integer_type T)


530 
 is_pure_typedef _ _ = false


531 
fun is_univ_typedef thy (Type (s, _)) =


532 
(case typedef_info thy s of


533 
SOME {set_def, prop_of_Rep, ...} =>


534 
(case set_def of


535 
SOME thm =>


536 
try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm


537 
 NONE =>


538 
try (fst o dest_Const o snd o HOLogic.dest_mem


539 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}


540 
 NONE => false)


541 
 is_univ_typedef _ _ = false


542 
fun is_datatype thy (T as Type (s, _)) =


543 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})


544 
andalso not (is_basic_datatype s)


545 
 is_datatype _ _ = false


546 


547 
(* theory > typ > (string * typ) list * (string * typ) *)


548 
fun all_record_fields thy T =


549 
let val (recs, more) = Record.get_extT_fields thy T in


550 
recs @ more :: all_record_fields thy (snd more)


551 
end


552 
handle TYPE _ => []


553 
(* styp > bool *)


554 
fun is_record_constr (x as (s, T)) =


555 
String.isSuffix Record.extN s andalso


556 
let val dataT = body_type T in


557 
is_record_type dataT andalso


558 
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN


559 
end


560 
(* theory > typ > int *)


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


562 
(* theory > string > typ > int *)


563 
fun no_of_record_field thy s T1 =


564 
find_index (equal s o fst) (Record.get_extT_fields thy T1 > single > op @)


565 
(* theory > styp > bool *)


566 
fun is_record_get thy (s, Type ("fun", [T1, _])) =


567 
exists (equal s o fst) (all_record_fields thy T1)


568 
 is_record_get _ _ = false


569 
fun is_record_update thy (s, T) =


570 
String.isSuffix Record.updateN s andalso


571 
exists (equal (unsuffix Record.updateN s) o fst)


572 
(all_record_fields thy (body_type T))


573 
handle TYPE _ => false


574 
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =


575 
(case typedef_info thy s' of


576 
SOME {Abs_name, ...} => s = Abs_name


577 
 NONE => false)


578 
 is_abs_fun _ _ = false


579 
fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =


580 
(case typedef_info thy s' of


581 
SOME {Rep_name, ...} => s = Rep_name


582 
 NONE => false)


583 
 is_rep_fun _ _ = false


584 


585 
(* theory > styp > styp *)


586 
fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =


587 
(case typedef_info thy s' of


588 
SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))


589 
 NONE => raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x]))


590 
 mate_of_rep_fun _ x = raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x])


591 


592 
(* theory > styp > bool *)


593 
fun is_coconstr thy (s, T) =


594 
let


595 
val {codatatypes, ...} = TheoryData.get thy


596 
val co_T = body_type T


597 
val co_s = dest_Type co_T > fst


598 
in


599 
exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)


600 
(AList.lookup (op =) codatatypes co_s > Option.map snd > these)


601 
end


602 
handle TYPE ("dest_Type", _, _) => false


603 
fun is_constr_like thy (s, T) =


604 
s mem [@{const_name FunBox}, @{const_name PairBox}] orelse


605 
let val (x as (s, T)) = (s, unbox_type T) in


606 
Refute.is_IDT_constructor thy x orelse is_record_constr x


607 
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))


608 
orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]


609 
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)


610 
orelse is_coconstr thy x


611 
end


612 
fun is_constr thy (x as (_, T)) =


613 
is_constr_like thy x


614 
andalso not (is_basic_datatype (fst (dest_Type (body_type T))))


615 
(* string > bool *)


616 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix


617 
val is_sel_like_and_no_discr =


618 
String.isPrefix sel_prefix


619 
orf (member (op =) [@{const_name fst}, @{const_name snd}])


620 


621 
datatype boxability =


622 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2


623 


624 
(* boxability > boxability *)


625 
fun in_fun_lhs_for InConstr = InSel


626 
 in_fun_lhs_for _ = InFunLHS


627 
fun in_fun_rhs_for InConstr = InConstr


628 
 in_fun_rhs_for InSel = InSel


629 
 in_fun_rhs_for InFunRHS1 = InFunRHS2


630 
 in_fun_rhs_for _ = InFunRHS1


631 


632 
(* extended_context > boxability > typ > bool *)


633 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =


634 
case T of


635 
Type ("fun", _) =>


636 
boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))


637 
 Type ("*", Ts) =>


638 
boxy mem [InPair, InFunRHS1, InFunRHS2]


639 
orelse (boxy mem [InExpr, InFunLHS]


640 
andalso exists (is_boxing_worth_it ext_ctxt InPair)


641 
(map (box_type ext_ctxt InPair) Ts))


642 
 _ => false


643 
(* extended_context > boxability > string * typ list > string *)


644 
and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =


645 
case triple_lookup (type_match thy) boxes (Type z) of


646 
SOME (SOME box_me) => box_me


647 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z)


648 
(* extended_context > boxability > typ > typ *)


649 
and box_type ext_ctxt boxy T =


650 
case T of


651 
Type (z as ("fun", [T1, T2])) =>


652 
if not (boxy mem [InConstr, InSel])


653 
andalso should_box_type ext_ctxt boxy z then


654 
Type (@{type_name fun_box},


655 
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])


656 
else


657 
box_type ext_ctxt (in_fun_lhs_for boxy) T1


658 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2


659 
 Type (z as ("*", Ts)) =>


660 
if should_box_type ext_ctxt boxy z then


661 
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)


662 
else


663 
Type ("*", map (box_type ext_ctxt


664 
(if boxy mem [InConstr, InSel] then boxy


665 
else InPair)) Ts)


666 
 _ => T


667 


668 
(* styp > styp *)


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


670 


671 
(* typ > int *)


672 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)


673 
(* string > int > string *)


674 
fun nth_sel_name_for_constr_name s n =


675 
if s = @{const_name Pair} then


676 
if n = 0 then @{const_name fst} else @{const_name snd}


677 
else


678 
sel_prefix_for n ^ s


679 
(* styp > int > styp *)


680 
fun nth_sel_for_constr x ~1 = discr_for_constr x


681 
 nth_sel_for_constr (s, T) n =


682 
(nth_sel_name_for_constr_name s n,


683 
body_type T > nth (maybe_curried_binder_types T) n)


684 
(* extended_context > styp > int > styp *)


685 
fun boxed_nth_sel_for_constr ext_ctxt =


686 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr


687 


688 
(* string > int *)


689 
fun sel_no_from_name s =


690 
if String.isPrefix discr_prefix s then


691 
~1


692 
else if String.isPrefix sel_prefix s then


693 
s > unprefix sel_prefix > Int.fromString > the


694 
else if s = @{const_name snd} then


695 
1


696 
else


697 
0


698 


699 
(* typ list > term > int > term *)


700 
fun eta_expand _ t 0 = t


701 
 eta_expand Ts (Abs (s, T, t')) n =


702 
Abs (s, T, eta_expand (T :: Ts) t' (n  1))


703 
 eta_expand Ts t n =


704 
fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))


705 
(List.take (binder_types (fastype_of1 (Ts, t)), n))


706 
(list_comb (incr_boundvars n t, map Bound (n  1 downto 0)))


707 


708 
(* term > term *)


709 
fun extensionalize t =


710 
case t of


711 
(t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1


712 
 Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>


713 
let val v = Var ((s, maxidx_of_term t + 1), T) in


714 
extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))


715 
end


716 
 _ => t


717 


718 
(* typ > term list > term *)


719 
fun distinctness_formula T =


720 
all_distinct_unordered_pairs_of


721 
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))


722 
#> List.foldr (s_conj o swap) @{const True}


723 


724 
(* typ > term *)


725 
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)


726 
fun suc_const T = Const (@{const_name Suc}, T > T)


727 


728 
(* theory > typ > styp list *)


729 
fun datatype_constrs thy (T as Type (s, Ts)) =


730 
if is_datatype thy T then


731 
case Datatype.get_info thy s of


732 
SOME {index, descr, ...} =>


733 
let val (_, dtyps, constrs) = AList.lookup (op =) descr index > the in


734 
map (fn (s', Us) =>


735 
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us > T))


736 
constrs


737 
end


738 
 NONE =>


739 
case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of


740 
SOME (_, xs' as (_ :: _)) =>


741 
map (apsnd (repair_constr_type thy T)) xs'


742 
 _ =>


743 
if is_record_type T then


744 
let


745 
val s' = unsuffix Record.ext_typeN s ^ Record.extN


746 
val T' = (Record.get_extT_fields thy T


747 
> apsnd single > uncurry append > map snd) > T


748 
in [(s', T')] end


749 
else case typedef_info thy s of


750 
SOME {abs_type, rep_type, Abs_name, ...} =>


751 
[(Abs_name, instantiate_type thy abs_type T rep_type > T)]


752 
 NONE =>


753 
if T = @{typ ind} then


754 
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]


755 
else


756 
[]


757 
else


758 
[]


759 
 datatype_constrs _ _ = []


760 
(* extended_context > typ > styp list *)


761 
fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) =


762 
map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy


763 
(* theory > typ > int *)


764 
val num_datatype_constrs = length oo datatype_constrs


765 


766 
(* string > string *)


767 
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}


768 
 constr_name_for_sel_like @{const_name snd} = @{const_name Pair}


769 
 constr_name_for_sel_like s' = original_name s'


770 
(* extended_context > styp > styp *)


771 
fun boxed_constr_for_sel ext_ctxt (s', T') =


772 
let val s = constr_name_for_sel_like s' in


773 
AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s


774 
> the > pair s


775 
end


776 
(* theory > styp > term *)


777 
fun discr_term_for_constr thy (x as (s, T)) =


778 
let val dataT = body_type T in


779 
if s = @{const_name Suc} then


780 
Abs (Name.uu, dataT,


781 
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))


782 
else if num_datatype_constrs thy dataT >= 2 then


783 
Const (discr_for_constr x)


784 
else


785 
Abs (Name.uu, dataT, @{const True})


786 
end


787 


788 
(* theory > styp > term > term *)


789 
fun discriminate_value thy (x as (_, T)) t =


790 
case strip_comb t of


791 
(Const x', args) =>


792 
if x = x' then @{const True}


793 
else if is_constr_like thy x' then @{const False}


794 
else betapply (discr_term_for_constr thy x, t)


795 
 _ => betapply (discr_term_for_constr thy x, t)


796 


797 
(* styp > term > term *)


798 
fun nth_arg_sel_term_for_constr (x as (s, T)) n =


799 
let val (arg_Ts, dataT) = strip_type T in


800 
if dataT = nat_T then


801 
@{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}


802 
else if is_pair_type dataT then


803 
Const (nth_sel_for_constr x n)


804 
else


805 
let


806 
(* int > typ > int * term *)


807 
fun aux m (Type ("*", [T1, T2])) =


808 
let


809 
val (m, t1) = aux m T1


810 
val (m, t2) = aux m T2


811 
in (m, HOLogic.mk_prod (t1, t2)) end


812 
 aux m T =


813 
(m + 1, Const (nth_sel_name_for_constr_name s m, dataT > T)


814 
$ Bound 0)


815 
val m = fold (Integer.add o num_factors_in_type)


816 
(List.take (arg_Ts, n)) 0


817 
in Abs ("x", dataT, aux m (nth arg_Ts n) > snd) end


818 
end


819 
(* theory > styp > term > int > typ > term *)


820 
fun select_nth_constr_arg thy x t n res_T =


821 
case strip_comb t of


822 
(Const x', args) =>


823 
if x = x' then nth args n


824 
else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)


825 
else betapply (nth_arg_sel_term_for_constr x n, t)


826 
 _ => betapply (nth_arg_sel_term_for_constr x n, t)


827 


828 
(* theory > styp > term list > term *)


829 
fun construct_value _ x [] = Const x


830 
 construct_value thy (x as (s, _)) args =


831 
let val args = map Envir.eta_contract args in


832 
case hd args of


833 
Const (x' as (s', _)) $ t =>


834 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s


835 
andalso forall (fn (n, t') =>


836 
select_nth_constr_arg thy x t n dummyT = t')


837 
(index_seq 0 (length args) ~~ args) then


838 
t


839 
else


840 
list_comb (Const x, args)


841 
 _ => list_comb (Const x, args)


842 
end


843 


844 
(* theory > typ > term > term *)


845 
fun constr_expand thy T t =


846 
(case head_of t of


847 
Const x => if is_constr_like thy x then t else raise SAME ()


848 
 _ => raise SAME ())


849 
handle SAME () =>


850 
let


851 
val x' as (_, T') =


852 
if is_pair_type T then


853 
let val (T1, T2) = HOLogic.dest_prodT T in


854 
(@{const_name Pair}, [T1, T2] > T)


855 
end


856 
else


857 
datatype_constrs thy T > the_single


858 
val arg_Ts = binder_types T'


859 
in


860 
list_comb (Const x', map2 (select_nth_constr_arg thy x' t)


861 
(index_seq 0 (length arg_Ts)) arg_Ts)


862 
end


863 


864 
(* (typ * int) list > typ > int *)


865 
fun card_of_type asgns (Type ("fun", [T1, T2])) =


866 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)


867 
 card_of_type asgns (Type ("*", [T1, T2])) =


868 
card_of_type asgns T1 * card_of_type asgns T2


869 
 card_of_type _ (Type (@{type_name itself}, _)) = 1


870 
 card_of_type _ @{typ prop} = 2


871 
 card_of_type _ @{typ bool} = 2


872 
 card_of_type _ @{typ unit} = 1


873 
 card_of_type asgns T =


874 
case AList.lookup (op =) asgns T of


875 
SOME k => k


876 
 NONE => if T = @{typ bisim_iterator} then 0


877 
else raise TYPE ("NitpickHOL.card_of_type", [T], [])


878 
(* int > (typ * int) list > typ > int *)


879 
fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =


880 
let


881 
val k1 = bounded_card_of_type max default_card asgns T1


882 
val k2 = bounded_card_of_type max default_card asgns T2


883 
in


884 
if k1 = max orelse k2 = max then max


885 
else Int.min (max, reasonable_power k2 k1)


886 
end


887 
 bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =


888 
let


889 
val k1 = bounded_card_of_type max default_card asgns T1


890 
val k2 = bounded_card_of_type max default_card asgns T2


891 
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end


892 
 bounded_card_of_type max default_card asgns T =


893 
Int.min (max, if default_card = ~1 then


894 
card_of_type asgns T


895 
else


896 
card_of_type asgns T


897 
handle TYPE ("NitpickHOL.card_of_type", _, _) =>


898 
default_card)


899 
(* theory > int > (typ * int) list > typ > int *)


900 
fun bounded_precise_card_of_type thy max default_card asgns T =


901 
let


902 
(* typ list > typ > int *)


903 
fun aux avoid T =


904 
(if T mem avoid then


905 
0


906 
else case T of


907 
Type ("fun", [T1, T2]) =>


908 
let


909 
val k1 = aux avoid T1


910 
val k2 = aux avoid T2


911 
in


912 
if k1 = 0 orelse k2 = 0 then 0


913 
else if k1 >= max orelse k2 >= max then max


914 
else Int.min (max, reasonable_power k2 k1)


915 
end


916 
 Type ("*", [T1, T2]) =>


917 
let


918 
val k1 = aux avoid T1


919 
val k2 = aux avoid T2


920 
in


921 
if k1 = 0 orelse k2 = 0 then 0


922 
else if k1 >= max orelse k2 >= max then max


923 
else Int.min (max, k1 * k2)


924 
end


925 
 Type (@{type_name itself}, _) => 1


926 
 @{typ prop} => 2


927 
 @{typ bool} => 2


928 
 @{typ unit} => 1


929 
 Type _ =>


930 
(case datatype_constrs thy T of


931 
[] => if is_integer_type T then 0 else raise SAME ()


932 
 constrs =>


933 
let


934 
val constr_cards =


935 
datatype_constrs thy T


936 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types


937 
o snd)


938 
in


939 
if exists (equal 0) constr_cards then 0


940 
else Integer.sum constr_cards


941 
end)


942 
 _ => raise SAME ())


943 
handle SAME () => AList.lookup (op =) asgns T > the_default default_card


944 
in Int.min (max, aux [] T) end


945 


946 
(* theory > typ > bool *)


947 
fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 []


948 


949 
(* term > bool *)


950 
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2


951 
 is_ground_term (Const _) = true


952 
 is_ground_term _ = false


953 


954 
(* term > word > word *)


955 
fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)


956 
 hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)


957 
 hashw_term _ = 0w0


958 
(* term > int *)


959 
val hash_term = Word.toInt o hashw_term


960 


961 
(* term list > (indexname * typ) list *)


962 
fun special_bounds ts =


963 
fold Term.add_vars ts [] > sort (TermOrd.fast_indexname_ord o pairself fst)


964 


965 
(* indexname * typ > term > term *)


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


967 


968 
(* term > bool *)


969 
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)


970 
$ Const (@{const_name TYPE}, _)) = true


971 
 is_arity_type_axiom _ = false


972 
(* theory > bool > term > bool *)


973 
fun is_typedef_axiom thy only_boring (@{const "==>"} $ _ $ t2) =


974 
is_typedef_axiom thy only_boring t2


975 
 is_typedef_axiom thy only_boring


976 
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)


977 
$ Const (_, Type ("fun", [T as Type (s, _), _])) $ Const _ $ _)) =


978 
is_typedef thy s


979 
andalso not (only_boring andalso


980 
(s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]


981 
orelse is_frac_type thy T))


982 
 is_typedef_axiom _ _ _ = false


983 


984 
(* Distinguishes between (1) constant definition axioms, (2) type arity and


985 
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).


986 
Typedef axioms are uninteresting to Nitpick, because it can retrieve them


987 
using "typedef_info". *)


988 
(* theory > (string * term) list > string list > term list * term list *)


989 
fun partition_axioms_by_definitionality thy axioms def_names =


990 
let


991 
val axioms = sort (fast_string_ord o pairself fst) axioms


992 
val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms


993 
val nondefs =


994 
OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms


995 
> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)


996 
in pairself (map snd) (defs, nondefs) end


997 


998 
(* Ideally we would check against "Complex_Main", not "Quickcheck", but any


999 
theory will do as long as it contains all the "axioms" and "axiomatization"


1000 
commands. *)


1001 
(* theory > bool *)


1002 
fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})


1003 


1004 
(* term > bool *)


1005 
val is_plain_definition =


1006 
let


1007 
(* term > bool *)


1008 
fun do_lhs t1 =


1009 
case strip_comb t1 of


1010 
(Const _, args) => forall is_Var args


1011 
andalso not (has_duplicates (op =) args)


1012 
 _ => false


1013 
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1


1014 
 do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =


1015 
do_lhs t1


1016 
 do_eq _ = false


1017 
in do_eq end


1018 


1019 
(* This table is not pretty. A better approach would be to avoid expanding the


1020 
operators to their lowlevel definitions, but this would require dealing with


1021 
overloading. *)


1022 
val built_in_built_in_defs =


1023 
[@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},


1024 
@{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},


1025 
@{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},


1026 
@{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},


1027 
@{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},


1028 
@{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},


1029 
@{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},


1030 
@{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},


1031 
@{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},


1032 
@{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},


1033 
@{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},


1034 
@{thm zero_nat_inst.zero_nat}]


1035 
> map prop_of


1036 


1037 
(* theory > term list * term list * term list *)


1038 
fun all_axioms_of thy =


1039 
let


1040 
(* theory list > term list *)


1041 
val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)


1042 
val specs = Defs.all_specifications_of (Theory.defs_of thy)


1043 
val def_names =


1044 
specs > maps snd


1045 
> filter #is_def > map #name > OrdList.make fast_string_ord


1046 
val thys = thy :: Theory.ancestors_of thy


1047 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys


1048 
val built_in_axioms = axioms_of_thys built_in_thys


1049 
val user_axioms = axioms_of_thys user_thys


1050 
val (built_in_defs, built_in_nondefs) =


1051 
partition_axioms_by_definitionality thy built_in_axioms def_names


1052 
> apsnd (filter (is_typedef_axiom thy false))


1053 
val (user_defs, user_nondefs) =


1054 
partition_axioms_by_definitionality thy user_axioms def_names


1055 
val defs = built_in_built_in_defs @


1056 
(thy > PureThy.all_thms_of


1057 
> filter (equal Thm.definitionK o Thm.get_kind o snd)


1058 
> map (prop_of o snd) > filter is_plain_definition) @


1059 
user_defs @ built_in_defs


1060 
in (defs, built_in_nondefs, user_nondefs) end


1061 


1062 
(* bool > styp > int option *)


1063 
fun arity_of_built_in_const fast_descrs (s, T) =


1064 
if s = @{const_name If} then


1065 
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3


1066 
else case AList.lookup (op =)


1067 
(built_in_consts


1068 
> fast_descrs ? append built_in_descr_consts) s of


1069 
SOME n => SOME n


1070 
 NONE =>


1071 
case AList.lookup (op =) built_in_typed_consts (s, T) of


1072 
SOME n => SOME n


1073 
 NONE =>


1074 
if is_fun_type T andalso is_set_type (domain_type T) then


1075 
AList.lookup (op =) built_in_set_consts s


1076 
else


1077 
NONE


1078 
(* bool > styp > bool *)


1079 
val is_built_in_const = is_some oo arity_of_built_in_const


1080 


1081 
(* This function is designed to work for both real definition axioms and


1082 
simplification rules (equational specifications). *)


1083 
(* term > term *)


1084 
fun term_under_def t =


1085 
case t of


1086 
@{const "==>"} $ _ $ t2 => term_under_def t2


1087 
 Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1


1088 
 @{const Trueprop} $ t1 => term_under_def t1


1089 
 Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1


1090 
 Abs (_, _, t') => term_under_def t'


1091 
 t1 $ _ => term_under_def t1


1092 
 _ => t


1093 


1094 
(* Here we crucially rely on "Refute.specialize_type" performing a preorder


1095 
traversal of the term, without which the wrong occurrence of a constant could


1096 
be matched in the face of overloading. *)


1097 
(* theory > bool > const_table > styp > term list *)


1098 
fun def_props_for_const thy fast_descrs table (x as (s, _)) =


1099 
if is_built_in_const fast_descrs x then


1100 
[]


1101 
else


1102 
these (Symtab.lookup table s)


1103 
> map_filter (try (Refute.specialize_type thy x))


1104 
> filter (equal (Const x) o term_under_def)


1105 


1106 
(* term > term *)


1107 
fun normalized_rhs_of thy t =


1108 
let


1109 
(* term > term *)


1110 
fun aux (v as Var _) t = lambda v t


1111 
 aux (c as Const (@{const_name TYPE}, T)) t = lambda c t


1112 
 aux _ _ = raise TERM ("NitpickHOL.normalized_rhs_of", [t])


1113 
val (lhs, rhs) =


1114 
case t of


1115 
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)


1116 
 @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>


1117 
(t1, t2)


1118 
 _ => raise TERM ("NitpickHOL.normalized_rhs_of", [t])


1119 
val args = strip_comb lhs > snd


1120 
in fold_rev aux args rhs end


1121 


1122 
(* theory > const_table > styp > term option *)


1123 
fun def_of_const thy table (x as (s, _)) =


1124 
if is_built_in_const false x orelse original_name s <> s then


1125 
NONE


1126 
else


1127 
x > def_props_for_const thy false table > List.last


1128 
> normalized_rhs_of thy > prefix_abs_vars s > SOME


1129 
handle List.Empty => NONE


1130 


1131 
datatype fixpoint_kind = Lfp  Gfp  NoFp


1132 


1133 
(* term > fixpoint_kind *)


1134 
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t


1135 
 fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp


1136 
 fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp


1137 
 fixpoint_kind_of_rhs _ = NoFp


1138 


1139 
(* theory > const_table > term > bool *)


1140 
fun is_mutually_inductive_pred_def thy table t =


1141 
let


1142 
(* term > bool *)


1143 
fun is_good_arg (Bound _) = true


1144 
 is_good_arg (Const (s, _)) =


1145 
s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]


1146 
 is_good_arg _ = false


1147 
in


1148 
case t > strip_abs_body > strip_comb of


1149 
(Const x, ts as (_ :: _)) =>


1150 
(case def_of_const thy table x of


1151 
SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts


1152 
 NONE => false)


1153 
 _ => false


1154 
end


1155 
(* theory > const_table > term > term *)


1156 
fun unfold_mutually_inductive_preds thy table =


1157 
map_aterms (fn t as Const x =>


1158 
(case def_of_const thy table x of


1159 
SOME t' =>


1160 
let val t' = Envir.eta_contract t' in


1161 
if is_mutually_inductive_pred_def thy table t' then t'


1162 
else t


1163 
end


1164 
 NONE => t)


1165 
 t => t)


1166 


1167 
(* term > string * term *)


1168 
fun pair_for_prop t =


1169 
case term_under_def t of


1170 
Const (s, _) => (s, t)


1171 
 Free _ => raise NOT_SUPPORTED "local definitions"


1172 
 t' => raise TERM ("NitpickHOL.pair_for_prop", [t, t'])


1173 


1174 
(* (Proof.context > term list) > Proof.context > const_table *)


1175 
fun table_for get ctxt =


1176 
get ctxt > map pair_for_prop > AList.group (op =) > Symtab.make


1177 


1178 
(* theory > (string * int) list *)


1179 
fun case_const_names thy =


1180 
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>


1181 
if is_basic_datatype dtype_s then


1182 
I


1183 
else


1184 
cons (case_name, AList.lookup (op =) descr index


1185 
> the > #3 > length))


1186 
(Datatype.get_all thy) [] @


1187 
map (apsnd length o snd) (#codatatypes (TheoryData.get thy))


1188 


1189 
(* Proof.context > term list > const_table *)


1190 
fun const_def_table ctxt ts =


1191 
table_for (map prop_of o Nitpick_Defs.get) ctxt


1192 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))


1193 
(map pair_for_prop ts)


1194 
(* term list > const_table *)


1195 
fun const_nondef_table ts =


1196 
fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []


1197 
> AList.group (op =) > Symtab.make


1198 
(* Proof.context > const_table *)


1199 
val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)


1200 
val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)


1201 
(* Proof.context > const_table > const_table *)


1202 
fun inductive_intro_table ctxt def_table =


1203 
table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)


1204 
def_table o prop_of)


1205 
o Nitpick_Intros.get) ctxt


1206 
(* theory > term list Inttab.table *)


1207 
fun ground_theorem_table thy =


1208 
fold ((fn @{const Trueprop} $ t1 =>


1209 
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)


1210 
 _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty


1211 


1212 
val basic_ersatz_table =


1213 
[(@{const_name prod_case}, @{const_name split}),


1214 
(@{const_name card}, @{const_name card'}),


1215 
(@{const_name setsum}, @{const_name setsum'}),


1216 
(@{const_name fold_graph}, @{const_name fold_graph'}),


1217 
(@{const_name wf}, @{const_name wf'}),


1218 
(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),


1219 
(@{const_name wfrec}, @{const_name wfrec'})]


1220 


1221 
(* theory > (string * string) list *)


1222 
fun ersatz_table thy =


1223 
fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table


1224 


1225 
(* const_table Unsynchronized.ref > string > term list > unit *)


1226 
fun add_simps simp_table s eqs =


1227 
Unsynchronized.change simp_table


1228 
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))


1229 


1230 
(* Similar to "Refute.specialize_type" but returns all matches rather than only


1231 
the first (preorder) match. *)


1232 
(* theory > styp > term > term list *)


1233 
fun multi_specialize_type thy (x as (s, T)) t =


1234 
let


1235 
(* term > (typ * term) list > (typ * term) list *)


1236 
fun aux (Const (s', T')) ys =


1237 
if s = s' then


1238 
(if AList.defined (op =) ys T' then


1239 
I


1240 
else if T = T' then


1241 
cons (T, t)


1242 
else


1243 
cons (T', Refute.monomorphic_term


1244 
(Sign.typ_match thy (T', T) Vartab.empty) t)


1245 
handle Type.TYPE_MATCH => I) ys


1246 
else


1247 
ys


1248 
 aux _ ys = ys


1249 
in map snd (fold_aterms aux t []) end


1250 


1251 
(* theory > const_table > styp > term list *)


1252 
fun nondef_props_for_const thy table (x as (s, _)) =


1253 
these (Symtab.lookup table s) > maps (multi_specialize_type thy x)


1254 
handle Refute.REFUTE _ =>


1255 
raise NOT_SUPPORTED ("too much polymorphism in axiom involving " ^


1256 
quote s)


1257 


1258 
(* theory > styp list > term list *)


1259 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) =


1260 
let val abs_T = Type (abs_s, abs_Ts) in


1261 
if is_univ_typedef thy abs_T then


1262 
[]


1263 
else case typedef_info thy abs_s of


1264 
SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,


1265 
...} =>


1266 
let


1267 
val rep_T = instantiate_type thy abs_type abs_T rep_type


1268 
val rep_t = Const (Rep_name, abs_T > rep_T)


1269 
val set_t = Const (set_name, rep_T > bool_T)


1270 
val set_t' =


1271 
prop_of_Rep > HOLogic.dest_Trueprop


1272 
> Refute.specialize_type thy (dest_Const rep_t)


1273 
> HOLogic.dest_mem > snd


1274 
in


1275 
[HOLogic.all_const abs_T


1276 
$ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]


1277 
> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))


1278 
> map HOLogic.mk_Trueprop


1279 
end


1280 
 NONE => []


1281 
end


1282 
(* theory > styp > term *)


1283 
fun inverse_axiom_for_rep_fun thy (x as (_, T)) =


1284 
typedef_info thy (fst (dest_Type (domain_type T)))


1285 
> the > #Rep_inverse > the > prop_of > Refute.specialize_type thy x


1286 


1287 
(* theory > int * styp > term *)


1288 
fun constr_case_body thy (j, (x as (_, T))) =


1289 
let val arg_Ts = binder_types T in


1290 
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))


1291 
(index_seq 0 (length arg_Ts)) arg_Ts)


1292 
end


1293 
(* theory > typ > int * styp > term > term *)


1294 
fun add_constr_case thy res_T (j, x) res_t =


1295 
Const (@{const_name If}, [bool_T, res_T, res_T] > res_T)


1296 
$ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t


1297 
(* theory > typ > typ > term *)


1298 
fun optimized_case_def thy dataT res_T =


1299 
let


1300 
val xs = datatype_constrs thy dataT


1301 
val func_Ts = map ((fn T => binder_types T > res_T) o snd) xs


1302 
val (xs', x) = split_last xs


1303 
in


1304 
constr_case_body thy (1, x)


1305 
> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')


1306 
> fold_rev (curry absdummy) (func_Ts @ [dataT])


1307 
end


1308 


1309 
val redefined_in_NitpickDefs_thy =


1310 
[@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},


1311 
@{const_name list_size}]


1312 


1313 
(* theory > string > typ > typ > term > term *)


1314 
fun optimized_record_get thy s rec_T res_T t =


1315 
let val constr_x = the_single (datatype_constrs thy rec_T) in


1316 
case no_of_record_field thy s rec_T of


1317 
~1 => (case rec_T of


1318 
Type (_, Ts as _ :: _) =>


1319 
let


1320 
val rec_T' = List.last Ts


1321 
val j = num_record_fields thy rec_T  1


1322 
in


1323 
select_nth_constr_arg thy constr_x t j res_T


1324 
> optimized_record_get thy s rec_T' res_T


1325 
end


1326 
 _ => raise TYPE ("NitpickHOL.optimized_record_get", [rec_T], []))


1327 
 j => select_nth_constr_arg thy constr_x t j res_T


1328 
end


1329 
(* theory > string > typ > term > term > term *)


1330 
fun optimized_record_update thy s rec_T fun_t rec_t =


1331 
let


1332 
val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T)


1333 
val Ts = binder_types constr_T


1334 
val n = length Ts


1335 
val special_j = no_of_record_field thy s rec_T


1336 
val ts = map2 (fn j => fn T =>


1337 
let


1338 
val t = select_nth_constr_arg thy constr_x rec_t j T


1339 
in


1340 
if j = special_j then


1341 
betapply (fun_t, t)


1342 
else if j = n  1 andalso special_j = ~1 then


1343 
optimized_record_update thy s


1344 
(rec_T > dest_Type > snd > List.last) fun_t t


1345 
else


1346 
t


1347 
end) (index_seq 0 n) Ts


1348 
in list_comb (Const constr_x, ts) end


1349 


1350 
(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a


1351 
constant, are said to be trivial. For those, we ignore the simplification


1352 
rules and use the definition instead, to ensure that builtin symbols like


1353 
"ord_nat_inst.less_eq_nat" are picked up correctly. *)


1354 
(* theory > const_table > styp > bool *)


1355 
fun has_trivial_definition thy table x =


1356 
case def_of_const thy table x of SOME (Const _) => true  _ => false


1357 


1358 
(* theory > const_table > string * typ > fixpoint_kind *)


1359 
fun fixpoint_kind_of_const thy table x =


1360 
if is_built_in_const false x then


1361 
NoFp


1362 
else


1363 
fixpoint_kind_of_rhs (the (def_of_const thy table x))


1364 
handle Option.Option => NoFp


1365 


1366 
(* extended_context > styp > bool *)


1367 
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}


1368 
: extended_context) x =


1369 
not (null (def_props_for_const thy fast_descrs intro_table x))


1370 
andalso fixpoint_kind_of_const thy def_table x <> NoFp


1371 
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}


1372 
: extended_context) x =


1373 
exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))


1374 
[!simp_table, psimp_table]


1375 
fun is_inductive_pred ext_ctxt =


1376 
is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)


1377 
fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =


1378 
(is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt


1379 
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)


1380 
andf (not o has_trivial_definition thy def_table)


1381 
andf (not o member (op =) redefined_in_NitpickDefs_thy o fst)


1382 


1383 
(* term * term > term *)


1384 
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t


1385 
 s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t


1386 
 s_betapply p = betapply p


1387 
(* term * term list > term *)


1388 
val s_betapplys = Library.foldl s_betapply


1389 


1390 
(* term > term *)


1391 
fun lhs_of_equation t =


1392 
case t of


1393 
Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1


1394 
 Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1


1395 
 @{const "==>"} $ _ $ t2 => lhs_of_equation t2


1396 
 @{const Trueprop} $ t1 => lhs_of_equation t1


1397 
 Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1


1398 
 Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1


1399 
 @{const "op >"} $ _ $ t2 => lhs_of_equation t2


1400 
 _ => NONE

08a39a957ed7
added Nitpick's theory and ML files to Isabelle/HOL;
