# HG changeset patch
# User blanchet
# Date 1325675393 -3600
# Node ID ecab67f5a5c2e6ef08de4e7a991612dc0ecdc254
# Parent  e6d33b200f42055add4c330695de402c489a0434
improved "set" support by code inspection

diff -r e6d33b200f42 -r ecab67f5a5c2 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -87,6 +87,8 @@
   val frac_from_term_pair : typ -> term -> term -> term
   val is_TFree : typ -> bool
   val is_fun_type : typ -> bool
+  val is_set_type : typ -> bool
+  val is_fun_or_set_type : typ -> bool
   val is_set_like_type : typ -> bool
   val is_pair_type : typ -> bool
   val is_lfp_iterator_type : typ -> bool
@@ -482,7 +484,11 @@
   | is_TFree _ = false
 fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
-fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
+fun is_set_type (Type (@{type_name set}, _)) = true
+  | is_set_type _ = false
+val is_fun_or_set_type = is_fun_type orf is_set_type
+fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
+    (body_type T' = bool_T)
   | is_set_like_type (Type (@{type_name set}, _)) = true
   | is_set_like_type _ = false
 fun is_pair_type (Type (@{type_name prod}, _)) = true
@@ -506,6 +512,7 @@
   | is_frac_type _ _ = false
 fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
 fun is_higher_order_type (Type (@{type_name fun}, _)) = true
+  | is_higher_order_type (Type (@{type_name set}, _)) = true
   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   | is_higher_order_type _ = false
 
@@ -1816,7 +1823,7 @@
 (** Axiom extraction/generation **)
 
 fun extensional_equal j T t1 t2 =
-  if is_fun_type T orelse is_set_like_type T then
+  if is_fun_or_set_type T then
     let
       val dom_T = pseudo_domain_type T
       val ran_T = pseudo_range_type T
@@ -2233,7 +2240,7 @@
   end
 
 fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
-    forall (not o (is_fun_type orf is_pair_type)) Ts
+    forall (not o (is_fun_or_set_type orf is_pair_type)) Ts
   | is_good_starred_linear_pred_type _ = false
 
 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
diff -r e6d33b200f42 -r ecab67f5a5c2 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -682,7 +682,8 @@
     val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
     val R' = if n = ~1 orelse is_word_type (body_type T) orelse
                 (is_fun_type (range_type T') andalso
-                 is_boolean_type (body_type T')) then
+                 is_boolean_type (body_type T')) orelse
+                (is_set_type (body_type T')) then
                best_non_opt_set_rep_for_type scope T'
              else
                best_opt_set_rep_for_type scope T' |> unopt_rep
@@ -718,7 +719,8 @@
    is representable or "Unrep", because unknown implies "Unrep". *)
 fun is_constructive u =
   is_Cst Unrep u orelse
-  (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
+  (not (is_fun_or_set_type (type_of u)) andalso
+   not (is_opt_rep (rep_of u))) orelse
   case u of
     Cst (Num _, _, _) => true
   | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
@@ -807,8 +809,9 @@
     fun triad_fn f = triad (f Pos) (f Neg)
     fun unrepify_nut_in_nut table def polar needle_u =
       let val needle_T = type_of needle_u in
-        substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown
-                                         else Unrep, needle_T, Any))
+        substitute_in_nut needle_u
+            (Cst (if is_fun_or_set_type needle_T then Unknown
+                  else Unrep, needle_T, Any))
         #> aux table def polar
       end
     and aux table def polar u =
diff -r e6d33b200f42 -r ecab67f5a5c2 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -301,7 +301,7 @@
 fun has_heavy_bounds_or_vars Ts t =
   let
     fun aux [] = false
-      | aux [T] = is_fun_type T orelse is_pair_type T
+      | aux [T] = is_fun_or_set_type T orelse is_pair_type T
       | aux _ = true
   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
 
@@ -311,7 +311,7 @@
     case t of
       Const x =>
       if not relax andalso is_constr ctxt stds x andalso
-         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+         not (is_fun_or_set_type (fastype_of1 (Ts, t_comb))) andalso
          has_heavy_bounds_or_vars Ts t_comb andalso
          not (loose_bvar (t_comb, level)) then
         let
@@ -1009,6 +1009,7 @@
       case T of
         Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
       | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
+      | Type (@{type_name set}, Ts) => fold (add_axioms_for_type depth) Ts
       | @{typ prop} => I
       | @{typ bool} => I
       | TFree (_, S) => add_axioms_for_sort depth T S