src/HOL/Nitpick_Examples/Record_Nits.thy
author blanchet
Fri Oct 23 18:59:24 2009 +0200 (2009-10-23)
changeset 33197 de6285ebcc05
child 34083 652719832159
permissions -rw-r--r--
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33197
     3
    Copyright   2009
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@33197
    14
record point2d =
blanchet@33197
    15
  xc :: int
blanchet@33197
    16
  yc :: int
blanchet@33197
    17
blanchet@33197
    18
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
blanchet@33197
    19
nitpick [expect = none]
blanchet@33197
    20
sorry
blanchet@33197
    21
blanchet@33197
    22
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    23
nitpick [expect = genuine]
blanchet@33197
    24
oops
blanchet@33197
    25
blanchet@33197
    26
lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
blanchet@33197
    27
nitpick [expect = genuine]
blanchet@33197
    28
oops
blanchet@33197
    29
blanchet@33197
    30
lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
blanchet@33197
    31
nitpick [expect = genuine]
blanchet@33197
    32
oops
blanchet@33197
    33
blanchet@33197
    34
record point3d = point2d +
blanchet@33197
    35
  zc :: int
blanchet@33197
    36
blanchet@33197
    37
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
blanchet@33197
    38
nitpick [expect = none]
blanchet@33197
    39
sorry
blanchet@33197
    40
blanchet@33197
    41
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    42
nitpick [expect = genuine]
blanchet@33197
    43
oops
blanchet@33197
    44
blanchet@33197
    45
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    46
nitpick [expect = genuine]
blanchet@33197
    47
oops
blanchet@33197
    48
blanchet@33197
    49
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
blanchet@33197
    50
nitpick [expect = genuine]
blanchet@33197
    51
oops
blanchet@33197
    52
blanchet@33197
    53
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
blanchet@33197
    54
nitpick [expect = genuine]
blanchet@33197
    55
oops
blanchet@33197
    56
blanchet@33197
    57
record point4d = point3d +
blanchet@33197
    58
  wc :: int
blanchet@33197
    59
blanchet@33197
    60
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
blanchet@33197
    61
nitpick [expect = none]
blanchet@33197
    62
sorry
blanchet@33197
    63
blanchet@33197
    64
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    65
nitpick [expect = genuine]
blanchet@33197
    66
oops
blanchet@33197
    67
blanchet@33197
    68
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    69
nitpick [expect = genuine]
blanchet@33197
    70
oops
blanchet@33197
    71
blanchet@33197
    72
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
blanchet@33197
    73
nitpick [expect = genuine]
blanchet@33197
    74
oops
blanchet@33197
    75
blanchet@33197
    76
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
blanchet@33197
    77
nitpick [expect = genuine]
blanchet@33197
    78
oops
blanchet@33197
    79
blanchet@33197
    80
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
blanchet@33197
    81
nitpick [expect = genuine]
blanchet@33197
    82
oops
blanchet@33197
    83
blanchet@33197
    84
end