isabelle: src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy@8b537e1af2ec (annotated)

46879 a8b1236e0837 tuned headers; wenzelm parents: 46585 diff changeset	1	(* Title: HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	2	Author: Lukas Bulwahn
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	3	Copyright 2010 TU Muenchen
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	4	*)
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	5
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	6	theory Quickcheck_Lattice_Examples
57921 9225b2761126 Quickcheck_Types is no longer needed due to 51aa30c9ee4e Andreas Lochbihler parents: 57573 diff changeset	7	imports Main
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	8	begin
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	9
57921 9225b2761126 Quickcheck_Types is no longer needed due to 51aa30c9ee4e Andreas Lochbihler parents: 57573 diff changeset	10	declare [[quickcheck_finite_type_size=5]]
9225b2761126 Quickcheck_Types is no longer needed due to 51aa30c9ee4e Andreas Lochbihler parents: 57573 diff changeset	11
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 57921 diff changeset	12	text \<open>We show how other default types help to find counterexamples to propositions if
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	13	the standard default type \<^typ>\<open>int\<close> is insufficient.\<close>
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	14
81132 dff7dfd8dce3 more robust declarations via "no syntax" bundles; wenzelm parents: 80914 diff changeset	15	unbundle lattice_syntax
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	16
44994 a915907a67d5 increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling bulwahn parents: 44845 diff changeset	17	declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
43888 ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 41413 diff changeset	18
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 57921 diff changeset	19	subsection \<open>Distributive lattices\<close>
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	20
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	21	lemma sup_inf_distrib2:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	22	"((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	23	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	24	by(simp add: inf_sup_aci sup_inf_distrib1)
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	25
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	26	lemma sup_inf_distrib2_1:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	27	"((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	28	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	29	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	30
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	31	lemma sup_inf_distrib2_2:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	32	"((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	33	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	34	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	35
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	36	lemma inf_sup_distrib1_1:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	37	"(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	38	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	39	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	40
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	41	lemma inf_sup_distrib2_1:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	42	"((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	43	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	44	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	45
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 57921 diff changeset	46	subsection \<open>Bounded lattices\<close>
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	47
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	48	lemma inf_bot_left [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	49	"\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	50	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	51	by (rule inf_absorb1) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	52
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	53	lemma inf_bot_left_1:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	54	"\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	55	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	56	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	57
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	58	lemma inf_bot_left_2:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	59	"y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	60	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	61	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	62
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	63	lemma inf_bot_left_3:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	64	"x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	65	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	66	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	67
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	68	lemma inf_bot_right [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	69	"(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	70	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	71	by (rule inf_absorb2) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	72
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	73	lemma inf_bot_right_1:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	74	"x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	75	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	76	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	77
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	78	lemma inf_bot_right_2:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	79	"(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	80	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	81	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	82
57573 2bfbeb0e69cd avoid duplicate fact name kleing parents: 46879 diff changeset	83	lemma sup_bot_right [simp]:
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	84	"(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	85	quickcheck[expect = counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	86	oops
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	87
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	88	lemma sup_bot_left [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	89	"\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	90	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	91	by (rule sup_absorb2) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	92
57573 2bfbeb0e69cd avoid duplicate fact name kleing parents: 46879 diff changeset	93	lemma sup_bot_right_2 [simp]:
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	94	"(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	95	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	96	by (rule sup_absorb1) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	97
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	98	lemma sup_eq_bot_iff [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	99	"(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	100	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	101	by (simp add: eq_iff)
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	102
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	103	lemma sup_top_left [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	104	"\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	105	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	106	by (rule sup_absorb1) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	107
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	108	lemma sup_top_right [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	109	"(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	110	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	111	by (rule sup_absorb2) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	112
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	113	lemma inf_top_left [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	114	"\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	115	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	116	by (rule inf_absorb2) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	117
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	118	lemma inf_top_right [simp]:
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	119	"x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	120	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	121	by (rule inf_absorb1) simp
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	122
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	123	lemma inf_eq_top_iff [simp]:
44845 5e51075cbd97 added syntactic classes for "inf" and "sup" krauss parents: 43888 diff changeset	124	"(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
37929 22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples bulwahn parents: 37916 diff changeset	125	quickcheck[expect = no_counterexample]
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	126	by (simp add: eq_iff)
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	127
81132 dff7dfd8dce3 more robust declarations via "no syntax" bundles; wenzelm parents: 80914 diff changeset	128	unbundle no lattice_syntax
37916 cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	129
cb55fd65faa6 adding Quickcheck examples for other quickcheck default types bulwahn parents: diff changeset	130	end

author	nipkow
	Tue, 17 Jun 2025 14:11:40 +0200
changeset 82733	8b537e1af2ec
parent 81132	dff7dfd8dce3
permissions	-rw-r--r--