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 typint 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