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