src/HOL/Lattices.thy
changeset 50615 965d4c108584
parent 49769 c7c2152322f2
child 51387 dbc4a77488b2
--- a/src/HOL/Lattices.thy	Fri Dec 21 23:52:10 2012 +0100
+++ b/src/HOL/Lattices.thy	Sat Dec 22 00:04:50 2012 +0100
@@ -20,9 +20,11 @@
   assumes idem [simp]: "f a a = a"
 begin
 
-lemma left_idem [simp]:
-  "f a (f a b) = f a b"
-  by (simp add: assoc [symmetric])
+lemma left_idem [simp]: "f a (f a b) = f a b"
+by (simp add: assoc [symmetric])
+
+lemma right_idem [simp]: "f (f a b) b = f a b"
+by (simp add: assoc)
 
 end
 
@@ -184,8 +186,11 @@
 lemma inf_idem: "x \<sqinter> x = x"
   by (fact inf.idem) (* already simp *)
 
-lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-  by (fact inf.left_idem)
+lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+  by (fact inf.left_idem) (* already simp *)
+
+lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
+  by (fact inf.right_idem) (* already simp *)
 
 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto