author blanchet Tue, 14 Sep 2010 14:22:49 +0200 changeset 39362 ee65900bfced parent 39361 520ea38711e4 child 39363 1c4e38d635e1
adapt examples to latest Nitpick changes + speed them up a little bit
```--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Sep 14 14:12:18 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Sep 14 14:22:49 2010 +0200
@@ -11,7 +11,7 @@
imports Nitpick
begin

-nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8,
+nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]

lemma "Suc x = x + 1"
@@ -232,13 +232,13 @@
oops

lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
-nitpick [expect = none]
-nitpick [dont_finitize, expect = none]
+nitpick [expect = potential] (* unfortunate *)
+nitpick [dont_finitize, expect = potential]
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 = none] (* unfortunate *)
-nitpick [dont_finitize, expect = none]
+nitpick [expect = potential] (* unfortunate *)
+nitpick [dont_finitize, expect = potential]
oops

end```
```--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 14 14:12:18 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 14 14:22:49 2010 +0200
@@ -38,8 +38,7 @@

lemma "P x \<Longrightarrow> P (THE y. P y)"
nitpick [show_consts, expect = genuine]
-nitpick [full_descrs, show_consts, expect = genuine]
-nitpick [dont_specialize, full_descrs, show_consts, expect = genuine]
+nitpick [dont_specialize, show_consts, expect = genuine]
oops

lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"```
```--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Sep 14 14:12:18 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Sep 14 14:22:49 2010 +0200
@@ -64,7 +64,7 @@
oops

lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [expect = none]
+nitpick [expect = potential] (* unfortunate *)
sorry

lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
@@ -162,10 +162,6 @@
nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
by (rule Zero_int_def_raw)

-lemma "Abs_Integ (Rep_Integ a) = a"
-nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
-by (rule Rep_Integ_inverse)
-
lemma "Abs_list (Rep_list a) = a"
nitpick [card = 1\<midarrow>2, expect = none]
by (rule Rep_list_inverse)```