# HG changeset patch
# User haftmann
# Date 1387880656 -3600
# Node ID 5c05f7c5f8aebd3ea38aa1fdefb0849dca529ad0
# Parent  356b4c0a2061de1f4fba51679dea15a036714575
tuning and augmentation of min/max lemmas;
more lemmas and simp rules for abstract lattices with order;
tuned proofs

diff -r 356b4c0a2061 -r 5c05f7c5f8ae src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Dec 24 11:24:14 2013 +0100
+++ b/src/HOL/Lattices.thy	Tue Dec 24 11:24:16 2013 +0100
@@ -190,7 +190,7 @@
   by (rule order_trans) auto
 
 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-  by (rule inf_greatest) (* FIXME: duplicate lemma *)
+  by (fact inf_greatest) (* FIXME: duplicate lemma *)
 
 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans inf_le1 inf_le2)
@@ -226,7 +226,7 @@
 
 lemma le_supI:
   "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
-  by (rule sup_least) (* FIXME: duplicate lemma *)
+  by (fact sup_least) (* FIXME: duplicate lemma *)
 
 lemma le_supE:
   "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
@@ -856,16 +856,16 @@
   by (simp add: inf_fun_def)
 
 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
-  by (simp add: inf_fun_def)
+  by (rule inf1E)
 
 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
-  by (simp add: inf_fun_def)
+  by (rule inf2E)
 
 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
-  by (simp add: inf_fun_def)
+  by (rule inf1E)
 
 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
-  by (simp add: inf_fun_def)
+  by (rule inf2E)
 
 lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
diff -r 356b4c0a2061 -r 5c05f7c5f8ae src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Tue Dec 24 11:24:14 2013 +0100
+++ b/src/HOL/Lattices_Big.thy	Tue Dec 24 11:24:16 2013 +0100
@@ -373,12 +373,8 @@
 
 lemmas le_maxI1 = min_max.sup_ge1
 lemmas le_maxI2 = min_max.sup_ge2
- 
-lemmas min_ac = min_max.inf_assoc min_max.inf_commute
-  min.left_commute
-
-lemmas max_ac = min_max.sup_assoc min_max.sup_commute
-  max.left_commute
+lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
+lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
 
 end
 
diff -r 356b4c0a2061 -r 5c05f7c5f8ae src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Dec 24 11:24:14 2013 +0100
+++ b/src/HOL/Orderings.thy	Tue Dec 24 11:24:16 2013 +0100
@@ -1155,7 +1155,7 @@
 lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"
 by (simp add: min_def)
 
-lemma max_absorb2: "x \<le> y ==> max x y = y"
+lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
 by (simp add: max_def)
 
 lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"