# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1589192141 -3600
# Node ID 5e315defb0383d2c0654c02606d27b008005cd35
# Parent  f424e164d75217584b0af76cb5a349cc0b04798f
the Uniq quantifier

diff -r f424e164d752 -r 5e315defb038 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Analysis/Infinite_Products.thy	Mon May 11 11:15:41 2020 +0100
@@ -1185,7 +1185,7 @@
 lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
 proof -
   have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
-    by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)
+    by (subst filterlim_sequentially_Suc) (simp add: raw_has_prod_def)
   also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
     by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod.atLeast1_atMost_eq lessThan_Suc_atMost
                   del: prod.cl_ivl_Suc)
@@ -1238,7 +1238,7 @@
   proof -
     have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"
       using M_L 
-      apply (subst (asm) LIMSEQ_Suc_iff[symmetric]) 
+      apply (subst (asm) filterlim_sequentially_Suc[symmetric]) 
       using atLeast0AtMost by auto
     then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"
       apply (subst (asm) prod.atLeast0_atMost_Suc_shift)
diff -r f424e164d752 -r 5e315defb038 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Analysis/Interval_Integral.thy	Mon May 11 11:15:41 2020 +0100
@@ -47,9 +47,9 @@
   with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
     by (cases a) auto
   moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
-    by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
+    by (simp add: Lim_PInfty filterlim_sequentially_Suc) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
   moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>"
-    by (simp add: LIMSEQ_Suc_iff Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
+    by (simp add: filterlim_sequentially_Suc Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
   ultimately show thesis
     by (intro that[of "\<lambda>i. real_of_ereal a + Suc i"])
        (auto simp: incseq_def PInf)
diff -r f424e164d752 -r 5e315defb038 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Deriv.thy	Mon May 11 11:15:41 2020 +0100
@@ -572,6 +572,7 @@
     bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
   using has_derivative_within [of f f' x UNIV]
   by simp
+
 lemma has_derivative_zero_unique:
   assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   shows "F = (\<lambda>h. 0)"
@@ -618,6 +619,9 @@
     unfolding fun_eq_iff right_minus_eq .
 qed
 
+lemma has_derivative_Uniq: "\<exists>\<^sub>\<le>\<^sub>1F. (f has_derivative F) (at x)"
+  by (simp add: Uniq_def has_derivative_unique)
+
 
 subsection \<open>Differentiability predicate\<close>
 
@@ -970,6 +974,9 @@
 lemma DERIV_unique: "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
   unfolding DERIV_def by (rule LIM_unique)
 
+lemma DERIV_Uniq: "\<exists>\<^sub>\<le>\<^sub>1D. DERIV f x :> D"
+  by (simp add: DERIV_unique Uniq_def)
+
 lemma DERIV_sum[derivative_intros]:
   "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow>
     ((\<lambda>x. sum (f x) S) has_field_derivative sum (f' x) S) F"
diff -r f424e164d752 -r 5e315defb038 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Fun.thy	Mon May 11 11:15:41 2020 +0100
@@ -190,6 +190,9 @@
 lemma inj_eq: "inj f \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
   by (simp add: inj_on_eq_iff)
 
+lemma inj_on_iff_Uniq: "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<exists>\<^sub>\<le>\<^sub>1y. y\<in>A \<and> f x = f y)"
+  by (auto simp: Uniq_def inj_on_def)
+
 lemma inj_on_id[simp]: "inj_on id A"
   by (simp add: inj_on_def)
 
diff -r f424e164d752 -r 5e315defb038 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/HOL.thy	Mon May 11 11:15:41 2020 +0100
@@ -117,12 +117,24 @@
 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
 
+definition Uniq :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "Uniq P \<equiv> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> y = x)"
+
 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
+syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(4?< _./ _)" [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
+
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
+
 syntax (ASCII)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
 syntax (input)
@@ -539,6 +551,14 @@
 
 subsubsection \<open>Unique existence\<close>
 
+lemma Uniq_I [intro?]:
+  assumes "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> y = x"
+  shows "Uniq P"
+  unfolding Uniq_def by (iprover intro: assms allI impI)
+
+lemma Uniq_D [dest?]: "\<lbrakk>Uniq P; P a; P b\<rbrakk> \<Longrightarrow> a=b"
+  unfolding Uniq_def by (iprover dest: spec mp)
+
 lemma ex1I:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   shows "\<exists>!x. P x"
@@ -562,7 +582,6 @@
 lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
   by (iprover intro: exI elim: ex1E)
 
-
 subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
 
 lemma disjCI:
@@ -854,6 +873,15 @@
     using \<open>P x\<close> \<section> \<section> by fast
 qed assumption
 
+text \<open>And again using Uniq\<close>
+lemma alt_ex1E':
+  assumes  "\<exists>!x. P x" "\<And>x. \<lbrakk>P x; \<exists>\<^sub>\<le>\<^sub>1x. P x\<rbrakk> \<Longrightarrow> R"
+  shows R
+  using assms unfolding Uniq_def by fast
+
+lemma ex1_iff_ex_Uniq: "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x) \<and> (\<exists>\<^sub>\<le>\<^sub>1x. P x)"
+  unfolding Uniq_def by fast
+
 
 ML \<open>
   structure Blast = Blast
@@ -901,6 +929,9 @@
 lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   by blast
 
+lemma the1_equality': "\<lbrakk>\<exists>\<^sub>\<le>\<^sub>1x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
+  unfolding Uniq_def by blast
+
 lemma the_sym_eq_trivial: "(THE y. x = y) = x"
   by blast
 
diff -r f424e164d752 -r 5e315defb038 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Mon May 11 11:15:41 2020 +0100
@@ -223,6 +223,9 @@
 lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B"
   by (blast intro: inj_onI dest: inv_into_injective injD)
 
+lemma inj_imp_bij_betw_inv: "inj f \<Longrightarrow> bij_betw (inv f) (f ` M) M"
+  by (simp add: bij_betw_def image_subsetI inj_on_inv_into)
+
 lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A"
   by (auto simp add: bij_betw_def inj_on_inv_into)
 
@@ -373,6 +376,17 @@
   qed
 qed
 
+lemma strict_mono_inv_on_range:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+  assumes "strict_mono f"
+  shows "strict_mono_on (inv f) (range f)"
+proof (clarsimp simp: strict_mono_on_def)
+  fix x y
+  assume "f x < f y"
+  then show "inv f (f x) < inv f (f y)"
+    using assms strict_mono_imp_inj_on strict_mono_less by fastforce
+qed
+
 lemma mono_bij_Inf:
   fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
   assumes "mono f" "bij f"
diff -r f424e164d752 -r 5e315defb038 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon May 11 11:15:41 2020 +0100
@@ -399,4 +399,189 @@
   qed
 qed
 
+subsection \<open>Properties of @{term enumerate} on finite sets\<close>
+
+lemma finite_enumerate_in_set: "\<lbrakk>finite S; n < card S\<rbrakk> \<Longrightarrow> enumerate S n \<in> S"
+proof (induction n arbitrary: S)
+  case 0
+  then show ?case
+    by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+next
+  case (Suc n)
+  show ?case
+    using Suc.prems Suc.IH [of "S - {LEAST n. n \<in> S}"]
+    apply (simp add: enumerate.simps)
+    by (metis Diff_empty Diff_insert0 Suc_lessD card.remove less_Suc_eq)
+qed
+
+lemma finite_enumerate_step: "\<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
+proof (induction n arbitrary: S)
+  case 0
+  then have "enumerate S 0 \<le> enumerate S (Suc 0)"
+    by (simp add: Least_le enumerate.simps(1) finite_enumerate_in_set)
+  moreover have "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}"
+    by (metis 0 Suc_lessD Suc_less_eq card_Suc_Diff1 enumerate_in_set finite_enumerate_in_set)
+  then have "enumerate S 0 \<noteq> enumerate (S - {enumerate S 0}) 0"
+    by auto
+  ultimately show ?case
+    by (simp add: enumerate_Suc')
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: enumerate_Suc' finite_enumerate_in_set)
+qed
+
+lemma finite_enumerate_mono: "\<lbrakk>m < n; finite S; n < card S\<rbrakk> \<Longrightarrow> enumerate S m < enumerate S n"
+  by (induct m n rule: less_Suc_induct) (auto intro: finite_enumerate_step)
+
+
+lemma finite_le_enumerate:
+  assumes "finite S" "n < card S"
+  shows "n \<le> enumerate S n"
+  using assms
+proof (induction n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  then have "n \<le> enumerate S n" by simp
+  also note finite_enumerate_mono[of n "Suc n", OF _ \<open>finite S\<close>]
+  finally show ?case
+    using Suc.prems(2) Suc_leI by blast
+qed
+
+lemma finite_enumerate:
+  assumes fS: "finite S"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on r {..<card S} \<and> (\<forall>n<card S. r n \<in> S)"
+  unfolding strict_mono_def
+  using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
+  by (metis lessThan_iff strict_mono_on_def)
+
+lemma finite_enumerate_Suc'':
+  fixes S :: "'a::wellorder set"
+  assumes "finite S" "Suc n < card S"
+  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+  using assms
+proof (induction n arbitrary: S)
+  case 0
+  then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
+    by (auto simp: enumerate.simps intro: Least_le)
+  then show ?case
+    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
+    by (metis Diff_iff dual_order.strict_iff_order singletonD singletonI)
+next
+  case (Suc n S)
+  then have "Suc n < card (S - {enumerate S 0})"
+    using Suc.prems(2) finite_enumerate_in_set by force
+  then show ?case
+    apply (subst (1 2) enumerate_Suc')
+    apply (simp add: Suc)
+    apply (intro arg_cong[where f = Least] HOL.ext)
+    using finite_enumerate_mono[OF zero_less_Suc \<open>finite S\<close>, of n] Suc.prems
+    by (auto simp flip: enumerate_Suc')
+qed
+
+lemma finite_enumerate_initial_segment:
+  fixes S :: "'a::wellorder set"
+  assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})"
+  shows "enumerate (S \<inter> {..<s}) n = enumerate S n"
+  using n
+proof (induction n)
+  case 0
+  have "(LEAST n. n \<in> S \<and> n < s) = (LEAST n. n \<in> S)"
+  proof (rule Least_equality)
+    have "\<exists>t. t \<in> S \<and> t < s"
+      by (metis "0" card_gt_0_iff disjoint_iff_not_equal lessThan_iff)
+    then show "(LEAST n. n \<in> S) \<in> S \<and> (LEAST n. n \<in> S) < s"
+      by (meson LeastI Least_le le_less_trans)
+  qed (simp add: Least_le)
+  then show ?case
+    by (auto simp: enumerate_0)
+next
+  case (Suc n)
+  then have less_card: "Suc n < card S"
+    by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
+  obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}"
+    by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
+  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+       (is "_ = ?r")
+  proof (intro Least_equality conjI)
+    show "?r \<in> S"
+      by (metis (mono_tags, lifting) LeastI mem_Collect_eq t)
+    show "?r < s"
+      using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms 
+      by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases)
+    show "enumerate S n < ?r"
+      by (metis (no_types, lifting) LeastI mem_Collect_eq t)
+  qed (auto simp: Least_le)
+  then show ?case
+    using Suc assms by (simp add: finite_enumerate_Suc'' less_card)
+qed
+
+lemma finite_enumerate_Ex:
+  fixes S :: "'a::wellorder set"
+  assumes S: "finite S"
+    and s: "s \<in> S"
+  shows "\<exists>n<card S. enumerate S n = s"
+  using s S
+proof (induction s arbitrary: S rule: less_induct)
+  case (less s)
+  show ?case
+  proof (cases "\<exists>y\<in>S. y < s")
+    case True
+    let ?T = "S \<inter> {..<s}"
+    have "finite ?T"
+      using less.prems(2) by blast
+    have TS: "card ?T < card S"
+      using less.prems by (blast intro: psubset_card_mono [OF \<open>finite S\<close>])
+    from True have y: "\<And>x. Max ?T < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
+      by (subst Max_less_iff) (auto simp: \<open>finite ?T\<close>)
+    then have y_in: "Max ?T \<in> {s'\<in>S. s' < s}"
+      using Max_in \<open>finite ?T\<close> by fastforce
+    with less.IH[of "Max ?T" ?T] obtain n where n: "enumerate ?T n = Max ?T" "n < card ?T"
+      using \<open>finite ?T\<close> by blast
+    then have "Suc n < card S"
+      using TS less_trans_Suc by blast
+    with S n have "enumerate S (Suc n) = s"
+      by (subst finite_enumerate_Suc'') (auto simp: y finite_enumerate_initial_segment less finite_enumerate_Suc'' intro!: Least_equality)
+    then show ?thesis
+      using \<open>Suc n < card S\<close> by blast
+  next
+    case False
+    then have "\<forall>t\<in>S. s \<le> t" by auto
+    moreover have "0 < card S"
+      using card_0_eq less.prems by blast
+    ultimately show ?thesis
+      using \<open>s \<in> S\<close>
+      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
+  qed
+qed
+
+lemma finite_bij_enumerate:
+  fixes S :: "'a::wellorder set"
+  assumes S: "finite S"
+  shows "bij_betw (enumerate S) {..<card S} S"
+proof -
+  have "\<And>n m. \<lbrakk>n \<noteq> m; n < card S; m < card S\<rbrakk> \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
+    using finite_enumerate_mono[OF _ \<open>finite S\<close>] by (auto simp: neq_iff)
+  then have "inj_on (enumerate S) {..<card S}"
+    by (auto simp: inj_on_def)
+  moreover have "\<forall>s \<in> S. \<exists>i<card S. enumerate S i = s"
+    using finite_enumerate_Ex[OF S] by auto
+  moreover note \<open>finite S\<close>
+  ultimately show ?thesis
+    unfolding bij_betw_def by (auto intro: finite_enumerate_in_set)
+qed
+
+lemma ex_bij_betw_strict_mono_card:
+  fixes M :: "'a::wellorder set"
+  assumes "finite M" 
+  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
+proof
+  show "bij_betw (enumerate M) {..<card M} M"
+    by (simp add: assms finite_bij_enumerate)
+  show "strict_mono_on (enumerate M) {..<card M}"
+    by (simp add: assms finite_enumerate_mono strict_mono_on_def)
+qed
+
 end
diff -r f424e164d752 -r 5e315defb038 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Limits.thy	Mon May 11 11:15:41 2020 +0100
@@ -2240,7 +2240,7 @@
   by (subst filterlim_cong[OF refl refl assms]) (rule refl)
 
 lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f"
-  by (auto simp: convergent_def LIMSEQ_Suc_iff)
+  by (auto simp: convergent_def filterlim_sequentially_Suc)
 
 lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f"
 proof (induct m arbitrary: f)
diff -r f424e164d752 -r 5e315defb038 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/List.thy	Mon May 11 11:15:41 2020 +0100
@@ -1707,6 +1707,9 @@
    else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)"
   by(auto dest: concat_eq_appendD)
 
+lemma hd_concat: "\<lbrakk>xs \<noteq> []; hd xs \<noteq> []\<rbrakk> \<Longrightarrow> hd (concat xs) = hd (hd xs)"
+  by (metis concat.simps(2) hd_Cons_tl hd_append2)
+
 
 subsubsection \<open>\<^const>\<open>nth\<close>\<close>
 
@@ -6084,6 +6087,33 @@
   obtains l where "strict_sorted l" "List.set l = A" "length l = card A"
   by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
 
+lemma strict_sorted_equal:
+  assumes "strict_sorted xs"
+      and "strict_sorted ys"
+      and "list.set ys = list.set xs"
+    shows "ys = xs"
+  using assms
+proof (induction xs arbitrary: ys)
+  case (Cons x xs)
+  show ?case
+  proof (cases ys)
+    case Nil
+    then show ?thesis
+      using Cons.prems by auto 
+  next
+    case (Cons y ys')
+    then have "xs = ys'"
+      by (metis Cons.prems list.inject sorted_distinct_set_unique strict_sorted_iff)
+    moreover have "x = y"
+      using Cons.prems \<open>xs = ys'\<close> local.Cons by fastforce
+    ultimately show ?thesis
+      using local.Cons by blast
+  qed
+qed auto
+
+lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. strict_sorted xs \<and> list.set xs = A"
+  by (simp add: Uniq_def strict_sorted_equal)
+
 
 subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
 
diff -r f424e164d752 -r 5e315defb038 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon May 11 11:15:41 2020 +0100
@@ -2095,7 +2095,7 @@
     have "eventually (\<lambda>y. dist y x < e) F" if "0 < e" for e :: real
     proof -
       from that have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
-        by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
+        by (subst filterlim_sequentially_Suc) (auto intro!: lim_1_over_n)
       then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
         using \<open>X \<longlonglongrightarrow> x\<close>
         unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff
diff -r f424e164d752 -r 5e315defb038 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Relation.thy	Mon May 11 11:15:41 2020 +0100
@@ -485,6 +485,10 @@
   "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
   by (simp add: single_valued_def single_valuedp_def)
 
+lemma single_valuedp_iff_Uniq:
+  "single_valuedp r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)"
+  unfolding Uniq_def single_valuedp_def by auto
+
 lemma single_valuedI:
   "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
   unfolding single_valued_def by blast
diff -r f424e164d752 -r 5e315defb038 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Series.thy	Mon May 11 11:15:41 2020 +0100
@@ -29,7 +29,7 @@
 text\<open>Variants of the definition\<close>
 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
   unfolding sums_def
-  apply (subst LIMSEQ_Suc_iff [symmetric])
+  apply (subst filterlim_sequentially_Suc [symmetric])
   apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
   done
 
@@ -68,7 +68,7 @@
 
 lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. sum f {..n})"
   by (simp_all only: summable_iff_convergent convergent_def
-        lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. sum f {..<n}"])
+        lessThan_Suc_atMost [symmetric] filterlim_sequentially_Suc[of "\<lambda>n. sum f {..<n}"])
 
 lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
   by (simp add: suminf_def sums_def lim_def)
@@ -182,6 +182,10 @@
   for a b :: 'a
   by (simp add: sums_iff)
 
+lemma sums_Uniq: "\<exists>\<^sub>\<le>\<^sub>1a. f sums a"
+  for a b :: 'a
+  by (simp add: sums_unique2 Uniq_def)
+
 lemma suminf_finite:
   assumes N: "finite N"
     and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
@@ -305,7 +309,7 @@
     unfolding lessThan_Suc_eq_insert_0
     by (simp add: ac_simps sum.atLeast1_atMost_eq image_Suc_lessThan)
   ultimately show ?thesis
-    by (auto simp: sums_def simp del: sum.lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
+    by (auto simp: sums_def simp del: sum.lessThan_Suc intro: filterlim_sequentially_Suc[THEN iffD1])
 qed
 
 lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
@@ -356,7 +360,7 @@
 lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
 proof -
   have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
-    by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
+    by (subst filterlim_sequentially_Suc) (simp add: sums_def)
   also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
     by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan sum.atLeast1_atMost_eq)
   also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
@@ -635,7 +639,7 @@
   assumes "f \<longlonglongrightarrow> c"
   shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
   unfolding sums_def
-proof (subst LIMSEQ_Suc_iff [symmetric])
+proof (subst filterlim_sequentially_Suc [symmetric])
   have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
     by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] sum_Suc_diff)
   also have "\<dots> \<longlonglongrightarrow> c - f 0"
diff -r f424e164d752 -r 5e315defb038 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Set.thy	Mon May 11 11:15:41 2020 +0100
@@ -819,6 +819,9 @@
 lemma subset_singleton_iff: "X \<subseteq> {a} \<longleftrightarrow> X = {} \<or> X = {a}"
   by blast
 
+lemma subset_singleton_iff_Uniq: "(\<exists>a. A \<subseteq> {a}) \<longleftrightarrow> (\<exists>\<^sub>\<le>\<^sub>1x. x \<in> A)"
+  unfolding Uniq_def by blast
+
 lemma singleton_conv [simp]: "{x. x = a} = {a}"
   by blast
 
@@ -1938,6 +1941,9 @@
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast
 
+lemma pairwise_disjnt_iff: "pairwise disjnt \<A> \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1 X. X \<in> \<A> \<and> x \<in> X)"
+  by (auto simp: Uniq_def disjnt_iff pairwise_def)
+
 lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
   by blast
 
diff -r f424e164d752 -r 5e315defb038 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Topological_Spaces.thy	Mon May 11 11:15:41 2020 +0100
@@ -891,6 +891,11 @@
   shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   by (auto intro!: tendsto_unique [OF assms tendsto_const])
 
+lemma (in t2_space) tendsto_unique':
+ assumes "F \<noteq> bot"
+ shows "\<exists>\<^sub>\<le>\<^sub>1l. (f \<longlongrightarrow> l) F"
+ using Uniq_def assms local.tendsto_unique by fastforce
+
 lemma Lim_in_closed_set:
   assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) F" "F \<noteq> bot" "(f \<longlongrightarrow> l) F"
   shows "l \<in> S"
@@ -1394,17 +1399,16 @@
 lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l \<Longrightarrow> f \<longlonglongrightarrow> l"
   by (rule LIMSEQ_offset [where k="Suc 0"]) simp
 
-lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
-  by (rule filterlim_sequentially_Suc)
-
 lemma LIMSEQ_lessThan_iff_atMost:
   shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
-  apply (subst LIMSEQ_Suc_iff [symmetric])
+  apply (subst filterlim_sequentially_Suc [symmetric])
   apply (simp only: lessThan_Suc_atMost)
   done
 
-lemma LIMSEQ_unique: "X \<longlonglongrightarrow> a \<Longrightarrow> X \<longlonglongrightarrow> b \<Longrightarrow> a = b"
-  for a b :: "'a::t2_space"
+lemma (in t2_space) LIMSEQ_Uniq: "\<exists>\<^sub>\<le>\<^sub>1l. X \<longlonglongrightarrow> l"
+ by (simp add: tendsto_unique')
+
+lemma (in t2_space) LIMSEQ_unique: "X \<longlonglongrightarrow> a \<Longrightarrow> X \<longlonglongrightarrow> b \<Longrightarrow> a = b"
   using trivial_limit_sequentially by (rule tendsto_unique)
 
 lemma LIMSEQ_le_const: "X \<longlonglongrightarrow> x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. a \<le> X n \<Longrightarrow> a \<le> x"
@@ -1741,6 +1745,10 @@
   for a :: "'a::perfect_space" and L M :: "'b::t2_space"
   using at_neq_bot by (rule tendsto_unique)
 
+lemma LIM_Uniq: "\<exists>\<^sub>\<le>\<^sub>1L::'b::t2_space. f \<midarrow>a\<rightarrow> L"
+  for a :: "'a::perfect_space"
+ by (auto simp add: Uniq_def LIM_unique)
+
 
 text \<open>Limits are equal for functions equal except at limit point.\<close>
 lemma LIM_equal: "\<forall>x. x \<noteq> a \<longrightarrow> f x = g x \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>a\<rightarrow> l)"
@@ -3824,4 +3832,5 @@
   then show ?thesis using open_subdiagonal closed_Diff by auto
 qed
 
+
 end
diff -r f424e164d752 -r 5e315defb038 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Transfer.thy	Mon May 11 11:15:41 2020 +0100
@@ -126,6 +126,9 @@
     (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
     (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
 
+lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
+  unfolding Uniq_def left_unique_def by force
+
 lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
 unfolding left_unique_def by blast
 
@@ -142,10 +145,16 @@
 using assms unfolding left_total_def by blast
 
 lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
-by(simp add: bi_unique_def)
+  by(simp add: bi_unique_def)
 
 lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
-by(simp add: bi_unique_def)
+  by(simp add: bi_unique_def)
+
+lemma bi_unique_iff: "bi_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z) \<and> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
+  unfolding Uniq_def bi_unique_def by force
+
+lemma right_unique_iff: "right_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
+  unfolding Uniq_def right_unique_def by force
 
 lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
 unfolding right_unique_def by fast
diff -r f424e164d752 -r 5e315defb038 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Wellfounded.thy	Mon May 11 11:15:41 2020 +0100
@@ -580,6 +580,9 @@
 lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)"
   by (simp add: less_than_def less_eq)
 
+lemma irrefl_less_than: "irrefl less_than"
+  using irrefl_def by blast
+
 lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
   using total_on_def by force+