# HG changeset patch
# User blanchet
# Date 1268245319 -3600
# Node ID 9ed327529a441e28406fac2656775b19e5f7cb4b
# Parent  c362465085c5ed6840e4df6b7669e9c0c3a111c6
improve precision of "card" in Nitpick

diff -r c362465085c5 -r 9ed327529a44 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Nitpick.thy	Wed Mar 10 19:21:59 2010 +0100
@@ -96,10 +96,10 @@
                 else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
 
 definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
-"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
+"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
 
 definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
-"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
 
 inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "fold_graph' f z {} z" |
diff -r c362465085c5 -r 9ed327529a44 src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Mar 10 19:21:59 2010 +0100
@@ -24,8 +24,6 @@
 fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
 *}
 
-ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
-
 ML {* genuine 1 @{prop "x = Not"} *}
 ML {* none 1 @{prop "\<exists>x. x = Not"} *}
 ML {* none 1 @{prop "\<not> False"} *}
diff -r c362465085c5 -r 9ed327529a44 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Mar 10 19:21:59 2010 +0100
@@ -336,7 +336,8 @@
     val max_solutions = 1
   in
     case solve_any_problem overlord NONE max_threads max_solutions problems of
-      NotInstalled => "unknown"
+      JavaNotInstalled => "unknown"
+    | KodkodiNotInstalled => "unknown"
     | Normal ([], _, _) => "none"
     | Normal _ => "genuine"
     | TimedOut _ => "unknown"