# HG changeset patch
# User blanchet
# Date 1277111760 -7200
# Node ID e482320bcbfe9c47d29c67dff34b8e948e971df0
# Parent  0681e46b4022dcbad2a5237f79629c1ae20934b9
adjusted Nitpick examples to latest changes + make them slightly faster

diff -r 0681e46b4022 -r e482320bcbfe src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Jun 21 11:15:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Jun 21 11:16:00 2010 +0200
@@ -187,7 +187,7 @@
 
 lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
 nitpick [unary_ints, expect = none]
-nitpick [binary_ints, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]
+nitpick [binary_ints, card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
 sorry
 
 lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
@@ -213,7 +213,7 @@
 "labels (Node x t u) = {x} \<union> labels t \<union> labels u"
 
 lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
-nitpick [expect = genuine]
+nitpick [expect = potential] (* unfortunate *)
 nitpick [dont_finitize, expect = potential]
 oops
 
@@ -222,12 +222,12 @@
 oops
 
 lemma "card (labels t) > 0"
-nitpick [expect = genuine]
+nitpick [expect = potential] (* unfortunate *)
 nitpick [dont_finitize, expect = potential]
 oops
 
 lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
-nitpick [expect = genuine]
+nitpick [expect = potential] (* unfortunate *)
 nitpick [dont_finitize, expect = potential]
 oops
 
@@ -237,7 +237,7 @@
 sorry
 
 lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
-nitpick [expect = genuine]
+nitpick [expect = none] (* unfortunate *)
 nitpick [dont_finitize, expect = none]
 oops
 
diff -r 0681e46b4022 -r e482320bcbfe src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Jun 21 11:15:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Jun 21 11:16:00 2010 +0200
@@ -7,13 +7,17 @@
 
 header {* Examples from the Nitpick Manual *}
 
+(* The "expect" arguments to Nitpick in this theory and the other example
+   theories are there so that the example can also serve as a regression test
+   suite. *)
+
 theory Manual_Nits
 imports Main Quotient_Product RealDef
 begin
 
 chapter {* 3. First Steps *}
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 subsection {* 3.1. Propositional Logic *}
 
@@ -379,7 +383,7 @@
 
 theorem S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 theorem S\<^isub>3_complete:
@@ -398,19 +402,19 @@
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 subsection {* 4.2. AA Trees *}
diff -r 0681e46b4022 -r e482320bcbfe src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Jun 21 11:15:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Jun 21 11:16:00 2010 +0200
@@ -76,8 +76,8 @@
 ML {* const @{term "[a::'a set]"} *}
 ML {* const @{term "[A \<union> (B::'a set)]"} *}
 ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
+ML {* const @{term "{(\<lambda>x::'a. x = a)} = C"} *}
 
-ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *}
 ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
 ML {* nonconst @{term "\<forall>a::'a. P a"} *}
 ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}