isabelle: src/HOL/Nitpick_Examples/Record_Nits.thy@0909deb8059b (annotated)

33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	1	(* Title: HOL/Nitpick_Examples/Record_Nits.thy
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
45035 60d2c03d5c70 reintroduced Minipick as Nitpick example blanchet parents: 42959 diff changeset	3	Copyright 2009-2011
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	4
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	5	Examples featuring Nitpick applied to records.
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	6	*)
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	7
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	8	section \<open>Examples Featuring Nitpick Applied to Records\<close>
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	9
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	10	theory Record_Nits
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	11	imports Main
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	12	begin
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	13
55893 aed17a173d16 fixed handling of 'case_prod' and other 'case' functions for interpreted types blanchet parents: 54680 diff changeset	14	nitpick_params [verbose, card = 1-6, max_potential = 0,
54680 93f6d33a754e reverted 86e0b402994c, which was accidentally qfinish'ed and pushed blanchet parents: 54633 diff changeset	15	sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
34083 652719832159 make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits blanchet parents: 33197 diff changeset	16
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	17	record point2d =
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	18	xc :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	19	yc :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	20
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	21	lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	22	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	23	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	24
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	25	lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	26	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	27	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	28
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	29	lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	30	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	31	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	32
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	33	lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	34	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	35	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	36
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	37	record point3d = point2d +
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	38	zc :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	39
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	40	lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	41	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	42	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	43
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	44	lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	45	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	46	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	47
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	48	lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	49	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	50	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	51
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	52	lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	53	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	54	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	55
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	56	lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	57	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	58	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	59
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	60	record point4d = point3d +
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	61	wc :: int
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	62
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	63	lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	64	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	65	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	66
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	67	lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	68	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	69	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	70
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	71	lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	72	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	73	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	74
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	75	lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	76	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	77	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	78
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	79	lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	80	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	81	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	82
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	83	lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	84	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	85	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	86
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	87	end

author	wenzelm
	Thu, 26 May 2016 17:51:22 +0200
changeset 63167	0909deb8059b
parent 58889	5b7a9633cfa8
child 74641	6f801e1073fa
permissions	-rw-r--r--