--- a/NEWS Tue May 12 16:29:26 2020 +0200
+++ b/NEWS Tue May 12 16:53:13 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 16:29:26 2020 +0200
+++ b/src/HOL/Analysis/Measurable.thy Tue May 12 16:53:13 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 16:29:26 2020 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue May 12 16:53:13 2020 +0100
@@ -524,7 +524,7 @@
instantiation nat :: conditionally_complete_linorder
begin
-definition "Sup (X::nat set) = Max X"
+definition "Sup (X::nat set) = (if X={} then 0 else Max X)"
definition "Inf (X::nat set) = (LEAST n. n \<in> X)"
lemma bdd_above_nat: "bdd_above X \<longleftrightarrow> finite (X::nat set)"
@@ -545,7 +545,7 @@
show "x \<le> Inf X" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y"
using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex)
show "x \<le> Sup X" if "x \<in> X" "bdd_above X"
- using that by (simp add: Sup_nat_def bdd_above_nat)
+ using that by (auto simp add: Sup_nat_def bdd_above_nat)
show "Sup X \<le> x" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
proof -
from that have "bdd_above X"
@@ -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/HOL.thy Tue May 12 16:29:26 2020 +0200
+++ b/src/HOL/HOL.thy Tue May 12 16:53:13 2020 +0100
@@ -10,6 +10,7 @@
"try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
"print_induct_rules" :: diag and
"quickcheck_params" :: thy_decl
+abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
begin
ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 12 16:29:26 2020 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 12 16:53:13 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