src/HOL/Nitpick_Examples/Datatype_Nits.thy
author blanchet
Fri Dec 18 12:00:29 2009 +0100 (2009-12-18)
changeset 34126 8a2c5d7aff51
parent 34083 652719832159
child 35076 cc19e2aef17e
permissions -rw-r--r--
polished Nitpick's binary integer support etc.;
etc. = improve inconsistent scope correction + sort values nicely in output
+ handle "mod" using the characterization "x mod y = x - x div y * y"
(instead of explicit code in Nitpick)
+ introduce KK = Kodkod as abbreviation
     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 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
    15 
    16 primrec rot where
    17 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    18 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
    19 "rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
    20 "rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
    21 "rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
    22 "rot NibbleF = Nibble0"
    23 
    24 lemma "rot n \<noteq> n"
    25 nitpick [card = 1\<midarrow>16, expect = none]
    26 sorry
    27 
    28 lemma "rot Nibble2 \<noteq> Nibble3"
    29 nitpick [card = 1, expect = none]
    30 nitpick [card = 2, expect = genuine]
    31 nitpick [card = 2, max Nibble2 = 0, expect = none]
    32 nitpick [card = 2, max Nibble3 = 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 = 20, 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 = 20, 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>12, 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>12, 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