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