src/HOL/Nitpick_Examples/Record_Nits.thy
author krauss
Mon Apr 04 09:32:50 2011 +0200 (2011-04-04)
changeset 42208 02513eb26eb7
parent 41278 8e1cde88aae6
child 42959 ee829022381d
permissions -rw-r--r--
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
     1 (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Examples featuring Nitpick applied to records.
     6 *)
     7 
     8 header {* Examples Featuring Nitpick Applied to Records *}
     9 
    10 theory Record_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    16 
    17 record point2d =
    18   xc :: int
    19   yc :: int
    20 
    21 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
    22 nitpick [expect = none]
    23 sorry
    24 
    25 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
    26 nitpick [expect = genuine]
    27 oops
    28 
    29 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
    30 nitpick [expect = genuine]
    31 oops
    32 
    33 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
    34 nitpick [expect = genuine]
    35 oops
    36 
    37 record point3d = point2d +
    38   zc :: int
    39 
    40 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
    41 nitpick [expect = none]
    42 sorry
    43 
    44 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
    45 nitpick [expect = genuine]
    46 oops
    47 
    48 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
    49 nitpick [expect = genuine]
    50 oops
    51 
    52 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
    53 nitpick [expect = genuine]
    54 oops
    55 
    56 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
    57 nitpick [expect = genuine]
    58 oops
    59 
    60 record point4d = point3d +
    61   wc :: int
    62 
    63 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
    64 nitpick [expect = none]
    65 sorry
    66 
    67 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
    68 nitpick [expect = genuine]
    69 oops
    70 
    71 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
    72 nitpick [expect = genuine]
    73 oops
    74 
    75 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
    76 nitpick [expect = genuine]
    77 oops
    78 
    79 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
    80 nitpick [expect = genuine]
    81 oops
    82 
    83 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
    84 nitpick [expect = genuine]
    85 oops
    86 
    87 end