src/HOL/Nitpick_Examples/Record_Nits.thy
author blanchet
Tue Aug 03 17:43:15 2010 +0200 (2010-08-03)
changeset 38185 b51677438b3a
parent 35284 9edc2bd6d2bd
child 40341 03156257040f
permissions -rw-r--r--
speed up Nitpick examples a little bit
     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 [card = 1\<midarrow>6, max_potential = 0,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    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