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