# HG changeset patch
# User nipkow
# Date 1356131090 -3600
# Node ID 965d4c108584ee55cf2dfea43f449ab5e80c8a84
# Parent  eefab127e9f16db3c4327f4af5a577694f726a81
added simp rule

diff -r eefab127e9f1 -r 965d4c108584 src/HOL/Lattices.thy
--- 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