src/HOL/Nitpick_Examples/Pattern_Nits.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 63167 0909deb8059b
permissions -rw-r--r--
tuned: each session has at most one defining entry;
     1 (*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2011
     4 
     5 Examples featuring Nitpick's "destroy_constrs" optimization.
     6 *)
     7 
     8 section \<open>Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization\<close>
     9 
    10 theory Pattern_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat_JNI,
    15                 max_threads = 1, timeout = 240]
    16 
    17 lemma "x = (case u of () \<Rightarrow> y)"
    18 nitpick [expect = genuine]
    19 oops
    20 
    21 lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
    22 nitpick [expect = genuine]
    23 oops
    24 
    25 lemma "x = (case p of (x, y) \<Rightarrow> y)"
    26 nitpick [expect = genuine]
    27 oops
    28 
    29 lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
    30 nitpick [expect = genuine]
    31 oops
    32 
    33 lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
    34 nitpick [expect = genuine]
    35 oops
    36 
    37 lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
    38 nitpick [expect = genuine]
    39 oops
    40 
    41 lemma "x = (case xs of
    42               [] \<Rightarrow> x
    43             | y # ys \<Rightarrow>
    44               (case ys of
    45                  [] \<Rightarrow> x
    46                | z # zs \<Rightarrow>
    47                  (case z of
    48                     None \<Rightarrow> x
    49                   | Some p \<Rightarrow>
    50                     (case p of
    51                        (a, b) \<Rightarrow> b))))"
    52 nitpick [expect = genuine]
    53 oops
    54 
    55 fun f1 where
    56 "f1 x () = x"
    57 
    58 lemma "x = f1 y u"
    59 nitpick [expect = genuine]
    60 oops
    61 
    62 fun f2 where
    63 "f2 x _ True = x" |
    64 "f2 _ y False = y"
    65 
    66 lemma "x = f2 x y b"
    67 nitpick [expect = genuine]
    68 oops
    69 
    70 fun f3 where
    71 "f3 (_, y) = y"
    72 
    73 lemma "x = f3 p"
    74 nitpick [expect = genuine]
    75 oops
    76 
    77 fun f4 where
    78 "f4 x 0 = x" |
    79 "f4 _ (Suc n) = n"
    80 
    81 lemma "x = f4 x n"
    82 nitpick [expect = genuine]
    83 oops
    84 
    85 fun f5 where
    86 "f5 x None = x" |
    87 "f5 _ (Some y) = y"
    88 
    89 lemma "x = f5 x opt"
    90 nitpick [expect = genuine]
    91 oops
    92 
    93 fun f6 where
    94 "f6 x [] = x" |
    95 "f6 _ (y # ys) = y"
    96 
    97 lemma "x = f6 x xs"
    98 nitpick [expect = genuine]
    99 oops
   100 
   101 fun f7 where
   102 "f7 _ (y # Some (a, b) # zs) = b" |
   103 "f7 x (y # None # zs) = x" |
   104 "f7 x [y] = x" |
   105 "f7 x [] = x"
   106 
   107 lemma "x = f7 x xs"
   108 nitpick [expect = genuine]
   109 oops
   110 
   111 lemma "u = ()"
   112 nitpick [expect = none]
   113 sorry
   114 
   115 lemma "\<exists>y. (b::bool) = y"
   116 nitpick [expect = none]
   117 sorry
   118 
   119 lemma "\<exists>x y. p = (x, y)"
   120 nitpick [expect = none]
   121 sorry
   122 
   123 lemma "\<exists>x. n = Suc x"
   124 nitpick [expect = genuine]
   125 oops
   126 
   127 lemma "\<exists>y. x = Some y"
   128 nitpick [expect = genuine]
   129 oops
   130 
   131 lemma "\<exists>y ys. xs = y # ys"
   132 nitpick [expect = genuine]
   133 oops
   134 
   135 lemma "\<exists>y a b zs. x = y # Some (a, b) # zs"
   136 nitpick [expect = genuine]
   137 oops
   138 
   139 end