# HG changeset patch
# User blanchet
# Date 1268149231 -3600
# Node ID ff484d4f2e14a3c7cda1c128418c73ecbca36bc4
# Parent  ed2c3830d8817205f7150c38f58c178f2930ff7e
more work on Nitpick's finite sets

diff -r ed2c3830d881 -r ff484d4f2e14 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 14:18:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 16:40:31 2010 +0100
@@ -264,20 +264,22 @@
                 $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
   | fin_fun_body _ _ _ = NONE
 
-(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
-fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
+(* mdata -> bool -> typ -> typ -> mtyp * sign_atom * mtyp *)
+fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
+                            T1 T2 =
   let
-    val M1 = fresh_mtype_for_type mdata T1
-    val M2 = fresh_mtype_for_type mdata T2
-    val a = if is_fin_fun_supported_type (body_type T2) andalso
-               exists_alpha_sub_mtype_fresh M1 then
+    val M1 = fresh_mtype_for_type mdata all_minus T1
+    val M2 = fresh_mtype_for_type mdata all_minus T2
+    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
+               is_fin_fun_supported_type (body_type T2) then
               V (Unsynchronized.inc max_fresh)
             else
               S Minus
   in (M1, a, M2) end
-(* mdata -> typ -> mtyp *)
+(* mdata -> bool -> typ -> mtyp *)
 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
-                                    datatype_mcache, constr_mcache, ...}) =
+                                    datatype_mcache, constr_mcache, ...})
+                         all_minus =
   let
     (* typ -> mtyp *)
     fun do_type T =
@@ -285,7 +287,7 @@
         MAlpha
       else case T of
         Type (@{type_name fun}, [T1, T2]) =>
-        MFun (fresh_mfun_for_fun_type mdata T1 T2)
+        MFun (fresh_mfun_for_fun_type mdata false T1 T2)
       | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
       | Type (z as (s, _)) =>
         if could_exist_alpha_sub_mtype thy alpha_T T then
@@ -347,14 +349,14 @@
     case AList.lookup (op =) (!constr_mcache) x of
       SOME M => M
     | NONE => if T = alpha_T then
-                let val M = fresh_mtype_for_type mdata T in
+                let val M = fresh_mtype_for_type mdata false T in
                   (Unsynchronized.change constr_mcache (cons (x, M)); M)
                 end
               else
-                (fresh_mtype_for_type mdata (body_type T);
+                (fresh_mtype_for_type mdata false (body_type T);
                  AList.lookup (op =) (!constr_mcache) x |> the)
   else
-    fresh_mtype_for_type mdata T
+    fresh_mtype_for_type mdata false T
 fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
     |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
@@ -629,7 +631,7 @@
                              alpha_T, max_fresh, ...}) =
   let
     (* typ -> mtyp *)
-    val mtype_for = fresh_mtype_for_type mdata
+    val mtype_for = fresh_mtype_for_type mdata false
     (* mtyp -> mtyp *)
     fun plus_set_mtype_for_dom M =
       MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
@@ -765,12 +767,6 @@
                   val ba_set_M = range_type T |> mtype_for_set
                 in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
               | @{const_name trancl} => do_fragile_set_operation T accum
-              | @{const_name rtrancl} =>
-                (print_g "*** rtrancl"; mtype_unsolvable)
-              | @{const_name finite} =>
-                let val M1 = mtype_for (domain_type (domain_type T)) in
-                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
-                end
               | @{const_name rel_comp} =>
                 let
                   val x = Unsynchronized.inc max_fresh
@@ -793,6 +789,10 @@
                          MFun (plus_set_mtype_for_dom a_M, S Minus,
                                plus_set_mtype_for_dom b_M)), accum)
                 end
+              | @{const_name finite} =>
+                let val M1 = mtype_for (domain_type (domain_type T)) in
+                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
+                end
               | @{const_name Sigma} =>
                 let
                   val x = Unsynchronized.inc max_fresh
@@ -840,13 +840,8 @@
                   (mtype_for_sel mdata x, accum)
                 else if is_constr thy stds x then
                   (mtype_for_constr mdata x, accum)
-                else if is_built_in_const thy stds fast_descrs x andalso
-                        s <> @{const_name is_unknown} andalso
-                        s <> @{const_name unknown} then
-                  (* the "unknown" part is a hack *)
-                  case def_of_const thy def_table x of
-                    SOME t' => do_term t' accum |>> mtype_of_mterm
-                  | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
+                else if is_built_in_const thy stds fast_descrs x then
+                  (fresh_mtype_for_type mdata true T, accum)
                 else
                   let val M = mtype_for T in
                     (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
@@ -934,7 +929,7 @@
     val M1 = mtype_of_mterm m1
     val M2 = mtype_of_mterm m2
     val accum = accum ||> add_mtypes_equal M1 M2
-    val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
     val m = MApp (MApp (MRaw (Const x,
                 MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
   in
@@ -950,7 +945,7 @@
 fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
   let
     (* typ -> mtyp *)
-    val mtype_for = fresh_mtype_for_type mdata
+    val mtype_for = fresh_mtype_for_type mdata false
     (* term -> accumulator -> mterm * accumulator *)
     val do_term = consider_term mdata
     (* sign -> term -> accumulator -> mterm * accumulator *)
@@ -1057,7 +1052,7 @@
   else
     let
       (* typ -> mtyp *)
-      val mtype_for = fresh_mtype_for_type mdata
+      val mtype_for = fresh_mtype_for_type mdata false
       (* term -> accumulator -> mterm * accumulator *)
       val do_term = consider_term mdata
       (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
@@ -1203,11 +1198,23 @@
             val T' = type_from_mtype T M
           in
             case t of
-              Const (x as (s, T)) =>
-              if s = @{const_name finite} then
+              Const (x as (s, _)) =>
+              if s = @{const_name insert} then
+                case nth_range_type 2 T' of
+                  set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
+                    Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
+                        Const (@{const_name If},
+                               bool_T --> set_T' --> set_T' --> set_T')
+                        $ (Const (@{const_name is_unknown}, elem_T' --> bool_T)
+                           $ Bound 1)
+                        $ (Const (@{const_name unknown}, set_T'))
+                        $ (coerce_term hol_ctxt Ts T' T (Const x)
+                           $ Bound 1 $ Bound 0)))
+                | _ => Const (s, T')
+              else if s = @{const_name finite} then
                 case domain_type T' of
-                  T1' as Type (@{type_name fin_fun}, _) =>
-                  Abs (Name.uu, T1', @{const True})
+                  set_T' as Type (@{type_name fin_fun}, _) =>
+                  Abs (Name.uu, set_T', @{const True})
                 | _ => Const (s, T')
               else if s = @{const_name "=="} orelse
                       s = @{const_name "op ="} then
@@ -1232,16 +1239,6 @@
             | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
                                 [m])
           end
-        | MAbs (s, T, M, a, m') =>
-          let
-            val T = type_from_mtype T M
-            val t' = term_from_mterm (T :: Ts) m'
-            val T' = fastype_of1 (T :: Ts, t')
-          in
-            Abs (s, T, t')
-            |> should_finitize (T --> T') a
-               ? construct_value thy stds (fin_fun_constr T T') o single
-          end
         | MApp (m1, m2) =>
           let
             val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
@@ -1257,6 +1254,16 @@
               | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
                                  [T1], [])
           in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
+        | MAbs (s, T, M, a, m') =>
+          let
+            val T = type_from_mtype T M
+            val t' = term_from_mterm (T :: Ts) m'
+            val T' = fastype_of1 (T :: Ts, t')
+          in
+            Abs (s, T, t')
+            |> should_finitize (T --> T') a
+               ? construct_value thy stds (fin_fun_constr T T') o single
+          end
     in
       Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
       pairself (map (term_from_mterm [])) msp
diff -r ed2c3830d881 -r ff484d4f2e14 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 14:18:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 16:40:31 2010 +0100
@@ -1342,6 +1342,8 @@
   let
     val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
              |> filter_out (fn Type (@{type_name fun_box}, _) => true
+                             | @{typ signed_bit} => true
+                             | @{typ unsigned_bit} => true
                              | T => is_small_finite_type hol_ctxt T orelse
                                     triple_lookup (type_match thy) monos T
                                     = SOME (SOME false))