src/HOL/Lattices.thy
changeset 34973 ae634fad947e
parent 34209 c7f621786035
child 35028 108662d50512
     1.1 --- a/src/HOL/Lattices.thy	Wed Jan 27 14:03:08 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Thu Jan 28 11:48:43 2010 +0100
     1.3 @@ -112,48 +112,73 @@
     1.4  
     1.5  subsubsection {* Equational laws *}
     1.6  
     1.7 +sublocale lower_semilattice < inf!: semilattice inf
     1.8 +proof
     1.9 +  fix a b c
    1.10 +  show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
    1.11 +    by (rule antisym) (auto intro: le_infI1 le_infI2)
    1.12 +  show "a \<sqinter> b = b \<sqinter> a"
    1.13 +    by (rule antisym) auto
    1.14 +  show "a \<sqinter> a = a"
    1.15 +    by (rule antisym) auto
    1.16 +qed
    1.17 +
    1.18  context lower_semilattice
    1.19  begin
    1.20  
    1.21 -lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    1.22 -  by (rule antisym) auto
    1.23 +lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    1.24 +  by (fact inf.assoc)
    1.25  
    1.26 -lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    1.27 -  by (rule antisym) (auto intro: le_infI1 le_infI2)
    1.28 +lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    1.29 +  by (fact inf.commute)
    1.30  
    1.31 -lemma inf_idem[simp]: "x \<sqinter> x = x"
    1.32 -  by (rule antisym) auto
    1.33 +lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    1.34 +  by (fact inf.left_commute)
    1.35  
    1.36 -lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    1.37 -  by (rule antisym) (auto intro: le_infI2)
    1.38 +lemma inf_idem: "x \<sqinter> x = x"
    1.39 +  by (fact inf.idem)
    1.40 +
    1.41 +lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    1.42 +  by (fact inf.left_idem)
    1.43  
    1.44  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    1.45    by (rule antisym) auto
    1.46  
    1.47  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    1.48    by (rule antisym) auto
    1.49 -
    1.50 -lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    1.51 -  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
    1.52 -  
    1.53 + 
    1.54  lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
    1.55  
    1.56  end
    1.57  
    1.58 +sublocale upper_semilattice < sup!: semilattice sup
    1.59 +proof
    1.60 +  fix a b c
    1.61 +  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
    1.62 +    by (rule antisym) (auto intro: le_supI1 le_supI2)
    1.63 +  show "a \<squnion> b = b \<squnion> a"
    1.64 +    by (rule antisym) auto
    1.65 +  show "a \<squnion> a = a"
    1.66 +    by (rule antisym) auto
    1.67 +qed
    1.68 +
    1.69  context upper_semilattice
    1.70  begin
    1.71  
    1.72 -lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    1.73 -  by (rule antisym) auto
    1.74 +lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    1.75 +  by (fact sup.assoc)
    1.76  
    1.77 -lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    1.78 -  by (rule antisym) (auto intro: le_supI1 le_supI2)
    1.79 +lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    1.80 +  by (fact sup.commute)
    1.81  
    1.82 -lemma sup_idem[simp]: "x \<squnion> x = x"
    1.83 -  by (rule antisym) auto
    1.84 +lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    1.85 +  by (fact sup.left_commute)
    1.86  
    1.87 -lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    1.88 -  by (rule antisym) (auto intro: le_supI2)
    1.89 +lemma sup_idem: "x \<squnion> x = x"
    1.90 +  by (fact sup.idem)
    1.91 +
    1.92 +lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    1.93 +  by (fact sup.left_idem)
    1.94  
    1.95  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    1.96    by (rule antisym) auto
    1.97 @@ -161,9 +186,6 @@
    1.98  lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    1.99    by (rule antisym) auto
   1.100  
   1.101 -lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   1.102 -  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
   1.103 -
   1.104  lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   1.105  
   1.106  end
   1.107 @@ -514,11 +536,12 @@
   1.108  lemmas le_maxI1 = min_max.sup_ge1
   1.109  lemmas le_maxI2 = min_max.sup_ge2
   1.110   
   1.111 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.112 -  mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
   1.113 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.114 +  min_max.inf.left_commute
   1.115  
   1.116 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.117 -  mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   1.118 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.119 +  min_max.sup.left_commute
   1.120 +
   1.121  
   1.122  
   1.123  subsection {* Bool as lattice *}