82 lemma inf_bot_right_2: |
82 lemma inf_bot_right_2: |
83 "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>" |
83 "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>" |
84 quickcheck[expect = counterexample] |
84 quickcheck[expect = counterexample] |
85 oops |
85 oops |
86 |
86 |
87 lemma inf_bot_right [simp]: |
87 lemma sup_bot_right [simp]: |
88 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>" |
88 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>" |
89 quickcheck[expect = counterexample] |
89 quickcheck[expect = counterexample] |
90 oops |
90 oops |
91 |
91 |
92 lemma sup_bot_left [simp]: |
92 lemma sup_bot_left [simp]: |
93 "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x" |
93 "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x" |
94 quickcheck[expect = no_counterexample] |
94 quickcheck[expect = no_counterexample] |
95 by (rule sup_absorb2) simp |
95 by (rule sup_absorb2) simp |
96 |
96 |
97 lemma sup_bot_right [simp]: |
97 lemma sup_bot_right_2 [simp]: |
98 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x" |
98 "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x" |
99 quickcheck[expect = no_counterexample] |
99 quickcheck[expect = no_counterexample] |
100 by (rule sup_absorb1) simp |
100 by (rule sup_absorb1) simp |
101 |
101 |
102 lemma sup_eq_bot_iff [simp]: |
102 lemma sup_eq_bot_iff [simp]: |