src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46879 a8b1236e0837 child 57573 2bfbeb0e69cd permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
```     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
```