src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 35284 9edc2bd6d2bd
parent 35078 6fd1052fe463
child 35386 45a4e19d3ebd
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -11,82 +11,67 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     1.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     1.9 +                timeout = 60 s]
    1.10  
    1.11  subsection {* Curry in a Hurry *}
    1.12  
    1.13  lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    1.14 -nitpick [card = 1\<midarrow>4, expect = none]
    1.15 -nitpick [card = 100, expect = none, timeout = none]
    1.16 +nitpick [card = 1\<midarrow>12, expect = none]
    1.17  by auto
    1.18  
    1.19  lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    1.20 -nitpick [card = 2]
    1.21 -nitpick [card = 1\<midarrow>4, expect = none]
    1.22 -nitpick [card = 10, expect = none]
    1.23 +nitpick [card = 1\<midarrow>12, expect = none]
    1.24  by auto
    1.25  
    1.26  lemma "split (curry f) = f"
    1.27 -nitpick [card = 1\<midarrow>4, expect = none]
    1.28 -nitpick [card = 10, expect = none]
    1.29 -nitpick [card = 40, expect = none]
    1.30 +nitpick [card = 1\<midarrow>12, expect = none]
    1.31  by auto
    1.32  
    1.33  lemma "curry (split f) = f"
    1.34 -nitpick [card = 1\<midarrow>4, expect = none]
    1.35 -nitpick [card = 40, expect = none]
    1.36 +nitpick [card = 1\<midarrow>12, expect = none]
    1.37  by auto
    1.38  
    1.39  lemma "(split o curry) f = f"
    1.40 -nitpick [card = 1\<midarrow>4, expect = none]
    1.41 -nitpick [card = 40, expect = none]
    1.42 +nitpick [card = 1\<midarrow>12, expect = none]
    1.43  by auto
    1.44  
    1.45  lemma "(curry o split) f = f"
    1.46 -nitpick [card = 1\<midarrow>4, expect = none]
    1.47 -nitpick [card = 1000, expect = none]
    1.48 +nitpick [card = 1\<midarrow>12, expect = none]
    1.49  by auto
    1.50  
    1.51  lemma "(split o curry) f = (\<lambda>x. x) f"
    1.52 -nitpick [card = 1\<midarrow>4, expect = none]
    1.53 -nitpick [card = 40, expect = none]
    1.54 +nitpick [card = 1\<midarrow>12, expect = none]
    1.55  by auto
    1.56  
    1.57  lemma "(curry o split) f = (\<lambda>x. x) f"
    1.58 -nitpick [card = 1\<midarrow>4, expect = none]
    1.59 -nitpick [card = 40, expect = none]
    1.60 +nitpick [card = 1\<midarrow>12, expect = none]
    1.61  by auto
    1.62  
    1.63  lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    1.64 -nitpick [card = 1\<midarrow>4, expect = none]
    1.65 -nitpick [card = 40, expect = none]
    1.66 +nitpick [card = 1\<midarrow>12, expect = none]
    1.67  by auto
    1.68  
    1.69  lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    1.70 -nitpick [card = 1\<midarrow>4, expect = none]
    1.71 -nitpick [card = 1000, expect = none]
    1.72 +nitpick [card = 1\<midarrow>12, expect = none]
    1.73  by auto
    1.74  
    1.75  lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    1.76 -nitpick [card = 1\<midarrow>4, expect = none]
    1.77 -nitpick [card = 1000, expect = none]
    1.78 +nitpick [card = 1\<midarrow>12, expect = none]
    1.79  by auto
    1.80  
    1.81  lemma "split o curry = (\<lambda>x. x)"
    1.82 -nitpick [card = 1\<midarrow>4, expect = none]
    1.83 -nitpick [card = 40, expect = none]
    1.84 +nitpick [card = 1\<midarrow>12, expect = none]
    1.85  apply (rule ext)+
    1.86  by auto
    1.87  
    1.88  lemma "curry o split = (\<lambda>x. x)"
    1.89 -nitpick [card = 1\<midarrow>4, expect = none]
    1.90 -nitpick [card = 100, expect = none]
    1.91 +nitpick [card = 1\<midarrow>12, expect = none]
    1.92  apply (rule ext)+
    1.93  by auto
    1.94  
    1.95  lemma "split (\<lambda>x y. f (x, y)) = f"
    1.96 -nitpick [card = 1\<midarrow>4, expect = none]
    1.97 -nitpick [card = 40, expect = none]
    1.98 +nitpick [card = 1\<midarrow>12, expect = none]
    1.99  by auto
   1.100  
   1.101  subsection {* Representations *}
   1.102 @@ -96,13 +81,12 @@
   1.103  by auto
   1.104  
   1.105  lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   1.106 -nitpick [card 'a = 35, card 'b = 34, expect = genuine]
   1.107 -nitpick [card = 1\<midarrow>15, mono, expect = none]
   1.108 +nitpick [card 'a = 25, card 'b = 24, expect = genuine]
   1.109 +nitpick [card = 1\<midarrow>10, mono, expect = none]
   1.110  oops
   1.111  
   1.112  lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
   1.113  nitpick [card = 1, expect = genuine]
   1.114 -nitpick [card = 2, expect = genuine]
   1.115  nitpick [card = 5, expect = genuine]
   1.116  oops
   1.117  
   1.118 @@ -112,8 +96,7 @@
   1.119  oops
   1.120  
   1.121  lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
   1.122 -nitpick [card = 1\<midarrow>6, expect = none]
   1.123 -nitpick [card = 20, expect = none]
   1.124 +nitpick [card = 1\<midarrow>12, expect = none]
   1.125  by auto
   1.126  
   1.127  lemma "fst (a, b) = a"
   1.128 @@ -121,7 +104,7 @@
   1.129  by auto
   1.130  
   1.131  lemma "\<exists>P. P = Id"
   1.132 -nitpick [card = 1\<midarrow>4, expect = none]
   1.133 +nitpick [card = 1\<midarrow>20, expect = none]
   1.134  by auto
   1.135  
   1.136  lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
   1.137 @@ -129,11 +112,11 @@
   1.138  by auto
   1.139  
   1.140  lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
   1.141 -nitpick [card = 1\<midarrow>6, expect = none]
   1.142 +nitpick [card = 1\<midarrow>4, expect = none]
   1.143  by auto
   1.144  
   1.145  lemma "Id (a, a)"
   1.146 -nitpick [card = 1\<midarrow>100, expect = none]
   1.147 +nitpick [card = 1\<midarrow>50, expect = none]
   1.148  by (auto simp: Id_def Collect_def)
   1.149  
   1.150  lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
   1.151 @@ -151,7 +134,7 @@
   1.152  lemma "g = Let (A \<or> B)"
   1.153  nitpick [card = 1, expect = none]
   1.154  nitpick [card = 2, expect = genuine]
   1.155 -nitpick [card = 20, expect = genuine]
   1.156 +nitpick [card = 12, expect = genuine]
   1.157  oops
   1.158  
   1.159  lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
   1.160 @@ -172,37 +155,30 @@
   1.161  
   1.162  lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
   1.163  nitpick [card = 1, expect = genuine]
   1.164 -nitpick [card = 2, expect = genuine]
   1.165 -nitpick [card = 4, expect = genuine]
   1.166  nitpick [card = 20, expect = genuine]
   1.167 -nitpick [card = 10, dont_box, expect = genuine]
   1.168 +nitpick [card = 5, dont_box, expect = genuine]
   1.169  oops
   1.170  
   1.171  lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
   1.172  nitpick [card = 3, expect = genuine]
   1.173  nitpick [card = 3, dont_box, expect = genuine]
   1.174 -nitpick [card = 5, expect = genuine]
   1.175  nitpick [card = 10, expect = genuine]
   1.176  oops
   1.177  
   1.178  lemma "f (a, b) = x"
   1.179 -nitpick [card = 3, expect = genuine]
   1.180 -nitpick [card = 10, expect = genuine]
   1.181 -nitpick [card = 16, expect = genuine]
   1.182 -nitpick [card = 30, expect = genuine]
   1.183 +nitpick [card = 12, expect = genuine]
   1.184  oops
   1.185  
   1.186  lemma "f (a, a) = f (c, d)"
   1.187 -nitpick [card = 4, expect = genuine]
   1.188 -nitpick [card = 20, expect = genuine]
   1.189 +nitpick [card = 12, expect = genuine]
   1.190  oops
   1.191  
   1.192  lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
   1.193 -nitpick [card = 2, expect = none]
   1.194 +nitpick [card = 1\<midarrow>12, expect = none]
   1.195  by auto
   1.196  
   1.197  lemma "\<exists>F. F a b = G a b"
   1.198 -nitpick [card = 3, expect = none]
   1.199 +nitpick [card = 2, expect = none]
   1.200  by auto
   1.201  
   1.202  lemma "f = split"
   1.203 @@ -216,12 +192,10 @@
   1.204  
   1.205  lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   1.206         A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
   1.207 -nitpick [card = 1\<midarrow>50, expect = none]
   1.208 +nitpick [card = 1\<midarrow>25, expect = none]
   1.209  by auto
   1.210  
   1.211  lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
   1.212 -nitpick [card = 3, expect = genuine]
   1.213 -nitpick [card = 4, expect = genuine]
   1.214  nitpick [card = 8, expect = genuine]
   1.215  oops
   1.216  
   1.217 @@ -230,30 +204,26 @@
   1.218  lemma "x = y"
   1.219  nitpick [card 'a = 1, expect = none]
   1.220  nitpick [card 'a = 2, expect = genuine]
   1.221 -nitpick [card 'a = 100, expect = genuine]
   1.222 -nitpick [card 'a = 1000, expect = genuine]
   1.223 +nitpick [card 'a = 200, expect = genuine]
   1.224  oops
   1.225  
   1.226  lemma "\<forall>x. x = y"
   1.227  nitpick [card 'a = 1, expect = none]
   1.228  nitpick [card 'a = 2, expect = genuine]
   1.229 -nitpick [card 'a = 100, expect = genuine]
   1.230 -nitpick [card 'a = 1000, expect = genuine]
   1.231 +nitpick [card 'a = 200, expect = genuine]
   1.232  oops
   1.233  
   1.234  lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   1.235  nitpick [card 'a = 1, expect = genuine]
   1.236 -nitpick [card 'a = 2, expect = genuine]
   1.237 -nitpick [card 'a = 100, expect = genuine]
   1.238 -nitpick [card 'a = 1000, expect = genuine]
   1.239 +nitpick [card 'a = 200, expect = genuine]
   1.240  oops
   1.241  
   1.242  lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   1.243 -nitpick [card 'a = 1\<midarrow>10, expect = none]
   1.244 +nitpick [card 'a = 1\<midarrow>20, expect = none]
   1.245  by auto
   1.246  
   1.247  lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   1.248 -nitpick [card = 1\<midarrow>40, expect = none]
   1.249 +nitpick [card = 1\<midarrow>20, expect = none]
   1.250  by auto
   1.251  
   1.252  lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   1.253 @@ -261,11 +231,10 @@
   1.254  by auto
   1.255  
   1.256  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   1.257 -nitpick [card = 1\<midarrow>5, expect = none]
   1.258 +nitpick [card = 1\<midarrow>4, expect = none]
   1.259  by auto
   1.260  
   1.261  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
   1.262 -nitpick [card = 1\<midarrow>2, expect = genuine]
   1.263  nitpick [card = 3, expect = genuine]
   1.264  oops
   1.265  
   1.266 @@ -273,7 +242,6 @@
   1.267         f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   1.268  nitpick [card = 1\<midarrow>2, expect = none]
   1.269  nitpick [card = 3, expect = none]
   1.270 -nitpick [card = 4, expect = none]
   1.271  sorry
   1.272  
   1.273  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   1.274 @@ -334,9 +302,6 @@
   1.275  
   1.276  lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   1.277  nitpick [card 'a = 1, expect = genuine]
   1.278 -nitpick [card 'a = 2, expect = genuine]
   1.279 -nitpick [card 'a = 3, expect = genuine]
   1.280 -nitpick [card 'a = 4, expect = genuine]
   1.281  nitpick [card 'a = 5, expect = genuine]
   1.282  oops
   1.283  
   1.284 @@ -390,8 +355,7 @@
   1.285  nitpick [card = 1, expect = genuine]
   1.286  nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   1.287  nitpick [card = 2, expect = genuine]
   1.288 -nitpick [card = 8, expect = genuine]
   1.289 -nitpick [card = 10, expect = unknown]
   1.290 +nitpick [card = 6, expect = genuine]
   1.291  oops
   1.292  
   1.293  lemma "\<And>x. f x y = f x y"
   1.294 @@ -416,11 +380,7 @@
   1.295  
   1.296  lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
   1.297  nitpick [card = 1, expect = genuine]
   1.298 -nitpick [card = 2, expect = genuine]
   1.299 -nitpick [card = 3, expect = genuine]
   1.300 -nitpick [card = 4, expect = genuine]
   1.301 -nitpick [card = 5, expect = genuine]
   1.302 -nitpick [card = 100, expect = genuine]
   1.303 +nitpick [card = 20, expect = genuine]
   1.304  oops
   1.305  
   1.306  lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   1.307 @@ -529,7 +489,7 @@
   1.308  lemma "x = Ex \<Longrightarrow> False"
   1.309  nitpick [card = 1, dont_box, expect = genuine]
   1.310  nitpick [card = 2, dont_box, expect = genuine]
   1.311 -nitpick [card = 8, dont_box, expect = genuine]
   1.312 +nitpick [card = 6, dont_box, expect = genuine]
   1.313  nitpick [card = 10, dont_box, expect = unknown]
   1.314  oops
   1.315  
   1.316 @@ -582,8 +542,8 @@
   1.317  nitpick [expect = none]
   1.318  by auto
   1.319  
   1.320 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
   1.321 -      "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
   1.322 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))"
   1.323 +      "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))"
   1.324  nitpick [expect = none]
   1.325  by auto
   1.326  
   1.327 @@ -796,7 +756,7 @@
   1.328  by auto
   1.329  
   1.330  lemma "((x, x), (x, x)) \<in> rtrancl {}"
   1.331 -nitpick [expect = none]
   1.332 +nitpick [card = 1\<midarrow>5, expect = none]
   1.333  by auto
   1.334  
   1.335  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
   1.336 @@ -931,9 +891,8 @@
   1.337  oops
   1.338  
   1.339  lemma "P x \<Longrightarrow> P (The P)"
   1.340 -nitpick [card = 1, expect = none]
   1.341  nitpick [card = 1\<midarrow>2, expect = none]
   1.342 -nitpick [card = 3\<midarrow>5, expect = genuine]
   1.343 +nitpick [card = 3, expect = genuine]
   1.344  nitpick [card = 8, expect = genuine]
   1.345  oops
   1.346