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