src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03)
changeset 55888 cac1add157e8
parent 55072 8488fdc4ddc0
child 55889 6bfbec3dff62
permissions -rw-r--r--
removed nonstandard models from Nitpick
     1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2014
     4 
     5 Examples from the Nitpick manual.
     6 *)
     7 
     8 header {* Examples from the Nitpick Manual *}
     9 
    10 (* The "expect" arguments to Nitpick in this theory and the other example
    11    theories are there so that the example can also serve as a regression test
    12    suite. *)
    13 
    14 theory Manual_Nits
    15 imports Main Real "~~/src/HOL/Library/Quotient_Product"
    16 begin
    17 
    18 
    19 section {* 2. First Steps *}
    20 
    21 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    22 
    23 
    24 subsection {* 2.1. Propositional Logic *}
    25 
    26 lemma "P \<longleftrightarrow> Q"
    27 nitpick [expect = genuine]
    28 apply auto
    29 nitpick [expect = genuine] 1
    30 nitpick [expect = genuine] 2
    31 oops
    32 
    33 
    34 subsection {* 2.2. Type Variables *}
    35 
    36 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    37 nitpick [verbose, expect = genuine]
    38 oops
    39 
    40 
    41 subsection {* 2.3. Constants *}
    42 
    43 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    44 nitpick [show_consts, expect = genuine]
    45 nitpick [dont_specialize, show_consts, expect = genuine]
    46 oops
    47 
    48 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    49 nitpick [expect = none]
    50 nitpick [card 'a = 1\<emdash>50, expect = none]
    51 (* sledgehammer *)
    52 by (metis the_equality)
    53 
    54 
    55 subsection {* 2.4. Skolemization *}
    56 
    57 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    58 nitpick [expect = genuine]
    59 oops
    60 
    61 lemma "\<exists>x. \<forall>f. f x = x"
    62 nitpick [expect = genuine]
    63 oops
    64 
    65 lemma "refl r \<Longrightarrow> sym r"
    66 nitpick [expect = genuine]
    67 oops
    68 
    69 
    70 subsection {* 2.5. Natural Numbers and Integers *}
    71 
    72 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    73 nitpick [expect = genuine]
    74 nitpick [binary_ints, bits = 16, expect = genuine]
    75 oops
    76 
    77 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
    78 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine]
    79 oops
    80 
    81 lemma "P Suc"
    82 nitpick [expect = none]
    83 oops
    84 
    85 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
    86 nitpick [card nat = 1, expect = genuine]
    87 nitpick [card nat = 2, expect = none]
    88 oops
    89 
    90 
    91 subsection {* 2.6. Inductive Datatypes *}
    92 
    93 lemma "hd (xs @ [y, y]) = hd xs"
    94 nitpick [expect = genuine]
    95 nitpick [show_consts, show_datatypes, expect = genuine]
    96 oops
    97 
    98 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    99 nitpick [show_datatypes, expect = genuine]
   100 oops
   101 
   102 
   103 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
   104 
   105 definition "three = {0\<Colon>nat, 1, 2}"
   106 typedef three = three
   107   unfolding three_def by blast
   108 
   109 definition A :: three where "A \<equiv> Abs_three 0"
   110 definition B :: three where "B \<equiv> Abs_three 1"
   111 definition C :: three where "C \<equiv> Abs_three 2"
   112 
   113 lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
   114 nitpick [show_datatypes, expect = genuine]
   115 oops
   116 
   117 fun my_int_rel where
   118 "my_int_rel (x, y) (u, v) = (x + v = u + y)"
   119 
   120 quotient_type my_int = "nat \<times> nat" / my_int_rel
   121 by (auto simp add: equivp_def fun_eq_iff)
   122 
   123 definition add_raw where
   124 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
   125 
   126 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
   127 unfolding add_raw_def by auto
   128 
   129 lemma "add x y = add x x"
   130 nitpick [show_datatypes, expect = genuine]
   131 oops
   132 
   133 ML {*
   134 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
   135     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
   136                          - snd (HOLogic.dest_number t2))
   137   | my_int_postproc _ _ _ _ t = t
   138 *}
   139 
   140 declaration {*
   141 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
   142 *}
   143 
   144 lemma "add x y = add x x"
   145 nitpick [show_datatypes]
   146 oops
   147 
   148 record point =
   149   Xcoord :: int
   150   Ycoord :: int
   151 
   152 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
   153 nitpick [show_datatypes, expect = genuine]
   154 oops
   155 
   156 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
   157 nitpick [show_datatypes, expect = genuine]
   158 oops
   159 
   160 
   161 subsection {* 2.8. Inductive and Coinductive Predicates *}
   162 
   163 inductive even where
   164 "even 0" |
   165 "even n \<Longrightarrow> even (Suc (Suc n))"
   166 
   167 lemma "\<exists>n. even n \<and> even (Suc n)"
   168 nitpick [card nat = 50, unary_ints, verbose, expect = potential]
   169 oops
   170 
   171 lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
   172 nitpick [card nat = 50, unary_ints, expect = genuine]
   173 oops
   174 
   175 inductive even' where
   176 "even' (0\<Colon>nat)" |
   177 "even' 2" |
   178 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
   179 
   180 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
   181 nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
   182 oops
   183 
   184 lemma "even' (n - 2) \<Longrightarrow> even' n"
   185 nitpick [card nat = 10, show_consts, expect = genuine]
   186 oops
   187 
   188 coinductive nats where
   189 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
   190 
   191 lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})"
   192 nitpick [card nat = 10, show_consts, expect = genuine]
   193 oops
   194 
   195 inductive odd where
   196 "odd 1" |
   197 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
   198 
   199 lemma "odd n \<Longrightarrow> odd (n - 2)"
   200 nitpick [card nat = 4, show_consts, expect = genuine]
   201 oops
   202 
   203 
   204 subsection {* 2.9. Coinductive Datatypes *}
   205 
   206 codatatype 'a llist = LNil | LCons 'a "'a llist"
   207 
   208 primcorec iterates where
   209 "iterates f a = LCons a (iterates f (f a))"
   210 
   211 lemma "xs \<noteq> LCons a xs"
   212 nitpick [expect = genuine]
   213 oops
   214 
   215 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
   216 nitpick [verbose, expect = genuine]
   217 oops
   218 
   219 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
   220 nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
   221 nitpick [card = 1\<emdash>5, expect = none]
   222 sorry
   223 
   224 
   225 subsection {* 2.10. Boxing *}
   226 
   227 datatype tm = Var nat | Lam tm | App tm tm
   228 
   229 primrec lift where
   230 "lift (Var j) k = Var (if j < k then j else j + 1)" |
   231 "lift (Lam t) k = Lam (lift t (k + 1))" |
   232 "lift (App t u) k = App (lift t k) (lift u k)"
   233 
   234 primrec loose where
   235 "loose (Var j) k = (j \<ge> k)" |
   236 "loose (Lam t) k = loose t (Suc k)" |
   237 "loose (App t u) k = (loose t k \<or> loose u k)"
   238 
   239 primrec subst\<^sub>1 where
   240 "subst\<^sub>1 \<sigma> (Var j) = \<sigma> j" |
   241 "subst\<^sub>1 \<sigma> (Lam t) =
   242  Lam (subst\<^sub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
   243 "subst\<^sub>1 \<sigma> (App t u) = App (subst\<^sub>1 \<sigma> t) (subst\<^sub>1 \<sigma> u)"
   244 
   245 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>1 \<sigma> t = t"
   246 nitpick [verbose, expect = genuine]
   247 nitpick [eval = "subst\<^sub>1 \<sigma> t", expect = genuine]
   248 (* nitpick [dont_box, expect = unknown] *)
   249 oops
   250 
   251 primrec subst\<^sub>2 where
   252 "subst\<^sub>2 \<sigma> (Var j) = \<sigma> j" |
   253 "subst\<^sub>2 \<sigma> (Lam t) =
   254  Lam (subst\<^sub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
   255 "subst\<^sub>2 \<sigma> (App t u) = App (subst\<^sub>2 \<sigma> t) (subst\<^sub>2 \<sigma> u)"
   256 
   257 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t"
   258 nitpick [card = 1\<emdash>5, expect = none]
   259 sorry
   260 
   261 
   262 subsection {* 2.11. Scope Monotonicity *}
   263 
   264 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   265 nitpick [verbose, expect = genuine]
   266 oops
   267 
   268 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
   269 nitpick [mono, expect = none]
   270 nitpick [expect = genuine]
   271 oops
   272 
   273 
   274 subsection {* 2.12. Inductive Properties *}
   275 
   276 inductive_set reach where
   277 "(4\<Colon>nat) \<in> reach" |
   278 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
   279 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
   280 
   281 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
   282 (* nitpick *)
   283 apply (induct set: reach)
   284   apply auto
   285  nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
   286  apply (thin_tac "n \<in> reach")
   287  nitpick [expect = genuine]
   288 oops
   289 
   290 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
   291 (* nitpick *)
   292 apply (induct set: reach)
   293   apply auto
   294  nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
   295  apply (thin_tac "n \<in> reach")
   296  nitpick [expect = genuine]
   297 oops
   298 
   299 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   300 by (induct set: reach) arith+
   301 
   302 
   303 section {* 3. Case Studies *}
   304 
   305 nitpick_params [max_potential = 0]
   306 
   307 
   308 subsection {* 3.1. A Context-Free Grammar *}
   309 
   310 datatype alphabet = a | b
   311 
   312 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   313   "[] \<in> S\<^sub>1"
   314 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
   315 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
   316 | "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
   317 | "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
   318 | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
   319 
   320 theorem S\<^sub>1_sound:
   321 "w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   322 nitpick [expect = genuine]
   323 oops
   324 
   325 inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
   326   "[] \<in> S\<^sub>2"
   327 | "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
   328 | "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
   329 | "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
   330 | "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
   331 | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
   332 
   333 theorem S\<^sub>2_sound:
   334 "w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   335 nitpick [expect = genuine]
   336 oops
   337 
   338 inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
   339   "[] \<in> S\<^sub>3"
   340 | "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
   341 | "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
   342 | "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
   343 | "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
   344 | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
   345 
   346 theorem S\<^sub>3_sound:
   347 "w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   348 nitpick [card = 1\<emdash>5, expect = none]
   349 sorry
   350 
   351 theorem S\<^sub>3_complete:
   352 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
   353 nitpick [expect = genuine]
   354 oops
   355 
   356 inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
   357   "[] \<in> S\<^sub>4"
   358 | "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
   359 | "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
   360 | "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
   361 | "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
   362 | "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
   363 | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   364 
   365 theorem S\<^sub>4_sound:
   366 "w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   367 nitpick [card = 1\<emdash>5, expect = none]
   368 sorry
   369 
   370 theorem S\<^sub>4_complete:
   371 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
   372 nitpick [card = 1\<emdash>5, expect = none]
   373 sorry
   374 
   375 theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
   376 "w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   377 "w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   378 "w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   379 nitpick [card = 1\<emdash>5, expect = none]
   380 sorry
   381 
   382 
   383 subsection {* 3.2. AA Trees *}
   384 
   385 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   386 
   387 primrec data where
   388 "data \<Lambda> = undefined" |
   389 "data (N x _ _ _) = x"
   390 
   391 primrec dataset where
   392 "dataset \<Lambda> = {}" |
   393 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
   394 
   395 primrec level where
   396 "level \<Lambda> = 0" |
   397 "level (N _ k _ _) = k"
   398 
   399 primrec left where
   400 "left \<Lambda> = \<Lambda>" |
   401 "left (N _ _ t\<^sub>1 _) = t\<^sub>1"
   402 
   403 primrec right where
   404 "right \<Lambda> = \<Lambda>" |
   405 "right (N _ _ _ t\<^sub>2) = t\<^sub>2"
   406 
   407 fun wf where
   408 "wf \<Lambda> = True" |
   409 "wf (N _ k t u) =
   410  (if t = \<Lambda> then
   411     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
   412   else
   413     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
   414 
   415 fun skew where
   416 "skew \<Lambda> = \<Lambda>" |
   417 "skew (N x k t u) =
   418  (if t \<noteq> \<Lambda> \<and> k = level t then
   419     N (data t) k (left t) (N x k (right t) u)
   420   else
   421     N x k t u)"
   422 
   423 fun split where
   424 "split \<Lambda> = \<Lambda>" |
   425 "split (N x k t u) =
   426  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
   427     N (data u) (Suc k) (N x k t (left u)) (right u)
   428   else
   429     N x k t u)"
   430 
   431 theorem dataset_skew_split:
   432 "dataset (skew t) = dataset t"
   433 "dataset (split t) = dataset t"
   434 nitpick [card = 1\<emdash>5, expect = none]
   435 sorry
   436 
   437 theorem wf_skew_split:
   438 "wf t \<Longrightarrow> skew t = t"
   439 "wf t \<Longrightarrow> split t = t"
   440 nitpick [card = 1\<emdash>5, expect = none]
   441 sorry
   442 
   443 primrec insort\<^sub>1 where
   444 "insort\<^sub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   445 "insort\<^sub>1 (N y k t u) x =
   446  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^sub>1 t x else t)
   447                              (if x > y then insort\<^sub>1 u x else u))"
   448 
   449 theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)"
   450 nitpick [expect = genuine]
   451 oops
   452 
   453 theorem wf_insort\<^sub>1_nat: "wf t \<Longrightarrow> wf (insort\<^sub>1 t (x\<Colon>nat))"
   454 nitpick [eval = "insort\<^sub>1 t x", expect = genuine]
   455 oops
   456 
   457 primrec insort\<^sub>2 where
   458 "insort\<^sub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   459 "insort\<^sub>2 (N y k t u) x =
   460  (split \<circ> skew) (N y k (if x < y then insort\<^sub>2 t x else t)
   461                        (if x > y then insort\<^sub>2 u x else u))"
   462 
   463 theorem wf_insort\<^sub>2: "wf t \<Longrightarrow> wf (insort\<^sub>2 t x)"
   464 nitpick [card = 1\<emdash>5, expect = none]
   465 sorry
   466 
   467 theorem dataset_insort\<^sub>2: "dataset (insort\<^sub>2 t x) = {x} \<union> dataset t"
   468 nitpick [card = 1\<emdash>5, expect = none]
   469 sorry
   470 
   471 end