src/HOL/Lattices.thy
changeset 32436 10cd49e0c067
parent 32204 b330aa4d59cb
child 32512 d14762642cdd
     1.1 --- a/src/HOL/Lattices.thy	Fri Aug 28 18:11:42 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Fri Aug 28 18:52:41 2009 +0200
     1.3 @@ -125,10 +125,10 @@
     1.4  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
     1.5    by (rule antisym) (auto intro: le_infI2)
     1.6  
     1.7 -lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     1.8 +lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     1.9    by (rule antisym) auto
    1.10  
    1.11 -lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    1.12 +lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    1.13    by (rule antisym) auto
    1.14  
    1.15  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    1.16 @@ -153,10 +153,10 @@
    1.17  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    1.18    by (rule antisym) (auto intro: le_supI2)
    1.19  
    1.20 -lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    1.21 +lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    1.22    by (rule antisym) auto
    1.23  
    1.24 -lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    1.25 +lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    1.26    by (rule antisym) auto
    1.27  
    1.28  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    1.29 @@ -199,7 +199,7 @@
    1.30  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.31  proof-
    1.32    have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    1.33 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    1.34 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
    1.35    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    1.36      by(simp add:inf_sup_absorb inf_commute)
    1.37    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    1.38 @@ -211,7 +211,7 @@
    1.39  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.40  proof-
    1.41    have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    1.42 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
    1.43 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
    1.44    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    1.45      by(simp add:sup_inf_absorb sup_commute)
    1.46    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)