src/HOL/Nitpick_Examples/Datatype_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;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Datatype_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 applied to datatypes.
blanchet@33197
     6
*)
blanchet@33197
     7
wenzelm@63167
     8
section \<open>Examples Featuring Nitpick Applied to Datatypes\<close>
blanchet@33197
     9
blanchet@33197
    10
theory Datatype_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@55893
    14
nitpick_params [verbose, card = 1-8, max_potential = 0,
blanchet@54680
    15
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
blanchet@34083
    16
haftmann@62597
    17
datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3
haftmann@62597
    18
  | Nibble4 | Nibble5 | Nibble6 | Nibble7
haftmann@62597
    19
  | Nibble8 | Nibble9 | NibbleA | NibbleB
haftmann@62597
    20
  | NibbleC | NibbleD | NibbleE | NibbleF
haftmann@62597
    21
blanchet@33197
    22
primrec rot where
blanchet@34126
    23
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
blanchet@34126
    24
"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
blanchet@34126
    25
"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
blanchet@34126
    26
"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
blanchet@34126
    27
"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
blanchet@33197
    28
"rot NibbleF = Nibble0"
blanchet@33197
    29
blanchet@33197
    30
lemma "rot n \<noteq> n"
blanchet@55893
    31
nitpick [card = 1-8,16, verbose, expect = none]
blanchet@33197
    32
sorry
blanchet@33197
    33
blanchet@33197
    34
lemma "rot Nibble2 \<noteq> Nibble3"
blanchet@33197
    35
nitpick [card = 1, expect = none]
blanchet@35284
    36
nitpick [card = 2, max Nibble4 = 0, expect = genuine]
blanchet@33197
    37
nitpick [card = 2, max Nibble2 = 0, expect = none]
blanchet@33197
    38
oops
blanchet@33197
    39
blanchet@33199
    40
lemma "(rot ^^ 15) n \<noteq> n"
blanchet@33197
    41
nitpick [card = 17, expect = none]
blanchet@33197
    42
sorry
blanchet@33197
    43
blanchet@33199
    44
lemma "(rot ^^ 15) n = n"
blanchet@33197
    45
nitpick [card = 17, expect = genuine]
blanchet@33197
    46
oops
blanchet@33197
    47
blanchet@33199
    48
lemma "(rot ^^ 16) n = n"
blanchet@33197
    49
nitpick [card = 17, expect = none]
blanchet@33197
    50
oops
blanchet@33197
    51
blanchet@58310
    52
datatype ('a, 'b) pd = Pd "'a \<times> 'b"
blanchet@33197
    53
blanchet@33197
    54
fun fs where
blanchet@33197
    55
"fs (Pd (a, _)) = a"
blanchet@33197
    56
blanchet@33197
    57
fun sn where
blanchet@33197
    58
"sn (Pd (_, b)) = b"
blanchet@33197
    59
blanchet@33197
    60
lemma "fs (Pd p) = fst p"
blanchet@35284
    61
nitpick [card = 12, expect = none]
blanchet@33197
    62
sorry
blanchet@33197
    63
blanchet@33197
    64
lemma "fs (Pd p) = snd p"
blanchet@33197
    65
nitpick [expect = genuine]
blanchet@33197
    66
oops
blanchet@33197
    67
blanchet@33197
    68
lemma "sn (Pd p) = snd p"
blanchet@35284
    69
nitpick [card = 12, expect = none]
blanchet@33197
    70
sorry
blanchet@33197
    71
blanchet@33197
    72
lemma "sn (Pd p) = fst p"
blanchet@33197
    73
nitpick [expect = genuine]
blanchet@33197
    74
oops
blanchet@33197
    75
blanchet@33197
    76
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
blanchet@40410
    77
nitpick [expect = none]
blanchet@33197
    78
sorry
blanchet@33197
    79
blanchet@33197
    80
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
blanchet@33197
    81
nitpick [expect = genuine]
blanchet@33197
    82
oops
blanchet@33197
    83
blanchet@58310
    84
datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
blanchet@33197
    85
blanchet@33197
    86
fun app where
blanchet@33197
    87
"app (Fn f) x = f x"
blanchet@33197
    88
blanchet@33197
    89
lemma "app (Fn g) y = g y"
blanchet@40410
    90
nitpick [expect = none]
blanchet@33197
    91
sorry
blanchet@33197
    92
blanchet@33197
    93
lemma "app (Fn g) y = g' y"
blanchet@33197
    94
nitpick [expect = genuine]
blanchet@33197
    95
oops
blanchet@33197
    96
blanchet@33197
    97
lemma "app (Fn g) y = g y'"
blanchet@33197
    98
nitpick [expect = genuine]
blanchet@33197
    99
oops
blanchet@33197
   100
blanchet@33197
   101
end