# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 91495051c2ec0d44cbae42bbb92209fcee852912
# Parent  298226ba5606dd60342b882d3a1235ecc2942a3c
improve precision of finite functions in monotonicity calculus

diff -r 298226ba5606 -r 91495051c2ec src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -229,6 +229,8 @@
   | is_fin_fun_supported_type @{typ bool} = true
   | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
   | is_fin_fun_supported_type _ = false
+
+(* TODO: clean this up *)
 fun fin_fun_body _ _ (t as @{term False}) = SOME t
   | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
   | fin_fun_body dom_T ran_T
@@ -307,14 +309,23 @@
       | _ => MType (simple_string_of_typ T, [])
   in do_type end
 
+val ground_and_sole_base_constrs = [@{const_name Nil}, @{const_name None}]
+
 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   | prodM_factors M = [M]
 fun curried_strip_mtype (MFun (M1, _, M2)) =
     curried_strip_mtype M2 |>> append (prodM_factors M1)
   | curried_strip_mtype M = ([], M)
 fun sel_mtype_from_constr_mtype s M =
-  let val (arg_Ms, dataM) = curried_strip_mtype M in
-    MFun (dataM, A Gen,
+  let
+    val (arg_Ms, dataM) = curried_strip_mtype M
+    val a = if member (op =) ground_and_sole_base_constrs
+                             (constr_name_for_sel_like s) then
+              Fls
+            else
+              Gen
+  in
+    MFun (dataM, A a,
           case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
   end
 
@@ -837,6 +848,8 @@
        case t of
          @{const False} =>
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
+       | Const (@{const_name None}, _) =>
+         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
        | @{const True} =>
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
        | Const (x as (s, T)) =>