src/HOL/Lattices.thy

--- a/src/HOL/Lattices.thy	Mon Aug 08 22:11:00 2011 +0200
+++ b/src/HOL/Lattices.thy	Mon Aug 08 22:33:36 2011 +0200
@@ -177,10 +177,10 @@
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   by (fact inf.left_commute)
 
-lemma inf_idem: "x \<sqinter> x = x"
+lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
   by (fact inf.idem)
 
-lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (fact inf.left_idem)
 
 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
@@ -216,10 +216,10 @@
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   by (fact sup.left_commute)
 
-lemma sup_idem: "x \<squnion> x = x"
+lemma sup_idem (*[simp]*): "x \<squnion> x = x"
   by (fact sup.idem)
 
-lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (fact sup.left_idem)
 
 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
@@ -240,10 +240,10 @@
   by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
-lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
+lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
 
-lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
+lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
   by (blast intro: antisym sup_ge1 sup_least inf_le1)
 
 lemmas inf_sup_aci = inf_aci sup_aci
@@ -436,11 +436,11 @@
   by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
-lemma compl_inf_bot:
+lemma compl_inf_bot (*[simp]*):
   "- x \<sqinter> x = \<bottom>"
   by (simp add: inf_commute inf_compl_bot)
 
-lemma compl_sup_top:
+lemma compl_sup_top (*[simp]*):
   "- x \<squnion> x = \<top>"
   by (simp add: sup_commute sup_compl_top)
 
@@ -522,7 +522,7 @@
   then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
 qed
 
-lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
+lemma compl_le_compl_iff (*[simp]*):
   "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   by (auto dest: compl_mono)