# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1589298782 -3600
# Node ID 919a55257e62f99badf8eef836ef6e569fe7953a
# Parent  ff6f3b09b8b4994e02e6f8d2b1c485433cd3ae34
Fixes for Sup{} = (0::nat)

diff -r ff6f3b09b8b4 -r 919a55257e62 NEWS
--- a/NEWS	Tue May 12 15:11:20 2020 +0100
+++ b/NEWS	Tue May 12 16:53:02 2020 +0100
@@ -33,6 +33,11 @@
 * Definitions in locales produce rule which can be added as congruence
 rule to protect foundational terms during simplification.
 
+*** HOL ***
+
+* Added the "at most 1" quantifier, Uniq.
+
+* For the natural numbers, Sup{} = 0.
 
 New in Isabelle2020 (April 2020)
 --------------------------------
diff -r ff6f3b09b8b4 -r 919a55257e62 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Tue May 12 15:11:20 2020 +0100
+++ b/src/HOL/Analysis/Measurable.thy	Tue May 12 16:53:02 2020 +0100
@@ -590,11 +590,11 @@
   fix a
   have F_empty_iff: "F x = {} \<longleftrightarrow> (\<forall>i. i \<notin> F x)" for x
     by auto
-  have "Measurable.pred M (\<lambda>x. if finite (F x) then if F x = {} then a = Max {}
+  have "Measurable.pred M (\<lambda>x. if finite (F x) then if F x = {} then a = 0
     else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None)"
     unfolding finite_nat_set_iff_bounded Ball_def F_empty_iff by measurable
   moreover have "(\<lambda>x. Sup (F x)) -` {a} \<inter> space M =
-    {x\<in>space M. if finite (F x) then if F x = {} then a = Max {}
+    {x\<in>space M. if finite (F x) then if F x = {} then a = 0
       else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None}"
     by (intro set_eqI)
        (auto simp: Sup_nat_def Max.infinite intro!: Max_in Max_eqI)
diff -r ff6f3b09b8b4 -r 919a55257e62 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 15:11:20 2020 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 16:53:02 2020 +0100
@@ -563,6 +563,10 @@
   shows "Inf K \<in> K"
 by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
 
+lemma Sup_nat_empty [simp]: "Sup {} = (0::nat)"
+  by (auto simp add: Sup_nat_def) 
+
+
 
 instantiation int :: conditionally_complete_linorder
 begin
diff -r ff6f3b09b8b4 -r 919a55257e62 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 12 15:11:20 2020 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 12 16:53:02 2020 +0100
@@ -160,7 +160,7 @@
   show "(SUP a\<in>A. of_nat a::real) \<le> of_nat (Sup A)"
     using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
   have "Sup A \<in> A"
-    unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
+    using assms by (auto simp: Sup_nat_def bdd_above_nat)
   then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::real)"
     by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
 qed
@@ -1476,7 +1476,7 @@
   show "(SUP a\<in>A. of_nat a::ennreal) \<le> of_nat (Sup A)"
     by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
   have "Sup A \<in> A"
-    unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
+    using assms by (auto simp: Sup_nat_def bdd_above_nat)
   then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::ennreal)"
     by (intro SUP_upper)
 qed