# 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 \ 0 \ x * y div y = (x::int)" nitpick [unary_ints, expect = none] -nitpick [binary_ints, expect = none, card = 1\5, bits = 1\5] +nitpick [binary_ints, card = 1\4, bits = 1\4, expect = none] sorry lemma "(x * y < 0) \ (x > 0 \ y < 0) \ (x < 0 \ y > (0::int))" @@ -213,7 +213,7 @@ "labels (Node x t u) = {x} \ labels t \ labels u" lemma "labels (Node x t u) \ 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 "(\n \ labels t. n + 2) \ 2" -nitpick [expect = genuine] +nitpick [expect = potential] (* unfortunate *) nitpick [dont_finitize, expect = potential] oops @@ -237,7 +237,7 @@ sorry lemma "(\i \ labels (Node x t u). f i\nat) = f x + (\i \ labels t. f i) + (\i \ 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 \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>3_complete: @@ -398,19 +402,19 @@ theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" "w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" "w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\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 \ (B::'a set)]"} *} ML {* const @{term "[A \ (B::'a set)] = [C]"} *} +ML {* const @{term "{(\x::'a. x = a)} = C"} *} -ML {* nonconst @{term "{(\x::'a. x = a)} = C"} *} ML {* nonconst @{term "\P (a::'a). P a"} *} ML {* nonconst @{term "\a::'a. P a"} *} ML {* nonconst @{term "(\a::'a. \ A a) = B"} *}