# HG changeset patch
# User blanchet
# Date 1325611997 -3600
# Node ID 8f6465f7021b56224f0417c297cebc811260de18
# Parent  b58591c75f0dd0f3e33ef7fd89dd4795141d2ed7
ported mono calculus to handle "set" type constructors

diff -r b58591c75f0d -r 8f6465f7021b src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -87,7 +87,7 @@
   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_set_like_type : typ -> bool
   val is_pair_type : typ -> bool
   val is_lfp_iterator_type : typ -> bool
   val is_gfp_iterator_type : typ -> bool
@@ -101,6 +101,7 @@
   val is_record_type : typ -> bool
   val is_number_type : Proof.context -> typ -> bool
   val is_higher_order_type : typ -> bool
+  val elem_type : typ -> typ
   val const_for_iterator_type : typ -> styp
   val strip_n_binders : int -> typ -> typ list * typ
   val nth_range_type : int -> typ -> typ
@@ -416,7 +417,7 @@
    ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
    ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
    ((@{const_name of_nat}, nat_T --> int_T), 0)]
-val built_in_set_consts =
+val built_in_set_like_consts =
   [(@{const_name ord_class.less_eq}, 2)]
 
 fun unarize_type @{typ "unsigned_bit word"} = nat_T
@@ -477,8 +478,9 @@
   | is_TFree _ = false
 fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
-fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
-  | is_set_type _ = false
+fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
+  | is_set_like_type (Type (@{type_name set}, _)) = true
+  | is_set_like_type _ = false
 fun is_pair_type (Type (@{type_name prod}, _)) = true
   | is_pair_type _ = false
 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
@@ -503,6 +505,9 @@
   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   | is_higher_order_type _ = false
 
+fun elem_type (Type (@{type_name set}, [T])) = T
+  | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
+
 fun iterator_type_for_const gfp (s, T) =
   Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
         binder_types T)
@@ -1314,8 +1319,8 @@
             if is_iterator_type T then SOME 0 else NONE
           | @{const_name Suc} =>
             if is_iterator_type (domain_type T) then SOME 0 else NONE
-          | _ => if is_fun_type T andalso is_set_type (domain_type T) then
-                   AList.lookup (op =) built_in_set_consts s
+          | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
+                   AList.lookup (op =) built_in_set_like_consts s
                  else
                    NONE
     end
diff -r b58591c75f0d -r 8f6465f7021b src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -224,6 +224,7 @@
         Type (@{type_name fun}, [T1, T2]) =>
         MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
       | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
+      | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
       | Type (z as (s, _)) =>
         if could_exist_alpha_sub_mtype ctxt alpha_T T then
           case AList.lookup (op =) (!datatype_mcache) z of
@@ -474,15 +475,18 @@
 
 fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
 fun prop_for_bool_var_equality (v1, v2) =
-  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
-           Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2))
+  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1,
+                                   Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
+                   Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1),
+                                   Prop_Logic.BoolVar v2))
 fun prop_for_assign (x, a) =
   let val (b1, b2) = bools_from_annotation a in
     Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
-             Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
+                     Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
   end
 fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
-  | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a))
+  | prop_for_assign_literal (x, (Minus, a)) =
+    Prop_Logic.SNot (prop_for_assign (x, a))
 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
   | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
@@ -499,7 +503,8 @@
   | prop_for_comp (aa1, aa2, Neq, []) =
     Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, []))
   | prop_for_comp (aa1, aa2, Leq, []) =
-    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
+    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2),
+                    prop_for_atom_assign (aa2, Gen))
   | prop_for_comp (aa1, aa2, cmp, xs) =
     Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen,
             prop_for_comp (aa1, aa2, cmp, []))
@@ -540,7 +545,8 @@
       SOME (extract_assigns max_var assigns asgs |> tap print_solution)
     val _ = print_problem comps clauses
     val prop =
-      Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
+      Prop_Logic.all (map prop_for_comp comps @
+                      map prop_for_assign_clause clauses)
   in
     if Prop_Logic.eval (K false) prop then
       do_assigns (K (SOME false))
@@ -739,6 +745,7 @@
         <= length ts
       | _ => true
     val mtype_for = fresh_mtype_for_type mdata false
+    fun mtype_for_set x T = MFun (mtype_for (elem_type T), V x, bool_M)
     fun do_all T (gamma, cset) =
       let
         val abs_M = mtype_for (domain_type (domain_type T))
@@ -774,6 +781,8 @@
         fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
             if T = set_T then set_M
             else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2)
+          | custom_mtype_for (Type (@{type_name set}, [T'])) =
+            custom_mtype_for (T' --> bool_T)
           | custom_mtype_for T = mtype_for T
       in
         (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete [] set_M))
@@ -840,10 +849,8 @@
             | @{const_name converse} =>
               let
                 val x = Unsynchronized.inc max_fresh
-                fun mtype_for_set T =
-                  MFun (mtype_for (domain_type T), V x, bool_M)
-                val ab_set_M = domain_type T |> mtype_for_set
-                val ba_set_M = range_type T |> mtype_for_set
+                val ab_set_M = domain_type T |> mtype_for_set x
+                val ba_set_M = range_type T |> mtype_for_set x
               in
                 (MFun (ab_set_M, A Gen, ba_set_M),
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
@@ -852,29 +859,25 @@
             | @{const_name rel_comp} =>
               let
                 val x = Unsynchronized.inc max_fresh
-                fun mtype_for_set T =
-                  MFun (mtype_for (domain_type T), V x, bool_M)
-                val bc_set_M = domain_type T |> mtype_for_set
-                val ab_set_M = domain_type (range_type T) |> mtype_for_set
-                val ac_set_M = nth_range_type 2 T |> mtype_for_set
+                val bc_set_M = domain_type T |> mtype_for_set x
+                val ab_set_M = domain_type (range_type T) |> mtype_for_set x
+                val ac_set_M = nth_range_type 2 T |> mtype_for_set x
               in
                 (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | @{const_name finite} =>
               let
-                val M1 = mtype_for (domain_type (domain_type T))
+                val M1 = mtype_for (elem_type (domain_type T))
                 val a = if exists_alpha_sub_mtype M1 then Fls else Gen
               in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
             | @{const_name prod} =>
               let
                 val x = Unsynchronized.inc max_fresh
-                fun mtype_for_set T =
-                  MFun (mtype_for (domain_type T), V x, bool_M)
-                val a_set_M = mtype_for_set (domain_type T)
+                val a_set_M = domain_type T |> mtype_for_set x
                 val b_set_M =
-                  mtype_for_set (range_type (domain_type (range_type T)))
-                val ab_set_M = mtype_for_set (nth_range_type 2 T)
+                  range_type (domain_type (range_type T)) |> mtype_for_set x
+                val ab_set_M = nth_range_type 2 T |> mtype_for_set x
               in
                 (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
@@ -886,7 +889,7 @@
                   val a_M = dest_MFun a_set_M |> #1
                 in (MFun (a_set_M, A Gen, a_M), accum) end
               else if s = @{const_name ord_class.less_eq} andalso
-                      is_set_type (domain_type T) then
+                      is_set_like_type (domain_type T) then
                 do_fragile_set_operation T accum
               else if is_sel s then
                 (mtype_for_sel mdata x, accum)