# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1589292680 -3600
# Node ID ff6f3b09b8b4994e02e6f8d2b1c485433cd3ae34
# Parent  7a997ead54b000a07d6b71012fe19cc7b187ae25
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)

diff -r 7a997ead54b0 -r ff6f3b09b8b4 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 10:59:59 2020 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 15:11:20 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"
diff -r 7a997ead54b0 -r ff6f3b09b8b4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 12 10:59:59 2020 +0200
+++ b/src/HOL/HOL.thy	Tue May 12 15:11:20 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>