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;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
blanchet@33197
     4
blanchet@33197
     5
Examples featuring Nitpick applied to records.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Examples Featuring Nitpick Applied to Records *}
blanchet@33197
     9
blanchet@33197
    10
theory Record_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@35078
    14
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
blanchet@34083
    15
blanchet@33197
    16
record point2d =
blanchet@33197
    17
  xc :: int
blanchet@33197
    18
  yc :: int
blanchet@33197
    19
blanchet@33197
    20
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
blanchet@33197
    21
nitpick [expect = none]
blanchet@33197
    22
sorry
blanchet@33197
    23
blanchet@33197
    24
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    25
nitpick [expect = genuine]
blanchet@33197
    26
oops
blanchet@33197
    27
blanchet@33197
    28
lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
blanchet@33197
    29
nitpick [expect = genuine]
blanchet@33197
    30
oops
blanchet@33197
    31
blanchet@33197
    32
lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
blanchet@33197
    33
nitpick [expect = genuine]
blanchet@33197
    34
oops
blanchet@33197
    35
blanchet@33197
    36
record point3d = point2d +
blanchet@33197
    37
  zc :: int
blanchet@33197
    38
blanchet@33197
    39
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
blanchet@33197
    40
nitpick [expect = none]
blanchet@33197
    41
sorry
blanchet@33197
    42
blanchet@33197
    43
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    44
nitpick [expect = genuine]
blanchet@33197
    45
oops
blanchet@33197
    46
blanchet@33197
    47
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    48
nitpick [expect = genuine]
blanchet@33197
    49
oops
blanchet@33197
    50
blanchet@33197
    51
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
blanchet@33197
    52
nitpick [expect = genuine]
blanchet@33197
    53
oops
blanchet@33197
    54
blanchet@33197
    55
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
blanchet@33197
    56
nitpick [expect = genuine]
blanchet@33197
    57
oops
blanchet@33197
    58
blanchet@33197
    59
record point4d = point3d +
blanchet@33197
    60
  wc :: int
blanchet@33197
    61
blanchet@33197
    62
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
blanchet@33197
    63
nitpick [expect = none]
blanchet@33197
    64
sorry
blanchet@33197
    65
blanchet@33197
    66
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    67
nitpick [expect = genuine]
blanchet@33197
    68
oops
blanchet@33197
    69
blanchet@33197
    70
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    71
nitpick [expect = genuine]
blanchet@33197
    72
oops
blanchet@33197
    73
blanchet@33197
    74
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
blanchet@33197
    75
nitpick [expect = genuine]
blanchet@33197
    76
oops
blanchet@33197
    77
blanchet@33197
    78
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
blanchet@33197
    79
nitpick [expect = genuine]
blanchet@33197
    80
oops
blanchet@33197
    81
blanchet@33197
    82
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
blanchet@33197
    83
nitpick [expect = genuine]
blanchet@33197
    84
oops
blanchet@33197
    85
blanchet@33197
    86
end