src/HOL/Nitpick_Examples/Datatype_Nits.thy
author blanchet
Fri Oct 23 18:59:24 2009 +0200 (2009-10-23)
changeset 33197 de6285ebcc05
child 33199 6c9b2a94a69c
permissions -rw-r--r--
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
     1 (*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009
     4 
     5 Examples featuring Nitpick applied to datatypes.
     6 *)
     7 
     8 header {* Examples Featuring Nitpick Applied to Datatypes *}
     9 
    10 theory Datatype_Nits
    11 imports Main
    12 begin
    13 
    14 primrec rot where
    15 "rot Nibble0 = Nibble1" |
    16 "rot Nibble1 = Nibble2" |
    17 "rot Nibble2 = Nibble3" |
    18 "rot Nibble3 = Nibble4" |
    19 "rot Nibble4 = Nibble5" |
    20 "rot Nibble5 = Nibble6" |
    21 "rot Nibble6 = Nibble7" |
    22 "rot Nibble7 = Nibble8" |
    23 "rot Nibble8 = Nibble9" |
    24 "rot Nibble9 = NibbleA" |
    25 "rot NibbleA = NibbleB" |
    26 "rot NibbleB = NibbleC" |
    27 "rot NibbleC = NibbleD" |
    28 "rot NibbleD = NibbleE" |
    29 "rot NibbleE = NibbleF" |
    30 "rot NibbleF = Nibble0"
    31 
    32 lemma "rot n \<noteq> n"
    33 nitpick [card = 1\<midarrow>16, expect = none]
    34 sorry
    35 
    36 lemma "rot Nibble2 \<noteq> Nibble3"
    37 nitpick [card = 1, expect = none]
    38 nitpick [card = 2, expect = genuine]
    39 nitpick [card = 2, max Nibble2 = 0, expect = none]
    40 nitpick [card = 2, max Nibble3 = 0, expect = none]
    41 oops
    42 
    43 lemma "fun_pow 15 rot n \<noteq> n"
    44 nitpick [card = 17, expect = none]
    45 sorry
    46 
    47 lemma "fun_pow 15 rot n = n"
    48 nitpick [card = 17, expect = genuine]
    49 oops
    50 
    51 lemma "fun_pow 16 rot n = n"
    52 nitpick [card = 17, expect = none]
    53 oops
    54 
    55 datatype ('a, 'b) pd = Pd "'a \<times> 'b"
    56 
    57 fun fs where
    58 "fs (Pd (a, _)) = a"
    59 
    60 fun sn where
    61 "sn (Pd (_, b)) = b"
    62 
    63 lemma "fs (Pd p) = fst p"
    64 nitpick [card = 20, expect = none]
    65 sorry
    66 
    67 lemma "fs (Pd p) = snd p"
    68 nitpick [expect = genuine]
    69 oops
    70 
    71 lemma "sn (Pd p) = snd p"
    72 nitpick [card = 20, expect = none]
    73 sorry
    74 
    75 lemma "sn (Pd p) = fst p"
    76 nitpick [expect = genuine]
    77 oops
    78 
    79 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    80 nitpick [card = 1\<midarrow>12, expect = none]
    81 sorry
    82 
    83 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    84 nitpick [expect = genuine]
    85 oops
    86 
    87 datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
    88 
    89 fun app where
    90 "app (Fn f) x = f x"
    91 
    92 lemma "app (Fn g) y = g y"
    93 nitpick [card = 1\<midarrow>12, expect = none]
    94 sorry
    95 
    96 lemma "app (Fn g) y = g' y"
    97 nitpick [expect = genuine]
    98 oops
    99 
   100 lemma "app (Fn g) y = g y'"
   101 nitpick [expect = genuine]
   102 oops
   103 
   104 end