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