author blanchet Wed Mar 10 19:21:59 2010 +0100 (2010-03-10) changeset 35699 9ed327529a44 parent 35698 c362465085c5 child 35700 951974ce903e
improve precision of "card" in Nitpick
 src/HOL/Nitpick.thy file | annotate | diff | revisions src/HOL/Nitpick_Examples/Mini_Nits.thy file | annotate | diff | revisions src/HOL/Tools/Nitpick/minipick.ML file | annotate | diff | revisions
```     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"
```