remove "minipick" (the toy version of Nitpick) and some tests;
authorblanchet
Mon Sep 06 17:51:26 2010 +0200 (2010-09-06)
changeset 3922170fd4a3c41ed
parent 39220 8420a873f534
child 39222 decf607a5a67
remove "minipick" (the toy version of Nitpick) and some tests;
a small step towards making the Nitpick tests take less time
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Nitpick_Examples.thy
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Nitpick/minipick.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 06 16:50:29 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 06 17:51:26 2010 +0200
     1.3 @@ -277,7 +277,6 @@
     1.4    Tools/nat_numeral_simprocs.ML \
     1.5    Tools/Nitpick/kodkod.ML \
     1.6    Tools/Nitpick/kodkod_sat.ML \
     1.7 -  Tools/Nitpick/minipick.ML \
     1.8    Tools/Nitpick/nitpick.ML \
     1.9    Tools/Nitpick/nitpick_hol.ML \
    1.10    Tools/Nitpick/nitpick_isar.ML \
    1.11 @@ -670,11 +669,10 @@
    1.12    Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    1.13    Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
    1.14    Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    1.15 -  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    1.16 -  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    1.17 -  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    1.18 -  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    1.19 -  Nitpick_Examples/Typedef_Nits.thy
    1.20 +  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
    1.21 +  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
    1.22 +  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
    1.23 +  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
    1.24  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    1.25  
    1.26  
     2.1 --- a/src/HOL/Nitpick.thy	Mon Sep 06 16:50:29 2010 +0200
     2.2 +++ b/src/HOL/Nitpick.thy	Mon Sep 06 17:51:26 2010 +0200
     2.3 @@ -24,7 +24,6 @@
     2.4       ("Tools/Nitpick/nitpick.ML")
     2.5       ("Tools/Nitpick/nitpick_isar.ML")
     2.6       ("Tools/Nitpick/nitpick_tests.ML")
     2.7 -     ("Tools/Nitpick/minipick.ML")
     2.8  begin
     2.9  
    2.10  typedecl bisim_iterator
    2.11 @@ -237,7 +236,6 @@
    2.12  use "Tools/Nitpick/nitpick.ML"
    2.13  use "Tools/Nitpick/nitpick_isar.ML"
    2.14  use "Tools/Nitpick/nitpick_tests.ML"
    2.15 -use "Tools/Nitpick/minipick.ML"
    2.16  
    2.17  setup {* Nitpick_Isar.setup *}
    2.18  
     3.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Sep 06 16:50:29 2010 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Sep 06 17:51:26 2010 +0200
     3.3 @@ -32,44 +32,6 @@
     3.4  nitpick [card = 1\<midarrow>12, expect = none]
     3.5  by auto
     3.6  
     3.7 -lemma "(split o curry) f = f"
     3.8 -nitpick [card = 1\<midarrow>12, expect = none]
     3.9 -by auto
    3.10 -
    3.11 -lemma "(curry o split) f = f"
    3.12 -nitpick [card = 1\<midarrow>12, expect = none]
    3.13 -by auto
    3.14 -
    3.15 -lemma "(split o curry) f = (\<lambda>x. x) f"
    3.16 -nitpick [card = 1\<midarrow>12, expect = none]
    3.17 -by auto
    3.18 -
    3.19 -lemma "(curry o split) f = (\<lambda>x. x) f"
    3.20 -nitpick [card = 1\<midarrow>12, expect = none]
    3.21 -by auto
    3.22 -
    3.23 -lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    3.24 -nitpick [card = 1\<midarrow>12, expect = none]
    3.25 -by auto
    3.26 -
    3.27 -lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    3.28 -nitpick [card = 1\<midarrow>12, expect = none]
    3.29 -by auto
    3.30 -
    3.31 -lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    3.32 -nitpick [card = 1\<midarrow>12, expect = none]
    3.33 -by auto
    3.34 -
    3.35 -lemma "split o curry = (\<lambda>x. x)"
    3.36 -nitpick [card = 1\<midarrow>12, expect = none]
    3.37 -apply (rule ext)+
    3.38 -by auto
    3.39 -
    3.40 -lemma "curry o split = (\<lambda>x. x)"
    3.41 -nitpick [card = 1\<midarrow>12, expect = none]
    3.42 -apply (rule ext)+
    3.43 -by auto
    3.44 -
    3.45  lemma "split (\<lambda>x y. f (x, y)) = f"
    3.46  nitpick [card = 1\<midarrow>12, expect = none]
    3.47  by auto
    3.48 @@ -150,31 +112,31 @@
    3.49  oops
    3.50  
    3.51  lemma "{a, b} = {b}"
    3.52 -nitpick [card = 100, expect = genuine]
    3.53 +nitpick [card = 50, expect = genuine]
    3.54  oops
    3.55  
    3.56  lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
    3.57  nitpick [card = 1, expect = genuine]
    3.58 -nitpick [card = 20, expect = genuine]
    3.59 +nitpick [card = 10, expect = genuine]
    3.60  nitpick [card = 5, dont_box, expect = genuine]
    3.61  oops
    3.62  
    3.63  lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
    3.64  nitpick [card = 3, expect = genuine]
    3.65  nitpick [card = 3, dont_box, expect = genuine]
    3.66 -nitpick [card = 10, expect = genuine]
    3.67 +nitpick [card = 8, expect = genuine]
    3.68  oops
    3.69  
    3.70  lemma "f (a, b) = x"
    3.71 -nitpick [card = 12, expect = genuine]
    3.72 +nitpick [card = 10, expect = genuine]
    3.73  oops
    3.74  
    3.75  lemma "f (a, a) = f (c, d)"
    3.76 -nitpick [card = 12, expect = genuine]
    3.77 +nitpick [card = 10, expect = genuine]
    3.78  oops
    3.79  
    3.80  lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
    3.81 -nitpick [card = 1\<midarrow>12, expect = none]
    3.82 +nitpick [card = 1\<midarrow>10, expect = none]
    3.83  by auto
    3.84  
    3.85  lemma "\<exists>F. F a b = G a b"
    3.86 @@ -187,7 +149,7 @@
    3.87  oops
    3.88  
    3.89  lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
    3.90 -nitpick [card = 20, expect = none]
    3.91 +nitpick [card = 15, expect = none]
    3.92  by auto
    3.93  
    3.94  lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
    3.95 @@ -204,30 +166,30 @@
    3.96  lemma "x = y"
    3.97  nitpick [card 'a = 1, expect = none]
    3.98  nitpick [card 'a = 2, expect = genuine]
    3.99 -nitpick [card 'a = 200, expect = genuine]
   3.100 +nitpick [card 'a = 100, expect = genuine]
   3.101  oops
   3.102  
   3.103  lemma "\<forall>x. x = y"
   3.104  nitpick [card 'a = 1, expect = none]
   3.105  nitpick [card 'a = 2, expect = genuine]
   3.106 -nitpick [card 'a = 200, expect = genuine]
   3.107 +nitpick [card 'a = 100, expect = genuine]
   3.108  oops
   3.109  
   3.110  lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   3.111  nitpick [card 'a = 1, expect = genuine]
   3.112 -nitpick [card 'a = 200, expect = genuine]
   3.113 +nitpick [card 'a = 100, expect = genuine]
   3.114  oops
   3.115  
   3.116  lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   3.117 -nitpick [card 'a = 1\<midarrow>20, expect = none]
   3.118 +nitpick [card 'a = 1\<midarrow>15, expect = none]
   3.119  by auto
   3.120  
   3.121  lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   3.122 -nitpick [card = 1\<midarrow>20, expect = none]
   3.123 +nitpick [card = 1\<midarrow>15, expect = none]
   3.124  by auto
   3.125  
   3.126  lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   3.127 -nitpick [card = 1\<midarrow>5, expect = none]
   3.128 +nitpick [card = 1\<midarrow>4, expect = none]
   3.129  by auto
   3.130  
   3.131  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   3.132 @@ -241,7 +203,6 @@
   3.133  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   3.134         f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   3.135  nitpick [card = 1\<midarrow>2, expect = none]
   3.136 -nitpick [card = 3, expect = none]
   3.137  sorry
   3.138  
   3.139  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   3.140 @@ -288,18 +249,6 @@
   3.141  nitpick [expect = none]
   3.142  sorry
   3.143  
   3.144 -lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
   3.145 -nitpick [expect = none]
   3.146 -sorry
   3.147 -
   3.148 -lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   3.149 -nitpick [expect = none]
   3.150 -by auto
   3.151 -
   3.152 -lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   3.153 -nitpick [expect = none]
   3.154 -by auto
   3.155 -
   3.156  lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   3.157  nitpick [card 'a = 1, expect = genuine]
   3.158  nitpick [card 'a = 5, expect = genuine]
   3.159 @@ -383,10 +332,6 @@
   3.160  nitpick [card = 20, expect = genuine]
   3.161  oops
   3.162  
   3.163 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   3.164 -nitpick [expect = none]
   3.165 -by auto
   3.166 -
   3.167  lemma "P x \<equiv> P x"
   3.168  nitpick [card = 1\<midarrow>10, expect = none]
   3.169  by auto
   3.170 @@ -456,14 +401,12 @@
   3.171  oops
   3.172  
   3.173  lemma "\<exists>!x. x = undefined"
   3.174 -nitpick [card = 30, expect = none]
   3.175 +nitpick [card = 15, expect = none]
   3.176  by auto
   3.177  
   3.178  lemma "x = All \<Longrightarrow> False"
   3.179  nitpick [card = 1, dont_box, expect = genuine]
   3.180 -nitpick [card = 2, dont_box, expect = genuine]
   3.181 -nitpick [card = 8, dont_box, expect = genuine]
   3.182 -nitpick [card = 10, dont_box, expect = unknown]
   3.183 +nitpick [card = 5, dont_box, expect = genuine]
   3.184  oops
   3.185  
   3.186  lemma "\<forall>x. f x y = f x y"
   3.187 @@ -482,15 +425,9 @@
   3.188  nitpick [expect = genuine]
   3.189  oops
   3.190  
   3.191 -lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
   3.192 -nitpick [expect = none]
   3.193 -by auto
   3.194 -
   3.195  lemma "x = Ex \<Longrightarrow> False"
   3.196  nitpick [card = 1, dont_box, expect = genuine]
   3.197 -nitpick [card = 2, dont_box, expect = genuine]
   3.198 -nitpick [card = 6, dont_box, expect = genuine]
   3.199 -nitpick [card = 10, dont_box, expect = unknown]
   3.200 +nitpick [card = 5, dont_box, expect = genuine]
   3.201  oops
   3.202  
   3.203  lemma "\<exists>x. f x y = f x y"
   3.204 @@ -513,10 +450,6 @@
   3.205  nitpick [expect = genuine]
   3.206  oops
   3.207  
   3.208 -lemma "Ex (\<lambda>x. f x y = f y x) = False"
   3.209 -nitpick [expect = genuine]
   3.210 -oops
   3.211 -
   3.212  lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
   3.213  nitpick [expect = none]
   3.214  by auto
   3.215 @@ -525,11 +458,6 @@
   3.216  nitpick [expect = none]
   3.217  by auto
   3.218  
   3.219 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
   3.220 -      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
   3.221 -nitpick [expect = none]
   3.222 -by auto
   3.223 -
   3.224  lemma "x = y \<Longrightarrow> y = x"
   3.225  nitpick [expect = none]
   3.226  by auto
   3.227 @@ -555,35 +483,10 @@
   3.228  nitpick [expect = none]
   3.229  by auto
   3.230  
   3.231 -lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
   3.232 -nitpick [expect = none]
   3.233 -by auto
   3.234 -
   3.235 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
   3.236 -      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
   3.237 -nitpick [expect = none]
   3.238 -by auto
   3.239 -
   3.240 -lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
   3.241 -nitpick [expect = none]
   3.242 -by auto
   3.243 -
   3.244 -lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
   3.245 -nitpick [expect = none]
   3.246 -by auto
   3.247 -
   3.248  lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
   3.249  nitpick [expect = none]
   3.250  by auto
   3.251  
   3.252 -lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
   3.253 -nitpick [expect = none]
   3.254 -by auto
   3.255 -
   3.256 -lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
   3.257 -nitpick [expect = none]
   3.258 -by auto
   3.259 -
   3.260  lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
   3.261  nitpick [expect = none]
   3.262  by auto
   3.263 @@ -592,12 +495,6 @@
   3.264  nitpick [expect = none]
   3.265  by auto
   3.266  
   3.267 -lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
   3.268 -      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
   3.269 -      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
   3.270 -nitpick [expect = none]
   3.271 -by auto
   3.272 -
   3.273  lemma "fst (x, y) = x"
   3.274  nitpick [expect = none]
   3.275  by (simp add: fst_def)
   3.276 @@ -642,10 +539,6 @@
   3.277  nitpick [expect = none]
   3.278  by auto
   3.279  
   3.280 -lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
   3.281 -nitpick [expect = none]
   3.282 -by auto
   3.283 -
   3.284  lemma "fst (x, y) = snd (y, x)"
   3.285  nitpick [expect = none]
   3.286  by auto
   3.287 @@ -662,10 +555,6 @@
   3.288  nitpick [expect = none]
   3.289  by auto
   3.290  
   3.291 -lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
   3.292 -nitpick [expect = none]
   3.293 -by (simp add: curry_def)
   3.294 -
   3.295  lemma "{} = (\<lambda>x. False)"
   3.296  nitpick [expect = none]
   3.297  by (metis Collect_def empty_def)
   3.298 @@ -722,10 +611,6 @@
   3.299  nitpick [expect = none]
   3.300  by (simp add: mem_def)
   3.301  
   3.302 -lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
   3.303 -nitpick [expect = none]
   3.304 -by simp
   3.305 -
   3.306  lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
   3.307  nitpick [expect = none]
   3.308  by simp
   3.309 @@ -743,10 +628,6 @@
   3.310  nitpick [expect = none]
   3.311  by auto
   3.312  
   3.313 -lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
   3.314 -nitpick [card = 1\<midarrow>2, expect = none]
   3.315 -by auto
   3.316 -
   3.317  lemma "((x, x), (x, x)) \<in> rtrancl {}"
   3.318  nitpick [card = 1\<midarrow>5, expect = none]
   3.319  by auto
   3.320 @@ -755,42 +636,18 @@
   3.321  nitpick [card = 1\<midarrow>5, expect = none]
   3.322  by auto
   3.323  
   3.324 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
   3.325 -nitpick [card = 1\<midarrow>5, expect = none]
   3.326 -by auto
   3.327 -
   3.328  lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
   3.329  nitpick [expect = none]
   3.330  by auto
   3.331  
   3.332 -lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
   3.333 -nitpick [expect = none]
   3.334 -by auto
   3.335 -
   3.336  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
   3.337  nitpick [card = 1\<midarrow>5, expect = none]
   3.338  by auto
   3.339  
   3.340 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
   3.341 -nitpick [card = 1\<midarrow>5, expect = none]
   3.342 -by auto
   3.343 -
   3.344  lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
   3.345  nitpick [card = 1\<midarrow>5, expect = none]
   3.346  by auto
   3.347  
   3.348 -lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
   3.349 -nitpick [expect = none]
   3.350 -by auto
   3.351 -
   3.352 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
   3.353 -nitpick [card = 1\<midarrow>5, expect = none]
   3.354 -by auto
   3.355 -
   3.356 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
   3.357 -nitpick [card = 1\<midarrow>5, expect = none]
   3.358 -by auto
   3.359 -
   3.360  lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
   3.361  nitpick [card = 1\<midarrow>5, expect = none]
   3.362  by auto
   3.363 @@ -799,22 +656,10 @@
   3.364  nitpick [card = 1\<midarrow>5, expect = none]
   3.365  by auto
   3.366  
   3.367 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
   3.368 -nitpick [card = 1\<midarrow>5, expect = none]
   3.369 -by auto
   3.370 -
   3.371  lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
   3.372  nitpick [card = 1\<midarrow>5, expect = none]
   3.373  by auto
   3.374  
   3.375 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
   3.376 -nitpick [card = 1\<midarrow>5, expect = none]
   3.377 -by auto
   3.378 -
   3.379 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
   3.380 -nitpick [card = 1\<midarrow>5, expect = none]
   3.381 -by auto
   3.382 -
   3.383  lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
   3.384  nitpick [card = 1\<midarrow>5, expect = none]
   3.385  by auto
   3.386 @@ -843,10 +688,6 @@
   3.387  nitpick [card 'a = 10, expect = genuine]
   3.388  oops
   3.389  
   3.390 -lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
   3.391 -nitpick [card = 1\<midarrow>7, expect = none]
   3.392 -oops
   3.393 -
   3.394  lemma "finite A"
   3.395  nitpick [expect = none]
   3.396  oops
     4.1 --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Mon Sep 06 16:50:29 2010 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Mon Sep 06 17:51:26 2010 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  theory Nitpick_Examples
     4.6  imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
     4.7 -        Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
     4.8 -        Tests_Nits Typedef_Nits
     4.9 +        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
    4.10 +        Typedef_Nits
    4.11  begin
    4.12  end
     5.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 06 16:50:29 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 06 17:51:26 2010 +0200
     5.3 @@ -71,7 +71,7 @@
     5.4                       [if null markers then "External" else "ExternalV2",
     5.5                        dir ^ dir_sep ^ exec, base ^ ".cnf",
     5.6                        if dev = ToFile then out_file else ""] @ markers @
     5.7 -                      (if dev = ToFile then [out_file] else []) @ args
     5.8 +                     (if dev = ToFile then [out_file] else []) @ args
     5.9                     end)
    5.10  fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    5.11      if incremental andalso mode = Batch then NONE else SOME (name, K ss)
     6.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Sep 06 16:50:29 2010 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,327 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/Nitpick/minipick.ML
     6.5 -    Author:     Jasmin Blanchette, TU Muenchen
     6.6 -    Copyright   2009, 2010
     6.7 -
     6.8 -Finite model generation for HOL formulas using Kodkod, minimalistic version.
     6.9 -*)
    6.10 -
    6.11 -signature MINIPICK =
    6.12 -sig
    6.13 -  datatype rep = SRep | RRep
    6.14 -  type styp = Nitpick_Util.styp
    6.15 -
    6.16 -  val vars_for_bound_var :
    6.17 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    6.18 -  val rel_expr_for_bound_var :
    6.19 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    6.20 -  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    6.21 -  val false_atom : Kodkod.rel_expr
    6.22 -  val true_atom : Kodkod.rel_expr
    6.23 -  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    6.24 -  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    6.25 -  val kodkod_problem_from_term :
    6.26 -    Proof.context -> (typ -> int) -> term -> Kodkod.problem
    6.27 -  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    6.28 -end;
    6.29 -
    6.30 -structure Minipick : MINIPICK =
    6.31 -struct
    6.32 -
    6.33 -open Kodkod
    6.34 -open Nitpick_Util
    6.35 -open Nitpick_HOL
    6.36 -open Nitpick_Peephole
    6.37 -open Nitpick_Kodkod
    6.38 -
    6.39 -datatype rep = SRep | RRep
    6.40 -
    6.41 -fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    6.42 -    List.app (check_type ctxt) Ts
    6.43 -  | check_type ctxt (Type (@{type_name prod}, Ts)) =
    6.44 -    List.app (check_type ctxt) Ts
    6.45 -  | check_type _ @{typ bool} = ()
    6.46 -  | check_type _ (TFree (_, @{sort "{}"})) = ()
    6.47 -  | check_type _ (TFree (_, @{sort HOL.type})) = ()
    6.48 -  | check_type ctxt T =
    6.49 -    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    6.50 -
    6.51 -fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
    6.52 -    replicate_list (card T1) (atom_schema_of SRep card T2)
    6.53 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    6.54 -    atom_schema_of SRep card T1
    6.55 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    6.56 -    atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    6.57 -  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    6.58 -    maps (atom_schema_of SRep card) Ts
    6.59 -  | atom_schema_of _ card T = [card T]
    6.60 -val arity_of = length ooo atom_schema_of
    6.61 -
    6.62 -fun index_for_bound_var _ [_] 0 = 0
    6.63 -  | index_for_bound_var card (_ :: Ts) 0 =
    6.64 -    index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
    6.65 -  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
    6.66 -fun vars_for_bound_var card R Ts j =
    6.67 -  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
    6.68 -                               (arity_of R card (nth Ts j)))
    6.69 -val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
    6.70 -fun decls_for R card Ts T =
    6.71 -  map2 (curry DeclOne o pair 1)
    6.72 -       (index_seq (index_for_bound_var card (T :: Ts) 0)
    6.73 -                  (arity_of R card (nth (T :: Ts) 0)))
    6.74 -       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    6.75 -
    6.76 -val atom_product = foldl1 Product o map Atom
    6.77 -
    6.78 -val false_atom = Atom 0
    6.79 -val true_atom = Atom 1
    6.80 -
    6.81 -fun formula_from_atom r = RelEq (r, true_atom)
    6.82 -fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    6.83 -
    6.84 -fun kodkod_formula_from_term ctxt card frees =
    6.85 -  let
    6.86 -    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    6.87 -        let
    6.88 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    6.89 -                    |> all_combinations
    6.90 -        in
    6.91 -          map2 (fn i => fn js =>
    6.92 -                   RelIf (formula_from_atom (Project (r, [Num i])),
    6.93 -                          atom_product js, empty_n_ary_rel (length js)))
    6.94 -               (index_seq 0 (length jss)) jss
    6.95 -          |> foldl1 Union
    6.96 -        end
    6.97 -      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    6.98 -        let
    6.99 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
   6.100 -                    |> all_combinations
   6.101 -          val arity2 = arity_of SRep card T2
   6.102 -        in
   6.103 -          map2 (fn i => fn js =>
   6.104 -                   Product (atom_product js,
   6.105 -                            Project (r, num_seq (i * arity2) arity2)
   6.106 -                            |> R_rep_from_S_rep T2))
   6.107 -               (index_seq 0 (length jss)) jss
   6.108 -          |> foldl1 Union
   6.109 -        end
   6.110 -      | R_rep_from_S_rep _ r = r
   6.111 -    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   6.112 -        Comprehension (decls_for SRep card Ts T,
   6.113 -            RelEq (R_rep_from_S_rep T
   6.114 -                       (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
   6.115 -      | S_rep_from_R_rep _ _ r = r
   6.116 -    fun to_F Ts t =
   6.117 -      (case t of
   6.118 -         @{const Not} $ t1 => Not (to_F Ts t1)
   6.119 -       | @{const False} => False
   6.120 -       | @{const True} => True
   6.121 -       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   6.122 -         All (decls_for SRep card Ts T, to_F (T :: Ts) t')
   6.123 -       | (t0 as Const (@{const_name All}, _)) $ t1 =>
   6.124 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   6.125 -       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   6.126 -         Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
   6.127 -       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   6.128 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   6.129 -       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   6.130 -         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   6.131 -       | Const (@{const_name ord_class.less_eq},
   6.132 -                Type (@{type_name fun},
   6.133 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   6.134 -         $ t1 $ t2 =>
   6.135 -         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   6.136 -       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   6.137 -       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   6.138 -       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   6.139 -       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   6.140 -       | Free _ => raise SAME ()
   6.141 -       | Term.Var _ => raise SAME ()
   6.142 -       | Bound _ => raise SAME ()
   6.143 -       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   6.144 -       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   6.145 -      handle SAME () => formula_from_atom (to_R_rep Ts t)
   6.146 -    and to_S_rep Ts t =
   6.147 -      case t of
   6.148 -        Const (@{const_name Pair}, _) $ t1 $ t2 =>
   6.149 -        Product (to_S_rep Ts t1, to_S_rep Ts t2)
   6.150 -      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
   6.151 -      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
   6.152 -      | Const (@{const_name fst}, _) $ t1 =>
   6.153 -        let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
   6.154 -          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
   6.155 -        end
   6.156 -      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
   6.157 -      | Const (@{const_name snd}, _) $ t1 =>
   6.158 -        let
   6.159 -          val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
   6.160 -          val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
   6.161 -          val fst_arity = pair_arity - snd_arity
   6.162 -        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
   6.163 -      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   6.164 -      | Bound j => rel_expr_for_bound_var card SRep Ts j
   6.165 -      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   6.166 -    and to_R_rep Ts t =
   6.167 -      (case t of
   6.168 -         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   6.169 -       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   6.170 -       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   6.171 -       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   6.172 -       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   6.173 -       | Const (@{const_name ord_class.less_eq},
   6.174 -                Type (@{type_name fun},
   6.175 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   6.176 -         to_R_rep Ts (eta_expand Ts t 1)
   6.177 -       | Const (@{const_name ord_class.less_eq}, _) =>
   6.178 -         to_R_rep Ts (eta_expand Ts t 2)
   6.179 -       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   6.180 -       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   6.181 -       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   6.182 -       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   6.183 -       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   6.184 -       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   6.185 -       | Const (@{const_name bot_class.bot},
   6.186 -                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   6.187 -         empty_n_ary_rel (arity_of RRep card T)
   6.188 -       | Const (@{const_name insert}, _) $ t1 $ t2 =>
   6.189 -         Union (to_S_rep Ts t1, to_R_rep Ts t2)
   6.190 -       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   6.191 -       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   6.192 -       | Const (@{const_name trancl}, _) $ t1 =>
   6.193 -         if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
   6.194 -           Closure (to_R_rep Ts t1)
   6.195 -         else
   6.196 -           raise NOT_SUPPORTED "transitive closure for function or pair type"
   6.197 -       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   6.198 -       | Const (@{const_name semilattice_inf_class.inf},
   6.199 -                Type (@{type_name fun},
   6.200 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   6.201 -         $ t1 $ t2 =>
   6.202 -         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   6.203 -       | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
   6.204 -         to_R_rep Ts (eta_expand Ts t 1)
   6.205 -       | Const (@{const_name semilattice_inf_class.inf}, _) =>
   6.206 -         to_R_rep Ts (eta_expand Ts t 2)
   6.207 -       | Const (@{const_name semilattice_sup_class.sup},
   6.208 -                Type (@{type_name fun},
   6.209 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   6.210 -         $ t1 $ t2 =>
   6.211 -         Union (to_R_rep Ts t1, to_R_rep Ts t2)
   6.212 -       | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
   6.213 -         to_R_rep Ts (eta_expand Ts t 1)
   6.214 -       | Const (@{const_name semilattice_sup_class.sup}, _) =>
   6.215 -         to_R_rep Ts (eta_expand Ts t 2)
   6.216 -       | Const (@{const_name minus_class.minus},
   6.217 -                Type (@{type_name fun},
   6.218 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   6.219 -         $ t1 $ t2 =>
   6.220 -         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   6.221 -       | Const (@{const_name minus_class.minus},
   6.222 -                Type (@{type_name fun},
   6.223 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   6.224 -         to_R_rep Ts (eta_expand Ts t 1)
   6.225 -       | Const (@{const_name minus_class.minus},
   6.226 -                Type (@{type_name fun},
   6.227 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   6.228 -         to_R_rep Ts (eta_expand Ts t 2)
   6.229 -       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   6.230 -       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   6.231 -       | Const (@{const_name Pair}, _) => raise SAME ()
   6.232 -       | Const (@{const_name fst}, _) $ _ => raise SAME ()
   6.233 -       | Const (@{const_name fst}, _) => raise SAME ()
   6.234 -       | Const (@{const_name snd}, _) $ _ => raise SAME ()
   6.235 -       | Const (@{const_name snd}, _) => raise SAME ()
   6.236 -       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   6.237 -       | Free (x as (_, T)) =>
   6.238 -         Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
   6.239 -       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   6.240 -       | Bound _ => raise SAME ()
   6.241 -       | Abs (_, T, t') =>
   6.242 -         (case fastype_of1 (T :: Ts, t') of
   6.243 -            @{typ bool} => Comprehension (decls_for SRep card Ts T,
   6.244 -                                          to_F (T :: Ts) t')
   6.245 -          | T' => Comprehension (decls_for SRep card Ts T @
   6.246 -                                 decls_for RRep card (T :: Ts) T',
   6.247 -                                 Subset (rel_expr_for_bound_var card RRep
   6.248 -                                                              (T' :: T :: Ts) 0,
   6.249 -                                         to_R_rep (T :: Ts) t')))
   6.250 -       | t1 $ t2 =>
   6.251 -         (case fastype_of1 (Ts, t) of
   6.252 -            @{typ bool} => atom_from_formula (to_F Ts t)
   6.253 -          | T =>
   6.254 -            let val T2 = fastype_of1 (Ts, t2) in
   6.255 -              case arity_of SRep card T2 of
   6.256 -                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   6.257 -              | arity2 =>
   6.258 -                let val res_arity = arity_of RRep card T in
   6.259 -                  Project (Intersect
   6.260 -                      (Product (to_S_rep Ts t2,
   6.261 -                                atom_schema_of RRep card T
   6.262 -                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
   6.263 -                       to_R_rep Ts t1),
   6.264 -                      num_seq arity2 res_arity)
   6.265 -                end
   6.266 -            end)
   6.267 -       | _ => raise NOT_SUPPORTED ("term " ^
   6.268 -                                   quote (Syntax.string_of_term ctxt t)))
   6.269 -      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   6.270 -  in to_F [] end
   6.271 -
   6.272 -fun bound_for_free card i (s, T) =
   6.273 -  let val js = atom_schema_of RRep card T in
   6.274 -    ([((length js, i), s)],
   6.275 -     [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
   6.276 -                   |> tuple_set_from_atom_schema])
   6.277 -  end
   6.278 -
   6.279 -fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   6.280 -                                   r =
   6.281 -    if body_type T2 = bool_T then
   6.282 -      True
   6.283 -    else
   6.284 -      All (decls_for SRep card Ts T1,
   6.285 -           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   6.286 -               (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
   6.287 -  | declarative_axiom_for_rel_expr _ _ _ r = One r
   6.288 -fun declarative_axiom_for_free card i (_, T) =
   6.289 -  declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
   6.290 -
   6.291 -fun kodkod_problem_from_term ctxt raw_card t =
   6.292 -  let
   6.293 -    val thy = ProofContext.theory_of ctxt
   6.294 -    fun card (Type (@{type_name fun}, [T1, T2])) =
   6.295 -        reasonable_power (card T2) (card T1)
   6.296 -      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   6.297 -      | card @{typ bool} = 2
   6.298 -      | card T = Int.max (1, raw_card T)
   6.299 -    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   6.300 -    val _ = fold_types (K o check_type ctxt) neg_t ()
   6.301 -    val frees = Term.add_frees neg_t []
   6.302 -    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   6.303 -    val declarative_axioms =
   6.304 -      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   6.305 -    val formula = kodkod_formula_from_term ctxt card frees neg_t
   6.306 -                  |> fold_rev (curry And) declarative_axioms
   6.307 -    val univ_card = univ_card 0 0 0 bounds formula
   6.308 -  in
   6.309 -    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   6.310 -     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   6.311 -  end
   6.312 -
   6.313 -fun solve_any_kodkod_problem thy problems =
   6.314 -  let
   6.315 -    val {overlord, ...} = Nitpick_Isar.default_params thy []
   6.316 -    val max_threads = 1
   6.317 -    val max_solutions = 1
   6.318 -  in
   6.319 -    case solve_any_problem overlord NONE max_threads max_solutions problems of
   6.320 -      JavaNotInstalled => "unknown"
   6.321 -    | JavaTooOld => "unknown"
   6.322 -    | KodkodiNotInstalled => "unknown"
   6.323 -    | Normal ([], _, _) => "none"
   6.324 -    | Normal _ => "genuine"
   6.325 -    | TimedOut _ => "unknown"
   6.326 -    | Interrupted _ => "unknown"
   6.327 -    | Error (s, _) => error ("Kodkod error: " ^ s)
   6.328 -  end
   6.329 -
   6.330 -end;