src/HOL/ex/Quickcheck_Lattice_Examples.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 37929 22e0797857e6
child 43888 ee4be704c2a4
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
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@37916
    21
subsection {* Distributive lattices *}
bulwahn@37916
    22
bulwahn@37916
    23
lemma sup_inf_distrib2:
bulwahn@37916
    24
 "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
bulwahn@37929
    25
  quickcheck[expect = no_counterexample]
bulwahn@37916
    26
by(simp add: inf_sup_aci sup_inf_distrib1)
bulwahn@37916
    27
bulwahn@37916
    28
lemma sup_inf_distrib2_1:
bulwahn@37916
    29
 "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
bulwahn@37929
    30
  quickcheck[expect = counterexample]
bulwahn@37916
    31
  oops
bulwahn@37916
    32
bulwahn@37916
    33
lemma sup_inf_distrib2_2:
bulwahn@37916
    34
 "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
bulwahn@37929
    35
  quickcheck[expect = counterexample]
bulwahn@37916
    36
  oops
bulwahn@37916
    37
bulwahn@37916
    38
lemma inf_sup_distrib1_1:
bulwahn@37916
    39
 "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
bulwahn@37929
    40
  quickcheck[expect = counterexample]
bulwahn@37916
    41
  oops
bulwahn@37916
    42
bulwahn@37916
    43
lemma inf_sup_distrib2_1:
bulwahn@37916
    44
 "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
bulwahn@37929
    45
  quickcheck[expect = counterexample]
bulwahn@37916
    46
  oops
bulwahn@37916
    47
bulwahn@37916
    48
subsection {* Bounded lattices *}
bulwahn@37916
    49
bulwahn@37916
    50
lemma inf_bot_left [simp]:
bulwahn@37916
    51
  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
bulwahn@37929
    52
  quickcheck[expect = no_counterexample]
bulwahn@37916
    53
  by (rule inf_absorb1) simp
bulwahn@37916
    54
bulwahn@37916
    55
lemma inf_bot_left_1:
bulwahn@37916
    56
  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
bulwahn@37929
    57
  quickcheck[expect = counterexample]
bulwahn@37916
    58
  oops
bulwahn@37916
    59
bulwahn@37916
    60
lemma inf_bot_left_2:
bulwahn@37916
    61
  "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
bulwahn@37929
    62
  quickcheck[expect = counterexample]
bulwahn@37916
    63
  oops
bulwahn@37916
    64
bulwahn@37916
    65
lemma inf_bot_left_3:
bulwahn@37916
    66
  "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
bulwahn@37929
    67
  quickcheck[expect = counterexample]
bulwahn@37916
    68
  oops
bulwahn@37916
    69
bulwahn@37916
    70
lemma inf_bot_right [simp]:
bulwahn@37916
    71
  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
bulwahn@37929
    72
  quickcheck[expect = no_counterexample]
bulwahn@37916
    73
  by (rule inf_absorb2) simp
bulwahn@37916
    74
bulwahn@37916
    75
lemma inf_bot_right_1:
bulwahn@37916
    76
  "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
bulwahn@37929
    77
  quickcheck[expect = counterexample]
bulwahn@37916
    78
  oops
bulwahn@37916
    79
bulwahn@37916
    80
lemma inf_bot_right_2:
bulwahn@37916
    81
  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
bulwahn@37929
    82
  quickcheck[expect = counterexample]
bulwahn@37916
    83
  oops
bulwahn@37916
    84
bulwahn@37916
    85
lemma inf_bot_right [simp]:
bulwahn@37916
    86
  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
bulwahn@37929
    87
  quickcheck[expect = counterexample]
bulwahn@37916
    88
  oops
bulwahn@37916
    89
bulwahn@37916
    90
lemma sup_bot_left [simp]:
bulwahn@37916
    91
  "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
bulwahn@37929
    92
  quickcheck[expect = no_counterexample]
bulwahn@37916
    93
  by (rule sup_absorb2) simp
bulwahn@37916
    94
bulwahn@37916
    95
lemma sup_bot_right [simp]:
bulwahn@37916
    96
  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
bulwahn@37929
    97
  quickcheck[expect = no_counterexample]
bulwahn@37916
    98
  by (rule sup_absorb1) simp
bulwahn@37916
    99
bulwahn@37916
   100
lemma sup_eq_bot_iff [simp]:
bulwahn@37916
   101
  "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
bulwahn@37929
   102
  quickcheck[expect = no_counterexample]
bulwahn@37916
   103
  by (simp add: eq_iff)
bulwahn@37916
   104
bulwahn@37916
   105
lemma sup_top_left [simp]:
bulwahn@37916
   106
  "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
bulwahn@37929
   107
  quickcheck[expect = no_counterexample]
bulwahn@37916
   108
  by (rule sup_absorb1) simp
bulwahn@37916
   109
bulwahn@37916
   110
lemma sup_top_right [simp]:
bulwahn@37916
   111
  "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
bulwahn@37929
   112
  quickcheck[expect = no_counterexample]
bulwahn@37916
   113
  by (rule sup_absorb2) simp
bulwahn@37916
   114
bulwahn@37916
   115
lemma inf_top_left [simp]:
bulwahn@37916
   116
  "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
bulwahn@37929
   117
  quickcheck[expect = no_counterexample]
bulwahn@37916
   118
  by (rule inf_absorb2) simp
bulwahn@37916
   119
bulwahn@37916
   120
lemma inf_top_right [simp]:
bulwahn@37916
   121
  "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
bulwahn@37929
   122
  quickcheck[expect = no_counterexample]
bulwahn@37916
   123
  by (rule inf_absorb1) simp
bulwahn@37916
   124
bulwahn@37916
   125
lemma inf_eq_top_iff [simp]:
bulwahn@37916
   126
  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
bulwahn@37929
   127
  quickcheck[expect = no_counterexample]
bulwahn@37916
   128
  by (simp add: eq_iff)
bulwahn@37916
   129
bulwahn@37916
   130
bulwahn@37916
   131
no_notation
bulwahn@37916
   132
  less_eq  (infix "\<sqsubseteq>" 50) and
bulwahn@37916
   133
  less (infix "\<sqsubset>" 50) and
bulwahn@37916
   134
  inf  (infixl "\<sqinter>" 70) and
bulwahn@37916
   135
  sup  (infixl "\<squnion>" 65) and
bulwahn@37916
   136
  top ("\<top>") and
bulwahn@37916
   137
  bot ("\<bottom>")
bulwahn@37916
   138
bulwahn@37916
   139
end