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