# 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 \ bool) \ nat" where -"card' X \ length (SOME xs. set xs = X \ distinct xs)" +"card' A \ if finite A then length (safe_Eps (\xs. set xs = A \ distinct xs)) else 0" definition setsum' :: "('a \ 'b\comm_monoid_add) \ ('a \ bool) \ 'b" where -"setsum' f A \ if finite A then listsum (map f (SOME xs. set xs = A \ distinct xs)) else 0" +"setsum' f A \ if finite A then listsum (map f (safe_Eps (\xs. set xs = A \ distinct xs))) else 0" inductive fold_graph' :: "('a \ 'b \ 'b) \ 'b \ ('a \ bool) \ 'b \ 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 "\x\'a. \y\'b. f x = y"} *} - ML {* genuine 1 @{prop "x = Not"} *} ML {* none 1 @{prop "\x. x = Not"} *} ML {* none 1 @{prop "\ 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"