--- a/src/HOL/Library/Extended_Real.thy Fri Jan 10 21:08:18 2025 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sun Jan 12 21:16:09 2025 +0000
@@ -68,10 +68,10 @@
lemma sup_continuous_iff_at_left:
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
- 'b::{complete_linorder, linorder_topology}"
+ 'b::{complete_linorder, linorder_topology}"
shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
- using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
- sup_continuous_mono[of f] by auto
+ using continuous_at_left_imp_sup_continuous sup_continuous_at_left sup_continuous_mono
+ by blast
lemma continuous_at_right_imp_inf_continuous:
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
@@ -79,8 +79,11 @@
shows "inf_continuous f"
unfolding inf_continuous_def
proof safe
- fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
- using continuous_at_Inf_mono [OF assms, of "range M"] by (simp add: image_comp)
+ fix M :: "nat \<Rightarrow> 'a"
+ assume "decseq M"
+ then show "f (INF i. M i) = (INF i. f (M i))"
+ using continuous_at_Inf_mono [OF assms, of "range M"]
+ by (simp add: image_comp)
qed
lemma inf_continuous_at_right:
@@ -96,9 +99,10 @@
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_right_sequentially[of _ top])
- fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S \<longlonglongrightarrow> x"
- from S_x have x_eq: "x = (INF i. S i)"
- by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
+ fix S :: "nat \<Rightarrow> 'a"
+ assume S: "decseq S" and S_x: "S \<longlonglongrightarrow> x"
+ then have x_eq: "x = (INF i. S i)"
+ using INF_Lim by blast
show "(\<lambda>n. f (S n)) \<longlonglongrightarrow> f x"
unfolding x_eq inf_continuousD[OF f S]
using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
@@ -109,8 +113,8 @@
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
'b::{complete_linorder, linorder_topology}"
shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f"
- using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
- inf_continuous_mono[of f] by auto
+ using continuous_at_right_imp_inf_continuous inf_continuous_at_right inf_continuous_mono
+ by blast
instantiation enat :: linorder_topology
begin
@@ -167,7 +171,7 @@
then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
by auto
then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
- by (auto simp add: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
+ by (auto simp: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
then show ?case
by auto
next
@@ -185,7 +189,7 @@
proof (rule antisym)
show "nhds \<infinity> \<le> (INF i. principal {enat i..})"
unfolding nhds_def
- using Ioi_le_Ico by (intro INF_greatest INF_lower) (auto simp add: open_enat_iff)
+ using Ioi_le_Ico by (intro INF_greatest INF_lower) (auto simp: open_enat_iff)
show "(INF i. principal {enat i..}) \<le> nhds \<infinity>"
unfolding nhds_def
by (intro INF_greatest) (force intro: INF_lower2[of "Suc _"] simp add: open_enat_iff Suc_ile_eq)
@@ -200,16 +204,15 @@
by (rule order_trans[OF _ add_mono[of aa aa 0 ba]]) auto
then have [simp]: "enat i \<le> ba \<Longrightarrow> enat i \<le> aa + ba" for aa ba i
by (metis add.commute)
- fix a b :: enat show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
- apply (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2
- filterlim_principal principal_prod_principal eventually_principal)
- subgoal for i
- by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
- subgoal for j i
- by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
- subgoal for j i
- by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
- done
+ fix a b :: enat
+ have "\<forall>\<^sub>F x in INF m n. principal ({enat n..} \<times> {enat m..}). enat i \<le> fst x + snd x"
+ "\<forall>\<^sub>F x in INF n. principal ({enat n..} \<times> {enat j}). enat i \<le> fst x + snd x"
+ "\<forall>\<^sub>F x in INF n. principal ({enat j} \<times> {enat n..}). enat i \<le> fst x + snd x"
+ for i j
+ by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
+ then show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
+ by (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2
+ filterlim_principal principal_prod_principal eventually_principal)
qed
text \<open>
@@ -221,8 +224,6 @@
datatype ereal = ereal real | PInfty | MInfty
-lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp
-
instantiation ereal :: uminus
begin
@@ -252,12 +253,12 @@
lemma
shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>"
- and MInfty_eq_minfinity[simp]: "MInfty = - \<infinity>"
- and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "- \<infinity> \<noteq> (\<infinity>::ereal)"
- and MInfty_neq_ereal[simp]: "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r"
+ and MInfty_eq_minfinity[simp]: "MInfty = -\<infinity>"
+ and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "-\<infinity> \<noteq> (\<infinity>::ereal)"
+ and MInfty_neq_ereal[simp]: "ereal r \<noteq> -\<infinity>" "-\<infinity> \<noteq> ereal r"
and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r"
and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = y"
- and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
+ and MInfty_cases[simp]: "(case -\<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
by (simp_all add: infinity_ereal_def)
declare
@@ -366,7 +367,7 @@
"ereal r + ereal p = ereal (r + p)"
| "\<infinity> + a = (\<infinity>::ereal)"
| "a + \<infinity> = (\<infinity>::ereal)"
-| "ereal r + -\<infinity> = - \<infinity>"
+| "ereal r + -\<infinity> = -\<infinity>"
| "-\<infinity> + ereal p = -(\<infinity>::ereal)"
| "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
proof goal_cases
@@ -410,7 +411,7 @@
lemma ereal_0_plus [simp]: "ereal 0 + x = x"
and plus_ereal_0 [simp]: "x + ereal 0 = x"
-by(simp_all flip: zero_ereal_def)
+ by(simp_all flip: zero_ereal_def)
instance ereal :: numeral ..
@@ -451,13 +452,13 @@
using assms by (cases rule: ereal3_cases[of a b c]) auto
lemma ereal_real: "ereal (real_of_ereal x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
- by (cases x) simp_all
+ by auto
lemma real_of_ereal_add:
fixes a b :: ereal
shows "real_of_ereal (a + b) =
(if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real_of_ereal a + real_of_ereal b else 0)"
- by (cases rule: ereal2_cases[of a b]) auto
+ by auto
subsubsection "Linear order on \<^typ>\<open>ereal\<close>"
@@ -485,14 +486,14 @@
lemma ereal_infty_less[simp]:
fixes x :: ereal
shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
- "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
- by (cases x, simp_all) (cases x, simp_all)
+ "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
+ by (cases x, simp_all)+
lemma ereal_infty_less_eq[simp]:
fixes x :: ereal
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
and "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
- by (auto simp add: less_eq_ereal_def)
+ by (auto simp: less_eq_ereal_def)
lemma ereal_less[simp]:
"ereal r < 0 \<longleftrightarrow> (r < 0)"
@@ -511,7 +512,7 @@
"0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"
"ereal r \<le> 1 \<longleftrightarrow> r \<le> 1"
"1 \<le> ereal r \<longleftrightarrow> 1 \<le> r"
- by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def)
+ by (auto simp: less_eq_ereal_def zero_ereal_def one_ereal_def)
lemma ereal_infty_less_eq2:
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"
@@ -527,16 +528,12 @@
by (cases rule: ereal2_cases[of x y]) auto
show "x \<le> y \<or> y \<le> x "
by (cases rule: ereal2_cases[of x y]) auto
- {
- assume "x \<le> y" "y \<le> x"
- then show "x = y"
- by (cases rule: ereal2_cases[of x y]) auto
- }
- {
- assume "x \<le> y" "y \<le> z"
- then show "x \<le> z"
- by (cases rule: ereal3_cases[of x y z]) auto
- }
+ assume "x \<le> y"
+ then show "y \<le> x \<Longrightarrow> x = y"
+ by (cases rule: ereal2_cases[of x y]) auto
+ show "y \<le> z \<Longrightarrow> x \<le> z"
+ using \<open>x \<le> y\<close>
+ by (cases rule: ereal3_cases[of x y z]) auto
qed
end
@@ -566,12 +563,12 @@
lemma ereal_MInfty_lessI[intro, simp]:
fixes a :: ereal
shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
- by (cases a) auto
+ by simp
lemma ereal_less_PInfty[intro, simp]:
fixes a :: ereal
shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
- by (cases a) auto
+ by simp
lemma ereal_less_ereal_Ex:
fixes a b :: ereal
@@ -590,7 +587,7 @@
assumes "a < b" and "c < d"
shows "a + c < b + d"
using assms
- by (cases a; force simp add: elim: less_ereal.elims)
+ by (cases a; force simp: elim: less_ereal.elims)
lemma ereal_minus_le_minus[simp]:
fixes a b :: ereal
@@ -643,7 +640,8 @@
lemma real_of_ereal_pos:
fixes x :: ereal
- shows "0 \<le> x \<Longrightarrow> 0 \<le> real_of_ereal x" by (cases x) auto
+ shows "0 \<le> x \<Longrightarrow> 0 \<le> real_of_ereal x"
+ by (cases x) auto
lemmas real_of_ereal_ord_simps =
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff
@@ -660,12 +658,12 @@
lemma ereal_abs_leI:
fixes x y :: ereal
shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
-by(cases x y rule: ereal2_cases)(simp_all)
+ by(cases x y rule: ereal2_cases)(simp_all)
lemma ereal_abs_add:
fixes a b::ereal
shows "abs(a+b) \<le> abs a + abs b"
-by (cases rule: ereal2_cases[of a b]) (auto)
+ by (cases rule: ereal2_cases[of a b]) (auto)
lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
by (cases x) auto
@@ -703,22 +701,13 @@
shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
by (cases rule: ereal2_cases[of b c]) auto
-lemma ereal_add_nonneg_eq_0_iff:
- fixes a b :: ereal
- shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
- by (cases a b rule: ereal2_cases) auto
-
lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)"
by auto
-lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
- by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
-
-lemma ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - (a::ereal)"
- by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
-
-lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
- by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
+lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < a"
+ and ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - a"
+ and ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> a" for a::ereal
+ using ereal_minus_le_minus ereal_minus_less_minus by fastforce+
lemmas ereal_uminus_reorder =
ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder
@@ -726,7 +715,7 @@
lemma ereal_bot:
fixes x :: ereal
assumes "\<And>B. x \<le> ereal B"
- shows "x = - \<infinity>"
+ shows "x = -\<infinity>"
proof (cases x)
case (real r)
with assms[of "r - 1"] show ?thesis
@@ -777,13 +766,7 @@
unfolding incseq_def by auto
lemma sum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
-proof (cases "finite A")
- case True
- then show ?thesis by induct auto
-next
- case False
- then show ?thesis by simp
-qed
+ by (induction A rule: infinite_finite_induct) auto
lemma sum_list_ereal [simp]: "sum_list (map (\<lambda>x. ereal (f x)) xs) = ereal (sum_list (map f xs))"
by (induction xs) simp_all
@@ -794,11 +777,7 @@
proof safe
assume *: "sum f P = \<infinity>"
show "finite P"
- proof (rule ccontr)
- assume "\<not> finite P"
- with * show False
- by auto
- qed
+ by (metis "*" Infty_neq_0(2) sum.infinite)
show "\<exists>i\<in>P. f i = \<infinity>"
proof (rule ccontr)
assume "\<not> ?thesis"
@@ -831,7 +810,8 @@
assume "\<not> ?thesis"
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
by auto
- from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
+ then obtain r where "\<forall>x\<in>A. f x = ereal (r x)"
+ by metis
with * show False
by auto
qed
@@ -855,33 +835,13 @@
shows "(\<Sum>x\<in>S. real_of_ereal (f x)) = real_of_ereal (sum f S)"
proof -
have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
- proof
- fix x
- assume "x \<in> S"
- from assms[OF this] show "\<exists>r. f x = ereal r"
- by (cases "f x") auto
- qed
- from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
+ using assms by blast
+ then obtain r where "\<forall>x\<in>S. f x = ereal (r x)"
+ by metis
then show ?thesis
by simp
qed
-lemma sum_ereal_0:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "finite A"
- and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
- shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
-proof
- assume "sum f A = 0" with assms show "\<forall>i\<in>A. f i = 0"
- proof (induction A)
- case (insert a A)
- then have "f a = 0 \<and> (\<Sum>a\<in>A. f a) = 0"
- by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: sum_nonneg)
- with insert show ?case
- by simp
- qed simp
-qed auto
-
subsubsection "Multiplication"
instantiation ereal :: "{comm_monoid_mult,sgn}"
@@ -954,7 +914,7 @@
lemma ereal_zero_mult[simp]:
fixes a :: ereal
shows "0 * a = 0"
- by (cases a) (simp_all add: zero_ereal_def)
+ by (metis ereal_mult_zero mult.commute)
lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
by (simp add: zero_ereal_def one_ereal_def)
@@ -990,7 +950,7 @@
by (cases x y rule: ereal2_cases) (auto simp: abs_mult)
lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
- by (simp_all add: zero_ereal_def one_ereal_def)
+ by (simp add: zero_ereal_def one_ereal_def)
lemma ereal_mult_minus_left[simp]:
fixes a b :: ereal
@@ -1003,11 +963,11 @@
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_mult_infty[simp]:
- "a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
+ "a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else -\<infinity>)"
by (cases a) auto
lemma ereal_infty_mult[simp]:
- "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
+ "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else -\<infinity>)"
by (cases a) auto
lemma ereal_mult_strict_right_mono:
@@ -1036,29 +996,31 @@
lemma ereal_mult_left_mono:
fixes a b c :: ereal
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
- using ereal_mult_right_mono
- by (simp add: mult.commute[of c])
+ by (simp add: ereal_mult_right_mono mult.commute)
lemma ereal_mult_mono:
fixes a b c d::ereal
assumes "b \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
shows "a * c \<le> b * d"
-by (metis ereal_mult_right_mono mult.commute order_trans assms)
+ by (metis ereal_mult_right_mono mult.commute order_trans assms)
lemma ereal_mult_mono':
fixes a b c d::ereal
assumes "a \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
shows "a * c \<le> b * d"
-by (metis ereal_mult_right_mono mult.commute order_trans assms)
+ by (metis ereal_mult_right_mono mult.commute order_trans assms)
lemma ereal_mult_mono_strict:
fixes a b c d::ereal
assumes "b > 0" "c > 0" "a < b" "c < d"
shows "a * c < b * d"
proof -
- have "c < \<infinity>" using \<open>c < d\<close> by auto
- then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
- moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
+ have "c < \<infinity>" using \<open>c < d\<close>
+ by auto
+ then have "a * c < b * c"
+ by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
+ moreover have "b * c \<le> b * d"
+ using assms(1,4) ereal_mult_left_mono by force
ultimately show ?thesis by simp
qed
@@ -1141,7 +1103,7 @@
lemma sum_ereal_right_distrib:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * sum f A = (\<Sum>n\<in>A. r * f n)"
- by (induct A rule: infinite_finite_induct) (auto simp: ereal_right_distrib sum_nonneg)
+ by (induct A rule: infinite_finite_induct) (auto simp: ereal_right_distrib sum_nonneg)
lemma sum_ereal_left_distrib:
"(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
@@ -1185,53 +1147,36 @@
lemma prod_ereal_0:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
-proof (cases "finite A")
- case True
- then show ?thesis by (induct A) auto
-qed auto
+ by (induction A rule: infinite_finite_induct) auto
lemma prod_ereal_pos:
fixes f :: "'a \<Rightarrow> ereal"
- assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+ assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
shows "0 \<le> (\<Prod>i\<in>I. f i)"
-proof (cases "finite I")
- case True
- from this pos show ?thesis
- by induct auto
-qed auto
+ using assms
+ by (induction I rule: infinite_finite_induct) auto
lemma prod_PInf:
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
-proof (cases "finite I")
- case True
- from this assms show ?thesis
- proof (induct I)
- case (insert i I)
- then have pos: "0 \<le> f i" "0 \<le> prod f I"
- by (auto intro!: prod_ereal_pos)
- from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> prod f I * f i = \<infinity>"
- by auto
- also have "\<dots> \<longleftrightarrow> (prod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> prod f I \<noteq> 0"
- using prod_ereal_pos[of I f] pos
- by (cases rule: ereal2_cases[of "f i" "prod f I"]) auto
- also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
- using insert by (auto simp: prod_ereal_0)
- finally show ?case .
- qed simp
+ using assms
+proof (induction I rule: infinite_finite_induct)
+ case (insert i I)
+ then have pos: "0 \<le> f i" "0 \<le> prod f I"
+ by (auto intro!: prod_ereal_pos)
+ from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> prod f I * f i = \<infinity>"
+ by auto
+ also have "\<dots> \<longleftrightarrow> (prod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> prod f I \<noteq> 0"
+ using prod_ereal_pos[of I f] pos
+ by (cases rule: ereal2_cases[of "f i" "prod f I"]) auto
+ also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
+ using insert by (auto simp: prod_ereal_0)
+ finally show ?case .
qed auto
lemma prod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (prod f A)"
-proof (cases "finite A")
- case True
- then show ?thesis
- by induct (auto simp: one_ereal_def)
-next
- case False
- then show ?thesis
- by (simp add: one_ereal_def)
-qed
+ by (induction A rule: infinite_finite_induct) (auto simp: one_ereal_def)
subsubsection \<open>Power\<close>
@@ -1268,18 +1213,7 @@
lemma ereal_uminus_lessThan[simp]:
fixes a :: ereal
shows "uminus ` {..<a} = {-a<..}"
-proof -
- {
- fix x
- assume "-a < x"
- then have "- x < - (- a)"
- by (simp del: ereal_uminus_uminus)
- then have "- x < a"
- by simp
- }
- then show ?thesis
- by force
-qed
+ by (force simp: ereal_uminus_less_reorder)
lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image)
@@ -1295,16 +1229,16 @@
lemma ereal_minus[simp]:
"ereal r - ereal p = ereal (r - p)"
"-\<infinity> - ereal r = -\<infinity>"
- "ereal r - \<infinity> = -\<infinity>"
+ "ereal r -\<infinity> = -\<infinity>"
"(\<infinity>::ereal) - x = \<infinity>"
- "-(\<infinity>::ereal) - \<infinity> = -\<infinity>"
+ "-(\<infinity>::ereal) -\<infinity> = -\<infinity>"
"x - -y = x + y"
"x - 0 = x"
"0 - x = -x"
by (simp_all add: minus_ereal_def)
lemma ereal_x_minus_x[simp]: "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
- by (cases x) simp_all
+ by auto
lemma ereal_eq_minus_iff:
fixes x y z :: ereal
@@ -1381,7 +1315,7 @@
lemma ereal_add_le_add_iff2:
fixes a b c :: ereal
shows "a + c \<le> b + c \<longleftrightarrow> a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
-by(cases rule: ereal3_cases[of a b c])(simp_all add: field_simps)
+ by (metis (no_types, lifting) add.commute ereal_add_le_add_iff)
lemma ereal_mult_le_mult_iff:
fixes a b c :: ereal
@@ -1413,8 +1347,7 @@
lemma ereal_between:
fixes x e :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- and "0 < e"
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>" and "0 < e"
shows "x - e < x"
and "x < x + e"
using assms by (cases x, cases e, auto)+
@@ -1435,11 +1368,11 @@
by(cases x y z rule: ereal3_cases) simp_all
lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
- by(cases x y rule: ereal2_cases) simp_all
+ by (simp add: add.commute minus_ereal_def)
lemma ereal_minus_diff_eq:
fixes x y :: ereal
- shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
+ shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> -\<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
by(cases x y rule: ereal2_cases) simp_all
lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
@@ -1522,10 +1455,9 @@
lemma zero_le_divide_ereal[simp]:
fixes a :: ereal
- assumes "0 \<le> a"
- and "0 \<le> b"
+ assumes "0 \<le> a" and "0 \<le> b"
shows "0 \<le> a / b"
- using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
+ by (simp add: assms divide_ereal_def ereal_inverse_nonneg_iff)
lemma ereal_le_divide_pos:
fixes x y z :: ereal
@@ -1582,15 +1514,14 @@
lemma ereal_mult_less_right:
fixes a b c :: ereal
- assumes "b * a < c * a"
- and "0 < a"
- and "a < \<infinity>"
+ assumes "b * a < c * a" "0 < a" "a < \<infinity>"
shows "b < c"
using assms
- by (cases rule: ereal3_cases[of a b c])
- (auto split: if_split_asm simp: zero_less_mult_iff zero_le_mult_iff)
-
-lemma ereal_mult_divide: fixes a b :: ereal shows "0 < b \<Longrightarrow> b < \<infinity> \<Longrightarrow> b * (a / b) = a"
+ by (metis order.asym ereal_mult_strict_left_mono linorder_neqE mult.commute)
+
+lemma ereal_mult_divide:
+ fixes a b :: ereal
+ shows "0 < b \<Longrightarrow> b < \<infinity> \<Longrightarrow> b * (a / b) = a"
by (cases a b rule: ereal2_cases) auto
lemma ereal_power_divide:
@@ -1609,12 +1540,10 @@
with z[of "1 / 2"] show "x \<le> y"
by (simp add: one_ereal_def)
next
- case (real r)
- note r = this
+ case r: (real r)
show "x \<le> y"
proof (cases y)
- case (real p)
- note p = this
+ case p: (real p)
have "r \<le> p"
proof (rule field_le_mult_one_interval)
fix z :: real
@@ -1624,7 +1553,7 @@
qed
then show "x \<le> y"
using p r by simp
- qed (insert y, simp_all)
+ qed (use y in simp_all)
qed simp
lemma ereal_divide_right_mono[simp]:
@@ -1647,16 +1576,15 @@
lemma ereal_divide_zero_left[simp]:
fixes a :: ereal
shows "0 / a = 0"
- by (cases a) (auto simp: zero_ereal_def)
+ using ereal_divide_eq_0_iff by blast
lemma ereal_times_divide_eq_left[simp]:
fixes a b c :: ereal
shows "b / c * a = b * a / c"
- by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff mult_less_0_iff)
+ by (metis divide_ereal_def mult.assoc mult.commute)
lemma ereal_times_divide_eq: "a * (b / c :: ereal) = a * b / c"
- by (cases a b c rule: ereal3_cases)
- (auto simp: field_simps zero_less_mult_iff)
+ by (metis ereal_times_divide_eq_left mult.commute)
lemma ereal_inverse_real [simp]: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
by auto
@@ -1672,29 +1600,26 @@
lemma ereal_distrib_left:
fixes a b c :: ereal
assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
- and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
- and "\<bar>c\<bar> \<noteq> \<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
shows "c * (a + b) = c * a + c * b"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+ by (metis assms ereal_distrib mult.commute)
lemma ereal_distrib_minus_left:
fixes a b c :: ereal
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
- and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
- and "\<bar>c\<bar> \<noteq> \<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
shows "c * (a - b) = c * a - c * b"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+ using assms ereal_distrib_left ereal_uminus_eq_reorder minus_ereal_def by auto
lemma ereal_distrib_minus_right:
fixes a b c :: ereal
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
- and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
- and "\<bar>c\<bar> \<noteq> \<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
shows "(a - b) * c = a * c - b * c"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+ by (metis assms ereal_distrib_minus_left mult.commute)
subsection "Complete lattice"
@@ -1780,8 +1705,13 @@
show "Inf {} = (top::ereal)"
unfolding top_ereal_def Inf_ereal_def
using ereal_infty_less_eq(1) ereal_less_eq(1) by blast
-qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
- simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
+ show "\<And>x::ereal. \<And>A. x \<in> A \<Longrightarrow> Inf A \<le> x"
+ "\<And>A z. (\<And>x::ereal. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
+ by (auto intro: someI2_ex ereal_complete_Inf simp: Inf_ereal_def)
+ show "\<And>x::ereal. \<And>A. x \<in> A \<Longrightarrow> x \<le> Sup A"
+ "\<And>A z. (\<And>x::ereal. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
+ by (auto intro: someI2_ex ereal_complete_Sup simp: Sup_ereal_def)
+qed
end
@@ -1844,7 +1774,7 @@
(if M = \<infinity> then UNIV
else if M = -\<infinity> then {}
else {..< real_of_ereal M})
- else if M = - \<infinity> then {}
+ else if M = -\<infinity> then {}
else if M = \<infinity> then {real_of_ereal N<..}
else {real_of_ereal N <..< real_of_ereal M})"
proof (cases "M = -\<infinity> \<or> M = \<infinity> \<or> N = -\<infinity> \<or> N = \<infinity>")
@@ -1865,7 +1795,7 @@
fixes a b::ereal
shows
"real_of_ereal ` {a<..<b} =
- (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
+ (if a < b then (if a = -\<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
@@ -1873,31 +1803,34 @@
shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
by force
-lemma
- interval_neqs:
+context
fixes r s t::real
- shows "{r<..<s} \<noteq> {t<..}"
- and "{r<..<s} \<noteq> {..<t}"
- and "{r<..<ra} \<noteq> UNIV"
- and "{r<..} \<noteq> {..<s}"
- and "{r<..} \<noteq> UNIV"
- and "{..<r} \<noteq> UNIV"
- and "{} \<noteq> {r<..}"
- and "{} \<noteq> {..<r}"
- subgoal
- by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
- subgoal
- by (metis (no_types, opaque_lifting) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
- lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
- subgoal by force
- subgoal
- by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
- lessThan_iff lessThan_non_empty less_irrefl not_le)
- subgoal by force
- subgoal by force
- subgoal using greaterThan_non_empty by blast
- subgoal using lessThan_non_empty by blast
- done
+begin
+
+lemma interval_Ioo_neq_Ioi: "{r<..<s} \<noteq> {t<..}"
+ by (simp add: set_eq_iff) (meson linordered_field_no_ub nless_le order_less_trans)
+
+lemma interval_Ioo_neq_Iio: "{r<..<s} \<noteq> {..<t}"
+ by (simp add: set_eq_iff) (meson linordered_field_no_lb order_less_irrefl order_less_trans)
+
+lemma interval_neq_ioo_UNIV: "{r<..<s} \<noteq> UNIV"
+ and interval_Ioi_neq_UNIV: "{r<..} \<noteq> UNIV"
+ and interval_Iio_neq_UNIV: "{..<r} \<noteq> UNIV"
+ by auto
+
+lemma interval_Ioi_neq_Iio: "{r<..} \<noteq> {..<s}"
+ by (simp add: set_eq_iff) (meson lt_ex order_less_irrefl order_less_trans)
+
+lemma interval_empty_neq_Ioi: "{} \<noteq> {r<..}"
+ and interval_empty_neq_Iio: "{} \<noteq> {..<r}"
+ by (auto simp: set_eq_iff linordered_field_no_ub linordered_field_no_lb)
+
+end
+
+lemmas interval_neqs = interval_Ioo_neq_Ioi interval_Ioo_neq_Iio
+ interval_neq_ioo_UNIV interval_Ioi_neq_Iio
+ interval_Ioi_neq_UNIV interval_Iio_neq_UNIV
+ interval_empty_neq_Ioi interval_empty_neq_Iio
lemma greaterThanLessThan_eq_iff:
fixes r s t u::real
@@ -1950,28 +1883,16 @@
case PInf
then show ?thesis
using assms
- apply clarsimp
- by (metis UNIV_I assms(1) ereal_less_PInfty greaterThan_iff less_eq_ereal_def less_le_trans real_image_ereal_ivl)
+ by (metis UNIV_I empty_iff greaterThan_iff order_less_le_trans real_image_ereal_ivl)
qed auto
lemma real_ereal_bound_lemma_down:
assumes s: "s \<in> real_of_ereal ` {a<..<b}"
and t: "t \<notin> real_of_ereal ` {a<..<b}"
and "t \<le> s"
- shows "a \<noteq> - \<infinity>"
-proof (cases b)
- case (real r)
- then show ?thesis
- using assms real_greaterThanLessThan_minus_infinity_eq by force
-next
- case PInf
- then show ?thesis
- using t real_greaterThanLessThan_infinity_eq by auto
-next
- case MInf
- then show ?thesis
- using s by auto
-qed
+shows "a \<noteq> -\<infinity>"
+ by (metis UNIV_I assms empty_iff lessThan_iff order_le_less_trans
+ real_greaterThanLessThan_minus_infinity_eq)
subsection "Topological space"
@@ -2005,13 +1926,19 @@
by (metis ereal_uminus_reorder(2) eventually_at_topological greaterThan_iff open_greaterThan)
qed
+
+
lemma at_infty_ereal_eq_at_top: "at \<infinity> = filtermap ereal at_top"
- unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
- top_ereal_def[symmetric]
- apply (subst eventually_nhds_top[of 0])
- apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
- apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans)
- done
+proof -
+ have "\<And>P b. \<forall>z. b \<le> z \<and> b \<noteq> z \<longrightarrow> P (ereal z) \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. P (ereal n)"
+ by (metis gt_ex order_less_le order_less_le_trans)
+ then show ?thesis
+ unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
+ top_ereal_def[symmetric]
+ apply (subst eventually_nhds_top[of 0])
+ apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
+ done
+qed
lemma ereal_Lim_uminus: "(f \<longlongrightarrow> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) \<longlongrightarrow> - f0) net"
using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
@@ -2024,7 +1951,8 @@
by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]:
- assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
+ assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F"
+ shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
proof -
have *: "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F" if "0 < c" "c < \<infinity>" for c :: ereal
using that
@@ -2039,7 +1967,7 @@
using c by (cases c) auto
then show ?thesis
proof (elim disjE conjE)
- assume "- \<infinity> < c" "c < 0"
+ assume "-\<infinity> < c" "c < 0"
then have "0 < - c" "- c < \<infinity>"
by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
then have "((\<lambda>x. (- c) * f x) \<longlongrightarrow> (- c) * x) F"
@@ -2050,26 +1978,28 @@
qed
lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:
- assumes "x \<noteq> 0" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
+ assumes "x \<noteq> 0" and f: "(f \<longlongrightarrow> x) F"
+ shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
proof cases
assume "\<bar>c\<bar> = \<infinity>"
show ?thesis
proof (rule filterlim_cong[THEN iffD1, OF refl refl _ tendsto_const])
have "0 < x \<or> x < 0"
- using \<open>x \<noteq> 0\<close> by (auto simp add: neq_iff)
+ using \<open>x \<noteq> 0\<close> by (auto simp: neq_iff)
then show "eventually (\<lambda>x'. c * x = c * f x') F"
proof
assume "0 < x" from order_tendstoD(1)[OF f this] show ?thesis
- by eventually_elim (insert \<open>0<x\<close> \<open>\<bar>c\<bar> = \<infinity>\<close>, auto)
+ by eventually_elim (use \<open>0<x\<close> \<open>\<bar>c\<bar> = \<infinity>\<close> in auto)
next
assume "x < 0" from order_tendstoD(2)[OF f this] show ?thesis
- by eventually_elim (insert \<open>x<0\<close> \<open>\<bar>c\<bar> = \<infinity>\<close>, auto)
+ by eventually_elim (use \<open>x<0\<close> \<open>\<bar>c\<bar> = \<infinity>\<close> in auto)
qed
qed
qed (rule tendsto_cmult_ereal[OF _ f])
lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
- assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> x + y) F"
+ assumes c: "y \<noteq> -\<infinity>" "x \<noteq> -\<infinity>" and f: "(f \<longlongrightarrow> x) F"
+ shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> x + y) F"
apply (intro tendsto_compose[OF _ f])
apply (auto intro!: order_tendstoI simp: eventually_at_topological)
apply (rule_tac x="{a - y <..}" in exI)
@@ -2079,7 +2009,8 @@
done
lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]:
- assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> x + y) F"
+ assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F"
+ shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> x + y) F"
apply (intro tendsto_compose[OF _ f])
apply (auto intro!: order_tendstoI simp: eventually_at_topological)
apply (rule_tac x="{a - y <..}" in exI)
@@ -2150,12 +2081,6 @@
shows "(INF x\<in>S. - f x) = - (SUP x\<in>S. f x)"
using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: image_comp)
-lemma ereal_SUP_uminus:
- fixes f :: "'a \<Rightarrow> ereal"
- shows "(SUP i \<in> R. - f i) = - (INF i \<in> R. f i)"
- using ereal_Sup_uminus_image_eq[of "f`R"]
- by (simp add: image_image)
-
lemma ereal_SUP_not_infty:
fixes f :: "_ \<Rightarrow> ereal"
shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>Sup (f ` A)\<bar> \<noteq> \<infinity>"
@@ -2171,13 +2096,7 @@
lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set"
shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
-proof
- assume "uminus ` X = Y"
- then have "uminus ` uminus ` X = uminus ` Y"
- by (simp add: inj_image_eq_iff)
- then show "X = uminus ` Y"
- by (simp add: image_image)
-qed (simp add: image_image)
+ by (metis ereal_minus_minus_image)
lemma Sup_eq_MInfty:
fixes S :: "ereal set"
@@ -2200,7 +2119,7 @@
shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
unfolding top_ereal_def[symmetric] by auto
-lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
+lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> -\<infinity>"
by auto
lemma Sup_ereal_close:
@@ -2215,15 +2134,11 @@
assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>"
and "0 < e"
shows "\<exists>x\<in>X. x < Inf X + e"
-proof (rule Inf_less_iff[THEN iffD1])
- show "Inf X < Inf X + e"
- using assms by (cases e) auto
-qed
+ by (meson Inf_less_iff assms ereal_between(2))
lemma SUP_PInfty:
"(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i\<in>A. f i :: ereal) = \<infinity>"
- unfolding top_ereal_def[symmetric] SUP_eq_top_iff
- by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
+ by (meson SUP_upper2 less_PInf_Ex_of_nat linorder_not_less)
lemma SUP_nat_Infty: "(SUP i. ereal (real i)) = \<infinity>"
by (rule SUP_PInfty) auto
@@ -2231,7 +2146,7 @@
lemma SUP_ereal_add_left:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
shows "(SUP i\<in>I. f i + c :: ereal) = (SUP i\<in>I. f i) + c"
-proof (cases "(SUP i\<in>I. f i) = - \<infinity>")
+proof (cases "(SUP i\<in>I. f i) = -\<infinity>")
case True
then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
unfolding Sup_eq_MInfty by auto
@@ -2254,7 +2169,7 @@
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
shows "(SUP i\<in>I. c - f i :: ereal) = c - (INF i\<in>I. f i)"
using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
- by (simp add: ereal_SUP_uminus minus_ereal_def)
+ by (simp add: ereal_SUP_uminus_eq minus_ereal_def)
lemma SUP_ereal_minus_left:
assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
@@ -2269,15 +2184,14 @@
using \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close> by (cases c b rule: ereal2_cases) auto
show ?thesis
using SUP_ereal_add_right[OF \<open>I \<noteq> {}\<close>, of "-c" f] \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close>
- by (auto simp add: * ereal_SUP_uminus_eq)
+ by (auto simp: * ereal_SUP_uminus_eq)
qed
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
shows "Sup (f ` UNIV) + y \<le> z"
- unfolding SUP_ereal_add_left[OF UNIV_not_empty \<open>y \<noteq> -\<infinity>\<close>, symmetric]
- by (rule SUP_least assms)+
+ by (metis SUP_ereal_add_left SUP_least UNIV_not_empty assms)
lemma SUP_combine:
fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
@@ -2295,13 +2209,21 @@
assumes inc: "incseq f" "incseq g"
and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
- apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
- apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
- apply (subst (2) add.commute)
- apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
- apply (subst (2) add.commute)
- apply (rule SUP_combine[symmetric] add_mono inc[THEN monoD] | assumption)+
- done
+proof -
+ have "\<And>i j k l. \<lbrakk>i \<le> j; k \<le> l\<rbrakk> \<Longrightarrow> f i + g k \<le> f j + g l"
+ by (meson add_mono inc incseq_def)
+ then have "(SUP i. f i + g i) = (SUP i j. f i + g j)"
+ by (simp add: SUP_combine)
+ also have "... = (SUP i j. g j + f i)"
+ by (simp add: add.commute)
+ also have "... = (SUP i. Sup (range g) + f i)"
+ by (simp add: SUP_ereal_add_left pos(1))
+ also have "... = (SUP i. f i + Sup (range g))"
+ by (simp add: add.commute)
+ also have "... = Sup (f ` UNIV) + Sup (g ` UNIV)"
+ by (simp add: SUP_eq_iff SUP_ereal_add_left pos(2))
+ finally show ?thesis .
+qed
lemma INF_eq_minf: "(INF i\<in>I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
@@ -2328,11 +2250,8 @@
assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<ge> f k + g k"
shows "(INF i\<in>I. f i + g i) = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
-proof cases
- assume "I = {}" then show ?thesis
- by (simp add: top_ereal_def)
-next
- assume "I \<noteq> {}"
+proof (cases "I = {}")
+ case False
show ?thesis
proof (rule antisym)
show "(INF i\<in>I. f i) + (INF i\<in>I. g i) \<le> (INF i\<in>I. f i + g i)"
@@ -2346,7 +2265,7 @@
using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
finally show "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. f i) + (INF i\<in>I. g i)" .
qed
-qed
+qed (simp add: top_ereal_def)
lemma INF_ereal_add:
fixes f :: "nat \<Rightarrow> ereal"
@@ -2363,34 +2282,24 @@
also have "\<dots> = Inf (f ` UNIV) + Inf (g ` UNIV)"
unfolding ereal_INF_uminus_eq
using assms INF_less
- by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
+ by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus_eq fin *)
finally show ?thesis .
qed
lemma SUP_ereal_add_pos:
fixes f g :: "nat \<Rightarrow> ereal"
- assumes inc: "incseq f" "incseq g"
- and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
+ assumes "incseq f" "incseq g"
+ and "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
-proof (intro SUP_ereal_add inc)
- fix i
- show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
- using pos[of i] by auto
-qed
+ by (simp add: SUP_ereal_add assms)
lemma SUP_ereal_sum:
fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. Sup ((f n) ` UNIV))"
-proof (cases "finite A")
- case True
- then show ?thesis using assms
- by induct (auto simp: incseq_sumI2 sum_nonneg SUP_ereal_add_pos)
-next
- case False
- then show ?thesis by simp
-qed
+ using assms
+ by (induction A rule: infinite_finite_induct) (auto simp: incseq_sumI2 sum_nonneg SUP_ereal_add_pos)
lemma SUP_ereal_mult_left:
fixes f :: "'a \<Rightarrow> ereal"
@@ -2454,18 +2363,11 @@
then obtain f where f: "?P f" ..
then have "range f \<subseteq> A" "incseq f"
by (auto simp: incseq_Suc_iff)
- moreover
- have "(SUP i. f i) = Sup A"
- proof (rule tendsto_unique)
- show "f \<longlonglongrightarrow> (SUP i. f i)"
- by (rule LIMSEQ_SUP \<open>incseq f\<close>)+
- show "f \<longlonglongrightarrow> Sup A"
- using l f
- by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
- (auto simp: Sup_upper)
- qed simp
- ultimately show ?thesis
- by auto
+ then have "(SUP i. f i) = Sup A"
+ by (meson LIMSEQ_SUP LIMSEQ_le Sup_subset_mono f l_Sup
+ order_class.order_eq_iff)
+ then show ?thesis
+ by (metis \<open>incseq f\<close> \<open>range f \<subseteq> A\<close>)
qed
lemma Inf_countable_INF:
@@ -2534,7 +2436,7 @@
lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
lemma ereal_of_enat_nonneg: "ereal_of_enat n \<ge> 0"
-by(cases n) simp_all
+ by simp
lemma ereal_of_enat_Sup:
assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a \<in> A. ereal_of_enat a)"
@@ -2584,15 +2486,11 @@
by (intro exI[of _ "max x z"]) fastforce
next
case (Basis S)
- {
- fix x
- have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t"
- by (cases x) auto
- }
- moreover note Basis
+ moreover have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" for x
+ by (cases x) auto
ultimately show ?case
by (auto split: ereal.split)
-qed (fastforce simp add: vimage_Union)+
+qed (fastforce simp: vimage_Union)+
lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
unfolding open_ereal_generated
@@ -2604,15 +2502,11 @@
by (intro exI[of _ "min x z"]) fastforce
next
case (Basis S)
- {
- fix x
- have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x"
- by (cases x) auto
- }
- moreover note Basis
+ moreover have "x \<noteq> -\<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" for x
+ by (cases x) auto
ultimately show ?case
by (auto split: ereal.split)
-qed (fastforce simp add: vimage_Union)+
+qed (fastforce simp: vimage_Union)+
lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
by (intro open_vimage continuous_intros)
@@ -2627,7 +2521,7 @@
using less_ereal.elims(2) by fastforce
ultimately show ?case
by auto
-qed (auto simp add: image_Union image_Int)
+qed (auto simp: image_Union image_Int)
lemma open_image_real_of_ereal:
fixes X::"ereal set"
@@ -2674,14 +2568,12 @@
qed
lemma open_PInfty2:
- assumes "open A"
- and "\<infinity> \<in> A"
+ assumes "open A" and "\<infinity> \<in> A"
obtains x where "{ereal x<..} \<subseteq> A"
using open_PInfty[OF assms] by auto
lemma open_MInfty2:
- assumes "open A"
- and "-\<infinity> \<in> A"
+ assumes "open A" and "-\<infinity> \<in> A"
obtains x where "{..<ereal x} \<subseteq> A"
using open_MInfty[OF assms] by auto
@@ -2727,17 +2619,9 @@
lemma ereal_open_cont_interval2:
fixes S :: "ereal set"
- assumes "open S"
- and "x \<in> S"
- and x: "\<bar>x\<bar> \<noteq> \<infinity>"
+ assumes "open S" and "x \<in> S" and "\<bar>x\<bar> \<noteq> \<infinity>"
obtains a b where "a < x" and "x < b" and "{a <..< b} \<subseteq> S"
-proof -
- obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
- using assms by (rule ereal_open_cont_interval)
- with that[of "x - e" "x + e"] ereal_between[OF x, of e]
- show thesis
- by auto
-qed
+ by (meson assms ereal_between ereal_open_cont_interval)
subsubsection \<open>Convergent sequences\<close>
@@ -2768,10 +2652,10 @@
lemma tendsto_PInfty: "(f \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
proof -
- {
- fix l :: ereal
+ { fix l :: ereal
assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
- from this[THEN spec, of "real_of_ereal l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
+ from this[THEN spec, of "real_of_ereal l"]
+ have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
by (cases l) (auto elim: eventually_mono)
}
then show ?thesis
@@ -2779,19 +2663,16 @@
qed
lemma tendsto_PInfty': "(f \<longlongrightarrow> \<infinity>) F = (\<forall>r>c. eventually (\<lambda>x. ereal r < f x) F)"
-proof (subst tendsto_PInfty, intro iffI allI impI)
- assume A: "\<forall>r>c. eventually (\<lambda>x. ereal r < f x) F"
- fix r :: real
- from A have A: "eventually (\<lambda>x. ereal r < f x) F" if "r > c" for r using that by blast
- show "eventually (\<lambda>x. ereal r < f x) F"
- proof (cases "r > c")
- case False
- hence B: "ereal r \<le> ereal (c + 1)" by simp
- have "c < c + 1" by simp
- from A[OF this] show "eventually (\<lambda>x. ereal r < f x) F"
- by eventually_elim (rule le_less_trans[OF B])
- qed (simp add: A)
-qed simp
+proof -
+ { fix r :: real
+ assume "\<forall>r>c. eventually (\<lambda>x. ereal r < f x) F"
+ then have "eventually (\<lambda>x. ereal r < f x) F"
+ if "r > c" for r using that by blast
+ then have "eventually (\<lambda>x. ereal r < f x) F"
+ by (smt (verit, del_insts) ereal_less_le eventually_mono gt_ex)
+ } then show ?thesis
+ using tendsto_PInfty by blast
+qed
lemma tendsto_PInfty_eq_at_top:
"((\<lambda>z. ereal (f z)) \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
@@ -2998,18 +2879,18 @@
lemma ereal_less_divide_pos:
fixes x y :: ereal
shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
- by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
+ by (simp add: ereal_less_divide_iff mult.commute)
lemma ereal_divide_less_pos:
fixes x y z :: ereal
shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
- by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
+ by (simp add: ereal_divide_less_iff mult.commute)
lemma ereal_divide_eq:
fixes a b c :: ereal
shows "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
- by (cases rule: ereal3_cases[of a b c])
- (simp_all add: field_simps)
+ by (metis ereal_divide_same ereal_times_divide_eq mult.commute
+ mult.right_neutral)
lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) \<noteq> -\<infinity>"
by (cases a) auto
@@ -3023,15 +2904,7 @@
using assms by auto
lemma real_ereal_id: "real_of_ereal \<circ> ereal = id"
-proof -
- {
- fix x
- have "(real_of_ereal \<circ> ereal) x = id x"
- by auto
- }
- then show ?thesis
- using ext by blast
-qed
+ by auto
lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
by (metis range_ereal open_ereal open_UNIV)
@@ -3040,7 +2913,7 @@
fixes a b c :: ereal
shows "c * (a + b) \<le> c * a + c * b"
by (cases rule: ereal3_cases[of a b c])
- (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
+ (auto simp: field_simps not_le mult_le_0_iff mult_less_0_iff)
lemma ereal_pos_distrib:
fixes a b c :: ereal
@@ -3049,7 +2922,7 @@
shows "c * (a + b) = c * a + c * b"
using assms
by (cases rule: ereal3_cases[of a b c])
- (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
+ (auto simp: field_simps not_le mult_le_0_iff mult_less_0_iff)
lemma ereal_LimI_finite:
fixes x :: ereal
@@ -3092,12 +2965,9 @@
qed
lemma tendsto_obtains_N:
- assumes "f \<longlonglongrightarrow> f0"
- assumes "open S"
- and "f0 \<in> S"
+ assumes "f \<longlonglongrightarrow> f0" "open S" "f0 \<in> S"
obtains N where "\<forall>n\<ge>N. f n \<in> S"
- using assms using tendsto_def
- using lim_explicit[of f f0] assms by auto
+ using assms lim_explicit by blast
lemma ereal_LimI_finite_iff:
fixes x :: ereal
@@ -3110,10 +2980,8 @@
fix r :: ereal
assume "r > 0"
then obtain N where "\<forall>n\<ge>N. u n \<in> {x - r <..< x + r}"
- apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
- using lim ereal_between[of x r] assms \<open>r > 0\<close>
- apply auto
- done
+ using lim ereal_between[of x r] assms \<open>r > 0\<close> tendsto_obtains_N[of u x "{x - r <..< x + r}"]
+ by auto
then have "\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
using ereal_minus_less[of r x]
by (cases r) auto
@@ -3129,7 +2997,7 @@
lemma ereal_Limsup_uminus:
fixes f :: "'a \<Rightarrow> ereal"
shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
- unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus_eq ..
+ unfolding Limsup_def Liminf_def ereal_SUP_uminus_eq ereal_INF_uminus_eq ..
lemma liminf_bounded_iff:
fixes x :: "nat \<Rightarrow> ereal"
@@ -3148,7 +3016,7 @@
let ?INF = "\<lambda>P g. Inf (g ` (Collect P))"
show "?F \<noteq> {}"
by (auto intro: eventually_True)
- show "(SUP P\<in>?F. ?INF P g) \<noteq> - \<infinity>"
+ show "(SUP P\<in>?F. ?INF P g) \<noteq> -\<infinity>"
unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
have "(SUP P\<in>?F. ?INF P f + (SUP P\<in>?F. ?INF P g)) \<le> (SUP P\<in>?F. (SUP P'\<in>?F. ?INF P f + ?INF P' g))"
@@ -3161,7 +3029,7 @@
by (intro add_mono INF_mono) auto
also have "\<dots> = (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)"
proof (rule SUP_ereal_add_right[symmetric])
- show "Inf (f ` {x. P x \<and> 0 \<le> f x}) \<noteq> - \<infinity>"
+ show "Inf (f ` {x. P x \<and> 0 \<le> f x}) \<noteq> -\<infinity>"
unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
qed fact
@@ -3186,7 +3054,7 @@
and x: "x \<ge> 0"
shows "(SUP i\<in>Y. f i) * ereal x = (SUP i\<in>Y. f i * ereal x)" (is "?lhs = ?rhs")
proof(cases "x = 0")
- case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
+ case True thus ?thesis by(auto simp: nonempty zero_ereal_def[symmetric])
next
case False
show ?thesis
@@ -3216,7 +3084,7 @@
lemma Sup_ereal_mult_left':
"\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i\<in>Y. f i) = (SUP i\<in>Y. ereal x * f i)"
-by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
+ by (smt (verit) Sup.SUP_cong Sup_ereal_mult_right' mult.commute)
lemma sup_continuous_add[order_continuous_intros]:
fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
@@ -3240,9 +3108,10 @@
using sup_continuous_mult_right[of c f] by (simp add: mult_ac)
lemma sup_continuous_ereal_of_enat[order_continuous_intros]:
- assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. ereal_of_enat (f x))"
- by (rule sup_continuous_compose[OF _ f])
- (auto simp: sup_continuous_def ereal_of_enat_SUP)
+ assumes f: "sup_continuous f"
+ shows "sup_continuous (\<lambda>x. ereal_of_enat (f x))"
+ by (metis UNIV_not_empty ereal_of_enat_SUP f sup_continuous_compose
+ sup_continuous_def)
subsubsection \<open>Sums\<close>
@@ -3250,14 +3119,7 @@
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<And>i. 0 \<le> f i"
shows "f sums (SUP n. \<Sum>i<n. f i)"
-proof -
- have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
- using add_mono[OF _ assms]
- by (auto intro!: incseq_SucI)
- from LIMSEQ_SUP[OF this]
- show ?thesis unfolding sums_def
- by (simp add: atLeast0LessThan)
-qed
+ by (simp add: LIMSEQ_SUP assms incseq_sumI sums_def)
lemma summable_ereal_pos:
fixes f :: "nat \<Rightarrow> ereal"
@@ -3279,32 +3141,17 @@
lemma suminf_bound:
fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
- and pos: "\<And>n. 0 \<le> f n"
+ assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" "\<And>n. 0 \<le> f n"
shows "suminf f \<le> x"
-proof (rule Lim_bounded)
- have "summable f" using pos[THEN summable_ereal_pos] .
- then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
- by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
- show "\<forall>n\<ge>0. sum f {..<n} \<le> x"
- using assms by auto
-qed
+ by (simp add: SUP_least assms suminf_ereal_eq_SUP)
lemma suminf_bound_add:
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
- and pos: "\<And>n. 0 \<le> f n"
+ and "\<And>n. 0 \<le> f n"
and "y \<noteq> -\<infinity>"
shows "suminf f + y \<le> x"
-proof (cases y)
- case (real r)
- then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
- using assms by (simp add: ereal_le_minus)
- then have "(\<Sum> n. f n) \<le> x - y"
- using pos by (rule suminf_bound)
- then show "(\<Sum> n. f n) + y \<le> x"
- using assms real by (simp add: ereal_le_minus)
-qed (insert assms, auto)
+ by (simp add: SUP_ereal_le_addI assms suminf_ereal_eq_SUP)
lemma suminf_upper:
fixes f :: "nat \<Rightarrow> ereal"
@@ -3325,20 +3172,7 @@
assumes "\<And>N. f N \<le> g N"
and "\<And>N. 0 \<le> f N"
shows "suminf f \<le> suminf g"
-proof (safe intro!: suminf_bound)
- fix n
- {
- fix N
- have "0 \<le> g N"
- using assms(2,1)[of N] by auto
- }
- have "sum f {..<n} \<le> sum g {..<n}"
- using assms by (auto intro: sum_mono)
- also have "\<dots> \<le> suminf g"
- using \<open>\<And>N. 0 \<le> g N\<close>
- by (rule suminf_upper)
- finally show "sum f {..<n} \<le> suminf g" .
-qed (rule assms(2))
+ by (meson assms order_trans suminf_le summable_ereal_pos)
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
@@ -3353,17 +3187,14 @@
unfolding sum.distrib
by (intro assms add_nonneg_nonneg SUP_ereal_add_pos incseq_sumI sum_nonneg ballI)
with assms show ?thesis
- by (subst (1 2 3) suminf_ereal_eq_SUP) auto
+ by (simp add: suminf_ereal_eq_SUP)
qed
lemma suminf_cmult_ereal:
fixes f g :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- and "0 \<le> a"
+ assumes "\<And>i. 0 \<le> f i" and "0 \<le> a"
shows "(\<Sum>i. a * f i) = a * suminf f"
- by (auto simp: sum_ereal_right_distrib[symmetric] assms
- ereal_zero_le_0_iff sum_nonneg suminf_ereal_eq_SUP
- intro!: SUP_ereal_mult_left)
+ by (simp add: assms sum_nonneg suminf_ereal_eq_SUP sum_ereal_right_distrib flip: SUP_ereal_mult_left)
lemma suminf_PInfty:
fixes f :: "nat \<Rightarrow> ereal"
@@ -3384,14 +3215,9 @@
shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
proof -
have "\<forall>i. \<exists>r. f i = ereal r"
- proof
- fix i
- show "\<exists>r. f i = ereal r"
- using suminf_PInfty[OF assms] assms(1)[of i]
- by (cases "f i") auto
- qed
- from choice[OF this] show ?thesis
- by auto
+ by (metis abs_ereal_ge0 abs_neq_infinity_cases assms suminf_PInfty)
+ then show ?thesis
+ by metis
qed
lemma summable_ereal:
@@ -3431,19 +3257,15 @@
and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
proof -
- {
- fix i
- have "0 \<le> f i"
- using ord[of i] by auto
- }
+ have 0: "0 \<le> f i" for i
+ using ord order_trans by blast
moreover
- from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> f i\<close> fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
- from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> g i\<close> fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
- {
- fix i
- have "0 \<le> f i - g i"
- using ord[of i] by (auto simp: ereal_le_minus_iff)
- }
+ obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))"
+ using 0 fin(1) suminf_PInfty_fun by presburger
+ obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))"
+ using fin(2) ord(2) suminf_PInfty_fun by presburger
+ have "0 \<le> f i - g i" for i
+ using ord(1) by auto
moreover
have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
using assms by (auto intro!: suminf_le_pos simp: field_simps)
@@ -3458,12 +3280,7 @@
qed
lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
-proof -
- have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
- by (rule suminf_upper) auto
- then show ?thesis
- by simp
-qed
+ by (metis ereal_less_eq(1) suminf_PInfty)
lemma summable_real_of_ereal:
fixes f :: "nat \<Rightarrow> ereal"
@@ -3475,14 +3292,8 @@
using assms by (auto intro: suminf_0_le)
with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
by (cases "(\<Sum>i. f i)") auto
- {
- fix i
- have "f i \<noteq> \<infinity>"
- using f by (intro suminf_PInfty[OF _ fin]) auto
- then have "\<bar>f i\<bar> \<noteq> \<infinity>"
- using f[of i] by auto
- }
- note fin = this
+ have fin: "\<bar>f i\<bar> \<noteq> \<infinity>" for i
+ by (simp add: assms(2) f suminf_PInfty)
have "(\<lambda>i. ereal (real_of_ereal (f i))) sums (\<Sum>i. ereal (real_of_ereal (f i)))"
using f
by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
@@ -3503,24 +3314,15 @@
by (auto intro!: SUP_ereal_sum [symmetric])
show ?thesis
using assms
- apply (subst (1 2) suminf_ereal_eq_SUP)
- apply (auto intro!: SUP_upper2 SUP_commute simp: *)
- done
+ by (auto simp: suminf_ereal_eq_SUP SUP_upper2 * intro!: SUP_commute)
qed
lemma suminf_sum_ereal:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
-proof (cases "finite A")
- case True
- then show ?thesis
- using nonneg
- by induct (simp_all add: suminf_add_ereal sum_nonneg)
-next
- case False
- then show ?thesis by simp
-qed
+ using nonneg
+by (induction A rule: infinite_finite_induct; simp add: suminf_add_ereal sum_nonneg)
lemma suminf_ereal_eq_0:
fixes f :: "nat \<Rightarrow> ereal"
@@ -3583,12 +3385,7 @@
lemma suminf_ereal_finite_neg:
assumes "summable f"
shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
-proof-
- from assms obtain x where "f sums x" by blast
- hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
- from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
- thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
-qed
+ by (simp add: assms suminf_ereal')
lemma SUP_ereal_add_directed:
fixes f g :: "'a \<Rightarrow> ereal"
@@ -3685,7 +3482,7 @@
by (auto simp: image_iff ereal_uminus_eq_reorder)
then show "open (range uminus :: ereal set)"
by simp
-qed (auto simp add: image_Union image_Int)
+qed (auto simp: image_Union image_Int)
lemma ereal_uminus_complement:
fixes S :: "ereal set"
@@ -3864,7 +3661,7 @@
and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
- by (auto simp add: ereal_all_split ereal_ex_split)
+ by (auto simp: ereal_all_split ereal_ex_split)
lemma ereal_tendsto_simps1:
"((f \<circ> real_of_ereal) \<longlongrightarrow> y) (at_left (ereal x)) \<longleftrightarrow> (f \<longlongrightarrow> y) (at_left x)"
@@ -3998,7 +3795,7 @@
from assms show "continuous_on UNIV (\<lambda>a. a * ereal c)"
using tendsto_cmult_ereal[of "ereal c" "\<lambda>x. x" ]
by (force simp: continuous_on_def mult_ac)
-qed (insert assms, auto simp: mono_def ereal_mult_right_mono)
+qed (use assms in \<open>auto simp: mono_def ereal_mult_right_mono\<close>)
lemma Liminf_ereal_mult_right:
assumes "F \<noteq> bot" "(c::real) \<ge> 0"
@@ -4025,7 +3822,7 @@
lemma limsup_ereal_mult_left:
"(c::real) \<ge> 0 \<Longrightarrow> limsup (\<lambda>n. ereal c * f n) = ereal c * limsup f"
- by (subst (1 2) mult.commute, rule limsup_ereal_mult_right) simp_all
+ by (simp add: Limsup_ereal_mult_left)
lemma Limsup_add_ereal_right:
"F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. g n + (c :: ereal)) = Limsup F g + c"
@@ -4081,45 +3878,39 @@
by(cases a) simp_all
lemma not_infty_ereal: "\<bar>x\<bar> \<noteq> \<infinity> \<longleftrightarrow> (\<exists>x'. x = ereal x')"
-by(cases x) simp_all
+ by auto
lemma neq_PInf_trans: fixes x y :: ereal shows "\<lbrakk> y \<noteq> \<infinity>; x \<le> y \<rbrakk> \<Longrightarrow> x \<noteq> \<infinity>"
-by auto
+ by auto
lemma mult_2_ereal: "ereal 2 * x = x + x"
-by(cases x) simp_all
+ by(cases x) simp_all
lemma ereal_diff_le_self: "0 \<le> y \<Longrightarrow> x - y \<le> (x :: ereal)"
-by(cases x y rule: ereal2_cases) simp_all
+ by(cases x y rule: ereal2_cases) simp_all
lemma ereal_le_add_self: "0 \<le> y \<Longrightarrow> x \<le> x + (y :: ereal)"
-by(cases x y rule: ereal2_cases) simp_all
+ by(cases x y rule: ereal2_cases) simp_all
lemma ereal_le_add_self2: "0 \<le> y \<Longrightarrow> x \<le> y + (x :: ereal)"
-by(cases x y rule: ereal2_cases) simp_all
-
-lemma ereal_le_add_mono1: "\<lbrakk> x \<le> y; 0 \<le> (z :: ereal) \<rbrakk> \<Longrightarrow> x \<le> y + z"
-using add_mono by fastforce
-
-lemma ereal_le_add_mono2: "\<lbrakk> x \<le> z; 0 \<le> (y :: ereal) \<rbrakk> \<Longrightarrow> x \<le> y + z"
-using add_mono by fastforce
+ by(cases x y rule: ereal2_cases) simp_all
lemma ereal_diff_nonpos:
fixes a b :: ereal shows "\<lbrakk> a \<le> b; a = \<infinity> \<Longrightarrow> b \<noteq> \<infinity>; a = -\<infinity> \<Longrightarrow> b \<noteq> -\<infinity> \<rbrakk> \<Longrightarrow> a - b \<le> 0"
by (cases rule: ereal2_cases[of a b]) auto
lemma minus_ereal_0 [simp]: "x - ereal 0 = x"
-by(simp flip: zero_ereal_def)
+ by(simp flip: zero_ereal_def)
lemma ereal_diff_eq_0_iff: fixes a b :: ereal
shows "(\<bar>a\<bar> = \<infinity> \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity>) \<Longrightarrow> a - b = 0 \<longleftrightarrow> a = b"
-by(cases a b rule: ereal2_cases) simp_all
+ by(cases a b rule: ereal2_cases) simp_all
lemma SUP_ereal_eq_0_iff_nonneg:
fixes f :: "_ \<Rightarrow> ereal" and A
assumes nonneg: "\<forall>x\<in>A. f x \<ge> 0"
- and A:"A \<noteq> {}"
- shows "(SUP x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
+ and A:"A \<noteq> {}"
+ shows "(SUP x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> _")
proof(intro iffI ballI)
fix x
assume "?lhs" "x \<in> A"
@@ -4129,32 +3920,38 @@
lemma ereal_divide_le_posI:
fixes x y z :: ereal
- shows "x > 0 \<Longrightarrow> z \<noteq> - \<infinity> \<Longrightarrow> z \<le> x * y \<Longrightarrow> z / x \<le> y"
-by (cases rule: ereal3_cases[of x y z])(auto simp: field_simps split: if_split_asm)
-
-lemma add_diff_eq_ereal: fixes x y z :: ereal
+ shows "x > 0 \<Longrightarrow> z \<noteq> -\<infinity> \<Longrightarrow> z \<le> x * y \<Longrightarrow> z / x \<le> y"
+ by (cases rule: ereal3_cases[of x y z])(auto simp: field_simps split: if_split_asm)
+
+lemma add_diff_eq_ereal:
+ fixes x y z :: ereal
shows "x + (y - z) = x + y - z"
-by(cases x y z rule: ereal3_cases) simp_all
+ by(cases x y z rule: ereal3_cases) simp_all
lemma ereal_diff_gr0:
- fixes a b :: ereal shows "a < b \<Longrightarrow> 0 < b - a"
+ fixes a b :: ereal
+ shows "a < b \<Longrightarrow> 0 < b - a"
by (cases rule: ereal2_cases[of a b]) auto
-lemma ereal_minus_minus: fixes x y z :: ereal shows
+lemma ereal_minus_minus:
+ fixes x y z :: ereal shows
"(\<bar>y\<bar> = \<infinity> \<Longrightarrow> \<bar>z\<bar> \<noteq> \<infinity>) \<Longrightarrow> x - (y - z) = x + z - y"
-by(cases x y z rule: ereal3_cases) simp_all
-
-lemma diff_add_eq_ereal: fixes a b c :: ereal shows "a - b + c = a + c - b"
-by(cases a b c rule: ereal3_cases) simp_all
-
-lemma diff_diff_commute_ereal: fixes x y z :: ereal shows "x - y - z = x - z - y"
-by(cases x y z rule: ereal3_cases) simp_all
-
-lemma ereal_diff_eq_MInfty_iff: fixes x y :: ereal shows "x - y = -\<infinity> \<longleftrightarrow> x = -\<infinity> \<and> y \<noteq> -\<infinity> \<or> y = \<infinity> \<and> \<bar>x\<bar> \<noteq> \<infinity>"
-by(cases x y rule: ereal2_cases) simp_all
-
-lemma ereal_diff_add_inverse: fixes x y :: ereal shows "\<bar>x\<bar> \<noteq> \<infinity> \<Longrightarrow> x + y - x = y"
-by(cases x y rule: ereal2_cases) simp_all
+ by(cases x y z rule: ereal3_cases) simp_all
+
+lemma diff_diff_commute_ereal:
+ fixes x y z :: ereal
+ shows "x - y - z = x - z - y"
+ by (metis add_diff_eq_ereal ereal_add_uminus_conv_diff)
+
+lemma ereal_diff_eq_MInfty_iff:
+ fixes x y :: ereal
+ shows "x - y = -\<infinity> \<longleftrightarrow> x = -\<infinity> \<and> y \<noteq> -\<infinity> \<or> y = \<infinity> \<and> \<bar>x\<bar> \<noteq> \<infinity>"
+ by(cases x y rule: ereal2_cases) simp_all
+
+lemma ereal_diff_add_inverse:
+ fixes x y :: ereal
+ shows "\<bar>x\<bar> \<noteq> \<infinity> \<Longrightarrow> x + y - x = y"
+ by(cases x y rule: ereal2_cases) simp_all
lemma tendsto_diff_ereal:
fixes x y :: ereal
@@ -4186,7 +3983,7 @@
text \<open>A small list of simple arithmetic expressions.\<close>
-value "- \<infinity> :: ereal"
+value "-\<infinity> :: ereal"
value "\<bar>-\<infinity>\<bar> :: ereal"
value "4 + 5 / 4 - ereal 2 :: ereal"
value "ereal 3 < \<infinity>"
--- a/src/HOL/Library/Word.thy Fri Jan 10 21:08:18 2025 +0100
+++ b/src/HOL/Library/Word.thy Sun Jan 12 21:16:09 2025 +0000
@@ -99,20 +99,10 @@
proof -
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
for k :: int
- proof
- assume ?P
- then show ?Q
- by auto
- next
- assume ?Q
- then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
- then have "even (take_bit LENGTH('a) k)"
- by simp
- then show ?P
- by simp
- qed
- show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
- transfer_prover
+ by (metis dvd_triv_left evenE even_take_bit_eq len_not_eq_0)
+ show ?thesis
+ unfolding even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]
+ by transfer_prover
qed
end
@@ -898,26 +888,17 @@
for a b :: \<open>'a::len word\<close>
using that by transfer (auto simp: nat_less_le bit_eq_iff bit_take_bit_iff)
-lemma bit_imp_le_length:
- \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close>
- for w :: \<open>'a::len word\<close>
- using that by transfer simp
+lemma bit_imp_le_length: \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close> for w :: \<open>'a::len word\<close>
+ by (meson bit_word.rep_eq that)
lemma not_bit_length [simp]:
\<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
- by transfer simp
+ using bit_imp_le_length by blast
lemma finite_bit_word [simp]:
\<open>finite {n. bit w n}\<close>
for w :: \<open>'a::len word\<close>
-proof -
- have \<open>{n. bit w n} \<subseteq> {0..LENGTH('a)}\<close>
- by (auto dest: bit_imp_le_length)
- moreover have \<open>finite {0..LENGTH('a)}\<close>
- by simp
- ultimately show ?thesis
- by (rule finite_subset)
-qed
+ by (metis bit_imp_le_length bounded_nat_set_is_finite mem_Collect_eq)
lemma bit_numeral_word_iff [simp]:
\<open>bit (numeral w :: 'a::len word) n
@@ -969,16 +950,7 @@
proof -
show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
- proof -
- from that
- have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
- = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
- by simp
- moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
- by simp
- ultimately show ?thesis
- by (simp add: take_bit_push_bit)
- qed
+ by (metis le_add2 push_bit_take_bit take_bit_tightened that)
qed
lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
@@ -1335,12 +1307,7 @@
lemma uint_div_distrib:
\<open>uint (v div w) = uint v div uint w\<close>
-proof -
- have \<open>int (unat (v div w)) = int (unat v div unat w)\<close>
- by (simp add: unat_div_distrib)
- then show ?thesis
- by (simp add: of_nat_div)
-qed
+ by (metis int_ops(8) of_nat_unat unat_div_distrib)
lemma unat_drop_bit_eq:
\<open>unat (drop_bit n w) = drop_bit n (unat w)\<close>
@@ -1348,12 +1315,7 @@
lemma uint_mod_distrib:
\<open>uint (v mod w) = uint v mod uint w\<close>
-proof -
- have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close>
- by (simp add: unat_mod_distrib)
- then show ?thesis
- by (simp add: of_nat_mod)
-qed
+ by (metis int_ops(9) of_nat_unat unat_mod_distrib)
context semiring_bit_operations
begin
@@ -1570,18 +1532,8 @@
fix k :: int
show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) 1 div take_bit LENGTH('a) k) =
take_bit LENGTH('a) (of_bool (take_bit LENGTH('a) k = take_bit LENGTH('a) 1))\<close>
- proof (cases \<open>take_bit LENGTH('a) k > 1\<close>)
- case False
- with take_bit_nonnegative [of \<open>LENGTH('a)\<close> k]
- have \<open>take_bit LENGTH('a) k = 0 \<or> take_bit LENGTH('a) k = 1\<close>
- by linarith
- then show ?thesis
- by auto
- next
- case True
- then show ?thesis
- by simp
- qed
+ using take_bit_nonnegative [of \<open>LENGTH('a)\<close> k]
+ by (smt (verit, best) div_by_1 of_bool_eq take_bit_of_0 take_bit_of_1 zdiv_eq_0_iff)
qed
lemma mod_word_one [simp]:
@@ -1594,17 +1546,7 @@
lemma mod_word_by_minus_1_eq [simp]:
\<open>w mod - 1 = w * of_bool (w < - 1)\<close> for w :: \<open>'a::len word\<close>
-proof (cases \<open>w = - 1\<close>)
- case True
- then show ?thesis
- by simp
-next
- case False
- moreover have \<open>w < - 1\<close>
- using False by (simp add: word_order.not_eq_extremum)
- ultimately show ?thesis
- by (simp add: mod_word_less)
-qed
+ using mod_word_less word_order.not_eq_extremum by fastforce
text \<open>Legacy theorems:\<close>
@@ -1776,12 +1718,12 @@
lemma wi_less:
"(word_of_int n < (word_of_int m :: 'a::len word)) =
(n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
- by transfer (simp add: take_bit_eq_mod)
+ by (simp add: uint_word_of_int word_less_def)
lemma wi_le:
"(word_of_int n \<le> (word_of_int m :: 'a::len word)) =
(n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))"
- by transfer (simp add: take_bit_eq_mod)
+ by (simp add: uint_word_of_int word_le_def)
subsection \<open>Bit-wise operations\<close>
@@ -1790,21 +1732,17 @@
includes bit_operations_syntax
begin
-lemma uint_take_bit_eq:
- \<open>uint (take_bit n w) = take_bit n (uint w)\<close>
- by transfer (simp add: ac_simps)
-
lemma take_bit_word_eq_self:
\<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
using that by transfer simp
lemma take_bit_length_eq [simp]:
\<open>take_bit LENGTH('a) w = w\<close> for w :: \<open>'a::len word\<close>
- by (rule take_bit_word_eq_self) simp
+ by (simp add: nat_le_linear take_bit_word_eq_self)
lemma bit_word_of_int_iff:
\<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
- by transfer rule
+ by (metis Word_eq_word_of_int bit_word.abs_eq)
lemma bit_uint_iff:
\<open>bit (uint w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w n\<close>
@@ -1819,13 +1757,13 @@
lemma bit_word_ucast_iff:
\<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
- by transfer (simp add: bit_take_bit_iff ac_simps)
+ by (meson bit_imp_possible_bit bit_unsigned_iff possible_bit_word)
lemma bit_word_scast_iff:
\<open>bit (scast w :: 'b::len word) n \<longleftrightarrow>
n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close>
for w :: \<open>'a::len word\<close>
- by transfer (auto simp: bit_signed_take_bit_iff le_less min_def)
+ by (metis One_nat_def bit_sint_iff bit_word_of_int_iff of_int_sint)
lemma bit_word_iff_drop_bit_and [code]:
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
@@ -1848,7 +1786,8 @@
lemma map_bit_range_eq_if_take_bit_eq:
\<open>map (bit k) [0..<n] = map (bit l) [0..<n]\<close>
if \<open>take_bit n k = take_bit n l\<close> for k l :: int
-using that proof (induction n arbitrary: k l)
+ using that
+proof (induction n arbitrary: k l)
case 0
then show ?case
by simp
@@ -1861,7 +1800,7 @@
moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int
by (simp add: fun_eq_iff bit_Suc)
moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close>
- by (auto simp: take_bit_Suc elim!: evenE oddE) arith+
+ by (metis Zero_neq_Suc even_take_bit_eq)
ultimately show ?case
by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) (simp add: bit_0)
qed
@@ -1917,10 +1856,9 @@
\<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
- apply (auto simp: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
- apply (metis Suc_pred add.commute le_less_Suc_eq len_gt_0 less_diff_conv)
- apply (metis le_antisym less_eq_decr_length_iff)
- done
+ apply (simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
+ by (metis add.commute add_lessD1 le_antisym less_diff_conv less_eq_decr_length_iff
+ nat_less_le)
lemma [code]:
\<open>Word.the_int (signed_drop_bit n w) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))\<close>
@@ -1968,18 +1906,19 @@
lemma set_bit_eq_idem_iff:
\<open>Bit_Operations.set_bit n w = w \<longleftrightarrow> bit w n \<or> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: bit_eq_iff) (auto simp: bit_simps not_le)
+ unfolding bit_eq_iff
+ by (auto simp: bit_simps not_le)
lemma unset_bit_eq_idem_iff:
\<open>unset_bit n w = w \<longleftrightarrow> bit w n \<longrightarrow> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: bit_eq_iff) (auto simp: bit_simps dest: bit_imp_le_length)
+ unfolding bit_eq_iff
+ by (auto simp: bit_simps dest: bit_imp_le_length)
lemma flip_bit_eq_idem_iff:
\<open>flip_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
- using linorder_le_less_linear
- by (simp add: bit_eq_iff) (auto simp: bit_simps)
+ by (simp add: flip_bit_eq_if set_bit_eq_idem_iff unset_bit_eq_idem_iff)
subsection \<open>Rotation\<close>
@@ -1988,28 +1927,20 @@
is \<open>\<lambda>n k. concat_bit (LENGTH('a) - n mod LENGTH('a))
(drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k))
(take_bit (n mod LENGTH('a)) k)\<close>
- subgoal for n k l
- by (simp add: concat_bit_def nat_le_iff less_imp_le
- take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>n mod LENGTH('a::len)\<close>])
- done
+ using take_bit_tightened by fastforce
lift_definition word_rotl :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close>
is \<open>\<lambda>n k. concat_bit (n mod LENGTH('a))
(drop_bit (LENGTH('a) - n mod LENGTH('a)) (take_bit LENGTH('a) k))
(take_bit (LENGTH('a) - n mod LENGTH('a)) k)\<close>
- subgoal for n k l
- by (simp add: concat_bit_def nat_le_iff less_imp_le
- take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>LENGTH('a) - n mod LENGTH('a::len)\<close>])
- done
+ using take_bit_tightened by fastforce
lift_definition word_roti :: \<open>int \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close>
is \<open>\<lambda>r k. concat_bit (LENGTH('a) - nat (r mod int LENGTH('a)))
(drop_bit (nat (r mod int LENGTH('a))) (take_bit LENGTH('a) k))
(take_bit (nat (r mod int LENGTH('a))) k)\<close>
- subgoal for r k l
- by (simp add: concat_bit_def nat_le_iff less_imp_le
- take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>nat (r mod int LENGTH('a::len))\<close>])
- done
+ by (smt (verit, best) len_gt_0 nat_le_iff of_nat_0_less_iff pos_mod_bound
+ take_bit_tightened)
lemma word_rotl_eq_word_rotr [code]:
\<open>word_rotl n = (word_rotr (LENGTH('a) - n mod LENGTH('a)) :: 'a::len word \<Rightarrow> 'a word)\<close>
@@ -2177,12 +2108,12 @@
by transfer simp
lemma word_numeral_alt: "numeral b = word_of_int (numeral b)"
- by (induct b, simp_all only: numeral.simps word_of_int_homs)
+ by simp
declare word_numeral_alt [symmetric, code_abbrev]
lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)"
- by (simp only: word_numeral_alt wi_hom_neg)
+ by simp
declare word_neg_numeral_alt [symmetric, code_abbrev]
@@ -2269,18 +2200,14 @@
by (fact of_int_1)
lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
- by (simp add: wi_hom_syms)
+ by simp
lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len word) = numeral bin"
- by (fact of_int_numeral)
-
-lemma word_of_int_neg_numeral [simp]:
- "(word_of_int (- numeral bin) :: 'a::len word) = - numeral bin"
- by (fact of_int_neg_numeral)
+ by simp
lemma word_int_case_wi:
"word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len))"
- by transfer (simp add: take_bit_eq_mod)
+ by (simp add: uint_word_of_int word_int_case_eq_uint)
lemma word_int_split:
"P (word_int_case f x) =
@@ -2290,7 +2217,7 @@
lemma word_int_split_asm:
"P (word_int_case f x) =
(\<nexists>n. x = (word_of_int n :: 'b::len word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len) \<and> \<not> P (f n))"
- by transfer (auto simp: take_bit_eq_mod)
+ using word_int_split by auto
lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
by transfer simp
@@ -2316,7 +2243,7 @@
lemma bin_nth_uint_imp: "bit (uint w) n \<Longrightarrow> n < LENGTH('a)"
for w :: "'a::len word"
- by transfer (simp add: bit_take_bit_iff)
+ by (simp add: bit_uint_iff)
lemma bin_nth_sint:
"LENGTH('a) \<le> n \<Longrightarrow>
@@ -2490,13 +2417,7 @@
lemma bit_last_iff:
\<open>bit w (LENGTH('a) - Suc 0) \<longleftrightarrow> sint w < 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
for w :: \<open>'a::len word\<close>
-proof -
- have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close>
- by (simp add: bit_uint_iff)
- also have \<open>\<dots> \<longleftrightarrow> ?Q\<close>
- by (simp add: sint_uint)
- finally show ?thesis .
-qed
+ by (simp add: bit_unsigned_iff sint_uint)
lemma drop_bit_eq_zero_iff_not_bit_last:
\<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close>
@@ -2624,7 +2545,7 @@
lemma take_bit_word_beyond_length_eq:
\<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
- using that by transfer simp
+ by (simp add: take_bit_word_eq_self that)
lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b
lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b
@@ -2726,28 +2647,39 @@
and "uint (1 :: 'a word) = take_bit (LENGTH('a)) 1"
by (simp_all add: uint_word_ariths take_bit_eq_mod)
-lemma sint_word_ariths:
+context
fixes a b :: "'a::len word"
- shows "sint (a + b) = signed_take_bit (LENGTH('a) - 1) (sint a + sint b)"
- and "sint (a - b) = signed_take_bit (LENGTH('a) - 1) (sint a - sint b)"
- and "sint (a * b) = signed_take_bit (LENGTH('a) - 1) (sint a * sint b)"
- and "sint (- a) = signed_take_bit (LENGTH('a) - 1) (- sint a)"
- and "sint (word_succ a) = signed_take_bit (LENGTH('a) - 1) (sint a + 1)"
- and "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)"
- and "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0"
- and "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1"
- subgoal
- by transfer (simp add: signed_take_bit_add)
- subgoal
- by transfer (simp add: signed_take_bit_diff)
- subgoal
- by transfer (simp add: signed_take_bit_mult)
- subgoal
- by transfer (simp add: signed_take_bit_minus)
- apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ)
- apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred)
- apply (simp_all add: sint_uint)
- done
+begin
+
+lemma sint_word_add: "sint (a + b) = signed_take_bit (LENGTH('a) - 1) (sint a + sint b)"
+ by transfer (simp add: signed_take_bit_add)
+
+lemma sint_word_diff: "sint (a - b) = signed_take_bit (LENGTH('a) - 1) (sint a - sint b)"
+ by transfer (simp add: signed_take_bit_diff)
+
+lemma sint_word_mult: "sint (a * b) = signed_take_bit (LENGTH('a) - 1) (sint a * sint b)"
+ by transfer (simp add: signed_take_bit_mult)
+
+lemma sint_word_minus: "sint (- a) = signed_take_bit (LENGTH('a) - 1) (- sint a)"
+ by transfer (simp add: signed_take_bit_minus)
+
+lemma sint_word_succ: "sint (word_succ a) = signed_take_bit (LENGTH('a) - 1) (sint a + 1)"
+ by (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ)
+
+lemma sint_word_pred: "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)"
+ by (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred)
+
+lemma sint_word_01:
+ "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0"
+ "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1"
+ by (simp_all add: sint_uint)
+
+end
+
+
+lemmas sint_word_ariths =
+ sint_word_add sint_word_diff sint_word_mult sint_word_minus
+ sint_word_succ sint_word_pred sint_word_01
lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
unfolding word_pred_m1 by simp
@@ -2831,24 +2763,14 @@
lemma mod_eq_0_imp_udvd [intro?]:
\<open>v udvd w\<close> if \<open>w mod v = 0\<close>
-proof -
- from that have \<open>unat (w mod v) = unat 0\<close>
- by simp
- then have \<open>unat w mod unat v = 0\<close>
- by (simp add: unat_mod_distrib)
- then have \<open>unat v dvd unat w\<close> ..
- then show ?thesis
- by (simp add: udvd_iff_dvd)
-qed
+ by (metis mod_0_imp_dvd that udvd_iff_dvd unat_0 unat_mod_distrib)
lemma udvd_imp_dvd:
\<open>v dvd w\<close> if \<open>v udvd w\<close> for v w :: \<open>'a::len word\<close>
proof -
from that obtain u :: \<open>'a word\<close> where \<open>unat w = unat v * unat u\<close> ..
- then have \<open>(word_of_nat (unat w) :: 'a word) = word_of_nat (unat v * unat u)\<close>
- by simp
then have \<open>w = v * u\<close>
- by simp
+ by (metis of_nat_mult of_nat_unat word_mult_def word_of_int_uint)
then show \<open>v dvd w\<close> ..
qed
@@ -2890,8 +2812,7 @@
with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1"
by (auto simp del: nat_uint_eq)
then show ?thesis
- by (simp only: unat_eq_nat_uint word_arith_wis mod_diff_right_eq)
- (metis of_int_1 uint_word_of_int unsigned_1)
+ by (metis uint_word_ariths(6) unat_eq_nat_uint word_pred_m1)
qed
lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p"
@@ -2981,7 +2902,7 @@
then unat a + unat b
else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
apply (auto simp: not_less le_iff_add)
- apply (metis (mono_tags, lifting) of_nat_add of_nat_unat take_bit_nat_eq_self_iff unsigned_less unsigned_of_nat unsigned_word_eqI)
+ using of_nat_inverse apply force
by (smt (verit, ccfv_SIG) numeral_Bit0 numerals(1) of_nat_0_le_iff of_nat_1 of_nat_add of_nat_eq_iff of_nat_power of_nat_unat uint_plus_if')
lemma unat_sub_if_size:
@@ -2996,11 +2917,12 @@
also have "\<dots> = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
by (simp add: nat_diff_distrib')
also have "\<dots> = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
- by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
+ by (simp add: nat_add_distrib nat_power_eq)
finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
}
then show ?thesis
- by (simp add: word_size) (metis nat_diff_distrib' uint_sub_if' un_ui_le unat_eq_nat_uint unsigned_greater_eq)
+ by (metis nat_diff_distrib' uint_range_size uint_sub_if' un_ui_le unat_eq_nat_uint
+ word_size)
qed
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
@@ -3144,8 +3066,7 @@
lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z"
for x z :: "'a::len word"
- by (simp add: word_less_def uint_sub_lem)
- (meson linorder_not_le uint_minus_simple_iff uint_sub_lem word_less_iff_unsigned)
+ by (meson linorder_not_le word_sub_le_iff)
lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z"
for x z :: "'a::len word"
@@ -3237,8 +3158,8 @@
by uint_arith
lemma udvd_incr_lem:
- "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
- uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
+ "\<lbrakk>up < uq; up = ua + n * uint K; uq = ua + n' * uint K\<rbrakk>
+ \<Longrightarrow> up + uint K \<le> uq"
by auto (metis int_distrib(1) linorder_not_less mult.left_neutral mult_right_mono uint_nonnegative zless_imp_add1_zle)
lemma udvd_incr':
@@ -3251,7 +3172,7 @@
assumes "p < q" "uint p = ua + n * uint K" "uint q = ua + n' * uint K"
shows "uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
proof -
- have "\<And>w wa. uint (w::'a word) \<le> uint wa + uint (w - wa)"
+ have "\<And>w v. uint (w::'a word) \<le> uint v + uint (w - v)"
by (metis (no_types) add_diff_cancel_left' diff_add_cancel uint_add_le)
moreover have "uint K + uint p \<le> uint q"
using assms by (metis (no_types) add_diff_cancel_left' diff_add_cancel udvd_incr_lem word_less_def)
@@ -3271,9 +3192,8 @@
"p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
unfolding udvd_unfold_int
- apply (simp add: uint_arith_simps split: if_split_asm)
- apply (metis (no_types, opaque_lifting) le_add_diff_inverse le_less_trans udvd_incr_lem)
- using uint_lt2p [of s] by simp
+ by (smt (verit, best) diff_add_cancel leD udvd_incr_lem uint_plus_if'
+ word_less_eq_iff_unsigned word_sub_le)
subsection \<open>Arithmetic type class instantiations\<close>
@@ -3372,13 +3292,13 @@
Abs_fnat_hom_1 word_arith_nat_div
word_arith_nat_mod
-lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
- by (fact arg_cong)
-
lemma unat_of_nat:
\<open>unat (word_of_nat x :: 'a::len word) = x mod 2 ^ LENGTH('a)\<close>
by transfer (simp flip: take_bit_eq_mod add: nat_take_bit_eq)
+lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
+ by (fact arg_cong)
+
lemmas unat_word_ariths = word_arith_nat_defs
[THEN trans [OF unat_cong unat_of_nat]]
@@ -3732,18 +3652,13 @@
lemma word_eq_reverseI:
\<open>v = w\<close> if \<open>word_reverse v = word_reverse w\<close>
-proof -
- from that have \<open>word_reverse (word_reverse v) = word_reverse (word_reverse w)\<close>
- by simp
- then show ?thesis
- by simp
-qed
+ by (metis that word_rev_rev)
lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
by (cases \<open>n < LENGTH('a)\<close>; transfer; force)
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
- by (induct n) (simp_all add: wi_hom_syms)
+ by simp
subsubsection \<open>shift functions in terms of lists of bools\<close>
@@ -3907,10 +3822,8 @@
by (metis take_bit_eq_mask take_bit_int_less_exp unsigned_take_bit_eq)
lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
- apply (auto simp flip: take_bit_eq_mask)
- apply (metis take_bit_int_eq_self_iff uint_take_bit_eq)
- apply (simp add: take_bit_int_eq_self unsigned_take_bit_eq word_uint_eqI)
- done
+ by (metis and_mask_bintr and_mask_lt_2p take_bit_int_eq_self take_bit_nonnegative
+ uint_sint word_of_int_uint)
lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 uint_0_iff)
@@ -4180,7 +4093,7 @@
assume \<open>m < LENGTH('a)\<close>
then have \<open>int (LENGTH('a) - Suc ((m + n) mod LENGTH('a))) =
int ((LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a))\<close>
- apply (simp only: of_nat_diff of_nat_mod)
+ unfolding of_nat_diff of_nat_mod
apply (simp add: Suc_le_eq add_less_le_mono of_nat_mod algebra_simps)
apply (simp only: mod_diff_left_eq [symmetric, of \<open>int LENGTH('a) * 2\<close>] mod_mult_self1_is_0 diff_0 minus_mod_int_eq)
apply (simp add: mod_simps)
@@ -4379,7 +4292,8 @@
and 4: "x' + y' = z'"
shows "(x + y) mod b = z' mod b'"
proof -
- from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
+ from 1 2[symmetric] 3[symmetric]
+ have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
by (simp add: mod_add_eq)
also have "\<dots> = (x' + y') mod b'"
by (simp add: mod_add_eq)
@@ -4481,7 +4395,7 @@
then have eq: "1 + n - m = 1 + (n - m)"
by simp
with False have "m \<le> n"
- by (metis "suc.prems" add.commute dual_order.antisym eq_iff_diff_eq_0 inc_le leI)
+ using inc_le linorder_not_le suc.prems word_le_minus_mono_left by fastforce
with False "suc.hyps" show ?thesis
using suc.IH [of "f 0 z" "f \<circ> (+) 1"]
by (simp add: word_rec_in2 eq add.assoc o_def)