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