src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46081 8f6465f7021b
parent 45980 af59825c40cf
child 46083 efeaa79f021b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
     1.3 @@ -87,7 +87,7 @@
     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_set_like_type : typ -> bool
     1.9    val is_pair_type : typ -> bool
    1.10    val is_lfp_iterator_type : typ -> bool
    1.11    val is_gfp_iterator_type : typ -> bool
    1.12 @@ -101,6 +101,7 @@
    1.13    val is_record_type : typ -> bool
    1.14    val is_number_type : Proof.context -> typ -> bool
    1.15    val is_higher_order_type : typ -> bool
    1.16 +  val elem_type : typ -> typ
    1.17    val const_for_iterator_type : typ -> styp
    1.18    val strip_n_binders : int -> typ -> typ list * typ
    1.19    val nth_range_type : int -> typ -> typ
    1.20 @@ -416,7 +417,7 @@
    1.21     ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
    1.22     ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
    1.23     ((@{const_name of_nat}, nat_T --> int_T), 0)]
    1.24 -val built_in_set_consts =
    1.25 +val built_in_set_like_consts =
    1.26    [(@{const_name ord_class.less_eq}, 2)]
    1.27  
    1.28  fun unarize_type @{typ "unsigned_bit word"} = nat_T
    1.29 @@ -477,8 +478,9 @@
    1.30    | is_TFree _ = false
    1.31  fun is_fun_type (Type (@{type_name fun}, _)) = true
    1.32    | is_fun_type _ = false
    1.33 -fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    1.34 -  | is_set_type _ = false
    1.35 +fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    1.36 +  | is_set_like_type (Type (@{type_name set}, _)) = true
    1.37 +  | is_set_like_type _ = false
    1.38  fun is_pair_type (Type (@{type_name prod}, _)) = true
    1.39    | is_pair_type _ = false
    1.40  fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
    1.41 @@ -503,6 +505,9 @@
    1.42    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.43    | is_higher_order_type _ = false
    1.44  
    1.45 +fun elem_type (Type (@{type_name set}, [T])) = T
    1.46 +  | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
    1.47 +
    1.48  fun iterator_type_for_const gfp (s, T) =
    1.49    Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
    1.50          binder_types T)
    1.51 @@ -1314,8 +1319,8 @@
    1.52              if is_iterator_type T then SOME 0 else NONE
    1.53            | @{const_name Suc} =>
    1.54              if is_iterator_type (domain_type T) then SOME 0 else NONE
    1.55 -          | _ => if is_fun_type T andalso is_set_type (domain_type T) then
    1.56 -                   AList.lookup (op =) built_in_set_consts s
    1.57 +          | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
    1.58 +                   AList.lookup (op =) built_in_set_like_consts s
    1.59                   else
    1.60                     NONE
    1.61      end