improve precision of "card" in Nitpick
authorblanchet
Wed Mar 10 19:21:59 2010 +0100 (2010-03-10)
changeset 356999ed327529a44
parent 35698 c362465085c5
child 35700 951974ce903e
improve precision of "card" in Nitpick
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Tools/Nitpick/minipick.ML
     1.1 --- a/src/HOL/Nitpick.thy	Wed Mar 10 17:46:28 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Mar 10 19:21:59 2010 +0100
     1.3 @@ -96,10 +96,10 @@
     1.4                  else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
     1.5  
     1.6  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
     1.7 -"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
     1.8 +"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
     1.9  
    1.10  definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
    1.11 -"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    1.12 +"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
    1.13  
    1.14  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
    1.15  "fold_graph' f z {} z" |
     2.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Mar 10 17:46:28 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Mar 10 19:21:59 2010 +0100
     2.3 @@ -24,8 +24,6 @@
     2.4  fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
     2.5  *}
     2.6  
     2.7 -ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
     2.8 -
     2.9  ML {* genuine 1 @{prop "x = Not"} *}
    2.10  ML {* none 1 @{prop "\<exists>x. x = Not"} *}
    2.11  ML {* none 1 @{prop "\<not> False"} *}
     3.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Mar 10 17:46:28 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Mar 10 19:21:59 2010 +0100
     3.3 @@ -336,7 +336,8 @@
     3.4      val max_solutions = 1
     3.5    in
     3.6      case solve_any_problem overlord NONE max_threads max_solutions problems of
     3.7 -      NotInstalled => "unknown"
     3.8 +      JavaNotInstalled => "unknown"
     3.9 +    | KodkodiNotInstalled => "unknown"
    3.10      | Normal ([], _, _) => "none"
    3.11      | Normal _ => "genuine"
    3.12      | TimedOut _ => "unknown"