src/HOL/Nitpick_Examples/Datatype_Nits.thy
author blanchet
Mon Feb 22 19:31:00 2010 +0100 (2010-02-22)
changeset 35284 9edc2bd6d2bd
parent 35078 6fd1052fe463
child 35386 45a4e19d3ebd
permissions -rw-r--r--
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
blanchet@33197
     4
blanchet@33197
     5
Examples featuring Nitpick applied to datatypes.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Examples Featuring Nitpick Applied to Datatypes *}
blanchet@33197
     9
blanchet@33197
    10
theory Datatype_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@35284
    14
nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
blanchet@35284
    15
                timeout = 60 s]
blanchet@34083
    16
blanchet@33197
    17
primrec rot where
blanchet@34126
    18
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
blanchet@34126
    19
"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
blanchet@34126
    20
"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
blanchet@34126
    21
"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
blanchet@34126
    22
"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
blanchet@33197
    23
"rot NibbleF = Nibble0"
blanchet@33197
    24
blanchet@33197
    25
lemma "rot n \<noteq> n"
blanchet@33197
    26
nitpick [card = 1\<midarrow>16, expect = none]
blanchet@33197
    27
sorry
blanchet@33197
    28
blanchet@33197
    29
lemma "rot Nibble2 \<noteq> Nibble3"
blanchet@33197
    30
nitpick [card = 1, expect = none]
blanchet@35284
    31
nitpick [card = 2, max Nibble4 = 0, expect = genuine]
blanchet@33197
    32
nitpick [card = 2, max Nibble2 = 0, expect = none]
blanchet@33197
    33
oops
blanchet@33197
    34
blanchet@33199
    35
lemma "(rot ^^ 15) n \<noteq> n"
blanchet@33197
    36
nitpick [card = 17, expect = none]
blanchet@33197
    37
sorry
blanchet@33197
    38
blanchet@33199
    39
lemma "(rot ^^ 15) n = n"
blanchet@33197
    40
nitpick [card = 17, expect = genuine]
blanchet@33197
    41
oops
blanchet@33197
    42
blanchet@33199
    43
lemma "(rot ^^ 16) n = n"
blanchet@33197
    44
nitpick [card = 17, expect = none]
blanchet@33197
    45
oops
blanchet@33197
    46
blanchet@33197
    47
datatype ('a, 'b) pd = Pd "'a \<times> 'b"
blanchet@33197
    48
blanchet@33197
    49
fun fs where
blanchet@33197
    50
"fs (Pd (a, _)) = a"
blanchet@33197
    51
blanchet@33197
    52
fun sn where
blanchet@33197
    53
"sn (Pd (_, b)) = b"
blanchet@33197
    54
blanchet@33197
    55
lemma "fs (Pd p) = fst p"
blanchet@35284
    56
nitpick [card = 12, expect = none]
blanchet@33197
    57
sorry
blanchet@33197
    58
blanchet@33197
    59
lemma "fs (Pd p) = snd p"
blanchet@33197
    60
nitpick [expect = genuine]
blanchet@33197
    61
oops
blanchet@33197
    62
blanchet@33197
    63
lemma "sn (Pd p) = snd p"
blanchet@35284
    64
nitpick [card = 12, expect = none]
blanchet@33197
    65
sorry
blanchet@33197
    66
blanchet@33197
    67
lemma "sn (Pd p) = fst p"
blanchet@33197
    68
nitpick [expect = genuine]
blanchet@33197
    69
oops
blanchet@33197
    70
blanchet@33197
    71
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
blanchet@35284
    72
nitpick [card = 1\<midarrow>10, expect = none]
blanchet@33197
    73
sorry
blanchet@33197
    74
blanchet@33197
    75
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
blanchet@33197
    76
nitpick [expect = genuine]
blanchet@33197
    77
oops
blanchet@33197
    78
blanchet@33197
    79
datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
blanchet@33197
    80
blanchet@33197
    81
fun app where
blanchet@33197
    82
"app (Fn f) x = f x"
blanchet@33197
    83
blanchet@33197
    84
lemma "app (Fn g) y = g y"
blanchet@35284
    85
nitpick [card = 1\<midarrow>10, expect = none]
blanchet@33197
    86
sorry
blanchet@33197
    87
blanchet@33197
    88
lemma "app (Fn g) y = g' y"
blanchet@33197
    89
nitpick [expect = genuine]
blanchet@33197
    90
oops
blanchet@33197
    91
blanchet@33197
    92
lemma "app (Fn g) y = g y'"
blanchet@33197
    93
nitpick [expect = genuine]
blanchet@33197
    94
oops
blanchet@33197
    95
blanchet@33197
    96
end