src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46115 ecab67f5a5c2
parent 46113 dd112cd72c48
child 46217 7b19666f0e3d
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.3 @@ -87,6 +87,8 @@
     1.4    val frac_from_term_pair : typ -> term -> term -> term
     1.5    val is_TFree : typ -> bool
     1.6    val is_fun_type : typ -> bool
     1.7 +  val is_set_type : typ -> bool
     1.8 +  val is_fun_or_set_type : typ -> bool
     1.9    val is_set_like_type : typ -> bool
    1.10    val is_pair_type : typ -> bool
    1.11    val is_lfp_iterator_type : typ -> bool
    1.12 @@ -482,7 +484,11 @@
    1.13    | is_TFree _ = false
    1.14  fun is_fun_type (Type (@{type_name fun}, _)) = true
    1.15    | is_fun_type _ = false
    1.16 -fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    1.17 +fun is_set_type (Type (@{type_name set}, _)) = true
    1.18 +  | is_set_type _ = false
    1.19 +val is_fun_or_set_type = is_fun_type orf is_set_type
    1.20 +fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
    1.21 +    (body_type T' = bool_T)
    1.22    | is_set_like_type (Type (@{type_name set}, _)) = true
    1.23    | is_set_like_type _ = false
    1.24  fun is_pair_type (Type (@{type_name prod}, _)) = true
    1.25 @@ -506,6 +512,7 @@
    1.26    | is_frac_type _ _ = false
    1.27  fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
    1.28  fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    1.29 +  | is_higher_order_type (Type (@{type_name set}, _)) = true
    1.30    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.31    | is_higher_order_type _ = false
    1.32  
    1.33 @@ -1816,7 +1823,7 @@
    1.34  (** Axiom extraction/generation **)
    1.35  
    1.36  fun extensional_equal j T t1 t2 =
    1.37 -  if is_fun_type T orelse is_set_like_type T then
    1.38 +  if is_fun_or_set_type T then
    1.39      let
    1.40        val dom_T = pseudo_domain_type T
    1.41        val ran_T = pseudo_range_type T
    1.42 @@ -2233,7 +2240,7 @@
    1.43    end
    1.44  
    1.45  fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
    1.46 -    forall (not o (is_fun_type orf is_pair_type)) Ts
    1.47 +    forall (not o (is_fun_or_set_type orf is_pair_type)) Ts
    1.48    | is_good_starred_linear_pred_type _ = false
    1.49  
    1.50  fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,