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