src/HOL/Nitpick_Examples/Datatype_Nits.thy
author blanchet
Fri Feb 26 16:49:46 2010 +0100 (2010-02-26)
changeset 35386 45a4e19d3ebd
parent 35284 9edc2bd6d2bd
child 37696 1a6f475085fc
permissions -rw-r--r--
more work on the new monotonicity stuff in Nitpick
     1 (*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     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 nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
    15                 timeout = 60 s]
    16 
    17 primrec rot where
    18 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    19 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
    20 "rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
    21 "rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
    22 "rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
    23 "rot NibbleF = Nibble0"
    24 
    25 lemma "rot n \<noteq> n"
    26 nitpick [card = 1\<midarrow>16, expect = none]
    27 sorry
    28 
    29 lemma "rot Nibble2 \<noteq> Nibble3"
    30 nitpick [card = 1, expect = none]
    31 nitpick [card = 2, max Nibble4 = 0, expect = genuine]
    32 nitpick [card = 2, max Nibble2 = 0, expect = none]
    33 oops
    34 
    35 lemma "(rot ^^ 15) n \<noteq> n"
    36 nitpick [card = 17, expect = none]
    37 sorry
    38 
    39 lemma "(rot ^^ 15) n = n"
    40 nitpick [card = 17, expect = genuine]
    41 oops
    42 
    43 lemma "(rot ^^ 16) n = n"
    44 nitpick [card = 17, expect = none]
    45 oops
    46 
    47 datatype ('a, 'b) pd = Pd "'a \<times> 'b"
    48 
    49 fun fs where
    50 "fs (Pd (a, _)) = a"
    51 
    52 fun sn where
    53 "sn (Pd (_, b)) = b"
    54 
    55 lemma "fs (Pd p) = fst p"
    56 nitpick [card = 12, expect = none]
    57 sorry
    58 
    59 lemma "fs (Pd p) = snd p"
    60 nitpick [expect = genuine]
    61 oops
    62 
    63 lemma "sn (Pd p) = snd p"
    64 nitpick [card = 12, expect = none]
    65 sorry
    66 
    67 lemma "sn (Pd p) = fst p"
    68 nitpick [expect = genuine]
    69 oops
    70 
    71 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    72 nitpick [card = 1\<midarrow>9, expect = none]
    73 sorry
    74 
    75 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    76 nitpick [expect = genuine]
    77 oops
    78 
    79 datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
    80 
    81 fun app where
    82 "app (Fn f) x = f x"
    83 
    84 lemma "app (Fn g) y = g y"
    85 nitpick [card = 1\<midarrow>10, expect = none]
    86 sorry
    87 
    88 lemma "app (Fn g) y = g' y"
    89 nitpick [expect = genuine]
    90 oops
    91 
    92 lemma "app (Fn g) y = g y'"
    93 nitpick [expect = genuine]
    94 oops
    95 
    96 end