--- 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)
--------------------------------
--- 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)
--- 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
--- 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