Theory Quickcheck_Lattice_Examples

(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
    Author:     Lukas Bulwahn
    Copyright   2010 TU Muenchen
*)

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]
by(simp add: inf_sup_aci sup_inf_distrib1)

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]
  by (simp add: eq_iff)

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]
  by (simp add: eq_iff)


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

end