merged
authorpaulson
Tue, 12 May 2020 16:53:13 +0100
changeset 72058 455b010d8436
parent 72057 f61b19358a8f (current diff)
parent 72055 919a55257e62 (diff)
child 72059 c095d3143047
merged
--- 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