# Theory Quickcheck_Lattice_Examples

theory Quickcheck_Lattice_Examples
imports Main
```(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
Author:     Lukas Bulwahn
*)

theory Quickcheck_Lattice_Examples
imports Main
begin

declare [[quickcheck_finite_type_size=5]]

text ‹We show how other default types help to find counterexamples to propositions if
the standard default type @{typ int} is insufficient.›

notation
less_eq  (infix "⊑" 50) and
less  (infix "⊏" 50) and
top ("⊤") and
bot ("⊥") and
inf (infixl "⊓" 70) and
sup (infixl "⊔" 65)

declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]

subsection ‹Distributive lattices›

lemma sup_inf_distrib2:
"((y :: 'a :: distrib_lattice) ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)"
quickcheck[expect = no_counterexample]

lemma sup_inf_distrib2_1:
"((y :: 'a :: lattice) ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)"
quickcheck[expect = counterexample]
oops

lemma sup_inf_distrib2_2:
"((y :: 'a :: distrib_lattice) ⊓ z') ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)"
quickcheck[expect = counterexample]
oops

lemma inf_sup_distrib1_1:
"(x :: 'a :: distrib_lattice) ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x' ⊓ z)"
quickcheck[expect = counterexample]
oops

lemma inf_sup_distrib2_1:
"((y :: 'a :: distrib_lattice) ⊔ z) ⊓ x = (y ⊓ x) ⊔ (y ⊓ x)"
quickcheck[expect = counterexample]
oops

subsection ‹Bounded lattices›

lemma inf_bot_left [simp]:
"⊥ ⊓ (x :: 'a :: bounded_lattice_bot) = ⊥"
quickcheck[expect = no_counterexample]
by (rule inf_absorb1) simp

lemma inf_bot_left_1:
"⊥ ⊓ (x :: 'a :: bounded_lattice_bot) = x"
quickcheck[expect = counterexample]
oops

lemma inf_bot_left_2:
"y ⊓ (x :: 'a :: bounded_lattice_bot) = ⊥"
quickcheck[expect = counterexample]
oops

lemma inf_bot_left_3:
"x ≠ ⊥ ==> y ⊓ (x :: 'a :: bounded_lattice_bot) ≠ ⊥"
quickcheck[expect = counterexample]
oops

lemma inf_bot_right [simp]:
"(x :: 'a :: bounded_lattice_bot) ⊓ ⊥ = ⊥"
quickcheck[expect = no_counterexample]
by (rule inf_absorb2) simp

lemma inf_bot_right_1:
"x ≠ ⊥ ==> (x :: 'a :: bounded_lattice_bot) ⊓ ⊥ = y"
quickcheck[expect = counterexample]
oops

lemma inf_bot_right_2:
"(x :: 'a :: bounded_lattice_bot) ⊓ ⊥ ~= ⊥"
quickcheck[expect = counterexample]
oops

lemma sup_bot_right [simp]:
"(x :: 'a :: bounded_lattice_bot) ⊔ ⊥ = ⊥"
quickcheck[expect = counterexample]
oops

lemma sup_bot_left [simp]:
"⊥ ⊔ (x :: 'a :: bounded_lattice_bot) = x"
quickcheck[expect = no_counterexample]
by (rule sup_absorb2) simp

lemma sup_bot_right_2 [simp]:
"(x :: 'a :: bounded_lattice_bot) ⊔ ⊥ = x"
quickcheck[expect = no_counterexample]
by (rule sup_absorb1) simp

lemma sup_eq_bot_iff [simp]:
"(x :: 'a :: bounded_lattice_bot) ⊔ y = ⊥ ⟷ x = ⊥ ∧ y = ⊥"
quickcheck[expect = no_counterexample]

lemma sup_top_left [simp]:
"⊤ ⊔ (x :: 'a :: bounded_lattice_top) = ⊤"
quickcheck[expect = no_counterexample]
by (rule sup_absorb1) simp

lemma sup_top_right [simp]:
"(x :: 'a :: bounded_lattice_top) ⊔ ⊤ = ⊤"
quickcheck[expect = no_counterexample]
by (rule sup_absorb2) simp

lemma inf_top_left [simp]:
"⊤ ⊓ x = (x :: 'a :: bounded_lattice_top)"
quickcheck[expect = no_counterexample]
by (rule inf_absorb2) simp

lemma inf_top_right [simp]:
"x ⊓ ⊤ = (x :: 'a :: bounded_lattice_top)"
quickcheck[expect = no_counterexample]
by (rule inf_absorb1) simp

lemma inf_eq_top_iff [simp]:
"(x :: 'a :: bounded_lattice_top) ⊓ y = ⊤ ⟷ x = ⊤ ∧ y = ⊤"
quickcheck[expect = no_counterexample]