src/HOL/Nitpick_Examples/Record_Nits.thy
author blanchet
Mon Dec 14 10:59:46 2009 +0100 (2009-12-14)
changeset 34083 652719832159
parent 33197 de6285ebcc05
child 35076 cc19e2aef17e
permissions -rw-r--r--
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
     1 (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009
     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 [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
    15 
    16 record point2d =
    17   xc :: int
    18   yc :: int
    19 
    20 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
    21 nitpick [expect = none]
    22 sorry
    23 
    24 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
    25 nitpick [expect = genuine]
    26 oops
    27 
    28 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
    29 nitpick [expect = genuine]
    30 oops
    31 
    32 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
    33 nitpick [expect = genuine]
    34 oops
    35 
    36 record point3d = point2d +
    37   zc :: int
    38 
    39 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
    40 nitpick [expect = none]
    41 sorry
    42 
    43 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
    44 nitpick [expect = genuine]
    45 oops
    46 
    47 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
    48 nitpick [expect = genuine]
    49 oops
    50 
    51 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
    52 nitpick [expect = genuine]
    53 oops
    54 
    55 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
    56 nitpick [expect = genuine]
    57 oops
    58 
    59 record point4d = point3d +
    60   wc :: int
    61 
    62 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
    63 nitpick [expect = none]
    64 sorry
    65 
    66 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
    67 nitpick [expect = genuine]
    68 oops
    69 
    70 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
    71 nitpick [expect = genuine]
    72 oops
    73 
    74 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
    75 nitpick [expect = genuine]
    76 oops
    77 
    78 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
    79 nitpick [expect = genuine]
    80 oops
    81 
    82 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
    83 nitpick [expect = genuine]
    84 oops
    85 
    86 end