|
1 (* Title: HOL/ex/Quickcheck_Lattice_Examples.thy |
|
2 Author: Lukas Bulwahn |
|
3 Copyright 2010 TU Muenchen |
|
4 *) |
|
5 |
|
6 theory Quickcheck_Lattice_Examples |
|
7 imports "~~/src/HOL/Library/Quickcheck_Types" |
|
8 begin |
|
9 |
|
10 text {* We show how other default types help to find counterexamples to propositions if |
|
11 the standard default type @{typ int} is insufficient. *} |
|
12 |
|
13 notation |
|
14 less_eq (infix "\<sqsubseteq>" 50) and |
|
15 less (infix "\<sqsubset>" 50) and |
|
16 top ("\<top>") and |
|
17 bot ("\<bottom>") and |
|
18 inf (infixl "\<sqinter>" 70) and |
|
19 sup (infixl "\<squnion>" 65) |
|
20 |
|
21 declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]] |
|
22 |
|
23 subsection {* Distributive lattices *} |
|
24 |
|
25 lemma sup_inf_distrib2: |
|
26 "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
|
27 quickcheck[expect = no_counterexample] |
|
28 by(simp add: inf_sup_aci sup_inf_distrib1) |
|
29 |
|
30 lemma sup_inf_distrib2_1: |
|
31 "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
|
32 quickcheck[expect = counterexample] |
|
33 oops |
|
34 |
|
35 lemma sup_inf_distrib2_2: |
|
36 "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
|
37 quickcheck[expect = counterexample] |
|
38 oops |
|
39 |
|
40 lemma inf_sup_distrib1_1: |
|
41 "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)" |
|
42 quickcheck[expect = counterexample] |
|
43 oops |
|
44 |
|
45 lemma inf_sup_distrib2_1: |
|
46 "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)" |
|
47 quickcheck[expect = counterexample] |
|
48 oops |
|
49 |
|
50 subsection {* Bounded lattices *} |
|
51 |
|
52 lemma inf_bot_left [simp]: |
|
53 "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>" |
|
54 quickcheck[expect = no_counterexample] |
|
55 by (rule inf_absorb1) simp |
|
56 |
|
57 lemma inf_bot_left_1: |
|
58 "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x" |
|
59 quickcheck[expect = counterexample] |
|
60 oops |
|
61 |
|
62 lemma inf_bot_left_2: |
|
63 "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>" |
|
64 quickcheck[expect = counterexample] |
|
65 oops |
|
66 |
|
67 lemma inf_bot_left_3: |
|
68 "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>" |
|
69 quickcheck[expect = counterexample] |
|
70 oops |
|
71 |
|
72 lemma inf_bot_right [simp]: |
|
73 "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>" |
|
74 quickcheck[expect = no_counterexample] |
|
75 by (rule inf_absorb2) simp |
|
76 |
|
77 lemma inf_bot_right_1: |
|
78 "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y" |
|
79 quickcheck[expect = counterexample] |
|
80 oops |
|
81 |
|
82 lemma inf_bot_right_2: |
|
83 "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>" |
|
84 quickcheck[expect = counterexample] |
|
85 oops |
|
86 |
|
87 lemma inf_bot_right [simp]: |
|
88 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>" |
|
89 quickcheck[expect = counterexample] |
|
90 oops |
|
91 |
|
92 lemma sup_bot_left [simp]: |
|
93 "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x" |
|
94 quickcheck[expect = no_counterexample] |
|
95 by (rule sup_absorb2) simp |
|
96 |
|
97 lemma sup_bot_right [simp]: |
|
98 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x" |
|
99 quickcheck[expect = no_counterexample] |
|
100 by (rule sup_absorb1) simp |
|
101 |
|
102 lemma sup_eq_bot_iff [simp]: |
|
103 "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
104 quickcheck[expect = no_counterexample] |
|
105 by (simp add: eq_iff) |
|
106 |
|
107 lemma sup_top_left [simp]: |
|
108 "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>" |
|
109 quickcheck[expect = no_counterexample] |
|
110 by (rule sup_absorb1) simp |
|
111 |
|
112 lemma sup_top_right [simp]: |
|
113 "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>" |
|
114 quickcheck[expect = no_counterexample] |
|
115 by (rule sup_absorb2) simp |
|
116 |
|
117 lemma inf_top_left [simp]: |
|
118 "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)" |
|
119 quickcheck[expect = no_counterexample] |
|
120 by (rule inf_absorb2) simp |
|
121 |
|
122 lemma inf_top_right [simp]: |
|
123 "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)" |
|
124 quickcheck[expect = no_counterexample] |
|
125 by (rule inf_absorb1) simp |
|
126 |
|
127 lemma inf_eq_top_iff [simp]: |
|
128 "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
129 quickcheck[expect = no_counterexample] |
|
130 by (simp add: eq_iff) |
|
131 |
|
132 |
|
133 no_notation |
|
134 less_eq (infix "\<sqsubseteq>" 50) and |
|
135 less (infix "\<sqsubset>" 50) and |
|
136 inf (infixl "\<sqinter>" 70) and |
|
137 sup (infixl "\<squnion>" 65) and |
|
138 top ("\<top>") and |
|
139 bot ("\<bottom>") |
|
140 |
|
141 end |