author paulson Tue, 07 Apr 2020 09:35:59 +0100 changeset 71721 df68b82c818d parent 71719 23abd7f9f054 (current diff) parent 71720 1d8a1f727879 (diff) child 71723 5bbd80875e02 child 71743 0239bee6bffd
merged
```--- a/src/HOL/Binomial.thy	Mon Apr 06 22:29:40 2020 +0200
+++ b/src/HOL/Binomial.thy	Tue Apr 07 09:35:59 2020 +0100
@@ -1058,9 +1058,7 @@
done
also have "\<dots> =
(fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
-    apply (subst div_mult_div_if_dvd)
-    apply (auto simp: fact_fact_dvd_fact algebra_simps)
-    done
+    by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
finally show ?thesis
qed
@@ -1179,17 +1177,13 @@
have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
have f: "bij_betw ?f ?A ?A'"
-    apply (rule bij_betw_byWitness[where f' = tl])
-    using assms
-    apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
-    done
+    by (rule bij_betw_byWitness[where f' = tl]) (use assms in \<open>auto simp: 2 1 simp flip: length_0_conv\<close>)
have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
using assms
-    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
-        simp del: length_greater_0_conv length_0_conv)
+    by (auto simp: 2 simp flip: length_0_conv intro!: 3)
have fin: "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" for M N :: nat
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]```
```--- a/src/HOL/Real_Vector_Spaces.thy	Mon Apr 06 22:29:40 2020 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Apr 07 09:35:59 2020 +0100
@@ -62,14 +62,10 @@
and span_raw_def: span = real_vector.span
and extend_basis_raw_def: extend_basis = real_vector.extend_basis
and dim_raw_def: dim = real_vector.dim
-    apply unfold_locales
-     apply (rule scaleR_scaleR)
-    apply (rule scaleR_one)
-   apply (force simp: linear_def)
-  apply (force simp: linear_def real_scaleR_def[abs_def])
-  done
+proof unfold_locales
+  show "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+    by (force simp: linear_def real_scaleR_def[abs_def])+

hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.dependent
@@ -86,9 +82,10 @@
rewrites  "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines construct_raw_def: construct = real_vector.construct
-  apply unfold_locales
-  unfolding linear_def real_scaleR_def
-  by (rule refl)+
+proof unfold_locales
+  show "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+  unfolding linear_def real_scaleR_def by auto
+qed (auto simp: linear_def)

hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.construct
@@ -390,8 +387,7 @@
by (auto simp: Reals_def)

lemma Reals_minus_iff [simp]: "- a \<in> \<real> \<longleftrightarrow> a \<in> \<real>"
-  apply (auto simp: Reals_def)
-  by (metis add.inverse_inverse of_real_minus rangeI)
+  using Reals_minus by fastforce

lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
@@ -514,10 +510,8 @@
using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)

lemma scaleR_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
-  apply (auto intro!: scaleR_left_mono)
-  apply (rule_tac x = "inverse c *\<^sub>R xa" in image_eqI)
-   apply (simp_all add: pos_le_divideR_eq[symmetric] scaleR_scaleR scaleR_one)
-  done
+  apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
+  by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)

end

@@ -1273,13 +1267,12 @@
assume "open S"
then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
unfolding open_dist bchoice_iff ..
-    then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
+    then have *: "(\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x}) = S" (is "?S = S")
by (fastforce simp: dist_real_def)
-    show "generate_topology (range lessThan \<union> range greaterThan) S"
-      apply (subst *)
-      apply (intro generate_topology_Union generate_topology.Int)
-       apply (auto intro: generate_topology.Basis)
-      done
+    moreover have "generate_topology (range lessThan \<union> range greaterThan) ?S"
+      by (force intro: generate_topology.Basis generate_topology_Union generate_topology.Int)
+    ultimately show "generate_topology (range lessThan \<union> range greaterThan) S"
+      by simp
next
fix S :: "real set"
assume "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1548,9 +1541,10 @@

lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
-  apply standard
-  by (metis bounded mult.commute)
+proof
+  show "\<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K"
+    by (metis bounded mult.commute)

lemma comp1:
assumes "bounded_linear g"
@@ -1653,11 +1647,10 @@
qed

lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
-  apply (rule bounded_bilinear.intro)
-      apply (auto simp: algebra_simps)
-  apply (rule_tac x=1 in exI)
-  done
+proof (rule bounded_bilinear.intro)
+  show "\<exists>K. \<forall>a b::'a. norm (a * b) \<le> norm a * norm b * K"
+    by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
+qed (auto simp: algebra_simps)

lemma bounded_linear_mult_left: "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
using bounded_bilinear_mult
@@ -1678,10 +1671,10 @@
unfolding divide_inverse by (rule bounded_linear_mult_left)

lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
-  apply (rule bounded_bilinear.intro)
-      apply (auto simp: algebra_simps)
-  apply (rule_tac x=1 in exI, simp)
-  done
+proof (rule bounded_bilinear.intro)
+  show "\<exists>K. \<forall>a b. norm (a *\<^sub>R b) \<le> norm a * norm b * K"
+    using less_eq_real_def by auto
+qed (auto simp: algebra_simps)

lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
using bounded_bilinear_scaleR
@@ -1716,11 +1709,11 @@

instance real_normed_algebra_1 \<subseteq> perfect_space
proof
-  show "\<not> open {x}" for x :: 'a
-    apply (clarsimp simp: open_dist dist_norm)
-    apply (rule_tac x = "x + of_real (e/2)" in exI)
-    apply simp
-    done
+  fix x::'a
+  have "\<And>e. 0 < e \<Longrightarrow> \<exists>y. norm (y - x) < e \<and> y \<noteq> x"
+    by (rule_tac x = "x + of_real (e/2)" in exI) auto
+  then show "\<not> open {x}"
+    by (clarsimp simp: open_dist dist_norm)
qed

@@ -1793,9 +1786,11 @@
qed

lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
-  apply (clarsimp simp: filterlim_at_top)
-  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI, linarith)
-  done
+proof (clarsimp simp: filterlim_at_top)
+  fix Z
+  show "\<forall>\<^sub>F x in sequentially. Z \<le> real x"
+    by (meson eventually_sequentiallyI nat_ceiling_le_eq)
+qed

lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
proof -
@@ -1814,17 +1809,20 @@
qed

lemma filterlim_sequentially_iff_filterlim_real:
-  "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
-  apply (rule iffI)
-  subgoal using filterlim_compose filterlim_real_sequentially by blast
-  subgoal premises prems
+  "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using filterlim_compose filterlim_real_sequentially by blast
+next
+  assume R: ?rhs
+  show ?lhs
proof -
have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
by (intro filterlim_compose[OF filterlim_nat_sequentially]
-          filterlim_compose[OF filterlim_floor_sequentially] prems)
+          filterlim_compose[OF filterlim_floor_sequentially] R)
then show ?thesis by simp
qed
-  done
+qed

subsubsection \<open>Limits of Sequences\<close>
@@ -1899,10 +1897,8 @@
shows "f \<midarrow>a\<rightarrow> l"
proof -
have "\<And>S. \<lbrakk>open S; l \<in> S; \<forall>\<^sub>F x in at a. g x \<in> S\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at a. f x \<in> S"
-    apply (clarsimp simp add: eventually_at)
-    apply (rule_tac x="min d R" in exI)
-     apply (auto simp: assms)
-    done
+    by (metis assms(2) assms(3) dual_order.strict_trans linorder_neqE_linordered_idom)
then show ?thesis
using assms by (simp add: tendsto_def)
qed
@@ -2171,16 +2167,19 @@
have "dist (u n) l \<le> dist (u n) ((u \<circ> r) n) + dist ((u \<circ> r) n) l"
by (rule dist_triangle)
also have "\<dots> < e/2 + e/2"
-        using N1[of n "r n"] N2[of n] that unfolding comp_def
-        by (auto simp: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
+        show "dist (u n) ((u \<circ> r) n) < e / 2"
+          using N1[of n "r n"] N2[of n] that unfolding comp_def
+          by (meson assms(2) le_trans max.bounded_iff strict_mono_imp_increasing)
+        show "dist ((u \<circ> r) n) l < e / 2"
+          using N2 that by auto
+      qed
finally show ?thesis by simp
qed
then show ?thesis unfolding eventually_sequentially by blast
qed
have "(\<lambda>n. dist (u n) l) \<longlonglongrightarrow> 0"
-    apply (rule order_tendstoI)
-    using * by auto (meson eventually_sequentiallyI less_le_trans zero_le_dist)
+    by (simp add: less_le_trans * order_tendstoI)
then show ?thesis using tendsto_dist_iff by auto
qed
```