(* Title: HOL/Nitpick_Examples/Record_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009, 2010
Examples featuring Nitpick applied to records.
*)
header {* 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