isabelle: src/HOL/Nitpick_Examples/Induct_Nits.thy@9943f8067f11 (annotated)

33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	1	(* Title: HOL/Nitpick_Examples/Induct_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 (co)inductive definitions.
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	8	header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
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 Induct_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
42959 ee829022381d use \<emdash> rather than \<midarrow> blanchet parents: 42208 diff changeset	14	nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
42208 02513eb26eb7 raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics. krauss parents: 41278 diff changeset	15	sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	16
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	17	inductive p1 :: "nat \<Rightarrow> bool" where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	18	"p1 0" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	19	"p1 n \<Longrightarrow> p1 (n + 2)"
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	coinductive q1 :: "nat \<Rightarrow> bool" where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	22	"q1 0" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	23	"q1 n \<Longrightarrow> q1 (n + 2)"
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 "p1 = q1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	26	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	27	nitpick [wf, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	28	nitpick [non_wf, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	29	nitpick [non_wf, dont_star_linear_preds, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	30	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	31
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	32	lemma "p1 \<noteq> q1"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	33	nitpick [expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	34	nitpick [wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	35	nitpick [non_wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	36	nitpick [non_wf, dont_star_linear_preds, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	37	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	38
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	39	lemma "p1 (n - 2) \<Longrightarrow> p1 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	40	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	41	nitpick [non_wf, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	42	nitpick [non_wf, dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	43	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	44
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	45	lemma "q1 (n - 2) \<Longrightarrow> q1 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	46	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	47	nitpick [non_wf, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	48	nitpick [non_wf, dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	49	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	50
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	51	inductive p2 :: "nat \<Rightarrow> bool" where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	52	"p2 n \<Longrightarrow> p2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	53
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	54	coinductive q2 :: "nat \<Rightarrow> bool" where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	55	"q2 n \<Longrightarrow> q2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	56
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	57	lemma "p2 = bot"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	58	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	59	nitpick [dont_star_linear_preds, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	60	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	61
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	62	lemma "q2 = bot"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	63	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	64	nitpick [dont_star_linear_preds, expect = genuine]
35671 ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1" blanchet parents: 35078 diff changeset	65	nitpick [wf, expect = quasi_genuine]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	66	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	67
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	68	lemma "p2 = top"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	69	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	70	nitpick [dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	71	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	72
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	73	lemma "q2 = top"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	74	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	75	nitpick [dont_star_linear_preds, expect = none]
35671 ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1" blanchet parents: 35078 diff changeset	76	nitpick [wf, expect = quasi_genuine]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	77	sorry
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 "p2 = q2"
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	nitpick [dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	82	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	83
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	84	lemma "p2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	85	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	86	nitpick [dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	87	nitpick [dont_specialize, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	88	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	89
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	90	lemma "q2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	91	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	92	nitpick [dont_star_linear_preds, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	93	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	94
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	95	lemma "\<not> p2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	96	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	97	nitpick [dont_star_linear_preds, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	98	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	99
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	100	lemma "\<not> q2 n"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	101	nitpick [expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	102	nitpick [dont_star_linear_preds, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	103	nitpick [dont_specialize, expect = genuine]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	104	oops
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	105
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	106	inductive p3 and p4 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	107	"p3 0" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	108	"p3 n \<Longrightarrow> p4 (Suc n)" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	109	"p4 n \<Longrightarrow> p3 (Suc n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	110
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	111	coinductive q3 and q4 where
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	112	"q3 0" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	113	"q3 n \<Longrightarrow> q4 (Suc n)" \|
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	114	"q4 n \<Longrightarrow> q3 (Suc n)"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	115
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	116	lemma "p3 = q3"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	117	nitpick [expect = none]
38186 c28018f5a1d6 example tweaking -- also prevents Nitpick_Tests from using more than 1 thread blanchet parents: 38185 diff changeset	118	nitpick [non_wf, expect = none]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	119	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	120
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	121	lemma "p4 = q4"
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	122	nitpick [expect = none]
38186 c28018f5a1d6 example tweaking -- also prevents Nitpick_Tests from using more than 1 thread blanchet parents: 38185 diff changeset	123	nitpick [non_wf, expect = none]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	124	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	125
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	126	lemma "p3 = top - p4"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	127	nitpick [expect = none]
38186 c28018f5a1d6 example tweaking -- also prevents Nitpick_Tests from using more than 1 thread blanchet parents: 38185 diff changeset	128	nitpick [non_wf, expect = none]
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	129	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	130
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	131	lemma "q3 = top - q4"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	132	nitpick [expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	133	nitpick [non_wf, expect = none]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	134	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	135
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	136	lemma "inf p3 q4 \<noteq> bot"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	137	nitpick [expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	138	nitpick [non_wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	139	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	140
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	141	lemma "inf q3 p4 \<noteq> bot"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	142	nitpick [expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	143	nitpick [non_wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	144	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	145
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	146	lemma "sup p3 q4 \<noteq> top"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	147	nitpick [expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	148	nitpick [non_wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	149	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	150
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45035 diff changeset	151	lemma "sup q3 p4 \<noteq> top"
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	152	nitpick [expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	153	nitpick [non_wf, expect = potential]
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	154	sorry
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	155
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: diff changeset	156	end

author	wenzelm
	Sat, 25 May 2013 17:40:44 +0200
changeset 52147	9943f8067f11
parent 45970	b6d0cff57d96
child 54633	86e0b402994c
permissions	-rw-r--r--