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