1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 18 10:38:37 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 18 18:48:07 2010 +0100
1.3 @@ -85,6 +85,7 @@
1.4 val is_integer_type : typ -> bool
1.5 val is_bit_type : typ -> bool
1.6 val is_word_type : typ -> bool
1.7 + val is_integer_like_type : typ -> bool
1.8 val is_record_type : typ -> bool
1.9 val is_number_type : theory -> typ -> bool
1.10 val const_for_iterator_type : typ -> styp
1.11 @@ -95,14 +96,13 @@
1.12 val curried_binder_types : typ -> typ list
1.13 val mk_flat_tuple : typ -> term list -> term
1.14 val dest_n_tuple : int -> term -> term list
1.15 - val instantiate_type : theory -> typ -> typ -> typ -> typ
1.16 val is_real_datatype : theory -> string -> bool
1.17 - val is_standard_datatype : hol_context -> typ -> bool
1.18 + val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
1.19 val is_quot_type : theory -> typ -> bool
1.20 val is_codatatype : theory -> typ -> bool
1.21 val is_pure_typedef : theory -> typ -> bool
1.22 val is_univ_typedef : theory -> typ -> bool
1.23 - val is_datatype : theory -> typ -> bool
1.24 + val is_datatype : theory -> (typ option * bool) list -> typ -> bool
1.25 val is_record_constr : styp -> bool
1.26 val is_record_get : theory -> styp -> bool
1.27 val is_record_update : theory -> styp -> bool
1.28 @@ -113,7 +113,7 @@
1.29 val mate_of_rep_fun : theory -> styp -> styp
1.30 val is_constr_like : theory -> styp -> bool
1.31 val is_stale_constr : theory -> styp -> bool
1.32 - val is_constr : theory -> styp -> bool
1.33 + val is_constr : theory -> (typ option * bool) list -> styp -> bool
1.34 val is_sel : string -> bool
1.35 val is_sel_like_and_no_discr : string -> bool
1.36 val box_type : hol_context -> boxability -> typ -> typ
1.37 @@ -141,8 +141,10 @@
1.38 val constr_name_for_sel_like : string -> string
1.39 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
1.40 val discriminate_value : hol_context -> styp -> term -> term
1.41 - val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
1.42 - val construct_value : theory -> styp -> term list -> term
1.43 + val select_nth_constr_arg :
1.44 + theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
1.45 + val construct_value :
1.46 + theory -> (typ option * bool) list -> styp -> term list -> term
1.47 val card_of_type : (typ * int) list -> typ -> int
1.48 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
1.49 val bounded_exact_card_of_type :
1.50 @@ -151,10 +153,13 @@
1.51 val special_bounds : term list -> (indexname * typ) list
1.52 val is_funky_typedef : theory -> typ -> bool
1.53 val all_axioms_of : theory -> term list * term list * term list
1.54 - val arity_of_built_in_const : bool -> styp -> int option
1.55 - val is_built_in_const : bool -> styp -> bool
1.56 + val arity_of_built_in_const :
1.57 + theory -> (typ option * bool) list -> bool -> styp -> int option
1.58 + val is_built_in_const :
1.59 + theory -> (typ option * bool) list -> bool -> styp -> bool
1.60 val term_under_def : term -> term
1.61 - val case_const_names : theory -> (string * int) list
1.62 + val case_const_names :
1.63 + theory -> (typ option * bool) list -> (string * int) list
1.64 val const_def_table : Proof.context -> term list -> const_table
1.65 val const_nondef_table : term list -> const_table
1.66 val const_simp_table : Proof.context -> const_table
1.67 @@ -165,7 +170,8 @@
1.68 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
1.69 val inverse_axioms_for_rep_fun : theory -> styp -> term list
1.70 val optimized_typedef_axioms : theory -> string * typ list -> term list
1.71 - val optimized_quot_type_axioms : theory -> string * typ list -> term list
1.72 + val optimized_quot_type_axioms :
1.73 + theory -> (typ option * bool) list -> string * typ list -> term list
1.74 val def_of_const : theory -> const_table -> styp -> term option
1.75 val fixpoint_kind_of_const :
1.76 theory -> const_table -> string * typ -> fixpoint_kind
1.77 @@ -340,44 +346,45 @@
1.78 (@{const_name trancl}, 1),
1.79 (@{const_name rel_comp}, 2),
1.80 (@{const_name image}, 2),
1.81 - (@{const_name Suc}, 0),
1.82 (@{const_name finite}, 1),
1.83 - (@{const_name nat}, 0),
1.84 - (@{const_name zero_nat_inst.zero_nat}, 0),
1.85 - (@{const_name one_nat_inst.one_nat}, 0),
1.86 - (@{const_name plus_nat_inst.plus_nat}, 0),
1.87 - (@{const_name minus_nat_inst.minus_nat}, 0),
1.88 - (@{const_name times_nat_inst.times_nat}, 0),
1.89 - (@{const_name div_nat_inst.div_nat}, 0),
1.90 - (@{const_name ord_nat_inst.less_nat}, 2),
1.91 - (@{const_name ord_nat_inst.less_eq_nat}, 2),
1.92 - (@{const_name nat_gcd}, 0),
1.93 - (@{const_name nat_lcm}, 0),
1.94 - (@{const_name zero_int_inst.zero_int}, 0),
1.95 - (@{const_name one_int_inst.one_int}, 0),
1.96 - (@{const_name plus_int_inst.plus_int}, 0),
1.97 - (@{const_name minus_int_inst.minus_int}, 0),
1.98 - (@{const_name times_int_inst.times_int}, 0),
1.99 - (@{const_name div_int_inst.div_int}, 0),
1.100 - (@{const_name uminus_int_inst.uminus_int}, 0),
1.101 - (@{const_name ord_int_inst.less_int}, 2),
1.102 - (@{const_name ord_int_inst.less_eq_int}, 2),
1.103 (@{const_name unknown}, 0),
1.104 (@{const_name is_unknown}, 1),
1.105 (@{const_name Tha}, 1),
1.106 (@{const_name Frac}, 0),
1.107 (@{const_name norm_frac}, 0)]
1.108 +val built_in_nat_consts =
1.109 + [(@{const_name Suc}, 0),
1.110 + (@{const_name nat}, 0),
1.111 + (@{const_name nat_gcd}, 0),
1.112 + (@{const_name nat_lcm}, 0)]
1.113 val built_in_descr_consts =
1.114 [(@{const_name The}, 1),
1.115 (@{const_name Eps}, 1)]
1.116 val built_in_typed_consts =
1.117 - [((@{const_name of_nat}, nat_T --> int_T), 0),
1.118 - ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
1.119 + [((@{const_name zero_class.zero}, int_T), 0),
1.120 + ((@{const_name one_class.one}, int_T), 0),
1.121 + ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
1.122 + ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
1.123 + ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
1.124 + ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
1.125 + ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
1.126 + ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
1.127 + ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
1.128 +val built_in_typed_nat_consts =
1.129 + [((@{const_name zero_class.zero}, nat_T), 0),
1.130 + ((@{const_name one_class.one}, nat_T), 0),
1.131 + ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
1.132 + ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
1.133 + ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
1.134 + ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
1.135 + ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
1.136 + ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
1.137 + ((@{const_name of_nat}, nat_T --> int_T), 0)]
1.138 val built_in_set_consts =
1.139 - [(@{const_name semilattice_inf_fun_inst.inf_fun}, 2),
1.140 - (@{const_name semilattice_sup_fun_inst.sup_fun}, 2),
1.141 - (@{const_name minus_fun_inst.minus_fun}, 2),
1.142 - (@{const_name ord_fun_inst.less_eq_fun}, 2)]
1.143 + [(@{const_name semilattice_inf_class.inf}, 2),
1.144 + (@{const_name semilattice_sup_class.sup}, 2),
1.145 + (@{const_name minus_class.minus}, 2),
1.146 + (@{const_name ord_class.less_eq}, 2)]
1.147
1.148 (* typ -> typ *)
1.149 fun unarize_type @{typ "unsigned_bit word"} = nat_T
1.150 @@ -449,17 +456,19 @@
1.151 | is_gfp_iterator_type _ = false
1.152 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
1.153 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
1.154 -val is_integer_type =
1.155 - member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
1.156 +fun is_integer_type T = (T = nat_T orelse T = int_T)
1.157 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
1.158 fun is_word_type (Type (@{type_name word}, _)) = true
1.159 | is_word_type _ = false
1.160 +fun is_integer_like_type T =
1.161 + is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
1.162 + T = @{typ bisim_iterator}
1.163 val is_record_type = not o null o Record.dest_recTs
1.164 (* theory -> typ -> bool *)
1.165 fun is_frac_type thy (Type (s, [])) =
1.166 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
1.167 | is_frac_type _ _ = false
1.168 -fun is_number_type thy = is_integer_type orf is_frac_type thy
1.169 +fun is_number_type thy = is_integer_like_type orf is_frac_type thy
1.170
1.171 (* bool -> styp -> typ *)
1.172 fun iterator_type_for_const gfp (s, T) =
1.173 @@ -507,13 +516,41 @@
1.174 | dest_n_tuple_type _ T =
1.175 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
1.176
1.177 +type typedef_info =
1.178 + {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
1.179 + set_def: thm option, prop_of_Rep: thm, set_name: string,
1.180 + Abs_inverse: thm option, Rep_inverse: thm option}
1.181 +
1.182 +(* theory -> string -> typedef_info *)
1.183 +fun typedef_info thy s =
1.184 + if is_frac_type thy (Type (s, [])) then
1.185 + SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
1.186 + Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
1.187 + set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
1.188 + |> Logic.varify,
1.189 + set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
1.190 + else case Typedef.get_info thy s of
1.191 + SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
1.192 + Rep_inverse, ...} =>
1.193 + SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
1.194 + Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
1.195 + set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
1.196 + Rep_inverse = SOME Rep_inverse}
1.197 + | NONE => NONE
1.198 +
1.199 +(* theory -> string -> bool *)
1.200 +val is_typedef = is_some oo typedef_info
1.201 +val is_real_datatype = is_some oo Datatype.get_info
1.202 +(* theory -> (typ option * bool) list -> typ -> bool *)
1.203 +fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
1.204 +
1.205 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
1.206 e.g., by adding a field to "Datatype_Aux.info". *)
1.207 -(* string -> bool *)
1.208 -val is_basic_datatype =
1.209 - member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
1.210 - @{type_name nat}, @{type_name int},
1.211 - "Code_Numeral.code_numeral"]
1.212 +(* theory -> (typ option * bool) list -> string -> bool *)
1.213 +fun is_basic_datatype thy stds s =
1.214 + member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
1.215 + @{type_name int}, "Code_Numeral.code_numeral"] s orelse
1.216 + (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
1.217
1.218 (* theory -> typ -> typ -> typ -> typ *)
1.219 fun instantiate_type thy T1 T1' T2 =
1.220 @@ -544,7 +581,8 @@
1.221 val (co_s, co_Ts) = dest_Type co_T
1.222 val _ =
1.223 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
1.224 - co_s <> "fun" andalso not (is_basic_datatype co_s) then
1.225 + co_s <> "fun" andalso
1.226 + not (is_basic_datatype thy [(NONE, true)] co_s) then
1.227 ()
1.228 else
1.229 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
1.230 @@ -554,35 +592,6 @@
1.231 (* typ -> theory -> theory *)
1.232 fun unregister_codatatype co_T = register_codatatype co_T "" []
1.233
1.234 -type typedef_info =
1.235 - {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
1.236 - set_def: thm option, prop_of_Rep: thm, set_name: string,
1.237 - Abs_inverse: thm option, Rep_inverse: thm option}
1.238 -
1.239 -(* theory -> string -> typedef_info *)
1.240 -fun typedef_info thy s =
1.241 - if is_frac_type thy (Type (s, [])) then
1.242 - SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
1.243 - Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
1.244 - set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
1.245 - |> Logic.varify,
1.246 - set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
1.247 - else case Typedef.get_info thy s of
1.248 - SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
1.249 - Rep_inverse, ...} =>
1.250 - SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
1.251 - Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
1.252 - set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
1.253 - Rep_inverse = SOME Rep_inverse}
1.254 - | NONE => NONE
1.255 -
1.256 -(* theory -> string -> bool *)
1.257 -val is_typedef = is_some oo typedef_info
1.258 -val is_real_datatype = is_some oo Datatype.get_info
1.259 -(* hol_context -> typ -> bool *)
1.260 -fun is_standard_datatype ({thy, stds, ...} : hol_context) =
1.261 - the o triple_lookup (type_match thy) stds
1.262 -
1.263 (* theory -> typ -> bool *)
1.264 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
1.265 | is_quot_type _ (Type ("FSet.fset", _)) = true
1.266 @@ -594,7 +603,8 @@
1.267 fun is_pure_typedef thy (T as Type (s, _)) =
1.268 is_typedef thy s andalso
1.269 not (is_real_datatype thy s orelse is_quot_type thy T orelse
1.270 - is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
1.271 + is_codatatype thy T orelse is_record_type T orelse
1.272 + is_integer_like_type T)
1.273 | is_pure_typedef _ _ = false
1.274 fun is_univ_typedef thy (Type (s, _)) =
1.275 (case typedef_info thy s of
1.276 @@ -607,11 +617,11 @@
1.277 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
1.278 | NONE => false)
1.279 | is_univ_typedef _ _ = false
1.280 -fun is_datatype thy (T as Type (s, _)) =
1.281 +(* theory -> (typ option * bool) list -> typ -> bool *)
1.282 +fun is_datatype thy stds (T as Type (s, _)) =
1.283 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
1.284 - is_quot_type thy T) andalso
1.285 - not (is_basic_datatype s)
1.286 - | is_datatype _ _ = false
1.287 + is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
1.288 + | is_datatype _ _ _ = false
1.289
1.290 (* theory -> typ -> (string * typ) list * (string * typ) *)
1.291 fun all_record_fields thy T =
1.292 @@ -699,15 +709,16 @@
1.293 let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
1.294 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
1.295 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
1.296 - x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
1.297 is_coconstr thy x
1.298 end
1.299 fun is_stale_constr thy (x as (_, T)) =
1.300 is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
1.301 not (is_coconstr thy x)
1.302 -fun is_constr thy (x as (_, T)) =
1.303 +(* theory -> (typ option * bool) list -> styp -> bool *)
1.304 +fun is_constr thy stds (x as (_, T)) =
1.305 is_constr_like thy x andalso
1.306 - not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
1.307 + not (is_basic_datatype thy stds
1.308 + (fst (dest_Type (unarize_type (body_type T))))) andalso
1.309 not (is_stale_constr thy x)
1.310 (* string -> bool *)
1.311 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
1.312 @@ -844,15 +855,16 @@
1.313 #> List.foldr (s_conj o swap) @{const True}
1.314
1.315 (* typ -> term *)
1.316 -fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
1.317 +fun zero_const T = Const (@{const_name zero_class.zero}, T)
1.318 fun suc_const T = Const (@{const_name Suc}, T --> T)
1.319
1.320 -(* theory -> typ -> styp list *)
1.321 -fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
1.322 +(* hol_context -> typ -> styp list *)
1.323 +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
1.324 + (T as Type (s, Ts)) =
1.325 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
1.326 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
1.327 | _ =>
1.328 - if is_datatype thy T then
1.329 + if is_datatype thy stds T then
1.330 case Datatype.get_info thy s of
1.331 SOME {index, descr, ...} =>
1.332 let
1.333 @@ -883,11 +895,11 @@
1.334 [])
1.335 | uncached_datatype_constrs _ _ = []
1.336 (* hol_context -> typ -> styp list *)
1.337 -fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
1.338 +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
1.339 case AList.lookup (op =) (!constr_cache) T of
1.340 SOME xs => xs
1.341 | NONE =>
1.342 - let val xs = uncached_datatype_constrs thy T in
1.343 + let val xs = uncached_datatype_constrs hol_ctxt T in
1.344 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
1.345 end
1.346 (* hol_context -> bool -> typ -> styp list *)
1.347 @@ -930,11 +942,11 @@
1.348 else betapply (discr_term_for_constr hol_ctxt x, t)
1.349 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
1.350
1.351 -(* styp -> term -> term *)
1.352 -fun nth_arg_sel_term_for_constr (x as (s, T)) n =
1.353 +(* theory -> (typ option * bool) list -> styp -> term -> term *)
1.354 +fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
1.355 let val (arg_Ts, dataT) = strip_type T in
1.356 - if dataT = nat_T then
1.357 - @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
1.358 + if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
1.359 + @{term "%n::nat. n - 1"}
1.360 else if is_pair_type dataT then
1.361 Const (nth_sel_for_constr x n)
1.362 else
1.363 @@ -952,24 +964,26 @@
1.364 (List.take (arg_Ts, n)) 0
1.365 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
1.366 end
1.367 -(* theory -> styp -> term -> int -> typ -> term *)
1.368 -fun select_nth_constr_arg thy x t n res_T =
1.369 - case strip_comb t of
1.370 - (Const x', args) =>
1.371 - if x = x' then nth args n
1.372 - else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
1.373 - else betapply (nth_arg_sel_term_for_constr x n, t)
1.374 - | _ => betapply (nth_arg_sel_term_for_constr x n, t)
1.375 +(* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
1.376 +fun select_nth_constr_arg thy stds x t n res_T =
1.377 + (case strip_comb t of
1.378 + (Const x', args) =>
1.379 + if x = x' then nth args n
1.380 + else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
1.381 + else raise SAME ()
1.382 + | _ => raise SAME())
1.383 + handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
1.384
1.385 -(* theory -> styp -> term list -> term *)
1.386 -fun construct_value _ x [] = Const x
1.387 - | construct_value thy (x as (s, _)) args =
1.388 +(* theory -> (typ option * bool) list -> styp -> term list -> term *)
1.389 +fun construct_value _ _ x [] = Const x
1.390 + | construct_value thy stds (x as (s, _)) args =
1.391 let val args = map Envir.eta_contract args in
1.392 case hd args of
1.393 Const (x' as (s', _)) $ t =>
1.394 if is_sel_like_and_no_discr s' andalso
1.395 constr_name_for_sel_like s' = s andalso
1.396 - forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
1.397 + forall (fn (n, t') =>
1.398 + select_nth_constr_arg thy stds x t n dummyT = t')
1.399 (index_seq 0 (length args) ~~ args) then
1.400 t
1.401 else
1.402 @@ -1167,24 +1181,31 @@
1.403 user_defs @ built_in_defs
1.404 in (defs, built_in_nondefs, user_nondefs) end
1.405
1.406 -(* bool -> styp -> int option *)
1.407 -fun arity_of_built_in_const fast_descrs (s, T) =
1.408 +(* theory -> (typ option * bool) list -> bool -> styp -> int option *)
1.409 +fun arity_of_built_in_const thy stds fast_descrs (s, T) =
1.410 if s = @{const_name If} then
1.411 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1.412 - else case AList.lookup (op =)
1.413 - (built_in_consts
1.414 - |> fast_descrs ? append built_in_descr_consts) s of
1.415 - SOME n => SOME n
1.416 - | NONE =>
1.417 - case AList.lookup (op =) built_in_typed_consts (s, T) of
1.418 - SOME n => SOME n
1.419 - | NONE =>
1.420 - if is_fun_type T andalso is_set_type (domain_type T) then
1.421 - AList.lookup (op =) built_in_set_consts s
1.422 - else
1.423 - NONE
1.424 -(* bool -> styp -> bool *)
1.425 -val is_built_in_const = is_some oo arity_of_built_in_const
1.426 + else
1.427 + let val std_nats = is_standard_datatype thy stds nat_T in
1.428 + case AList.lookup (op =)
1.429 + (built_in_consts
1.430 + |> std_nats ? append built_in_nat_consts
1.431 + |> fast_descrs ? append built_in_descr_consts) s of
1.432 + SOME n => SOME n
1.433 + | NONE =>
1.434 + case AList.lookup (op =)
1.435 + (built_in_typed_consts
1.436 + |> std_nats ? append built_in_typed_nat_consts)
1.437 + (s, unarize_type T) of
1.438 + SOME n => SOME n
1.439 + | NONE =>
1.440 + if is_fun_type T andalso is_set_type (domain_type T) then
1.441 + AList.lookup (op =) built_in_set_consts s
1.442 + else
1.443 + NONE
1.444 + end
1.445 +(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
1.446 +val is_built_in_const = is_some oooo arity_of_built_in_const
1.447
1.448 (* This function is designed to work for both real definition axioms and
1.449 simplification rules (equational specifications). *)
1.450 @@ -1202,9 +1223,10 @@
1.451 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1.452 traversal of the term, without which the wrong occurrence of a constant could
1.453 be matched in the face of overloading. *)
1.454 -(* theory -> bool -> const_table -> styp -> term list *)
1.455 -fun def_props_for_const thy fast_descrs table (x as (s, _)) =
1.456 - if is_built_in_const fast_descrs x then
1.457 +(* theory -> (typ option * bool) list -> bool -> const_table -> styp
1.458 + -> term list *)
1.459 +fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
1.460 + if is_built_in_const thy stds fast_descrs x then
1.461 []
1.462 else
1.463 these (Symtab.lookup table s)
1.464 @@ -1229,10 +1251,11 @@
1.465
1.466 (* theory -> const_table -> styp -> term option *)
1.467 fun def_of_const thy table (x as (s, _)) =
1.468 - if is_built_in_const false x orelse original_name s <> s then
1.469 + if is_built_in_const thy [(NONE, false)] false x orelse
1.470 + original_name s <> s then
1.471 NONE
1.472 else
1.473 - x |> def_props_for_const thy false table |> List.last
1.474 + x |> def_props_for_const thy [(NONE, false)] false table |> List.last
1.475 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
1.476 handle List.Empty => NONE
1.477
1.478 @@ -1282,10 +1305,10 @@
1.479 fun table_for get ctxt =
1.480 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1.481
1.482 -(* theory -> (string * int) list *)
1.483 -fun case_const_names thy =
1.484 +(* theory -> (typ option * bool) list -> (string * int) list *)
1.485 +fun case_const_names thy stds =
1.486 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1.487 - if is_basic_datatype dtype_s then
1.488 + if is_basic_datatype thy stds dtype_s then
1.489 I
1.490 else
1.491 cons (case_name, AList.lookup (op =) descr index
1.492 @@ -1366,7 +1389,7 @@
1.493 end
1.494 | NONE => []
1.495 end
1.496 -fun optimized_quot_type_axioms thy abs_z =
1.497 +fun optimized_quot_type_axioms thy stds abs_z =
1.498 let
1.499 val abs_T = Type abs_z
1.500 val rep_T = rep_type_for_quot_type thy abs_T
1.501 @@ -1375,7 +1398,7 @@
1.502 val x_var = Var (("x", 0), rep_T)
1.503 val y_var = Var (("y", 0), rep_T)
1.504 val x = (@{const_name Quot}, rep_T --> abs_T)
1.505 - val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
1.506 + val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
1.507 val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
1.508 val normal_x = normal_t $ x_var
1.509 val normal_y = normal_t $ y_var
1.510 @@ -1392,31 +1415,31 @@
1.511 $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
1.512 end
1.513
1.514 -(* theory -> int * styp -> term *)
1.515 -fun constr_case_body thy (j, (x as (_, T))) =
1.516 +(* theory -> (typ option * bool) list -> int * styp -> term *)
1.517 +fun constr_case_body thy stds (j, (x as (_, T))) =
1.518 let val arg_Ts = binder_types T in
1.519 - list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
1.520 + list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
1.521 (index_seq 0 (length arg_Ts)) arg_Ts)
1.522 end
1.523 (* hol_context -> typ -> int * styp -> term -> term *)
1.524 -fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
1.525 +fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
1.526 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
1.527 - $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
1.528 + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
1.529 $ res_t
1.530 (* hol_context -> typ -> typ -> term *)
1.531 -fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
1.532 +fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
1.533 let
1.534 val xs = datatype_constrs hol_ctxt dataT
1.535 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1.536 val (xs', x) = split_last xs
1.537 in
1.538 - constr_case_body thy (1, x)
1.539 + constr_case_body thy stds (1, x)
1.540 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
1.541 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1.542 end
1.543
1.544 (* hol_context -> string -> typ -> typ -> term -> term *)
1.545 -fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
1.546 +fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
1.547 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
1.548 case no_of_record_field thy s rec_T of
1.549 ~1 => (case rec_T of
1.550 @@ -1425,65 +1448,56 @@
1.551 val rec_T' = List.last Ts
1.552 val j = num_record_fields thy rec_T - 1
1.553 in
1.554 - select_nth_constr_arg thy constr_x t j res_T
1.555 + select_nth_constr_arg thy stds constr_x t j res_T
1.556 |> optimized_record_get hol_ctxt s rec_T' res_T
1.557 end
1.558 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1.559 []))
1.560 - | j => select_nth_constr_arg thy constr_x t j res_T
1.561 + | j => select_nth_constr_arg thy stds constr_x t j res_T
1.562 end
1.563 (* hol_context -> string -> typ -> term -> term -> term *)
1.564 -fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
1.565 +fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
1.566 let
1.567 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
1.568 val Ts = binder_types constr_T
1.569 val n = length Ts
1.570 val special_j = no_of_record_field thy s rec_T
1.571 - val ts = map2 (fn j => fn T =>
1.572 - let
1.573 - val t = select_nth_constr_arg thy constr_x rec_t j T
1.574 - in
1.575 - if j = special_j then
1.576 - betapply (fun_t, t)
1.577 - else if j = n - 1 andalso special_j = ~1 then
1.578 - optimized_record_update hol_ctxt s
1.579 - (rec_T |> dest_Type |> snd |> List.last) fun_t t
1.580 - else
1.581 - t
1.582 - end) (index_seq 0 n) Ts
1.583 + val ts =
1.584 + map2 (fn j => fn T =>
1.585 + let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
1.586 + if j = special_j then
1.587 + betapply (fun_t, t)
1.588 + else if j = n - 1 andalso special_j = ~1 then
1.589 + optimized_record_update hol_ctxt s
1.590 + (rec_T |> dest_Type |> snd |> List.last) fun_t t
1.591 + else
1.592 + t
1.593 + end) (index_seq 0 n) Ts
1.594 in list_comb (Const constr_x, ts) end
1.595
1.596 -(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
1.597 - constant, are said to be trivial. For those, we ignore the simplification
1.598 - rules and use the definition instead, to ensure that built-in symbols like
1.599 - "ord_nat_inst.less_eq_nat" are picked up correctly. *)
1.600 -(* theory -> const_table -> styp -> bool *)
1.601 -fun has_trivial_definition thy table x =
1.602 - case def_of_const thy table x of SOME (Const _) => true | _ => false
1.603 -
1.604 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1.605 fun fixpoint_kind_of_const thy table x =
1.606 - if is_built_in_const false x then
1.607 + if is_built_in_const thy [(NONE, false)] false x then
1.608 NoFp
1.609 else
1.610 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1.611 handle Option.Option => NoFp
1.612
1.613 (* hol_context -> styp -> bool *)
1.614 -fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
1.615 - : hol_context) x =
1.616 - not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
1.617 - fixpoint_kind_of_const thy def_table x <> NoFp
1.618 -fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
1.619 - : hol_context) x =
1.620 - exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
1.621 +fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
1.622 + ...} : hol_context) x =
1.623 + fixpoint_kind_of_const thy def_table x <> NoFp andalso
1.624 + not (null (def_props_for_const thy stds fast_descrs intro_table x))
1.625 +fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
1.626 + ...} : hol_context) x =
1.627 + exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
1.628 + x)))
1.629 [!simp_table, psimp_table]
1.630 fun is_inductive_pred hol_ctxt =
1.631 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
1.632 fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
1.633 (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
1.634 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1.635 - andf (not o has_trivial_definition thy def_table)
1.636
1.637 (* term * term -> term *)
1.638 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1.639 @@ -1522,7 +1536,7 @@
1.640 val unfold_max_depth = 255
1.641
1.642 (* hol_context -> term -> term *)
1.643 -fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
1.644 +fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
1.645 case_names, def_table, ground_thm_table,
1.646 ersatz_table, ...}) =
1.647 let
1.648 @@ -1537,8 +1551,11 @@
1.649 |> ran_T = nat_T ? Integer.max 0
1.650 val s = numeral_prefix ^ signed_string_of_int j
1.651 in
1.652 - if is_integer_type ran_T then
1.653 - Const (s, ran_T)
1.654 + if is_integer_like_type ran_T then
1.655 + if is_standard_datatype thy stds ran_T then
1.656 + Const (s, ran_T)
1.657 + else
1.658 + funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
1.659 else
1.660 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1.661 $ Const (s, int_T))
1.662 @@ -1577,9 +1594,9 @@
1.663 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1.664 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1.665 (Abs (Name.uu, body_type T,
1.666 - select_nth_constr_arg thy x (Bound 0) n res_T), [])
1.667 + select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
1.668 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1.669 - (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
1.670 + (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
1.671 (* int -> typ list -> term -> styp -> term list -> term *)
1.672 and do_const depth Ts t (x as (s, T)) ts =
1.673 case AList.lookup (op =) ersatz_table s of
1.674 @@ -1588,7 +1605,7 @@
1.675 | NONE =>
1.676 let
1.677 val (const, ts) =
1.678 - if is_built_in_const fast_descrs x then
1.679 + if is_built_in_const thy stds fast_descrs x then
1.680 (Const x, ts)
1.681 else case AList.lookup (op =) case_names s of
1.682 SOME n =>
1.683 @@ -1600,7 +1617,7 @@
1.684 |> do_term (depth + 1) Ts, ts)
1.685 end
1.686 | _ =>
1.687 - if is_constr thy x then
1.688 + if is_constr thy stds x then
1.689 (Const x, ts)
1.690 else if is_stale_constr thy x then
1.691 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
1.692 @@ -1635,7 +1652,7 @@
1.693 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1.694 else if is_rep_fun thy x then
1.695 let val x' = mate_of_rep_fun thy x in
1.696 - if is_constr thy x' then
1.697 + if is_constr thy stds x' then
1.698 select_nth_constr_arg_with_args depth Ts x' ts 0
1.699 (range_type T)
1.700 else
1.701 @@ -1659,7 +1676,7 @@
1.702 in do_term 0 [] end
1.703
1.704 (* hol_context -> typ -> term list *)
1.705 -fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
1.706 +fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
1.707 let
1.708 val xs = datatype_constrs hol_ctxt T
1.709 val set_T = T --> bool_T
1.710 @@ -1677,8 +1694,8 @@
1.711 fun nth_sub_bisim x n nth_T =
1.712 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1.713 else HOLogic.eq_const nth_T)
1.714 - $ select_nth_constr_arg thy x x_var n nth_T
1.715 - $ select_nth_constr_arg thy x y_var n nth_T
1.716 + $ select_nth_constr_arg thy stds x x_var n nth_T
1.717 + $ select_nth_constr_arg thy stds x y_var n nth_T
1.718 (* styp -> term *)
1.719 fun case_func (x as (_, T)) =
1.720 let
1.721 @@ -1695,7 +1712,7 @@
1.722 map case_func xs @ [x_var]))),
1.723 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1.724 $ (Const (@{const_name insert}, T --> set_T --> set_T)
1.725 - $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
1.726 + $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
1.727 |> map HOLogic.mk_Trueprop
1.728 end
1.729
1.730 @@ -1753,9 +1770,9 @@
1.731
1.732 (* hol_context -> const_table -> styp -> bool *)
1.733 fun uncached_is_well_founded_inductive_pred
1.734 - ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
1.735 + ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
1.736 : hol_context) (x as (_, T)) =
1.737 - case def_props_for_const thy fast_descrs intro_table x of
1.738 + case def_props_for_const thy stds fast_descrs intro_table x of
1.739 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1.740 [Const x])
1.741 | intro_ts =>
1.742 @@ -1999,10 +2016,10 @@
1.743 raw_inductive_pred_axiom hol_ctxt x
1.744
1.745 (* hol_context -> styp -> term list *)
1.746 -fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
1.747 +fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
1.748 psimp_table, ...}) (x as (s, _)) =
1.749 - case def_props_for_const thy fast_descrs (!simp_table) x of
1.750 - [] => (case def_props_for_const thy fast_descrs psimp_table x of
1.751 + case def_props_for_const thy stds fast_descrs (!simp_table) x of
1.752 + [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
1.753 [] => [inductive_pred_axiom hol_ctxt x]
1.754 | psimps => psimps)
1.755 | simps => simps