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