(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

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, 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