src/HOL/Nitpick_Examples/Datatype_Nits.thy
author blanchet
Mon Dec 14 10:59:46 2009 +0100 (2009-12-14)
changeset 34083 652719832159
parent 33199 6c9b2a94a69c
child 34126 8a2c5d7aff51
permissions -rw-r--r--
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33197
     3
    Copyright   2009
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@34083
    14
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
blanchet@34083
    15
blanchet@33197
    16
primrec rot where
blanchet@33197
    17
"rot Nibble0 = Nibble1" |
blanchet@33197
    18
"rot Nibble1 = Nibble2" |
blanchet@33197
    19
"rot Nibble2 = Nibble3" |
blanchet@33197
    20
"rot Nibble3 = Nibble4" |
blanchet@33197
    21
"rot Nibble4 = Nibble5" |
blanchet@33197
    22
"rot Nibble5 = Nibble6" |
blanchet@33197
    23
"rot Nibble6 = Nibble7" |
blanchet@33197
    24
"rot Nibble7 = Nibble8" |
blanchet@33197
    25
"rot Nibble8 = Nibble9" |
blanchet@33197
    26
"rot Nibble9 = NibbleA" |
blanchet@33197
    27
"rot NibbleA = NibbleB" |
blanchet@33197
    28
"rot NibbleB = NibbleC" |
blanchet@33197
    29
"rot NibbleC = NibbleD" |
blanchet@33197
    30
"rot NibbleD = NibbleE" |
blanchet@33197
    31
"rot NibbleE = NibbleF" |
blanchet@33197
    32
"rot NibbleF = Nibble0"
blanchet@33197
    33
blanchet@33197
    34
lemma "rot n \<noteq> n"
blanchet@33197
    35
nitpick [card = 1\<midarrow>16, expect = none]
blanchet@33197
    36
sorry
blanchet@33197
    37
blanchet@33197
    38
lemma "rot Nibble2 \<noteq> Nibble3"
blanchet@33197
    39
nitpick [card = 1, expect = none]
blanchet@33197
    40
nitpick [card = 2, expect = genuine]
blanchet@33197
    41
nitpick [card = 2, max Nibble2 = 0, expect = none]
blanchet@33197
    42
nitpick [card = 2, max Nibble3 = 0, expect = none]
blanchet@33197
    43
oops
blanchet@33197
    44
blanchet@33199
    45
lemma "(rot ^^ 15) n \<noteq> n"
blanchet@33197
    46
nitpick [card = 17, expect = none]
blanchet@33197
    47
sorry
blanchet@33197
    48
blanchet@33199
    49
lemma "(rot ^^ 15) n = n"
blanchet@33197
    50
nitpick [card = 17, expect = genuine]
blanchet@33197
    51
oops
blanchet@33197
    52
blanchet@33199
    53
lemma "(rot ^^ 16) n = n"
blanchet@33197
    54
nitpick [card = 17, expect = none]
blanchet@33197
    55
oops
blanchet@33197
    56
blanchet@33197
    57
datatype ('a, 'b) pd = Pd "'a \<times> 'b"
blanchet@33197
    58
blanchet@33197
    59
fun fs where
blanchet@33197
    60
"fs (Pd (a, _)) = a"
blanchet@33197
    61
blanchet@33197
    62
fun sn where
blanchet@33197
    63
"sn (Pd (_, b)) = b"
blanchet@33197
    64
blanchet@33197
    65
lemma "fs (Pd p) = fst p"
blanchet@33197
    66
nitpick [card = 20, expect = none]
blanchet@33197
    67
sorry
blanchet@33197
    68
blanchet@33197
    69
lemma "fs (Pd p) = snd p"
blanchet@33197
    70
nitpick [expect = genuine]
blanchet@33197
    71
oops
blanchet@33197
    72
blanchet@33197
    73
lemma "sn (Pd p) = snd p"
blanchet@33197
    74
nitpick [card = 20, expect = none]
blanchet@33197
    75
sorry
blanchet@33197
    76
blanchet@33197
    77
lemma "sn (Pd p) = fst p"
blanchet@33197
    78
nitpick [expect = genuine]
blanchet@33197
    79
oops
blanchet@33197
    80
blanchet@33197
    81
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
blanchet@33197
    82
nitpick [card = 1\<midarrow>12, expect = none]
blanchet@33197
    83
sorry
blanchet@33197
    84
blanchet@33197
    85
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
blanchet@33197
    86
nitpick [expect = genuine]
blanchet@33197
    87
oops
blanchet@33197
    88
blanchet@33197
    89
datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
blanchet@33197
    90
blanchet@33197
    91
fun app where
blanchet@33197
    92
"app (Fn f) x = f x"
blanchet@33197
    93
blanchet@33197
    94
lemma "app (Fn g) y = g y"
blanchet@33197
    95
nitpick [card = 1\<midarrow>12, expect = none]
blanchet@33197
    96
sorry
blanchet@33197
    97
blanchet@33197
    98
lemma "app (Fn g) y = g' y"
blanchet@33197
    99
nitpick [expect = genuine]
blanchet@33197
   100
oops
blanchet@33197
   101
blanchet@33197
   102
lemma "app (Fn g) y = g y'"
blanchet@33197
   103
nitpick [expect = genuine]
blanchet@33197
   104
oops
blanchet@33197
   105
blanchet@33197
   106
end