src/HOL/ex/Quickcheck_Lattice_Examples.thy
changeset 37929 22e0797857e6
parent 37916 cb55fd65faa6
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Jul 21 18:13:15 2010 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Jul 21 19:21:07 2010 +0200
     1.3 @@ -22,109 +22,109 @@
     1.4  
     1.5  lemma sup_inf_distrib2:
     1.6   "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
     1.7 -  quickcheck
     1.8 +  quickcheck[expect = no_counterexample]
     1.9  by(simp add: inf_sup_aci sup_inf_distrib1)
    1.10  
    1.11  lemma sup_inf_distrib2_1:
    1.12   "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    1.13 -  quickcheck
    1.14 +  quickcheck[expect = counterexample]
    1.15    oops
    1.16  
    1.17  lemma sup_inf_distrib2_2:
    1.18   "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    1.19 -  quickcheck
    1.20 +  quickcheck[expect = counterexample]
    1.21    oops
    1.22  
    1.23  lemma inf_sup_distrib1_1:
    1.24   "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
    1.25 -  quickcheck
    1.26 +  quickcheck[expect = counterexample]
    1.27    oops
    1.28  
    1.29  lemma inf_sup_distrib2_1:
    1.30   "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
    1.31 -  quickcheck
    1.32 +  quickcheck[expect = counterexample]
    1.33    oops
    1.34  
    1.35  subsection {* Bounded lattices *}
    1.36  
    1.37  lemma inf_bot_left [simp]:
    1.38    "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    1.39 -  quickcheck
    1.40 +  quickcheck[expect = no_counterexample]
    1.41    by (rule inf_absorb1) simp
    1.42  
    1.43  lemma inf_bot_left_1:
    1.44    "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
    1.45 -  quickcheck
    1.46 +  quickcheck[expect = counterexample]
    1.47    oops
    1.48  
    1.49  lemma inf_bot_left_2:
    1.50    "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    1.51 -  quickcheck
    1.52 +  quickcheck[expect = counterexample]
    1.53    oops
    1.54  
    1.55  lemma inf_bot_left_3:
    1.56    "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
    1.57 -  quickcheck
    1.58 +  quickcheck[expect = counterexample]
    1.59    oops
    1.60  
    1.61  lemma inf_bot_right [simp]:
    1.62    "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
    1.63 -  quickcheck
    1.64 +  quickcheck[expect = no_counterexample]
    1.65    by (rule inf_absorb2) simp
    1.66  
    1.67  lemma inf_bot_right_1:
    1.68    "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
    1.69 -  quickcheck
    1.70 +  quickcheck[expect = counterexample]
    1.71    oops
    1.72  
    1.73  lemma inf_bot_right_2:
    1.74    "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
    1.75 -  quickcheck
    1.76 +  quickcheck[expect = counterexample]
    1.77    oops
    1.78  
    1.79  lemma inf_bot_right [simp]:
    1.80    "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
    1.81 -  quickcheck
    1.82 +  quickcheck[expect = counterexample]
    1.83    oops
    1.84  
    1.85  lemma sup_bot_left [simp]:
    1.86    "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
    1.87 -  quickcheck
    1.88 +  quickcheck[expect = no_counterexample]
    1.89    by (rule sup_absorb2) simp
    1.90  
    1.91  lemma sup_bot_right [simp]:
    1.92    "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
    1.93 -  quickcheck
    1.94 +  quickcheck[expect = no_counterexample]
    1.95    by (rule sup_absorb1) simp
    1.96  
    1.97  lemma sup_eq_bot_iff [simp]:
    1.98    "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    1.99 -  quickcheck
   1.100 +  quickcheck[expect = no_counterexample]
   1.101    by (simp add: eq_iff)
   1.102  
   1.103  lemma sup_top_left [simp]:
   1.104    "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
   1.105 -  quickcheck
   1.106 +  quickcheck[expect = no_counterexample]
   1.107    by (rule sup_absorb1) simp
   1.108  
   1.109  lemma sup_top_right [simp]:
   1.110    "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
   1.111 -  quickcheck
   1.112 +  quickcheck[expect = no_counterexample]
   1.113    by (rule sup_absorb2) simp
   1.114  
   1.115  lemma inf_top_left [simp]:
   1.116    "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
   1.117 -  quickcheck
   1.118 +  quickcheck[expect = no_counterexample]
   1.119    by (rule inf_absorb2) simp
   1.120  
   1.121  lemma inf_top_right [simp]:
   1.122    "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
   1.123 -  quickcheck
   1.124 +  quickcheck[expect = no_counterexample]
   1.125    by (rule inf_absorb1) simp
   1.126  
   1.127  lemma inf_eq_top_iff [simp]:
   1.128    "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   1.129 -  quickcheck
   1.130 +  quickcheck[expect = no_counterexample]
   1.131    by (simp add: eq_iff)
   1.132  
   1.133