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