src/HOL/Nitpick_Examples/Datatype_Nits.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 63167 0909deb8059b
permissions -rw-r--r--
tuned: each session has at most one defining entry;
     1 (*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2011
     4 
     5 Examples featuring Nitpick applied to datatypes.
     6 *)
     7 
     8 section \<open>Examples Featuring Nitpick Applied to Datatypes\<close>
     9 
    10 theory Datatype_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 1-8, max_potential = 0,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    16 
    17 datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3
    18   | Nibble4 | Nibble5 | Nibble6 | Nibble7
    19   | Nibble8 | Nibble9 | NibbleA | NibbleB
    20   | NibbleC | NibbleD | NibbleE | NibbleF
    21 
    22 primrec rot where
    23 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    24 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
    25 "rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
    26 "rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
    27 "rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
    28 "rot NibbleF = Nibble0"
    29 
    30 lemma "rot n \<noteq> n"
    31 nitpick [card = 1-8,16, verbose, expect = none]
    32 sorry
    33 
    34 lemma "rot Nibble2 \<noteq> Nibble3"
    35 nitpick [card = 1, expect = none]
    36 nitpick [card = 2, max Nibble4 = 0, expect = genuine]
    37 nitpick [card = 2, max Nibble2 = 0, expect = none]
    38 oops
    39 
    40 lemma "(rot ^^ 15) n \<noteq> n"
    41 nitpick [card = 17, expect = none]
    42 sorry
    43 
    44 lemma "(rot ^^ 15) n = n"
    45 nitpick [card = 17, expect = genuine]
    46 oops
    47 
    48 lemma "(rot ^^ 16) n = n"
    49 nitpick [card = 17, expect = none]
    50 oops
    51 
    52 datatype ('a, 'b) pd = Pd "'a \<times> 'b"
    53 
    54 fun fs where
    55 "fs (Pd (a, _)) = a"
    56 
    57 fun sn where
    58 "sn (Pd (_, b)) = b"
    59 
    60 lemma "fs (Pd p) = fst p"
    61 nitpick [card = 12, expect = none]
    62 sorry
    63 
    64 lemma "fs (Pd p) = snd p"
    65 nitpick [expect = genuine]
    66 oops
    67 
    68 lemma "sn (Pd p) = snd p"
    69 nitpick [card = 12, expect = none]
    70 sorry
    71 
    72 lemma "sn (Pd p) = fst p"
    73 nitpick [expect = genuine]
    74 oops
    75 
    76 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    77 nitpick [expect = none]
    78 sorry
    79 
    80 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    81 nitpick [expect = genuine]
    82 oops
    83 
    84 datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
    85 
    86 fun app where
    87 "app (Fn f) x = f x"
    88 
    89 lemma "app (Fn g) y = g y"
    90 nitpick [expect = none]
    91 sorry
    92 
    93 lemma "app (Fn g) y = g' y"
    94 nitpick [expect = genuine]
    95 oops
    96 
    97 lemma "app (Fn g) y = g y'"
    98 nitpick [expect = genuine]
    99 oops
   100 
   101 end