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
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@38185
    14
nitpick_params [card = 1\<midarrow>6, max_potential = 0,
blanchet@38185
    15
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
blanchet@34083
    16
blanchet@33197
    17
record point2d =
blanchet@33197
    18
  xc :: int
blanchet@33197
    19
  yc :: int
blanchet@33197
    20
blanchet@33197
    21
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
blanchet@33197
    22
nitpick [expect = none]
blanchet@33197
    23
sorry
blanchet@33197
    24
blanchet@33197
    25
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    26
nitpick [expect = genuine]
blanchet@33197
    27
oops
blanchet@33197
    28
blanchet@33197
    29
lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
blanchet@33197
    30
nitpick [expect = genuine]
blanchet@33197
    31
oops
blanchet@33197
    32
blanchet@33197
    33
lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
blanchet@33197
    34
nitpick [expect = genuine]
blanchet@33197
    35
oops
blanchet@33197
    36
blanchet@33197
    37
record point3d = point2d +
blanchet@33197
    38
  zc :: int
blanchet@33197
    39
blanchet@33197
    40
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
blanchet@33197
    41
nitpick [expect = none]
blanchet@33197
    42
sorry
blanchet@33197
    43
blanchet@33197
    44
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    45
nitpick [expect = genuine]
blanchet@33197
    46
oops
blanchet@33197
    47
blanchet@33197
    48
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    49
nitpick [expect = genuine]
blanchet@33197
    50
oops
blanchet@33197
    51
blanchet@33197
    52
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
blanchet@33197
    53
nitpick [expect = genuine]
blanchet@33197
    54
oops
blanchet@33197
    55
blanchet@33197
    56
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
blanchet@33197
    57
nitpick [expect = genuine]
blanchet@33197
    58
oops
blanchet@33197
    59
blanchet@33197
    60
record point4d = point3d +
blanchet@33197
    61
  wc :: int
blanchet@33197
    62
blanchet@33197
    63
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
blanchet@33197
    64
nitpick [expect = none]
blanchet@33197
    65
sorry
blanchet@33197
    66
blanchet@33197
    67
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
blanchet@33197
    68
nitpick [expect = genuine]
blanchet@33197
    69
oops
blanchet@33197
    70
blanchet@33197
    71
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
blanchet@33197
    72
nitpick [expect = genuine]
blanchet@33197
    73
oops
blanchet@33197
    74
blanchet@33197
    75
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
blanchet@33197
    76
nitpick [expect = genuine]
blanchet@33197
    77
oops
blanchet@33197
    78
blanchet@33197
    79
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
blanchet@33197
    80
nitpick [expect = genuine]
blanchet@33197
    81
oops
blanchet@33197
    82
blanchet@33197
    83
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
blanchet@33197
    84
nitpick [expect = genuine]
blanchet@33197
    85
oops
blanchet@33197
    86
blanchet@33197
    87
end