src/HOL/Nitpick_Examples/Record_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35284 9edc2bd6d2bd
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 [sat_solver = MiniSat_JNI, 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