author paulson Tue, 01 Sep 2020 22:01:27 +0100 changeset 72463 11b81cd70633 parent 72462 6b620d91e8cc child 72468 a77ac58b1d96
de-applying
```--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Aug 31 17:18:47 2020 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Sep 01 22:01:27 2020 +0100
@@ -174,16 +174,8 @@
using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp

lemma one_less_of_natD:
-  "(1::'a::linordered_semidom) < of_nat n \<Longrightarrow> 1 < n"
-  using zero_le_one[where 'a='a]
-  apply (cases n)
-  apply simp
-  subgoal for n'
-    apply (cases n')
-    apply simp
-    apply simp
-    done
-  done
+  assumes "(1::'a::linordered_semidom) < of_nat n" shows "1 < n"
+  by (cases n) (use assms in auto)

subsection \<open>Defining the extended non-negative reals\<close>

@@ -353,8 +345,7 @@
apply (subst (2) rel_fun_def)
apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
apply (subst (asm) max.absorb2)
-    apply (rule SUP_upper2)
-    apply auto
+    apply (auto intro: SUP_upper2)
done
qed

@@ -369,10 +360,7 @@
by (induction n) (auto simp: zero_ennreal.rep_eq one_ennreal.rep_eq plus_ennreal.rep_eq)

lemma enn2ereal_numeral[simp]: "enn2ereal (numeral a) = numeral a"
-  apply (subst of_nat_numeral[of a, symmetric])
-  apply (subst enn2ereal_of_nat)
-  apply simp
-  done
+  by (metis enn2ereal_of_nat numeral_eq_ereal of_nat_numeral)

lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
unfolding cr_ennreal_def pcr_ennreal_def by auto
@@ -543,10 +531,7 @@
by transfer (auto simp: top_ereal_def max_def)

lemma minus_top_ennreal: "x - top = (if x = top then top else 0:: ennreal)"
-  apply transfer
-  subgoal for x
-    by (cases x) (auto simp: top_ereal_def max_def)
-  done
+  by transfer (use ereal_eq_minus_iff top_ereal_def in force)

lemma bot_ennreal: "bot = (0::ennreal)"
by transfer rule
@@ -585,12 +570,7 @@

fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (x + y) - y = x"
-  apply transfer
-  subgoal for x y
-    apply (cases x y rule: ereal2_cases)
-    apply (auto split: split_max simp: top_ereal_def)
-    done
-  done
+  by transfer (metis ereal_eq_minus_iff max_absorb2 not_MInfty_nonneg top_ereal_def)

fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (y + x) - y = x"
@@ -599,12 +579,7 @@
lemma
fixes a b :: ennreal
shows "a - b = 0 \<Longrightarrow> a \<le> b"
-  apply transfer
-  subgoal for a b
-    apply (cases a b rule: ereal2_cases)
-    apply (auto simp: not_le max_def split: if_splits)
-    done
-  done
+  by transfer (metis ereal_diff_gr0 le_cases max.absorb2 not_less)

lemma ennreal_minus_cancel:
fixes a b c :: ennreal
@@ -618,12 +593,7 @@
fixes a b c :: "ennreal"
shows "sup (c + a) (c + b) = c + sup a b"
-  apply transfer
-  subgoal for a b c
-    apply (cases a b c rule: ereal3_cases)
-    apply (auto simp flip: ereal_max)
-    done
-  done
+  by transfer (metis add_left_mono le_cases sup.absorb2 sup.orderE)

fixes a b c :: ennreal
@@ -668,12 +638,7 @@

lemma ennreal_minus_eq_0:
"a - b = 0 \<Longrightarrow> a \<le> (b::ennreal)"
-  apply transfer
-  subgoal for a b
-    apply (cases a b rule: ereal2_cases)
-    apply (auto simp: zero_ereal_def max.absorb2 simp flip: ereal_max)
-    done
-  done
+  by transfer (metis ereal_diff_gr0 le_cases max.absorb2 not_less)

lemma ennreal_mono_minus_cancel:
fixes a b c :: ennreal
@@ -684,20 +649,12 @@
lemma ennreal_mono_minus:
fixes a b c :: ennreal
shows "c \<le> b \<Longrightarrow> a - b \<le> a - c"
-  apply transfer
-  apply (rule max.mono)
-  apply simp
-  subgoal for a b c
-    by (cases a b c rule: ereal3_cases) auto
-  done
+  by transfer (meson ereal_minus_mono max.mono order_refl)

lemma ennreal_minus_pos_iff:
fixes a b :: ennreal
shows "a < top \<or> b < top \<Longrightarrow> 0 < a - b \<Longrightarrow> b < a"
-  apply transfer
-  subgoal for a b
-    by (cases a b rule: ereal2_cases) (auto simp: less_max_iff_disj)
-  done
+  by transfer (use add.left_neutral ereal_minus_le_iff less_irrefl not_less in fastforce)

lemma ennreal_inverse_top[simp]: "inverse top = (0::ennreal)"
by transfer (simp add: top_ereal_def ereal_inverse_eq_0)
@@ -795,10 +752,7 @@
fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b - a + a = b"
unfolding infinity_ennreal_def
-  apply transfer
-  subgoal for a b
-    by (cases a b rule: ereal2_cases) (auto simp: max_absorb2)
-  done

lemma ennreal_diff_self[simp]: "a \<noteq> top \<Longrightarrow> a - a = (0::ennreal)"
@@ -806,12 +760,7 @@
lemma ennreal_minus_mono:
fixes a b c :: ennreal
shows "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> c - d"
-  apply transfer
-  apply (rule max.mono)
-  apply simp
-  subgoal for a b c d
-    by (cases a b c d rule: ereal3_cases[case_product ereal_cases]) auto
-  done
+  by transfer (meson ereal_minus_mono max.mono order_refl)

lemma ennreal_minus_eq_top[simp]: "a - (b::ennreal) = top \<longleftrightarrow> a = top"
by transfer (auto simp: top_ereal_def max.absorb2 ereal_minus_eq_PInfty_iff split: split_max)
@@ -1035,10 +984,11 @@
(auto simp: ennreal_mult prod_nonneg)

lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
-  apply (cases "0 \<le> c")
-  apply (cases a b rule: ennreal2_cases)
-  apply (auto simp: ennreal_mult[symmetric] ennreal_neg ennreal_top_mult)
-  done
+proof (cases "0 \<le> c")
+  case True
+  then show ?thesis
+    by (metis ennreal_eq_0_iff ennreal_mult_right_cong ennreal_neq_top mult_divide_eq_ennreal)
+qed (use ennreal_neg in auto)

lemma ennreal_le_epsilon:
"(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
@@ -1246,17 +1196,17 @@

lemma sup_continuous_e2ennreal[order_continuous_intros]:
assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
-  apply (rule sup_continuous_compose[OF _ f])
-  apply (rule continuous_at_left_imp_sup_continuous)
-  apply (auto simp: mono_def e2ennreal_mono continuous_at_e2ennreal)
-  done
+proof (rule sup_continuous_compose[OF _ f])
+  show "sup_continuous e2ennreal"
+    by (simp add: continuous_at_e2ennreal continuous_at_left_imp_sup_continuous e2ennreal_mono mono_def)
+qed

lemma sup_continuous_enn2ereal[order_continuous_intros]:
assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. enn2ereal (f x))"
-  apply (rule sup_continuous_compose[OF _ f])
-  apply (rule continuous_at_left_imp_sup_continuous)
-  apply (simp_all add: mono_def less_eq_ennreal.rep_eq continuous_at_enn2ereal)
-  done
+proof (rule sup_continuous_compose[OF _ f])
+  show "sup_continuous enn2ereal"
+  by (simp add: continuous_at_enn2ereal continuous_at_left_imp_sup_continuous less_eq_ennreal.rep_eq mono_def)
+qed

lemma sup_continuous_mult_left_ennreal':
fixes c :: "ennreal"
@@ -1308,13 +1258,14 @@
assumes lim: "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
assumes *: "\<forall>\<^sub>F x in F. 0 \<le> f x" and x: "0 \<le> x"
shows "(f \<longlongrightarrow> x) F"
-  using continuous_on_tendsto_compose[OF continuous_on_enn2ereal lim]
-  apply simp
-  apply (subst (asm) tendsto_cong)
-  using *
-  apply eventually_elim
-  apply (auto simp: max_absorb2 \<open>0 \<le> x\<close>)
-  done
+proof -
+  have "((\<lambda>x. enn2ereal (ennreal (f x))) \<longlongrightarrow> enn2ereal (ennreal x)) F
+    \<longleftrightarrow> (f \<longlongrightarrow> enn2ereal (ennreal x)) F"
+    using "*" eventually_mono
+    by (intro tendsto_cong) fastforce
+  then show ?thesis
+    using assms(1) continuous_at_enn2ereal isCont_tendsto_compose x by fastforce
+qed

lemma tendsto_ennreal_iff[simp]:
"\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
@@ -1584,10 +1535,7 @@
apply transfer
subgoal for A
using Sup_countable_SUP[of A]
-    apply (clarsimp simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
-    subgoal for f
-      by (intro exI[of _ f]) auto
-    done
+    by (force simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
done

lemma ennreal_Inf_countable_INF:
@@ -1645,13 +1593,12 @@
done

-lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *)
+lemma ennreal_SUP_const_minus:
fixes f :: "'a \<Rightarrow> ennreal"
shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x\<in>I. c - f x) = c - (SUP x\<in>I. f x)"
apply (transfer fixing: I)
unfolding ex_in_conv[symmetric]
-  apply (auto simp add: sup_max[symmetric] SUP_upper2 sup_absorb2
-              simp del: sup_ereal_def)
+  apply (auto simp add: SUP_upper2 sup_absorb2 simp flip: sup_ereal_def)
apply (subst INF_ereal_minus_right[symmetric])
apply (auto simp del: sup_ereal_def simp add: sup_INF)
done
@@ -1725,8 +1672,7 @@
lemma ennreal_approx_unit:
"(\<And>a::ennreal. 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * z \<le> y) \<Longrightarrow> z \<le> y"
apply (subst SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z, simplified])
-  apply (rule SUP_least)
-  apply auto
+  apply (auto intro: SUP_least)
done

lemma suminf_ennreal2:
@@ -1804,7 +1750,7 @@
subsection \<open>\<^typ>\<open>ennreal\<close> theorems\<close>

lemma neq_top_trans: fixes x y :: ennreal shows "\<lbrakk> y \<noteq> top; x \<le> y \<rbrakk> \<Longrightarrow> x \<noteq> top"
-by (auto simp: top_unique)
+  by (auto simp: top_unique)

lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus top_unique)
@@ -2012,8 +1958,6 @@
assumes "(u \<longlongrightarrow> ennreal l) F" "l \<ge> 0"
shows "((\<lambda>n. enn2real (u n)) \<longlongrightarrow> l) F"
unfolding enn2real_def
-  apply (intro tendsto_intros)
-  apply (subst enn2ereal_ennreal[symmetric])
-  by (intro tendsto_intros assms)+
+  by (metis assms enn2ereal_ennreal lim_real_of_ereal tendsto_enn2erealI)

end```
```--- a/src/HOL/Library/Extended_Real.thy	Mon Aug 31 17:18:47 2020 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 01 22:01:27 2020 +0100
@@ -133,10 +133,7 @@
next
case (Suc n')
then have "{enat n} = {enat n' <..< enat (Suc n)}"
-    apply auto
-    apply (case_tac x)
-    apply auto
-    done
+    using enat_iless by (fastforce simp: set_eq_iff)
then show ?thesis
by simp
qed
@@ -147,10 +144,7 @@
proof safe
assume "\<infinity> \<notin> A"
then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n})"
-    apply auto
-    apply (case_tac x)
-    apply auto
-    done
+    by (simp add: set_eq_iff) (metis not_enat_eq)
moreover have "open \<dots>"
by (auto intro: open_enat)
ultimately show "open A"
@@ -158,10 +152,7 @@
next
fix n assume "{enat n <..} \<subseteq> A"
then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n}) \<union> {enat n <..}"
-    apply auto
-    apply (case_tac x)
-    apply auto
-    done
+    using enat_ile leI by (simp add: set_eq_iff) blast
moreover have "open \<dots>"
by (intro open_Un open_UN ballI open_enat open_greaterThan)
ultimately show "open A"
@@ -191,12 +182,14 @@
lemma nhds_enat: "nhds x = (if x = \<infinity> then INF i. principal {enat i..} else principal {x})"
proof auto
show "nhds \<infinity> = (INF i. principal {enat i..})"
-    unfolding nhds_def
-    apply (auto intro!: antisym INF_greatest simp add: open_enat_iff cong: rev_conj_cong)
-    apply (auto intro!: INF_lower Ioi_le_Ico) []
-    subgoal for x i
-      by (auto intro!: INF_lower2[of "Suc i"] simp: subset_eq Ball_def eSuc_enat Suc_ile_eq)
-    done
+  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)
+    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)
+  qed
show "nhds (enat i) = principal {enat i}" for i
qed
@@ -594,14 +587,10 @@

fixes a b c d :: ereal
-  assumes "a < b"
-    and "c < d"
+  assumes "a < b" and "c < d"
shows "a + c < b + d"
-using assms
-apply (cases a)
-apply (cases rule: ereal3_cases[of b c d], auto)
-apply (cases rule: ereal3_cases[of b c d], auto)
-done
+  using assms
+  by (cases a; force simp add: elim: less_ereal.elims)

lemma ereal_minus_le_minus[simp]:
fixes a b :: ereal
@@ -1036,12 +1025,13 @@

lemma ereal_mult_right_mono:
fixes a b c :: ereal
-  shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-  apply (cases "c = 0")
-  apply simp
-  apply (cases rule: ereal3_cases[of a b c])
-  apply (auto simp: zero_le_mult_iff)
-  done
+  assumes "a \<le> b" "0 \<le> c"
+  shows "a * c \<le> b * c"
+proof (cases "c = 0")
+  case False
+  with assms show ?thesis
+    by (cases rule: ereal3_cases[of a b c]) auto
+qed auto

lemma ereal_mult_left_mono:
fixes a b c :: ereal
@@ -1076,7 +1066,7 @@
fixes a b c d::ereal
assumes "a > 0" "c > 0" "a < b" "c < d"
shows "a * c < b * d"
-apply (rule ereal_mult_mono_strict, auto simp add: assms) using assms by auto
+  using assms ereal_mult_mono_strict by auto

lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"
@@ -1134,14 +1124,19 @@
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
-  apply (induct w rule: num_induct)
-  apply (simp only: numeral_One one_ereal_def)
-  apply (simp only: numeral_inc ereal_plus_1)
-  done
+proof (induct w rule: num_induct)
+  case One
+  then show ?case
+    by simp
+next
+  case (inc x)
+  then show ?case
+    by (simp add: inc numeral_inc)
+qed

lemma distrib_left_ereal_nn:
"c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c"
-by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)
+  by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)

lemma sum_ereal_right_distrib:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1158,79 +1153,32 @@

lemma ereal_le_epsilon:
fixes x y :: ereal
-  assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
+  assumes "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
shows "x \<le> y"
-proof -
-  {
-    assume a: "\<exists>r. y = ereal r"
-    then obtain r where r_def: "y = ereal r"
-      by auto
-    {
-      assume "x = -\<infinity>"
-      then have ?thesis by auto
-    }
-    moreover
-    {
-      assume "x \<noteq> -\<infinity>"
-      then obtain p where p_def: "x = ereal p"
-      using a assms[rule_format, of 1]
-        by (cases x) auto
-      {
-        fix e
-        have "0 < e \<longrightarrow> p \<le> r + e"
-          using assms[rule_format, of "ereal e"] p_def r_def by auto
-      }
-      then have "p \<le> r"
-        apply (subst field_le_epsilon)
-        apply auto
-        done
-      then have ?thesis
-        using r_def p_def by auto
-    }
-    ultimately have ?thesis
-      by blast
-  }
-  moreover
-  {
-    assume "y = -\<infinity> \<or> y = \<infinity>"
-    then have ?thesis
-      using assms[rule_format, of 1] by (cases x) auto
-  }
-  ultimately show ?thesis
-    by (cases y) auto
+proof (cases "x = -\<infinity> \<or> x = \<infinity> \<or> y = -\<infinity> \<or> y = \<infinity>")
+  case True
+  then show ?thesis
+    using assms[of 1] by auto
+next
+  case False
+  then obtain p q where "x = ereal p" "y = ereal q"
+    by (metis MInfty_eq_minfinity ereal.distinct(3) uminus_ereal.elims)
+  then show ?thesis
+    by (metis assms field_le_epsilon ereal_less(2) ereal_less_eq(3) plus_ereal.simps(1))
qed

lemma ereal_le_epsilon2:
fixes x y :: ereal
-  assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e"
+  assumes "\<And>e::real. 0 < e \<Longrightarrow> x \<le> y + ereal e"
shows "x \<le> y"
-proof -
-  {
-    fix e :: ereal
-    assume "e > 0"
-    {
-      assume "e = \<infinity>"
-      then have "x \<le> y + e"
-        by auto
-    }
-    moreover
-    {
-      assume "e \<noteq> \<infinity>"
-      then obtain r where "e = ereal r"
-        using \<open>e > 0\<close> by (cases e) auto
-      then have "x \<le> y + e"
-        using assms[rule_format, of r] \<open>e>0\<close> by auto
-    }
-    ultimately have "x \<le> y + e"
-      by blast
-  }
-  then show ?thesis
-    using ereal_le_epsilon by auto
+proof (rule ereal_le_epsilon)
+  show "\<And>\<epsilon>::ereal. 0 < \<epsilon> \<Longrightarrow> x \<le> y + \<epsilon>"
+  using assms less_ereal.elims(2) zero_less_real_of_ereal by fastforce
qed

lemma ereal_le_real:
fixes x y :: ereal
-  assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z"
+  assumes "\<And>z. x \<le> ereal z \<Longrightarrow> y \<le> ereal z"
shows "y \<le> x"
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)

@@ -1240,10 +1188,7 @@
proof (cases "finite A")
case True
then show ?thesis by (induct A) auto
-next
-  case False
-  then show ?thesis by auto
-qed
+qed auto

lemma prod_ereal_pos:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1253,10 +1198,7 @@
case True
from this pos show ?thesis
by induct auto
-next
-  case False
-  then show ?thesis by simp
-qed
+qed auto

lemma prod_PInf:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1278,10 +1220,7 @@
using insert by (auto simp: prod_ereal_0)
finally show ?case .
qed simp
-next
-  case False
-  then show ?thesis by simp
-qed
+qed auto

lemma prod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (prod f A)"
proof (cases "finite A")
@@ -1478,13 +1417,7 @@
and "0 < e"
shows "x - e < x"
and "x < x + e"
-  using assms
-  apply (cases x, cases e)
-  apply auto
-  using assms
-  apply (cases x, cases e)
-  apply auto
-  done
+  using assms  by (cases x, cases e, auto)+

lemma ereal_minus_eq_PInfty_iff:
fixes x y :: ereal
@@ -1494,28 +1427,28 @@
fixes x y z :: ereal
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> 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

fixes x y z :: ereal
shows "x + y - z = x - z + y"
-by(cases x y z rule: ereal3_cases) simp_all
+  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(cases x y rule: ereal2_cases) simp_all

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"
-by(cases x y rule: ereal2_cases) simp_all
+  by(cases x y rule: ereal2_cases) simp_all

lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
-by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
+  by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma ereal_abs_diff:
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)

subsubsection \<open>Division\<close>
@@ -1843,17 +1776,10 @@
instance
proof
show "Sup {} = (bot::ereal)"
-    apply (auto simp: bot_ereal_def Sup_ereal_def)
-    apply (rule some1_equality)
-    apply (metis ereal_bot ereal_less_eq(2))
-    apply (metis ereal_less_eq(2))
-    done
+    using ereal_bot by (auto simp: bot_ereal_def Sup_ereal_def)
show "Inf {} = (top::ereal)"
-    apply (auto simp: top_ereal_def Inf_ereal_def)
-    apply (rule some1_equality)
-    apply (metis ereal_top ereal_less_eq(1))
-    apply (metis ereal_less_eq(1))
-    done
+    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)

@@ -1868,51 +1794,35 @@
qed

lemma min_PInf [simp]: "min (\<infinity>::ereal) x = x"
-by (metis min_top top_ereal_def)
+  by (metis min_top top_ereal_def)

lemma min_PInf2 [simp]: "min x (\<infinity>::ereal) = x"
-by (metis min_top2 top_ereal_def)
+  by (metis min_top2 top_ereal_def)

lemma max_PInf [simp]: "max (\<infinity>::ereal) x = \<infinity>"
-by (metis max_top top_ereal_def)
+  by (metis max_top top_ereal_def)

lemma max_PInf2 [simp]: "max x (\<infinity>::ereal) = \<infinity>"
-by (metis max_top2 top_ereal_def)
+  by (metis max_top2 top_ereal_def)

lemma min_MInf [simp]: "min (-\<infinity>::ereal) x = -\<infinity>"
-by (metis min_bot bot_ereal_def)
+  by (metis min_bot bot_ereal_def)

lemma min_MInf2 [simp]: "min x (-\<infinity>::ereal) = -\<infinity>"
-by (metis min_bot2 bot_ereal_def)
+  by (metis min_bot2 bot_ereal_def)

lemma max_MInf [simp]: "max (-\<infinity>::ereal) x = x"
-by (metis max_bot bot_ereal_def)
+  by (metis max_bot bot_ereal_def)

lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
-by (metis max_bot2 bot_ereal_def)
+  by (metis max_bot2 bot_ereal_def)

subsection \<open>Extended real intervals\<close>

lemma real_greaterThanLessThan_infinity_eq:
"real_of_ereal ` {N::ereal<..<\<infinity>} =
(if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
-proof -
-  {
-    fix x::real
-    have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
-      by (auto intro!: image_eqI[where x="ereal x"])
-  } moreover {
-    fix x::ereal
-    assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
-    then have "real_of_ereal N < real_of_ereal x"
-      by (cases N; cases x; simp)
-  } moreover {
-    fix x::real
-    assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
-    then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
-      by (cases N) (auto intro!: image_eqI[where x="ereal x"])
-  } ultimately show ?thesis by auto
-qed
+  by (force simp: real_less_ereal_iff intro!: image_eqI[where x="ereal _"] elim!: less_ereal.elims)

lemma real_greaterThanLessThan_minus_infinity_eq:
"real_of_ereal ` {-\<infinity><..<N::ereal} =
@@ -1926,12 +1836,7 @@

lemma real_greaterThanLessThan_inter:
"real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
-  apply safe
-  subgoal by force
-  subgoal by force
-  subgoal for x y z
-    by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
-  done
+  by (force elim!: less_ereal.elims)

lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
(if N = \<infinity> then {} else
@@ -1942,11 +1847,19 @@
else if M = - \<infinity> then {}
else if M = \<infinity> then {real_of_ereal N<..}
else {real_of_ereal N <..< real_of_ereal M})"
-  apply (subst real_greaterThanLessThan_inter)
-  apply (subst real_greaterThanLessThan_minus_infinity_eq)
-  apply (subst real_greaterThanLessThan_infinity_eq)
-  apply auto
-  done
+proof (cases "M = -\<infinity> \<or> M = \<infinity> \<or> N = -\<infinity> \<or> N = \<infinity>")
+  case True
+  then show ?thesis
+    by (auto simp: real_greaterThanLessThan_minus_infinity_eq real_greaterThanLessThan_infinity_eq )
+next
+  case False
+  then obtain p q where "M = ereal p" "N = ereal q"
+    by (metis MInfty_eq_minfinity ereal.distinct(3) uminus_ereal.elims)
+  moreover have "\<And>x. \<lbrakk>q < x; x < p\<rbrakk> \<Longrightarrow> x \<in> real_of_ereal ` {ereal q<..<ereal p}"
+    by (metis greaterThanLessThan_iff imageI less_ereal.simps(1) real_of_ereal.simps(1))
+  ultimately show ?thesis
+    by (auto elim!: less_ereal.elims)
+qed

lemma real_image_ereal_ivl:
fixes a b::ereal
@@ -2033,31 +1946,32 @@
assumes "t \<notin> real_of_ereal ` {a<..<b}"
assumes "s \<le> t"
shows "b \<noteq> \<infinity>"
-  using assms
-  apply (cases b)
-  subgoal by force
-  subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
-    ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
-    image_eqI less_imp_le linordered_field_no_ub not_less order_trans
-    real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
-  subgoal by force
-  done
+proof (cases b)
+  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)
+qed auto

lemma real_ereal_bound_lemma_down:
-  assumes "s \<in> real_of_ereal ` {a<..<b}"
-  assumes "t \<notin> real_of_ereal ` {a<..<b}"
-  assumes "t \<le> s"
+  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>"
-  using assms
-  apply (cases b)
-  subgoal
-    apply safe
-    using assms(1)
-    apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
-    done
-  subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
-  subgoal by auto
-  done
+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

subsection "Topological space"
@@ -2081,14 +1995,15 @@
using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]

-lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) \<longlongrightarrow> - x) F"
-  apply (rule tendsto_compose[where g=uminus])
-  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
-  apply (rule_tac x="{..< -a}" in exI)
-  apply (auto split: ereal.split simp: ereal_less_uminus_reorder) []
-  apply (rule_tac x="{- a <..}" in exI)
-  apply (auto split: ereal.split simp: ereal_uminus_reorder) []
-  done
+lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]:
+  assumes "(f \<longlongrightarrow> x) F"
+  shows "((\<lambda>x. - f x::ereal) \<longlongrightarrow> - x) F"
+proof (rule tendsto_compose[OF order_tendstoI assms])
+  show "\<And>a. a < - x \<Longrightarrow> \<forall>\<^sub>F x in at x. a < - x"
+    by (metis ereal_less_uminus_reorder eventually_at_topological lessThan_iff open_lessThan)
+  show "\<And>a. - x < a \<Longrightarrow> \<forall>\<^sub>F x in at x. - x < a"
+    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
@@ -2384,7 +2299,7 @@
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 (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
+   apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
@@ -2711,38 +2626,22 @@
unfolding open_generated_order[where 'a=real]
proof (induct rule: generate_topology.induct)
case (Basis S)
-  moreover {
-    fix x
-    have "ereal ` {..< x} = { -\<infinity> <..< ereal x }"
-      apply auto
-      apply (case_tac xa)
-      apply auto
-      done
-  }
-  moreover {
-    fix x
-    have "ereal ` {x <..} = { ereal x <..< \<infinity> }"
-      apply auto
-      apply (case_tac xa)
-      apply auto
-      done
-  }
+  moreover have "\<And>x. ereal ` {..< x} = { -\<infinity> <..< ereal x }"
+    using ereal_less_ereal_Ex by auto
+  moreover have "\<And>x. ereal ` {x <..} = { ereal x <..< \<infinity> }"
+    using less_ereal.elims(2) by fastforce
ultimately show ?case
-     by auto
+    by auto
qed (auto simp add: image_Union image_Int)

lemma open_image_real_of_ereal:
fixes X::"ereal set"
assumes "open X"
-  assumes "\<infinity> \<notin> X"
-  assumes "-\<infinity> \<notin> X"
+  assumes infty: "\<infinity> \<notin> X" "-\<infinity> \<notin> X"
shows "open (real_of_ereal ` X)"
proof -
have "real_of_ereal ` X = ereal -` X"
-    apply safe
-    subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
-    subgoal using image_iff by fastforce
-    done
+    using infty ereal_real by (force simp: set_eq_iff)
thus ?thesis
by (auto intro!: open_ereal_vimage assms)
qed
@@ -3452,13 +3351,15 @@

fixes f g :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-    and "\<And>i. 0 \<le> g i"
+  assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
-  apply (subst (1 2 3) suminf_ereal_eq_SUP)
-  unfolding sum.distrib
-  done
+proof -
+  have "(SUP n. \<Sum>i<n. f i + g i) = (SUP n. sum f {..<n}) + (SUP n. sum g {..<n})"
+    unfolding sum.distrib
+  with assms show ?thesis
+    by (subst (1 2 3) suminf_ereal_eq_SUP) auto
+qed

lemma suminf_cmult_ereal:
fixes f g :: "nat \<Rightarrow> ereal"
@@ -3602,20 +3503,13 @@
and "\<And>n i. 0 \<le> f n i"
shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
proof -
-  {
-    fix n :: nat
-    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
-      using assms
-      by (auto intro!: SUP_ereal_sum [symmetric])
-  }
-  note * = this
+  have *: "\<And>n. (\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
+    using assms
+    by (auto intro!: SUP_ereal_sum [symmetric])
show ?thesis
using assms
apply (subst (1 2) suminf_ereal_eq_SUP)
-    unfolding *
-    apply (auto intro!: SUP_upper2)
-    apply (subst SUP_commute)
-    apply rule
+    apply (auto intro!: SUP_upper2 SUP_commute simp: *)
done
qed

@@ -3764,10 +3658,7 @@
show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n\<in>I. f n i)"
using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
show "(SUP n. \<Sum>i<n. SUP n\<in>I. f n i) = (SUP n\<in>I. SUP j. \<Sum>i<j. f n i)"
-    apply (subst SUP_commute)
-    apply (subst SUP_ereal_sum_directed)
-    apply (auto intro!: assms simp: finite_subset)
-    done
+    by (auto simp: finite_subset SUP_commute SUP_ereal_sum_directed assms)
qed

lemma ereal_dense3:
@@ -3821,13 +3712,11 @@
and t: "\<bar>t\<bar> \<noteq> \<infinity>"
shows "open ((\<lambda>x. m * x + t) ` S)"
proof -
-  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
+  have "continuous_on UNIV (\<lambda>x. inverse m * (x + - t))"
using m t
-    apply (intro open_vimage \<open>open S\<close>)
-    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
-    apply auto
-    done
+    by (intro continuous_at_imp_continuous_on ballI continuous_at[THEN iffD2]; force)
+  then have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
+    using \<open>open S\<close> open_vimage by blast
also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
using m t by (auto simp: divide_ereal_def mult.commute minus_ereal_def
simp flip: uminus_ereal.simps)
@@ -3902,8 +3791,7 @@
proof -
from 1 2 have "limsup X \<le> liminf X" by auto
hence 3: "limsup X = liminf X"
-    apply (subst eq_iff, rule conjI)
-    by (rule Liminf_le_Limsup, auto)
+    by (simp add: Liminf_le_Limsup order_class.order.antisym)
hence 4: "convergent (\<lambda>n. ereal (X n))"
by (subst convergent_ereal)
hence "limsup X = lim (\<lambda>n. ereal(X n))"
@@ -3911,8 +3799,7 @@
also from 1 2 3 have "limsup X = L" by auto
finally have "lim (\<lambda>n. ereal(X n)) = L" ..
hence "(\<lambda>n. ereal (X n)) \<longlonglongrightarrow> L"
-    apply (elim subst)
-    by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
+    using "4" convergent_LIMSEQ_iff by force
thus ?thesis by simp
qed

@@ -3954,13 +3841,8 @@
next
case (real r)
then show ?thesis
-    unfolding liminf_SUP_INF limsup_INF_SUP
-    apply (subst INF_ereal_minus_right)
-    apply auto
-    apply (subst SUP_ereal_minus_right)
-    apply auto
-    done
-qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
+    by (simp add: liminf_SUP_INF limsup_INF_SUP INF_ereal_minus_right SUP_ereal_minus_right)
+qed (use \<open>c \<noteq> -\<infinity>\<close> in simp)

subsubsection \<open>Continuity\<close>
@@ -4055,39 +3937,20 @@

lemma continuous_on_iff_real:
fixes f :: "'a::t2_space \<Rightarrow> ereal"
-  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
shows "continuous_on A f \<longleftrightarrow> continuous_on A (real_of_ereal \<circ> f)"
-proof -
+proof
+  assume L: "continuous_on A f"
have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
using assms by force
-  then have *: "continuous_on (f ` A) real_of_ereal"
-    using continuous_on_real by (simp add: continuous_on_subset)
-  have **: "continuous_on ((real_of_ereal \<circ> f) ` A) ereal"
-    by (intro continuous_on_ereal continuous_on_id)
-  {
-    assume "continuous_on A f"
-    then have "continuous_on A (real_of_ereal \<circ> f)"
-      apply (subst continuous_on_compose)
-      using *
-      apply auto
-      done
-  }
-  moreover
-  {
-    assume "continuous_on A (real_of_ereal \<circ> f)"
-    then have "continuous_on A (ereal \<circ> (real_of_ereal \<circ> f))"
-      apply (subst continuous_on_compose)
-      using **
-      apply auto
-      done
-    then have "continuous_on A f"
-      apply (subst continuous_on_cong[of _ A _ "ereal \<circ> (real_of_ereal \<circ> f)"])
-      using assms ereal_real
-      apply auto
-      done
-  }
-  ultimately show ?thesis
-    by auto
+  then show "continuous_on A (real_of_ereal \<circ> f)"
+    by (meson L continuous_on_compose continuous_on_real continuous_on_subset)
+next
+  assume R: "continuous_on A (real_of_ereal \<circ> f)"
+  then have "continuous_on A (ereal \<circ> (real_of_ereal \<circ> f))"
+    by (meson continuous_at_iff_ereal continuous_on_eq_continuous_within)
+  then show "continuous_on A f"
+    using assms ereal_real' by auto
qed

lemma continuous_uminus_ereal [continuous_intros]: "continuous_on (A :: ereal set) uminus"
@@ -4149,7 +4012,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_left:
assumes "F \<noteq> bot" "(c::real) \<ge> 0"
@@ -4321,10 +4184,7 @@

lemma continuous_on_diff_ereal:
"continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>g x\<bar> \<noteq> \<infinity>) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ereal)"
-  apply (auto simp: continuous_on_def)
-  apply (intro tendsto_diff_ereal)
-  apply metis+
-  done
+  by (auto simp: tendsto_diff_ereal continuous_on_def)

subsubsection \<open>Tests for code generator\<close>```