# HG changeset patch
# User nipkow
# Date 1516188426 -3600
# Node ID aab817885622fe31ae45bac0a18aba82823705a7
# Parent  12bcfbac45a1555f4e7a05f53d40cdcbc82f72d7
more lemmas by Gouezele

diff -r 12bcfbac45a1 -r aab817885622 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 17 09:55:03 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 17 12:27:06 2018 +0100
@@ -659,9 +659,6 @@
   subgoal for a b c
     apply (cases a b c rule: ereal3_cases)
     apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
-    apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
-                simp del: sup_ereal_def)
-    apply (auto simp add: top_ereal_def)
     done
   done
 
diff -r 12bcfbac45a1 -r aab817885622 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Jan 17 09:55:03 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jan 17 12:27:06 2018 +0100
@@ -1776,6 +1776,31 @@
     using zero_neq_one by blast
 qed
 
+lemma min_PInf [simp]: "min (\<infinity>::ereal) x = x"
+by (metis min_top top_ereal_def)
+
+lemma min_PInf2 [simp]: "min x (\<infinity>::ereal) = x"
+by (metis min_top2 top_ereal_def)
+
+lemma max_PInf [simp]: "max (\<infinity>::ereal) x = \<infinity>"
+by (metis max_top top_ereal_def)
+
+lemma max_PInf2 [simp]: "max x (\<infinity>::ereal) = \<infinity>"
+by (metis max_top2 top_ereal_def)
+
+lemma min_MInf [simp]: "min (-\<infinity>::ereal) x = -\<infinity>"
+by (metis min_bot bot_ereal_def)
+
+lemma min_MInf2 [simp]: "min x (-\<infinity>::ereal) = -\<infinity>"
+by (metis min_bot2 bot_ereal_def)
+
+lemma max_MInf [simp]: "max (-\<infinity>::ereal) x = x"
+by (metis max_bot bot_ereal_def)
+
+lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
+by (metis max_bot2 bot_ereal_def)
+
+
 subsubsection "Topological space"
 
 instantiation ereal :: linear_continuum_topology
diff -r 12bcfbac45a1 -r aab817885622 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jan 17 09:55:03 2018 +0100
+++ b/src/HOL/Orderings.thy	Wed Jan 17 12:27:06 2018 +0100
@@ -1287,6 +1287,18 @@
   "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
   by (fact bot.not_eq_extremum)
 
+lemma max_bot[simp]: "max bot x = x"
+by(simp add: max_def bot_unique)
+
+lemma max_bot2[simp]: "max x bot = x"
+by(simp add: max_def bot_unique)
+
+lemma min_bot[simp]: "min bot x = bot"
+by(simp add: min_def bot_unique)
+
+lemma min_bot2[simp]: "min x bot = bot"
+by(simp add: min_def bot_unique)
+
 end
 
 class top =
@@ -1315,6 +1327,18 @@
   "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
   by (fact top.not_eq_extremum)
 
+lemma max_top[simp]: "max top x = top"
+by(simp add: max_def top_unique)
+
+lemma max_top2[simp]: "max x top = top"
+by(simp add: max_def top_unique)
+
+lemma min_top[simp]: "min top x = x"
+by(simp add: min_def top_unique)
+
+lemma min_top2[simp]: "min x top = x"
+by(simp add: min_def top_unique)
+
 end