src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46083 efeaa79f021b
parent 46081 8f6465f7021b
child 46086 096697aec8a7
     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 @@ -102,6 +102,8 @@
     1.4    val is_number_type : Proof.context -> typ -> bool
     1.5    val is_higher_order_type : typ -> bool
     1.6    val elem_type : typ -> typ
     1.7 +  val pseudo_domain_type : typ -> typ
     1.8 +  val pseudo_range_type : typ -> typ
     1.9    val const_for_iterator_type : typ -> styp
    1.10    val strip_n_binders : int -> typ -> typ list * typ
    1.11    val nth_range_type : int -> typ -> typ
    1.12 @@ -382,6 +384,8 @@
    1.13     (@{const_name Pair}, 2),
    1.14     (@{const_name fst}, 1),
    1.15     (@{const_name snd}, 1),
    1.16 +   (@{const_name Set.member}, 2),
    1.17 +   (@{const_name Collect}, 1),
    1.18     (@{const_name Id}, 0),
    1.19     (@{const_name converse}, 1),
    1.20     (@{const_name trancl}, 1),
    1.21 @@ -505,8 +509,13 @@
    1.22    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.23    | is_higher_order_type _ = false
    1.24  
    1.25 -fun elem_type (Type (@{type_name set}, [T])) = T
    1.26 +fun elem_type (Type (@{type_name set}, [T'])) = T'
    1.27    | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
    1.28 +fun pseudo_domain_type (Type (@{type_name fun}, [T1, _])) = T1
    1.29 +  | pseudo_domain_type T = elem_type T
    1.30 +fun pseudo_range_type (Type (@{type_name fun}, [_, T2])) = T2
    1.31 +  | pseudo_range_type (Type (@{type_name set}, _)) = bool_T
    1.32 +  | pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], [])
    1.33  
    1.34  fun iterator_type_for_const gfp (s, T) =
    1.35    Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
    1.36 @@ -575,8 +584,8 @@
    1.37  (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
    1.38     e.g., by adding a field to "Datatype_Aux.info". *)
    1.39  fun is_basic_datatype thy stds s =
    1.40 -  member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int},
    1.41 -                 "Code_Numeral.code_numeral"] s orelse
    1.42 +  member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
    1.43 +                 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
    1.44    (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
    1.45  
    1.46  fun repair_constr_type ctxt body_T' T =
    1.47 @@ -959,6 +968,8 @@
    1.48      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
    1.49    | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
    1.50      card_of_type assigns T1 * card_of_type assigns T2
    1.51 +  | card_of_type assigns (Type (@{type_name set}, [T'])) =
    1.52 +    reasonable_power 2 (card_of_type assigns T')
    1.53    | card_of_type _ (Type (@{type_name itself}, _)) = 1
    1.54    | card_of_type _ @{typ prop} = 2
    1.55    | card_of_type _ @{typ bool} = 2
    1.56 @@ -983,6 +994,9 @@
    1.57        val k1 = bounded_card_of_type max default_card assigns T1
    1.58        val k2 = bounded_card_of_type max default_card assigns T2
    1.59      in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
    1.60 +  | bounded_card_of_type max default_card assigns
    1.61 +                         (Type (@{type_name set}, [T'])) =
    1.62 +    bounded_card_of_type max default_card assigns (T' --> bool_T)
    1.63    | bounded_card_of_type max default_card assigns T =
    1.64      Int.min (max, if default_card = ~1 then
    1.65                      card_of_type assigns T
    1.66 @@ -1016,6 +1030,7 @@
    1.67            | (k1, k2) =>
    1.68              if k1 >= max orelse k2 >= max then max
    1.69              else Int.min (max, k1 * k2))
    1.70 +       | Type (@{type_name set}, [T']) => aux avoid (T' --> bool_T)
    1.71         | Type (@{type_name itself}, _) => 1
    1.72         | @{typ prop} => 2
    1.73         | @{typ bool} => 2
    1.74 @@ -1256,7 +1271,7 @@
    1.75  
    1.76  (* FIXME: detect "rep_datatype"? *)
    1.77  fun is_funky_typedef_name ctxt s =
    1.78 -  member (op =) [@{type_name unit}, @{type_name prod},
    1.79 +  member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
    1.80                   @{type_name Sum_Type.sum}, @{type_name int}] s orelse
    1.81    is_frac_type ctxt (Type (s, []))
    1.82  fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
    1.83 @@ -2311,6 +2326,7 @@
    1.84        case T of
    1.85          Type (@{type_name fun}, Ts) => fold aux Ts accum
    1.86        | Type (@{type_name prod}, Ts) => fold aux Ts accum
    1.87 +      | Type (@{type_name set}, Ts) => fold aux Ts accum
    1.88        | Type (@{type_name itself}, [T1]) => aux T1 accum
    1.89        | Type (_, Ts) =>
    1.90          if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
    1.91 @@ -2323,7 +2339,6 @@
    1.92                         | xs => map snd xs)
    1.93        | _ => insert (op =) T accum
    1.94    in aux end
    1.95 -
    1.96  fun ground_types_in_type hol_ctxt binarize T =
    1.97    add_ground_types hol_ctxt binarize T []
    1.98  fun ground_types_in_terms hol_ctxt binarize ts =