Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 35284 9edc2bd6d2bd
parent 35078 6fd1052fe463
child 35386 45a4e19d3ebd
equal deleted inserted replaced
35283:7ae51d5ea05d 35284:9edc2bd6d2bd 
     9 
     9 
    10 theory Core_Nits
 
    10 theory Core_Nits
 
    11 imports Main
 
    11 imports Main
 
    12 begin
 
    12 begin
 
    13 
    13 
    14 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
    14 nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
 
       
    15                 timeout = 60 s]
 
    15 
    16 
    16 subsection {* Curry in a Hurry *}
 
    17 subsection {* Curry in a Hurry *}
 
    17 
    18 
    18 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
 
    19 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
 
    19 nitpick [card = 1\<midarrow>4, expect = none]
 
    20 nitpick [card = 1\<midarrow>12, expect = none]
 
    20 nitpick [card = 100, expect = none, timeout = none]
 
       
    21 by auto
 
    21 by auto
 
    22 
    22 
    23 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
 
    23 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
 
    24 nitpick [card = 2]
 
    24 nitpick [card = 1\<midarrow>12, expect = none]
 
    25 nitpick [card = 1\<midarrow>4, expect = none]
 
       
    26 nitpick [card = 10, expect = none]
 
       
    27 by auto
 
    25 by auto
 
    28 
    26 
    29 lemma "split (curry f) = f"
 
    27 lemma "split (curry f) = f"
 
    30 nitpick [card = 1\<midarrow>4, expect = none]
 
    28 nitpick [card = 1\<midarrow>12, expect = none]
 
    31 nitpick [card = 10, expect = none]
 
       
    32 nitpick [card = 40, expect = none]
 
       
    33 by auto
 
    29 by auto
 
    34 
    30 
    35 lemma "curry (split f) = f"
 
    31 lemma "curry (split f) = f"
 
    36 nitpick [card = 1\<midarrow>4, expect = none]
 
    32 nitpick [card = 1\<midarrow>12, expect = none]
 
    37 nitpick [card = 40, expect = none]
 
       
    38 by auto
 
    33 by auto
 
    39 
    34 
    40 lemma "(split o curry) f = f"
 
    35 lemma "(split o curry) f = f"
 
    41 nitpick [card = 1\<midarrow>4, expect = none]
 
    36 nitpick [card = 1\<midarrow>12, expect = none]
 
    42 nitpick [card = 40, expect = none]
 
       
    43 by auto
 
    37 by auto
 
    44 
    38 
    45 lemma "(curry o split) f = f"
 
    39 lemma "(curry o split) f = f"
 
    46 nitpick [card = 1\<midarrow>4, expect = none]
 
    40 nitpick [card = 1\<midarrow>12, expect = none]
 
    47 nitpick [card = 1000, expect = none]
 
       
    48 by auto
 
    41 by auto
 
    49 
    42 
    50 lemma "(split o curry) f = (\<lambda>x. x) f"
 
    43 lemma "(split o curry) f = (\<lambda>x. x) f"
 
    51 nitpick [card = 1\<midarrow>4, expect = none]
 
    44 nitpick [card = 1\<midarrow>12, expect = none]
 
    52 nitpick [card = 40, expect = none]
 
       
    53 by auto
 
    45 by auto
 
    54 
    46 
    55 lemma "(curry o split) f = (\<lambda>x. x) f"
 
    47 lemma "(curry o split) f = (\<lambda>x. x) f"
 
    56 nitpick [card = 1\<midarrow>4, expect = none]
 
    48 nitpick [card = 1\<midarrow>12, expect = none]
 
    57 nitpick [card = 40, expect = none]
 
       
    58 by auto
 
    49 by auto
 
    59 
    50 
    60 lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
 
    51 lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
 
    61 nitpick [card = 1\<midarrow>4, expect = none]
 
    52 nitpick [card = 1\<midarrow>12, expect = none]
 
    62 nitpick [card = 40, expect = none]
 
       
    63 by auto
 
    53 by auto
 
    64 
    54 
    65 lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
 
    55 lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
 
    66 nitpick [card = 1\<midarrow>4, expect = none]
 
    56 nitpick [card = 1\<midarrow>12, expect = none]
 
    67 nitpick [card = 1000, expect = none]
 
       
    68 by auto
 
    57 by auto
 
    69 
    58 
    70 lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
 
    59 lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
 
    71 nitpick [card = 1\<midarrow>4, expect = none]
 
    60 nitpick [card = 1\<midarrow>12, expect = none]
 
    72 nitpick [card = 1000, expect = none]
 
       
    73 by auto
 
    61 by auto
 
    74 
    62 
    75 lemma "split o curry = (\<lambda>x. x)"
 
    63 lemma "split o curry = (\<lambda>x. x)"
 
    76 nitpick [card = 1\<midarrow>4, expect = none]
 
    64 nitpick [card = 1\<midarrow>12, expect = none]
 
    77 nitpick [card = 40, expect = none]
 
       
    78 apply (rule ext)+
 
    65 apply (rule ext)+
 
    79 by auto
 
    66 by auto
 
    80 
    67 
    81 lemma "curry o split = (\<lambda>x. x)"
 
    68 lemma "curry o split = (\<lambda>x. x)"
 
    82 nitpick [card = 1\<midarrow>4, expect = none]
 
    69 nitpick [card = 1\<midarrow>12, expect = none]
 
    83 nitpick [card = 100, expect = none]
 
       
    84 apply (rule ext)+
 
    70 apply (rule ext)+
 
    85 by auto
 
    71 by auto
 
    86 
    72 
    87 lemma "split (\<lambda>x y. f (x, y)) = f"
 
    73 lemma "split (\<lambda>x y. f (x, y)) = f"
 
    88 nitpick [card = 1\<midarrow>4, expect = none]
 
    74 nitpick [card = 1\<midarrow>12, expect = none]
 
    89 nitpick [card = 40, expect = none]
 
       
    90 by auto
 
    75 by auto
 
    91 
    76 
    92 subsection {* Representations *}
 
    77 subsection {* Representations *}
 
    93 
    78 
    94 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
 
    79 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
 
    95 nitpick [expect = none]
 
    80 nitpick [expect = none]
 
    96 by auto
 
    81 by auto
 
    97 
    82 
    98 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
 
    83 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
 
    99 nitpick [card 'a = 35, card 'b = 34, expect = genuine]
 
    84 nitpick [card 'a = 25, card 'b = 24, expect = genuine]
 
   100 nitpick [card = 1\<midarrow>15, mono, expect = none]
 
    85 nitpick [card = 1\<midarrow>10, mono, expect = none]
 
   101 oops
 
    86 oops
 
   102 
    87 
   103 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
 
    88 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
 
   104 nitpick [card = 1, expect = genuine]
 
    89 nitpick [card = 1, expect = genuine]
 
   105 nitpick [card = 2, expect = genuine]
 
       
   106 nitpick [card = 5, expect = genuine]
 
    90 nitpick [card = 5, expect = genuine]
 
   107 oops
 
    91 oops
 
   108 
    92 
   109 lemma "P (\<lambda>x. x)"
 
    93 lemma "P (\<lambda>x. x)"
 
   110 nitpick [card = 1, expect = genuine]
 
    94 nitpick [card = 1, expect = genuine]
 
   111 nitpick [card = 5, expect = genuine]
 
    95 nitpick [card = 5, expect = genuine]
 
   112 oops
 
    96 oops
 
   113 
    97 
   114 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
 
    98 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
 
   115 nitpick [card = 1\<midarrow>6, expect = none]
 
    99 nitpick [card = 1\<midarrow>12, expect = none]
 
   116 nitpick [card = 20, expect = none]
 
       
   117 by auto
 
   100 by auto
 
   118 
   101 
   119 lemma "fst (a, b) = a"
 
   102 lemma "fst (a, b) = a"
 
   120 nitpick [card = 1\<midarrow>20, expect = none]
 
   103 nitpick [card = 1\<midarrow>20, expect = none]
 
   121 by auto
 
   104 by auto
 
   122 
   105 
   123 lemma "\<exists>P. P = Id"
 
   106 lemma "\<exists>P. P = Id"
 
   124 nitpick [card = 1\<midarrow>4, expect = none]
 
   107 nitpick [card = 1\<midarrow>20, expect = none]
 
   125 by auto
 
   108 by auto
 
   126 
   109 
   127 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
 
   110 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
 
   128 nitpick [card = 1\<midarrow>3, expect = none]
 
   111 nitpick [card = 1\<midarrow>3, expect = none]
 
   129 by auto
 
   112 by auto
 
   130 
   113 
   131 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
 
   114 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
 
   132 nitpick [card = 1\<midarrow>6, expect = none]
 
   115 nitpick [card = 1\<midarrow>4, expect = none]
 
   133 by auto
 
   116 by auto
 
   134 
   117 
   135 lemma "Id (a, a)"
 
   118 lemma "Id (a, a)"
 
   136 nitpick [card = 1\<midarrow>100, expect = none]
 
   119 nitpick [card = 1\<midarrow>50, expect = none]
 
   137 by (auto simp: Id_def Collect_def)
 
   120 by (auto simp: Id_def Collect_def)
 
   138 
   121 
   139 lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
 
   122 lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
 
   140 nitpick [card = 1\<midarrow>10, expect = none]
 
   123 nitpick [card = 1\<midarrow>10, expect = none]
 
   141 by (auto simp: Id_def Collect_def)
 
   124 by (auto simp: Id_def Collect_def)
 
   149 by auto
 
   132 by auto
 
   150 
   133 
   151 lemma "g = Let (A \<or> B)"
 
   134 lemma "g = Let (A \<or> B)"
 
   152 nitpick [card = 1, expect = none]
 
   135 nitpick [card = 1, expect = none]
 
   153 nitpick [card = 2, expect = genuine]
 
   136 nitpick [card = 2, expect = genuine]
 
   154 nitpick [card = 20, expect = genuine]
 
   137 nitpick [card = 12, expect = genuine]
 
   155 oops
 
   138 oops
 
   156 
   139 
   157 lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
 
   140 lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
 
   158 nitpick [expect = none]
 
   141 nitpick [expect = none]
 
   159 by auto
 
   142 by auto
 
   170 nitpick [card = 100, expect = genuine]
 
   153 nitpick [card = 100, expect = genuine]
 
   171 oops
 
   154 oops
 
   172 
   155 
   173 lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
 
   156 lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
 
   174 nitpick [card = 1, expect = genuine]
 
   157 nitpick [card = 1, expect = genuine]
 
   175 nitpick [card = 2, expect = genuine]
 
       
   176 nitpick [card = 4, expect = genuine]
 
       
   177 nitpick [card = 20, expect = genuine]
 
   158 nitpick [card = 20, expect = genuine]
 
   178 nitpick [card = 10, dont_box, expect = genuine]
 
   159 nitpick [card = 5, dont_box, expect = genuine]
 
   179 oops
 
   160 oops
 
   180 
   161 
   181 lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
 
   162 lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
 
   182 nitpick [card = 3, expect = genuine]
 
   163 nitpick [card = 3, expect = genuine]
 
   183 nitpick [card = 3, dont_box, expect = genuine]
 
   164 nitpick [card = 3, dont_box, expect = genuine]
 
   184 nitpick [card = 5, expect = genuine]
 
       
   185 nitpick [card = 10, expect = genuine]
 
   165 nitpick [card = 10, expect = genuine]
 
   186 oops
 
   166 oops
 
   187 
   167 
   188 lemma "f (a, b) = x"
 
   168 lemma "f (a, b) = x"
 
   189 nitpick [card = 3, expect = genuine]
 
   169 nitpick [card = 12, expect = genuine]
 
   190 nitpick [card = 10, expect = genuine]
 
       
   191 nitpick [card = 16, expect = genuine]
 
       
   192 nitpick [card = 30, expect = genuine]
 
       
   193 oops
 
   170 oops
 
   194 
   171 
   195 lemma "f (a, a) = f (c, d)"
 
   172 lemma "f (a, a) = f (c, d)"
 
   196 nitpick [card = 4, expect = genuine]
 
   173 nitpick [card = 12, expect = genuine]
 
   197 nitpick [card = 20, expect = genuine]
 
       
   198 oops
 
   174 oops
 
   199 
   175 
   200 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
 
   176 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
 
       
   177 nitpick [card = 1\<midarrow>12, expect = none]
 
       
   178 by auto
 
       
   179 
       
   180 lemma "\<exists>F. F a b = G a b"
 
   201 nitpick [card = 2, expect = none]
 
   181 nitpick [card = 2, expect = none]
 
   202 by auto
 
       
   203 
       
   204 lemma "\<exists>F. F a b = G a b"
 
       
   205 nitpick [card = 3, expect = none]
 
       
   206 by auto
 
   182 by auto
 
   207 
   183 
   208 lemma "f = split"
 
   184 lemma "f = split"
 
   209 nitpick [card = 1, expect = none]
 
   185 nitpick [card = 1, expect = none]
 
   210 nitpick [card = 2, expect = genuine]
 
   186 nitpick [card = 2, expect = genuine]
 
   214 nitpick [card = 20, expect = none]
 
   190 nitpick [card = 20, expect = none]
 
   215 by auto
 
   191 by auto
 
   216 
   192 
   217 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   193 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   218        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
 
   194        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
 
   219 nitpick [card = 1\<midarrow>50, expect = none]
 
   195 nitpick [card = 1\<midarrow>25, expect = none]
 
   220 by auto
 
   196 by auto
 
   221 
   197 
   222 lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
 
   198 lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
 
   223 nitpick [card = 3, expect = genuine]
 
       
   224 nitpick [card = 4, expect = genuine]
 
       
   225 nitpick [card = 8, expect = genuine]
 
   199 nitpick [card = 8, expect = genuine]
 
   226 oops
 
   200 oops
 
   227 
   201 
   228 subsection {* Quantifiers *}
 
   202 subsection {* Quantifiers *}
 
   229 
   203 
   230 lemma "x = y"
 
   204 lemma "x = y"
 
   231 nitpick [card 'a = 1, expect = none]
 
   205 nitpick [card 'a = 1, expect = none]
 
   232 nitpick [card 'a = 2, expect = genuine]
 
   206 nitpick [card 'a = 2, expect = genuine]
 
   233 nitpick [card 'a = 100, expect = genuine]
 
   207 nitpick [card 'a = 200, expect = genuine]
 
   234 nitpick [card 'a = 1000, expect = genuine]
 
       
   235 oops
 
   208 oops
 
   236 
   209 
   237 lemma "\<forall>x. x = y"
 
   210 lemma "\<forall>x. x = y"
 
   238 nitpick [card 'a = 1, expect = none]
 
   211 nitpick [card 'a = 1, expect = none]
 
   239 nitpick [card 'a = 2, expect = genuine]
 
   212 nitpick [card 'a = 2, expect = genuine]
 
   240 nitpick [card 'a = 100, expect = genuine]
 
   213 nitpick [card 'a = 200, expect = genuine]
 
   241 nitpick [card 'a = 1000, expect = genuine]
 
       
   242 oops
 
   214 oops
 
   243 
   215 
   244 lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
 
   216 lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
 
   245 nitpick [card 'a = 1, expect = genuine]
 
   217 nitpick [card 'a = 1, expect = genuine]
 
   246 nitpick [card 'a = 2, expect = genuine]
 
   218 nitpick [card 'a = 200, expect = genuine]
 
   247 nitpick [card 'a = 100, expect = genuine]
 
       
   248 nitpick [card 'a = 1000, expect = genuine]
 
       
   249 oops
 
   219 oops
 
   250 
   220 
   251 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
 
   221 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
 
   252 nitpick [card 'a = 1\<midarrow>10, expect = none]
 
   222 nitpick [card 'a = 1\<midarrow>20, expect = none]
 
   253 by auto
 
   223 by auto
 
   254 
   224 
   255 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
 
   225 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
 
   256 nitpick [card = 1\<midarrow>40, expect = none]
 
   226 nitpick [card = 1\<midarrow>20, expect = none]
 
   257 by auto
 
   227 by auto
 
   258 
   228 
   259 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
 
   229 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
 
   260 nitpick [card = 1\<midarrow>5, expect = none]
 
   230 nitpick [card = 1\<midarrow>5, expect = none]
 
   261 by auto
 
   231 by auto
 
   262 
   232 
   263 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
 
   233 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
 
   264 nitpick [card = 1\<midarrow>5, expect = none]
 
   234 nitpick [card = 1\<midarrow>4, expect = none]
 
   265 by auto
 
   235 by auto
 
   266 
   236 
   267 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
 
   237 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
 
   268 nitpick [card = 1\<midarrow>2, expect = genuine]
 
       
   269 nitpick [card = 3, expect = genuine]
 
   238 nitpick [card = 3, expect = genuine]
 
   270 oops
 
   239 oops
 
   271 
   240 
   272 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
 
   241 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
 
   273        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
 
   242        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
 
   274 nitpick [card = 1\<midarrow>2, expect = none]
 
   243 nitpick [card = 1\<midarrow>2, expect = none]
 
   275 nitpick [card = 3, expect = none]
 
   244 nitpick [card = 3, expect = none]
 
   276 nitpick [card = 4, expect = none]
 
       
   277 sorry
 
   245 sorry
 
   278 
   246 
   279 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
 
   247 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
 
   280        f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
 
   248        f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
 
   281 nitpick [card = 1\<midarrow>2, expect = genuine]
 
   249 nitpick [card = 1\<midarrow>2, expect = genuine]
 
   332 nitpick [expect = none]
 
   300 nitpick [expect = none]
 
   333 by auto
 
   301 by auto
 
   334 
   302 
   335 lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
 
   303 lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
 
   336 nitpick [card 'a = 1, expect = genuine]
 
   304 nitpick [card 'a = 1, expect = genuine]
 
   337 nitpick [card 'a = 2, expect = genuine]
 
       
   338 nitpick [card 'a = 3, expect = genuine]
 
       
   339 nitpick [card 'a = 4, expect = genuine]
 
       
   340 nitpick [card 'a = 5, expect = genuine]
 
   305 nitpick [card 'a = 5, expect = genuine]
 
   341 oops
 
   306 oops
 
   342 
   307 
   343 lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
 
   308 lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
 
   344            else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
 
   309            else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
 
   388 
   353 
   389 lemma "x \<equiv> all \<Longrightarrow> False"
 
   354 lemma "x \<equiv> all \<Longrightarrow> False"
 
   390 nitpick [card = 1, expect = genuine]
 
   355 nitpick [card = 1, expect = genuine]
 
   391 nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
 
   356 nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
 
   392 nitpick [card = 2, expect = genuine]
 
   357 nitpick [card = 2, expect = genuine]
 
   393 nitpick [card = 8, expect = genuine]
 
   358 nitpick [card = 6, expect = genuine]
 
   394 nitpick [card = 10, expect = unknown]
 
       
   395 oops
 
   359 oops
 
   396 
   360 
   397 lemma "\<And>x. f x y = f x y"
 
   361 lemma "\<And>x. f x y = f x y"
 
   398 nitpick [expect = none]
 
   362 nitpick [expect = none]
 
   399 oops
 
   363 oops
 
   414 nitpick [expect = none]
 
   378 nitpick [expect = none]
 
   415 by auto
 
   379 by auto
 
   416 
   380 
   417 lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
 
   381 lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
 
   418 nitpick [card = 1, expect = genuine]
 
   382 nitpick [card = 1, expect = genuine]
 
   419 nitpick [card = 2, expect = genuine]
 
   383 nitpick [card = 20, expect = genuine]
 
   420 nitpick [card = 3, expect = genuine]
 
       
   421 nitpick [card = 4, expect = genuine]
 
       
   422 nitpick [card = 5, expect = genuine]
 
       
   423 nitpick [card = 100, expect = genuine]
 
       
   424 oops
 
   384 oops
 
   425 
   385 
   426 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
 
   386 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
 
   427 nitpick [expect = none]
 
   387 nitpick [expect = none]
 
   428 by auto
 
   388 by auto
 
   527 by auto
 
   487 by auto
 
   528 
   488 
   529 lemma "x = Ex \<Longrightarrow> False"
 
   489 lemma "x = Ex \<Longrightarrow> False"
 
   530 nitpick [card = 1, dont_box, expect = genuine]
 
   490 nitpick [card = 1, dont_box, expect = genuine]
 
   531 nitpick [card = 2, dont_box, expect = genuine]
 
   491 nitpick [card = 2, dont_box, expect = genuine]
 
   532 nitpick [card = 8, dont_box, expect = genuine]
 
   492 nitpick [card = 6, dont_box, expect = genuine]
 
   533 nitpick [card = 10, dont_box, expect = unknown]
 
   493 nitpick [card = 10, dont_box, expect = unknown]
 
   534 oops
 
   494 oops
 
   535 
   495 
   536 lemma "\<exists>x. f x y = f x y"
 
   496 lemma "\<exists>x. f x y = f x y"
 
   537 nitpick [expect = none]
 
   497 nitpick [expect = none]
 
   580 
   540 
   581 lemma "x = y \<and> y = z \<Longrightarrow> x = z"
 
   541 lemma "x = y \<and> y = z \<Longrightarrow> x = z"
 
   582 nitpick [expect = none]
 
   542 nitpick [expect = none]
 
   583 by auto
 
   543 by auto
 
   584 
   544 
   585 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
 
   545 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))"
 
   586       "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
 
   546       "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))"
 
   587 nitpick [expect = none]
 
   547 nitpick [expect = none]
 
   588 by auto
 
   548 by auto
 
   589 
   549 
   590 lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
 
   550 lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
 
   591 nitpick [expect = none]
 
   551 nitpick [expect = none]
 
   794 lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
 
   754 lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
 
   795 nitpick [card = 1\<midarrow>2, expect = none]
 
   755 nitpick [card = 1\<midarrow>2, expect = none]
 
   796 by auto
 
   756 by auto
 
   797 
   757 
   798 lemma "((x, x), (x, x)) \<in> rtrancl {}"
 
   758 lemma "((x, x), (x, x)) \<in> rtrancl {}"
 
   799 nitpick [expect = none]
 
   759 nitpick [card = 1\<midarrow>5, expect = none]
 
   800 by auto
 
   760 by auto
 
   801 
   761 
   802 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
 
   762 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
 
   803 nitpick [card = 1\<midarrow>5, expect = none]
 
   763 nitpick [card = 1\<midarrow>5, expect = none]
 
   804 by auto
 
   764 by auto
 
   929 nitpick [card = 2, expect = none]
 
   889 nitpick [card = 2, expect = none]
 
   930 nitpick [card = 3\<midarrow>5, expect = genuine]
 
   890 nitpick [card = 3\<midarrow>5, expect = genuine]
 
   931 oops
 
   891 oops
 
   932 
   892 
   933 lemma "P x \<Longrightarrow> P (The P)"
 
   893 lemma "P x \<Longrightarrow> P (The P)"
 
   934 nitpick [card = 1, expect = none]
 
       
   935 nitpick [card = 1\<midarrow>2, expect = none]
 
   894 nitpick [card = 1\<midarrow>2, expect = none]
 
   936 nitpick [card = 3\<midarrow>5, expect = genuine]
 
   895 nitpick [card = 3, expect = genuine]
 
   937 nitpick [card = 8, expect = genuine]
 
   896 nitpick [card = 8, expect = genuine]
 
   938 oops
 
   897 oops
 
   939 
   898 
   940 lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
 
   899 lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
 
   941 nitpick [expect = genuine]
 
   900 nitpick [expect = genuine]
isabelle