src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 33197 de6285ebcc05
child 33199 6c9b2a94a69c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     1.3 @@ -0,0 +1,1123 @@
     1.4 +(*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2009
     1.7 +
     1.8 +Examples featuring Nitpick's functional core.
     1.9 +*)
    1.10 +
    1.11 +header {* Examples Featuring Nitpick's Functional Core *}
    1.12 +
    1.13 +theory Core_Nits
    1.14 +imports Main
    1.15 +begin
    1.16 +
    1.17 +subsection {* Curry in a Hurry *}
    1.18 +
    1.19 +lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    1.20 +nitpick [card = 1\<midarrow>4, expect = none]
    1.21 +nitpick [card = 100, expect = none, timeout = none]
    1.22 +by auto
    1.23 +
    1.24 +lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    1.25 +nitpick [card = 2]
    1.26 +nitpick [card = 1\<midarrow>4, expect = none]
    1.27 +nitpick [card = 10, expect = none]
    1.28 +by auto
    1.29 +
    1.30 +lemma "split (curry f) = f"
    1.31 +nitpick [card = 1\<midarrow>4, expect = none]
    1.32 +nitpick [card = 10, expect = none]
    1.33 +nitpick [card = 40, expect = none]
    1.34 +by auto
    1.35 +
    1.36 +lemma "curry (split f) = f"
    1.37 +nitpick [card = 1\<midarrow>4, expect = none]
    1.38 +nitpick [card = 40, expect = none]
    1.39 +by auto
    1.40 +
    1.41 +lemma "(split o curry) f = f"
    1.42 +nitpick [card = 1\<midarrow>4, expect = none]
    1.43 +nitpick [card = 40, expect = none]
    1.44 +by auto
    1.45 +
    1.46 +lemma "(curry o split) f = f"
    1.47 +nitpick [card = 1\<midarrow>4, expect = none]
    1.48 +nitpick [card = 1000, 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 +by auto
    1.55 +
    1.56 +lemma "(curry o split) f = (\<lambda>x. x) f"
    1.57 +nitpick [card = 1\<midarrow>4, expect = none]
    1.58 +nitpick [card = 40, expect = none]
    1.59 +by auto
    1.60 +
    1.61 +lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    1.62 +nitpick [card = 1\<midarrow>4, expect = none]
    1.63 +nitpick [card = 40, expect = none]
    1.64 +by auto
    1.65 +
    1.66 +lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    1.67 +nitpick [card = 1\<midarrow>4, expect = none]
    1.68 +nitpick [card = 1000, expect = none]
    1.69 +by auto
    1.70 +
    1.71 +lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    1.72 +nitpick [card = 1\<midarrow>4, expect = none]
    1.73 +nitpick [card = 1000, expect = none]
    1.74 +by auto
    1.75 +
    1.76 +lemma "split o curry = (\<lambda>x. x)"
    1.77 +nitpick [card = 1\<midarrow>4, expect = none]
    1.78 +nitpick [card = 40, expect = none]
    1.79 +apply (rule ext)+
    1.80 +by auto
    1.81 +
    1.82 +lemma "curry o split = (\<lambda>x. x)"
    1.83 +nitpick [card = 1\<midarrow>4, expect = none]
    1.84 +nitpick [card = 100, expect = none]
    1.85 +apply (rule ext)+
    1.86 +by auto
    1.87 +
    1.88 +lemma "split (\<lambda>x y. f (x, y)) = f"
    1.89 +nitpick [card = 1\<midarrow>4, expect = none]
    1.90 +nitpick [card = 40, expect = none]
    1.91 +by auto
    1.92 +
    1.93 +subsection {* Representations *}
    1.94 +
    1.95 +lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
    1.96 +nitpick [expect = none]
    1.97 +by auto
    1.98 +
    1.99 +lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   1.100 +nitpick [card 'a = 35, card 'b = 34, expect = genuine]
   1.101 +nitpick [card = 1\<midarrow>15, mono, expect = none]
   1.102 +oops
   1.103 +
   1.104 +lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
   1.105 +nitpick [card = 1, expect = genuine]
   1.106 +nitpick [card = 2, expect = genuine]
   1.107 +nitpick [card = 5, expect = genuine]
   1.108 +oops
   1.109 +
   1.110 +lemma "P (\<lambda>x. x)"
   1.111 +nitpick [card = 1, expect = genuine]
   1.112 +nitpick [card = 5, expect = genuine]
   1.113 +oops
   1.114 +
   1.115 +lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
   1.116 +nitpick [card = 1\<midarrow>6, expect = none]
   1.117 +nitpick [card = 20, expect = none]
   1.118 +by auto
   1.119 +
   1.120 +lemma "fst (a, b) = a"
   1.121 +nitpick [card = 1\<midarrow>20, expect = none]
   1.122 +by auto
   1.123 +
   1.124 +lemma "\<exists>P. P = Id"
   1.125 +nitpick [card = 1\<midarrow>4, expect = none]
   1.126 +by auto
   1.127 +
   1.128 +lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
   1.129 +nitpick [card = 1\<midarrow>3, expect = none]
   1.130 +by auto
   1.131 +
   1.132 +lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
   1.133 +nitpick [card = 1\<midarrow>6, expect = none]
   1.134 +by auto
   1.135 +
   1.136 +lemma "Id (a, a)"
   1.137 +nitpick [card = 1\<midarrow>100, expect = none]
   1.138 +by (auto simp: Id_def Collect_def)
   1.139 +
   1.140 +lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
   1.141 +nitpick [card = 1\<midarrow>20, expect = none]
   1.142 +by (auto simp: Id_def Collect_def)
   1.143 +
   1.144 +lemma "UNIV (x\<Colon>'a\<times>'a)"
   1.145 +nitpick [card = 1\<midarrow>50, expect = none]
   1.146 +sorry
   1.147 +
   1.148 +lemma "{} = A - A"
   1.149 +nitpick [card = 1\<midarrow>100, expect = none]
   1.150 +by auto
   1.151 +
   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 +oops
   1.157 +
   1.158 +lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
   1.159 +nitpick [expect = none]
   1.160 +by auto
   1.161 +
   1.162 +lemma "A \<subseteq> B"
   1.163 +nitpick [card = 100, expect = genuine]
   1.164 +oops
   1.165 +
   1.166 +lemma "A = {b}"
   1.167 +nitpick [card = 100, expect = genuine]
   1.168 +oops
   1.169 +
   1.170 +lemma "{a, b} = {b}"
   1.171 +nitpick [card = 100, expect = genuine]
   1.172 +oops
   1.173 +
   1.174 +lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
   1.175 +nitpick [card = 1, expect = genuine]
   1.176 +nitpick [card = 2, expect = genuine]
   1.177 +nitpick [card = 4, expect = genuine]
   1.178 +nitpick [card = 20, expect = genuine]
   1.179 +nitpick [card = 10, dont_box, expect = genuine]
   1.180 +oops
   1.181 +
   1.182 +lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
   1.183 +nitpick [card = 3, expect = genuine]
   1.184 +nitpick [card = 3, dont_box, expect = genuine]
   1.185 +nitpick [card = 5, expect = genuine]
   1.186 +nitpick [card = 10, expect = genuine]
   1.187 +oops
   1.188 +
   1.189 +lemma "f (a, b) = x"
   1.190 +nitpick [card = 3, expect = genuine]
   1.191 +nitpick [card = 10, expect = genuine]
   1.192 +nitpick [card = 16, expect = genuine]
   1.193 +nitpick [card = 30, expect = genuine]
   1.194 +oops
   1.195 +
   1.196 +lemma "f (a, a) = f (c, d)"
   1.197 +nitpick [card = 4, expect = genuine]
   1.198 +nitpick [card = 20, expect = genuine]
   1.199 +oops
   1.200 +
   1.201 +lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
   1.202 +nitpick [card = 2, expect = none]
   1.203 +by auto
   1.204 +
   1.205 +lemma "\<exists>F. F a b = G a b"
   1.206 +nitpick [card = 3, expect = none]
   1.207 +by auto
   1.208 +
   1.209 +lemma "f = split"
   1.210 +nitpick [card = 1, expect = none]
   1.211 +nitpick [card = 2, expect = genuine]
   1.212 +oops
   1.213 +
   1.214 +lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
   1.215 +nitpick [card = 20, expect = none]
   1.216 +by auto
   1.217 +
   1.218 +lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   1.219 +       A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
   1.220 +nitpick [card = 1\<midarrow>50, expect = none]
   1.221 +by auto
   1.222 +
   1.223 +lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
   1.224 +nitpick [card = 3, expect = genuine]
   1.225 +nitpick [card = 4, expect = genuine]
   1.226 +nitpick [card = 8, expect = genuine]
   1.227 +oops
   1.228 +
   1.229 +subsection {* Quantifiers *}
   1.230 +
   1.231 +lemma "x = y"
   1.232 +nitpick [card 'a = 1, expect = none]
   1.233 +nitpick [card 'a = 2, expect = genuine]
   1.234 +nitpick [card 'a = 100, expect = genuine]
   1.235 +nitpick [card 'a = 1000, expect = genuine]
   1.236 +oops
   1.237 +
   1.238 +lemma "\<forall>x. x = y"
   1.239 +nitpick [card 'a = 1, expect = none]
   1.240 +nitpick [card 'a = 2, expect = genuine]
   1.241 +nitpick [card 'a = 100, expect = genuine]
   1.242 +nitpick [card 'a = 1000, expect = genuine]
   1.243 +oops
   1.244 +
   1.245 +lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   1.246 +nitpick [card 'a = 1, expect = genuine]
   1.247 +nitpick [card 'a = 2, expect = genuine]
   1.248 +nitpick [card 'a = 100, expect = genuine]
   1.249 +nitpick [card 'a = 1000, expect = genuine]
   1.250 +oops
   1.251 +
   1.252 +lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   1.253 +nitpick [card 'a = 1\<midarrow>10, expect = none]
   1.254 +by auto
   1.255 +
   1.256 +lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   1.257 +nitpick [card = 1\<midarrow>40, expect = none]
   1.258 +by auto
   1.259 +
   1.260 +lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   1.261 +nitpick [card = 1\<midarrow>5, expect = none]
   1.262 +by auto
   1.263 +
   1.264 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   1.265 +nitpick [card = 1\<midarrow>5, expect = none]
   1.266 +by auto
   1.267 +
   1.268 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
   1.269 +nitpick [card = 1\<midarrow>2, expect = genuine]
   1.270 +nitpick [card = 3, expect = genuine]
   1.271 +oops
   1.272 +
   1.273 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   1.274 +       f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   1.275 +nitpick [card = 1\<midarrow>2, expect = none]
   1.276 +nitpick [card = 3, expect = none]
   1.277 +nitpick [card = 4, expect = none]
   1.278 +sorry
   1.279 +
   1.280 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   1.281 +       f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
   1.282 +nitpick [card = 1\<midarrow>2, expect = genuine]
   1.283 +oops
   1.284 +
   1.285 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   1.286 +       f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
   1.287 +nitpick [card = 1\<midarrow>2, expect = genuine]
   1.288 +oops
   1.289 +
   1.290 +lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   1.291 +       f u v w x = f u (g u) w (h u w)"
   1.292 +nitpick [card = 1\<midarrow>2, expect = none]
   1.293 +sorry
   1.294 +
   1.295 +lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   1.296 +       f u v w x = f u (g u w) w (h u)"
   1.297 +nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   1.298 +oops
   1.299 +
   1.300 +lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   1.301 +       f u v w x = f u (g u) w (h u w)"
   1.302 +nitpick [card = 1\<midarrow>2, dont_box, expect = none]
   1.303 +sorry
   1.304 +
   1.305 +lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   1.306 +       f u v w x = f u (g u w) w (h u)"
   1.307 +nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   1.308 +oops
   1.309 +
   1.310 +lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
   1.311 +nitpick [card = 1, expect = genuine]
   1.312 +nitpick [card = 2\<midarrow>5, expect = none]
   1.313 +oops
   1.314 +
   1.315 +lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
   1.316 +nitpick [card = 1, expect = genuine]
   1.317 +nitpick [card = 2, expect = none]
   1.318 +oops
   1.319 +
   1.320 +lemma "\<forall>x. if (\<exists>y. x = y) then True else False"
   1.321 +nitpick [expect = none]
   1.322 +sorry
   1.323 +
   1.324 +lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
   1.325 +nitpick [expect = none]
   1.326 +sorry
   1.327 +
   1.328 +lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   1.329 +nitpick [expect = none]
   1.330 +by auto
   1.331 +
   1.332 +lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   1.333 +nitpick [expect = none]
   1.334 +by auto
   1.335 +
   1.336 +lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   1.337 +nitpick [card 'a = 1, expect = genuine]
   1.338 +nitpick [card 'a = 2, expect = genuine]
   1.339 +nitpick [card 'a = 3, expect = genuine]
   1.340 +nitpick [card 'a = 4, expect = genuine]
   1.341 +nitpick [card 'a = 5, expect = genuine]
   1.342 +oops
   1.343 +
   1.344 +lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
   1.345 +           else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   1.346 +nitpick [expect = none]
   1.347 +by auto
   1.348 +
   1.349 +lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x)
   1.350 +           else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   1.351 +nitpick [expect = none]
   1.352 +by auto
   1.353 +
   1.354 +lemma "let x = (\<forall>x. P x) in if x then x else \<not> x"
   1.355 +nitpick [expect = none]
   1.356 +by auto
   1.357 +
   1.358 +lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x"
   1.359 +nitpick [expect = none]
   1.360 +by auto
   1.361 +
   1.362 +subsection {* Schematic Variables *}
   1.363 +
   1.364 +lemma "x = ?x"
   1.365 +nitpick [expect = none]
   1.366 +by auto
   1.367 +
   1.368 +lemma "\<forall>x. x = ?x"
   1.369 +nitpick [expect = genuine]
   1.370 +oops
   1.371 +
   1.372 +lemma "\<exists>x. x = ?x"
   1.373 +nitpick [expect = none]
   1.374 +by auto
   1.375 +
   1.376 +lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
   1.377 +nitpick [expect = none]
   1.378 +by auto
   1.379 +
   1.380 +lemma "\<forall>x. ?x = ?y"
   1.381 +nitpick [expect = none]
   1.382 +by auto
   1.383 +
   1.384 +lemma "\<exists>x. ?x = ?y"
   1.385 +nitpick [expect = none]
   1.386 +by auto
   1.387 +
   1.388 +subsection {* Known Constants *}
   1.389 +
   1.390 +lemma "x \<equiv> all \<Longrightarrow> False"
   1.391 +nitpick [card = 1, expect = genuine]
   1.392 +nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   1.393 +nitpick [card = 2, expect = genuine]
   1.394 +nitpick [card = 8, expect = genuine]
   1.395 +nitpick [card = 10, expect = unknown]
   1.396 +oops
   1.397 +
   1.398 +lemma "\<And>x. f x y = f x y"
   1.399 +nitpick [expect = none]
   1.400 +oops
   1.401 +
   1.402 +lemma "\<And>x. f x y = f y x"
   1.403 +nitpick [expect = genuine]
   1.404 +oops
   1.405 +
   1.406 +lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   1.407 +nitpick [expect = none]
   1.408 +by auto
   1.409 +
   1.410 +lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   1.411 +nitpick [expect = genuine]
   1.412 +oops
   1.413 +
   1.414 +lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
   1.415 +nitpick [expect = none]
   1.416 +by auto
   1.417 +
   1.418 +lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
   1.419 +nitpick [card = 1, expect = genuine]
   1.420 +nitpick [card = 2, expect = genuine]
   1.421 +nitpick [card = 3, expect = genuine]
   1.422 +nitpick [card = 4, expect = genuine]
   1.423 +nitpick [card = 5, expect = genuine]
   1.424 +nitpick [card = 100, expect = genuine]
   1.425 +oops
   1.426 +
   1.427 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   1.428 +nitpick [expect = none]
   1.429 +by auto
   1.430 +
   1.431 +lemma "P x \<equiv> P x"
   1.432 +nitpick [card = 1\<midarrow>10, expect = none]
   1.433 +by auto
   1.434 +
   1.435 +lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
   1.436 +nitpick [card = 1\<midarrow>10, expect = none]
   1.437 +by auto
   1.438 +
   1.439 +lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
   1.440 +nitpick [card = 1\<midarrow>10, expect = none]
   1.441 +by auto
   1.442 +
   1.443 +lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
   1.444 +nitpick [expect = genuine]
   1.445 +oops
   1.446 +
   1.447 +lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))"
   1.448 +nitpick [expect = none]
   1.449 +by auto
   1.450 +
   1.451 +lemma "P x \<Longrightarrow> P x"
   1.452 +nitpick [card = 1\<midarrow>10, expect = none]
   1.453 +by auto
   1.454 +
   1.455 +lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
   1.456 +nitpick [expect = none]
   1.457 +by auto
   1.458 +
   1.459 +lemma "True \<Longrightarrow> False"
   1.460 +nitpick [expect = genuine]
   1.461 +oops
   1.462 +
   1.463 +lemma "x = Not"
   1.464 +nitpick [expect = genuine]
   1.465 +oops
   1.466 +
   1.467 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))"
   1.468 +nitpick [expect = none]
   1.469 +by auto
   1.470 +
   1.471 +lemma "x = True"
   1.472 +nitpick [expect = genuine]
   1.473 +oops
   1.474 +
   1.475 +lemma "x = False"
   1.476 +nitpick [expect = genuine]
   1.477 +oops
   1.478 +
   1.479 +lemma "x = undefined"
   1.480 +nitpick [expect = genuine]
   1.481 +oops
   1.482 +
   1.483 +lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined"
   1.484 +nitpick [expect = genuine]
   1.485 +oops
   1.486 +
   1.487 +lemma "undefined = undefined"
   1.488 +nitpick [expect = none]
   1.489 +by auto
   1.490 +
   1.491 +lemma "f undefined = f undefined"
   1.492 +nitpick [expect = none]
   1.493 +by auto
   1.494 +
   1.495 +lemma "f undefined = g undefined"
   1.496 +nitpick [card = 33, expect = genuine]
   1.497 +oops
   1.498 +
   1.499 +lemma "\<exists>!x. x = undefined"
   1.500 +nitpick [card = 30, expect = none]
   1.501 +by auto
   1.502 +
   1.503 +lemma "x = All \<Longrightarrow> False"
   1.504 +nitpick [card = 1, dont_box, expect = genuine]
   1.505 +nitpick [card = 2, dont_box, expect = genuine]
   1.506 +nitpick [card = 8, dont_box, expect = genuine]
   1.507 +nitpick [card = 10, dont_box, expect = unknown]
   1.508 +oops
   1.509 +
   1.510 +lemma "\<forall>x. f x y = f x y"
   1.511 +nitpick [expect = none]
   1.512 +oops
   1.513 +
   1.514 +lemma "\<forall>x. f x y = f y x"
   1.515 +nitpick [expect = genuine]
   1.516 +oops
   1.517 +
   1.518 +lemma "All (\<lambda>x. f x y = f x y) = True"
   1.519 +nitpick [expect = none]
   1.520 +by auto
   1.521 +
   1.522 +lemma "All (\<lambda>x. f x y = f x y) = False"
   1.523 +nitpick [expect = genuine]
   1.524 +oops
   1.525 +
   1.526 +lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
   1.527 +nitpick [expect = none]
   1.528 +by auto
   1.529 +
   1.530 +lemma "x = Ex \<Longrightarrow> False"
   1.531 +nitpick [card = 1, dont_box, expect = genuine]
   1.532 +nitpick [card = 2, dont_box, expect = genuine]
   1.533 +nitpick [card = 8, dont_box, expect = genuine]
   1.534 +nitpick [card = 10, dont_box, expect = unknown]
   1.535 +oops
   1.536 +
   1.537 +lemma "\<exists>x. f x y = f x y"
   1.538 +nitpick [expect = none]
   1.539 +oops
   1.540 +
   1.541 +lemma "\<exists>x. f x y = f y x"
   1.542 +nitpick [expect = none]
   1.543 +oops
   1.544 +
   1.545 +lemma "Ex (\<lambda>x. f x y = f x y) = True"
   1.546 +nitpick [expect = none]
   1.547 +by auto
   1.548 +
   1.549 +lemma "Ex (\<lambda>x. f x y = f y x) = True"
   1.550 +nitpick [expect = none]
   1.551 +by auto
   1.552 +
   1.553 +lemma "Ex (\<lambda>x. f x y = f x y) = False"
   1.554 +nitpick [expect = genuine]
   1.555 +oops
   1.556 +
   1.557 +lemma "Ex (\<lambda>x. f x y = f y x) = False"
   1.558 +nitpick [expect = genuine]
   1.559 +oops
   1.560 +
   1.561 +lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
   1.562 +nitpick [expect = none]
   1.563 +by auto
   1.564 +
   1.565 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))"
   1.566 +nitpick [expect = none]
   1.567 +by auto
   1.568 +
   1.569 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
   1.570 +      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
   1.571 +nitpick [expect = none]
   1.572 +by auto
   1.573 +
   1.574 +lemma "x = y \<Longrightarrow> y = x"
   1.575 +nitpick [expect = none]
   1.576 +by auto
   1.577 +
   1.578 +lemma "x = y \<Longrightarrow> f x = f y"
   1.579 +nitpick [expect = none]
   1.580 +by auto
   1.581 +
   1.582 +lemma "x = y \<and> y = z \<Longrightarrow> x = z"
   1.583 +nitpick [expect = none]
   1.584 +by auto
   1.585 +
   1.586 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
   1.587 +      "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
   1.588 +nitpick [expect = none]
   1.589 +by auto
   1.590 +
   1.591 +lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
   1.592 +nitpick [expect = none]
   1.593 +by auto
   1.594 +
   1.595 +lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b"
   1.596 +nitpick [expect = none]
   1.597 +by auto
   1.598 +
   1.599 +lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
   1.600 +nitpick [expect = none]
   1.601 +by auto
   1.602 +
   1.603 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
   1.604 +      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
   1.605 +nitpick [expect = none]
   1.606 +by auto
   1.607 +
   1.608 +lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
   1.609 +nitpick [expect = none]
   1.610 +by auto
   1.611 +
   1.612 +lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
   1.613 +nitpick [expect = none]
   1.614 +by auto
   1.615 +
   1.616 +lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
   1.617 +nitpick [expect = none]
   1.618 +by auto
   1.619 +
   1.620 +lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
   1.621 +nitpick [expect = none]
   1.622 +by auto
   1.623 +
   1.624 +lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
   1.625 +nitpick [expect = none]
   1.626 +by auto
   1.627 +
   1.628 +lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
   1.629 +nitpick [expect = none]
   1.630 +by auto
   1.631 +
   1.632 +lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))"
   1.633 +nitpick [expect = none]
   1.634 +by auto
   1.635 +
   1.636 +lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
   1.637 +      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
   1.638 +      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
   1.639 +nitpick [expect = none]
   1.640 +by auto
   1.641 +
   1.642 +lemma "fst (x, y) = x"
   1.643 +nitpick [expect = none]
   1.644 +by (simp add: fst_def)
   1.645 +
   1.646 +lemma "snd (x, y) = y"
   1.647 +nitpick [expect = none]
   1.648 +by (simp add: snd_def)
   1.649 +
   1.650 +lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x"
   1.651 +nitpick [expect = none]
   1.652 +by (simp add: fst_def)
   1.653 +
   1.654 +lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y"
   1.655 +nitpick [expect = none]
   1.656 +by (simp add: snd_def)
   1.657 +
   1.658 +lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x"
   1.659 +nitpick [expect = none]
   1.660 +by (simp add: fst_def)
   1.661 +
   1.662 +lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y"
   1.663 +nitpick [expect = none]
   1.664 +by (simp add: snd_def)
   1.665 +
   1.666 +lemma "fst (x\<Colon>'a\<times>'b, y) = x"
   1.667 +nitpick [expect = none]
   1.668 +by (simp add: fst_def)
   1.669 +
   1.670 +lemma "snd (x\<Colon>'a\<times>'b, y) = y"
   1.671 +nitpick [expect = none]
   1.672 +by (simp add: snd_def)
   1.673 +
   1.674 +lemma "fst (x, y\<Colon>'a\<times>'b) = x"
   1.675 +nitpick [expect = none]
   1.676 +by (simp add: fst_def)
   1.677 +
   1.678 +lemma "snd (x, y\<Colon>'a\<times>'b) = y"
   1.679 +nitpick [expect = none]
   1.680 +by (simp add: snd_def)
   1.681 +
   1.682 +lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
   1.683 +nitpick [expect = none]
   1.684 +by (simp add: fst_def)
   1.685 +
   1.686 +lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
   1.687 +nitpick [expect = none]
   1.688 +by (simp add: snd_def)
   1.689 +
   1.690 +lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
   1.691 +nitpick [expect = none]
   1.692 +by auto
   1.693 +
   1.694 +lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
   1.695 +nitpick [expect = none]
   1.696 +by auto
   1.697 +
   1.698 +lemma "fst (x, y) = snd (y, x)"
   1.699 +nitpick [expect = none]
   1.700 +by auto
   1.701 +
   1.702 +lemma "(x, x) \<in> Id"
   1.703 +nitpick [expect = none]
   1.704 +by auto
   1.705 +
   1.706 +lemma "(x, y) \<in> Id \<Longrightarrow> x = y"
   1.707 +nitpick [expect = none]
   1.708 +by auto
   1.709 +
   1.710 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
   1.711 +nitpick [expect = none]
   1.712 +by auto
   1.713 +
   1.714 +lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
   1.715 +nitpick [expect = none]
   1.716 +by (simp add: curry_def)
   1.717 +
   1.718 +lemma "{} = (\<lambda>x. False)"
   1.719 +nitpick [expect = none]
   1.720 +by (metis Collect_def bot_set_eq empty_def)
   1.721 +
   1.722 +lemma "x \<in> {}"
   1.723 +nitpick [expect = genuine]
   1.724 +oops
   1.725 +
   1.726 +lemma "{a, b} = {b}"
   1.727 +nitpick [expect = genuine]
   1.728 +oops
   1.729 +
   1.730 +lemma "{a, b} \<noteq> {b}"
   1.731 +nitpick [expect = genuine]
   1.732 +oops
   1.733 +
   1.734 +lemma "{a} = {b}"
   1.735 +nitpick [expect = genuine]
   1.736 +oops
   1.737 +
   1.738 +lemma "{a} \<noteq> {b}"
   1.739 +nitpick [expect = genuine]
   1.740 +oops
   1.741 +
   1.742 +lemma "{a, b, c} = {c, b, a}"
   1.743 +nitpick [expect = none]
   1.744 +by auto
   1.745 +
   1.746 +lemma "UNIV = (\<lambda>x. True)"
   1.747 +nitpick [expect = none]
   1.748 +by (simp only: UNIV_def Collect_def)
   1.749 +
   1.750 +lemma "UNIV x = True"
   1.751 +nitpick [expect = none]
   1.752 +by (simp only: UNIV_def Collect_def)
   1.753 +
   1.754 +lemma "x \<notin> UNIV"
   1.755 +nitpick [expect = genuine]
   1.756 +oops
   1.757 +
   1.758 +lemma "op \<in> = (\<lambda>x P. P x)"
   1.759 +nitpick [expect = none]
   1.760 +apply (rule ext)
   1.761 +apply (rule ext)
   1.762 +by (simp add: mem_def)
   1.763 +
   1.764 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
   1.765 +nitpick [expect = none]
   1.766 +apply (rule ext)
   1.767 +apply (rule ext)
   1.768 +by (simp add: mem_def)
   1.769 +
   1.770 +lemma "P x = (x \<in> P)"
   1.771 +nitpick [expect = none]
   1.772 +by (simp add: mem_def)
   1.773 +
   1.774 +lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
   1.775 +nitpick [expect = none]
   1.776 +by simp
   1.777 +
   1.778 +lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
   1.779 +nitpick [expect = none]
   1.780 +by simp
   1.781 +
   1.782 +lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
   1.783 +nitpick [card = 1\<midarrow>2, expect = none]
   1.784 +by auto
   1.785 +
   1.786 +lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
   1.787 +nitpick [card = 1\<midarrow>3, expect = none]
   1.788 +apply (rule ext)
   1.789 +by auto
   1.790 +
   1.791 +lemma "(x, x) \<in> rtrancl {(y, y)}"
   1.792 +nitpick [expect = none]
   1.793 +by auto
   1.794 +
   1.795 +lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
   1.796 +nitpick [card = 1\<midarrow>2, expect = none]
   1.797 +by auto
   1.798 +
   1.799 +lemma "((x, x), (x, x)) \<in> rtrancl {}"
   1.800 +nitpick [expect = none]
   1.801 +by auto
   1.802 +
   1.803 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
   1.804 +nitpick [card = 1\<midarrow>5, expect = none]
   1.805 +by auto
   1.806 +
   1.807 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
   1.808 +nitpick [card = 1\<midarrow>5, expect = none]
   1.809 +by auto
   1.810 +
   1.811 +lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
   1.812 +nitpick [expect = none]
   1.813 +by auto
   1.814 +
   1.815 +lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
   1.816 +nitpick [expect = none]
   1.817 +by auto
   1.818 +
   1.819 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
   1.820 +nitpick [card = 1\<midarrow>5, expect = none]
   1.821 +by auto
   1.822 +
   1.823 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
   1.824 +nitpick [card = 1\<midarrow>5, expect = none]
   1.825 +by auto
   1.826 +
   1.827 +lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
   1.828 +nitpick [card = 1\<midarrow>5, expect = none]
   1.829 +by auto
   1.830 +
   1.831 +lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
   1.832 +nitpick [expect = none]
   1.833 +by auto
   1.834 +
   1.835 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
   1.836 +nitpick [card = 1\<midarrow>5, expect = none]
   1.837 +by auto
   1.838 +
   1.839 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
   1.840 +nitpick [card = 1\<midarrow>5, expect = none]
   1.841 +by auto
   1.842 +
   1.843 +lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
   1.844 +nitpick [card = 1\<midarrow>5, expect = none]
   1.845 +by auto
   1.846 +
   1.847 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
   1.848 +nitpick [card = 1\<midarrow>5, expect = none]
   1.849 +by auto
   1.850 +
   1.851 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
   1.852 +nitpick [card = 1\<midarrow>5, expect = none]
   1.853 +by auto
   1.854 +
   1.855 +lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
   1.856 +nitpick [card = 1\<midarrow>5, expect = none]
   1.857 +by auto
   1.858 +
   1.859 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
   1.860 +nitpick [card = 1\<midarrow>5, expect = none]
   1.861 +by auto
   1.862 +
   1.863 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
   1.864 +nitpick [card = 1\<midarrow>5, expect = none]
   1.865 +by auto
   1.866 +
   1.867 +lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
   1.868 +nitpick [card = 1\<midarrow>5, expect = none]
   1.869 +by auto
   1.870 +
   1.871 +lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
   1.872 +nitpick [card = 5, expect = genuine]
   1.873 +oops
   1.874 +
   1.875 +lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B"
   1.876 +nitpick [expect = none]
   1.877 +by auto
   1.878 +
   1.879 +lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
   1.880 +nitpick [expect = none]
   1.881 +by auto
   1.882 +
   1.883 +lemma "A \<union> - A = UNIV"
   1.884 +nitpick [expect = none]
   1.885 +by auto
   1.886 +
   1.887 +lemma "A \<inter> - A = {}"
   1.888 +nitpick [expect = none]
   1.889 +by auto
   1.890 +
   1.891 +lemma "A = -(A\<Colon>'a set)"
   1.892 +nitpick [card 'a = 10, expect = genuine]
   1.893 +oops
   1.894 +
   1.895 +lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
   1.896 +nitpick [expect = none]
   1.897 +oops
   1.898 +
   1.899 +lemma "finite A"
   1.900 +nitpick [expect = none]
   1.901 +oops
   1.902 +
   1.903 +lemma "finite A \<Longrightarrow> finite B"
   1.904 +nitpick [expect = none]
   1.905 +oops
   1.906 +
   1.907 +lemma "All finite"
   1.908 +nitpick [expect = none]
   1.909 +oops
   1.910 +
   1.911 +subsection {* The and Eps *}
   1.912 +
   1.913 +lemma "x = The"
   1.914 +nitpick [card = 5, expect = genuine]
   1.915 +oops
   1.916 +
   1.917 +lemma "\<exists>x. x = The"
   1.918 +nitpick [card = 1\<midarrow>3]
   1.919 +by auto
   1.920 +
   1.921 +lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
   1.922 +nitpick [expect = none]
   1.923 +by auto
   1.924 +
   1.925 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z"
   1.926 +nitpick [expect = genuine]
   1.927 +oops
   1.928 +
   1.929 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
   1.930 +nitpick [card = 2, expect = none]
   1.931 +nitpick [card = 3\<midarrow>5, expect = genuine]
   1.932 +oops
   1.933 +
   1.934 +lemma "P x \<Longrightarrow> P (The P)"
   1.935 +nitpick [card = 1, expect = none]
   1.936 +nitpick [card = 1\<midarrow>2, expect = none]
   1.937 +nitpick [card = 3\<midarrow>5, expect = genuine]
   1.938 +nitpick [card = 8, expect = genuine]
   1.939 +oops
   1.940 +
   1.941 +lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
   1.942 +nitpick [expect = genuine]
   1.943 +oops
   1.944 +
   1.945 +lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
   1.946 +nitpick [card = 1\<midarrow>5, expect = none]
   1.947 +by auto
   1.948 +
   1.949 +lemma "x = Eps"
   1.950 +nitpick [card = 5, expect = genuine]
   1.951 +oops
   1.952 +
   1.953 +lemma "\<exists>x. x = Eps"
   1.954 +nitpick [card = 1\<midarrow>3, expect = none]
   1.955 +by auto
   1.956 +
   1.957 +lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
   1.958 +nitpick [expect = none]
   1.959 +by auto
   1.960 +
   1.961 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z"
   1.962 +nitpick [expect = genuine]
   1.963 +apply auto
   1.964 +oops
   1.965 +
   1.966 +lemma "P x \<Longrightarrow> P (Eps P)"
   1.967 +nitpick [card = 1\<midarrow>8, expect = none]
   1.968 +by (metis exE_some)
   1.969 +
   1.970 +lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
   1.971 +nitpick [expect = genuine]
   1.972 +oops
   1.973 +
   1.974 +lemma "P (Eps P)"
   1.975 +nitpick [expect = genuine]
   1.976 +oops
   1.977 +
   1.978 +lemma "(P\<Colon>nat set) (Eps P)"
   1.979 +nitpick [expect = genuine]
   1.980 +oops
   1.981 +
   1.982 +lemma "\<not> P (Eps P)"
   1.983 +nitpick [expect = genuine]
   1.984 +oops
   1.985 +
   1.986 +lemma "\<not> (P\<Colon>nat set) (Eps P)"
   1.987 +nitpick [expect = genuine]
   1.988 +oops
   1.989 +
   1.990 +lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
   1.991 +nitpick [expect = none]
   1.992 +sorry
   1.993 +
   1.994 +lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
   1.995 +nitpick [expect = none]
   1.996 +sorry
   1.997 +
   1.998 +lemma "P (The P)"
   1.999 +nitpick [expect = genuine]
  1.1000 +oops
  1.1001 +
  1.1002 +lemma "(P\<Colon>nat set) (The P)"
  1.1003 +nitpick [expect = genuine]
  1.1004 +oops
  1.1005 +
  1.1006 +lemma "\<not> P (The P)"
  1.1007 +nitpick [expect = genuine]
  1.1008 +oops
  1.1009 +
  1.1010 +lemma "\<not> (P\<Colon>nat set) (The P)"
  1.1011 +nitpick [expect = genuine]
  1.1012 +oops
  1.1013 +
  1.1014 +lemma "The P \<noteq> x"
  1.1015 +nitpick [expect = genuine]
  1.1016 +oops
  1.1017 +
  1.1018 +lemma "The P \<noteq> (x\<Colon>nat)"
  1.1019 +nitpick [expect = genuine]
  1.1020 +oops
  1.1021 +
  1.1022 +lemma "P x \<Longrightarrow> P (The P)"
  1.1023 +nitpick [expect = genuine]
  1.1024 +oops
  1.1025 +
  1.1026 +lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)"
  1.1027 +nitpick [expect = genuine]
  1.1028 +oops
  1.1029 +
  1.1030 +lemma "P = {x} \<Longrightarrow> P (The P)"
  1.1031 +nitpick [expect = none]
  1.1032 +oops
  1.1033 +
  1.1034 +lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
  1.1035 +nitpick [expect = none]
  1.1036 +oops
  1.1037 +
  1.1038 +consts Q :: 'a
  1.1039 +
  1.1040 +lemma "Q (Eps Q)"
  1.1041 +nitpick [expect = genuine]
  1.1042 +oops
  1.1043 +
  1.1044 +lemma "(Q\<Colon>nat set) (Eps Q)"
  1.1045 +nitpick [expect = none]
  1.1046 +oops
  1.1047 +
  1.1048 +lemma "\<not> Q (Eps Q)"
  1.1049 +nitpick [expect = genuine]
  1.1050 +oops
  1.1051 +
  1.1052 +lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
  1.1053 +nitpick [expect = genuine]
  1.1054 +oops
  1.1055 +
  1.1056 +lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
  1.1057 +nitpick [expect = none]
  1.1058 +sorry
  1.1059 +
  1.1060 +lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
  1.1061 +nitpick [expect = none]
  1.1062 +sorry
  1.1063 +
  1.1064 +lemma "Q (The Q)"
  1.1065 +nitpick [expect = genuine]
  1.1066 +oops
  1.1067 +
  1.1068 +lemma "(Q\<Colon>nat set) (The Q)"
  1.1069 +nitpick [expect = genuine]
  1.1070 +oops
  1.1071 +
  1.1072 +lemma "\<not> Q (The Q)"
  1.1073 +nitpick [expect = genuine]
  1.1074 +oops
  1.1075 +
  1.1076 +lemma "\<not> (Q\<Colon>nat set) (The Q)"
  1.1077 +nitpick [expect = genuine]
  1.1078 +oops
  1.1079 +
  1.1080 +lemma "The Q \<noteq> x"
  1.1081 +nitpick [expect = genuine]
  1.1082 +oops
  1.1083 +
  1.1084 +lemma "The Q \<noteq> (x\<Colon>nat)"
  1.1085 +nitpick [expect = genuine]
  1.1086 +oops
  1.1087 +
  1.1088 +lemma "Q x \<Longrightarrow> Q (The Q)"
  1.1089 +nitpick [expect = genuine]
  1.1090 +oops
  1.1091 +
  1.1092 +lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)"
  1.1093 +nitpick [expect = genuine]
  1.1094 +oops
  1.1095 +
  1.1096 +lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
  1.1097 +nitpick [expect = none]
  1.1098 +oops
  1.1099 +
  1.1100 +lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
  1.1101 +nitpick [expect = none]
  1.1102 +oops
  1.1103 +
  1.1104 +subsection {* Destructors and Recursors *}
  1.1105 +
  1.1106 +lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
  1.1107 +nitpick [card = 2, expect = none]
  1.1108 +by auto
  1.1109 +
  1.1110 +lemma "bool_rec x y True = x"
  1.1111 +nitpick [card = 2, expect = none]
  1.1112 +by auto
  1.1113 +
  1.1114 +lemma "bool_rec x y False = y"
  1.1115 +nitpick [card = 2, expect = none]
  1.1116 +by auto
  1.1117 +
  1.1118 +lemma "(x\<Colon>bool) = bool_rec x x True"
  1.1119 +nitpick [card = 2, expect = none]
  1.1120 +by auto
  1.1121 +
  1.1122 +lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"
  1.1123 +nitpick [expect = none]
  1.1124 +sorry
  1.1125 +
  1.1126 +end