# Theory Record_Nits

theory Record_Nits
imports Main
```(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
Author:     Jasmin Blanchette, TU Muenchen

Examples featuring Nitpick applied to records.
*)

section ‹Examples Featuring Nitpick Applied to Records›

theory Record_Nits
imports Main
begin

nitpick_params [verbose, card = 1-6, max_potential = 0,
sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]

record point2d =
xc :: int
yc :: int

lemma "⦇xc = x, yc = y⦈ = p⦇xc := x, yc := y⦈"
nitpick [expect = none]
sorry

lemma "⦇xc = x, yc = y⦈ = p⦇xc := x⦈"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y⦈ ≠ p"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y⦈ = p"
nitpick [expect = genuine]
oops

record point3d = point2d +
zc :: int

lemma "⦇xc = x, yc = y, zc = z⦈ = p⦇xc := x, yc := y, zc := z⦈"
nitpick [expect = none]
sorry

lemma "⦇xc = x, yc = y, zc = z⦈ = p⦇xc := x⦈"
nitpick [expect = genuine]
oops

lemma "⦇xc = x, yc = y, zc = z⦈ = p⦇zc := z⦈"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y, zc := z⦈ ≠ p"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y, zc := z⦈ = p"
nitpick [expect = genuine]
oops

record point4d = point3d +
wc :: int

lemma "⦇xc = x, yc = y, zc = z, wc = w⦈ = p⦇xc := x, yc := y, zc := z, wc := w⦈"
nitpick [expect = none]
sorry

lemma "⦇xc = x, yc = y, zc = z, wc = w⦈ = p⦇xc := x⦈"
nitpick [expect = genuine]
oops

lemma "⦇xc = x, yc = y, zc = z, wc = w⦈ = p⦇zc := z⦈"
nitpick [expect = genuine]
oops

lemma "⦇xc = x, yc = y, zc = z, wc = w⦈ = p⦇wc := w⦈"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y, zc := z, wc := w⦈ ≠ p"
nitpick [expect = genuine]
oops

lemma "p⦇xc := x, yc := y, zc := z, wc := w⦈ = p"
nitpick [expect = genuine]
oops

end
```