src/HOL/ex/Quickcheck_Lattice_Examples.thy
changeset 37916 cb55fd65faa6
child 37929 22e0797857e6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Jul 21 18:11:51 2010 +0200
     1.3 @@ -0,0 +1,139 @@
     1.4 +(*  Title:      HOL/ex/Quickcheck_Lattice_Examples.thy
     1.5 +    Author:     Lukas Bulwahn
     1.6 +    Copyright   2010 TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +theory Quickcheck_Lattice_Examples
    1.10 +imports Quickcheck_Types
    1.11 +begin
    1.12 +
    1.13 +text {* We show how other default types help to find counterexamples to propositions if
    1.14 +  the standard default type @{typ int} is insufficient. *}
    1.15 +
    1.16 +notation
    1.17 +  less_eq  (infix "\<sqsubseteq>" 50) and
    1.18 +  less  (infix "\<sqsubset>" 50) and
    1.19 +  top ("\<top>") and
    1.20 +  bot ("\<bottom>") and
    1.21 +  inf (infixl "\<sqinter>" 70) and
    1.22 +  sup (infixl "\<squnion>" 65)
    1.23 +
    1.24 +subsection {* Distributive lattices *}
    1.25 +
    1.26 +lemma sup_inf_distrib2:
    1.27 + "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    1.28 +  quickcheck
    1.29 +by(simp add: inf_sup_aci sup_inf_distrib1)
    1.30 +
    1.31 +lemma sup_inf_distrib2_1:
    1.32 + "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    1.33 +  quickcheck
    1.34 +  oops
    1.35 +
    1.36 +lemma sup_inf_distrib2_2:
    1.37 + "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    1.38 +  quickcheck
    1.39 +  oops
    1.40 +
    1.41 +lemma inf_sup_distrib1_1:
    1.42 + "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
    1.43 +  quickcheck
    1.44 +  oops
    1.45 +
    1.46 +lemma inf_sup_distrib2_1:
    1.47 + "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
    1.48 +  quickcheck
    1.49 +  oops
    1.50 +
    1.51 +subsection {* Bounded lattices *}
    1.52 +
    1.53 +lemma inf_bot_left [simp]:
    1.54 +  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    1.55 +  quickcheck
    1.56 +  by (rule inf_absorb1) simp
    1.57 +
    1.58 +lemma inf_bot_left_1:
    1.59 +  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
    1.60 +  quickcheck
    1.61 +  oops
    1.62 +
    1.63 +lemma inf_bot_left_2:
    1.64 +  "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    1.65 +  quickcheck
    1.66 +  oops
    1.67 +
    1.68 +lemma inf_bot_left_3:
    1.69 +  "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
    1.70 +  quickcheck
    1.71 +  oops
    1.72 +
    1.73 +lemma inf_bot_right [simp]:
    1.74 +  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
    1.75 +  quickcheck
    1.76 +  by (rule inf_absorb2) simp
    1.77 +
    1.78 +lemma inf_bot_right_1:
    1.79 +  "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
    1.80 +  quickcheck
    1.81 +  oops
    1.82 +
    1.83 +lemma inf_bot_right_2:
    1.84 +  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
    1.85 +  quickcheck
    1.86 +  oops
    1.87 +
    1.88 +lemma inf_bot_right [simp]:
    1.89 +  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
    1.90 +  quickcheck
    1.91 +  oops
    1.92 +
    1.93 +lemma sup_bot_left [simp]:
    1.94 +  "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
    1.95 +  quickcheck
    1.96 +  by (rule sup_absorb2) simp
    1.97 +
    1.98 +lemma sup_bot_right [simp]:
    1.99 +  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
   1.100 +  quickcheck
   1.101 +  by (rule sup_absorb1) simp
   1.102 +
   1.103 +lemma sup_eq_bot_iff [simp]:
   1.104 +  "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.105 +  quickcheck
   1.106 +  by (simp add: eq_iff)
   1.107 +
   1.108 +lemma sup_top_left [simp]:
   1.109 +  "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
   1.110 +  quickcheck
   1.111 +  by (rule sup_absorb1) simp
   1.112 +
   1.113 +lemma sup_top_right [simp]:
   1.114 +  "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
   1.115 +  quickcheck
   1.116 +  by (rule sup_absorb2) simp
   1.117 +
   1.118 +lemma inf_top_left [simp]:
   1.119 +  "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
   1.120 +  quickcheck
   1.121 +  by (rule inf_absorb2) simp
   1.122 +
   1.123 +lemma inf_top_right [simp]:
   1.124 +  "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
   1.125 +  quickcheck
   1.126 +  by (rule inf_absorb1) simp
   1.127 +
   1.128 +lemma inf_eq_top_iff [simp]:
   1.129 +  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   1.130 +  quickcheck
   1.131 +  by (simp add: eq_iff)
   1.132 +
   1.133 +
   1.134 +no_notation
   1.135 +  less_eq  (infix "\<sqsubseteq>" 50) and
   1.136 +  less (infix "\<sqsubset>" 50) and
   1.137 +  inf  (infixl "\<sqinter>" 70) and
   1.138 +  sup  (infixl "\<squnion>" 65) and
   1.139 +  top ("\<top>") and
   1.140 +  bot ("\<bottom>")
   1.141 +
   1.142 +end